The Formal Testbench and the Master Rule

Build a formal bench from its four parts, run one rule as an assertion and as an assumption, and see why the verb decides what gets checked.

Lesson: F3.1
Time: 15 min
Runs on: SymbiYosys
Check: 4 questions

A register slice reached the formal team with a bench copied from a simulation checker. Its downstream rule, hold the data while stalled, was an assume, because in that bench the rule described the neighbour block. In the formal bench the slice was that neighbour, so the run passed in under a second, and the slice corrupted data on its first stall in silicon.

The counterexample: new data during a stall

Measured with smtbmc yices at depth 20. The stall starts at step 2; the sampled violation is step 3, reported at step 4. The byte values are the solver's choice.

Four Parts, No Stimulus

A Formal Bench Has Four Parts and No StimulusThe solver drives every input. Assumptions prune what it may drive; assertions check what the design does with it. The checker module holds both and is bound to the design. Arrows mean "acts on".

call: who calls whomdata: where the transaction goes

Read the diagram as text

Solver: any value on every input, every step (F1.2)
Assumptions: about inputs: what the neighbours promise
slice (the DUT): the synthesised RTL, untouched
Bound checker: ports and internals as inputs, behind FORMAL (A7.1)
Assertions: about outputs and state: what the DUT promises
Covers: what must stay possible (F3.5)

Solver → slice (the DUT): in_valid, in_data, out_ready
Assumptions → Solver: prunes
slice (the DUT) → Bound checker: bind
Bound checker → Assumptions: in
Bound checker → Assertions: out
Bound checker → Covers

No driver, no clock generator, no scoreboard class. The checker is the only monitor, and every rule in it is either a promise about an input or a claim about an output.

A formal bench is the design, a checker bound to it (A7.1 Packaging and binding), assumptions about inputs and assertions about outputs and state. Nothing drives the inputs: the solver picks them (F1.2). Covers come later in this module; they show the assumptions left the interesting behaviour possible.

Assume What Comes in, Assert What Goes Out

Run A: the downstream rule as a claim

assume property (@(posedge clk) disable iff (rst) in_valid && !in_ready |=> in_valid && in_data == in_data_q);
assert property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data));
assert property (@(posedge clk) disable iff (rst) in_valid && in_ready |=> out_valid);

FAIL at reported step 4.

Run B: one word changed

assume property (@(posedge clk) disable iff (rst) in_valid && !in_ready |=> in_valid && in_data == in_data_q);
assume property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data));
assert property (@(posedge clk) disable iff (rst) in_valid && in_ready |=> out_valid);

BMC PASS to depth 20, with the bug still in the RTL.

An input is the environment's choice, so a rule about it is a promise you accept. An output is the design's work, so a rule about it is a claim you check. Run B tells the solver to discard every world where out_data moves during a stall: the bug's worlds vanish, and the run is green (F1.3).

Nothing in run B's summary warns you. Apart from timestamps it reads line for line like the fixed design's pass, ending DONE (PASS, rc=0). F3.2 shows the cover that would have exposed it.

Run	Properties in	Measured result	Time
A: downstream rule as `assert`	props.sv	FAIL at reported step 4	647 ms
B: the same line as `assume`	props.sv	BMC PASS to depth 20	661 ms
A, clocked immediate form	design.sv	FAIL at reported step 4	514 ms
B, clocked immediate form	design.sv	BMC PASS to depth 20	533 ms
Fixed RTL, rule asserted	props.sv	BMC PASS to depth 20	643 ms
Fixed RTL, upstream assumption deleted	props.sv	BMC PASS to depth 20	643 ms
Buggy RTL, upstream assumption deleted	props.sv	FAIL at reported step 4	643 ms

smtbmc yices, mode bmc, depth 20, reset assumed in step 0. Both forms agree on every run. Time is wall time on this machine.

The same checker can serve the other side of the link with the verbs swapped. That reuses the text, not the work: the swapped run needs its own covers and often an assumption the first side never needed.

From SVA to What the Engine Runs

Concurrent SVA	What the engine runs (clocked immediate form)
`a \|-> b`	`if (a) assert(b);`
`a \|=> b`	a flop `a_q <= a;` then `if (a_q) assert(b);`
`a \|-> ##2 b`	a two-deep shift of `a`, then `if (a_q2) assert(b);`
`a \|-> ##[1:4] b`	a counter started by `a` and cleared by `b`; it fails if it runs out
`$past(x)`	a register `x_q <= x;` with a declared initial value, or read behind an `f_past_valid` flop
`$stable(x)`	`x == x_q`
`$rose(x)`	`x && !x_q`
`disable iff (rst)`	`if (!rst)` on the check, and `!rst &&` on every pending flop

The eight constructs of the engine's concurrent subset. A1.2 Clocks and sampling covers the first-tick value of $past. This page declares every history register with an initial value. Reset holds in step 0, so no live check reads that first value.

This engine checks $stable(out_data) directly, because out_data is a register with a declared initial value. It refuses history on a primary input: the upstream rule written with $stable(in_data) comes back UNSUPPORTED_INPUT_HISTORY: in_data. So the bench keeps in_data_q, last cycle's in_data, and the rule reads in_data == in_data_q.

That asks the same question as $stable(in_data) from step 1 on; step 0 is reset, where disable iff turns the rule off. The engine also samples disable iff at the clock edge, so every lab here uses one clock and a synchronous, active-high rst.

Asked in Interviews

