Sandia's Formal Hardware Design and Verification, Present and Future
summary
Sandia applies Yosys and SMT-based equivalence checks to real ASIC designs and finds concrete results — an RTL one‑cycle Verilog RISC‑V spec is proven equivalent to complex synthesised designs and uncovers two critical bugs; Verific and manual SMT model inspection ensure traceability from netlist to proof. Targets are constrained 1980s‑class systems (≈100KB firmware, hard real‑time scanline deadlines). Roadmap moves from SMT‑based workflows toward a correct‑by‑construction MDD pipeline with a Coq‑like deep specification.
AI-written summary · about