Robust latch mapping for combinational equivalence checking

Existing literature on combinational equivalence checking concentrates on comparing combinational blocks and assumes that a latch mapping (register mapping) has already been constructed. We describe an algorithm for automatically constructing a latch mapping. It is based on the functionality of the circuits being compared rather than on heuristics. As a result, if two circuits are combinationally equivalent, then our algorithm is guaranteed to find a latch mapping. Our empirical results show that the method is practical on large circuits.