Formal and simulation are not competitors. The same SVA properties run in both: in a formal tool they are proven, in a UVM testbench they are checked on every cycle of every test. Assumptions written for formal become checks that the testbench really drives legal inputs, and covers count in both. This article shows how to write properties once and use them everywhere, and how the two methods divide the work.
8 min read | Intermediate
What You'll Learn
- Package properties in a checker module bound to the design
- Explain what happens to assert, assume and cover in simulation
- Use simulation to validate formal assumptions
- Divide verification goals between formal and simulation
One Set of Properties
Properties are usually kept in a separate checker module and attached to the design with bind, as the ifdef FORMAL and the wrapper article introduced:
module fifo_sva (input clk, input rst, input push, input pop, input full, input empty, input [2:0] count);
m_no_push_full: assume property (@(posedge clk) disable iff (rst) full |-> !push);
a_count_max: assert property (@(posedge clk) disable iff (rst) count <= 3'd4);
a_flags: assert property (@(posedge clk) disable iff (rst) !(full && empty));
c_full: cover property (@(posedge clk) disable iff (rst) full);
endmodule
bind fifo fifo_sva u_sva (.*);
The formal setup reads the design and the checker file. The simulation setup compiles the same two files into the testbench. Nothing is duplicated, and a property fixed in one place is fixed for both.
What Each Statement Does in Simulation
| Statement | Formal tool | Simulator |
|---|---|---|
assert property | proven, or counterexample | checked every clock; an error message on failure |
assume property | restricts the inputs | checked like an assertion: the testbench must obey it |
cover property | reachability, with a trace | counted every time it happens, in the coverage report |
The middle row is important. In simulation, an assumption is a check on the testbench and on the neighbor blocks. If a test drives an input that the formal assumption forbids, the simulator reports it. That validates the assumptions with real stimulus, which the formal tool itself cannot do.
Quick Check
Q: An assumption fires as a failure in a system-level simulation. What does that mean for the formal proofs of the block?
Show Answer
The real environment breaks a promise the proofs relied on. Either the neighbor has a bug, or the assumption was wrong and the proofs must be redone without it. In both cases the formal results are not valid for that system until it is resolved.
Dividing the Work
- Formal: the rules of control blocks, proven for all inputs; corner cases of concurrency; interface protocol rules; equivalence after synthesis.
- Simulation: end-to-end function of the subsystem and chip; long scenarios such as boot sequences and software; performance; wide datapaths against reference models.
- Both: the shared assertions, which formal proves at block level and simulation keeps checking when the block runs in its real context.
A block that is fully proven with formal often needs only a light simulation testbench for integration. A coverage hole in simulation can be classified by formal, as the coverage closure article showed.
Quick Check
Q: A FIFO is fully proven with formal. Should its assertions still be enabled in the chip-level simulation?
Show Answer
Yes. They cost little, and they check that the FIFO's assumptions hold in the real chip and that it is connected correctly. A failure there points straight at the integration problem.
Practical Details
- Guard formal-only helper logic, such as tracked values with
(* anyconst *), so that it is not compiled in simulation, or give it a simulation equivalent. - Disable assertions during reset with
disable iff, so that simulation does not report noise while signals are X. - Use the same names in both reports, so that a property's status can be followed from formal to simulation.
- Keep the checker files in the same repository as the RTL, and review them with the RTL.
Running It in ChipVerify Lab
The lab runs the formal side with the immediate form of the properties, as shown throughout this tutorial. In a commercial or full-SVA simulator, the same SVA checker file is compiled with the testbench. The examples of Chapter 7 keep their SVA form as comments at the top of each file, ready to be moved into a checker module.
Common Mistakes
Mistake #1: Writing separate assertions for formal and simulation
Two copies drift apart. Keep one checker module and bind it in both flows.
Mistake #2: Disabling assumptions in simulation
Assumptions are the cheapest way to validate the formal environment. Keep them enabled as checks in every simulation that includes the block.
Mistake #3: Proving a block and dropping its simulation entirely
The proof covers the block under its assumptions. Integration, connectivity and the assumptions themselves still need the system-level runs.
Practice Exercise
Challenge: Split the Verification of a Subsystem
This is a pencil and paper exercise. A DMA engine has a register interface, a descriptor fetch state machine, a 16-entry data FIFO, an arbiter between read and write channels, and a 64-bit data path with byte alignment logic. Say which parts you would verify with formal, which with simulation, and which assertions you would share.
Hint
Look for control logic with clear rules, and for wide data manipulation.
Solution
Formal: the register interface (protocol and read-after-write), the descriptor state machine (legal states, no deadlock, covers), the FIFO (full proof), the arbiter (mutual exclusion and fairness). Simulation: complete DMA transfers with many descriptor chains, the byte alignment data path against a reference model, and performance. Shared: the bus protocol assertions, the FIFO and arbiter assertions, and the descriptor state machine assumptions, which simulation validates against the real bus model.
Summary
- Write properties once, in a checker module bound to the design, and use them in formal and simulation.
- In simulation, assertions are checked every cycle, assumptions become checks on the environment, and covers are counted.
- Simulation validates formal assumptions with real stimulus.
- Formal takes the control rules and corner cases; simulation takes end-to-end function, long scenarios and wide datapaths.
