Over-Constraining

An assumption removes input sequences from the search. When it removes only impossible ones, the check becomes accurate. When it removes legal ones too, the check becomes blind: bugs that need those inputs are never found, and every assertion still passes. This is called over-constraining, and it is the most dangerous mistake in formal verification, because it produces a clean result. This article shows an over-constrained check that hides a real bug, and the ways to notice it.

9 min read | Intermediate

What You'll Learn

• Explain how an assumption that is too strong hides bugs
• Find an over-constraint with a cover or a check that is meant to fail
• Recognize contradictory assumptions and how the tool reports them
• Explain why a contradiction in a single state goes unreported

Too Strong Means Blind

Each assumption cuts away part of the input space. The goal is to cut exactly the impossible part. An assumption that cuts more leaves a smaller search, and the tool only checks what is left.

The problem is that the result looks the same either way: PASS. A correct check and an over-constrained check cannot be told apart by their assertion results. You need a separate signal, and that signal is reachability: can the situations the specification allows still happen under the assumptions?

The Design: a Tracker With an Off-by-One

This is the transaction tracker from the input protocol assumptions article, with a 3-bit counter and a bug in the limit check:

module txn3 (input clk, input rst, input go, input resp,
             output req, output [2:0] outstanding);
  reg [2:0] cnt;
  assign outstanding = cnt;
  assign req = go && (cnt <= 3'd3);            // bug: should be cnt < 3
  always @(posedge clk)
    if (rst)               cnt <= 3'd0;
    else if (req && !resp) cnt <= cnt + 3'd1;
    else if (!req && resp) cnt <= cnt - 3'd1;
endmodule

With 3 requests in flight, a new go still lets a fourth one out. The rule cnt <= 3 catches it, as long as the tool may raise go while 3 requests are in flight. The specification allows that: the block that drives go does not know the count, and the tracker is supposed to block the request itself.

The Over-Constrained Check

An engineer adds an assumption that seems harmless, "go only when there is room":

m_resp: assume property (@(posedge clk) disable iff (rst) resp |-> cnt != 3'd0);
m_room: assume property (@(posedge clk) disable iff (rst) go |-> cnt < 3'd3);   // too strong
a_max:  assert property (@(posedge clk) disable iff (rst) cnt <= 3'd3);

The run passes. Of course: m_room forbids exactly the situation in which the bug happens. The assumption is not in the specification. It describes what the engineer expected the neighbor to do, not what the neighbor promises.

Noticing It: Reachability

The question to ask is: "can go arrive while 3 requests are in flight?". The specification says yes. In SVA it is a cover:

c_go_full: cover property (@(posedge clk) disable iff (rst) go && cnt == 3'd3);

In cover mode, SymbiYosys reports it unreachable under the assumptions:

SBY [run] engine_0: ##   0:00:00  Checking cover reachability in step 9..
SBY [run] engine_0: ##   0:00:00  Unreached cover statement at txn3: design.sv:23.36-23.61
SBY [run] summary: unreached cover statements:
SBY [run] DONE (FAIL, rc=2)

A cover that the specification allows but the check cannot reach is the signature of over-constraining. Remove m_room and the run fails at step 6:

Three requests go out in steps 1 to 3. In step 4, go is high with 3 in flight, the faulty test lets a fourth request out, and the count is 4 in step 5. Change the test to cnt < 3'd3 and the run passes without the extra assumption.

Contradictory Assumptions

The extreme case is a set of assumptions that can never be met together, for example assume (go) and assume (!go) from two different engineers. Then no input sequence is legal, and every assertion holds trivially. SymbiYosys detects this when it happens from the start and stops with an error:

SBY [run] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY [run] engine_0: ##   0:00:00  Assumptions are unsatisfiable!
SBY [run] DONE (ERROR, rc=16)

The lab reports this run as ERROR. A contradiction that only happens in some states is not reported at all. Suppose an assumption can never be met when the count is 2. Every trace that reaches count 2 is then cut off, silently, and the tool never looks beyond it. On the buggy tracker, such an assumption makes the check pass with no warning, because the bug needs the count to pass through 2. Only covers for the states after it reveal the problem.

Running It in ChipVerify Lab

The lab panel runs assertions, not covers, but you can ask a reachability question with a check that is meant to fail: assert the negation of the situation. If the assertion fails, the situation is reachable, and the counterexample is a trace that reaches it.

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the memory only responds to a request that is in flight
  always @(*) if (!init) assume (!resp || cnt != 3'd0);
  // OVER-CONSTRAINED: "go only when there is room"
  always @(*) if (!init) assume (!go || cnt < 3'd3);
  // never more than 3 in flight
  always @(posedge clk) if (!init) assert (cnt <= 3'd3);
  // reachability, meant to fail: go while 3 are in flight
  always @(posedge clk) if (!init) assert (!(go && cnt == 3'd3));
`endif

With m_room, everything passes, including the check that was meant to fail. That pass is the warning. Remove m_room and the run fails at step 5 on the reachability check, which shows that the situation is now in the search. Comment out the reachability check and the real assertion fails at step 6.

Common Mistakes