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

// formal: prove 4 expect pass slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
//   addr 0 CTRL   read/write, reset 0x00
//   addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
//                 set_err (a set wins over a clear in the same cycle); bits 7:2 read 0; reset 0x00
//   addr 2 ID     read-only constant 0xA5 (writes ignored)
//   addr 3 DATA   read/write, reset 0x3C
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       wr_en,
  input  wire [1:0] addr,
  input  wire [7:0] wdata,
  input  wire       set_done,
  input  wire       set_err,
  output wire [7:0] rdata
);
  reg [7:0] ctrl, data, id_r;
  reg [1:0] status;                       // [0] DONE, [1] ERR

  wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
  assign rdata = (addr == 2'd0) ? ctrl :
                 (addr == 2'd1) ? {6'b0, status} :
                 (addr == 2'd2) ? id_val : data;

  wire w_ctrl   = wr_en && addr == 2'd0;
  wire w_status = wr_en && addr == 2'd1;
  wire w_id     = wr_en && addr == 2'd2;
  wire w_data   = wr_en && addr == 2'd3;

  wire [1:0] hw_set = {set_err, set_done};
  wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) : (status & ~wdata[1:0]);

  always @(posedge clk) begin
    if (rst) begin
      ctrl   <= 8'h00;
      status <= 2'b00;
      data   <= (BUG == 3) ? 8'h00 : 8'h3C;
      id_r   <= 8'hA5;
    end else begin
      if (w_ctrl) ctrl <= wdata;
      if (w_data) data <= wdata;
      if (w_id && BUG == 2) id_r <= wdata;
      status <= (w_status ? after_w : status) | hw_set;
    end
  end

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

  // ---- state properties: true in every cycle after the reset cycle ----
  always @(*) if (!init) begin
    a_id_const:  assert (addr != 2'd2 || rdata == 8'hA5);
    a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
  end

  // ---- transition properties: they look one cycle back ----
  always @(posedge clk) if (!init) begin
    if ($past(rst)) begin
      a_rst_ctrl:   assert (ctrl == 8'h00);
      a_rst_status: assert (status == 2'b00);
      a_rst_data:   assert (data == 8'h3C);
    end
    if (!$past(rst)) begin
      a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
      a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
      a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
      a_w1c_err:  assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err))  || !status[1]);
      a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
      a_hw_set:   assert (!$past(set_done) || status[0]);
      a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
      a_isolate_data: assert ($past(w_data) || data == $past(data));
    end
  end

  // ---- covers ----
  always @(*) if (!init) begin
    c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
    c_both_bits: cover (status == 2'b11);
    c_id_write:  cover (w_id);
    c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
  end
`endif
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
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

// formal: cover 4 expect reached slang top csr_block
`define FORMAL
// csr_block: four 8-bit registers on a synchronous write port with a combinational read.
//   addr 0 CTRL   read/write, reset 0x00
//   addr 1 STATUS bit 0 DONE, bit 1 ERR: write 1 to clear, set by the hardware pulses set_done and
//                 set_err (a set wins over a clear in the same cycle); bits 7:2 read 0; reset 0x00
//   addr 2 ID     read-only constant 0xA5 (writes ignored)
//   addr 3 DATA   read/write, reset 0x3C
// A write (wr_en with addr and wdata) takes effect at the clock edge; rdata shows the register
// selected by addr. Synchronous active-high reset. BUG selects a variant (0 is the design as specified).
module csr_block #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       wr_en,
  input  wire [1:0] addr,
  input  wire [7:0] wdata,
  input  wire       set_done,
  input  wire       set_err,
  output wire [7:0] rdata
);
  reg [7:0] ctrl, data, id_r;
  reg [1:0] status;                       // [0] DONE, [1] ERR

  wire [7:0] id_val = (BUG == 2) ? id_r : 8'hA5;
  assign rdata = (addr == 2'd0) ? ctrl :
                 (addr == 2'd1) ? {6'b0, status} :
                 (addr == 2'd2) ? id_val : data;

  wire w_ctrl   = wr_en && addr == 2'd0;
  wire w_status = wr_en && addr == 2'd1;
  wire w_id     = wr_en && addr == 2'd2;
  wire w_data   = wr_en && addr == 2'd3;

  wire [1:0] hw_set = {set_err, set_done};
  wire [1:0] after_w = (BUG == 1) ? (status | wdata[1:0]) : (status & ~wdata[1:0]);

  always @(posedge clk) begin
    if (rst) begin
      ctrl   <= 8'h00;
      status <= 2'b00;
      data   <= (BUG == 3) ? 8'h00 : 8'h3C;
      id_r   <= 8'hA5;
    end else begin
      if (w_ctrl) ctrl <= wdata;
      if (w_data) data <= wdata;
      if (w_id && BUG == 2) id_r <= wdata;
      status <= (w_status ? after_w : status) | hw_set;
    end
  end

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

  // ---- state properties: true in every cycle after the reset cycle ----
  always @(*) if (!init) begin
    a_id_const:  assert (addr != 2'd2 || rdata == 8'hA5);
    a_status_hi: assert (addr != 2'd1 || rdata[7:2] == 6'b0);
  end

  // ---- transition properties: they look one cycle back ----
  always @(posedge clk) if (!init) begin
    if ($past(rst)) begin
      a_rst_ctrl:   assert (ctrl == 8'h00);
      a_rst_status: assert (status == 2'b00);
      a_rst_data:   assert (data == 8'h3C);
    end
    if (!$past(rst)) begin
      a_ctrl_rw: assert (!($past(w_ctrl)) || ctrl == $past(wdata));
      a_data_rw: assert (!($past(w_data)) || data == $past(wdata));
      a_w1c_done: assert (!($past(w_status) && $past(wdata[0]) && !$past(set_done)) || !status[0]);
      a_w1c_err:  assert (!($past(w_status) && $past(wdata[1]) && !$past(set_err))  || !status[1]);
      a_w1c_zero: assert (!($past(w_status) && !$past(wdata[0]) && $past(status[0])) || status[0]);
      a_hw_set:   assert (!$past(set_done) || status[0]);
      a_isolate_ctrl: assert ($past(w_ctrl) || ctrl == $past(ctrl));
      a_isolate_data: assert ($past(w_data) || data == $past(data));
    end
  end

  // ---- covers ----
  always @(*) if (!init) begin
    c_w1c_clear: cover (w_status && wdata[0] && status[0] && !set_done);
    c_both_bits: cover (status == 2'b11);
    c_id_write:  cover (w_id);
    c_set_collision: cover (w_status && wdata[0] && status[0] && set_done);
  end
`endif
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
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

# ---- 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)

# the register map as data: (name, address, access, reset value)
TABLE = [("CTRL", 0, "rw", 0x00), ("STATUS", 1, "w1c", 0x00), ("ID", 2, "ro", 0xA5), ("DATA", 3, "rw", 0x3C)]
def labels(table):
    out = set()
    for name, addr, access, reset in table:
        n = name.lower()
        if access != "ro":
            out.add("a_rst_" + n)                                  # a reset value
        if access == "rw":
            out |= {"a_%s_rw" % n, "a_isolate_%s" % n}              # read back, and no change from other addresses
        if access == "w1c":
            out |= {"a_w1c_done", "a_w1c_err", "a_w1c_zero", "a_hw_set", "a_status_hi"}
        if access == "ro":
            out.add("a_%s_const" % n)                               # the constant on every read
    return out
LISTING = {"a_id_const", "a_status_hi", "a_rst_ctrl", "a_rst_status", "a_rst_data", "a_ctrl_rw", "a_data_rw",
           "a_w1c_done", "a_w1c_err", "a_w1c_zero", "a_hw_set", "a_isolate_ctrl", "a_isolate_data"}
assert labels(TABLE) == LISTING
assert len(LISTING) == 13
grown = TABLE + [("SCRATCH", 4, "rw", 0x00)]     # illustrative extra row
assert labels(grown) - LISTING == {"a_rst_scratch", "a_scratch_rw", "a_isolate_scratch"}, "the check must report the uncovered row"
assert labels(TABLE[:3]) != LISTING, "a table without DATA no longer explains the listing"
print("PASS: the table generates the 13 listed labels and reports a row the listing lacks")

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 = {
    "csr-prove": ("prove", 4, "proved"),
    "csr-cover": ("cover", 4, "reached"),
}
REQUIRED = ["csr-reset-values", "csr-readwrite-and-isolation", "csr-id-and-status-read", "csr-w1c-and-race", "csr-covers"]
MUTANTS = ["csr-W%d" % i for i in range(1, 4)]
REGISTER = {"reset-at-step-0": None}                 # discharged by the pair rows of lesson 3
YOUR_ROWS = []          # fill from your own runs
bad = ledger_ok(YOUR_ROWS, RUNS, REQUIRED, MUTANTS, REGISTER, set(), final=False)
if YOUR_ROWS:
    assert bad == [], bad
    print("PASS: stage 2 register 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))