Four Counterexamples Worked

On this page

Part 8 of 10, lesson 10 of 13Methodology and DebugAll levels

Why it matters

Triage becomes a habit after four runs end to end: a starving arbiter, a scoreboard that needs a rule from the source, a free cut that invents arithmetic, an induction step that leaks. Each has the failing run, trace, diagnosis, fix and proof.

Job of this lesson: read four failures to their root causes and prove all four after the fix.

Case 1: a design bug in the arbiter

With the planted bug the pointer stops advancing when requester 0 wins. A helper invariant, waited cycles plus requesters still ahead at most 3, fails at step 2; the requirement itself fails only at step 5 with the helpers off.

rr_arbiter.sv

// formal: bmc 3 expect fail slang top rr_arbiter define BUG=1
`define FORMAL
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  reg [1:0] last;
  wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
                       (last == 2'd1) ? 4'b1100 :
                       (last == 2'd2) ? 4'b1000 : 4'b0000;
  wire [3:0] hi_req  = req & hi_mask;
  wire [3:0] lo_req  = (BUG == 3) ? (req | (4'b0001 << last)) : req;
  function [3:0] lowest;
    input [3:0] v;
    lowest = v & (~v + 4'd1);
  endfunction
  wire [3:0] g_hi = lowest(hi_req);
  wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
  assign grant = g_hi | g_lo;
  wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
  always @(posedge clk) begin
    if (rst) last <= 2'd3;
    else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [2:0] wt0, wt1, wt2, wt3;
  always @(posedge clk) begin
    if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
    else begin
      wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
      wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
      wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
      wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
    end
  end
  always @(*) if (!init) begin
    a_onehot0:  assert ((grant & (grant - 4'd1)) == 4'd0);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    a_wt0: assert (wt0 <= 3'd3);
    a_wt1: assert (wt1 <= 3'd3);
    a_wt2: assert (wt2 <= 3'd3);
    a_wt3: assert (wt3 <= 3'd3);
  end
  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  endfunction
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
      h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
      h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
      h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
    end
  end endgenerate
  always @(*) if (!init) begin
    c_g0: cover (grant[0]);
    c_g1: cover (grant[1]);
    c_g2: cover (grant[2]);
    c_g3: cover (grant[3]);
    c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
    c_idle: cover (req == 4'b0000 && grant == 4'b0000);
  end
`endif
endmodule

Step	req	last	grant	wt3	wt3 + ahead(3)	Which condition breaks
1	1111	3	0001	0	3	None: requester 0 first after reset
2	any	3	-	1	4	`h_wt3`: three requesters still ahead of requester 3, because the pointer did not move

Diagnosis: the pointer should be 0 at step 2, giving 1 + 2 = 3. Legal start, no excluding rule, replays on the design: a design bug. Fix: advance the pointer on every grant; the proof then holds at depth 4:

rr_arbiter.sv

// formal: prove 4 expect pass slang top rr_arbiter
`define FORMAL
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  reg [1:0] last;
  wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
                       (last == 2'd1) ? 4'b1100 :
                       (last == 2'd2) ? 4'b1000 : 4'b0000;
  wire [3:0] hi_req  = req & hi_mask;
  wire [3:0] lo_req  = (BUG == 3) ? (req | (4'b0001 << last)) : req;
  function [3:0] lowest;
    input [3:0] v;
    lowest = v & (~v + 4'd1);
  endfunction
  wire [3:0] g_hi = lowest(hi_req);
  wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
  assign grant = g_hi | g_lo;
  wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
  always @(posedge clk) begin
    if (rst) last <= 2'd3;
    else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [2:0] wt0, wt1, wt2, wt3;
  always @(posedge clk) begin
    if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
    else begin
      wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
      wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
      wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
      wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
    end
  end
  always @(*) if (!init) begin
    a_onehot0:  assert ((grant & (grant - 4'd1)) == 4'd0);
    a_no_phantom: assert ((grant & ~req) == 4'd0);
    a_work_cons:  assert (!(|req) || (|grant));
    a_wt0: assert (wt0 <= 3'd3);
    a_wt1: assert (wt1 <= 3'd3);
    a_wt2: assert (wt2 <= 3'd3);
    a_wt3: assert (wt3 <= 3'd3);
  end
  function [1:0] ahead;
    input [1:0] i;
    ahead = i - last - 2'd1;
  endfunction
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
      h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
      h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
      h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
    end
  end endgenerate
  always @(*) if (!init) begin
    c_g0: cover (grant[0]);
    c_g1: cover (grant[1]);
    c_g2: cover (grant[2]);
    c_g3: cover (grant[3]);
    c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
    c_idle: cover (req == 4'b0000 && grant == 4'b0000);
  end
`endif
endmodule

Case 2: a missing assumption on the skid stage

