Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C MARDI 23 janvier, 10h30 ------------- Adam Chlipala ------------- MIT ===================================================== 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. 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.