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

def bridge(bug, steps):
    ovld = svld = 0
    odat = sdat = 0
    acc = dlv = 0
    queue, log = [], []
    for iv, d, orr in steps:
        in_xfer = bool(iv) and not svld
        out_xfer = bool(ovld) and bool(orr)
        stalled = bool(ovld) and not orr
        if in_xfer:
            queue.append(d)
        log.append(dict(ovld=ovld, svld=svld, acc=acc, dlv=dlv, odat=odat,
                        conserve=(acc - dlv == ovld + svld),
                        data=(not out_xfer) or (bool(queue) and odat == queue[0])))
        if out_xfer and queue:
            queue.pop(0)
        n_ovld, n_svld, n_odat, n_sdat = ovld, svld, odat, sdat
        if stalled:
            if in_xfer and bug != 1:
                n_svld, n_sdat = 1, d
            if bug == 2 and not iv:
                n_ovld = 0
            if bug == 3 and in_xfer:
                n_odat = d
        elif svld:
            n_odat, n_ovld, n_svld = sdat, 1, 0
        else:
            n_odat, n_ovld = d, int(bool(iv))
        acc, dlv = acc + int(in_xfer), dlv + int(out_xfer)
        ovld, svld, odat, sdat = n_ovld, n_svld, n_odat, n_sdat
    return log
def first_fail(log, key):
    return next((i + 1 for i, r in enumerate(log) if not r[key]), None)     # step numbers start at 1 after the reset
A, Bw = 0x0A, 0x0B
w1 = bridge(1, [(1, A, 0), (1, Bw, 0), (0, 0, 0)])
w2 = bridge(2, [(1, A, 0), (0, 0, 0), (0, 0, 0)])
w3 = bridge(3, [(1, A, 0), (1, Bw, 0), (0, 0, 1)])
assert first_fail(w1, "conserve") == 3 and first_fail(w2, "conserve") == 3
assert first_fail(w3, "data") == 3 and first_fail(w3, "conserve") is None
good = bridge(0, [(1, A, 0), (1, Bw, 0), (0, 0, 1), (0, 0, 1)])
assert first_fail(good, "conserve") is None and first_fail(good, "data") is None
print("PASS: conservation sees W1 and W2 at step 3; the data check sees W3 at step 3 and conservation never does")

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

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

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

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

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

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

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

// formal: bmc 14 expect pass slang top hs_bridge define BUG=3
`define FORMAL
// property-set mutation: every assertion except the skid, conservation, valid-hold and ready properties is turned into a cover (its label starts with x_)
// 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);
    x_a_data_hold:  cover (!($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) x_a_data: cover (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      x_h_in_out:  cover (!(tv && dlv == tn) || (ovld && odat == td));
      x_h_in_skid: cover (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      x_h_pos:     cover (!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

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 12 expect pass slang top bridge_rule_top define BUG=1 define RULE=1
`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: the bridge under an extra rule on its input. RULE=0 removes the rule.
module bridge_rule_top #(parameter BUG = 0, parameter RULE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire       in_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(BUG)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg t_init = 1'b1;
  always @(posedge clk) t_init <= 1'b0;
  always @(*) if (t_init) assume (rst);
  // the rule: the upstream never sends while the output is not ready
  always @(*) if (RULE && !t_init) assume (!in_valid || 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
126

// formal: bmc 12 expect pass slang top bridge_rule_top define BUG=3 define RULE=1
`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: the bridge under an extra rule on its input. RULE=0 removes the rule.
module bridge_rule_top #(parameter BUG = 0, parameter RULE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire       in_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(BUG)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg t_init = 1'b1;
  always @(posedge clk) t_init <= 1'b0;
  always @(*) if (t_init) assume (rst);
  // the rule: the upstream never sends while the output is not ready
  always @(*) if (RULE && !t_init) assume (!in_valid || 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
126

// formal: bmc 4 expect fail slang top bridge_rule_top define BUG=2 define RULE=1
`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: the bridge under an extra rule on its input. RULE=0 removes the rule.
module bridge_rule_top #(parameter BUG = 0, parameter RULE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire       in_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(BUG)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg t_init = 1'b1;
  always @(posedge clk) t_init <= 1'b0;
  always @(*) if (t_init) assume (rst);
  // the rule: the upstream never sends while the output is not ready
  always @(*) if (RULE && !t_init) assume (!in_valid || 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
126

// formal: bmc 4 expect fail slang top bridge_rule_top define BUG=1 define RULE=0
`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: the bridge under an extra rule on its input. RULE=0 removes the rule.
module bridge_rule_top #(parameter BUG = 0, parameter RULE = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  input  wire       out_ready,
  output wire       in_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  hs_bridge #(.BUG(BUG)) u (.clk(clk), .rst(rst), .in_valid(in_valid),
    .in_ready(in_ready), .in_data(in_data), .out_valid(out_valid),
    .out_ready(out_ready), .out_data(out_data));
`ifdef FORMAL
  reg t_init = 1'b1;
  always @(posedge clk) t_init <= 1'b0;
  always @(*) if (t_init) assume (rst);
  // the rule: the upstream never sends while the output is not ready
  always @(*) if (RULE && !t_init) assume (!in_valid || 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

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

RESULTS = {("W1", "rule"): "pass", ("W1", "plain"): "counterexample", ("W2", "rule"): "counterexample", ("W2", "plain"): "counterexample",
           ("W3", "rule"): "pass", ("W3", "plain"): "counterexample"}
hidden = sorted(v for v in ("W1", "W2", "W3") if RESULTS[(v, "rule")] == "pass" and RESULTS[(v, "plain")] == "counterexample")
assert hidden == ["W1", "W3"]
row = dict(property="bridge-under-rule", design="hs_bridge", status="bounded", bound=12, why="rule on: no input while stalled",
           run="bridge-rule-on", assumes=["reset-at-step-0", "no-input-while-stalled"], cover="c_stall step 2", kills=["bridge-W1"], rev=3)
RUNS = {"bridge-rule-on": ("bmc", 12, "bounded"), "bridge-w1": ("bmc", 4, "counterexample")}
bad = ledger_ok([row], RUNS, [], ["bridge-W1"], {"reset-at-step-0": None}, set(), final=False)
assert "unregistered-assume:bridge-under-rule:no-input-while-stalled" in bad
assert "survivor:bridge-W1" in bad and "unsupported-kill:bridge-under-rule:bridge-W1" in bad, bad
print("PASS: a pass under an input rule is refused as the evidence of a kill: the fault it hides stays a survivor")

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

// formal: prove 12 expect unproven slang top hs_bridge define HELPER=0
`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

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

// formal: bmc 5 expect fail slang top hs_bridge
`define FORMAL
// mutant bridge-m-ready-comb: in_ready also depends on out_ready in the same cycle
// 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 || out_ready;
  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