A waveform shows a flag rising in the same cycle as its enable, and the engineer writes the property against that cycle. The proof fails, and nothing is wrong with the design: the monitor samples before the clock edge updates the registers, while the eye reads the waved value after it. This lesson's one job is to end that one-cycle reading error.
A concurrent assertion sees the values present at the clock edge, which are the register outputs computed by the previous cycle. A property that compares a current input with a current register output is therefore comparing two different cycles: the input of now against the state of before. The fix is mechanical: anything the design registered last cycle is named with the sampled-value function of the previous cycle, and a property that looks one cycle back skips the cycle after reset, whose previous cycle is the reset cycle itself.
The sampled-value functions are all comparisons of this sample with the previous one, so each is a history flop and a gate:
Function | Boolean history form | True when |
|---|---|---|
$past(x) | x_d1 | Always: it is the value itself, one cycle old. |
$rose(x) | x && !x_d1 | x is high now and was low last cycle. |
$fell(x) | !x && x_d1 | x is low now and was high last cycle. |
$stable(x) | x == x_d1 | x equals its previous sample. |
$changed(x) | x != x_d1 | x differs from its previous sample. |
In the cycle right after reset the previous sample belongs to the reset cycle, whose inputs were arbitrary, so every row above needs the same guard. The textbook reset disable does not give that guard. A disable condition switches off the evaluation in the cycles where it is true and nothing else: the cycle after reset is evaluated, and its history reaches back into the reset cycle.
The formal model has one clock, and an enable is data: when the enable is low the register holds, so the monitor qualifies its history with the sampled enable and makes no check when it was low. A clock that genuinely stops ticking is a different circuit: an assertion clocked by it goes quiet without ever failing.
A flag takes the value of its input when the enable is high and holds otherwise. The wrong property demands the flag equal the input now; the right one demands it equal the sampled input when the enable was sampled high, and says nothing when the enable was low:
Cycle | Value before edge (what the monitor sees) | Value after edge (what the wave shows) |
|---|---|---|
1 | flag 0, enable 1, in 1 | flag 1 |
2 | flag 1, enable 0, in 0 | flag 1 (holds) |
3 | flag 1, enable 1, in 0 | flag 0 |
Read cycle 2 the wrong way and the flag looks broken: input 0, flag 1. Read it at the edge and it is correct: the enable was low, so there is nothing to compare, and the flag keeps its old value. The pair below runs both readings on the same module; only the parameter selecting the property differs:
// formal: bmc 6 expect fail slang define WHICH=0
`define FORMAL
// sampled_flag: flag takes d when en is high, else holds. WHICH selects the
// property: 0 checks the flag against the input NOW (wrong cycle), 1 checks it
// against the sampled input when the enable was sampled high (right offset).
module sampled_flag #(parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire d,
input wire en,
output reg q
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) begin
if (rst) q <= 1'b0;
else if (en) q <= d;
end
always @(posedge clk) if (!init && !$past(rst)) begin
if (WHICH == 0) w_same_cycle: assert (q == d);
else w_right_offset: assert (!$past(en) || q == $past(d));
end
endmoduleThe same-cycle form fails: the solver drives the input away from the held flag while the enable is low, which is legal behaviour the property wrongly forbids. The history form passes on the same design:
// formal: bmc 6 expect pass slang define WHICH=1
`define FORMAL
// sampled_flag: flag takes d when en is high, else holds. WHICH selects the
// property: 0 checks the flag against the input NOW (wrong cycle), 1 checks it
// against the sampled input when the enable was sampled high (right offset).
module sampled_flag #(parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire d,
input wire en,
output reg q
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) begin
if (rst) q <= 1'b0;
else if (en) q <= d;
end
always @(posedge clk) if (!init && !$past(rst)) begin
if (WHICH == 0) w_same_cycle: assert (q == d);
else w_right_offset: assert (!$past(en) || q == $past(d));
end
endmoduleThe next module clears a flag on reset and otherwise copies its input every cycle. The rule is that in every cycle except the first one after a reset edge, where the flag holds its reset value, the flag equals the input sampled one cycle before. The textbook form of the guarded rule keeps the history inside the antecedent and relies on the disable only for the reset cycles themselves:
// not-run: implication operators are not accepted by this front end
// textbook: assert property (@(posedge clk) disable iff (rst) !$past(rst) |-> q == $past(d));
// disable iff (rst) switches the check off IN the reset cycles; the guard !$past(rst) removes the
// cycle after reset, where $past(d) is the input of the reset cycleThe Boolean concurrent form the open flow accepts has no implication, so the guard becomes a disjunction. Written with the disable alone the rule fails on the good design, because the first cycle after reset compares the reset value with an arbitrary old input. With the guard it passes:
// formal: bmc 6 expect fail slang top rst_mask define WHICH=0
`define FORMAL
// rst_mask: q takes d every cycle and is cleared by reset. The rule under test:
// in every cycle except the first one after a reset edge (where q holds the reset value), q equals
// the d sampled one cycle before.
// WHICH=0 writes it naively (disable iff is the only reset handling); WHICH=1 adds the guard.
module rst_mask #(parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire d,
output reg q
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) begin
if (rst) q <= 1'b0;
else q <= d;
end
generate if (WHICH == 0) begin : g_naive
p_naive: assert property (@(posedge clk) disable iff (rst || init) q == $past(d));
end else begin : g_guarded
p_guarded: assert property (@(posedge clk) disable iff (rst || init) $past(rst) || q == $past(d));
end endgenerate
endmodule// formal: bmc 6 expect pass slang top rst_mask define WHICH=1
`define FORMAL
// rst_mask: q takes d every cycle and is cleared by reset. The rule under test:
// in every cycle except the first one after a reset edge (where q holds the reset value), q equals
// the d sampled one cycle before.
// WHICH=0 writes it naively (disable iff is the only reset handling); WHICH=1 adds the guard.
module rst_mask #(parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire d,
output reg q
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) begin
if (rst) q <= 1'b0;
else q <= d;
end
generate if (WHICH == 0) begin : g_naive
p_naive: assert property (@(posedge clk) disable iff (rst || init) q == $past(d));
end else begin : g_guarded
p_guarded: assert property (@(posedge clk) disable iff (rst || init) $past(rst) || q == $past(d));
end endgenerate
endmoduleBoth runs use the same disable condition; only the guard differs, because the disable never covered the cycle after reset.
Every history reference is guarded past reset: the check skips the cycle after a reset edge, because the previous cycle is the reset cycle with whatever inputs it had. A disable condition alone does not do this.
Enable-qualified registers get enable-qualified history: the property repeats the sampled enable and makes no claim when it was low.
The property comment names the cycle it checks: same cycle, or one cycle after the sampled condition.
When a property fails in its first checked cycle, suspect the offset before the design: delay the antecedent by one cycle. A failure that vanishes was a sampling error; one that stays put across both offsets is a real candidate.
The previous cycle: with the enable sampled high, the flag now equals the input sampled then. The current input belongs to the next edge, so comparing against it fails on every legal hold. With the enable sampled low there is no comparison at all.