research-article

Public Access

Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations

Authors:

Dominic P. Mulligan,

Nikos Nikoleris,

Caroline TrippelAuthors Info & Claims

MICRO '21: MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture

Pages 679 - 694

https://doi.org/10.1145/3466752.3480087

Published: 17 October 2021 Publication History

All formats PDF

Abstract

Modern hardware complexity makes it challenging to determine if a given microarchitecture adheres to a particular memory consistency model (MCM). This observation inspired the Check tools, which formally check that a specific microarchitecture correctly implements an MCM with respect to a suite of litmus test programs. Unfortunately, despite their effectiveness and efficiency, the Check tools must be supplied a microarchitecture in the guise of a manually constructed axiomatic specification, called a μspec model.

To facilitate MCM verification—and enable the Check tools to consume processor RTL directly—we introduce a methodology and associated tool, rtl2μspec, for automatically synthesizing μspec models from processor designs written in Verilog or SystemVerilog, with the help of modest user-provided design metadata. As a case study, we use rtl2μspec to facilitate the Check-based verification of the four-core RISC-V V-scale (multi-V-scale) processor’s MCM implementation. We show that rtl2μspec can synthesize a complete, and proven correct by construction, μspec model from the SystemVerilog design of the multi-V-scale processor in 6.84 minutes. Subsequent Check-based MCM verification of the synthesized μspec model takes less than one second per litmus test.

References

[1]

2009. Institute of electrical and electronic engineers (IEEE) standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language.

[2]

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in Weak Memory Models. Proceedings of the 22nd International Conference on Computer Aided Verification (CAV)(2010). http://dx.doi.org/10.1007/978-3-642-14295-6_25

Digital Library

[3]

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011. Litmus: Running Tests Against Hardware. Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2011).

[4]

Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Transactions on Programming Languages and Systems (TOPLAS) 36, 2(2014), 7:1–7:74.

Digital Library

[5]

Arm. 2013. Arm Architecture Reference Manual.

[6]

Arm. 2021. The Arm memory model tool. https://developer.arm.com/architectures/cpu-architecture/a-profile/memory-model-tool Accessed 12th April 2021.

[7]

Krste Asanović. 2017. The RISC-V Memory Consistency Model. RISC-V Organization(2017). https://riscv.org/2017/04/risc-v-memory-consistency-model/

[8]

Verific Design Automation. 2019. Verific’s Parser Platform.

[9]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press.

Digital Library

[10]

C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. 2009. Satisfiability modulo theories. In Handbook of Satisfiability. 825–885.

[11]

James Bornholt and Emina Torlak. 2017. Synthesizing Memory Models from Framework Sketches and Litmus Tests. Proceedings of the 38th Conference on Programming Language Design and Implementation (PLDI)(2017).

Digital Library

[12]

Cadence Design Systems, Inc.[n.d.]. Cadence JasperGold formal verification platform. https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform.html Accessed 12th April 2021.

[13]

Nathan Chong and Samin Ishtiaq. 2008. Reasoning about the Arm Weakly Consistent Memory Model. In Proceedings of the ACM SIGPLAN workshop on memory systems performance and correctness (MPSC). 16–19.

Digital Library

[14]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2000. Model Checking. MIT Press.

[15]

Francisco Corella, James M. Stone, and Charles Barton. 1993. A formal specification of the PowerPC shared memory architecture. Technical Report Computer Science Technical Report RC 18638(81566), IBM Research Division, T.J. Watson Research Center (1993).

[16]

M. Elver and V. Nagarajan. 2016. McVerSi: A test generation framework for fast memory consistency verification in simulation. In 2016 IEEE International Symposium on High Performance Computer Architecture (HPCA). 618–630.

[17]

Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. 2017. Mixed-size concurrency: Arm, POWER, C/C++11, and SC. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (POPL). 429–442.

Digital Library

[18]

Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. 2015. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In Proceedings of the 48th International Symposium on Microarchitecture (MICRO). 635–646.

Digital Library

[19]

Naorin Hossain, Caroline Trippel, and Margaret Martonosi. 2020. TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests. Proceedings of the 47th International Symposium on Computer Architecture (ISCA)(2020).

Digital Library

[20]

IBM. 2013. Power ISA Version 2.07.

[21]

