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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

// formal: bmc 12 expect pass slang top sync_fifo define BUG=5
`define FORMAL
// property-set mutation: every assertion except the count, flag, pointer and transition properties is turned into a cover (its label starts with x_)
// sync_fifo: 4-entry, 8-bit synchronous FIFO with a combinational read of the oldest word.
// Synchronous active-high reset. count is an output so that properties can see it.
// BUG selects a variant (0 is the design as specified); HELPER=0 removes the helper assertion.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

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

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

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

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

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

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

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

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

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

  // ---- covers: the triggers of the properties can happen ----
  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
    c_tracked_read: cover (tv && !empty && rptr == tslot);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule