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: prove 4 expect pass slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`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: bmc 7 expect fail slang top sync_fifo define BUG=1
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`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: bmc 5 expect fail slang top sync_fifo define BUG=3
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`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: bmc 4 expect fail slang top sync_fifo define BUG=4
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`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: prove 4 expect pass slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);

  // reset empties the FIFO: in the cycle after a reset cycle every control register holds its reset value
  always @(posedge clk) if (!init && $past(rst)) a_reset: assert (count == 3'd0 && wptr == 2'd0 && rptr == 2'd0);
`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 3 expect fail slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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'd1;   // planted: reset leaves one phantom word
      rptr  <= 2'd0;
      count <= 3'd1;
    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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);

  // reset empties the FIFO: in the cycle after a reset cycle every control register holds its reset value
  always @(posedge clk) if (!init && $past(rst)) a_reset: assert (count == 3'd0 && wptr == 2'd0 && rptr == 2'd0);
`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

// formal: cover 6 expect reached slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
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;   // forgets the pop
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

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

  // ---- safety properties (after the reset cycle) ----
  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);                       // no overflow, no underflow wrap
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    // helper invariant: occupancy equals pointer distance (mod 4) unless full
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  // ---- transition properties (use history: skip the cycle after reset) ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    // push alone when not full adds one; pop alone when not empty removes one
    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);
    // push into a full FIFO (and no pop) is ignored: occupancy unchanged
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    // simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
    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) ----
  // free constant: (* anyconst *) alone is not honoured by the front end named in the header, so the
  // value is also assumed equal to its one-cycle-old copy (works in both front ends;
  // a clocked assume ($stable) lags one step and leaks at the last step: do not use it)
  (* 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 value 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);
  // helper invariant needed for the induction step of a_data
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  // ---- covers: the properties are not vacuous ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);

  // antecedent covers for the transition properties
  always @(*) if (!init) begin
    c_ovf: cover (push && !pop && full);
    c_pop: cover (pop && !push && !empty);
  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

// formal: bmc 14 expect pass slang top rsp_unit define LAT=1
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); 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

// formal: cover 7 expect reached slang top rsp_unit
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); 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

// formal: bmc 8 expect fail slang top rsp_unit define BUG=1
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); 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

// formal: bmc 5 expect fail slang top rsp_unit define BUG=1 define LAT=1
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); 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

// formal: bmc 14 expect pass slang top rsp_unit define BUG=2 define ONE=0
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); 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

// formal: bmc 5 expect fail slang top rsp_unit define BUG=2
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); 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

// formal: bmc 5 expect fail slang top rsp_unit define EXACT=1
`define FORMAL
// rsp_unit: accepts one request at a time and answers it d + 2 cycles later (d is sampled with the request, so the
// latency is 2 to 5 cycles). BUG: 0 none, 1 slow (one extra cycle, 3 to 6), 2 duplicate answer, 3 answer dropped.
// ONE=1 checks one answer per request, EXACT=1 adds a wrong window, LAT=1 adds the exact-latency check.
module rsp_unit #(parameter BUG = 0, parameter ONE = 1, parameter EXACT = 0, parameter LAT = 0) (
  input wire clk, input wire rst, input wire req, input wire [1:0] d, output reg rsp);
  reg busy; reg [2:0] cnt; reg dup;
  wire acc = req && !busy;
  always @(posedge clk) begin
    rsp <= 1'b0;
    if (rst) begin busy <= 1'b0; cnt <= 3'd0; dup <= 1'b0; end
    else begin
      dup <= 1'b0;
      if (acc) begin busy <= 1'b1; cnt <= {1'b0, d} + ((BUG == 1) ? 3'd1 : 3'd0); end
      else if (busy && cnt != 3'd0) cnt <= cnt - 3'd1;
      else if (busy) begin
        busy <= 1'b0;
        rsp <= (BUG != 3);
        dup <= (BUG == 2);
      end
      if (dup) rsp <= 1'b1;
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // harness: waiting = a request is unanswered (cleared by the first answer), age = cycles it has waited,
  // pend = requests accepted minus answers seen
  reg waiting; reg [2:0] age; reg [1:0] pend;
  always @(posedge clk) begin
    if (rst) begin waiting <= 1'b0; age <= 3'd0; pend <= 2'd0; end
    else begin
      pend <= pend + {1'b0, acc} - {1'b0, rsp};
      if (rsp && waiting) begin waiting <= acc; age <= acc ? 3'd1 : 3'd0; end
      else if (acc) begin waiting <= 1'b1; age <= 3'd1; end
      else if (waiting) age <= (age == 3'd7) ? age : age + 3'd1;
    end
  end
  // bounded response (a safety property, not liveness): no request waits longer than 5 cycles
  always @(*) if (!init) a_within5: assert (age <= 3'd5);
  // exact latency: the answer comes d + 2 cycles after the request, where d is the value sampled WITH that request.
  // dacc holds d from the last accepted request, which is what a gated past value would give.
  reg [1:0] dacc;
  always @(posedge clk) if (acc) dacc <= d;
  generate if (LAT) begin : g_lat
    always @(*) if (!init && rsp && waiting) a_lat: assert (age == {1'b0, dacc} + 3'd2);
  end endgenerate
  // one answer per request: an answer needs an outstanding request, and requests are not stacked
  generate if (ONE) begin : g_one
    always @(*) if (!init) begin
      a_pend_max:   assert (pend <= 2'd1);
      a_no_phantom: assert (!rsp || pend != 2'd0);
    end
  end endgenerate
  // the wrong window: "answered exactly 3 cycles after the request"
  generate if (EXACT) begin : g_exact
    always @(posedge clk) if (!init && !$past(rst)) a_exact3: assert (!rsp || $past(acc, 3));
  end endgenerate
  always @(*) if (!init) begin c_acc: cover (acc); c_rsp: cover (rsp); c_slow: cover (rsp && age == 3'd5); end
`endif
endmodule