Equivalence checking Vs Property Checking

Equivalence checking and property checking are two important techniques for verifying the correctness of hardware designs. In this blog post, we will explain the difference between them.

Equivalence checking is a portion of a larger discipline called formal verification. This technology uses mathematical modeling techniques to prove that two representations of design exhibit the same behavior. This approach should not be confused with functional verification, which uses exhaustive simulation to verify the correctness of a design. It is a method of comparing two different representations of the same design, such as a high-level description and a low-level implementation, and proving that they are functionally equivalent. For example, suppose we have a design that performs addition of two 8-bit numbers, and we want to verify that it matches the specification. We can use equivalence checking to compare the design with a reference model that implements the same functionality, such as a simple adder circuit. If the equivalence checker can prove that the two models produce the same output for every possible input, then we can conclude that the design is correct.

Once a verified version of a design has been identified, equivalence checking can be used to determine if an alternate representation of the design behaves the same as the verified version. This technique does not use input vectors so it is more efficient. Equivalence checking is useful to verify that a design’s function has not changed after an operation like synthesis, or after a functional ECO has been applied.

Property checking is a method of verifying that a design satisfies certain properties or specifications, such as safety, liveness, or performance. For example, suppose we have a design that implements a traffic light controller, and we want to verify that it meets some requirements. We can use property checking to express the requirements as logical formulas, such as "the light should never be green in both directions at the same time", or "the light should change from red to green after at most 10 seconds". Then, we can use a property checker to check whether the design satisfies these formulas for all possible scenarios. If the property checker can prove that the design meets all the requirements, then we can conclude that the design is correct.

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

Lets look at them with examples

In this example, we have two modules: adder and adder_tb. The adder module is a simple 4-bit adder that takes two inputs a and b and produces an output sum. The adder_tb module is a testbench that instantiates the adder module and applies some test vectors to it. The $display statement in the testbench prints the value of sum after 10 time units.

To perform equivalence checking on this design, we can compare the RTL code of the adder module with its gate-level netlist. If they are logically equivalent, then we can conclude that the implementation has not changed the functionality of the design.

module adder (input [3:0] a, b, output [3:0] sum);

    assign sum = a + b;

endmodule

module adder_tb;

    reg [3:0] a, b;

    wire [3:0] sum;

    adder dut (.a(a), .b(b), .sum(sum));

    initial begin

        a = 4'b0000;

        b = 4'b0001;

        #10 $display("sum = %b", sum);

        $finish;

    end

endmodule

Here’s an example of property checking using SystemVerilog assertions:

In this example, we have two modules: counter and counter_tb. The counter module is a simple 4-bit counter that increments its output count on every clock cycle. The counter_tb module is a testbench that instantiates the counter module and applies some test vectors to it. The $assert statement in the testbench checks whether the counter has counted up to 15 (i.e., 4’b1111) after 100 time units.

To perform property checking on this design, we can use formal verification tools such as model checkers or theorem provers to verify whether the assertion holds for all possible input sequences.

module counter (input clk, reset, output reg [3:0] count);

    always @(posedge clk) begin

        if (reset) begin

            count <= 4'b0000;

        end else begin

            count <= count + 1;

        end

    end

endmodule

module counter_tb;

    reg clk, reset;

    wire [3:0] count;

    counter dut (.clk(clk), .reset(reset), .count(count));

    initial begin

        clk = 1'b0;

        reset = 1'b1;

        #10 reset = 1'b0;

        #100 $display("count = %b", count);

        #100 $assert(count == 4'b1111) else $error("Counter did not count up to 15");

        $finish;

    end

    always #5 clk = ~clk;

endmodule