W1C, Read-Only and Reset-Value Proofs

On this page

Part 5 of 10, lesson 5 of 20Formal ApplicationsAll levels

Why it matters

Write-1-to-clear is the most mis-proved register behaviour. The check must relate the written data to the status in the same cycle the write is presented: sample the data a cycle late and the property compares the clear against whatever the bus holds now, passing on some traffic and failing on other. The symptom is a proof that flickers with the stimulus, which engineers then quieten by weakening the property until it proves and catches nothing.

The core idea

Sample in the antecedent cycle. Every property here reads the previous cycle's write signals and data together with the current state: a write of 1 to a status bit with no hardware set in that same write cycle leaves the bit clear now; a write of 0 leaves a set bit set; a read-only register reads its constant whatever was written; reset values are checked on the cycle after a reset cycle. The history must be skipped for the cycle right after reset, because the previous cycle is the reset cycle with whatever inputs it had.

Worked example: three families, each with its bug

The proof below is the register module with the full set. Each family is killed by a planted variant: writing 1 sets the bit instead of clearing it (the clear family), the ID register accepting writes (the read-only family), and DATA resetting to zero (the reset family, shown in the previous lesson as well). Each variant is read from the table of results below the blocks:

csr_block.sv

// formal: prove 4 expect pass slang top csr_block
`define FORMAL
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;

  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])
                                  : (status & ~wdata[1:0]);

  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);

  always @(*) if (!init) begin
    a_id_const:  assert (addr != 2'd2 || rdata == 8'hA5);
    a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
  end

  always @(posedge clk) if (!init) begin
    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
      a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
      a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
      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]);
      a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
      a_hw_set:   assert (!$past(set_done) || status[0]);
      a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
      a_isolate_data: assert ($past(w_data) || data == $past(data));
    end
  end

  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

csr_block.sv

// formal: bmc 4 expect fail slang top csr_block define BUG=1
`define FORMAL
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;

  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])
                                  : (status & ~wdata[1:0]);

  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);

  always @(*) if (!init) begin
    a_id_const:  assert (addr != 2'd2 || rdata == 8'hA5);
    a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
  end

  always @(posedge clk) if (!init) begin
    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
      a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
      a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
      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]);
      a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
      a_hw_set:   assert (!$past(set_done) || status[0]);
      a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
      a_isolate_data: assert ($past(w_data) || data == $past(data));
    end
  end

  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

csr_block.sv

// formal: bmc 3 expect fail slang top csr_block define BUG=2
`define FORMAL
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;

  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])
                                  : (status & ~wdata[1:0]);

  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);

  always @(*) if (!init) begin
    a_id_const:  assert (addr != 2'd2 || rdata == 8'hA5);
    a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
  end

  always @(posedge clk) if (!init) begin
    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
      a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
      a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
      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]);
      a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
      a_hw_set:   assert (!$past(set_done) || status[0]);
      a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
      a_isolate_data: assert ($past(w_data) || data == $past(data));
    end
  end

  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

csr_block.sv

// formal: bmc 3 expect fail slang top csr_block define BUG=3
`define FORMAL
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;

  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])
                                  : (status & ~wdata[1:0]);

  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);

  always @(*) if (!init) begin
    a_id_const:  assert (addr != 2'd2 || rdata == 8'hA5);
    a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
  end

  always @(posedge clk) if (!init) begin
    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
      a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
      a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
      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]);
      a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
      a_hw_set:   assert (!$past(set_done) || status[0]);
      a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
      a_isolate_data: assert ($past(w_data) || data == $past(data));
    end
  end

  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

Family	Variant	Property that fails	Step reported	Trace
write-1-to-clear	writing 1 sets the bit	`a_w1c_err` (and `a_w1c_done`)	3	step 1: write 0x02 to STATUS, no hardware set; step 2: ERR reads 1; reported at step 3
read-only	ID accepts writes	`a_id_const`	2	step 1: write to offset 2; step 2: a read of offset 2 returns the written value
reset value	DATA resets to 0x00	`a_rst_data`	2	step 1 holds 0x00 after the reset edge; reported at step 2

All three traces are two or three steps long: reset, stimulate, observe. The step numbers are the ones the runs reported. The written-0 half of the W1C family, a register that clears a bit that software wrote as 0, is guarded by a_w1c_zero; the register block has no variant for it, so the race lesson runs that mutation on a lesson-local status register.

