Sequential Equivalence

Some design changes move or replace registers: a state machine re-encoded from binary to one-hot, logic retimed across a register, a pipeline stage added. The two versions no longer have matching registers, so their logic cannot be compared cone by cone. Sequential equivalence compares them over time instead: from reset, with the same inputs, do they produce the same outputs in every cycle? This article checks a traffic light controller against its one-hot re-encoding, finds a bug in the re-encoding, and proves the fixed version equivalent.

9 min read | Intermediate

What You'll Learn

• Explain when combinational equivalence no longer applies
• Build a sequential miter with a shared reset and shared inputs
• Find a difference between two encodings of a state machine
• Prove sequential equivalence with k-induction and with the Yosys equiv flow

When Registers Do Not Match

A binary state machine with three states uses two flip-flops; the same machine one-hot uses three. No register of one corresponds to a register of the other, so a combinational check has nothing to pair. Yet both machines should behave identically on their outputs. The comparison must run over time: start both from reset, apply the same input sequence, and compare outputs cycle by cycle.

That is a property check on a miter with state, exactly the kind of check this tutorial has run since Chapter 2. A bounded check finds differences; a proof needs induction, and often a helper that relates the two state encodings.

The Example: a Traffic Light

A side-road light stays green until a car waits, then goes yellow for one cycle, red for one cycle, and back to green:

module tl_bin (input clk, input rst, input car, output red, output yellow, output 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

The one-hot version writes the next-state logic per flip-flop, and gets the red one wrong:

module tl_onehot (input clk, input rst, input car, output red, output yellow, output green);
  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

The Sequential Miter

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

The run fails at step 4:

A car arrives in step 1, both lights go yellow in step 2 and red in step 3. In step 3 another car waits. The binary version goes back to green, as specified. The one-hot version turns green too, but because of the extra term (r && car) it also keeps red on: two lights at once, and red stuck for as long as cars keep coming. Fix the line to r <= y; and the run passes.

Proving Equivalence

A bounded run shows no difference within its depth. For a proof, SymbiYosys in prove mode tries k-induction on the miter. With k = 1 it returns UNKNOWN: the induction step starts from pairs of states that agree on their outputs in one cycle but are not a real pair, such as one-hot states that no reset can produce. With k = 2 the proof passes, because such state pairs cannot produce matching outputs for two cycles in a row and then diverge.

Yosys has a dedicated flow for the same question. equiv_make pairs the outputs, equiv_simple -seq checks them over a few cycles, and equiv_induct completes the proof by induction:

read_verilog tl_bin.v
read_verilog tl_onehot.v
proc
equiv_make tl_bin tl_onehot equiv
hierarchy -top equiv
equiv_simple -seq 5
equiv_induct
equiv_status

  Of those cells 3 are proven and 0 are unproven.
  Equivalence successfully proven!

Commercial sequential equivalence tools add automatic state mapping for common transformations such as re-encoding and retiming, so that large designs can be proven.

Running It in ChipVerify Lab

The example contains both controllers and the miter, with the bug in the one-hot version. Set the top module to tl_miter and run.

Common Mistakes