Equivalence Checking vs Property Checking: Differences and Examples

Equivalence checking proves that two versions of the same design behave identically, for example RTL against the gate-level netlist produced by synthesis. Property checking proves that one design satisfies a set of properties written from the specification, such as "two grants are never active together". Both are formal methods that cover all input values without test vectors, but equivalence checking needs a trusted reference design, while property checking needs well-written properties.

Equivalence checking and property checking are two important techniques for verifying the correctness of hardware designs. In this post I explain the difference between them, with examples that you can run.

Key takeaways

• Equivalence checking compares two models of the same design; property checking compares one model against a set of properties.
• Equivalence checking is the standard sign-off step after synthesis, scan insertion, optimisation and functional ECOs.
• Property checking (model checking) is used to prove control logic, protocols, arbiters and safety rules, often with SystemVerilog Assertions (SVA).
• Neither replaces simulation completely; they are complementary, and most chip projects use all three.

Equivalence checking

Equivalence checking is part of the larger discipline called formal verification. It uses mathematical techniques to prove that two representations of a design exhibit the same behaviour. It is a way of comparing two different representations of the same design, such as a register-transfer level (RTL) description and a gate-level implementation, and proving that they are functionally equivalent.

It should not be confused with functional verification by simulation. Simulation checks the design against chosen input vectors, so it is only exhaustive for very small designs; a 64-bit adder already has 2¹²⁸ input pairs. Equivalence checking needs no input vectors, which is why it is so efficient for its job.

Once a verified version of a design exists, equivalence checking can show whether an alternate representation behaves the same as the verified version. It is used to confirm that a design's function has not changed after an operation such as synthesis, or after a functional ECO (engineering change order) has been applied.

How it works

• Combinational equivalence (the common case): the tool matches registers between the two designs (key points), then proves that the logic cones feeding each matched register and output are identical, using BDDs or SAT solvers.
• Sequential equivalence: when register mapping changes, for example after retiming or clock gating, the tool must reason over several clock cycles. This is harder and slower.

Example: a small adder

Suppose we have a design that adds two 4-bit numbers and we want to confirm that the netlist matches the RTL. The RTL is the reference; the netlist is the implementation. If the checker proves the two produce the same output for every possible input, the implementation has not changed the function.

The original version of this example declared a 4-bit sum, which drops the carry: 15 + 1 gives 0. Below the sum is 5 bits wide. The second module is a hand-written ripple-carry adder standing in for a synthesised netlist.

module adder (input [3:0] a, b, output [4:0] sum);
  assign sum = a + b;
endmodule

// Gate-level ripple-carry version, standing in for a netlist
module adder_gates (input [3:0] a, b, output [4:0] sum);
  wire [4:0] c;
  assign c[0] = 1'b0;
  genvar i;
  generate for (i = 0; i < 4; i = i + 1) begin : fa
    assign sum[i] = a[i] ^ b[i] ^ c[i];
    assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i]));
  end endgenerate
  assign sum[4] = c[4];
endmodule

module adder_tb;
  reg  [3:0] a, b;
  wire [4:0] s_rtl, s_gate;
  integer i, errors;
  adder       u_rtl  (.a(a), .b(b), .sum(s_rtl));
  adder_gates u_gate (.a(a), .b(b), .sum(s_gate));
  initial begin
    errors = 0;
    for (i = 0; i < 256; i = i + 1) begin
      {a, b} = i;
      #1;
      if (s_rtl !== s_gate) errors = errors + 1;
    end
    $display("compared 256 input pairs, mismatches = %0d", errors);
    $finish;
  end
endmodule

For four bits a simulator can try all 256 input pairs, and this testbench reports zero mismatches. That is exactly what an equivalence checker proves, but without enumerating inputs, so the same proof works for a 64-bit adder where enumeration is impossible. In a real flow you would load the RTL and the netlist into a tool such as Synopsys Formality, Cadence Conformal or the open-source Yosys equivalence commands.

Property checking

Property checking verifies that a design satisfies certain properties taken from its specification. Properties are usually grouped as:

• Safety: something bad never happens, for example "the light is never green in both directions at the same time".
• Liveness: something good eventually happens, for example "a request is eventually granted".
• Bounded response: something happens within a time limit, for example "the light changes from red to green within at most 10 seconds".

