Silver Oak: Hardware Software Co-Design and Co-Verification in Coq
This presentation describes a proof of concept project Silver Oak which demonstrates the formal specification, implementation and verification of a subset of the OpenTitan silicon root of trust chip specification. The system is almost entirely implemented in the Coq theorem prover and includes theorems and proofs that span hardware and software components. A structural hardware description language called Cava (inspired by the Lava DSL in Haskell) was used to implement an AES encryption/decryption block. The Bedrock 2 DSLn Coq from MT was used to implement the driver code that runs on a RISC-V core which communicates with the AES hardware block over the TileLink bus.
We were able to produce both hardware and software components extracted from Coq (RISC-V code for the software, SystemVerilog for the hardware) that functioned as drop-in replacements for the C driver code for the AES block and the AES hardware block. Both extracted components were no larger or slower than the original block and the FPGA-based hardware system was able to function correctly with the high assurance blocks extracted from Coq.
This project demonstrates the viability of co-developing hardware and software in a single framework that supports formal specification and verification, while also permitting the extraction of performant code and hardware with proofs that span the hardware software divide.
Sat 17 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30
|They're the same picture: a software-verification flow adapted for hardware verification
|Design for Hardware Memory Model Verification
Yao Hsiao Stanford University, Yasas Seneviratne University of Virginia, Tommy Tracy II University of Virginia, Kevin Skadron University of Virginia, Caroline Trippel Stanford UniversityFile Attached
|Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware
|NFC:Next-generation Formal verification for high performance Caches
|Sandia's Formal Hardware Design and Verification, Present and Future
Noah Evans Sandia National Laboratories
|Silver Oak: Hardware Software Co-Design and Co-Verification in Coq