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: the induction step

SystemVerilog Formal Verification

The induction step for q <= 9 with K = 1, run in the lab. Change the property to q != 11 to see a false step failure.

Open in IDE
design.sv
// Induction step written as a bounded check: no reset, the property assumed for K steps and asserted in step K.
// Run at depth 2 or more.
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
  // induction step in the lab: start anywhere, never reset
  always @(*) assume (!rst);
  reg [7:0] step = 8'd0;
  always @(posedge clk) step <= step + 8'd1;
  // the properties hold in the first K steps ...
  always @(*) if (step < 8'd1) assume (q <= 4'd9);
  // ... and must still hold in step K
  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.