For a traffic light controller we would express these requirements as logical formulas, then use a property checker (model checker) to check whether the design satisfies them for every reachable state and input sequence. If the checker proves all properties, the design meets those requirements. If not, it returns a counter-example trace that shows exactly how a property fails, which is often the most useful output.

The quality of the result depends on the properties. A design can pass every property and still be wrong if an important requirement was never written down, which is why property sets are reviewed against the specification.

Example: a 4-bit counter

Here is a simple 4-bit counter that increments on every clock after reset:

module counter (input clk, reset, output reg [3:0] count);
  always @(posedge clk) begin
    if (reset) count <= 4'b0000;
    else       count <= count + 1'b1;
  end
endmodule

The properties we want are "reset clears the count" and "out of reset, every clock adds one, wrapping from 15 to 0". In SystemVerilog Assertions, which formal tools read directly, they look like this:

module counter_props (input clk, reset, input [3:0] count);
  // Reset clears the count on the next clock
  a_reset: assert property (@(posedge clk) reset |=> count == 4'd0);

  // Out of reset, each clock adds one (wraps 15 to 0)
  a_increment: assert property (@(posedge clk) disable iff (reset)
                 !$past(reset) |-> count == $past(count) + 4'd1);
endmodule

// Attach to the design without editing it
bind counter counter_props u_props (.clk(clk), .reset(reset), .count(count));

A model checker proves these for all input sequences. The same idea can be tried in a plain simulator with an immediate assertion:

module counter_tb;
  reg clk = 1'b0, reset = 1'b1;
  wire [3:0] count;
  reg  [3:0] prev_count;
  reg        prev_reset = 1'b1;
  counter dut (.clk(clk), .reset(reset), .count(count));
  always #5 clk = ~clk;

  // Check: out of reset, every clock adds one to count (wrapping 15 to 0)
  always @(posedge clk) begin
    #1;
    if (!reset && !prev_reset)
      assert (count == prev_count + 4'd1)
        else $error("count did not increment: %0d -> %0d", prev_count, count);
    prev_count = count;
    prev_reset = reset;
  end

  initial begin
    #12 reset = 1'b0;
    repeat (20) @(posedge clk);
    #2 $display("count = %0d after 20 clocks out of reset", count);
    $finish;
  end
endmodule

This runs with no assertion failures and prints a count of 4, because 20 clocks wrap the 4-bit counter once (20 mod 16 = 4).

Two fixes from the original version of this example. First, $assert is not a SystemVerilog task; the keyword is assert. Second, the original check expected the count to be 15 at time 210, but with reset released at time 10 and a 10-unit clock, 20 clock edges have passed by then and the counter reads 4, so the check would fail. A property that describes the behaviour on every cycle is both correct and far stronger than a single check at one moment.

Side by side

Aspect	Equivalence checking	Property checking
Compares	Two models of the same design	One model against properties
Needs	A trusted reference (often the RTL)	Properties written from the specification
Typical use	RTL vs netlist after synthesis, scan, ECO, optimisation	Control logic, protocols, arbiters, FIFOs, safety rules
Main limit	Says nothing if the reference is wrong	Only as good as the properties; state explosion on large blocks
Output on failure	Non-equivalent points and a distinguishing input	Counter-example trace

The main difference is that equivalence checking compares two models of the same design, while property checking compares one model with a set of properties. Equivalence checking is useful when we have a reference model that we trust and want to ensure that our implementation matches it. Property checking is useful when we have requirements to verify and no reference model. Both techniques are complementary and can be used together to reach high confidence in a hardware design.

Common mistakes

• Treating a passed equivalence check as proof the design is correct: it only proves the netlist matches the RTL, bugs included.
• Writing properties that are trivially true (vacuous), for example an implication whose trigger can never occur; check cover properties too.
• Over-constraining inputs with assumptions so that real failures are hidden.
• Running combinational equivalence on a retimed design and chasing false mismatches; it needs sequential equivalence.

FAQ

Is equivalence checking formal verification?

Yes. It is the most widely used formal method in chip design, run on almost every synthesised block.

Can property checking replace simulation?

For some blocks it gives full proof, but large data-path designs often hit state-space limits. Most teams combine formal proofs on control logic with simulation for the full chip.

Do I need a formal tool to use assertions?

No. The same SVA properties can run in a simulator, where they check only the cycles you simulate. A formal tool proves them for all cycles.