The scoreboard counts offered and accepted words; offers minus accepts must be one while an offer waits, else zero. That holds only if the source keeps in_valid high until its word is accepted, a rule the environment owes. With a free source it fails at depth 6:

hs_bridge.sv

// formal: bmc 8 expect fail slang top hs_env_check define RULE=0
`define FORMAL
// hs_bridge RTL only: its own checks are removed, so the scoreboard below is the only property.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;
  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;
  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;
  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end
endmodule
// Lesson-local wrapper: a scoreboard that counts offered words by the first cycle of each offer.
// RULE 0: the source is free. 1: the valid/ready rule is assumed. 2: a rule that is too strong.
module hs_env_check #(parameter RULE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(0), .HELPER(0)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg pend, st_q, acc_q, vld_q;
  reg [3:0] offers, accepts;
  always @(posedge clk) begin
    pend  <= !rst && in_valid && !in_ready;
    vld_q <= !rst && in_valid;
    st_q  <= !rst && out_valid && !out_ready;
    acc_q <= !rst && in_valid && in_ready;
    if (rst) begin offers <= 4'd0; accepts <= 4'd0; end
    else begin
      if (in_valid && !pend)     offers  <= offers + 4'd1;
      if (in_valid && in_ready)  accepts <= accepts + 4'd1;
    end
  end
  generate if (RULE == 1) begin : g_rule
    always @(*) if (!init) assume (!pend || in_valid);
  end else if (RULE == 2) begin : g_too_strong
    always @(*) if (!init) assume (!(st_q && vld_q) || in_valid);
  end endgenerate
  always @(*) if (!init) a_offer_balance: assert (offers - accepts == {3'b0, pend});
  always @(*) if (!init) c_legal_drop: cover (st_q && acc_q && !in_valid);
`endif
endmodule

Step	in_valid	in_ready	offers / accepts	Which condition breaks
1 to 2	1	1	0 / 0, 1 / 1	Two words offered and accepted, the second into the skid
3	1	0	2 / 2	Skid full: the offer waits
4	0	0	3 / 2	The source drops valid while its offer waits
5	1	0	3 / 2	`a_offer_balance`: one open offer, none waiting

Diagnosis: legal start, and the spec's valid/ready rule would have excluded the trace: a missing assumption. The rule: in_valid && !in_ready implies in_valid next cycle. Fix: assume it, and assert it on the source. The block proves, and a cover shows a source may still stop right after an accepted word (step 3):

hs_bridge.sv

// formal: prove 4 expect pass slang top hs_env_check define RULE=1
`define FORMAL
// hs_bridge RTL only: its own checks are removed, so the scoreboard below is the only property.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;
  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;
  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;
  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end
endmodule
// Lesson-local wrapper: a scoreboard that counts offered words by the first cycle of each offer.
// RULE 0: the source is free. 1: the valid/ready rule is assumed. 2: a rule that is too strong.
module hs_env_check #(parameter RULE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(0), .HELPER(0)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg pend, st_q, acc_q, vld_q;
  reg [3:0] offers, accepts;
  always @(posedge clk) begin
    pend  <= !rst && in_valid && !in_ready;
    vld_q <= !rst && in_valid;
    st_q  <= !rst && out_valid && !out_ready;
    acc_q <= !rst && in_valid && in_ready;
    if (rst) begin offers <= 4'd0; accepts <= 4'd0; end
    else begin
      if (in_valid && !pend)     offers  <= offers + 4'd1;
      if (in_valid && in_ready)  accepts <= accepts + 4'd1;
    end
  end
  generate if (RULE == 1) begin : g_rule
    always @(*) if (!init) assume (!pend || in_valid);
  end else if (RULE == 2) begin : g_too_strong
    always @(*) if (!init) assume (!(st_q && vld_q) || in_valid);
  end endgenerate
  always @(*) if (!init) a_offer_balance: assert (offers - accepts == {3'b0, pend});
  always @(*) if (!init) c_legal_drop: cover (st_q && acc_q && !in_valid);
`endif
endmodule

hs_bridge.sv

