Séminaire des équipes de recherche
Kami: Modular Verification of Digital Hardware in Coq
In the formal-methods world, the hardware industry's use of formal verification is often touted as quite advanced compared to the state of practice in software. The claim seems to be true, but software-verification specialists might be surprised at how weak are the theorems that tend to be proved about hardware.
In this talk, I will present our Kami framework for the Coq proof assistant, which applies to digital-hardware verification the sorts of functional-correctness techniques that are well-known in the programming-languages community, with some twists.
- Date : 23/01/2018
- Lieu : Inria de Paris- 2 rue Simone Iff - Salle Lions 1- bâtiment C
- Intervenant(s) : Adam Chlipala
Kami is based on an embedded domain-specific language for hardware programming, inspired by the Bluespec language. Certain software-like modularity techniques are available, which in turn leads to modular proofs of components, while still making it possible to compile these programs to circuit-like forms.
The unifying specification formalization is refinement for labeled transition systems. Put more directly, an implementation is correct if any log of its interactions with the world could also be generated by the specification. Our framework design includes more hardware-appropriate versions of classic Coq tactics for software verification. There are also some unusual features to support mixing native Coq code with deeply embedded hardware designs, as intermediate stages in refinement processes from specifications to compilable code.
We have been applying Kami to implementations (including a family of multicore chips) of the RISC-V open instruction set, which is a social development worth paying attention to in its own right, for instance because of ongoing efforts to give it an official mechanized semantics.
Kami is joint work with Murali Vijayaraghavan, Joonwon Choi, Arvind, and Benjamin Sherman.
- Date : 23/01/2018
- Heure: 10:30
- Entrée gratuite