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

import random

def trace_counter(n, rng, last=9):
    s, out = 0, []
    for _ in range(n):
        out.append(s)
        if rng.choice([0, 1]):
            s = 0 if s == last else s + 1
    return out

def trace_fifo(n, rng):
    count, w, r, out = 0, 0, 0, []
    for _ in range(n):
        push, pop = rng.choice([0, 1]), rng.choice([0, 1])
        dp = push and count < 4
        dq = pop and count > 0
        out.append((count, w, r))
        if dp:
            w = (w + 1) % 4
        if dq:
            r = (r + 1) % 4
        count += dp - dq
    return out

rng = random.Random(7)
samples_c = trace_counter(8, rng)
samples_f = trace_fifo(8, rng)

reach_c = set(range(10))                                     # exhaustive reachable counter states
reach_f = {(c, (r + c) % 4, r) for c in range(5) for r in range(4)}   # (count, wptr, rptr): 20 states
assert len(reach_f) == 20

cands_c = {"count<=9": lambda s: s <= 9,
           "count!=15": lambda s: s != 15,
           "count<=5": lambda s: s <= 5}
cands_f = {"count%4 == (wptr-rptr)%4": lambda t: t[0] % 4 == (t[1] - t[2]) % 4,
           "count<=4": lambda t: t[0] <= 4,
           "wptr == rptr": lambda t: t[1] == t[2]}

surv_c = {n for n, p in cands_c.items() if all(p(s) for s in samples_c)}
surv_f = {n for n, p in cands_f.items() if all(p(t) for t in samples_f)}
assert "count<=5" in surv_c, "the seeded trace must show the sample illusion"
assert "wptr == rptr" not in surv_f

proven_c = {n for n in surv_c if all(cands_c[n](s) for s in reach_c)}
proven_f = {n for n in surv_f if all(cands_f[n](t) for t in reach_f)}
assert proven_c == {"count<=9", "count!=15"}, proven_c        # count<=5 is dropped by the full set
assert proven_f == {"count%4 == (wptr-rptr)%4", "count<=4"}, proven_f

# injected data: a corrupted sample that the pointer relation refutes
bad_sample = (2, 0, 1)   # count 2 with wptr 0 and rptr 1
assert not cands_f["count%4 == (wptr-rptr)%4"](bad_sample)

# simple path: the longest loop-free window of states satisfying never-15 that ends in a violation
def succ(s, free, last=9):
    nxt = 0 if s == last else (s + 1) % 16
    return {s, nxt} if free else {nxt}

P = set(range(15))
def longest_simple_window(free):
    best = 0
    def dfs(s, path):
        nonlocal best
        for t in succ(s, free):
            if t not in P:
                best = max(best, len(path))
            elif t not in path:
                dfs(t, path | {t})
    for s in P:
        dfs(s, {s})
    return best

assert longest_simple_window(True) == 5    # free enable: self loops cannot extend a simple window
assert longest_simple_window(False) == 5   # enable high gives the same chain
assert longest_simple_window(True) + 1 == 6   # the step would close at k = 6, as the enable-high runs did
print("PASS: count<=5 survives the samples and dies against the reachable set; simple-path window 5, k = 6")

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

// formal: prove 2 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
//   rst (synchronous, active high) : count <= 0
//   en  = 1                        : count <= (count == 9) ? 0 : count + 1
//   en  = 0                        : count holds
//   tc  = en && (count == 9)       : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);

  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end

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

  // P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
  // unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
  // so no k of k-induction closes it).
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  // P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate

  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end

  // sticky flag: the counter has wrapped at least once
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  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

// formal: bmc 8 expect fail slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
//   rst (synchronous, active high) : count <= 0
//   en  = 1                        : count <= (count == 9) ? 0 : count + 1
//   en  = 0                        : count holds
//   tc  = en && (count == 9)       : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);

  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end

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

  // P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
  // unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
  // so no k of k-induction closes it).
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  // P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate

  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end

  // sticky flag: the counter has wrapped at least once
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
  always @(*) if (!init) a_cand5: assert (count <= 4'd5);   // plausible from a short trace, false of the design
`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

// formal: prove 1 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.
// This copy keeps the control properties only: no data-integrity harness.
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));
    // occupancy equals pointer distance (mod 4)
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  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

// 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.
// This copy keeps the control properties only: no data-integrity harness.
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));
    // occupancy equals pointer distance (mod 4)
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

`endif
endmodule