RTLcheck
Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Michael Pellauer · 2017
Paramount to the viability of a parallel architecture is the correct implementation of its memory consistency model (MCM). Although tools exist for verifying consistency models at several design levels, a problematic verification gap exists between checking an abstract microarchitectural specification of a consistency model and verifying that the actual processor RTL implements it correctly.