Logic synthesis and verification on fixed topology

We discuss about logic synthesis and formal verification of combinational circuits mapped to a given fixed topology. Here “fixed topology” means that circuit structures in terms of net lists except for gate/cell types are fixed in advance. That is, for logic synthesis, what should be generated are the types of gates/cells (or simply gates) in the circuits, and all the others are prefixed before synthesis. As the circuit topology is fixed in advance, placement and routing could be shared among different designs and minimum ECO can be realized by keeping the same layout. Also, we can show that we do not need many test vectors in order to guarantee 100% correctness of such synthesis. Small numbers of test vectors, such as only 100 test vectors for 30 input circuits, are sufficient to test if the circuits behave correctly for all possible input value combinations. That is, very efficient formal verification can be realized through simulations with small numbers of test vectors. We present SAT based implementation of the synthesis and a test vector generation method with preliminary but encouraging experimental results.