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

// formal: prove 4 expect pass slang top pipe3
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule

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

// formal: bmc 5 expect fail slang top pipe3 define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1, parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= (BUG == 1) ? s[3:0] * c[3:0] : s[3:0] * c1;      // BUG 1: stage 2 takes its operand straight from the input
      y  <= (BUG == 2) ? s[3:0] * c1 + 8'd1 : p + 8'd1;      // BUG 2: stage 3 skips stage 2
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule

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

// formal: bmc 5 expect fail slang top pipe3 define BUG=2
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1, parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= (BUG == 1) ? s[3:0] * c[3:0] : s[3:0] * c1;      // BUG 1: stage 2 takes its operand straight from the input
      y  <= (BUG == 2) ? s[3:0] * c1 + 8'd1 : p + 8'd1;      // BUG 2: stage 3 skips stage 2
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule

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

// formal: bmc 5 expect fail slang top pipe3_eq define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
  always @(posedge clk) if (!init && !$past(rst)) a_loc3: assert (y2 == $past(s2_ret) * $past(c2_ret) + 8'd1);   // stage 3 on its own
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule

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

// formal: bmc 6 expect fail slang top pipe3_eq define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) c_differ: cover (!same);   // the end-to-end check is off; this only watches
  always @(posedge clk) if (!init && !$past(rst)) a_loc3: assert (y2 == $past(s2_ret) * $past(c2_ret) + 8'd1);   // stage 3 on its own
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule

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

// formal: bmc 12 expect pass slang top pipe3_eq define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) c_differ: cover (!same);   // the end-to-end check is off; this only watches
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule

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

// formal: prove 5 expect pass slang top pipe3_eq
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
module pipe3 #(parameter CHECK = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [7:0] dbg_p          // stage-2 register, exposed for the miter's helper invariant
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [7:0] p;
  assign dbg_p = p;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      p  <= s[3:0] * c1;
      y  <= p + 8'd1;
    end
  end

`ifdef FORMAL
  // CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
  generate if (CHECK) begin : g_chk
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // hist counts clean cycles since reset (saturates at 3): y is only specified after 3
  reg [1:0] hist;
  always @(posedge clk) begin
    if (rst) hist <= 2'd0;
    else if (hist != 2'd3) hist <= hist + 2'd1;
  end

  // input history, as plain registers (works in every front end)
  reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
  always @(posedge clk) begin
    sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
    sa2 <= sa1;    sb2 <= sb1;    sc2 <= sc1;
    sa3 <= sa2;    sb3 <= sb2;    sc3 <= sc2;
  end
  wire [3:0] sum3 = sa3 + sb3;       // low 4 bits of a + b three cycles ago

  // functional property with latency 3, checked only after 3 clean cycles
  always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
  // after reset the output register is 0
  always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
  always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
  end endgenerate
`endif
endmodule

module pipe3_retimed #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output reg  [7:0] y,
  output wire [3:0] dbg_s2,        // stage-2 registers, exposed for the miter's helper invariant
  output wire [3:0] dbg_c2
);
  reg [7:0] s;
  reg [3:0] c1;
  reg [3:0] s2, c2;
  assign dbg_s2 = s2;
  assign dbg_c2 = c2;
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
    else begin
      s  <= a + b;
      c1 <= c[3:0];
      s2 <= s[3:0];
      c2 <= c1;
      y  <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
    end
  end
endmodule

module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  input  wire [7:0] c,
  output wire       same
);
  wire [7:0] y1, y2, p_ref;
  wire [3:0] s2_ret, c2_ret;
  pipe3 #(.CHECK(0))     u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
  pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
  assign same = (y1 == y2);

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
  always @(posedge clk) if (!init && !$past(rst)) a_loc3: assert (y2 == $past(s2_ret) * $past(c2_ret) + 8'd1);   // stage 3 on its own
  // helper invariant across the moved cut: the reference's stage-2 register p equals the
  // twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
  end endgenerate
  always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule