Solutions: Counter and Induction

On this page

Part 10 of 10, lesson 21 of 24Capstone: A Chip-Block Verification LabAll levels

Why it matters

A true property that is not inductive has a counterexample to its step in a state reset cannot reach. The counter makes the shape small enough to see: states 10 to 14 satisfy never-15 and lead to it, and a held enable lets any of them repeat. The repair is one assertion that excludes the whole region, and it must itself be proved.

The helper and the windows

The helper is count <= 9. It is inductive on its own, because from any state at or below 9 the next state is at or below 9, and with it the full set closes at a window of two (the step and hold rules read history, so a window of one fails them). A set of just the range helper and never-15 closes at a window of one. Without the helper no window closes, whatever the depth.

mod10_counter.sv

// formal: prove 1 expect unproven slang top mod10_counter
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

mod10_counter.sv

// formal: prove 2 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

mod10_counter.sv

// formal: prove 1 expect pass slang top mod10_counter
`define FORMAL
// property-set mutation: every assertion except a_range and a_not15 is turned into a cover (its label starts with x_)
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) x_a_tc: cover (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    x_a_step: cover (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    x_a_hold: cover ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

mod10_counter.sv

// formal: prove 4 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

Stage 4 ran the same design without the helper: unproven at depth 10, with a bounded pass to depth 20. The FIFO shows the same shape with its tracked-slot helper, which says the memory word at the tracked slot equals the shadow value while the slot is being followed; without it the data property fails its step at every window to twelve, and with it the proof closes at window two.

The counter fault

Variant	Cause in the listing	Fix	Fails (step), smallest depth
W1	The wrap constant is 10 instead of 9: the counter counts to 10 and the terminal pulse arrives a count late.	`last = 9`.	`a_tc` (10), `a_range` (11), `a_step` (12); depth 11; depth 10 passes

The pulse is due when the count reads 9, which is at step 10 (one reset step, then nine counts). The faulty design pulses at 10 instead, so the pulse property fails at step 10. A bounded claim below depth 11 is therefore not a claim about the terminal pulse at all.

example.py

def counter(buggy, steps):
    count, rows, last = 0, [], 10 if buggy else 9
    for step in range(1, steps + 1):                 # step 1 is the first state after the reset; the enable is held high
        tc = int(count == last)
        rows.append(dict(step=step, count=count, tc=tc, a_tc=(tc == int(count == 9)), a_range=(count <= 9)))
        count = 0 if count == last else count + 1
    return rows
good, bad = counter(False, 14), counter(True, 14)
assert all(r["a_tc"] and r["a_range"] for r in good)
assert next(r["step"] for r in bad if not r["a_tc"]) == 10
assert next(r["step"] for r in bad if not r["a_range"]) == 11
assert [r["step"] for r in good if r["tc"]] == [10], "the correct pulse is at step 10"
assert [r["step"] for r in bad if r["tc"]] == [11], "the faulty pulse is one count late"
print("PASS: the pulse property fails at step 10 and the range property at step 11 on the faulty counter")

mod10_counter.sv

// formal: bmc 10 expect pass slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

mod10_counter.sv

// formal: bmc 11 expect fail slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

The assumed bound

In stage 4 a small module with a planted fault passed because its bound was written as an assumption. The same module with the bound asserted fails at depth 5. The design did not change between the two runs; the debt did. Every helper in this lab is asserted, and the ledger lists it as a property, never as an assumption.

bound_check_b.sv

// formal: bmc 5 expect fail slang top bound_check_b define BUG=1
`define FORMAL
// lesson-local counter with a small bound, second form
module bound_check_b #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  output reg  [1:0] c
);
  always @(posedge clk) begin
    if (rst) c <= 2'd0;
    else if (BUG == 1 && c == 2'd2) c <= 2'd3;
    else c <= (c == 2'd2) ? 2'd0 : c + 2'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) begin
    a_bound: assert (c <= 2'd2);
    a_never3: assert (c != 2'd3);
  end
`endif
endmodule

What the review looks for

The window is reported for every proof, with the failing assertion at the first window that fails.
The helper is proved on its own before it is used, and is asserted, never assumed.
A bounded pass one depth short of the fault is filed beside the counterexample.

Verify and debug

When a step fails, print the start state: whether reset can reach it decides everything. Prove a helper alone before conjoining it. If a proof passes with a fault planted, delete each assumption in turn.

Check yourself One word separates a proof that passes with a fault planted from one that fails. Which word, and what is it worth?

Assume against assert: an assumption prunes the fault from the model and the proof passes; an assertion tests the design and the fault fails. The word decides whether the proof checks the design or the wish.

Check yourself Why does a helper that excludes only some unreachable states not repair the counter?

The remaining unreachable states still lead to the violation. Only a statement that excludes the whole region, and is itself inductive, closes the step.

Check yourself The counter proof closes at a window of two and the cover needs depth 15. Why are both filed?

They answer different questions: the window justifies the word proven; the cover depth justifies that the wrap and the pulse can happen.

Navigate

Why it matters

The helper and the windows

The counter fault

The assumed bound

What the review looks for

Verify and debug

Related topics

Solutions: Counter and Induction

Why it matters

The helper and the windows

The counter fault

The assumed bound

What the review looks for

Verify and debug

Related topics

Why it matters

The helper and the windows

The counter fault

The assumed bound

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The helper and the windows

The counter fault

The assumed bound

What the review looks for

Verify and debug

Related topics

Up next