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 Sticky Error Flag (with a bug)

SystemVerilog Formal Verification

An error flag that should stay set until cleared but forgets the error. Checked with $past, $rose and $fell.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   a_hold: assert property (@(posedge clk) disable iff (rst) flag && !clr |=> flag);
//   a_rise: assert property (@(posedge clk) disable iff (rst) $rose(flag) |-> $past(err));
//   a_fall: assert property (@(posedge clk) disable iff (rst) $fell(flag) |-> $past(clr));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module sticky (input clk, input rst, input err, input clr, output reg flag);
  // error flag: set by err, stays set until clr
  always @(posedge clk)
    if (rst)      flag <= 1'b0;
    else if (clr) flag <= 1'b0;
    else          flag <= err;                    // bug: should be "else if (err) flag <= 1'b1;"

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // once set, it stays set until clr or rst
  always @(posedge clk) if (!init && $past(flag) && !$past(clr) && !$past(rst)) assert (flag);
  // it only rises after an err
  always @(posedge clk) if (!init && $rose(flag)) assert ($past(err));
  // it only falls after clr or rst
  always @(posedge clk) if (!init && $fell(flag)) assert ($past(clr) || $past(rst));
`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.