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 LFSR: distance from reset

SystemVerilog Formal Verification

A 16-bit LFSR that never reaches zero. Change the asserted value to measure how many cycles a state is from reset.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   a_nonzero: assert property (@(posedge clk) disable iff (rst) s != 16'h0000);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module lfsr16 (input clk, input rst, input en, output reg [15:0] s);
  // 16-bit maximal-length LFSR (taps 16, 14, 13, 11); never reaches the all-zero state
  wire fb = s[15] ^ s[13] ^ s[12] ^ s[10];
  always @(posedge clk)
    if (rst)     s <= 16'h0001;
    else if (en) s <= {s[14:0], fb};

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (s != 16'h0000);
`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.