Memory and Tracked Entry Abstraction

On this page

Part 3 of 10, lesson 11 of 19Property Development and ConstraintsAll levels

Why it matters

A memory is mostly state the property never reads. Proving read-after-write for one entry stands for all of them, as long as the address is free and the unwritten entries are not read as if they were written. Job of this lesson: a 12-entry, eight-bit memory behind a four-bit address, proved with one tracked entry, and three ways it goes wrong: an address outside the legal range, a lost write at one address, and a read before any write.

The core idea

The tracker holds a free address ta (and a one-cycle-old copy that pins it), a valid bit tv and a shadow word td. A read of the tracked address after the tracked write must return td. The address needs a range constraint because the memory has 12 entries and the address has 16 values: assume (ta < 12) removes four values and is real. On a power-of-two memory, assume (ta <= 4'd15) on a four-bit address would remove none and prove nothing.

Probe	What it shows	Result below
No range assumption	Addresses 12 to 15 ignore a write; the tracker still expects it	False failure at step 3
A lost write at entry 11	A fault at one address, found because the address is free	`a_rd` fails at step 3
Read before any write	The memory is not reset: the content is arbitrary	`a_uninit` fails at step 2; the rule is wrong, not the memory
Covers per region	The proof exercised low, middle and high addresses	Reached within depth 4

Worked example

The helper h_mem (while the entry is followed, the memory holds the shadow) completes the induction step; without it the step fails. First the proof, then the false failure with the range assumption removed:

mem12.sv

// formal: prove 4 expect pass slang top mem12
`define FORMAL
// mem12: 12-entry, 8-bit memory behind a 4-bit address (addresses 12 to 15 do not exist). Writes to them are ignored,
// reads of them return 0. The memory is not reset. Read data is registered: it shows up one cycle after re
// and holds the value from before any write in that same cycle. BUG=1: a write to entry 11 is lost.
// Probes: UNINIT=1 adds a property about reading an entry that was never written; RANGE=0 removes the address range assumption.
module mem12 #(parameter BUG = 0, parameter RANGE = 1, parameter UNINIT = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       we,
  input  wire [3:0] waddr,
  input  wire [7:0] wdata,
  input  wire       re,
  input  wire [3:0] raddr,
  output reg  [7:0] rdata
);
  reg [7:0] mem [0:11];
  always @(posedge clk) begin
    if (we && waddr < 4'd12 && !(BUG == 1 && waddr == 4'd11)) mem[waddr] <= wdata;
    if (re) rdata <= (raddr < 4'd12) ? mem[raddr] : 8'h00;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the tracked entry: one free address, a copy of it one cycle old, a valid bit and one shadow word
  (* anyconst *) wire [3:0] ta;
  reg [3:0] ta_q;
  always @(posedge clk) ta_q <= ta;
  always @(*) if (!init) assume (ta == ta_q);
  generate if (RANGE) begin : g_range
    always @(*) if (!init) assume (ta < 4'd12);              // a real constraint: 12 entries, 4 address bits
  end endgenerate
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle
  always @(posedge clk) begin
    if (rst) begin tv <= 1'b0; chk <= 1'b0; chk0 <= 1'b0; end
    else begin
      if (we && waddr == ta) begin tv <= 1'b1; td <= wdata; end
      chk  <= re && raddr == ta && tv;
      chk0 <= re && raddr == ta && !tv;
      ex   <= td;
    end
  end
  // helper for the induction step: while the entry is followed, the memory really holds the shadow word
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv && ta < 4'd12) h_mem: assert (mem[ta] == td);
  end endgenerate
  always @(*) if (!init && chk) a_rd: assert (rdata == ex);                 // read returns the last write
  generate if (UNINIT) begin : g_u
    always @(*) if (!init && chk0) a_uninit: assert (rdata == 8'h00);       // a read before any write: wrong rule
  end endgenerate
  always @(*) if (!init) begin
    c_rd_lo:  cover (chk && ta < 4'd4);
    c_rd_mid: cover (chk && ta >= 4'd4 && ta < 4'd8);
    c_rd_hi:  cover (chk && ta >= 4'd8);
  end
`endif
endmodule

mem12.sv

// formal: prove 6 expect unproven slang top mem12 define HELPER=0
`define FORMAL
// mem12: 12-entry, 8-bit memory behind a 4-bit address (addresses 12 to 15 do not exist). Writes to them are ignored,
// reads of them return 0. The memory is not reset. Read data is registered: it shows up one cycle after re
// and holds the value from before any write in that same cycle. BUG=1: a write to entry 11 is lost.
// Probes: UNINIT=1 adds a property about reading an entry that was never written; RANGE=0 removes the address range assumption.
module mem12 #(parameter BUG = 0, parameter RANGE = 1, parameter UNINIT = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       we,
  input  wire [3:0] waddr,
  input  wire [7:0] wdata,
  input  wire       re,
  input  wire [3:0] raddr,
  output reg  [7:0] rdata
);
  reg [7:0] mem [0:11];
  always @(posedge clk) begin
    if (we && waddr < 4'd12 && !(BUG == 1 && waddr == 4'd11)) mem[waddr] <= wdata;
    if (re) rdata <= (raddr < 4'd12) ? mem[raddr] : 8'h00;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the tracked entry: one free address, a copy of it one cycle old, a valid bit and one shadow word
  (* anyconst *) wire [3:0] ta;
  reg [3:0] ta_q;
  always @(posedge clk) ta_q <= ta;
  always @(*) if (!init) assume (ta == ta_q);
  generate if (RANGE) begin : g_range
    always @(*) if (!init) assume (ta < 4'd12);              // a real constraint: 12 entries, 4 address bits
  end endgenerate
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle
  always @(posedge clk) begin
    if (rst) begin tv <= 1'b0; chk <= 1'b0; chk0 <= 1'b0; end
    else begin
      if (we && waddr == ta) begin tv <= 1'b1; td <= wdata; end
      chk  <= re && raddr == ta && tv;
      chk0 <= re && raddr == ta && !tv;
      ex   <= td;
    end
  end
  // helper for the induction step: while the entry is followed, the memory really holds the shadow word
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv && ta < 4'd12) h_mem: assert (mem[ta] == td);
  end endgenerate
  always @(*) if (!init && chk) a_rd: assert (rdata == ex);                 // read returns the last write
  generate if (UNINIT) begin : g_u
    always @(*) if (!init && chk0) a_uninit: assert (rdata == 8'h00);       // a read before any write: wrong rule
  end endgenerate
  always @(*) if (!init) begin
    c_rd_lo:  cover (chk && ta < 4'd4);
    c_rd_mid: cover (chk && ta >= 4'd4 && ta < 4'd8);
    c_rd_hi:  cover (chk && ta >= 4'd8);
  end
`endif
endmodule

mem12.sv

// formal: bmc 4 expect fail slang top mem12 define RANGE=0
`define FORMAL
// mem12: 12-entry, 8-bit memory behind a 4-bit address (addresses 12 to 15 do not exist). Writes to them are ignored,
// reads of them return 0. The memory is not reset. Read data is registered: it shows up one cycle after re
// and holds the value from before any write in that same cycle. BUG=1: a write to entry 11 is lost.
// Probes: UNINIT=1 adds a property about reading an entry that was never written; RANGE=0 removes the address range assumption.
module mem12 #(parameter BUG = 0, parameter RANGE = 1, parameter UNINIT = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       we,
  input  wire [3:0] waddr,
  input  wire [7:0] wdata,
  input  wire       re,
  input  wire [3:0] raddr,
  output reg  [7:0] rdata
);
  reg [7:0] mem [0:11];
  always @(posedge clk) begin
    if (we && waddr < 4'd12 && !(BUG == 1 && waddr == 4'd11)) mem[waddr] <= wdata;
    if (re) rdata <= (raddr < 4'd12) ? mem[raddr] : 8'h00;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the tracked entry: one free address, a copy of it one cycle old, a valid bit and one shadow word
  (* anyconst *) wire [3:0] ta;
  reg [3:0] ta_q;
  always @(posedge clk) ta_q <= ta;
  always @(*) if (!init) assume (ta == ta_q);
  generate if (RANGE) begin : g_range
    always @(*) if (!init) assume (ta < 4'd12);              // a real constraint: 12 entries, 4 address bits
  end endgenerate
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle
  always @(posedge clk) begin
    if (rst) begin tv <= 1'b0; chk <= 1'b0; chk0 <= 1'b0; end
    else begin
      if (we && waddr == ta) begin tv <= 1'b1; td <= wdata; end
      chk  <= re && raddr == ta && tv;
      chk0 <= re && raddr == ta && !tv;
      ex   <= td;
    end
  end
  // helper for the induction step: while the entry is followed, the memory really holds the shadow word
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv && ta < 4'd12) h_mem: assert (mem[ta] == td);
  end endgenerate
  always @(*) if (!init && chk) a_rd: assert (rdata == ex);                 // read returns the last write
  generate if (UNINIT) begin : g_u
    always @(*) if (!init && chk0) a_uninit: assert (rdata == 8'h00);       // a read before any write: wrong rule
  end endgenerate
  always @(*) if (!init) begin
    c_rd_lo:  cover (chk && ta < 4'd4);
    c_rd_mid: cover (chk && ta >= 4'd4 && ta < 4'd8);
    c_rd_hi:  cover (chk && ta >= 4'd8);
  end
`endif
endmodule

Step	Inputs	State	What the property sees
1	we 1, waddr 12, wdata 78 (for example)	ta 12	The memory ignores the write; the tracker records 78
2	re 1, raddr 12	-	Read of an address that does not exist
3	-	rdata 0, shadow 78	`a_rd` fails: the read of 12 to 15 returns 0

A real fault, then: a write to entry 11 is lost. It fails at step 3 (depth 3 passes), with ta chosen as 11; the failing property is a_rd itself when the helper is off. Then the uninitialised read: the property "a read before any write returns 0" fails at step 2, whatever the memory does, because its contents are arbitrary:

mem12.sv

// formal: bmc 4 expect fail slang top mem12 define BUG=1 define HELPER=0
`define FORMAL
// mem12: 12-entry, 8-bit memory behind a 4-bit address (addresses 12 to 15 do not exist). Writes to them are ignored,
// reads of them return 0. The memory is not reset. Read data is registered: it shows up one cycle after re
// and holds the value from before any write in that same cycle. BUG=1: a write to entry 11 is lost.
// Probes: UNINIT=1 adds a property about reading an entry that was never written; RANGE=0 removes the address range assumption.
module mem12 #(parameter BUG = 0, parameter RANGE = 1, parameter UNINIT = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       we,
  input  wire [3:0] waddr,
  input  wire [7:0] wdata,
  input  wire       re,
  input  wire [3:0] raddr,
  output reg  [7:0] rdata
);
  reg [7:0] mem [0:11];
  always @(posedge clk) begin
    if (we && waddr < 4'd12 && !(BUG == 1 && waddr == 4'd11)) mem[waddr] <= wdata;
    if (re) rdata <= (raddr < 4'd12) ? mem[raddr] : 8'h00;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the tracked entry: one free address, a copy of it one cycle old, a valid bit and one shadow word
  (* anyconst *) wire [3:0] ta;
  reg [3:0] ta_q;
  always @(posedge clk) ta_q <= ta;
  always @(*) if (!init) assume (ta == ta_q);
  generate if (RANGE) begin : g_range
    always @(*) if (!init) assume (ta < 4'd12);              // a real constraint: 12 entries, 4 address bits
  end endgenerate
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle
  always @(posedge clk) begin
    if (rst) begin tv <= 1'b0; chk <= 1'b0; chk0 <= 1'b0; end
    else begin
      if (we && waddr == ta) begin tv <= 1'b1; td <= wdata; end
      chk  <= re && raddr == ta && tv;
      chk0 <= re && raddr == ta && !tv;
      ex   <= td;
    end
  end
  // helper for the induction step: while the entry is followed, the memory really holds the shadow word
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv && ta < 4'd12) h_mem: assert (mem[ta] == td);
  end endgenerate
  always @(*) if (!init && chk) a_rd: assert (rdata == ex);                 // read returns the last write
  generate if (UNINIT) begin : g_u
    always @(*) if (!init && chk0) a_uninit: assert (rdata == 8'h00);       // a read before any write: wrong rule
  end endgenerate
  always @(*) if (!init) begin
    c_rd_lo:  cover (chk && ta < 4'd4);
    c_rd_mid: cover (chk && ta >= 4'd4 && ta < 4'd8);
    c_rd_hi:  cover (chk && ta >= 4'd8);
  end
`endif
endmodule

mem12.sv

// formal: bmc 3 expect fail slang top mem12 define UNINIT=1
`define FORMAL
// mem12: 12-entry, 8-bit memory behind a 4-bit address (addresses 12 to 15 do not exist). Writes to them are ignored,
// reads of them return 0. The memory is not reset. Read data is registered: it shows up one cycle after re
// and holds the value from before any write in that same cycle. BUG=1: a write to entry 11 is lost.
// Probes: UNINIT=1 adds a property about reading an entry that was never written; RANGE=0 removes the address range assumption.
module mem12 #(parameter BUG = 0, parameter RANGE = 1, parameter UNINIT = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       we,
  input  wire [3:0] waddr,
  input  wire [7:0] wdata,
  input  wire       re,
  input  wire [3:0] raddr,
  output reg  [7:0] rdata
);
  reg [7:0] mem [0:11];
  always @(posedge clk) begin
    if (we && waddr < 4'd12 && !(BUG == 1 && waddr == 4'd11)) mem[waddr] <= wdata;
    if (re) rdata <= (raddr < 4'd12) ? mem[raddr] : 8'h00;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the tracked entry: one free address, a copy of it one cycle old, a valid bit and one shadow word
  (* anyconst *) wire [3:0] ta;
  reg [3:0] ta_q;
  always @(posedge clk) ta_q <= ta;
  always @(*) if (!init) assume (ta == ta_q);
  generate if (RANGE) begin : g_range
    always @(*) if (!init) assume (ta < 4'd12);              // a real constraint: 12 entries, 4 address bits
  end endgenerate
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle
  always @(posedge clk) begin
    if (rst) begin tv <= 1'b0; chk <= 1'b0; chk0 <= 1'b0; end
    else begin
      if (we && waddr == ta) begin tv <= 1'b1; td <= wdata; end
      chk  <= re && raddr == ta && tv;
      chk0 <= re && raddr == ta && !tv;
      ex   <= td;
    end
  end
  // helper for the induction step: while the entry is followed, the memory really holds the shadow word
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv && ta < 4'd12) h_mem: assert (mem[ta] == td);
  end endgenerate
  always @(*) if (!init && chk) a_rd: assert (rdata == ex);                 // read returns the last write
  generate if (UNINIT) begin : g_u
    always @(*) if (!init && chk0) a_uninit: assert (rdata == 8'h00);       // a read before any write: wrong rule
  end endgenerate
  always @(*) if (!init) begin
    c_rd_lo:  cover (chk && ta < 4'd4);
    c_rd_mid: cover (chk && ta >= 4'd4 && ta < 4'd8);
    c_rd_hi:  cover (chk && ta >= 4'd8);
  end
`endif
endmodule

mem12.sv

// formal: cover 4 expect reached slang top mem12
`define FORMAL
// mem12: 12-entry, 8-bit memory behind a 4-bit address (addresses 12 to 15 do not exist). Writes to them are ignored,
// reads of them return 0. The memory is not reset. Read data is registered: it shows up one cycle after re
// and holds the value from before any write in that same cycle. BUG=1: a write to entry 11 is lost.
// Probes: UNINIT=1 adds a property about reading an entry that was never written; RANGE=0 removes the address range assumption.
module mem12 #(parameter BUG = 0, parameter RANGE = 1, parameter UNINIT = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       we,
  input  wire [3:0] waddr,
  input  wire [7:0] wdata,
  input  wire       re,
  input  wire [3:0] raddr,
  output reg  [7:0] rdata
);
  reg [7:0] mem [0:11];
  always @(posedge clk) begin
    if (we && waddr < 4'd12 && !(BUG == 1 && waddr == 4'd11)) mem[waddr] <= wdata;
    if (re) rdata <= (raddr < 4'd12) ? mem[raddr] : 8'h00;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the tracked entry: one free address, a copy of it one cycle old, a valid bit and one shadow word
  (* anyconst *) wire [3:0] ta;
  reg [3:0] ta_q;
  always @(posedge clk) ta_q <= ta;
  always @(*) if (!init) assume (ta == ta_q);
  generate if (RANGE) begin : g_range
    always @(*) if (!init) assume (ta < 4'd12);              // a real constraint: 12 entries, 4 address bits
  end endgenerate
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle
  always @(posedge clk) begin
    if (rst) begin tv <= 1'b0; chk <= 1'b0; chk0 <= 1'b0; end
    else begin
      if (we && waddr == ta) begin tv <= 1'b1; td <= wdata; end
      chk  <= re && raddr == ta && tv;
      chk0 <= re && raddr == ta && !tv;
      ex   <= td;
    end
  end
  // helper for the induction step: while the entry is followed, the memory really holds the shadow word
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv && ta < 4'd12) h_mem: assert (mem[ta] == td);
  end endgenerate
  always @(*) if (!init && chk) a_rd: assert (rdata == ex);                 // read returns the last write
  generate if (UNINIT) begin : g_u
    always @(*) if (!init && chk0) a_uninit: assert (rdata == 8'h00);       // a read before any write: wrong rule
  end endgenerate
  always @(*) if (!init) begin
    c_rd_lo:  cover (chk && ta < 4'd4);
    c_rd_mid: cover (chk && ta >= 4'd4 && ta < 4'd8);
    c_rd_hi:  cover (chk && ta >= 4'd8);
  end
`endif
endmodule

The covers c_rd_lo, c_rd_mid and c_rd_hi are all reached within depth 4 (not within 3). A cover not reached within N is inconclusive, so a region whose cover is missing is a region not exercised.

example.py

import re
SRC = """  reg [7:0] mem [0:11];
  reg init = 1'b1;
  reg [3:0] ta_q;
  reg tv; reg [7:0] td;                                      // the entry has been written; what it should hold
  reg chk, chk0; reg [7:0] ex;                               // a read of the tracked entry happened last cycle"""
def declared(src):
    """Width in bits of every register declared in the text (an array counts all its entries)."""
    regs = {}
    for stmt in re.findall(r"reg\b([^;]*);", src):
        m = re.match(r"\s*(?:\[(\d+):0\])?\s*(.*)", stmt)
        width = int(m.group(1)) + 1 if m.group(1) else 1
        for part in m.group(2).split(","):
            nm = re.match(r"\s*(\w+)(?:\s*\[0:(\d+)\])?", part)
            regs[nm.group(1)] = width * (int(nm.group(2)) + 1 if nm.group(2) else 1)
    return regs
def cost(src):
    r = declared(src)
    return r["mem"], r["ta_q"] + r["tv"] + r["td"], r["chk"] + r["chk0"] + r["ex"]
memory, tracker, check = cost(SRC)
assert (memory, tracker, check) == (96, 13, 10)   # the read data is registered, so the check carries its own flags and word
assert tracker + check < memory
# injected fault: a shadow that keeps a copy of every entry is not an abstraction at all
full = SRC.replace("reg tv; reg [7:0] td;", "reg tv; reg [7:0] td [0:11];")
assert full != SRC
m2, t2, c2 = cost(full)
assert t2 == 101 and not (t2 + c2 < m2)
# a missing register is an error, not a silent zero
try:
    cost(SRC.replace("reg tv;", ""))
    raise SystemExit("FAIL: a missing register was accepted")
except KeyError:
    pass
print("PASS: 96 memory bits are stood for by %d tracker flip-flops (+%d for the registered read check); a full shadow is rejected" % (tracker, check))

What a reviewer looks for

The tracked address is free and constrained to the legal map by an assumption that removes something; a bound that removes nothing is deleted.
Each region of the map has a cover, and a planted fault at the edge entry fails.
Reads before the first write are either excluded by a guard or the memory is reset; no property depends on arbitrary content.

Verify and debug

Read a failing trace for the tracked address first. An address of 12 to 15 means the range assumption is missing, which is what the run without it shows. The address of the planted fault (entry 11, a lost write) is a real failure; it appears at depth 4 and not at depth 3. A read before any write is a wrong property, not a bug: the memory is not reset. Then read the three region covers: a region whose cover is missing is a region the proof never exercised.

Check yourself Why does a read of a never-written entry give a counterexample on a good memory?

The memory is not reset, so the solver picks any content for the entry. The rule that the read returns zero is wrong; reads are checked only after a write.

Navigate

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Memory and Tracked Entry Abstraction

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Up next