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 4 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

# ---- formal lab results ledger, engine v2: every row cites a typed run (kind, depth, outcome[, design]) ----
STATUS = ("proven", "bounded", "cex", "cover-reached", "inconclusive")
FROM_RUN = {"proven": {("prove", "proved")},
            "bounded": {("bmc", "bounded")},
            "cex": {("bmc", "counterexample"), ("prove", "counterexample")},
            "cover-reached": {("cover", "reached")},
            "inconclusive": {("prove", "unproven"), ("cover", "not-reached")}}
NEED = {"sync_fifo": 9, "rr_arbiter": 5, "hs_bridge": 4, "csr_block": 3,
        "pipe3": 5, "pipe3_eq": 5, "mod10_counter": 15, "toggle_demo": 4}
KEYS = ("property", "design", "status", "bound", "why", "run", "assumes", "cover", "kills", "rev")
REV = 3
ALWAYS = "reset-at-step-0"
TRACKED = "tracked-constant-stable"
def row_problems(e, runs, tracked):
    n = e.get("property", "?")
    miss = [k for k in KEYS if k not in e]
    if miss:
        return ["missing-field:%s:%s" % (n, ",".join(miss))]
    if e["status"] not in STATUS:
        return ["bad-status:" + n]
    p = []
    if e["rev"] != REV:
        p.append("stale:" + n)
    if e["run"] not in runs:
        return p + ["no-such-run:" + n]
    kind, depth, outcome = runs[e["run"]][:3]
    if len(runs[e["run"]]) > 3 and runs[e["run"]][3] != e["design"]:
        p.append("run-of-another-design:" + n)         # a run typed with its design may be cited only by that design's rows
    if (kind, outcome) not in FROM_RUN[e["status"]]:
        p.append("status-not-from-run:" + n)
    if e["bound"] != depth:
        p.append("bound-not-run-depth:" + n)
    has_cover = bool(str(e["cover"]).strip())
    if e["status"] in ("proven", "bounded") and not (has_cover and e["kills"]):
        p.append("no-evidence:" + n)
    if e["status"] == "cover-reached" and not has_cover:
        p.append("no-evidence:" + n)
    if e["status"] == "cex" and not e["kills"]:
        p.append("no-evidence:" + n)
    if e["status"] == "bounded":
        if e["design"] not in NEED:
            p.append("unknown-design:" + n)
        elif depth < NEED[e["design"]]:
            p.append("short-bound:" + n)
        if len(str(e["why"]).strip()) < 12:
            p.append("unjustified:" + n)
    if ALWAYS not in e["assumes"]:
        p.append("hidden-assume:%s:%s" % (n, ALWAYS))
    if n in tracked and TRACKED not in e["assumes"]:
        p.append("hidden-assume:%s:%s" % (n, TRACKED))
    return p
def ledger_ok(ledger, runs, required, mutants, register, tracked, final=True):
    names = [e.get("property") for e in ledger]
    bad = ["duplicate:" + n for n in sorted({n for n in names if names.count(n) > 1})]
    bad += ["missing-row:" + r for r in sorted(set(required) - set(names))]
    bad += [q for e in ledger for q in row_problems(e, runs, tracked)]
    good = [e for e in ledger if not row_problems(e, runs, tracked)]      # only a row without complaints counts as evidence
    solid = {e["property"] for e in good if e["status"] in ("proven", "cover-reached")}
    for a, rows in sorted(register.items()):
        if rows is None:
            if final:
                bad.append("deferred-assume:" + a)      # a stage may defer a discharge; a final package may not
        elif not (rows and all(r in solid for r in rows)):
            bad.append("open-assume:" + a)
    bad += ["unregistered-assume:%s:%s" % (e.get("property"), a) for e in ledger
            for a in e.get("assumes", []) if a not in register]
    killed = {m for e in good if e["status"] == "cex" for m in e["kills"]}
    bad += ["survivor:" + m for m in sorted(set(mutants) - killed)]
    bad += ["unsupported-kill:%s:%s" % (e.get("property"), m) for e in ledger
            if e.get("status") in ("proven", "bounded") for m in e.get("kills", []) if m not in killed]
    return bad
def mutation_score(ledger, mutants):
    assert mutants, "no mutants registered"
    killed = {m for e in ledger if e.get("status") == "cex" for m in e.get("kills", [])}
    return len(killed & set(mutants)) / len(mutants)

RUNS = {
    "fifo-prove": ("prove", 4, "proved"),
}
REQUIRED = ["fifo-state-and-flags", "fifo-transitions", "fifo-data-integrity"]
MUTANTS = ["fifo-W%d" % i for i in range(1, 6)]
REGISTER = {"reset-at-step-0": None, "tracked-constant-stable": None}   # discharged by later rows
TRACKED_ROWS = {"fifo-data-integrity"}
YOUR_ROWS = []          # fill from your own runs: one dict per row, the fields of the harness lesson
bad = ledger_ok(YOUR_ROWS, RUNS, REQUIRED, MUTANTS, REGISTER, TRACKED_ROWS, final=False)
if YOUR_ROWS:
    assert bad == [], bad
    print("PASS: stage 1 FIFO package consistent")
else:
    expected = ["missing-row:" + r for r in REQUIRED] + ["survivor:" + m for m in MUTANTS]
    assert sorted(bad) == sorted(expected), bad
    print("PASS: the empty package is rejected with %d complaints" % len(bad))