Worked example: the mis-sampled form

The textbook slip is checking the clear against the data bus one cycle later than the write. The module below is a one-bit write-1-to-clear register, correct in itself, and carries either the correct check or the mis-sampled one. Both are in the Boolean history form the tool accepts. The correct check reads the strobe, the data and the hardware set from the same previous cycle; the mis-sampled check reads the data from the current cycle:

w1c_one.sv

// formal: prove 4 expect pass slang top w1c_one
`define FORMAL
module w1c_one #(parameter LATE = 0) (
  input  wire clk,
  input  wire rst,
  input  wire w,        // write strobe
  input  wire wd,       // write data bit
  input  wire hw,       // hardware set pulse
  output reg  status
);
  always @(posedge clk) begin
    if (rst) status <= 1'b0;
    else status <= ((w && wd) ? 1'b0 : status) | hw;
  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
    if (LATE == 0) p_clear: assert (!($past(w) && $past(wd) && !$past(hw)) || !status);   // data and strobe from the same cycle
    else           p_late:  assert (!($past(w) && wd && !$past(hw)) || !status);          // data read one cycle late
  end
`endif
endmodule

The mis-sampled check fails on this correct register. The write at step 2 carries a 0, so the bit correctly stays set; at step 3 the bus moves on and carries a 1, and the mis-sampled check, reading that 1, demands a clear that the write never asked for. A check that fails or passes depending on what the bus does next is flickering with traffic, and the usual wrong cure is to weaken it:

Step	w	wd	hw	status	What the checks read
1	0	1	1	0	hardware sets the bit; status is 1 at step 2
2	1	0	0	1	write presents 0: the bit correctly stays 1
3	0	1	1	1	mis-sampled check: strobe from step 2, data 1 from step 3, demands a clear: fails. Correct check: data 0 from step 2: no demand

w1c_one.sv

// formal: bmc 6 expect fail slang top w1c_one define LATE=1
`define FORMAL
module w1c_one #(parameter LATE = 0) (
  input  wire clk,
  input  wire rst,
  input  wire w,        // write strobe
  input  wire wd,       // write data bit
  input  wire hw,       // hardware set pulse
  output reg  status
);
  always @(posedge clk) begin
    if (rst) status <= 1'b0;
    else status <= ((w && wd) ? 1'b0 : status) | hw;
  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
    if (LATE == 0) p_clear: assert (!($past(w) && $past(wd) && !$past(hw)) || !status);   // data and strobe from the same cycle
    else           p_late:  assert (!($past(w) && wd && !$past(hw)) || !status);          // data read one cycle late
  end
`endif
endmodule

The failing run reports the mis-sampled check at step 4, one step after the state it judges, which follows the reporting rule of this course. The correct form samples the write controls, the write data and the hardware set from the same previous cycle; one sentence pins the cycle for every property in this topic: the consequent is judged in the current cycle against inputs presented in the previous cycle.

What the review looks for

Every history-based property skips the cycle after reset, and the skip is visible in the code.
Write-1-to-clear has both directions: written 1 clears, written 0 keeps, hardware set wins.
Read-only means proved ignored: a write to the offset followed by a read still returns the constant.
Every family has a failing partner that was run, not described.

Verify and debug

A W1C failure with hardware setting in the same cycle is not a failure: the priority says the set wins, and the property conditions the clear on no set. Check the set inputs in the trace before touching the RTL. A flickering property that depends on bus idle patterns is almost always mis-sampled data; align every sampled signal to the same cycle.

Check yourself The clear property conditions on no hardware set in the write cycle. What would removing that condition do?

It would create spurious failures whenever software clears a bit the hardware sets in the same cycle, and engineers would weaken the property to stop the noise. The priority is part of the specification, so it belongs in the property.

Navigate

Why it matters

The core idea

Worked example: three families, each with its bug

Worked example: the mis-sampled form

What the review looks for

Verify and debug

Related topics

W1C, Read-Only and Reset-Value Proofs

Why it matters

The core idea

Worked example: three families, each with its bug

Worked example: the mis-sampled form

What the review looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: three families, each with its bug

Worked example: the mis-sampled form

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: three families, each with its bug

Worked example: the mis-sampled form

What the review looks for

Verify and debug

Related topics

Up next