Design for Formal, and the Formal Engineer's Week

Know the design habits that make a block cheap to prove, see one measured before-and-after, and know what a formal engineer's week is made of.

Lesson: F9.3
Time: 20 min
Runs on: SymbiYosys
Check: 4 questions

Two engineers were given the same FIFO to prove. One got the simulation RTL: int counters, a debug timestamp in the control, two reset styles. The other got it after an afternoon of changes by its designer. The first spent two days writing helpers; the second proof closed on the first run, with the function unchanged.

Seven Habits

Habit	Before	After
State as wide as it needs to be	`int wp, rp, used;`	`reg [1:0] wp, rp; reg [2:0] used;`
Control apart from data	payload bits steer the queue	the queue never reads the payload (data independence, F4.4)
No free-running counter in control	a 16-bit timer in every cone	a `FORMAL` switch narrows it to 4 bits (F8.3)
One reset style	async on half the flops, sync on the rest	one synchronous reset
Exposed state	the count is internal	the count is a port or a bindable signal
Small blocks, clean interfaces	one module with three jobs	three modules, each with a handshake
Parameters for depth and width	magic numbers	`DEPTH`, `WIDTH` that a bench can shrink (F4.5)

Seven habits a designer can adopt in an afternoon. None changes the function.

Each habit removes states the design never reaches but the solver must still consider. A 32-bit pointer that only ever holds 0 to 2 leaves four billion values the induction step may start from.

The habits cost little when the RTL is first written: a parameter, a narrower declaration, a switch around debug logic. Ask for them at the design review, before the first UNKNOWN arrives.

One FIFO, Two Encodings

	`fifo_f`, two- and three-bit state	Same FIFO, `int` state (A8.1)
Flop bits in the RTL (Yosys)	16	105
`abc pdr`, no helpers	Prove PASS (abc pdr), 1.3 s	Prove PASS (abc pdr), 1.5 s
k-induction, k = 12, no helpers	UNKNOWN at k = 12 (base case passed, induction step failed)	UNKNOWN at k = 12 (base case passed, induction step failed)
k-induction, k = 12, F8.1's helpers	Prove PASS (k = 12), 0.9 s	UNKNOWN at k = 12 (base case passed, induction step failed)

DEPTH 3, WIDTH 8, the same F8.1 properties and tracker in both; reset assumed in step 0. Only the declarations of wp, rp and used differ.

IC3 closes both in about the same time: it builds its own invariant and the extra bits cost little here. k-induction tells them apart. The helpers that close fifo_f leave the int copy UNKNOWN: its induction step starts with wp = -4 and rp = -2, which pass wp < DEPTH because int is signed (F2.4, F4.6).

So the cost of wide state is not always seconds. It is the helper set. The narrow design needs F8.1's helpers; the wide one needs more, written by someone who knows the design well.

A Timer the Bench Can Shrink

`wdt16`	Cover `bark`, depth 40
16-bit timer, as built	cover unreached within depth 40
4-bit timer, the `FORMAL` setting	Cover PASS, last cover reached at step 18

F8.3's watchdog: the bark needs a full count, 65,535 cycles at 16 bits. One parameter the bench can override brings it within reach.

A designer who writes the width as a parameter has done the abstraction for you; one who hard-codes 16 bits leaves you to cut the counter yourself (F4.5).

The Week

A Formal Engineer's Week (Typical, Not Measured)Five days as a strip. The proportions are a typical shape, not a measurement; the order repeats every block.

Read the diagram as text

Monday: read: spec and RTL; plan rows and assumptions with the designer
Tuesday: wiggle: covers before asserts; first traces shown to the designer
Wednesday: debug: counterexamples, one by one: RTL, assumption, property or reset
Thursday: converge: helpers, a split, an engine change for the UNKNOWNs
Friday: regress: nightly runs, plan fields filled, assumptions handed to DV

Monday: read → Tuesday: wiggle
Tuesday: wiggle → Wednesday: debug
Wednesday: debug → Thursday: converge
Thursday: converge → Friday: regress
Thursday: converge → Wednesday: debug: a new trace

Most hours go to reading traces with the designer. The proof is the last of them.

