Title: RISC-V ISA Formal Specification Speaker: Thomas Bourgeat, MIT Venue: 8th RISC-V Workshop, Barcelona Date: Monday May 7, 2018 Abstract: In this tutorial we will demonstrate several flavors of a formal specification of the RISC-V ISA, written in Haskell. We will present the important part of the code, use it as a software simulator, automatically transform it into a coq specification (used to prove the correctness of a small imperative language), and automatically synthesize it to circuit (to model check against other designs). If time permits, we will show how the same code can be used to explore some non-determinism in the specification. Registration info: https://riscv.org/workshops/