Kami: A Platform for High-Level Parametric Hardware ...

1 24 Kami: A Platform for High-Level Parametric HardwareSpecification and Its Modular VerificationJOONWON CHOI , MURALIDARAN VIJAYARAGHAVAN , BENJAMIN SHERMAN, ADAMCHLIPALA, and ARVIND,MIT CSAIL, USAIt has become fairly standard in programming-languages research to verify functional programs in proofassistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coqlibrary that uses labeled transition systems to enable similar expressive and modular reasoning for hardwaredesigns expressed in the style of the Bluespec language. We can specify, implement, and verify realisticdesigns entirely within Coq, ending with automatic extraction into a pipeline that bottoms out in methodology has been evaluated in a case study verifying an infinite family of multicore systems, withcache-coherent shared memory and pipelined cores implementing (the base integer subset of ) the RISC-Vinstruction Concepts: Hardware Theorem proving and SAT solving; Hardware description languages andcompilation; High-Level and register-transfer level synthesis;Additional Key Words and Phrases: formal verification, Hardware , proof assistantsACM Reference Format:Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind.

2 2017. Kami: APlatform for High-Level Parametric Hardware specification and Its Modular ACM , ICFP, Article 24 (September 2017), 30 INTRODUCTIONIn the face of skepticism about the practical potential of formal methods, the standard response ofthe specialist is that formal methods already play a widespread and essential role in quality controlfor the computer- Hardware industry. However, researchers with experienceonlyon the softwareside might be surprised at some pervasive limitations of the kinds of formal methods that industryapplies to Hardware , typically based on model checking and satisfiability solving, where analysisreduces to explicit state-space exploration. For instance:(1)Verification effort is focused on (relatively) small components of full systems, for instanceon the floating-point units of processors. While complete verification of the algorithmsimplementing floating-point arithmetic requires heroic effort by itself, these individual resultsarenot composed into full-system theorems.

3 (2)Relativelyweak propertiesare proved, with considerable abstraction gaps from the naturalcorrectness conditions, even for limited components of full systems. For instance, it is common Choi and Vijayaraghavan are primary authors with equal contributions, and their two names are listed to make digital or hard copies of part or all of this work for personal or classroom use is granted without feeprovided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,contact the owner/author(s). 2017 Copyright held by the owner/author(s).2475-1421/2017/9-ART24 ACM Program. Lang., Vol. 1, No. ICFP, Article 24. Publication date: September :2J. Choi, M. Vijayaraghavan, B. Sherman, A. Chlipala, and Arvindfor engineers to think about specifications and manually come up with invariants to beasserted about circuits, with no formal connection back to specs.

4 (3)Thescopeof verifiable components is fundamentally limited by thestate-space-explosionproblem. For example, in order to verify cache-coherence protocols with Murphi [Dill et ], a widely used model checker designed for that exact task, at one point the biggestsystem that could be verified had only 3 cores interacting with a single-address memoryhaving two potential values. While improvements to algorithms and Hardware (for runningthe analysis) continually increase the feasible system size, there are fundamental limitationsof such tools that explore finite state spaces, in the face of exponential growth in state spacesas we add processor cores or memory addresses. One mitigation, rarely applied in industry, isverification ofparameterizedsystems, with variables standing for the number of cores. Butadoption of this strategy is mostly limited tomodelsof real Hardware systems, not connectedto synthesis pipelines that generate real instead the standard procedure used in the programming-languages research commu-nity to verify software programs with proof assistants.

5 (1)Implement the program in the functional programming language built into the proof assistant.(2) In a rich higher-order logic, state the most natural correctness theorem for the program.(3)Prove the theorem using scripts oftacticsfor proof steps at different levels of granularity,saving the user from tedious details while still giving an opportunity to spell out the keyinsights manually.(4)Useextractionto translate the program to a language like OCaml automatically, and fromhere use standard development tools to compile and run this paper, we introduce theKamiframework for the Coq proof assistant, which bringsthis style of development and verification to the world of computer architecture, simultaneouslyreversing all of the weaknesses enumerated above for most Hardware -verification tools. Kamimakes it possible to code and verify a fairly realistic processor within Coq and then extract it torun on FPGAs (and almost certainly in silicon, though we have not yet had the opportunity tofabricate a real chip).

