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] [Google Scholar] [DBLP] [Citeseer] [url]

MICRO '21: 54th Annual IEEE/ACM International Symposium on Microarchitecture, Virtual Event, Greece, October 18-22, 2021
ACM
Pages 679-694
2021
Note(s): leakage contracts

uSpec