Over-Constraint Seen Through Covers

On this page

Part 7 of 10, lesson 2 of 15Formal Coverage and SignoffAll levels

Why it matters

The most flattering formal result is also the emptiest: every assertion proves in seconds, nothing ever fails, and the dashboard is uniformly positive. The usual cause is not a perfect design but an environment model that excludes nearly all behaviour: two assumptions that contradict each other, a reset held for ever, or one assumed-impossible state that the design needs in order to do anything. Ordinary activity covers expose all three in one run, because a strangled environment cannot produce ordinary traffic.

The core idea

Assumptions prune traces: each one removes the behaviours it forbids. That is their job, and also the danger. When the pruned set includes the scenarios the properties claim to check, the assertions prove over an empty or threadbare trace set and the covers of basic activity go silent. The rule: covers of ordinary activity are required, and an unreachable required cover is a sign-off failure with an owner. The assumption list is reviewed line by line; an assumption nothing needs is deleted, and one everything needs is reviewed twice.

Worked example: one counter, four harnesses

A three-bit counter has one check, a step property (after a clean cycle the value goes up by one), and one required cover, the value 5. The parameter BUG selects the harness. The healthy harness comes first: the check passes and the cover is reached at step 6, inside depth 8.

oc_demo.sv

// formal: bmc 8 expect pass top oc_demo
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

oc_demo.sv

// formal: cover 8 expect reached top oc_demo
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

Variant 1 adds two assumptions that together forbid every instant: the value 5 is required and forbidden at once. No trace of useful length satisfies them, so the assertion passes and the cover is not reached within 8: inconclusive in general, here explained by the contradictory assumptions.

oc_demo.sv

// formal: bmc 8 expect pass top oc_demo define BUG=1
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

oc_demo.sv

// formal: cover 8 expect fail top oc_demo define BUG=1
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

Variant 2 assumes the reset input high at every step: the reset is never released, the counter sits at zero, and the step check is never evaluated because its guard needs a clean previous cycle. The cover is again not reached within 8, inconclusive in general and here explained by the assumption.

oc_demo.sv

// formal: bmc 8 expect pass top oc_demo define BUG=2
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

oc_demo.sv

// formal: cover 8 expect fail top oc_demo define BUG=2
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

Variant 3 assumes the state 5 never occurs, the commonest real shape: someone excluded a state to make a proof converge, and the cover that needs it went silent. The check passes at depth 8 only because no trace is long enough to reach step 6 without visiting the forbidden state. The cover is not reached within 8: inconclusive in general, here explained by the assumption that forbids the state.

oc_demo.sv

// formal: bmc 8 expect pass top oc_demo define BUG=3
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

oc_demo.sv

// formal: cover 8 expect fail top oc_demo define BUG=3
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

Variant	Assumption that caused it	How the assumption list reveals it
1: contradictory pair	The trigger condition is assumed true and assumed false.	Two entries name the same signal with opposite polarity.
2: reset held for ever	The reset input is assumed high at every step.	The reset appears in the list as always asserted, with no release rule.
3: assumed-impossible state	The state the cover needs is assumed never to occur.	An assumption names the same condition as a required cover: the first suspect.

Silence alone is not the whole story, so show that the passes are empty: inject a real fault into the counter (it skips from 2 to 4). The healthy harness catches it; the contradictory harness lets it through, and every assertion still passes.

oc_demo.sv

// formal: bmc 8 expect fail top oc_demo define MUT=1
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

oc_demo.sv

// formal: bmc 8 expect pass top oc_demo define BUG=1 define MUT=1
module oc_demo #(parameter BUG = 0, parameter MUT = 0) (input wire clk, input wire rst);
  reg [2:0] n;
  always @(posedge clk) begin
    if (rst) n <= 3'd0;
    else n <= (MUT == 1 && n == 3'd2) ? 3'd4 : n + 3'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  wire trig = (n == 3'd5);
  // the check: after a clean cycle the counter moves up by one
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (n == $past(n) + 3'd1);
  end
  always @(*) if (!init) begin
    if (BUG == 1) begin assume (trig); assume (!trig); end  // required and forbidden at once
    if (BUG == 2) assume (rst);                              // reset never released
    if (BUG == 3) assume (!trig);                            // the needed state is excluded
  end
  always @(*) if (!init) begin
    c_live: cover (trig);
  end
`endif
endmodule

The repair in all three cases is the same: delete the assumption, or replace it by an assertion on the neighbour that justifies it, and rerun until the activity cover is reached again. The owner rule stays: a required cover that stays silent blocks sign-off until someone owns the assumption under suspicion.

What the reviewer looks for

Covers of ordinary activity exist for every interface: traffic flows, stalls happen, resets release.
The assumption list is short, each entry names the rule it models, and each is discharged elsewhere or flagged.
A silent required cover blocks sign-off; the entry names an owner and the assumption under suspicion.

Verify and debug

Suspect over-constraint when everything passes suspiciously fast or a cover you consider trivial stays silent. Bisect the assumption list: disable half, rerun the covers, and repeat until the silent cover speaks. The assumption whose removal restores activity is wrong or stronger than its documented rule. Also check reset polarity and gating: a reset held for ever and an enable never driven look the same as a contradiction from the cover's point of view.

Check yourself Half the assumption list is disabled and a silent cover becomes reachable. What do you conclude?

The disabled half contains an over-strong or wrong assumption. Re-enable one at a time until the cover goes silent again; that assumption needs a documented justification or removal.

Navigate

Why it matters

The core idea

Worked example: one counter, four harnesses

What the reviewer looks for

Verify and debug

Related topics

Over-Constraint Seen Through Covers

Why it matters

The core idea

Worked example: one counter, four harnesses

What the reviewer looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: one counter, four harnesses

What the reviewer looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: one counter, four harnesses

What the reviewer looks for

Verify and debug

Related topics

Up next