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 Saturating Counter

SystemVerilog Formal Verification

A counter that stops at 12. Two assertions: never above 12, and stays at 12. Passes; try depth 20 with PRO.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   a_max:  assert property (@(posedge clk) disable iff (rst) q <= 4'd12);
//   a_stay: assert property (@(posedge clk) disable iff (rst) (q == 4'd12) |=> (q == 4'd12));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module sat_counter (input clk, input rst, input en, output reg [3:0] q);
  always @(posedge clk)
    if (rst)                    q <= 4'd0;
    else if (en && q != 4'd12)  q <= q + 4'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // never above 12
  always @(posedge clk) if (!init) assert (q <= 4'd12);
  // once at 12 it stays at 12 (until a reset)
  always @(posedge clk) if (!init && !$past(rst) && $past(q) == 4'd12 && !rst) assert (q == 4'd12);
`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.