On Proving the Correctness of Optimizing Transformations in a Digital Design Automation System

As part of our research for the Carnegie-Mellon University Design Automation System, we have been investigating methods for proving that the system produces correct designs from correct specifications. This paper presents a mathematical model of the behavior of hardware descriptions which has been used to prove that some of the optimizing transformations applied to abstract hardware descriptions in the system preserve behavioral equivalence. The model goes beyond the usual computational models used in program verification in that it takes into account the proper sequencing of "events" which represent interactions with the environment.