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 Traffic Light: Reachable States

SystemVerilog Formal Verification

A 2-bit state machine with three states; prove that the unused encoding 11 is never reached from reset.

Open in IDE
design.sv
// SVA form of the property (used by commercial formal tools):
//   assert property (@(posedge clk) disable iff (rst) state != 2'b11);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module traffic (input clk, input rst, input tick, output reg [1:0] state);
  localparam RED = 2'd0, GREEN = 2'd1, YELLOW = 2'd2;
  always @(posedge clk)
    if (rst) state <= RED;
    else if (tick)
      case (state)
        RED:     state <= GREEN;
        GREEN:   state <= YELLOW;
        YELLOW:  state <= RED;
        default: state <= RED;
      endcase

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