A status bit is set by hardware in the exact cycle software clears it. One of them must win, and the choice is a specification decision with silicon consequences: if the clear wins, a real event is lost silently; if the set wins, software must clear again. The symptom of getting it wrong is an interrupt that occasionally never arrives, found months later under load. This lesson pins the common priority, hardware set wins, and proves it with the collision covered.
Write the priority as logic, then as a property, then cover the collision so the priority proof is not vacuous. The next state is the cleared value with the hardware sets forced back on: the set wins by construction, and the properties check the set-wins case, the clear-alone case, and the keep case for a written 0. The collision cover demands a cycle where both arrive together; without it the priority property could pass on a design where the collision never happens. The register block already has the race: its status register is set by two hardware pulses and cleared by software, and the proof of the previous lessons includes a_hw_set.
Cycle (simulation trace) | Inputs on | STATUS before | STATUS after | Meaning |
|---|---|---|---|---|
10 | write 0x02 to STATUS, set_done = 1 | ERR set (0x02) | DONE set (0x01) | ERR cleared and DONE set in the same cycle: both effects land |
12 | write 0x01 to STATUS, set_done = 1 | DONE set (0x01) | DONE still set (0x01) | the clear of DONE meets the hardware set of DONE: the set wins |
The rows are the register block's own simulated behaviour. The lesson-local module below is a minimal two-bit status register with the same priority, small enough to mutate both ways:
The proof checks three things for both bits: a hardware set always leaves the bit set (the priority), a software clear with no set in that cycle clears, and a software write of 0 keeps a set bit. Two covers show the collision is reachable on each bit:
// formal: prove 4 expect pass slang top race_status
`define FORMAL
module race_status #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire w_status,
input wire [1:0] wdata,
input wire [1:0] hw_set,
output reg [1:0] status
);
// BUG 2: any write to the register clears everything, including bits written as 0
wire [1:0] cleared = (BUG == 2) ? 2'b00 : (status & ~wdata);
wire [1:0] simultaneous = hw_set & wdata & {2{w_status}};
always @(posedge clk) begin
if (rst) status <= 2'b00;
// correct: the hardware set wins. BUG 1 lets the clear win by subtracting
// a simultaneous set back off, which loses the event.
else status <= ((w_status ? cleared : status) | hw_set) & ~((BUG == 1) ? simultaneous : 2'b00);
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
// priority: a hardware set always leaves the bit set (both bits)
r_hw_sets: assert ((($past(hw_set)) & ~status) == 2'b00);
// a software clear with no hardware set that cycle clears
r_clear_alone: assert (((($past(wdata) & ~$past(hw_set)) & {2{$past(w_status)}}) & status) == 2'b00);
// a software write of 0 keeps a set bit
r_zero_keeps: assert (((($past(status) & ~$past(wdata)) & {2{$past(w_status)}}) & ~status) == 2'b00);
end
always @(*) if (!init) begin
c_collision_0: cover (w_status && wdata[0] && hw_set[0]);
c_collision_1: cover (w_status && wdata[1] && hw_set[1]);
end
`endif
endmodule// formal: cover 6 expect reached slang top race_status
`define FORMAL
module race_status #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire w_status,
input wire [1:0] wdata,
input wire [1:0] hw_set,
output reg [1:0] status
);
// BUG 2: any write to the register clears everything, including bits written as 0
wire [1:0] cleared = (BUG == 2) ? 2'b00 : (status & ~wdata);
wire [1:0] simultaneous = hw_set & wdata & {2{w_status}};
always @(posedge clk) begin
if (rst) status <= 2'b00;
// correct: the hardware set wins. BUG 1 lets the clear win by subtracting
// a simultaneous set back off, which loses the event.
else status <= ((w_status ? cleared : status) | hw_set) & ~((BUG == 1) ? simultaneous : 2'b00);
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
// priority: a hardware set always leaves the bit set (both bits)
r_hw_sets: assert ((($past(hw_set)) & ~status) == 2'b00);
// a software clear with no hardware set that cycle clears
r_clear_alone: assert (((($past(wdata) & ~$past(hw_set)) & {2{$past(w_status)}}) & status) == 2'b00);
// a software write of 0 keeps a set bit
r_zero_keeps: assert (((($past(status) & ~$past(wdata)) & {2{$past(w_status)}}) & ~status) == 2'b00);
end
always @(*) if (!init) begin
c_collision_0: cover (w_status && wdata[0] && hw_set[0]);
c_collision_1: cover (w_status && wdata[1] && hw_set[1]);
end
`endif
endmoduleBoth collision covers are reached at step 1, each as its own run: the priority proof is only meaningful because the collision can happen.
The first partner lets the clear win: it subtracts a simultaneous set back off, so a hardware event arriving with the clear is lost. The property that fails is the priority check, at the first collision. Read the trace by the collision cycle:
Step | w_status | wdata | hw_set | status | Outcome |
|---|---|---|---|---|---|
1 | 1 | 0x2 | 0x3 | 0x0 | collision on bit 1: hardware sets both bits, software clears bit 1 |
2 | - | - | - | 0x1 | bit 1 was lost: the set bits should read 0x3 |
3 | - | - | - | - |
|
// formal: bmc 6 expect fail slang top race_status define BUG=1
`define FORMAL
module race_status #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire w_status,
input wire [1:0] wdata,
input wire [1:0] hw_set,
output reg [1:0] status
);
// BUG 2: any write to the register clears everything, including bits written as 0
wire [1:0] cleared = (BUG == 2) ? 2'b00 : (status & ~wdata);
wire [1:0] simultaneous = hw_set & wdata & {2{w_status}};
always @(posedge clk) begin
if (rst) status <= 2'b00;
// correct: the hardware set wins. BUG 1 lets the clear win by subtracting
// a simultaneous set back off, which loses the event.
else status <= ((w_status ? cleared : status) | hw_set) & ~((BUG == 1) ? simultaneous : 2'b00);
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
// priority: a hardware set always leaves the bit set (both bits)
r_hw_sets: assert ((($past(hw_set)) & ~status) == 2'b00);
// a software clear with no hardware set that cycle clears
r_clear_alone: assert (((($past(wdata) & ~$past(hw_set)) & {2{$past(w_status)}}) & status) == 2'b00);
// a software write of 0 keeps a set bit
r_zero_keeps: assert (((($past(status) & ~$past(wdata)) & {2{$past(w_status)}}) & ~status) == 2'b00);
end
always @(*) if (!init) begin
c_collision_0: cover (w_status && wdata[0] && hw_set[0]);
c_collision_1: cover (w_status && wdata[1] && hw_set[1]);
end
`endif
endmoduleHow to read it: step 0 is the reset step, so the status registers read unknown until the reset edge. At step 1 w_status is high with wdata 0x2 and hw_set is 0x3. At step 2 status_ok reads 0x3, the set having won, and status_bug reads 0x1, bit 1 lost; lost_bug is high at step 2 and lost_ok never rises. The proof run reports the failing check one step after the state, at step 3.
Root cause: the clear path removes the set it should preserve; fix the RTL priority and keep the cover. The second partner is the W1C polarity slip that the register proofs guard with the written-0 check: any write to the register clears everything, including bits written as 0. Only r_zero_keeps fails, because the written-1 clear still works:
// formal: bmc 6 expect fail slang top race_status define BUG=2
`define FORMAL
module race_status #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire w_status,
input wire [1:0] wdata,
input wire [1:0] hw_set,
output reg [1:0] status
);
// BUG 2: any write to the register clears everything, including bits written as 0
wire [1:0] cleared = (BUG == 2) ? 2'b00 : (status & ~wdata);
wire [1:0] simultaneous = hw_set & wdata & {2{w_status}};
always @(posedge clk) begin
if (rst) status <= 2'b00;
// correct: the hardware set wins. BUG 1 lets the clear win by subtracting
// a simultaneous set back off, which loses the event.
else status <= ((w_status ? cleared : status) | hw_set) & ~((BUG == 1) ? simultaneous : 2'b00);
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
// priority: a hardware set always leaves the bit set (both bits)
r_hw_sets: assert ((($past(hw_set)) & ~status) == 2'b00);
// a software clear with no hardware set that cycle clears
r_clear_alone: assert (((($past(wdata) & ~$past(hw_set)) & {2{$past(w_status)}}) & status) == 2'b00);
// a software write of 0 keeps a set bit
r_zero_keeps: assert (((($past(status) & ~$past(wdata)) & {2{$past(w_status)}}) & ~status) == 2'b00);
end
always @(*) if (!init) begin
c_collision_0: cover (w_status && wdata[0] && hw_set[0]);
c_collision_1: cover (w_status && wdata[1] && hw_set[1]);
end
`endif
endmoduleStep | w_status | wdata | hw_set | status | Outcome |
|---|---|---|---|---|---|
1 | 0 | 0x0 | 0x1 | 0x0 | hardware sets bit 0 |
2 | 1 | 0x0 | 0x0 | 0x1 | software writes 0x0 to the register |
3 | - | - | - | 0x0 | bit 0 was cleared by a write of 0: it should stay 0x1 |
4 | - | - | - | - |
|
How to read it: step 0 is the reset step. At step 1 hw_set is 1; at step 2 both registers read 1 and w_status is high with wdata 0. At step 3 status_ok still reads 1 while status_bug has dropped to 0, and wrongly_bug is high; wrongly_ok never rises. The replay shows the variant at step 3; the proof run reports it one step later.
The priority is stated in one sentence in the specification and matches the RTL expression exactly.
The collision has a cover for every bit, and the cover is reached by its own run: set-wins proved without a collision is vacuous.
Software consequences are documented: with set-wins, a clear-then-read may still show set.
Read a race failure at the collision cycle: which arrived, which won, what the priority says. If the trace has no collision, the cover is the failure. The hardware priority must be total over all same-cycle combinations; never resolve a race by ordering software around it.
Not necessarily: the hardware may have set the bit again, or in the same cycle as the clear. The driver clears until it reads clear, and the proof guarantees a clear with no concurrent set takes effect.