Formal verification and assertions
Check the rules your block must satisfy, written as SystemVerilog Assertions (SVA), including scenarios simulation may miss.
How the check works
A proof is only meaningful within its assumptions.
Define the conditions
State the design rule and the environment assumptions.
Check the property
Search for a violating sequence and assess trigger reachability.
Read the result
Record a proof, counterexample, bounded result, or unresolved check.
A bounded pass covers only the checked depth. Cover checks help expose properties that never had a chance to fire.
What you receive
- The property file and the formal tool configuration.
- A proof log for each property, or the depth reached and why.
- Cover results showing which property triggers were reached and which remain unresolved.
- A counterexample trace when the tool finds a property violation.
When this is useful
- Control logic, an arbiter, or a protocol state machine keeps producing late bugs.
- A formal run passes but nobody can say what it actually checked.
- You want the same checks to keep running in your regression.
Problem, approach, and required inputs
The problem
A green simulation only shows the design worked on the tests someone wrote. For control logic, handshakes, and arbiters, the failing case is often one nobody thought to test. A formal pass can also mean nothing if the property was never able to fire.
What we do
We express design requirements as properties and agree the environment assumptions. Relevant cover checks assess whether property triggers can occur. The report distinguishes unbounded proofs, bounded results, failures, and unresolved checks, including unreached triggers. Property integration is agreed for the selected tool flow.
What we will need from you
- The block, under NDA.
- Its specification or interface description.
Example from real work
Real issue on an open source RISC-V core
Proving a debug path in a RISC-V core can never run
An open coverage hole in a RISC-V core's controller. We proved two of its conditions can never happen and wrote a test that reaches the third.
More real issues
- Open source RISC-V core, coverage hole 1004 · Reachable, test suppliedReaching an interrupt and debug clash as a core wakes up
- Open source RISC-V core, coverage hole 1005 · Waiver, with a software ruleShowing a hardware loop hole needs software to break a rule
- Open source RISC-V core, coverage hole 1007 · Dead code, provenProving a single step stall in a RISC-V core never happens
- Open source RISC-V core, coverage hole 1022 · Dead code, provenWhy the FPU arbiter in a RISC-V core never arbitrates
- Open source RISC-V core, coverage hole 1006 · Waiver, with a software ruleShowing two hardware loop guards need a software rule
Technical details
How the result is checked
Proof logs and cover traces are kept exactly as the tool produced them. The SystemVerilog Assertions (SVA), configuration, and run instructions are included for the agreed tool flow.
Tools used for this kind of work
- SymbiYosys
- Yosys
- z3
- SystemVerilog Assertions
Scripts are handed over as agreed in the scope. Properties are standard SystemVerilog Assertions and can be adapted to a commercial tool. If we have not tested your simulator or flow, the scope says so.
Discuss this problem.
Tell us what you are trying to verify and what is blocking you. An engineer replies, and the scope comes back in writing after a call.
Discuss a verification problem