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 Magic Value: Left-Over Debug Code

SystemVerilog Formal Verification

An alarm that must never be raised hides behind one 32-bit value; random simulation almost never finds it, formal does in a few cycles.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   assert property (@(posedge clk) disable iff (rst) !alarm);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module alarm_unit (input clk, input rst, input [31:0] data, output reg alarm);
  always @(posedge clk)
    if (rst)                       alarm <= 1'b0;
    else if (data == 32'hDEADBEEF) alarm <= 1'b1;   // left-over debug code

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (!alarm);
`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.