Most property bugs are not clever. They are a check on the wrong side of the interface, a flipped polarity, a reset that is never looked at, a trigger that never fires, or a comment that says eventually about a window. Each is invisible in a passing report and each is caught by one line of a checklist. This lesson's one job is that checklist, applied to three flawed properties until the routine is mechanical.
Review every property against the same nine questions. Direction: is it asserted on an output and assumed on an input? Polarity: is it the specification's sense, not its negation? Reset and first cycle: does it check the cycle after reset instead of hiding from it? Cover: does its antecedent cover reach? Cone: does its cone contain the logic it claims? Mutation: does a mutant fail it? One-to-one: is it counted, not implied? Comment: does it say within N cycles or eventually, matching the proof behind it? Width and signedness: is no expression narrower than its operands, and no unsigned comparison hiding a signed bound? A property that passes all nine is reviewed; anything else is a draft.
Each listing below fails at least one checklist question. Name every defect before reading the table:
// bad-example: asserted on an input, wrong side of the interface
// w_input_check: assert($stable(in_data) || !in_valid);
// an input stability rule constrains the environment, so it must be assumed;
// asserted, it fails the first time the environment legally presents a new word// bad-example: wrong reset handling, polarity flipped
// always @(posedge clk) begin
// if (!rst) w_wrong_reset: assert(out != 8'h3C);
// end
// the check is off during reset and nothing checks the first cycle after it, so a wrong
// reset value passes; and it asserts the forbidden value instead of the specified one// bad-example: level antecedent, bare implication, wrong comment
// eventually every request is answered <- the comment promises no bound
// assert property (@(posedge clk) req |-> ##[1:3] ack);
// textbook: an attempt in every cycle req is high, a window of three, a bare implication
// Boolean form of the same rule: !req_d3 || ack_d2 || ack_d1 || ackListing | Defects (checklist questions failed) |
|---|---|
Input stability asserted | Direction: inputs are assumed, never asserted. Fix: assume on the input, assert the matching output hold. |
Reset handling and polarity | Reset and first cycle: reset values need a check on the cycle after the reset edge. Polarity: it asserts the wrong value. Fix: check the specified value on the cycle after reset. |
Level, bare, eventually | Cover and edge: held requests start an attempt per cycle; the edge form is needed. One-to-one: a duplicate answer satisfies the window, a counter is needed. Comment: the rule is a three-cycle window, so the comment must say within 3 cycles, not eventually. Fix: edge antecedent, outstanding counter, within-N comment. |
Width and signedness has no listing of its own; it is the question to ask of every comparison, for instance of the three-bit outstanding counter below, whose bound must fit its width.
The corrected pattern below is a request and response stage with all three fixes applied: the response is asserted on the block's own output, the antecedent is the rising edge, the window is one to two cycles after the edge and says so, an outstanding counter enforces one answer per request, and the value after reset is checked on the cycle after the reset edge. It passes on the good stage:
// formal: bmc 10 expect pass slang top rsp_fixed define BUG=0
`define FORMAL
// rsp_fixed: a request/response stage with the review fixes applied. The response is asserted
// on the block's own output (ack), the antecedent is the rising edge of req, the window is one to
// two cycles after the edge, the outstanding counter enforces one answer per request, and the
// value after reset is checked on the cycle after the reset edge.
// BUG=1: a duplicate answer one cycle after the real one. BUG=2: the answer is one cycle too late.
module rsp_fixed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire req,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2;
reg [2:0] open_n; // requests accepted and not yet answered
wire rose = req && !req_q;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; ack <= 1'b0; open_n <= 3'd0;
end else begin
req_q <= req; rose_d1 <= rose; rose_d2 <= rose_d1;
ack <= (BUG == 2) ? rose_d2 : (rose || (BUG == 1 && rose_d1));
open_n <= open_n + {2'b0, rose} - {2'b0, ack};
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
// within 2 cycles of the rising edge, never "eventually"
a_window: assert (!rose_d2 || $past(ack) || ack);
// one answer per request
a_one: assert (open_n <= 3'd1);
end
// value after reset, checked on the cycle after the reset edge
always @(posedge clk) if (!init && $past(rst)) a_rst_idle: assert (!ack);
endmoduleA fix is only reviewed when a mutant fails it. The first mutant sends a duplicate answer one cycle after the real one: it satisfies the window, so only the counter fails. The second answers one cycle too late: the window fails:
// formal: bmc 10 expect fail slang top rsp_fixed define BUG=1
`define FORMAL
// rsp_fixed: a request/response stage with the review fixes applied. The response is asserted
// on the block's own output (ack), the antecedent is the rising edge of req, the window is one to
// two cycles after the edge, the outstanding counter enforces one answer per request, and the
// value after reset is checked on the cycle after the reset edge.
// BUG=1: a duplicate answer one cycle after the real one. BUG=2: the answer is one cycle too late.
module rsp_fixed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire req,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2;
reg [2:0] open_n; // requests accepted and not yet answered
wire rose = req && !req_q;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; ack <= 1'b0; open_n <= 3'd0;
end else begin
req_q <= req; rose_d1 <= rose; rose_d2 <= rose_d1;
ack <= (BUG == 2) ? rose_d2 : (rose || (BUG == 1 && rose_d1));
open_n <= open_n + {2'b0, rose} - {2'b0, ack};
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
// within 2 cycles of the rising edge, never "eventually"
a_window: assert (!rose_d2 || $past(ack) || ack);
// one answer per request
a_one: assert (open_n <= 3'd1);
end
// value after reset, checked on the cycle after the reset edge
always @(posedge clk) if (!init && $past(rst)) a_rst_idle: assert (!ack);
endmodule// formal: bmc 10 expect fail slang top rsp_fixed define BUG=2
`define FORMAL
// rsp_fixed: a request/response stage with the review fixes applied. The response is asserted
// on the block's own output (ack), the antecedent is the rising edge of req, the window is one to
// two cycles after the edge, the outstanding counter enforces one answer per request, and the
// value after reset is checked on the cycle after the reset edge.
// BUG=1: a duplicate answer one cycle after the real one. BUG=2: the answer is one cycle too late.
module rsp_fixed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire req,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2;
reg [2:0] open_n; // requests accepted and not yet answered
wire rose = req && !req_q;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; ack <= 1'b0; open_n <= 3'd0;
end else begin
req_q <= req; rose_d1 <= rose; rose_d2 <= rose_d1;
ack <= (BUG == 2) ? rose_d2 : (rose || (BUG == 1 && rose_d1));
open_n <= open_n + {2'b0, rose} - {2'b0, ack};
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
// within 2 cycles of the rising edge, never "eventually"
a_window: assert (!rose_d2 || $past(ack) || ack);
// one answer per request
a_one: assert (open_n <= 3'd1);
end
// value after reset, checked on the cycle after the reset edge
always @(posedge clk) if (!init && $past(rst)) a_rst_idle: assert (!ack);
endmoduleStage | Window check | Counter check | Run result |
|---|---|---|---|
Good | Holds | Holds | No counterexample to depth 10 |
Duplicate answer (BUG=1) | Holds: the real answer is inside the window | Fails: one answer too many | Counterexample |
Late answer (BUG=2) | Fails: no answer inside the window | Holds: one outstanding request at most | Counterexample |
The nine questions are answered in writing per property, not from memory: direction, polarity, reset, cover, cone, mutation, one-to-one, comment, width.
Signal widths and signedness are explicit in the property: no expression narrower than its operands, no unsigned comparison of a signed bound.
Every fix is paired with its defect: the corrected block runs beside the listing it replaces, and the mutant that the listing missed fails the fix.
Apply the checklist to your own properties before anyone else does: run the antecedent covers, run the mutants, and read each comment against the header behind it. A within comment over a bounded run and an eventually comment over an unbounded proof are both honest; anything crossed is the next defect. Keep the checklist in the review template so every property carries its nine answers into sign-off.
Not yet: reviewed is not proven. The nine questions say the rule is well formed and well evidenced. The proof still has to run, with its bound justified and its assumptions discharged, before anyone claims anything.