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

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.

24 Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification JOONWON CHOI∗, MURALIDARAN VIJAYARAGHAVAN∗, BENJAMIN SHERMAN, ADAM CHLIPALA, and ARVIND, MIT CSAIL, USA It has become fairly standard in programming-languages research to verify functional programs in proof

Loading..

Tags:

  High, Hardware, Specification, Levels, Parametric, Akim, High level parametric hardware specification and

Information

Related search queries