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 Tick Divider (with a bug)

SystemVerilog Formal Verification

A divide-by-3 tick that comes every 4 cycles. The period property finds the off-by-one wrap.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   a_period: assert property (@(posedge clk) disable iff (rst) tick |=> !tick [*N-1] ##1 tick);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module tick_div #(parameter N = 3) (input clk, input rst, output tick);
  // one-cycle tick every N cycles, e.g. to slow a peripheral down
  reg [3:0] cnt;
  assign tick = (cnt == N - 1);
  always @(posedge clk)
    if (rst)                   cnt <= 4'd0;
    else if (cnt == N)         cnt <= 4'd0;     // bug: should wrap at N - 1
    else                       cnt <= cnt + 4'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // helper: cycles since the last tick (or since reset)
  reg [3:0] gap = 4'd0;
  always @(posedge clk) gap <= (rst || tick) ? 4'd1 : gap + 4'd1;
  // ticks are exactly N cycles apart
  always @(*) if (!init && tick && seen) assert (gap == N);
  // and never more than N cycles apart
  always @(*) if (!init) assert (gap <= N);
  reg seen = 1'b0;
  always @(posedge clk) if (!rst && tick) seen <= 1'b1; else if (rst) seen <= 1'b0;
`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.