Silver Oak: Hardware Software Co-Design and Co-Verification in Coq
summary
A prototype called Silver Oak formalizes parts of the OpenTitan root‑of‑trust in Coq, using Cava for an AES hardware block and Bedrock 2 for the RISC‑V driver, connected over TileLink; Coq extracts working SystemVerilog and RISC‑V binaries that act as drop‑in replacements, match original size and speed, and run on FPGA with passing tests, and a combined Coq theorem links hardware and driver semantics end‑to‑end (some verification goals remain incomplete).
AI-written summary · about