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