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 Watchdog: a deep bug

SystemVerilog Formal Verification

A watchdog that wraps after 1023 cycles. Passes at depth 100 from reset; start anywhere to find it in two steps.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   a_hold: assert property (@(posedge clk) disable iff (rst) tout && !kick |=> tout);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module timeout (input clk, input rst, input kick, output tout);
  // watchdog: tout goes high after 1000 cycles without a kick and stays high until a kick
  reg [9:0] cnt;
  assign tout = (cnt >= 10'd1000);
  always @(posedge clk)
    if (rst || kick) cnt <= 10'd0;
    else             cnt <= cnt + 10'd1;   // bug: keeps counting and wraps after 1023

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  // start from reset: the bug is more than 1000 cycles away
  always @(*) if (init) assume (rst);
  // once tout is high, it stays high until a kick or reset
  always @(posedge clk) if (!init && !$past(rst) && $past(tout) && !$past(kick)) assert (tout);
`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.