Intel Corporation. 2007. Intel 64 architecture memory ordering white paper.

[22]

Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (1978), 558–565.

Digital Library

[23]

Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Transactions on Computing 28, 9 (1979), 690–691.

Digital Library

[24]

Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2014. PipeCheck: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models. Proceedings of the 47th International Symposium on Microarchitecture (MICRO)(2014).

Digital Library

[25]

Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee. 2016. COATCheck: Verifying Memory Ordering at the Hardware-OS Interface. Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2016).

Digital Library

[26]

Daniel Lustig, Andrew Wright, Alexandros Papakonstantinou, and Olivier Giroux. 2017. Automated Synthesis of Comprehensive Memory Model Litmus Test Suites. Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2017).

Digital Library

[27]

Sela Mador-Haim, Rajeev Alur, and Milo M K. Martin. 2010. Generating Litmus Tests for Contrasting Memory Consistency Models. 22nd International Conference on Computer Aided Verification (CAV) (2010).

[28]

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An Axiomatic Memory Model for POWER Multiprocessors. Proceedings of the 24th International Conference on Computer Aided Verification (CAV)(2012).

Digital Library

[29]

Albert Magyar. 2016. A Verilog implementation of the RISC-V Z-scale microprocessor. https://github.com/ucb-bar/vscale.

[30]

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Aarti Gupta. 2018. PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. Proceedings of the 51st International Symposium on Microarchitecture (MICRO)(2018).

Digital Library

[31]

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. 2017. RTLCheck: Verifying the Memory Consistency of RTL Designs. Proceedings of the 50th International Symposium on Microarchitecture (MICRO)(2017).

Digital Library

[32]

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. 2017. RTLCheck: Verifying the Memory Consistency of RTL Designs. https://github.com/ymanerka/rtlcheck.

[33]

Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2015. CCICheck: Using μhb Graphs to Verify the Coherence-consistency Interface. Proceedings of the 48th International Symposium on Microarchitecture (MICRO)(2015).

Digital Library

[34]

Themis Melissaris, Markos Markakis, Kelly Shaw, and Margaret Martonosi. 2020. PerpLE: Improving the Speed and Effectiveness of Memory Consistency Testing. In 2020 53rd Annual IEEE/ACM International Symposium on Microarchitecture (MICRO).

[35]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A Better x86 Memory Model: x86-TSO. Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs)(2009).

Digital Library

[36]

Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2017. Simplifying Arm Concurrency: Multicopy-atomic Axiomatic and Operational Models for Armv8. ACM Programming Languages(2017).

[37]

Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-End Verification of Arm® Processors with ISA-Formal. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV).

[38]

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding POWER Microprocessors. Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI)(2011).

Digital Library

[39]

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors. Commun. ACM 53, 7 (2010), 89–97.

Digital Library

[40]

Tyler Sorensen and Alastair F. Donaldson. 2016. Exposing Errors Related to Weak Memory in GPU Applications. In Proceedings of the 37th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 100–113.

Digital Library

[41]

Caroline Trippel, Daniel Lustig, and Margaret Martonosi. 2018. CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests. Proceedings of the 51st International Symposium on Microarchitecture (MICRO)(2018).

Digital Library

[42]

Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2017. TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2017).

Digital Library

[43]

Srikanth Vijayaraghavan and Meyyappan Ramanathan. 2014. A Practical Guide for SystemVerilog Assertions. Springer Publishing Company, Incorporated.

[44]

Andrew Waterman and Krste Asanović (Eds.). 2018. The RISC-V Instruction Set Manual Volume I: User-level ISA. RISC-V International. Document version 2.2.

[45]

John Wickerson, Mark Batty, Tyler Sorensen, and George A Constantinides. 2017. Automatically comparing memory consistency models. Proceedings of the 44th Symposium on Principles of Programming Languages (POPL) (2017).

Digital Library

[46]

Clifford Wolf, Johann Glaser, and Johannes Kepler. 2013. Yosys: a free Verilog synthesis suite. In Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip).

[47]

Y. Yang, Ganesh Gopalakrishnan, G. Lindstrom, and K. Slind. 2004. Nemos: a framework for axiomatic and executable specifications of memory consistency models. In Proceedings of the 18th International Parallel and Distributed Processing Symposium. 31–.

