A register came out of reset with the wrong value and no property noticed. The property that should have caught it switched itself off while reset was active, and it only ever evaluated in cycles where its reset-time condition was already true. Reset-caused bugs show up in what the outputs hold when reset releases. This lesson separates the two and states how the open flow models a reset that arrives between clocks.
Job of this lesson: use disable guards without masking reset-time bugs, get the polarity right, and state the asynchronous-reset caveat.
A disable iff (rst) guard switches a property off while reset is high. It masks a bug only when the property's evaluation lies inside reset, for example a check whose trigger is reset itself. The reset-value check belongs on the first cycle after reset, which a past-of-reset term selects. A polarity mistake disables the property when it should run, so a cover proves the property is evaluated.
The caveat, as measured: the open flow turns an asynchronous reset into a level that takes effect in the same step, so the immediate check “reset implies q is 0” passes for an asynchronous register and fails for a synchronous one. Timing between clock edges (glitches, recovery and removal) is not modelled; the signoff names the separate check that covers it.
The design is a block of four registers: control, write-1-to-clear status, a read-only identifier and a data register that resets to 0x3C. The good design proves, with reset values checked on the first cycle after a reset edge. The planted bug resets the data register to 0 instead: the wrong value exists at step 1 and the check reports it at step 2.
// formal: prove 4 expect pass slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block define BUG=3
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- state-based safety: always true after the reset cycle ----
always @(*) if (!init) begin
a_id_const: assert (addr != 2'd2 || rdata == 8'hA5); // ID reads 0xA5
a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0); // unimplemented bits read 0
end
// ---- transition properties: they look one cycle back, so skip the cycle after reset ----
always @(posedge clk) if (!init) begin
// reset values, visible on the first cycle after a reset edge
if ($past(rst)) begin
a_rst_ctrl: assert (ctrl == 8'h00);
a_rst_status: assert (status == 2'b00);
a_rst_data: assert (data == 8'h3C);
end
if (!$past(rst)) begin
// read-write registers read back what was written
a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
// write-1-to-clear: a 1 written to a bit clears it unless hardware sets it that cycle
a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
a_w1c_err: assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err)) || !status[1]);
// write-1-to-clear: writing 0 leaves the bit alone (it stays set)
a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
// hardware set always wins
a_hw_set: assert (!$past(set_done) || status[0]);
// other registers do not change on a write to a different address
a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
a_isolate_data: assert ($past(w_data) || data == $past(data));
end
end
// covers: the interesting events can happen
always @(*) if (!init) begin
c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
c_both_bits: cover (status == 2'b11);
c_id_write: cover (w_id);
end
`endif
endmoduleStep | rst | data | Note |
|---|---|---|---|
0 | 1 | arbitrary | Power-up; reset asserted. |
1 | 0 | 00 | The wrong value exists here, right after the reset edge. |
2 | 0 | 00 | The first-enabled-cycle check reports it here. |
Now the guard. A concurrent property under disable iff (rst || init) with the condition !rst || data == 8'h3C is evaluated only when rst is low, where its first term is true: it passes on the buggy design. Replacing !rst by !$past(rst) makes it evaluate on the first enabled cycle: it fails on the buggy design and proves on the good one.
// formal: bmc 6 expect pass slang top csr_block define BUG=3
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// masked: evaluated only while rst is low, where !rst is already true
a_reset_masked: assert property (@(posedge clk) disable iff (rst || init) !rst || data == 8'h3C);
`endif
endmodule// formal: bmc 3 expect fail slang top csr_block define BUG=3
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// first enabled cycle: the previous cycle was reset, so data must hold its reset value
a_reset_value: assert property (@(posedge clk) disable iff (rst || init) !$past(rst) || data == 8'h3C);
`endif
endmodule// formal: prove 4 expect pass slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
a_reset_value: assert property (@(posedge clk) disable iff (rst || init) !$past(rst) || data == 8'h3C);
`endif
endmoduleThe polarity check is a cover that the guarded check is ever evaluated. With the right sense it is reached; with the sense inverted (disable iff (!rst)) the cover cannot be reached. Not reached within 6 is inconclusive alone; next to the reached run it shows the guard was backwards.
// formal: cover 3 expect reached slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
cover property (@(posedge clk) disable iff (rst || init) $past(rst));
`endif
endmodule// formal: cover 6 expect fail slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a simple synchronous write/read port.
// addr 0 CTRL read/write, reset 0x00
// addr 1 STATUS bit0 DONE, bit1 ERR: write-1-to-clear, set by hardware pulses
// set_done / set_err (a set wins over a clear in the same cycle);
// bits 7:2 read 0, reset 0x00
// addr 2 ID read-only, constant 0xA5 (writes ignored)
// addr 3 DATA read/write, reset 0x3C
// Write: wr_en with addr and wdata, takes effect at the clock edge. Read is combinational
// on addr (rdata = selected register, current value). Synchronous active-high reset.
// BUG: 0 none, 1 W1C writes 1 (writing 1 sets the bit instead of clearing it),
// 2 ID is writable, 3 DATA reset value wrong (0x00 instead of 0x3C).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire wr_en,
input wire [1:0] addr,
input wire [7:0] wdata,
input wire set_done,
input wire set_err,
output wire [7:0] rdata
);
reg [7:0] ctrl, data, id_r;
reg [1:0] status; // [0] DONE, [1] ERR
wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
assign rdata = (addr == 2'd0) ? ctrl :
(addr == 2'd1) ? {6'b0, status} :
(addr == 2'd2) ? id_val : data;
wire w_ctrl = wr_en && addr == 2'd0;
wire w_status = wr_en && addr == 2'd1;
wire w_id = wr_en && addr == 2'd2;
wire w_data = wr_en && addr == 2'd3;
wire [1:0] hw_set = {set_err, set_done};
wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) // writing 1 sets
: (status & ~wdata[1:0]); // writing 1 clears
always @(posedge clk) begin
if (rst) begin
ctrl <= 8'h00;
status <= 2'b00;
data <= (BUG == 3) ? 8'h00 : 8'h3C;
id_r <= 8'hA5;
end else begin
if (w_ctrl) ctrl <= wdata;
if (w_data) data <= wdata;
if (w_id && BUG == 2) id_r <= wdata;
status <= (w_status ? after_w : status) | hw_set;
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// inverted sense: disabled whenever rst is low
cover property (@(posedge clk) disable iff (!rst) $past(rst) && !rst);
`endif
endmoduleFinally the asynchronous caveat on one register with the reset style as a parameter:
// formal: bmc 4 expect pass slang top reg_demo define ASYNC=1
`define FORMAL
module reg_demo #(parameter ASYNC = 0) (
input wire clk,
input wire rst,
input wire [3:0] a,
output reg [3:0] q
);
generate if (ASYNC) begin : g_async
always @(posedge clk or posedge rst) if (rst) q <= 4'd0; else q <= a;
end else begin : g_sync
always @(posedge clk) if (rst) q <= 4'd0; else q <= a;
end endgenerate
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// judged in the step where rst is high, before the clock edge
always @(*) if (!init && rst) a_in_reset: assert (q == 4'd0);
`endif
endmodule// formal: bmc 4 expect fail slang top reg_demo define ASYNC=0
`define FORMAL
module reg_demo #(parameter ASYNC = 0) (
input wire clk,
input wire rst,
input wire [3:0] a,
output reg [3:0] q
);
generate if (ASYNC) begin : g_async
always @(posedge clk or posedge rst) if (rst) q <= 4'd0; else q <= a;
end else begin : g_sync
always @(posedge clk) if (rst) q <= 4'd0; else q <= a;
end endgenerate
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// judged in the step where rst is high, before the clock edge
always @(*) if (!init && rst) a_in_reset: assert (q == 4'd0);
`endif
endmoduleReset values are checked on the first enabled cycle; a disable guard is never the only check.
One reset name and sense across checkers, a cover that each guarded property is evaluated, and the async caveat recorded.
Mutate each reset value and confirm the first-enabled-cycle check fires at the stated step. Flip a guard on purpose and confirm the evaluation cover goes unreachable; if it does not, the cover proves nothing. For asynchronous resets, record the separate check that covers timing.
It is evaluated on the first cycle after reset, so a wrong reset value fails at step 2; a property that is evaluated only while reset is low is true there by construction.
That clock-edge timing (glitches, recovery and removal) is outside the model, and which separate check covers it.