Formal with Simulation

Turn a block assumption into a system assertion with one line and a bind, measure what is lost without it, replay a formal cover trace as a directed test, and decide what stays in simulation.

Lesson: F7.4
Time: 20 min
Runs on: SymbiYosys
Check: 5 questions

The FIFO was proven under one assumption: the producer never pushes when full. A DMA engine, tired of waiting, pushed into a full FIFO once. Nothing fired in system simulation, because the assumption lived only in the formal bench.

Three Things Cross Between the Benches

What Crosses Between the Block and the SystemBlock-level formal on the left, system-level simulation on the right. Three things travel between them, each in a fixed direction.

Read the diagram as text

assume at the block: the producer never pushes when full
assert in the system: the same line, bound into the FIFO
cover trace: a reachable state formal found
directed test: the trace replayed in a simulator
system failure: a symptom seen in simulation or the lab
cover question: how could this state be reached? (F5.9)
one property file: a define picks the verb

assume at the block → one property file
one property file → assert in the system
cover trace → directed test: trace_tb.v
system failure → cover question

A block proven under an assumption is proven only where the assumption holds. The system bench is where that gets checked.

Formal proves the block; simulation runs the system. An assumption at the block becomes an assertion in the system. A cover trace becomes a directed test. A failure seen in the system becomes a cover for formal to explain.

One Line, Two Verbs

The property module and its bind (A7.1). Formal tools define FORMAL, so the line is an assumption there and an assertion everywhere else.

module fifo_rules(input clk, rst, push, full);
`ifdef FORMAL
  `define PROMISE assume     // block level: the producer's promise is an assumption
`else
  `define PROMISE assert     // system level: the same line, checked
`endif
  p_no_push_full: `PROMISE property (@(posedge clk) disable iff (rst) !(push && full));
    else $display("PROMISE failed: push while full, cycle %0d", $root.tb.cycles);
endmodule

bind fifo_nf fifo_rules u_rules(.clk(clk), .rst(rst), .push(push), .full(full));

fifo_nf, no full guard	Measured result
With the promise as an assumption, `abc pdr`	Prove PASS (abc pdr)
Without it, `bmc` depth 20	FAIL at reported step 7: `used` reaches 5

The FIFO is correct only under the promise. Its proof is a deal: the system must keep its side.

The block without its promise

Measured: the FIFO alone, without the promise, bmc depth 20: FAIL at reported step 7. The solver plays the producer and breaks the promise at once.

This FIFO has no full guard, which saves logic on its write path. Its proof holds only while every producer keeps the promise. Bound into the system bench, the same line checks every producer on every cycle.

The Promise, Checked in the System

Cause and Symptom, MeasuredThe faulty producer stops waiting once. The promise fires at that cycle; without it, the first sign is 7 cycles later, at the sink.

Read the diagram as text

cycle 10: push while full: the promise assertion fires here
used = 5, full drops: the extra write overwrites the oldest entry
producer keeps pushing: largest used: 7
cycle 17: sink error: expected 4, read 12

cycle 10: push while full → used = 5, full drops
used = 5, full drops → producer keeps pushing
producer keeps pushing → cycle 17: sink error

Verilator runs of the system bench (40 items, a sink that reads in bursts). The symptom names the FIFO; the cause was the producer.

System bench on Verilator	Promise assertion	Sink	Largest `used`
Faulty producer, promise bound	fires at cycle 10	error at cycle 17	7
Correct producer, promise bound	silent; `full` high for 106 cycles	no error	4
Faulty producer, no bind	not there	error at cycle 17	7

Verilator 5.052. The second row is a real pass: the promise was tested on every one of those cycles (A1.3).

With the bind, the failure names the producer at the cycle it broke the promise. Without it, the first sign is 7 cycles later and points at the FIFO, whose proof says it is correct. That gap is the cost of a promise nobody checks.

A Cover Trace Becomes a Test

Replayed step	push	pop	used	full
1	1	1	0	0
2	1	0	1	0
3	1	0	2	0
4	1	0	3	0
5	0	1	4	1
6	0	0	3	0

SBY's trace0_tb.v for the cover "full, then a read" (Cover reached, reported step 6), run on Verilator 5.052. It needed one edit: Verilator rejects it with "Duplicate declaration of signal: 'genclock'", so the duplicate reg genclock = 1; line was deleted.