Cited By

Witharana HJayasena AMishra P(2024)Incremental Concolic Testing of Register-Transfer Level DesignsACM Transactions on Design Automation of Electronic Systems10.1145/365562129:3(1-23)Online publication date: 3-May-2024
https://dl.acm.org/doi/10.1145/3655621
Deutschmann LMüller JFadiheh MStoffel DKunz W(2024)A Scalable Formal Verification Methodology for Data-Oblivious HardwareIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.337424943:9(2551-2564)Online publication date: Sep-2024
https://doi.org/10.1109/TCAD.2024.3374249
Geeson LSmith L(2024)Compiler Testing with Relaxed Memory Models2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444836(334-348)Online publication date: 2-Mar-2024
https://doi.org/10.1109/CGO57630.2024.10444836
Show More Cited By

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Formal Verification of Out-of-Order Processor
ICCMS '09: Proceedings of the 2009 International Conference on Computer Modeling and Simulation

Out-of-order execution is a fundamental technique to achieve instruction-level parallelization in processor designs. The verification of out-of-order processor is a main challenge in processor design. This paper presents a formal method to model and ...
Linear Time Memory Consistency Verification

Verifying the execution of a parallel program against a given memory consistency model (memory consistency verification) is a crucial problem in the functional validation of Chip Multiprocessor (CMP). In the absence of additional information, the above ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MICRO '21: MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture

October 2021

1322 pages

ISBN:9781450385572

DOI:10.1145/3466752

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

National Science Foundation

Conference

MICRO '21

Sponsor:

SIGMICRO

MICRO '21: 54th Annual IEEE/ACM International Symposium on Microarchitecture

October 18 - 22, 2021

Virtual Event, Greece

Acceptance Rates

Overall Acceptance Rate 484 of 2,242 submissions, 22%

Upcoming Conference

MICRO '24

Sponsor:
sigmicro

57th Annual IEEE/ACM International Symposium on Microarchitecture

November 2 - 6, 2024

Austin , TX , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
1,109
Total Downloads

Downloads (Last 12 months)313
Downloads (Last 6 weeks)29

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Witharana HJayasena AMishra P(2024)Incremental Concolic Testing of Register-Transfer Level DesignsACM Transactions on Design Automation of Electronic Systems10.1145/365562129:3(1-23)Online publication date: 3-May-2024
https://dl.acm.org/doi/10.1145/3655621
Deutschmann LMüller JFadiheh MStoffel DKunz W(2024)A Scalable Formal Verification Methodology for Data-Oblivious HardwareIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.337424943:9(2551-2564)Online publication date: Sep-2024
https://doi.org/10.1109/TCAD.2024.3374249
Geeson LSmith L(2024)Compiler Testing with Relaxed Memory Models2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444836(334-348)Online publication date: 2-Mar-2024
https://doi.org/10.1109/CGO57630.2024.10444836
Erata FDeng SZaghloul FXiong WDemir OSzefer J(2023)Survey of Approaches and Techniques for Security Verification of Computer SystemsACM Journal on Emerging Technologies in Computing Systems10.1145/356478519:1(1-34)Online publication date: 19-Jan-2023
https://dl.acm.org/doi/10.1145/3564785
Luo MXiong WLee GLi YYang XZhang ATian YLee HSuh G(2023)AutoCAT: Reinforcement Learning for Automated Exploration of Cache-Timing Attacks2023 IEEE International Symposium on High-Performance Computer Architecture (HPCA)10.1109/HPCA56546.2023.10070947(317-332)Online publication date: Mar-2023
https://doi.org/10.1109/HPCA56546.2023.10070947
Ray S(2023)Verification and Its Role in Design of Modern ComputersHandbook of Computer Architecture10.1007/978-981-15-6401-7_33-1(1-12)Online publication date: 15-Jun-2023
https://doi.org/10.1007/978-981-15-6401-7_33-1
Mosier NLachnitt HNemati HTrippel CSalapura VZahran MChong FTang L(2022)Axiomatic hardware-software contracts for securityProceedings of the 49th Annual International Symposium on Computer Architecture10.1145/3470496.3527412(72-86)Online publication date: 18-Jun-2022
https://dl.acm.org/doi/10.1145/3470496.3527412

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents