Register Files and Memories

Register files and small memories store data at addresses, so their main rule is simple: a read returns the last value written to that address. Checking it for every address in simulation means a test per address and per pattern. Formal checks every address at once with a tracked address, chosen freely by the tool. This article applies it to a processor register file whose register 0 must always read as zero, and finds that it does not.

8 min read | Intermediate

What You'll Learn

• Check read-after-write for every address with a tracked address
• Write properties for special registers, such as a register hardwired to zero
• Explain why memories without a reset start with arbitrary contents in formal
• Find and fix a zero register that can be written and read

The Tracked Address

The idea is the address version of the tracked value. The tool picks one address ta, constant for the whole run. The formal code remembers the last value written there. Whenever that address is read, the result must be the remembered value. Because the tool may pick any address, a failure for any address is found.

In SVA flows, ta is an undriven signal with an assumption $stable(ta). In the lab, it is declared with (* anyconst *).

The Design: a Register File With x0

In the RISC-V architecture, register x0 always reads as zero, and writes to it are ignored. Compilers rely on it: "add x0 to x5" is how a register copy is written. This 8-register version gets it wrong:

module regfile_x0 (input clk, input we, input [2:0] waddr, input [7:0] wdata,
                   input [2:0] raddr, output [7:0] rdata);
  reg [7:0] x [0:7];
  always @(posedge clk) if (we) x[waddr] <= wdata;     // bug: register 0 is written too
  assign rdata = (raddr == 3'd0) ? x[0] : x[raddr];      // and read back
endmodule

The read multiplexer has a special case for register 0, but it returns the stored register instead of zero, and the write is not blocked either.

The Properties

`ifdef FORMAL
  // register 0 reads as zero
  always @(*) if (raddr == 3'd0) assert (rdata == 8'd0);
  // read after write, with a tracked register
  (* anyconst *) reg [2:0] ta;
  reg [7:0] tv; reg tvalid = 1'b0;
  always @(posedge clk) if (we && waddr == ta) begin tv <= wdata; tvalid <= 1'b1; end
  always @(*) if (tvalid && raddr == ta && ta != 3'd0) assert (rdata == tv);
`endif

In SVA the two rules read:

a_x0:  assert property (@(posedge clk) raddr == 3'd0 |-> rdata == 8'd0);
a_raw: assert property (@(posedge clk) tvalid && raddr == ta && ta != 3'd0 |-> rdata == tv);

The run fails in the very first step: the tool reads register 0 and gets 128. There is no write in the trace at all. The register file has no reset, so in formal every register starts with an arbitrary value, just as in silicon after power-up. Register 0 is a real flip-flop here, so it holds whatever it started with. The rule is broken without any write.

The Fix

always @(posedge clk) if (we && waddr != 3'd0) x[waddr] <= wdata;
assign rdata = (raddr == 3'd0) ? 8'd0 : x[raddr];

Both properties pass. The read-after-write rule passes for every register except 0, which is excluded from it because the zero rule covers it.

Beyond Register Files

The same two techniques cover most storage:

• Single-port and dual-port RAMs: read after write with a tracked address, plus a rule for a read and a write to the same address in the same cycle, as the specification defines it (old data, new data, or undefined).
• Bypass logic in a pipeline: a read in the same cycle as a write to the same register returns the new value.
• Byte enables: track one address and one byte lane.

As the performance article showed, the memory size barely affects run time on the lab engine with this check, so the full-size memory can usually stay in.

Running It in ChipVerify Lab

The example below is the buggy register file with both properties. It fails in step 0.

Common Mistakes