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

// formal: prove 4 expect unproven slang top csr_reset_pair
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
//   addr 0 CTRL   read/write, reset 0x00
//   addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
//                 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
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
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]) : (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);

  // ---- state properties: true in every cycle after the reset cycle ----
  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

  // ---- transition properties: they look one cycle back ----
  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

  // ---- covers ----
  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);
    c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
  end
`endif
endmodule
// lesson-local wrapper: two copies of csr_block with identical inputs
module csr_reset_pair (
  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] rdata1,
  output wire [7:0] rdata2
);
  csr_block u1 (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
    .set_done(set_done), .set_err(set_err), .rdata(rdata1));
  csr_block u2 (.clk(clk), .rst(rst), .wr_en(wr_en), .addr(addr), .wdata(wdata),
    .set_done(set_done), .set_err(set_err), .rdata(rdata2));
`ifdef FORMAL
  reg c_init = 1'b1;
  always @(posedge clk) c_init <= 1'b0;
  always @(*) if (c_init) assume (rst);
  always @(*) if (!c_init) a_det: assert (rdata1 == rdata2);
  always @(*) if (!c_init) c_pair_write: cover (wr_en && addr == 2'd3);
`endif
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
127
128

// formal: prove 4 expect pass slang top hs_reset_pair_ctrl
`define FORMAL
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;

  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;

  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;

  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
  reg [3:0] acc, dlv;
  always @(posedge clk) begin
    if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
    else begin
      if (in_xfer)  acc <= acc + 4'd1;
      if (out_xfer) dlv <= dlv + 4'd1;
    end
  end

  always @(*) if (!init) begin
    a_skid_needs_out: assert (!svld || ovld);
    a_conserve:       assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
  end

  // ---- protocol: history-based, so skip the cycle after reset ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
    a_data_hold:  assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
    a_no_ready_comb: assert (in_ready == !svld);
  end

  // ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
  (* anyconst *) wire [3:0] tn;
  reg [3:0] tn_q;
  always @(posedge clk) tn_q <= tn;
  always @(*) if (!init) assume (tn == tn_q);
  reg       tv;      // the tracked word has been accepted and not yet delivered
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
      else if (out_xfer && dlv == tn) tv <= 1'b0;
    end
  end
  always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_in_out:  assert (!(tv && dlv == tn) || (ovld && odat == td));
      h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      h_pos:     assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
    end
  end endgenerate

  // ---- covers ----
  always @(*) if (!init) begin
    c_stall:     cover (stalled);
    c_skid_used: cover (svld);
    c_backpress_full: cover (!in_ready);
    c_flow:      cover (in_xfer && out_xfer);
    c_tracked_out: cover (out_xfer && tv && dlv == tn);
  end
`endif
endmodule
// lesson-local wrapper: two identical hs_bridge copies with identical inputs
module hs_reset_pair_ctrl (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire       in_ready1,
  output wire       in_ready2,
  output wire       out_valid1,
  output wire       out_valid2
);
  hs_bridge u1 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready1),
    .in_data(in_data), .out_valid(out_valid1), .out_ready(out_ready), .out_data());
  hs_bridge u2 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(in_ready2),
    .in_data(in_data), .out_valid(out_valid2), .out_ready(out_ready), .out_data());
`ifdef FORMAL
  reg c_init = 1'b1;
  always @(posedge clk) c_init <= 1'b0;
  always @(*) if (c_init) assume (rst);
  always @(*) if (!c_init) a_det_ctrl: assert (in_ready1 == in_ready2 && out_valid1 == out_valid2);
  always @(*) if (!c_init) c_pair_flow: cover (in_valid && in_ready1 && out_ready);
`endif
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

// formal: bmc 2 expect fail slang top hs_reset_pair_data
`define FORMAL
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;

  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;

  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;

  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
  reg [3:0] acc, dlv;
  always @(posedge clk) begin
    if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
    else begin
      if (in_xfer)  acc <= acc + 4'd1;
      if (out_xfer) dlv <= dlv + 4'd1;
    end
  end

  always @(*) if (!init) begin
    a_skid_needs_out: assert (!svld || ovld);
    a_conserve:       assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
  end

  // ---- protocol: history-based, so skip the cycle after reset ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
    a_data_hold:  assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
    a_no_ready_comb: assert (in_ready == !svld);
  end

  // ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
  (* anyconst *) wire [3:0] tn;
  reg [3:0] tn_q;
  always @(posedge clk) tn_q <= tn;
  always @(*) if (!init) assume (tn == tn_q);
  reg       tv;      // the tracked word has been accepted and not yet delivered
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
      else if (out_xfer && dlv == tn) tv <= 1'b0;
    end
  end
  always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_in_out:  assert (!(tv && dlv == tn) || (ovld && odat == td));
      h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      h_pos:     assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
    end
  end endgenerate

  // ---- covers ----
  always @(*) if (!init) begin
    c_stall:     cover (stalled);
    c_skid_used: cover (svld);
    c_backpress_full: cover (!in_ready);
    c_flow:      cover (in_xfer && out_xfer);
    c_tracked_out: cover (out_xfer && tv && dlv == tn);
  end
`endif
endmodule
// lesson-local wrapper: two identical hs_bridge copies with identical inputs
module hs_reset_pair_data (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire [7:0] out_data1,
  output wire [7:0] out_data2
);
  hs_bridge u1 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(),
    .in_data(in_data), .out_valid(), .out_ready(out_ready), .out_data(out_data1));
  hs_bridge u2 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(),
    .in_data(in_data), .out_valid(), .out_ready(out_ready), .out_data(out_data2));
`ifdef FORMAL
  reg c_init = 1'b1;
  always @(posedge clk) c_init <= 1'b0;
  always @(*) if (c_init) assume (rst);
  always @(*) if (!c_init) a_det_data: assert (out_data1 == out_data2);
`endif
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
127
128
129
130
131
132

// formal: prove 4 expect unproven slang top hs_reset_pair_written
`define FORMAL
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;

  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;

  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;

  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
  reg [3:0] acc, dlv;
  always @(posedge clk) begin
    if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
    else begin
      if (in_xfer)  acc <= acc + 4'd1;
      if (out_xfer) dlv <= dlv + 4'd1;
    end
  end

  always @(*) if (!init) begin
    a_skid_needs_out: assert (!svld || ovld);
    a_conserve:       assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
  end

  // ---- protocol: history-based, so skip the cycle after reset ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
    a_data_hold:  assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
    a_no_ready_comb: assert (in_ready == !svld);
  end

  // ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
  (* anyconst *) wire [3:0] tn;
  reg [3:0] tn_q;
  always @(posedge clk) tn_q <= tn;
  always @(*) if (!init) assume (tn == tn_q);
  reg       tv;      // the tracked word has been accepted and not yet delivered
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
      else if (out_xfer && dlv == tn) tv <= 1'b0;
    end
  end
  always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_in_out:  assert (!(tv && dlv == tn) || (ovld && odat == td));
      h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      h_pos:     assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
    end
  end endgenerate

  // ---- covers ----
  always @(*) if (!init) begin
    c_stall:     cover (stalled);
    c_skid_used: cover (svld);
    c_backpress_full: cover (!in_ready);
    c_flow:      cover (in_xfer && out_xfer);
    c_tracked_out: cover (out_xfer && tv && dlv == tn);
  end
`endif
endmodule
// lesson-local wrapper: two identical hs_bridge copies with identical inputs
module hs_reset_pair_written (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire [7:0] out_data1,
  output wire [7:0] out_data2
);
  wire ready1;
  hs_bridge u1 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(ready1),
    .in_data(in_data), .out_valid(), .out_ready(out_ready), .out_data(out_data1));
  hs_bridge u2 (.clk(clk), .rst(rst), .in_valid(in_valid), .in_ready(),
    .in_data(in_data), .out_valid(), .out_ready(out_ready), .out_data(out_data2));
`ifdef FORMAL
  reg c_init = 1'b1;
  always @(posedge clk) c_init <= 1'b0;
  always @(*) if (c_init) assume (rst);
  reg seen = 1'b0;                       // a word has been accepted since the last reset
  always @(posedge clk) begin
    if (rst) seen <= 1'b0;
    else if (in_valid && ready1) seen <= 1'b1;
  end
  always @(*) if (!c_init) a_det_written: assert (!seen || out_data1 == out_data2);
  always @(*) if (!c_init) c_pair_written: cover (seen && out_data1 == 8'hA5);
`endif
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235

// formal: prove 2 expect pass slang top fifo_bridge_chain
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO with a combinational read of the oldest word.
// Synchronous active-high reset. count is an output so that properties can see it.
// BUG selects a variant (0 is the design as specified); HELPER=0 removes the helper assertion.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  // ---- harness: the first cycle is a reset, the state before it is arbitrary ----
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // ---- state properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (they read history, so skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  // ---- data integrity by tracked-slot abstraction: one free slot, one shadow value ----
  // The free constant is an anyconst wire that is also assumed equal to its one-cycle-old copy;
  // this form works in both front ends, while a clocked assume of stability lags one step.
  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;      // the tracked slot holds a word we are watching
  reg [7:0] td;      // the value that should be there
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule
// hs_bridge: valid/ready register stage with a skid register (two words can be held).
// Output stage ovld/odat plus skid stage svld/sdat. in_ready is a function of a register only.
// Synchronous active-high reset empties both stages. A transfer happens in a cycle where valid
// and ready are both 1. BUG selects a variant (0 is the design as specified); HELPER=0 removes the helpers.
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;

  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;

  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;

  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // ---- counters: accepted and delivered words (4 bits, wrap at 16) ----
  reg [3:0] acc, dlv;
  always @(posedge clk) begin
    if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
    else begin
      if (in_xfer)  acc <= acc + 4'd1;
      if (out_xfer) dlv <= dlv + 4'd1;
    end
  end

  always @(*) if (!init) begin
    a_skid_needs_out: assert (!svld || ovld);
    a_conserve:       assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
  end

  // ---- protocol: history-based, so skip the cycle after reset ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
    a_data_hold:  assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
    a_no_ready_comb: assert (in_ready == !svld);
  end

  // ---- data integrity by tracked-word abstraction: follow the n-th accepted word ----
  (* anyconst *) wire [3:0] tn;
  reg [3:0] tn_q;
  always @(posedge clk) tn_q <= tn;
  always @(*) if (!init) assume (tn == tn_q);
  reg       tv;      // the tracked word has been accepted and not yet delivered
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
      else if (out_xfer && dlv == tn) tv <= 1'b0;
    end
  end
  always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_in_out:  assert (!(tv && dlv == tn) || (ovld && odat == td));
      h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      h_pos:     assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
    end
  end endgenerate

  // ---- covers ----
  always @(*) if (!init) begin
    c_stall:     cover (stalled);
    c_skid_used: cover (svld);
    c_backpress_full: cover (!in_ready);
    c_flow:      cover (in_xfer && out_xfer);
    c_tracked_out: cover (out_xfer && tv && dlv == tn);
  end
`endif
endmodule
// lesson-local wrapper: FIFO into bridge, with a mode that selects the bridge source (the connectivity table is below)
module fifo_bridge_chain #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       mode,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       ext_valid,
  input  wire [7:0] ext_data,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  wire [7:0] frdata;
  wire ffull, fempty;
  wire [2:0] fcount;
  wire bin_valid, bin_ready;
  wire [7:0] bin_data;
  wire take = bin_valid && bin_ready;
  sync_fifo u_f (.clk(clk), .rst(rst), .push(push), .wdata(wdata),
    .pop(take && !mode), .rdata(frdata), .full(ffull), .empty(fempty), .count(fcount));
  assign bin_valid = (BUG == 2) ? (mode ? !fempty : ext_valid) : (mode ? ext_valid : !fempty);
  assign bin_data  = (BUG == 1) ? (mode ? frdata : ext_data) : (mode ? ext_data : frdata);
  hs_bridge u_b (.clk(clk), .rst(rst), .in_valid(bin_valid), .in_ready(bin_ready),
    .in_data(bin_data), .out_valid(out_valid), .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg d_init = 1'b1;
  always @(posedge clk) d_init <= 1'b0;
  always @(*) if (d_init) assume (rst);
  // one assertion per row of the table, under the row's mode condition
  always @(*) if (!d_init) begin
    a_row_d0: assert (mode != 1'b0 || bin_data == frdata);
    a_row_d1: assert (mode != 1'b1 || bin_data == ext_data);
    a_row_v0: assert (mode != 1'b0 || bin_valid == !fempty);
    a_row_v1: assert (mode != 1'b1 || bin_valid == ext_valid);
  end
  always @(*) if (!d_init) c_chain_fifo_word: cover (!mode && bin_valid && bin_data == 8'hA5);
`endif
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

# ---- formal lab results ledger, engine v2: every row cites a typed run (kind, depth, outcome[, design]) ----
STATUS = ("proven", "bounded", "cex", "cover-reached", "inconclusive")
FROM_RUN = {"proven": {("prove", "proved")},
            "bounded": {("bmc", "bounded")},
            "cex": {("bmc", "counterexample"), ("prove", "counterexample")},
            "cover-reached": {("cover", "reached")},
            "inconclusive": {("prove", "unproven"), ("cover", "not-reached")}}
NEED = {"sync_fifo": 9, "rr_arbiter": 5, "hs_bridge": 4, "csr_block": 3,
        "pipe3": 5, "pipe3_eq": 5, "mod10_counter": 15, "toggle_demo": 4}
KEYS = ("property", "design", "status", "bound", "why", "run", "assumes", "cover", "kills", "rev")
REV = 3
ALWAYS = "reset-at-step-0"
TRACKED = "tracked-constant-stable"
def row_problems(e, runs, tracked):
    n = e.get("property", "?")
    miss = [k for k in KEYS if k not in e]
    if miss:
        return ["missing-field:%s:%s" % (n, ",".join(miss))]
    if e["status"] not in STATUS:
        return ["bad-status:" + n]
    p = []
    if e["rev"] != REV:
        p.append("stale:" + n)
    if e["run"] not in runs:
        return p + ["no-such-run:" + n]
    kind, depth, outcome = runs[e["run"]][:3]
    if len(runs[e["run"]]) > 3 and runs[e["run"]][3] != e["design"]:
        p.append("run-of-another-design:" + n)         # a run typed with its design may be cited only by that design's rows
    if (kind, outcome) not in FROM_RUN[e["status"]]:
        p.append("status-not-from-run:" + n)
    if e["bound"] != depth:
        p.append("bound-not-run-depth:" + n)
    has_cover = bool(str(e["cover"]).strip())
    if e["status"] in ("proven", "bounded") and not (has_cover and e["kills"]):
        p.append("no-evidence:" + n)
    if e["status"] == "cover-reached" and not has_cover:
        p.append("no-evidence:" + n)
    if e["status"] == "cex" and not e["kills"]:
        p.append("no-evidence:" + n)
    if e["status"] == "bounded":
        if e["design"] not in NEED:
            p.append("unknown-design:" + n)
        elif depth < NEED[e["design"]]:
            p.append("short-bound:" + n)
        if len(str(e["why"]).strip()) < 12:
            p.append("unjustified:" + n)
    if ALWAYS not in e["assumes"]:
        p.append("hidden-assume:%s:%s" % (n, ALWAYS))
    if n in tracked and TRACKED not in e["assumes"]:
        p.append("hidden-assume:%s:%s" % (n, TRACKED))
    return p
def ledger_ok(ledger, runs, required, mutants, register, tracked, final=True):
    names = [e.get("property") for e in ledger]
    bad = ["duplicate:" + n for n in sorted({n for n in names if names.count(n) > 1})]
    bad += ["missing-row:" + r for r in sorted(set(required) - set(names))]
    bad += [q for e in ledger for q in row_problems(e, runs, tracked)]
    good = [e for e in ledger if not row_problems(e, runs, tracked)]      # only a row without complaints counts as evidence
    solid = {e["property"] for e in good if e["status"] in ("proven", "cover-reached")}
    for a, rows in sorted(register.items()):
        if rows is None:
            if final:
                bad.append("deferred-assume:" + a)      # a stage may defer a discharge; a final package may not
        elif not (rows and all(r in solid for r in rows)):
            bad.append("open-assume:" + a)
    bad += ["unregistered-assume:%s:%s" % (e.get("property"), a) for e in ledger
            for a in e.get("assumes", []) if a not in register]
    killed = {m for e in good if e["status"] == "cex" for m in e["kills"]}
    bad += ["survivor:" + m for m in sorted(set(mutants) - killed)]
    bad += ["unsupported-kill:%s:%s" % (e.get("property"), m) for e in ledger
            if e.get("status") in ("proven", "bounded") for m in e.get("kills", []) if m not in killed]
    return bad
def mutation_score(ledger, mutants):
    assert mutants, "no mutants registered"
    killed = {m for e in ledger if e.get("status") == "cex" for m in e.get("kills", [])}
    return len(killed & set(mutants)) / len(mutants)

RUNS = {
    "csr-pair-nohelp": ("prove", 4, "unproven"),
    "hs-pair-ctrl": ("prove", 4, "proved"),
    "hs-pair-data": ("bmc", 2, "counterexample"),
    "hs-pair-written-nohelp": ("prove", 4, "unproven"),
    "chain-prove": ("prove", 2, "proved"),
}
REQUIRED = ["csr-reset-determinism", "bridge-control-determinism", "bridge-data-after-write", "chain-connectivity"]
MUTANTS = ["csr-pair-noreset", "hs-pair-noreset", "hs-pair-data-claim", "chain-swap-data", "chain-swap-valid"]
REGISTER = {"reset-at-step-0": ["csr-reset-determinism", "bridge-control-determinism"]}
YOUR_ROWS = []          # fill from your own runs
bad = ledger_ok(YOUR_ROWS, RUNS, REQUIRED, MUTANTS, REGISTER, set(), final=False)
if YOUR_ROWS:
    assert bad == [], bad
    verdict = "stage 2 pair and chain package consistent"
else:
    expected = (["missing-row:" + r for r in REQUIRED] + ["survivor:" + m for m in MUTANTS]
                + ["open-assume:reset-at-step-0"])
    assert sorted(bad) == sorted(expected), bad
    verdict = "the empty package is rejected: the reset assumption has no discharging rows"
# an unproven pair row cannot discharge the assumption: the run is inconclusive, not proven
inconclusive = dict(property="csr-reset-determinism", design="csr_block", status="inconclusive", bound=4, why="the step fails",
                    run="csr-pair-nohelp", assumes=["reset-at-step-0"], cover="", kills=[], rev=3)
assert "open-assume:reset-at-step-0" in ledger_ok([inconclusive], RUNS, [], [], REGISTER, set(), final=False)
print("PASS: %s; an inconclusive pair does not discharge the reset assumption" % verdict)