Reengineering from Partial Specifications through BDD Representation of Functional Constraint

Document Type


Publication Date



This technical report presents a Binary Decision Diagram (BDD) technique for representing the relationships between structures in a known or partially known combinational circuit implementation. Circuits are represented as Structural BDDs (SBDDs) which contain decision variables for circuit structures. The satisfying set of an SBDD represents the subset of the boolean space determined by these variables which encapsulates the circuit's behavior. Representation of partial knowledge in the implementation is made possible by the introduction of blackbox decision variables, which have multiple 1-paths when unknown. We present SBDD-based techniques for representing partially specified circuits as well as for introducing new information and deducing unspecified information from structural context. These techniques are used to discover the functional behavior of unknown components in circuit descriptions from the known structure of the circuit and from SIS generated ATPG test vectors.


Technical Report MSU-CPS-97-3