// formal: cover 8 expect reached slang top hs_env_check define RULE=1
`define FORMAL
// hs_bridge RTL only: its own checks are removed, so the scoreboard below is the only property.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;
  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;
  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;
  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end
endmodule
// Lesson-local wrapper: a scoreboard that counts offered words by the first cycle of each offer.
// RULE 0: the source is free. 1: the valid/ready rule is assumed. 2: a rule that is too strong.
module hs_env_check #(parameter RULE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(0), .HELPER(0)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg pend, st_q, acc_q, vld_q;
  reg [3:0] offers, accepts;
  always @(posedge clk) begin
    pend  <= !rst && in_valid && !in_ready;
    vld_q <= !rst && in_valid;
    st_q  <= !rst && out_valid && !out_ready;
    acc_q <= !rst && in_valid && in_ready;
    if (rst) begin offers <= 4'd0; accepts <= 4'd0; end
    else begin
      if (in_valid && !pend)     offers  <= offers + 4'd1;
      if (in_valid && in_ready)  accepts <= accepts + 4'd1;
    end
  end
  generate if (RULE == 1) begin : g_rule
    always @(*) if (!init) assume (!pend || in_valid);
  end else if (RULE == 2) begin : g_too_strong
    always @(*) if (!init) assume (!(st_q && vld_q) || in_valid);
  end endgenerate
  always @(*) if (!init) a_offer_balance: assert (offers - accepts == {3'b0, pend});
  always @(*) if (!init) c_legal_drop: cover (st_q && acc_q && !in_valid);
`endif
endmodule

The mirror failure is a rule that is too strong: valid held while the output is stalled. A word may be accepted into an empty skid and the source stop. The cover is then not reached within 8, here more than a bound: they contradict at the same step.

hs_bridge.sv

// formal: cover 8 expect fail slang top hs_env_check define RULE=2
`define FORMAL
// hs_bridge RTL only: its own checks are removed, so the scoreboard below is the only property.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;
  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;
  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;
  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end
endmodule
// Lesson-local wrapper: a scoreboard that counts offered words by the first cycle of each offer.
// RULE 0: the source is free. 1: the valid/ready rule is assumed. 2: a rule that is too strong.
module hs_env_check #(parameter RULE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(0), .HELPER(0)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg pend, st_q, acc_q, vld_q;
  reg [3:0] offers, accepts;
  always @(posedge clk) begin
    pend  <= !rst && in_valid && !in_ready;
    vld_q <= !rst && in_valid;
    st_q  <= !rst && out_valid && !out_ready;
    acc_q <= !rst && in_valid && in_ready;
    if (rst) begin offers <= 4'd0; accepts <= 4'd0; end
    else begin
      if (in_valid && !pend)     offers  <= offers + 4'd1;
      if (in_valid && in_ready)  accepts <= accepts + 4'd1;
    end
  end
  generate if (RULE == 1) begin : g_rule
    always @(*) if (!init) assume (!pend || in_valid);
  end else if (RULE == 2) begin : g_too_strong
    always @(*) if (!init) assume (!(st_q && vld_q) || in_valid);
  end endgenerate
  always @(*) if (!init) a_offer_balance: assert (offers - accepts == {3'b0, pend});
  always @(*) if (!init) c_legal_drop: cover (st_q && acc_q && !in_valid);
`endif
endmodule

Case 3: an abstraction artefact at a free cut point

This pipeline replaces the stage-2 product with an input, cutval. The latency property fails at step 4: the cut invents values the multiplier never makes.

cut_pipe.sv

// formal: bmc 6 expect fail slang top cut_pipe define CONTRACT=0
`define FORMAL
// Lesson-local: pipe3 with the stage-2 product replaced by the input cutval.
// CONTRACT 0: the cut is free. 1: cutval is assumed equal to the product. 2: a wrong contract (product plus one).
module cut_pipe #(parameter CONTRACT = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  input  wire [7:0] cutval,
  output reg  [7:0] y
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= cutval;
      y  <= p + 8'd1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;
  wire [7:0] prod = s[3:0] * c1;
  generate if (CONTRACT == 1) begin : g_contract
    always @(*) if (!init) assume (cutval == prod);
  end else if (CONTRACT == 2) begin : g_wrong
    always @(*) if (!init) assume (cutval == prod + 8'd1);
  end endgenerate
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
`endif
endmodule

Step	a, b, c	cutval	p	y	Which condition breaks
1	0, 1, 0	0	0	0	None: inputs enter
2 to 3	0, 0, 0	255, 0	0, 255	1, 1	The real product is 1 x 0 = 0; the cut offers 255 and p holds it
4	0, 0, 0	0	0	0	`a_latency3`: y is 255 + 1 = 0 in eight bits, expected 1

Diagnosis: the trace does not replay on the real block: the abstraction is wrong. Fix: assume the contract at the cut, cutval equals the product, and prove it on the real block. The abstraction proves; a wrong contract, product plus one, fails at the same depth:

cut_pipe.sv

// formal: prove 4 expect pass slang top cut_pipe define CONTRACT=1
`define FORMAL
// Lesson-local: pipe3 with the stage-2 product replaced by the input cutval.
// CONTRACT 0: the cut is free. 1: cutval is assumed equal to the product. 2: a wrong contract (product plus one).
module cut_pipe #(parameter CONTRACT = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  input  wire [7:0] cutval,
  output reg  [7:0] y
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= cutval;
      y  <= p + 8'd1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;
  wire [7:0] prod = s[3:0] * c1;
  generate if (CONTRACT == 1) begin : g_contract
    always @(*) if (!init) assume (cutval == prod);
  end else if (CONTRACT == 2) begin : g_wrong
    always @(*) if (!init) assume (cutval == prod + 8'd1);
  end endgenerate
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
`endif
endmodule

