Lesson 8.4 · Formal Equivalence Verification

RTL-to-RTL equivalence

Designers constantly change RTL in ways that should not change behaviour: cleaning up code, fixing timing, adding clock gating, changing parameters. Instead of re-running the full regression and hoping it notices, you can prove the new version equivalent to the old one.

Combinational refactoring: a priority encoder

prio_enc_v1.sv

// prio_enc_v1.sv — original: explicit casez
module prio_enc_v1 (
  input  logic [7:0] req,
  output logic [2:0] idx,     // index of the LOWEST set bit
  output logic       any
);
  always_comb begin
    casez (req)
      8'b???????1: idx = 3'd0;
      8'b??????10: idx = 3'd1;
      8'b?????100: idx = 3'd2;
      8'b????1000: idx = 3'd3;
      8'b???10000: idx = 3'd4;
      8'b??100000: idx = 3'd5;
      8'b?1000000: idx = 3'd6;
      8'b10000000: idx = 3'd7;
      default:     idx = 3'd0;
    endcase
  end
  assign any = |req;
endmodule

prio_enc_v2.sv

// prio_enc_v2.sv — refactored: compact loop
module prio_enc_v2 (
  input  logic [7:0] req,
  output logic [2:0] idx,
  output logic       any
);
  always_comb begin
    idx = 3'd0;
    for (int i = 7; i >= 0; i--)      // last match wins -> lowest index
      if (req[i]) idx = 3'(i);
  end
  assign any = |req;
endmodule

prio_enc_eq.sv

// prio_enc_eq.sv — miter: both versions, same inputs, outputs must match
module prio_enc_eq (input logic [7:0] req);
  logic [2:0] idx1, idx2;
  logic       any1, any2;

  prio_enc_v1 u_ref (.req, .idx(idx1), .any(any1));
  prio_enc_v2 u_imp (.req, .idx(idx2), .any(any2));

  always_comb begin
    a_idx_eq: assert (idx1 == idx2);
    a_any_eq: assert (any1 == any2);
  end
endmodule

Sequential change: retiming a register

To fix timing, a designer moves a register from the output of an adder to its inputs. The flops are now different (two 8-bit input registers instead of one 9-bit output register), so combinational FEV cannot map them — but the input/output behaviour is unchanged. This needs sequential equivalence: both designs start from reset, and the outputs must match on every cycle.

adder_retime.sv

// adder_retime.sv — two versions of a registered adder
module adder_reg_out (                       // original: register after the adder
  input  logic       clk, rst,
  input  logic [7:0] a, b,
  output logic [8:0] sum
);
  always_ff @(posedge clk)
    if (rst) sum <= '0;
    else     sum <= a + b;
endmodule

module adder_reg_in (                        // retimed: registers before the adder
  input  logic       clk, rst,
  input  logic [7:0] a, b,
  output logic [8:0] sum
);
  logic [7:0] a_q, b_q;
  always_ff @(posedge clk)
    if (rst) begin a_q <= '0; b_q <= '0; end
    else     begin a_q <= a;  b_q <= b;  end
  assign sum = a_q + b_q;
endmodule

adder_seq_eq.sv

// adder_seq_eq.sv — sequential equivalence miter
module adder_seq_eq (
  input logic       clk, rst,
  input logic [7:0] a, b
);
  logic [8:0] sum_ref, sum_imp;
  adder_reg_out u_ref (.clk, .rst, .a, .b, .sum(sum_ref));
  adder_reg_in  u_imp (.clk, .rst, .a, .b, .sum(sum_imp));

  initial assume (rst);
  a_seq_equiv: assert property (@(posedge clk) disable iff (rst) sum_ref == sum_imp);
endmodule

Note the reset value: 0 + 0 = 0, so both versions agree right after reset. If the retimed version had reset its input registers to, say, 1, the miter would fail in the first cycle — a classic retiming bug that only sequential equivalence catches.