Automatic precondition verification for high-level design transformations

A precondition verification system for high-level (register-transfer-level) design transformations is described. The system can verify spatial preconditions in terms of the data path composition and topology, as well as temporal preconditions in terms of assertions on the control flow paths. The system is implemented in Prolog and incorporates a mixture of techniques including symbolic equivalence and partial evaluation to effectively verify the preconditions in the presence of arbitrarily nested data-dependent decision points (conditional and iterative constructs) in the control graph. An example which shows how the system can be used for precondition verification is presented