Question	Answer
How is a formal testbench structured?	The DUT, a bound checker, assumptions on inputs, assertions on outputs and state, and any modelling code, all behind `FORMAL`.
Why "assume inputs, assert outputs"?	An assumption on an output deletes the design behaviours you meant to check, and the pass looks like any other pass.
Can I verify the master by swapping assume and assert in the slave checker?	The text is reusable. The run needs its own covers and usually a few new assumptions.

Try It

props.sv: the concurrent form

assume property (@(posedge clk) disable iff (rst) in_valid && !in_ready |=> in_valid && in_data == in_data_q);
assert property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data));
assert property (@(posedge clk) disable iff (rst) in_valid && in_ready |=> out_valid);

One promise about the input side, two claims about the output side.

The clocked immediate form of the same three rules

always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [7:0] in_data_q=0;          // last cycle's in_data
  always @(posedge clk) in_data_q <= in_data;
  reg in_stall_q=0, out_stall_q=0, accept_q=0;
  reg [7:0] out_data_q=0;
  always @(posedge clk) begin
    in_stall_q  <= !rst && in_valid && !in_ready;
    out_stall_q <= !rst && out_valid && !out_ready;
    accept_q    <= !rst && in_valid && in_ready;
    out_data_q  <= out_data;
    if (!rst && in_stall_q)  assume(in_valid && in_data == in_data_q);   // in: upstream
    if (!rst && out_stall_q) assert(out_valid && out_data == out_data_q);   // out: downstream
    if (!rst && accept_q)    assert(out_valid);
  end

Each |=> becomes a flop that remembers its antecedent.

The whole task. Depth is the default, 20. read_verilog -formal defines FORMAL, so the bench lines never reach synthesis.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv props.sv
prep -top slice
[files]
design.sv
props.sv

Label the rules
In props.sv, mark each line "in" or "out" by the signals it constrains.
Run with the bug
Run as it is: FAIL at reported step 4. In the trace find the stall and the byte that replaced the held one.
Change the verb
Change the downstream assert to assume and run: BMC PASS to depth 20. What did the tool stop looking at?
Fix the RTL
Put assert back. Make the data register load only on in_valid && in_ready and run: BMC PASS to depth 20.
Delete the upstream promise
Remove the first line of props.sv and run the fixed design again: BMC PASS to depth 20. These two claims never relied on it.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module slice(input clk, rst, in_valid, input [7:0] in_data, input out_ready,
  output in_ready, output reg out_valid=0, output reg [7:0] out_data=0);
  assign in_ready = !out_valid || out_ready;
  always @(posedge clk) begin
    if (rst) out_valid <= 0;
    else if (in_ready) out_valid <= in_valid;
    if (in_valid) out_data <= in_data;   // bug: loads during a stall
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [7:0] in_data_q=0;          // last cycle's in_data
  always @(posedge clk) in_data_q <= in_data;
`endif
endmodule

assume property (@(posedge clk) disable iff (rst) in_valid && !in_ready |=> in_valid && in_data == in_data_q);
assert property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data));
assert property (@(posedge clk) disable iff (rst) in_valid && in_ready |=> out_valid);

Check Yourself

Predict the outputslice with the stall bug, mode bmc, default depth 20, smtbmc yices, reset assumed in step 0. props.sv holds the upstream rule as assume, the downstream rule as assume and the accept rule as assert. The summary verdict is:

module slice(input clk, rst, in_valid, input [7:0] in_data, input out_ready,
  output in_ready, output reg out_valid=0, output reg [7:0] out_data=0);
  assign in_ready = !out_valid || out_ready;
  always @(posedge clk) begin
    if (rst) out_valid <= 0;
    else if (in_ready) out_valid <= in_valid;
    if (in_valid) out_data <= in_data;   // bug: loads during a stall
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [7:0] in_data_q=0;          // last cycle's in_data
  always @(posedge clk) in_data_q <= in_data;
`endif
endmodule

Read included file: props.sv

assume property (@(posedge clk) disable iff (rst) in_valid && !in_ready |=> in_valid && in_data == in_data_q);
assume property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data));
assert property (@(posedge clk) disable iff (rst) in_valid && in_ready |=> out_valid);

ConceptWhich line in the slice checker is written with the wrong verb?

assume property (... in_valid && !in_ready |=> in_valid);assume property (... out_valid && !out_ready |=> $stable(out_data));cover property (... out_valid && !out_ready && in_valid);assert property (... in_valid && in_ready |=> out_valid);

ConceptWhy does |=> become a flop in the clocked immediate form?

The engine has no |=> operator, so the consequent is dropped.The flop makes the consequent optional when the antecedent is false.The consequent is checked a sample later, so the antecedent is stored.The flop delays the checker's clock by one cycle, so it samples late.

Read the waveformIn the run-A trace, at which step does out_data change while the previous step was a stall (out_valid high, out_ready low)?

The counterexample: new data during a stall

Measured with smtbmc yices at depth 20. The stall starts at step 2; the sampled violation is step 3, reported at step 4. The byte values are the solver's choice.

Step 0, the reset stepStep 4, the last stepStep 1, where in_valid first risesStep 3

Remember

A formal bench is the DUT, a bound checker, assumptions on inputs and assertions on outputs and state; the solver is the stimulus.
Assume what comes in, assert what goes out. An assumption on an output deletes the bug and the pass looks normal.
Every concurrent construct has an immediate form: |=> is a flop, $past is a register, disable iff clears pending flops.
This engine refuses $past and $stable on primary inputs; keep a registered copy in the bench.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.