cut_pipe.sv

// formal: bmc 6 expect fail slang top cut_pipe define CONTRACT=2
`define FORMAL
// Lesson-local: pipe3 with the stage-2 product replaced by the input cutval.
// CONTRACT 0: the cut is free. 1: cutval is assumed equal to the product. 2: a wrong contract (product plus one).
module cut_pipe #(parameter CONTRACT = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  input  wire [7:0] cutval,
  output reg  [7:0] y
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= cutval;
      y  <= p + 8'd1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;
  wire [7:0] prod = s[3:0] * c1;
  generate if (CONTRACT == 1) begin : g_contract
    always @(*) if (!init) assume (cutval == prod);
  end else if (CONTRACT == 2) begin : g_wrong
    always @(*) if (!init) assume (cutval == prod + 8'd1);
  end endgenerate
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
`endif
endmodule

On the real block, a shadow register prod_q holds the last product and the assertion p == prod_q proves the contract. The wrong contract planted there fails at step 2:

pipe3.sv

// formal: prove 4 expect pass slang top pipe3
`define FORMAL
// pipe3 only, with a shadow register prod_q and the assertion a_contract added. WRONG=1 plants a wrong contract.
module pipe3 #(parameter CHECK = 1, parameter WRONG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end
`ifdef FORMAL
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;
  reg [7:0] prod_q;
  reg       pv;
  always @(posedge clk) begin prod_q <= s[3:0] * c1; pv <= !rst; end
  always @(*) if (!init && pv) a_contract: assert (p == prod_q + WRONG);
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

pipe3.sv

// formal: bmc 6 expect fail slang top pipe3 define WRONG=1
`define FORMAL
// pipe3 only, with a shadow register prod_q and the assertion a_contract added. WRONG=1 plants a wrong contract.
module pipe3 #(parameter CHECK = 1, parameter WRONG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end
`ifdef FORMAL
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;
  reg [7:0] prod_q;
  reg       pv;
  always @(posedge clk) begin prod_q <= s[3:0] * c1; pv <= !rst; end
  always @(*) if (!init && pv) a_contract: assert (p == prod_q + WRONG);
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

Case 4: a counterexample to induction on the decade counter

The claim that the count is never 15 is true but not inductive. At k = 6 the base passes and the step fails: unproven, not guilty. The trace starts at 13, which no reset reaches:

mod10_counter.sv

// formal: prove 6 expect unproven slang top mod10_counter define HELPER=0
`define FORMAL
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

Step	count	en	Reading
0	13	0	Start: unreachable, satisfies the claim
1 to 5	13, 14, 14, 14, 14	1, 0, 0, 0, 1	Counts into 14 and holds: a state can repeat, so no window helps
6	15	-	The claim fails: the step leaked

Fix: strengthen with the range invariant and prove it. The set holds at depth 4:

mod10_counter.sv

// formal: prove 4 expect pass slang top mod10_counter
`define FORMAL
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

What the review looks for

Each case has a failing run, a passing run after the fix and a trace naming the breaking condition; contracts are proven and assumptions come with a legal-traffic cover.

Verify and debug

Rerun every block after an RTL edit: a failing partner that stops failing means its bug has moved. Run the other planted bugs against the properties meant to catch them; one no bug breaks may be too weak, as the one-line claim was in the splitting lesson.

Check yourself The helper invariant fails at step 2 but the requirement only fails at step 5. Which do you fix?

Neither yet: read the helper first, because an invariant failing is not yet a requirement failing. Here both point at the stuck pointer, and one RTL change fixes both.

Navigate

Why it matters

Case 1: a design bug in the arbiter

Case 2: a missing assumption on the skid stage

Case 3: an abstraction artefact at a free cut point

Case 4: a counterexample to induction on the decade counter

What the review looks for

Verify and debug

Related topics

Four Counterexamples Worked

Why it matters

Case 1: a design bug in the arbiter

Case 2: a missing assumption on the skid stage

Case 3: an abstraction artefact at a free cut point

Case 4: a counterexample to induction on the decade counter

What the review looks for

Verify and debug

Related topics

Why it matters

Case 1: a design bug in the arbiter

Case 2: a missing assumption on the skid stage

Case 3: an abstraction artefact at a free cut point

Case 4: a counterexample to induction on the decade counter

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

Case 1: a design bug in the arbiter

Case 2: a missing assumption on the skid stage

Case 3: an abstraction artefact at a free cut point

Case 4: a counterexample to induction on the decade counter

What the review looks for

Verify and debug

Related topics

Up next