Processor design verification
AssigneeOracle International Corporation
InventorsPaul N. Loewenstein, Basant Vinaik
Life of this patent
Estimating the term…
Abstract
A system and method for verifying that a processor design having caches conforms to a specific memory model. The caches might not be maintained coherent in real time. Specifically, the system and method make use of a checker that conforms to the memory model, a time-stamping scheme, and a store buffering scheme to identify a bug(s) in the processor design that violates the memory model and/or loads an incorrect value in response to a load instruction.
Claims20
A method for verifying that a processor design conforms with a memory model, comprising:
- receiving, from a simulation of the processor design and by a checker conforming to the memory model, a memory-committed (MC) confirmation for a load instruction executed by a strand in the processor design;
- obtaining, by the checker and in response to the MC confirmation for the load instruction, a load timestamp associated with the load instruction and a plurality of caches in the processor design;
- inserting, into a load queue of the checker corresponding to the strand, a load entry comprising the load timestamp in response to the MC confirmation for the load instruction;
- receiving, by the checker and after inserting the load entry into the load queue, a strand-committed (SC) confirmation for the load instruction from the simulation of the processor design;
- determining, by the checker and in response to the SC confirmation for the load instruction, a snapshot for the load instruction based on the load timestamp;
- obtaining a load value for the load instruction from the simulation of the processor design;
- and
- determining an error in the processor design by comparing the load value and the snapshot.
A system for verifying that a processor design conforms with a memory model, the system comprising:
- a simulation of the processor design comprising:
- a plurality of caches;
- and
- a strand configured to obtain a load value by executing a load instruction;
- a timestamp engine configured to generate a load timestamp in response to a memory-committed (MC) confirmation for the load instruction from the simulation;
- a checker conforming to the memory model and comprising:
- a store queue for the strand;
- a load queue for the strand configured to store a load entry with the load timestamp in response to the MC confirmation;
- and
- a global store buffer accessed to determine a snapshot for the load instruction in response to a strand-committed (SC) confirmation for the load instruction, wherein the SC confirmation is from the simulation;
- and
- a verification engine configured to determine an error in the processor design by comparing the load value and the snapshot.
A non-transitory computer readable medium (CRM) storing instructions for verifying that a processor design conforms to a memory model, the instructions comprising functionality for:
- receiving, from a simulation of the processor design and using a checker conforming to the memory model, a memory-committed (MC) confirmation for a load instruction executed by a strand in the processor design;
- obtaining, using the checker and in response to the MC confirmation for the load instruction, a load timestamp associated with the load instruction and a plurality of caches in the processor design;
- inserting, into a load queue of the checker corresponding to the strand, a load entry comprising the load timestamp in response to the MC confirmation for the load instruction;
- receiving, using the checker and after inserting the load entry into the load queue, a strand-committed (SC) confirmation for the load instruction from the simulation of the processor design;
- determining, using the checker and in response to the SC confirmation for the load instruction, a snapshot for the load instruction based on the load timestamp;
- obtaining a load value for the load instruction from the simulation of the processor design;
- and
- determining an error in the processor design by comparing the load value and the snapshot.
Dependencies are inferred from the claim text.