Toward Unification of Synthesis and Verification in Topologically Constrained Logic Design

In logic synthesis, the search space is infinite in the sense that any number of gates can be connected using any topology to come up with the best circuit under performance and other constraints. In formal verification, to achieve full coverage, an n-input circuit must be checked either explicitly or implicitly using the complete set of 2ⁿ input values. There are, however, situations when the possible circuit topologies are limited. Logic optimization methods, in general, do not change circuit topologies dramatically. Most of them are based on series of local circuit transformations. In this paper, we discuss formal verification of circuits produced by logic synthesis where the search space is limited, and only gates or subcircuits are transformed whereas their interconnections never change. If there are p possible transformations for each gate or subcircuit, and there are m gates or subcircuits in the entire circuit, the number of all possible transformations for the entire circuit is p^m. Logic synthesis with this restriction attempts to find the best circuit among the p^m alternatives. The logic synthesis problem can be formulated as a sequence of incremental SAT problems and the complete set of test patterns can be computed, which detects all possible errors in the synthesized circuit. As long as the search space is limited to the p^m alternatives, such complete set of test patterns can be used for formal verification. The number of test patterns needed in this case is experimentally shown to be very small, e.g., a few hundred, even for circuits having several hundred inputs and several thousand gates. With the complete set of test patterns generated for the circuit transformations, logic synthesis and formal verification are unified in the sense that the small number of test patterns allows for logic synthesis with 100% correctness.