Unlocking Hardware-Software Co-Design with Coq: Silver Oak Methodology 🚀

Ben Blaxill (Groq), Samuel Grütter (Massachusetts Institute of Technology), Jade Philipoom (Google, Germany), Satnam Singh (Groq)

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.