6 We also emphasize that our use of verified is more in the tradition ofCompCert [Leroy 2006] or seL4 [Klein et al. 2009] than of the day-to-day practices of verificationengineers in the Hardware industry: we prove that a systemwith any number of shared-memorycores with associated coherent cachescorrectly implements thefunctional-correctness specification ofour instruction set, with respect to sequential must reconsider each of the steps of the recipe above, so that they apply properly to hardwaredesigns. On one level, the central new challenge is the fundamentallimitationsof Hardware circuits,where every variable must have a finite domain and where loops and recursion are not supporteddirectly. On another level, the challenge is to support all of theopportunitiesthat circuits provide torealize levels of parallelism far beyond what is feasible in software, where in some sense all the gateson a circuit board are constantly running in parallel.

7 Just as most uses of proof assistants verifyfunctional programs rather than assembly programs, to help the proof author focus on the essentialproblems, in Kami we code Hardware designs at a higher abstraction level than circuits: we formalizea subset of the Bluespec Hardware description language, whose fundamental structuring principleis sets of state-change rules that execute atomically, with a scheduler automatically choosing howto interleave may be more familiar with Verilog or other Hardware descriptions at the level of so-calledregister-transfer languages (RTL). RTL programs describe circuits as networks of gates, but withoutphysical-placement details. Concerns oftimingcomplicate programming at this level. The designeris often required to know how many clock cycles go by between when a signal flows into a moduleProc. ACM Program. Lang., Vol. 1, No. ICFP, Article 24. Publication date: September : High-Level Parametric Hardware specification and its Modular Verification24:3on one wire and when a related signal comes out on another wire.

8 Bluespec abstracts these issues,much like how a C compiler abstracts details of a call stack. It is also the case that RTL designs makeparallelism explicit, which is convenient for maximizing performance, but which creates challengesfor correctness reasoning: proofs must consider explicit simultaneous execution of instead exposes a transaction-based model with the fiction that fragments of code runindependently and in sequence, and the commercial Bluespec compiler deals automatically with thechallenges (timing and parallelization) that Verilog forces upon the programmer. As we progressthrough introducing the modular proof techniques at the heart of Kami, it should become clearthat essentially none of them would apply in the traditional RTL model. It naturally follows thatinstead of verifying the circuits produced after synthesis from Bluespec, we verify that a high -levelimplementation refines a High-Level specification , both written in Kami.

9 If we trust (or later verify)the Bluespec compiler to preserve the semantics while translating from Kami programs into RTLcircuits, then we are guaranteed that the RTL circuits of the implementation refine the high -levelspecification .The next challenge is choosing the right kind of correctness theorem to ascribe to the com-ponents of a system, so that the individual theorems can be composed in a black-box way intofull-system results. Here we follow our previous work [Vijayaraghavan et ] in adapting ideasfrom process algebra. We formalize Hardware components aslabeled transition systems, with aninteraction-centric operational semantics that helps us reason about each component individuallywhile abstracting over its environment. Our previous work [Vijayaraghavan et ] suffersfrom one of the problems we mentioned earlier: it applies only tomodelsof real Hardware designs,with no path toward extraction-style generation of synthesizable circuits.

10 We previously applied amanual and error-prone process to example Hardware designs, formalizing each one directly asan inductive relation in Coq. With Kami, we work instead with explicit program syntax designedto be trivially translatable to real Bluespec syntax, to which we can apply Bluespec s commercialsynthesis tools to produce Hardware last challenge is to figure out the Hardware analogues of the workhorse proof tactics ofsoftware verification, like induction, execution-based simplification, and rewriting , whose closestequivalents turn out to be simulation arguments, inlining of method definitions, and replacementof one Hardware module with another proved to be compatible, rest of the paper proceeds through a running example (Section 2); the syntax, semantics,and correctness notions of Kami (Section 3); more background on Bluespec and its practicality,including the approach to automatic RTL synthesis (Section 4); the key framework lemmas usedin modular proofs (Section 5); our case-study multicore system (Section 6).