Equivalence Checking of Hierarchical Combinational Circuits

This paper presents a method for verifying that two hierarchical combinational circuits implement the same Boolean functions. The key new feature of the method is its ability to exploit the modularity of the circuits to reuse results obtained from one part of the circuits in other parts. We demonstrate the method on large adder and multiplier circuits