A Memory Controller: One Symbolic Address

Check read-after-write for every address with one tracked address, close the proof with buffer invariants, and measure what memory abstraction and data independence buy.

Lesson: F8.6
Time: 20 min
Runs on: SymbiYosys
Check: 4 questions

A memory controller buffered two writes and forwarded them to reads of the same address. The forwarding compare looked at entry 0 only, so a read of the address in entry 1 returned stale memory. Random tests rarely had two different addresses pending at a read. One symbolic address is every address at once, and the trace takes five steps.

The Write Buffer Sits Between the Port and the ArrayWrites enter a two-entry buffer and drain to the array when no read uses the port. A read must see the newest buffered copy of its address. The bench shadows one address the solver picks.

data: where the transaction goes

Read the diagram as text

write port: we, waddr, wdata; wready while entry 1 is free
two-entry buffer: entry 0 oldest, entry 1 newest
16 x 8 array: one port: a commit or a read each cycle
read port: rdata one cycle after re: entry 1, else entry 0, else the array
shadow of f_addr: (* anyconst *) f_addr; f_data = the last write accepted to it

write port → two-entry buffer
two-entry buffer → 16 x 8 array: commit
two-entry buffer → read port: forward
16 x 8 array → read port
write port → shadow of f_addr

The property never looks inside the buffer: a read of f_addr returns f_data. wb_mem has 162 flops, 128 of them the array.

One Row Stands for All

The read of f_addr skips entry 1

Measured with smtbmc yices: FAIL at reported step 5, 0.5 s. The solver chose f_addr = B; any address would do.

The memory spec is one sentence: a read of A returns the last value written to A. The bench picks A as a free constant, keeps one shadow byte, and checks every read of A against it (F4.4). Because A is free, the tool picks the address that fails.

This controller does not merge writes to the same address. Two buffered copies may share an address, and the newer must win, which is why forwarding checks entry 1 first. The trace shows which path the wrong byte took. Entry 1 held the newest write and the buggy compare looked only at entry 0, so the array answered with an old value.

Closing the Proof

Correct wb_mem	Measured result
bmc depth 10	BMC PASS to depth 10, 0.7 s
bmc depth 12	BMC PASS to depth 12, 2.2 s
bmc depth 20	time limit (20 s), no verdict, 20.1 s
prove k = 4, read-after-write only	UNKNOWN at k = 4 (base case passed, induction step failed), 0.5 s
prove k = 2, plus four buffer invariants	Prove PASS (k = 2), 0.5 s
`abc pdr`, read-after-write only	time limit (20 s), no verdict, 20.1 s
`abc pdr` with a 60 s allowance	Prove PASS (abc pdr), 20.9 s

smtbmc yices unless noted. The array makes every bounded step expensive.

The invariants say what the buffer already does. Entries fill in order; the newest buffered copy of f_addr equals the shadow; with no copy buffered, the array row equals the shadow. With them, k-induction closes at k = 2 in half a second. PDR finds its own invariant, but here it needs about twenty seconds.

Abstraction and Data Width

Model	Flops	`abc pdr`	With the invariants, prove k = 2	BUG_FWD0, bmc 20
16 x 8 array, 8-bit data	162	Prove PASS (abc pdr), 20.9 s	Prove PASS (k = 2), 0.5 s	FAIL at reported step 5
One tracked row, a free value for any other address	42 (by construction)	Prove PASS (abc pdr), 8.2 s	Prove PASS (k = 2), 0.5 s	FAIL at reported step 5
16 x 2 array, 2-bit data	48	Prove PASS (abc pdr), 3.6 s	Prove PASS (k = 2), 0.5 s	-

The one-row model may return anything for addresses other than f_addr, so it over-approximates the array: a PASS carries over, and it still finds the bug.

Memory abstraction (F4.5) keeps the one row the property reads. Data independence keeps the control: no decision in this controller reads the data, so a proof at two bits is a proof at eight. Both cut the PDR time here.

Asked in Interviews

Question	Answer
What is a symbolic address?	One free-constant address followed through the design with a shadow of its value. The proof covers every address.
How is a memory abstracted?	Keep the tracked row and return a free value for every other address, or let the solver keep arrays uninterpreted.
Why can you narrow the data width?	Data independence: no control decision reads the data, so the control proof is the same at any width.

Try It

The lab task. The twins run the covers, the proofs and the two smaller models.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top wb_mem
[files]
design.sv

The property, one invariant and one cover in concurrent SVA.

(* anyconst *) reg [3:0] f_addr;
assert property (@(posedge clk) disable iff (rst) re && raddr == f_addr && f_valid |=> rdata == $past(f_data));
assert property (@(posedge clk) disable iff (rst) v1 |-> v0);
cover property (@(posedge clk) disable iff (rst) re && raddr == f_addr && hit1 && !hit0);

As the engine runs it.

  (* anyconst *) reg [3:0] f_addr;        // the tracked address: the solver picks it

Covers
A read served by entry 1 at step 4; a read from the array with the buffer full at step 5.
The bug
Run as loaded: FAIL at reported step 5. Walk back from the wrong rdata to the forwarding compare.
Prove
Fix the compare, then run prove at k = 4 without invariants and at k = 2 with them.
Data width
Run the 2-bit twin with abc pdr: 3.6 s. Write the one-line data-independence note.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module wb_mem #(parameter W = 8)(input clk, rst, we, input [3:0] waddr, input [W-1:0] wdata,
  input re, input [3:0] raddr, output wready, output reg [W-1:0] rdata = 0);
