RTLcheck: Verifying the memory consistency of RTL designs

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Michael Pellauer
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture
MICRO-50 '17
Cambridge, Massachusetts
Association for Computing Machinery
New York, NY, USA
Pages 463-476
2017
Note(s): uspec, weak memory, CPU verification
Papers: hsiao:micro:2021
  • Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations [hsiao:micro:2021]