Ready-to-run snippets

Code Examples

Ready-to-run Verilog, SystemVerilog, and UVM examples. Click any to open it live in the IDE.

← All examples

FV Register File with x0 (with a bug)

SystemVerilog Formal Verification

Register 0 should always read as zero, but it is a real register. Read-after-write is checked with a tracked register.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   a_x0: assert property (@(posedge clk) raddr == 3'd0 |-> rdata == 8'd0);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module regfile_x0 (input clk, input we, input [2:0] waddr, input [7:0] wdata,
                   input [2:0] raddr, output [7:0] rdata);
  // 8 registers; register 0 always reads as zero (as in RISC-V)
  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

`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
endmodule
Admin mode — edit and delete controls are visible on each row. Use the IDE to add new snippets via File → Save as Snippet.