1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// formal: prove 4 expect pass slang top csr_review
`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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// formal: bmc 8 expect pass slang top csr_review define BUG=2 define NOID=1
`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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// formal: bmc 8 expect pass slang top csr_review define BUG=2 define OUTA=1
`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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// formal: cover 4 expect reached slang top csr_review
`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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// formal: cover 6 expect fail slang top csr_review define NOID=1
`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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// formal: cover 6 expect reached slang top csr_review define BUG=2 define OUTA=1
`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

// csr_review: the register block behind an environment that carries the assumptions under review.
// The first four assumptions are always on. NOID=1 adds the fifth, OUTA=1 adds the sixth.
module csr_review #(parameter BUG = 0, parameter NOID = 0, parameter OUTA = 0) (
  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
);
  wire [7:0] rdata;
  csr_block #(.BUG(BUG)) u_dut (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
                                .set_done(set_done), .set_err(set_err), .rdata(rdata));
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) begin
`ifdef FORMAL
    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5
`endif
  end
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

import re
HARNESS = """    if (init) assume (rst);                                  // 1: the first cycle is a reset
    if (rst) assume (!wr_en);                                // 2: no register write during reset
    if (rst) assume (!set_done && !set_err);                 // 3: no hardware set pulse during reset
    assume (addr <= 2'd3);                                   // 4: addresses are 0 to 3
    if (NOID) assume (!(wr_en && addr == 2'd2));             // 5: nobody writes the read-only ID register
    if (OUTA) assume (addr != 2'd2 || rdata == 8'hA5);       // 6: the ID register always reads 0xA5"""
LABELS = ["a_id_const","a_status_hi","a_rst_ctrl","a_rst_status","a_rst_data","a_ctrl_rw","a_data_rw","a_w1c_done","a_w1c_err","a_w1c_zero","a_hw_set","a_isolate_ctrl","a_isolate_data"]   # assertion labels in the block's file
NEIGHBOUR = ["a_no_wr_in_reset", "a_no_set_in_reset", "a_addr_range"]   # owed by the bus master and the event source
KINDS = {"reset", "interface", "mode", "timing", "temporary", "abstraction"}
OUTPUTS = {"rdata"}
WIDTH = {"addr": 2}

def review(rows, text):
    problems = []
    exprs = [e.strip() for e in re.findall(r"assume \((.*)\);", text)]
    if len(rows) != len(exprs):
        problems.append("ledger has %d rows, harness has %d assumptions" % (len(rows), len(exprs)))
    for name, kind, owner, label, expr in rows:
        if kind not in KINDS or not owner:
            problems.append(name + ": kind or owner missing")
        if label not in LABELS + NEIGHBOUR:
            problems.append(name + ": discharge %r is not an assertion" % label)
        if expr not in exprs:
            problems.append(name + ": expression not in the harness")
        if any(o in expr for o in OUTPUTS):
            problems.append(name + ": assumes a design output")
        m = re.match(r"(\w+) <= 2'd(\d+)", expr)
        if m and int(m.group(2)) >= 2 ** WIDTH[m.group(1)] - 1:
            problems.append(name + ": bound every value satisfies")
    return problems

rows = [("reset first", "reset", "designer", "a_rst_ctrl", "rst"),
        ("no write in reset", "interface", "bus master", "a_no_wr_in_reset", "!wr_en"),
        ("no set in reset", "interface", "event source", "a_no_set_in_reset", "!set_done && !set_err"),
        ("address range", "interface", "bus master", "a_addr_range", "addr <= 2'd3"),
        ("no ID write", "temporary", "nobody", "none", "!(wr_en && addr == 2'd2)"),
        ("ID reads A5", "interface", "designer", "a_id_const", "addr != 2'd2 || rdata == 8'hA5")]
found = review(rows, HARNESS)
assert any("not an assertion" in p for p in found), found
assert any("assumes a design output" in p for p in found), found
assert any("every value satisfies" in p for p in found), found
good = review(rows[:3], "\n".join(HARNESS.splitlines()[:3]))
assert good == [], good
assert any("rows" in p for p in review(rows[:3], HARNESS))
print("PASS: ledger rejects an undischarged row, an output assume, a vacuous bound and row-count drift; the sound rows pass")