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 Pulse Timer: assert, assume, cover

SystemVerilog Formal Verification

A timer that is busy for 3 cycles. Passes with the assumption "no start while busy"; remove it to see the counterexample.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   m_start: assume property (@(posedge clk) disable iff (rst) busy |-> !start);
//   a_run:   assert property (@(posedge clk) disable iff (rst) not (busy [*4]));
//   c_end:   cover  property (@(posedge clk) disable iff (rst) busy ##1 !busy);
// The open-source engine in ChipVerify Lab reads the equivalent block below. The lab panel runs the assertion check; the cover is used in cover mode.
module pulse_timer (input clk, input rst, input start, output busy);
  reg [1:0] cnt;
  assign busy = (cnt != 2'd0);
  always @(posedge clk)
    if (rst)             cnt <= 2'd0;
    else if (start)      cnt <= 2'd3;
    else if (cnt != 0)   cnt <= cnt - 2'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // assumption: no new start while the timer is busy
  always @(*) if (!init && busy) assume (!start);
  // busy is never high for more than 3 cycles in a row
  reg [2:0] run = 3'd0;
  always @(posedge clk) run <= (busy && !rst) ? run + 3'd1 : 3'd0;
  always @(posedge clk) if (!init) assert (run <= 3'd3);
  // the end of a busy period can be reached
  always @(posedge clk) if (!init && !$past(rst)) cover ($past(busy) && !busy);
`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.