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 APB Register Block (with a bug)

SystemVerilog Formal Verification

A write to the read-only ID register at 0xC also lands in the scratch register. Found with read-after-write.

Open in IDE
design.sv
// SVA form of the master rules (assumptions) used by commercial formal tools:
//   m_access: assume property (@(posedge clk) disable iff (rst) psel && !penable |=> psel && penable);
//   m_stable: assume property (@(posedge clk) disable iff (rst) psel && !penable |=> $stable(paddr) && $stable(pwrite) && $stable(pwdata));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module apb_regs (input clk, input rst,
                 input psel, input penable, input pwrite, input [3:0] paddr, input [7:0] pwdata,
                 output reg [7:0] prdata, output pready, output [7:0] ctrl);
  // registers at 0x0 (ctrl), 0x4 (data), 0x8 (scratch); 0xC is a read-only ID register = 8'hA5
  reg [7:0] r0, r1, r2;
  assign pready = 1'b1;                                  // no wait states
  assign ctrl = r0;
  wire wr = psel && penable && pwrite;
  always @(posedge clk)
    if (rst) begin
      r0 <= 8'd0; r1 <= 8'd0; r2 <= 8'd0;
    end else if (wr)
      case (paddr[3:2])
        2'd0: r0 <= pwdata;
        2'd1: r1 <= pwdata;
        default: r2 <= pwdata;                           // bug: a write to 0xC also lands in r2
      endcase
  always @(*)
    case (paddr[3:2])
      2'd0: prdata = r0;
      2'd1: prdata = r1;
      2'd2: prdata = r2;
      default: prdata = 8'hA5;
    endcase

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // APB master rules (assumptions): setup phase then access phase, signals stable in between
  always @(posedge clk) if (!init && !$past(rst) && $past(psel && !penable)) assume (psel && penable);
  always @(posedge clk) if (!init && !$past(rst) && $past(psel && !penable))
    assume (paddr == $past(paddr) && pwrite == $past(pwrite) && pwdata == $past(pwdata));
  always @(posedge clk) if (!init && !$past(rst) && $past(psel && penable)) assume (!penable);
  always @(*) if (!psel) assume (!penable);
  always @(posedge clk) if (!init && penable) assume ($past(psel && !penable) && !$past(rst));
  always @(*) if (init) assume (!psel);
  always @(*) assume (paddr[1:0] == 2'b00);             // word-aligned addresses
  // the ID register always reads A5
  always @(*) if (!init && psel && paddr[3:2] == 2'd3) assert (prdata == 8'hA5);
  // read after write for a tracked register address
  (* anyconst *) reg [1:0] ta;
  reg [7:0] tv; reg tvalid = 1'b0;
  always @(posedge clk) if (rst) tvalid <= 1'b0; else if (wr && paddr[3:2] == ta) begin tv <= pwdata; tvalid <= 1'b1; end
  always @(*) if (!init && tvalid && ta != 2'd3 && psel && penable && !pwrite && paddr[3:2] == ta) assert (prdata == 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.