Step 5 matches the formal trace: four entries, full high, a read. Any simulator can now reach the state the solver found, which turns a formal cover into a regression test.

What Stays in Simulation

Formal, at the block	Simulation, at the system
control logic, handshakes, data integrity	the check that every block assumption holds
corner cases within the depth budget	long scenarios across many blocks
proofs for all time where they close	performance, software bring-up, anything too deep

The answer for each block is a column in the plan (F7.5).

Coverage combines by direction. A bin that formal proves unreachable is waived from the simulation goal (F5.7); a bin that simulation hits proves nothing beyond that trace. A proven block counts toward sign-off only with its assumptions checked in the system.

Semiformal runs sit between the two: simulate to a deep state, then search formally from there. They find bugs; they prove nothing about states the trace did not reach.

Asked in Interviews

Question	Answer
How does an assumption at one level become an assertion at the next?	The same property text with the verb picked by a define, bound into the system bench. The block proof is valid only where that assertion never fires.
What does a formal cover trace give the simulation team?	A directed test that reaches a state formal found. SBY writes it as a Verilog testbench; on Verilator it needed one edit.
What is semiformal verification?	Simulation to a deep state, then formal search from it. Deep bug hunting, not a proof.

Try It

The lab is fifo_nf with the promise in props.sv as an assumption, abc pdr: Prove PASS (abc pdr) in 0.7 s. The simulation twin is the system bench with the faulty producer and the promise bound as an assertion.

One property, two verbs.

assume property (@(posedge clk) disable iff (rst) !(push && full));   // props.sv, formal
assert property (@(posedge clk) disable iff (rst) !(push && full));   // system bench

Name the assumption
Read props.sv and say, in one sentence, what the FIFO needs from its producer.
Remove it
Clear props.sv, set mode bmc, depth 20, and run. Read used at the failing step.
Check it in the system
Run the simulation twin. Then delete the bind line and run again: count the cycles between the two messages.

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 fifo_nf(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty, output reg [2:0] used = 0);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr = 0, rd_ptr = 0;
  assign full  = used == 3'd4;
  assign empty = used == 3'd0;
  wire rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; used <= 0; end
    else begin
      if (push) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end   // no full guard
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      used <= used + push - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(used <= 3'd4);
    if (empty || full) assert(wr_ptr == rd_ptr);
  end
`endif
endmodule

assume property (@(posedge clk) disable iff (rst) !(push && full));

Check Yourself

Predict the outputfifo_nf with no props.sv (the promise removed), mode bmc, depth 20, smtbmc yices, reset assumed in step 0. At which step does SBY report the failure?

module fifo_nf(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty, output reg [2:0] used = 0);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr = 0, rd_ptr = 0;
  assign full  = used == 3'd4;
  assign empty = used == 3'd0;
  wire rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; used <= 0; end
    else begin
      if (push) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end   // no full guard
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      used <= used + push - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(used <= 3'd4);
    if (empty || full) assert(wr_ptr == rd_ptr);
  end
`endif
endmodule

Predict the outputfifo_nf with the promise as an assumption in props.sv, mode prove, abc pdr, reset assumed in step 0. The verdict is:

module fifo_nf(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty, output reg [2:0] used = 0);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr = 0, rd_ptr = 0;
  assign full  = used == 3'd4;
  assign empty = used == 3'd0;
  wire rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; used <= 0; end
    else begin
      if (push) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end   // no full guard
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      used <= used + push - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(used <= 3'd4);
    if (empty || full) assert(wr_ptr == rd_ptr);
  end
`endif
endmodule

Read included file: props.sv

assume property (@(posedge clk) disable iff (rst) !(push && full));

ConceptWhich handoff statement is wrong?

A failure seen in the system can be posed as a cover.A formal cover trace can be replayed as a directed test.A block proven under an assumption is proven in the system.An assumption at the block is an assertion in the system.

ConceptA block is formally signed off. What should simulation still check?

Only the datapath, since formal covered the control logic.Nothing: a block proof covers every system that uses it.The same assertions again, to confirm the formal result.Its assumptions, long multi-block scenarios and performance.

Read the waveformIn the measured trace of the FIFO without its promise, at which step does used first exceed 4?