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 Lockstep Counters: strengthened

SystemVerilog Formal Verification

The induction step with the helper invariant a == b passes with K = 1.

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.
// K = 1: run at depth 2 or more.
// SVA: a_same: assert property (@(posedge clk) disable iff (rst) a == b);   // helper
module lockstep (input clk, input rst, input en, output done_a, output done_b);
  // two copies of the same counter, as in a lockstep safety design
  reg [3:0] a, b;
  always @(posedge clk)
    if (rst) begin
      a <= 4'd0; b <= 4'd0;
    end else if (en) begin
      a <= (a == 4'd9) ? 4'd0 : a + 4'd1;
      b <= (b == 4'd9) ? 4'd0 : b + 4'd1;
    end
  assign done_a = (a == 4'd9);
  assign done_b = (b == 4'd9);

`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 (done_a == done_b && a == b);
  // ... and must still hold in step K
  always @(*) if (step == 8'd1) assert (done_a == done_b && a == b);
`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.