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 Over-Constrained Check (hides a bug)

SystemVerilog Formal Verification

A tracker with an off-by-one limit. An assumption that is too strong makes everything pass; find and remove it.

Open in IDE
design.sv
// SVA form (used by commercial formal tools):
//   m_room:    assume property (@(posedge clk) disable iff (rst) go |-> cnt < 3'd3);   // too strong
//   a_max:     assert property (@(posedge clk) disable iff (rst) cnt <= 3'd3);
//   c_go_full: cover  property (@(posedge clk) disable iff (rst) go && cnt == 3'd3);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module txn3 (input clk, input rst, input go, input resp,
             output req, output [2:0] outstanding);
  // issues read requests to a memory, at most 3 in flight
  reg [2:0] cnt;
  assign outstanding = cnt;
  assign req = go && (cnt <= 3'd3);            // bug: should be cnt < 3
  always @(posedge clk)
    if (rst)               cnt <= 3'd0;
    else if (req && !resp) cnt <= cnt + 3'd1;
    else if (!req && resp) cnt <= cnt - 3'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the memory only responds to a request that is in flight
  always @(*) if (!init) assume (!resp || cnt != 3'd0);
  // OVER-CONSTRAINED: "go only when there is room"
  always @(*) if (!init) assume (!go || cnt < 3'd3);
  // never more than 3 in flight
  always @(posedge clk) if (!init) assert (cnt <= 3'd3);
  // reachability, meant to fail: go while 3 are in flight
  always @(posedge clk) if (!init) assert (!(go && cnt == 3'd3));
`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.