A General Methodology for Synthesis and Verification of Register-Transfer Designs

The general relationship between register-transfer synthesis and verification is discussed, and common mechanisms are shown to underlie both tasks. The paper proposes a framework for combined synthesis and verification of hardware that supports any combination of user-selectable synthesis techniques. The synthesis process can begin with any degree of completion of a partial design, and verification of the partial design can be achieved by completing its synthesis while subjecting it to constraints that can be generated from a "template" and user constraints. The driving force was the work done by Hafer [3] on a synthesis model. The model was augmented by adding variables and constraints in order to verify interconnections. A multilevel, multidimensional design representation [6] is introduced which is shown to to be equivalent to Hafer\´s model. This equivalence relationship is exploited in deriving constraints off the design representation. These constraints can be manipulated in a variety of ways before being input to a linear program which completes the synthesis/verification process. An example is presented in which verification and synthesis occur simultaneously and the contribution of each automatically varies, depending on the number of previous design decisions.