SEC: Sequential Equivalence

Flops with No Partner

Sequential equivalence drops the matched-state assumption. Gold and gate may have different flops, encodings or pipeline depths. The question is now: from reset, for every input sequence, are the outputs equal at every step, or equal after a stated latency?

That is a safety property over time, so it needs the full machinery: BMC for bugs, induction or PDR for the proof.

The Latency Is Part of the Specification

assert property (@(posedge clk) disable iff (rst)
  pipe_valid |-> pipe_sum == $past(gold_sum, 2));

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // modelling code: the gold's {valid, sum}, one and two cycles back
  localparam LAT = 2;
  reg [17:0] gold_q1 = 0, gold_q2 = 0;
  always @(posedge clk) begin
    gold_q1 <= rst ? 18'd0 : {gold_valid, gold_sum};
    gold_q2 <= rst ? 18'd0 : gold_q1;
  end
  wire [17:0] gold_d = LAT == 1 ? gold_q1 : gold_q2;
  always @(posedge clk) if (!rst) begin
    assert(pipe_valid == gold_d[17]);
    if (pipe_valid) assert(pipe_sum == gold_d[16:0]);
  end

The gate's output at step t equals the gold's at step t − 2. Write the latency as 1 and the proof fails at the first valid result: FAIL at reported step 3. Nothing in the design is wrong; the specification was.

Bugs, Then the Proof

BMC found the stale stage at reported step 4. On the fixed pipeline, k-induction (F2.4) fails at k = 2 and closes at k = 3: the latency plus one. With three steps in the window, every pipeline register has been reloaded from inputs the step can see. PDR finds the same proof with no k.

Notice what the miter checks without being told: valid itself must arrive on time, so a stage that drops or doubles a result fails too. If induction ever needs help on a deeper pipeline, the helper is "stage register equals the delayed gold operand" (F4.6).

What Sequential Equivalence Covers

EQY can also try this pair. With no flops to match it compares outputs in the same cycle, and the runner reports UNKNOWN: equivalence not proven. That is the honest result for a pipeline: EQY's partitions assume the outputs line up in time, and here they do not.

Asked in Interviews

Try It

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top sec_top
[files]
design.sv

1. Find the bubble

   Run as loaded: FAIL at reported step 4. Read valid in the trace and name the cycle the operation entered.

2. Fix the stage

   In add_pipe2, make stage 2 load on v1, the stage-1 valid. Run bmc again.

3. Prove it

   Switch to prove. Try depth 2, then 3: UNKNOWN at k = 2 (base case passed, induction step failed), then Prove PASS (k = 3).

4. Break the specification

   Set LAT to 1: FAIL at reported step 3.

module adder(input clk, rst, valid, input [15:0] a, b, output [16:0] sum, output valid_out);
  assign sum = a + b;
  assign valid_out = valid;
endmodule

module adder(input clk, rst, valid, input [15:0] a, b,
  output reg [16:0] sum = 0, output reg valid_out = 0);
  reg [8:0] lo1 = 0;            // stage 1: low bytes added, carry in bit 8
  reg [7:0] ah1 = 0, bh1 = 0;   // stage 1: high bytes, not yet added
  reg v1 = 0;
  wire [8:0] hi = ah1 + bh1 + lo1[8];
  always @(posedge clk) begin
    if (rst) begin v1 <= 0; valid_out <= 0; end
    else begin
      v1 <= valid;
      valid_out <= v1;
      if (valid) begin lo1 <= a[7:0] + b[7:0]; ah1 <= a[15:8]; bh1 <= b[15:8]; end
      if (v1) sum <= {hi, lo1[7:0]};
    end
  end
endmodule

Check Yourself

module add_comb(input [15:0] a, b, input valid, output [16:0] sum, output valid_out);
  assign sum = a + b;
  assign valid_out = valid;
endmodule

module add_pipe2(input clk, rst, valid, input [15:0] a, b,
  output reg [16:0] sum = 0, output reg valid_out = 0);
  reg [8:0] lo1 = 0;            // stage 1: low bytes added, carry in bit 8
  reg [7:0] ah1 = 0, bh1 = 0;   // stage 1: high bytes, not yet added
  reg v1 = 0;
  wire [8:0] hi = ah1 + bh1 + lo1[8];
  always @(posedge clk) begin
    if (rst) begin v1 <= 0; valid_out <= 0; end
    else begin
      v1 <= valid;
      valid_out <= v1;
      if (valid) begin lo1 <= a[7:0] + b[7:0]; ah1 <= a[15:8]; bh1 <= b[15:8]; end
      if (v1) sum <= {hi, lo1[7:0]};
    end
  end
endmodule

module sec_top(input clk, rst, valid, input [15:0] a, b);
  wire [16:0] gold_sum, pipe_sum;
  wire gold_valid, pipe_valid;
  add_comb  gold(.a(a), .b(b), .valid(valid), .sum(gold_sum), .valid_out(gold_valid));
  add_pipe2 pipe(.clk(clk), .rst(rst), .valid(valid), .a(a), .b(b), .sum(pipe_sum), .valid_out(pipe_valid));
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // modelling code: the gold's {valid, sum}, one and two cycles back
  localparam LAT = 1;
  reg [17:0] gold_q1 = 0, gold_q2 = 0;
  always @(posedge clk) begin
    gold_q1 <= rst ? 18'd0 : {gold_valid, gold_sum};
    gold_q2 <= rst ? 18'd0 : gold_q1;
  end
  wire [17:0] gold_d = LAT == 1 ? gold_q1 : gold_q2;
  always @(posedge clk) if (!rst) begin
    assert(pipe_valid == gold_d[17]);
    if (pipe_valid) assert(pipe_sum == gold_d[16:0]);
  end
`endif
endmodule