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

ABD - Boolean Equivalence Checker

Often we have two implementations of a combinational circuit to check for equivalence.

RTL version: pre-synthesis,
Gate-level version: post-synthesis or post-layout.

Error sources: manual implementation of one of them, manual edits to synthesiser outputs and EDA tool faults.

Boolean equivalence: do the two functions produce the same output?

For all input combinations ?
For a subset of input combinations (some input patterns are don't cares).

Method: Create a MITRE of the two designs using a disjunction of XOR gate outputs.
Then: feed negation of mitre to a SAT solver.
Result: if there are no solutions, designs are equivalent.