Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations

Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline Trippel
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture
Virtual Event, Greece
Association for Computing Machinery
New York, NY, USA
Pages 679-694
Note(s): ISA specification