`ifdef FORMAL
  (* anyconst *) reg [3:0] f_addr;        // the tracked address: the solver picks it
`endif
  reg v0 = 0, v1 = 0;                     // entry 0 is the oldest
  reg [3:0] a0 = 0, a1 = 0;
  reg [W-1:0] d0 = 0, d1 = 0;
  assign wready = !v1;
  wire acc = we && wready;                // a write is accepted
  wire commit = v0 && !re;                // the array port is free: entry 0 goes to the array
  reg [W-1:0] mem [0:15];
  wire [W-1:0] arr_rd = mem[raddr];
  always @(posedge clk) if (commit) mem[a0] <= d0;
  wire hit1 = v1 && a1 == raddr, hit0 = v0 && a0 == raddr;
  always @(posedge clk) begin
    if (re) rdata <= hit0 ? d0 : arr_rd;   // bug: entry 1 is never checked
    if (rst) begin v0 <= 0; v1 <= 0; end
    else if (commit) begin                // entry 1 moves up; an accepted write fills the free slot
      v0 <= v1 || acc; a0 <= v1 ? a1 : waddr; d0 <= v1 ? d1 : wdata;
      v1 <= v1 && acc; a1 <= waddr; d1 <= wdata;
    end else if (acc) begin
      if (!v0) begin v0 <= 1; a0 <= waddr; d0 <= wdata; end
      else begin v1 <= 1; a1 <= waddr; d1 <= wdata; end
    end
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // The shadow: the last value accepted for the tracked address.
  reg f_valid = 0, f_chk = 0;
  reg [W-1:0] f_data = 0, f_exp = 0;
  always @(posedge clk) begin
    if (rst) f_valid <= 0;
    else if (acc && waddr == f_addr) begin f_valid <= 1; f_data <= wdata; end
    f_chk <= !rst && re && raddr == f_addr && f_valid;
    f_exp <= f_data;
  end
  always @(posedge clk) if (!rst) begin
    if (f_chk) assert(rdata == f_exp);    // a read returns the last write to its address
  end
`endif
endmodule

Check Yourself

Predict the outputwb_mem with BUG_FWD0, mode bmc, default depth 20, smtbmc yices, reset assumed in step 0, the read-after-write property with one free-constant address. The verdict is:

module wb_mem #(parameter W = 8)(input clk, rst, we, input [3:0] waddr, input [W-1:0] wdata,
  input re, input [3:0] raddr, output wready, output reg [W-1:0] rdata = 0);
`ifdef FORMAL
  (* anyconst *) reg [3:0] f_addr;        // the tracked address: the solver picks it
`endif
  reg v0 = 0, v1 = 0;                     // entry 0 is the oldest
  reg [3:0] a0 = 0, a1 = 0;
  reg [W-1:0] d0 = 0, d1 = 0;
  assign wready = !v1;
  wire acc = we && wready;                // a write is accepted
  wire commit = v0 && !re;                // the array port is free: entry 0 goes to the array
  reg [W-1:0] mem [0:15];
  wire [W-1:0] arr_rd = mem[raddr];
  always @(posedge clk) if (commit) mem[a0] <= d0;
  wire hit1 = v1 && a1 == raddr, hit0 = v0 && a0 == raddr;
  always @(posedge clk) begin
    if (re) rdata <= hit0 ? d0 : arr_rd;   // bug: entry 1 is never checked
    if (rst) begin v0 <= 0; v1 <= 0; end
    else if (commit) begin                // entry 1 moves up; an accepted write fills the free slot
      v0 <= v1 || acc; a0 <= v1 ? a1 : waddr; d0 <= v1 ? d1 : wdata;
      v1 <= v1 && acc; a1 <= waddr; d1 <= wdata;
    end else if (acc) begin
      if (!v0) begin v0 <= 1; a0 <= waddr; d0 <= wdata; end
      else begin v1 <= 1; a1 <= waddr; d1 <= wdata; end
    end
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // The shadow: the last value accepted for the tracked address.
  reg f_valid = 0, f_chk = 0;
  reg [W-1:0] f_data = 0, f_exp = 0;
  always @(posedge clk) begin
    if (rst) f_valid <= 0;
    else if (acc && waddr == f_addr) begin f_valid <= 1; f_data <= wdata; end
    f_chk <= !rst && re && raddr == f_addr && f_valid;
    f_exp <= f_data;
  end
  always @(posedge clk) if (!rst) begin
    if (f_chk) assert(rdata == f_exp);    // a read returns the last write to its address
  end
`endif
endmodule

ConceptWhich modelling line is wrong?

(* anyconst *) reg [3:0] f_addr;(* anyseq *) reg [3:0] f_addr;if (f_chk) assert(rdata == f_exp);if (acc && waddr == f_addr) f_data <= wdata;

ConceptWhat is data independence, and what does it let you do here?

The tool ignores data bits in every property it is given.It only applies to FIFOs, where data never changes.No control decision reads the data, so a 2-bit proof covers 8 bits.The address can be left free, so any address is checked.

Read the waveformIn the BUG_FWD0 trace, where was the write to f_addr held at the read, and where did rdata come from?

The read of f_addr skips entry 1

Measured with smtbmc yices: FAIL at reported step 5, 0.5 s. The solver chose f_addr = B; any address would do.

Entry 0; the forwarding pathNowhere; the shadow flopEntry 1; the forwarding pathEntry 1; the array, stale

Remember

One free-constant address and one shadow byte check read-after-write for every address.
The property watches the ports; the trace shows which internal path carried the wrong data.
Buffer invariants close k-induction at k = 2; PDR needs no help but more time.
A one-row memory model over-approximates soundly; data independence lets you narrow the width.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.