HOME       UP       PREV       FURTHER NOTES       NEXT (Automated versus Manual Proof Tools)  

ABD - Boolean Equivalence Checker

Often we have two implementations of a combinational circuit to check for equivalence. For example, they might be:

  1. RTL version: pre-synthesis,
  2. 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?

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.

A mitre compares the outputs from a pair of supposedly-equivalent combinational components.

20: (C) 2012-18, DJ Greaves, University of Cambridge, Computer Laboratory.