Why it matters

The reassuring proof is one line: assert that no signal is unknown, watch it pass, ship. It proves nothing, because in a two-state model there is no unknown for the check to find: the predicate is constant false, so its negation is constant true, and it is just as true of a design with an unreset register as of one without. The unreset register that motivated the check is still unreset. This lesson shows what the flow here does with that assertion, then asks the questions the tool can answer.

The core idea

A two-state formal model has no X or Z. An unreset register holds an arbitrary but fixed zero or one, chosen by the solver to try to break the proof. A missing reset therefore shows up as a counterexample from an arbitrary value, never as an unknown. Asserting the absence of X in that model is asserting a property of the modelling, not of the design. The table below is the whole boundary in one place:

Worked example: the assertion that cannot discriminate

The textbook assertion is below. It is a concept block, not a run, because this flow cannot run it usefully. The native front end does not treat the unknown test as constant false: it treats it as a free value, so the assertion is refuted at step 1 on a correctly reset register and on an unreset one alike (this was run on both). The other front end rejects the unknown test outright. Either way the assertion cannot tell the two designs apart, which is the practical form of 'proves nothing'. In a strict two-state semantics it would be constant true, and cannot tell them apart either:

// not-run: the unknown-absence assertion cannot be run usefully in this flow (refuted on every design, or rejected)
// x_no_unknown: assert (!$isunknown(status));   // two-state: constant true; this flow: refuted on a reset register too

What the flow can answer are two honest questions about the same register, each as a runnable check. The module below holds the register twice, a copy A and a copy B driven by the same inputs, with free and different initial values. The question 'is the register zero after reset' is r_after_reset; the question 'does the reset make the two copies agree, whatever they held before' is d_copies. With a reset clause on both, both pass:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

// formal: prove 4 expect pass slang top xdemo
module xdemo #(parameter RESET = 1) (
  input  wire clk,
  input  wire rst,
  input  wire set,
  output reg  status,
  output reg  status_b
);
  // copy A and copy B of the same register, driven by the same inputs
  always @(posedge clk) begin
    if (RESET != 0 && rst) begin status <= 1'b0; status_b <= 1'b0; end
    else if (set)          begin status <= 1'b1; status_b <= 1'b1; end
  end

  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init && $past(rst)) begin
    r_after_reset: assert (status == 1'b0);       // the reset value
    d_copies:      assert (status == status_b);   // the copies agree: reset determinism
  end
endmodule

Remove the reset clause and the same two questions fail. This is the unreset register the unknown check was meant to catch, and it is caught as a counterexample from an arbitrary value: copy A starts at 1 and copy B at 0, nothing resets them, and the checks that judge the cycle after reset fail. The register is reported at step 2, one step after the state it judges, which follows the reporting rule of the course:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

// formal: bmc 6 expect fail slang top xdemo define RESET=0
module xdemo #(parameter RESET = 1) (
  input  wire clk,
  input  wire rst,
  input  wire set,
  output reg  status,
  output reg  status_b
);
  // copy A and copy B of the same register, driven by the same inputs
  always @(posedge clk) begin
    if (RESET != 0 && rst) begin status <= 1'b0; status_b <= 1'b0; end
    else if (set)          begin status <= 1'b1; status_b <= 1'b1; end
  end

  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init && $past(rst)) begin
    r_after_reset: assert (status == 1'b0);       // the reset value
    d_copies:      assert (status == status_b);   // the copies agree: reset determinism
  end
endmodule

Root cause: a missing reset clause, found by the right question. Fix the RTL by adding the reset clause; the proof above is the same module with the clause in place.

What the review looks for

• No unknown-absence assertion anywhere in the proof set: the review rejects it as modelling theatre.

• Every control register has a reset-determinism or reset-value argument tracing to a proof in this topic or the register topic.

• Unreset storage is listed explicitly with its justification: memory arrays, data paths, and what reads them first.

Verify and debug

Suspect every proof that passes suspiciously fast on a new design: mutate the reset logic to confirm the proof can fail, as the second run above does. A determinism failure names the register whose copies differ; add the reset clause, do not constrain the initial value, unless the initial value is itself specified and reviewed.

Related topics

• Next: Reset Determinism Proofs

• RTL: X-Propagation Discipline