back

End-to-end formal ISA verification of RISC-V processors with riscv-formal

If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!

Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.

Video duration
00:29:05
Language
English
Abstract
Formal hardware verification (hardware model checking) can prove that a design has a specified property. Historically only very simple properties in simple designs have been provable this way, but improvements in model checkers over the last decade enable us to prove very complex design properties nowadays. riscv-formal is a framework for formally verifying RISC-V processors directly against a formal ISA specification. In this presentation I will discuss how the complex task of verifying a processor against the ISA specification is broken down into smaller verification problems, and other techniques that I employed to successfully implement riscv-formal.

Formal hardware verification (hardware model checking) can prove that a design has a specified property. This is different from simulation, which can only demonstrate that a property holds for some concrete traces (sets of inputs). Historically only very simple properties in simple designs have been provable this way, but improvements in model checkers over the last decade enable us to prove very complex design properties nowadays.

riscv-formal is a framework for formally verifying RISC-V processors directly against a formal ISA specification. (The ISA specification used in riscv-formal is itself formally verified against Spike , the official RISC-V simulator and "golden reference" implementation.) riscv-formal can be made to work with any existing processor design, all that is needed is to add an additional RVFI (RISC-V formal interface) trace port to the core.

riscv-formal by default uses the open source SymbiYosys toolchain to perform the formal proofs, but it should be compatible with all major HDL formal verification flows.

In this presentation I will discuss how the complex task of verifying a processor against the ISA specification is broken down into smaller verification problems in riscv-formal, how to implement RVFI, how integrate a core with riscv-formal, and what kind of bugs can be detected using our method.

Most of the proofs performed by riscv-formal are bounded proofs, i.e. it is only proven that the properties hold for the first N cycles after reset. But with a sufficiently large N we can create high confidence that in fact all relevant states can be reached within the bound of the proof and that therefore the bounded case is a sufficient proxy for the more general unbounded case. Abstractions, cut-points, and blackboxing can further help extend the effective bound of the proof. The presentation also touches on those techniques.

Talk ID
8768
Event:
34c3
Day
1
Room
Saal Clarke
Start
12:45 p.m.
Duration
00:30:00
Track
Resilience
Type of
lecture
Speaker
Clifford Wolf
Talk Slug & media link
34c3-8768-end-to-end_formal_isa_verification_of_risc-v_processors_with_riscv-formal

Talk & Speaker speed statistics

Very rough underestimation:
150.3 wpm
863.4 spm
157.6 wpm
904.7 spm
100.0% Checking done100.0%
0.0% Syncing done0.0%
0.0% Transcribing done0.0%
0.0% Nothing done yet0.0%
  

Work on this video on Amara!

Talk & Speaker speed statistics with word clouds

Whole talk:
150.3 wpm
863.4 spm
instructionprocessorriscv-formalregisterspecificationinterfaceproofsformalbugschecksrisc-vthingsfileverificationcheckaddcorecounterprocessorsisastateproofcoupleprogramwritefindprovestuffreadtoolsabstractionslistbehaviorcliffordmemorydesigncyclesboundedeasierconsistencycourseversionimplementtimeopenunboundedquestionsloadbetterexample
Clifford Wolf:
157.6 wpm
904.7 spm
instructionprocessorriscv-formalregisterspecificationproofschecksthingsbugsformalinterfacefilerisc-vcounterprocessorsverificationaddcheckisawritecoupleprogramcoreproveproofstufftoolsstatebehaviorlistreadfindabstractionseasiermemorydesigncyclescourseconsistencyimplementcorrectlyboundedunboundedbettersmallexampleriscv-boundsloadsupport