A consistency checker for memory subsystem traces
2016
Verifying the memory subsystem in a modern shared-memory multiprocessor is a big challenge. Optimized implementations are highly sophisticated, yet must provide subtle consistency and liveness guarantees for the correct execution of concurrent programs. We present a tool that supports efficient specification-based testing of the memory subsystem against a range of formally specified consistency models. Our tool operates directly on the memory subsystem interface, promoting a compositional approach to system-on-chip verification, and can be used to search for simple failure cases - assisting rapid debug. It has recently been incorporated into the development flows of two open-source implementations - Berkeley's Rocket Chip (RISC-V) and Cambridge's BERI (MIPS) - where it has uncovered a number of serious bugs.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
21
References
3
Citations
NaN
KQI