Case study (formal verification)
A scalable floating-point verification workflow using RTL-to-RTL model checking against a golden reference, structured into staged helper assertions to make proofs converge.
- Focus: proof structure · helper lemmas · counterexample-guided refinement
- Domains: floating-point · arithmetic · correctness-critical blocks
- Stack: SystemVerilog · SVA · formal tooling · Python automation
Problem
Floating-point units are correctness-critical and difficult to cover comprehensively with simulation alone. Formal proofs often fail without a disciplined decomposition strategy.
Approach
- Direct RTL-to-RTL checking to reduce abstraction/translation gaps
- Divide-and-conquer proof plan (staged helper assertions / lemmas)
- Iteration driven by counterexamples and coverage
Evidence and links
Preprint
Publication details and canonical venue links are maintained on the Publications page.
Building proof structures for arithmetic blocks?
If you want to collaborate, discuss roles, or review artifacts, reach out.