Using Formal to Vaccinate RISC-V Designs Against Catastrophic Bugs
summary
A push‑button Formalizer app synthesizes formal properties from the RISC‑V ISA, runs with any vendor tool (Cadence/Mentor/Synopsys), and outputs proofs plus an interoperable ISA coverage database. Case studies: Ibex yields 50% proofs <30 min, 80% <2 hrs while some store‑byte proofs take ~10h20m. The flow finds injected bugs, exposes a decode‑during‑debug corner case caught in seven cycles, and proves RV32I compliance and unreachable or covered instruction sequences.
AI-written summary · about
chapters (13)
- 0:00Intro
- 1:29PODCAST SERIES
- 3:41ARCHITECTURE TO SILICON
- 8:32SIMULATION BASED VERIFICATION
- 10:16SIMULATION VS FORMAL VERIFICATION
- 12:10CHALLENGES WITH PROPERTY CHECKING
- 13:03AUTOMATED SOLUTION
- 17:2715A COVERAGE ANALYZER - NEW SOLUTION
- 18:50ARCHITECTS, DESIGNERS and VERIFICATION ENGINEERS
- 20:16COVERAGE ANALYZER EXAMPLE
- 22:41ARCHITECTURAL VIOLATION FOR ZERORISCY
- 23:31KEY FEATURES
- 24:00SUMMARY