Formal work is reading: specs, RTL and traces, mostly with the designer in the room. Convergence work comes after the bench is right, and regressions after that.

The handoff to simulation is weekly (F7.4). The assumption list and the cover traces go out; the question "did the system keep our assumptions?" comes back. Ask designers to run covers on fresh RTL before any testbench exists.

A Third Block, Without Running It

F7.1's counter, rewritten with an asynchronous reset on the debug mirror alone.

module ctr_dbg(input clk, rst, arst_n, en, fast_in, ...);
  always @(posedge clk) if (rst) count <= 0; else ...      // synchronous
  always @(posedge clk or negedge arst_n)                  // asynchronous,
    if (!arst_n) dbg <= 0; else dbg <= count;              // debug mirror only

It breaks "one reset style". The bench must say what the second reset is: tie it to the first, or let SBY model it with async2sync or multiclock on (F1.6). Either is a plan entry with a reason.

Asked in Interviews

Question	Answer
What does a formal engineer do all day?	Plan from the spec, wiggle with covers, debug traces with the designer, converge proofs, regress, and hand assumptions and cover traces to DV.
What is design for formal?	Right-sized state, control apart from data, no free-running counters in control, one reset, exposed state, small blocks, parameters.
What would you ask a designer to change first?	Whatever the checklist flags, with a measured pair like the FIFO above as the reason.

Try It

The lab is fifo_f with F8.1's helpers under k-induction: Prove PASS (k = 12), 0.9 s. The twins are its int copy and the two timers. Fill the table from the summaries.

fifo_f (F8.1)

  reg [1:0] wp = 0, rp = 0;
  reg [2:0] used = 0;

Prove PASS (k = 12) with the helpers.

As A8.1 declares it

  integer wp = 0, rp = 0, used = 0;

UNKNOWN at k = 12 (base case passed, induction step failed) with the same helpers.

