The DMA's coverage model once had an illegal bin: illegal_bins both, because "the DMA never reports DONE and ERR together". Nobody had checked that sentence against the RTL; it was a habit of the tests, which always cleared ERR. It took a scratch simulation that happened to run a full job after a truncated one to read STATUS = 0x6 and expose the claim as wrong (bench war story 10). Asked the same question, an open-source formal tool returned a 12-cycle counterexample in well under a second, without anyone writing a test for it.
That is the case for formal in one story, not a case for replacing the bench: the same tool would struggle to prove that a 4 KB transfer through a real DMA's address generator and AXI bursts comes out right. Where is the line, how do you split the DMA's plan across it, and what does each kind of result promise at sign-off?
A simulation runs one input sequence per test and checks what happens. A formal tool builds a mathematical model of the design and asks a solver whether any input sequence, within the rules you allow, can make a property fail. The rules you allow are assumptions (assume): the legal behaviour of the environment, such as "the APB master holds PADDR until PREADY". The properties to check are assertions (assert). A cover asks the opposite question, "show me a trace where this happens", and proves a behaviour is reachable.
Think of checking a combination lock. Simulation tries combinations, thousands per second, chosen cleverly, but can never say that no other combination opens it. Formal takes the mechanism apart and shows that only one combination lines up the wheels. That is far stronger, and it only works while the mechanism is small enough to reason about.
Formal produces three kinds of answer. A counterexample (CEX) is a trace that breaks an assertion: the tool found a bug or a missing assumption. A full proof says the assertion holds in every reachable state, for every legal input, forever; engines get there with induction or IC3/PDR. A bounded proof says only that no failure exists within the first N clock cycles after reset; it is what you get when a full proof does not converge, and N is called the proof depth.
Formal is strong at | Why | Typical use |
|---|---|---|
Control logic rules | Small state, many interleavings that random stimulus rarely hits | Register access rules, FSM transitions, arbitration, handshakes |
Deadlock and liveness | "Eventually" can only be proved, never fully simulated | A request is always granted, a FIFO never wedges full and empty at once |
Connectivity | The question is structural and exhaustive | SoC pin-mux, interrupt and reset wiring under every configuration |
Sequential equivalence | Two designs compared over all inputs | Retiming, clock gating, a re-pipelined block against the original |
X-propagation | Every X source traced to every observation point | Which uninitialised flops can reach an output after reset |
Register (CSR) apps | Properties generated from the register description | Access policies, reset values, no aliasing between addresses |
Coverage unreachability | Proving a hole can never be hit | Turning code coverage holes into reviewed exclusions |
Formal struggles in the opposite cases. Wide data paths: multipliers, floating point and cryptography make the solver's problem explode, so those blocks are checked by simulation against a model or with specialised equivalence flows. Deep sequential depth: a counter that must reach 65,535 before something interesting happens, a 1,024-entry FIFO, or an end-to-end property over a long packet needs abstraction before it converges. System behaviour: software-driven flows, many blocks interacting and performance questions stay in simulation and emulation. The Formal course covers the techniques that push the line outwards, such as abstraction and convergence tactics.
One honest detail: for this tiny DMA, the XOR of a single word is trivial for formal too. What stays in simulation is the end-to-end promise ("the Nth output word is the Nth input word XOR KEY, for every packet length") and everything around it: the driver, the interrupt flow, reset mid-job. In a production DMA with address generation and bursts, that is where the state explodes.
The register rules are short properties on signals inside dma_dut. Written as a checker module and attached with bind (the next lesson covers the mechanism), they run in the UVM bench with no RTL edits. This exact module was bound into the bench in a scratch run with Verilator's --assert and stayed silent through dma_smoke_test, dma_rand_test, dma_truncate_test, dma_ral_job_test and dma_ral_busy_len_test.
// snippet: bound into dma_dut in a scratch run (Verilator 5.048, --assert)
module dma_rules_checker (
input logic clk, rst_n, xfer, pwrite, busy, done, err, irq_en, irq, go, take, last_word,
input logic [7:0] paddr,
input logic [31:0] pwdata, key,
input logic [15:0] len, count
);
import uvm_pkg::*;
default clocking cb @(posedge clk); endclocking
// LEN and KEY writes are ignored while BUSY
a_len_busy: assert property (disable iff (!rst_n)
xfer && pwrite && paddr == 8'h08 && busy |=> $stable(len))
else `uvm_error("DMA_RULE", "LEN changed by a write while BUSY")
a_key_busy: assert property (disable iff (!rst_n)
xfer && pwrite && paddr == 8'h0C && busy |=> $stable(key))
else `uvm_error("DMA_RULE", "KEY changed by a write while BUSY")
// W1C: writing 1 to DONE clears it, unless the last word lands in the same cycle
a_done_w1c: assert property (disable iff (!rst_n)
xfer && pwrite && paddr == 8'h04 && pwdata[1] && !(take && last_word) |=> !done)
else `uvm_error("DMA_RULE", "DONE not cleared by a W1C write")
// BUSY rises only because of a GO write; a job never runs past LEN
a_busy_go: assert property (disable iff (!rst_n) $rose(busy) |-> $past(go))
else `uvm_error("DMA_RULE", "BUSY rose without a GO write")
a_count_lt_len: assert property (disable iff (!rst_n) busy |-> count < len)
else `uvm_error("DMA_RULE", "COUNT reached LEN while still BUSY")
a_irq: assert property (disable iff (!rst_n) irq == (irq_en && (done || err)))
else `uvm_error("DMA_RULE", "IRQ does not match IRQ_EN & (DONE | ERR)")
endmodule
bind dma_dut dma_rules_checker u_rules (.*); // .* connects dma_dut's own signals by nameNotice the last scratch test. dma_ral_busy_len_test writes LEN = 9 while the DMA is busy, and the register model's mirror check reports its expected RegModel mismatch. a_len_busy stays silent in the same run, and both are right: the property checks the DUT's rule (the write is ignored), while the mirror mismatch is the model's limitation. A property on the RTL cannot be fooled by a stale testbench model.
To prove the rules, a formal harness instantiates the DUT with every input free and adds the environment's rules as assumptions. The APB part is exactly the protocol the bench's driver follows; the stream inputs are left fully free, so the solver may send any data, any TLAST and any TREADY pattern.
// snippet: formal harness (Yosys + yosys-smtbmc + z3), scratch run
module dma_formal (
input logic clk, rst_n,
input logic [7:0] paddr,
input logic psel, penable, pwrite,
input logic [31:0] pwdata, s_tdata,
input logic s_tvalid, s_tlast, m_tready
);
logic [31:0] prdata, m_tdata;
logic pready, pslverr, s_tready, m_tvalid, m_tlast, irq;
dma_dut dut (.*); // every input above is free: the solver picks its values
logic past_valid = 1'b0;
always_ff @(posedge clk) past_valid <= 1'b1;
// The environment: start in reset, then the APB master obeys the protocol.
always_comb if (!past_valid) assume (!rst_n);
always_comb if (!rst_n) assume (!psel); // bus idle in reset
always_comb if (penable) assume (psel); // PENABLE never without PSEL
always_ff @(posedge clk) if (past_valid && rst_n) begin
if ($past(psel && !penable)) assume (psel && penable); // setup -> access
if (!$past(psel)) assume (!penable); // PENABLE only after setup
if ($past(psel && !(penable && pready))) // held until PREADY
assume (psel && paddr == $past(paddr) && pwrite == $past(pwrite) && pwdata == $past(pwdata));
if ($past(psel && penable && !pready)) assume (penable);
if ($past(psel && penable && pready)) assume (!penable);
end
endmoduleCommercial formal tools read the bound concurrent-SVA module above directly. The open-source flow used for the scratch run (Yosys's built-in front end with yosys-smtbmc and the z3 solver) reads neither bind nor concurrent assertions, so the same rules were written as clocked immediate assertions with $past and included inside a scratch copy of the DUT. The meaning is the same; only the spelling changes.
// snippet: dma_rules.svh, included inside a scratch copy of dma_dut under `ifdef FORMAL
always_ff @(posedge clk) if (f_past_valid && $past(rst_n) && rst_n) begin
if ($past(xfer && pwrite && paddr == 8'h08 && busy)) a_len_busy: assert (len == $past(len));
if ($past(xfer && pwrite && paddr == 8'h0C && busy)) a_key_busy: assert (key == $past(key));
if ($past(xfer && pwrite && paddr == 8'h04 && pwdata[1] && !(take && last_word)))
a_done_w1c: assert (!done);
if (busy && !$past(busy)) a_busy_go: assert ($past(go));
end
always_comb if (rst_n) begin
a_count_lt_len: assert (!busy || count < len);
a_irq: assert (irq == (irq_en && (done || err)));
`ifdef CLAIM_NOT_BOTH
a_not_both: assert (!(done && err)); // the old "illegal bin" claim
`endif
c_done_len3: cover (done && count == 16'd3); // reachability witnesses
c_err: cover (err);
endyosys -p "read_verilog -formal -sv -DFORMAL dma_dut_f.sv dma_formal.sv; prep -top dma_formal;
async2sync; dffunmap; write_smt2 -wires base.smt2"
yosys-smtbmc -s z3 -t 25 base.smt2 # bounded check, 25 cycles
yosys-smtbmc -s z3 -i -t 25 base.smt2 # induction
yosys-smtbmc -s z3 -c -t 30 base.smt2 # covers## 0:00:00 Checking assertions in step 24..
## 0:00:00 Status: PASSED (bounded: no failure in 25 cycles)
## 0:00:00 Trying induction in step 25..
## 0:00:00 Trying induction in step 24..
## 0:00:00 Trying induction in step 23..
## 0:00:00 Temporal induction successful.
## 0:00:00 Status: PASSED (with the bounded run: a full proof)
## 0:00:00 Reached cover statement in step 8 at dma_formal.dut: c_err
## 0:00:00 Reached cover statement in step 10 at dma_formal.dut: c_done_len3The bounded run checks every legal input sequence of up to 25 cycles from reset. On its own it says nothing about cycle 26.
The induction run shows that if all assertions held for a few consecutive cycles (two, here), they hold in the next one, from any state, reachable or not. That last part is also induction's failure mode: the tool may report a counterexample that starts from a state the design can never reach (a counter value no reset path produces, two state machines out of step). That is not a bug; it means the properties are too weak to rule the state out. The fix is a helper assertion that states the invariant (for example, COUNT never exceeds LEN while BUSY), proven along with the rest, or a deeper induction. Together with a base case at least that deep (the 25-cycle run), that is a full, unbounded proof. It covers LEN = 65,535 jobs, which no 25-cycle bound reaches. (SymbiYosys's prove mode runs exactly this pair.)
The covers prove the interesting behaviour is reachable under the assumptions: an ERR in 8 cycles (LEN write, GO, one early TLAST) and a finished 3-word job in 10. A proof under assumptions that allow nothing would be worthless, and the covers are the evidence that they allow something.
Now the old claim. Rebuilt with -DCLAIM_NOT_BOTH, the run fails:
## 0:00:00 Checking assertions in step 12..
## 0:00:00 BMC failed!
## 0:00:00 Assert failed in dma_formal.dut: a_not_both
## 0:00:00 Status: FAILEDThe counterexample trace, read from the VCD the tool wrote, is short: write LEN = 2, write GO, send one word with TLAST (ERR is set and BUSY drops), write GO again without clearing ERR, send two words. At step 12 DONE and ERR are both 1. That is the STATUS = 0x6 the scratch simulation stumbled on, found on purpose.
One plan, two kinds of closure. Each plan item names how it closes: by a proof, by functional coverage, or by both. Most commercial flows can annotate the plan with formal status (proven, bounded to depth N, failed, cover reached or unreachable) next to simulation coverage; the mechanism is tool-specific, the idea is not.
Bounded proofs need a justified depth. A bound is evidence only if it is deeper than the behaviour it must cover. Measure it with covers: if the deepest interesting cover is reached at step 10, a bound of 25 explores well beyond it; if a required behaviour needs 70,000 cycles, no practical bound counts and you need a full proof or an abstraction. The bounded-proof sign-off lesson goes deeper.
Proof strength is measured too. A proven assertion that checks very little is a false pass in formal clothing. Formal coverage (which logic the proofs actually depend on) and mutation checks answer "would these properties notice a bug?", the formal twin of the fault campaign.
Unreachable means excluded, with a reason. Formal can prove a code coverage hole unreachable, which turns it into a reviewed exclusion instead of a guess.
The APB rules in the harness are assumptions because, in formal, nothing else drives the inputs. In simulation the bench's driver drives them, and the same rules become assertions that check the driver. That is why teams keep one property file per interface with a switch that turns input-side rules into assume for formal and assert for simulation. Every simulation run then validates the formal environment: if the real driver ever breaks an assumption, the formal proofs were made against a fictional master. The next lesson builds that APB checker and catches a broken driver with it. More on the pattern in Reusing Properties in Formal.
Too weak. The first version of the harness above gated every APB assumption on $past(rst_n), and had no "idle in reset" rule. The proofs passed. The cover trace for c_done_len3, read out of curiosity, showed the master asserting PSEL and PENABLE together in the first cycle after reset, with no setup cycle: an illegal master. A second reading showed PENABLE dropping in the middle of a wait state. Neither hole made a proof fail, but both meant the proofs covered behaviour no real master produces, and could have produced counterexamples nobody should debug. Both holes were found the same way: by reading a cover witness as if it were a waveform from a real bench.
Too strong. Add one innocent-looking assumption, "packets are always full length" (assume (!s_tlast)), and rerun. Every assertion still passes. But:
## 0:00:00 Reached cover statement in step 10 at dma_formal.dut: c_done_len3
## 0:00:00 Checking cover reachability in step 29..
## 0:00:00 Unreached cover statement at dma_formal.dut: c_err
## 0:00:00 Status: FAILEDThe over-constraint removed the whole error path, so any assertion about ERR now passes vacuously. The rule that prevents both failures: every assumption gets a cover for the behaviour it is supposed to allow, and every cover trace gets read at least once. The over-constraint scenario in the Formal course is the interview version of this story.
a_count_lt_len as "bounded, depth 40", not proven. A colleague says that is enough because jobs are at most 16 words in the tests. Is it?No. LEN is a 16-bit register, so the design allows jobs up to 65,535 words, and a depth of 40 cycles never reaches a COUNT anywhere near that. The test constraint is a property of the bench, not the design. Either get a full proof (here, induction succeeds because the property is inductive on its own) or add a helper invariant or abstraction until it converges, and record the depth argument explicitly if it stays bounded.
First, that the covers for the main behaviours (a finished job, an error, a W1C clear) are reached, which shows the assumptions are not so strong that they rule out real traffic. Second, read at least one cover trace as a waveform and check the environment looks like a real master: setup before access, signals held until PREADY. Under-constraint shows up there before it shows up as a confusing counterexample.
Next: the APB rules appeared twice in this lesson, as formal assumptions and as checks on the bench's driver. Assertion VIP and bind packages them once, attaches them to the DMA without touching the RTL, and catches a real driver bug with them.