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 Decimal Counter: bounded pass or proof?

SystemVerilog Formal Verification

A mod-10 counter with the rule q <= 9. The normal run is the base case; the induction step is included as a comment.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   a_digit: assert property (@(posedge clk) disable iff (rst) q <= 4'd9);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module mod10 (input clk, input rst, input en, output reg [3:0] q);
  // decimal digit counter: 0, 1, ..., 9, 0, ...
  always @(posedge clk)
    if (rst)     q <= 4'd0;
    else if (en) q <= (q == 4'd9) ? 4'd0 : q + 4'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) assert (q <= 4'd9);

  // The induction step, in a form the lab can run (see the article "Proofs in Practice"):
  // replace the three lines of the reset block above with these and run at depth 2.
  //   always @(*) assume (!rst);
  //   reg [7:0] step = 8'd0;
  //   always @(posedge clk) step <= step + 8'd1;
  //   always @(*) if (step < 8'd1) assume (q <= 4'd9);
  //   always @(*) if (step == 8'd1) assert (q <= 4'd9);
`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.