Formal Assurance for RISC-V Implementations
summary
Galois applies mechanized specs and formal proofs to RISC-V, compiling Haskell specs with Clash→Verilog and checking RTL equivalence with JasperGold equivalence checking and open tools, but notes those methods scale poorly for deep pipelines and out‑of‑order cores and mostly target Verilog. Work includes a DSL called Lando, a RISC‑V security test suite, metrics and a dashboard, and a small realized configuration: 32‑bit RISC‑V Piccolo with AES‑128 formally verified hardware crypto. Many components are prototype or early stage and tool integration remains a challenge.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:31About Galois
- 6:12RISC-V Assurance
- 9:25A Way Forward
- 11:06Correctness Specifications
- 12:21Specification Validation
- 13:39Specification Verification
- 15:17Security Specifications
- 16:26Measurement and Metrics
- 18:29Working with Measurements
- 19:48Example Feature Model (Unconfigured)
- 21:21Example Feature Model (Configured)
- 22:02R&D Status
- 23:31Open Challenges
related talks
24mDemocratising Formal Verification of RISC V Processors
19mAn Open Source Approach to System Security
25mRISC-V System-level Certification from Verification Foundations
16mAutomated Certification and Benchmarking for RISC-V Architectures
45mVerified seL4 on secure RISC-V processors
13mRISC-V: Securing the Future of Open Source Computing
20mRISC-V open designs and contributions to hardware security research and development activities
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era