Processor design verification

摘要

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.

主权项

1. 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.