RTLCheck: Verifying the memory consistency of RTL designs

Yatin A. Manerkar, Daniel Lustig, Margaret Rose Martonosi, Michael Pellauer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

Abstract

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. This paper presents RTLCheck, a methodology and tool for narrowing the microarchitecture/RTL MCM verification gap. Given a set of microarchitectural axioms about MCM behavior, an RTL design, and user-provided mappings to assist in connecting the two, RTLCheck automatically generates the SystemVerilog Assertions (SVA) needed to verify that the implementation satisfies the microarchitectural specification for a given litmus test program. When combined with existing automated MCM verification tools, RTLCheck enables test-based full-stack MCM verification from high-level languages to RTL.We evaluate RTLCheck on a multicore version of the RISC-V V-scale processor, and discover a bug in its memory implementation. Once the bug is fixed, we verify that the multicore V-scale implementation satisfies sequential consistency across 56 litmus tests. The JasperGold property verifier finds complete proofs for 89% of our properties, and can find bounded proofs for the remaining properties.

Original languageEnglish (US)
Title of host publicationMICRO 2017 - 50th Annual IEEE/ACM International Symposium on Microarchitecture Proceedings
PublisherIEEE Computer Society
Pages463-476
Number of pages14
ISBN (Electronic)9781450349529
DOIs
StatePublished - Oct 14 2017
Event50th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2017 - Cambridge, United States
Duration: Oct 14 2017Oct 18 2017

Publication series

NameProceedings of the Annual International Symposium on Microarchitecture, MICRO
VolumePart F131207
ISSN (Print)1072-4451

Other

Other50th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2017
CountryUnited States
CityCambridge
Period10/14/1710/18/17

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Keywords

  • Automated verification
  • Memory consistency models
  • RTL
  • SVA

Fingerprint Dive into the research topics of 'RTLCheck: Verifying the memory consistency of RTL designs'. Together they form a unique fingerprint.

Cite this