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 Counter 0 to 5 (with a bug)

SystemVerilog Formal Verification

A counter that should count from 0 to 5 wraps at 6; the formal check finds it. Fix the wrap value.

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

`ifdef FORMAL
  reg init = 1'b1;                                // high only in the first cycle
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);             // start from a reset
  always @(posedge clk) if (!init) assert (q <= 3'd5);
`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.