Consistency and observability invariance in multi-level logic synthesis
Patrick C. McGeer, Robert K. Brayton · 2003
An m-function network on n primary inputs as forming an n+m-dimensional space is depicted. In this space there are points that can never occur due to mutual dependencies among the functions. This set has been called the satisfiability don't-care (SDC) set of the network and can be viewed as a function over the extended space. The authors demonstrate a sharp criterion for determining which transformations of the network preserve the SDC, and show that most of the operations of the MIS-II synthesis system preserve the SDC. This has importance for implications which are used in a number of network manipulations. This analysis also clarifies how other operations change the SDC, but in very predictable ways. It is shown that a most of the algebraic and some Boolean operations commonly used in logic synthesis preserve the testability of all but a single node in a network. An interesting example is algebraic division (or resubstitution) of one node into another.>