Run the pair
Run the lab and its int twin. Open the twin's induction trace and read wp and rp in step 0.
Run IC3
Run both under abc pdr and compare the times.
Run the timers
Run the bark cover at both widths.
Name the habit
For the third block above, name the habit it breaks and the bench line it needs.

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_f #(parameter DEPTH = 3, WIDTH = 8)(input clk, rst, write_en, read_en,
  input [WIDTH-1:0] write_data, output full, empty, read_valid, output [WIDTH-1:0] read_data);
  reg [WIDTH-1:0] mem [0:3];                    // four slots, as A8.1
  reg [WIDTH-1:0] resp = 0, late_data = 0;
  reg resp_valid = 0, late_valid = 0;
  reg [1:0] wp = 0, rp = 0;
  reg [2:0] used = 0;
  wire take_w = write_en && used < DEPTH;
  wire take_r = read_en && used > 0;
  assign full = used == DEPTH;
  assign empty = used == 0;
  assign read_valid = resp_valid;
  assign read_data = resp;
  always @(posedge clk)
    if (rst) begin used <= 0; wp <= 0; rp <= 0; resp_valid <= 0; late_valid <= 0; end
    else begin
      late_valid <= resp_valid;
      if (resp_valid) late_data <= resp;
      resp_valid <= take_r;
      if (take_r) begin resp <= mem[rp]; rp <= rp == DEPTH - 1 ? 2'd0 : rp + 2'd1; end
      if (take_w) begin
        mem[wp] <= write_data;
        wp <= wp == DEPTH - 1 ? 2'd0 : wp + 2'd1;
      end
      used <= used + take_w - take_r;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: two consecutive accepted writes, picked by the solver, and their data.
  wire f_pick = $anyseq;
  reg f_in1 = 0, f_in2 = 0, f_out1 = 0, f_done = 0, f_chk1 = 0, f_chk2 = 0;
  reg [1:0] f_ahead = 0;                  // entries in front of the first tracked one
  reg [WIDTH-1:0] f_d1 = 0, f_d2 = 0;
  reg f_tr = 0;                           // an accepted read last cycle
  always @(posedge clk)
    if (rst) begin f_in1 <= 0; f_in2 <= 0; f_out1 <= 0; f_done <= 0; f_chk1 <= 0; f_chk2 <= 0; f_tr <= 0; end
    else begin
      f_tr <= take_r; f_chk1 <= 0; f_chk2 <= 0;
      if (!f_in1 && !f_out1 && !f_done && take_w && f_pick) begin
        f_in1 <= 1; f_d1 <= write_data; f_ahead <= used - take_r;
      end else if ((f_in1 || f_out1) && !f_in2 && take_w) begin f_in2 <= 1; f_d2 <= write_data; end
      if (f_in1 && take_r) begin
        if (f_ahead == 0) begin f_in1 <= 0; f_out1 <= 1; f_chk1 <= 1; end
        else f_ahead <= f_ahead - 2'd1;
      end
      if (f_out1 && f_in2 && take_r) begin f_out1 <= 0; f_in2 <= 0; f_done <= 1; f_chk2 <= 1; end
    end
  always @(posedge clk) if (!rst) begin
    if (f_chk1) assert(read_valid && read_data == f_d1);   // nothing lost, nothing changed
    if (f_chk2) assert(read_valid && read_data == f_d2);   // the next one comes next
    assert(used <= DEPTH);                                 // glue: the count
    assert(full == (used == DEPTH) && empty == (used == 0));
    assert(wp < DEPTH && rp < DEPTH);                      // glue: the pointers
    assert(used == (wp >= rp ? wp - rp : wp + DEPTH - rp) || used == DEPTH && wp == rp);
    assert(read_valid == f_tr);                            // valid only after an accepted read
    // helpers for k-induction: where the tracked data sits
    if (f_in1) assert(f_ahead < used && mem[rp + f_ahead >= DEPTH ? rp + f_ahead - DEPTH : rp + f_ahead] == f_d1);
    if (f_in1 && f_in2) assert(f_ahead + 3'd2 <= used && mem[rp + f_ahead + 1 >= DEPTH ? rp + f_ahead + 1 - DEPTH : rp + f_ahead + 1] == f_d2);
    if (f_in1 && !f_in2) assert(f_ahead + 2'd1 == used);
    if (f_out1 && f_in2) assert(used != 0 && mem[rp] == f_d2);
    if (f_out1 && !f_in2) assert(used == 0);
    if (f_chk1 || f_chk2) assert(f_tr);
    assert(!(f_in1 && f_out1) && !(f_done && (f_in1 || f_out1 || f_in2)) && (!f_in2 || f_in1 || f_out1));
  end
`endif
endmodule

Check Yourself

Predict the outputThe int FIFO with F8.1's helpers, mode prove, depth 12, smtbmc yices, reset assumed in step 0. The verdict:

module fifo_f #(parameter DEPTH = 3, WIDTH = 8)(input clk, rst, write_en, read_en,
  input [WIDTH-1:0] write_data, output full, empty, read_valid, output [WIDTH-1:0] read_data);
  reg [WIDTH-1:0] mem [0:3];                    // four slots, as A8.1
  reg [WIDTH-1:0] resp = 0, late_data = 0;
  reg resp_valid = 0, late_valid = 0;
  integer wp = 0, rp = 0, used = 0;            // A8.1: int state
  wire take_w = write_en && used < DEPTH;
  wire take_r = read_en && used > 0;
  assign full = used == DEPTH;
  assign empty = used == 0;
  assign read_valid = resp_valid;
  assign read_data = resp;
  always @(posedge clk)
    if (rst) begin used <= 0; wp <= 0; rp <= 0; resp_valid <= 0; late_valid <= 0; end
    else begin
      late_valid <= resp_valid;
      if (resp_valid) late_data <= resp;
      resp_valid <= take_r;
      if (take_r) begin resp <= mem[rp]; rp <= rp == DEPTH - 1 ? 2'd0 : rp + 2'd1; end
      if (take_w) begin
        mem[wp] <= write_data;
        wp <= wp == DEPTH - 1 ? 2'd0 : wp + 2'd1;
      end
      used <= used + take_w - take_r;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: two consecutive accepted writes, picked by the solver, and their data.
  wire f_pick = $anyseq;
  reg f_in1 = 0, f_in2 = 0, f_out1 = 0, f_done = 0, f_chk1 = 0, f_chk2 = 0;
  reg [1:0] f_ahead = 0;                  // entries in front of the first tracked one
  reg [WIDTH-1:0] f_d1 = 0, f_d2 = 0;
  reg f_tr = 0;                           // an accepted read last cycle
  always @(posedge clk)
    if (rst) begin f_in1 <= 0; f_in2 <= 0; f_out1 <= 0; f_done <= 0; f_chk1 <= 0; f_chk2 <= 0; f_tr <= 0; end
    else begin
      f_tr <= take_r; f_chk1 <= 0; f_chk2 <= 0;
      if (!f_in1 && !f_out1 && !f_done && take_w && f_pick) begin
        f_in1 <= 1; f_d1 <= write_data; f_ahead <= used - take_r;
      end else if ((f_in1 || f_out1) && !f_in2 && take_w) begin f_in2 <= 1; f_d2 <= write_data; end
      if (f_in1 && take_r) begin
        if (f_ahead == 0) begin f_in1 <= 0; f_out1 <= 1; f_chk1 <= 1; end
        else f_ahead <= f_ahead - 2'd1;
      end
      if (f_out1 && f_in2 && take_r) begin f_out1 <= 0; f_in2 <= 0; f_done <= 1; f_chk2 <= 1; end
    end
  always @(posedge clk) if (!rst) begin
    if (f_chk1) assert(read_valid && read_data == f_d1);   // nothing lost, nothing changed
    if (f_chk2) assert(read_valid && read_data == f_d2);   // the next one comes next
    assert(used <= DEPTH);                                 // glue: the count
    assert(full == (used == DEPTH) && empty == (used == 0));
    assert(wp < DEPTH && rp < DEPTH);                      // glue: the pointers
    assert(used == (wp >= rp ? wp - rp : wp + DEPTH - rp) || used == DEPTH && wp == rp);
    assert(read_valid == f_tr);                            // valid only after an accepted read
    // helpers for k-induction: where the tracked data sits
    if (f_in1) assert(f_ahead < used && mem[rp + f_ahead >= DEPTH ? rp + f_ahead - DEPTH : rp + f_ahead] == f_d1);
    if (f_in1 && f_in2) assert(f_ahead + 3'd2 <= used && mem[rp + f_ahead + 1 >= DEPTH ? rp + f_ahead + 1 - DEPTH : rp + f_ahead + 1] == f_d2);
    if (f_in1 && !f_in2) assert(f_ahead + 2'd1 == used);
    if (f_out1 && f_in2) assert(used != 0 && mem[rp] == f_d2);
    if (f_out1 && !f_in2) assert(used == 0);
    if (f_chk1 || f_chk2) assert(f_tr);
    assert(!(f_in1 && f_out1) && !(f_done && (f_in1 || f_out1 || f_in2)) && (!f_in2 || f_in1 || f_out1));
  end
`endif
endmodule

ConceptWhich design habit is wrong?

Use one synchronous reset style for every flop in the block.Put the debug timestamp in the pointers' block so formal sees it.Size every pointer with $clog2(DEPTH) bits, never with an int.Narrow each long timer under a parameter the formal bench can set.

ConceptWhy does a 32-bit int pointer hurt induction more than BMC?

BMC ignores the width of every signal, and induction does not ignore it.The solver cannot reason about 32-bit values at all, so it gives up.Induction may start anywhere the properties allow; BMC starts from reset.Induction unrolls many more steps than BMC does at the same depth.

ConceptWhat takes most of a formal engineer's week?

Writing SVA syntax, line by line, from the language reference.Waiting for the solvers to finish their long runs on the farm.Running, checking and archiving the nightly regression results.Reading counterexamples with the designer, and the work around them.

Remember

Design habits that remove unreachable states: right-sized state, control apart from data, narrowed timers, one reset, exposed state, small blocks, parameters.
Measured: IC3 closes both FIFO encodings in similar time; k-induction with the same helpers closes only the narrow one.
A parameterised timer turns an unreachable cover into a reached one.
A formal week is mostly reading traces with the designer; the proof comes last.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.