HOME       UP       PREV       FURTHER NOTES       NEXT (ABD - Sequential Logic Equivalence: Example)  

Boolean Equivalence Checker

Often we have two implementations to check for equivalence, for instance, when RTL is turned into a gate-level netlist by synthesis we have:

After place and route operations, it is common to extract the netlist out from the masks and check that for correctness, so this is another source of the same netlist.

There two main sources of potential errors: 1. manual edits at any point may upset correctness. 2. EDA tools used in the flow may have bugs.

The boolean equivalence problem is do two functions produce the same output. However, are we interested for all input combinations? No, normally we are only interested in a subset of input combinations (because of don't care conditions).

The standard method is to create a mitre of the two designs using a disjunction of XOR gate outputs. Then, feed negation of mitre to a SAT solver to see if it can find any input condition that produces a one on the output.

SAT solving is a matter of trying all input combinations, so has exponential cost in theory and is NP complete. However, modern solvers such as zChaff essentially exploit the intrinsic structure of the problem so that they normally are quite quick at finding the answer.

Result: if there are no input combinations that make the mitre indicate a functionality difference, then the designs are equivalent.

Commercial example »Formality

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.