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 Mod-60 Counter: a deep bug

SystemVerilog Formal Verification

The bug needs 62 cycles to show. Passes at depth 10, fails at depth 63 (PRO). Scale it down with a parameter to find it on the free tier.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   a_60: assert property (@(posedge clk) disable iff (rst) q <= 6'd59);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module mod60 (input clk, input rst, input en, output reg [5:0] q);
  always @(posedge clk)
    if (rst)     q <= 6'd0;
    else if (en) q <= (q == 6'd60) ? 6'd0 : q + 6'd1;   // bug: should wrap at 59

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