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: binary vs one-hot (with a bug)

SystemVerilog Formal Verification

Sequential equivalence of two encodings of the same state machine, with a bug in the one-hot version.

Open in IDE
Related tutorial:
tl_bin.v
module tl_bin (input clk, input rst, input car, output red, output yellow, output green);
  // traffic light for a side road: GREEN -> YELLOW when a car waits, YELLOW -> RED, RED -> GREEN
  localparam G = 2'd0, Y = 2'd1, R = 2'd2;
  reg [1:0] st;
  always @(posedge clk)
    if (rst) st <= G;
    else case (st)
      G: if (car) st <= Y;
      Y:          st <= R;
      R:          st <= G;
      default:    st <= G;
    endcase
  assign green  = (st == G);
  assign yellow = (st == Y);
  assign red    = (st == R);
endmodule
tl_onehot.v
module tl_onehot (input clk, input rst, input car, output red, output yellow, output green);
  // the same controller, re-encoded one-hot: one flip-flop per state
  reg g, y, r;
  always @(posedge clk)
    if (rst) begin g <= 1'b1; y <= 1'b0; r <= 1'b0; end
    else begin
      g <= (g && !car) || r;
      y <= g && car;
      r <= y || (r && car);                    // bug: should be r <= y;
    end
  assign green = g; assign yellow = y; assign red = r;
endmodule
miter.sv
// Sequential miter: shared reset, shared inputs, outputs equal in every cycle.
module tl_miter (input clk, input rst, input car);
  wire r1, y1, g1, r2, y2, g2;
  tl_bin    u_bin (.clk(clk), .rst(rst), .car(car), .red(r1), .yellow(y1), .green(g1));
  tl_onehot u_one (.clk(clk), .rst(rst), .car(car), .red(r2), .yellow(y2), .green(g2));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // both versions start from reset together and see the same inputs: outputs must match
  always @(*) if (!init) assert (r1 == r2 && y1 == y2 && g1 == g2);
`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.