On Proving the Correctness of Optimizing Transformations in a Digital Design Automation System
- 1 January 1981
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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.Keywords
This publication has 11 references indexed in Scilit:
- A Formal Method for the Specification, Analysis, and Design of Register-Transfer Level Digital LogicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1981
- VLSI Design Methodology - the Problem of the 80's for Microprocessor DesignPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- The CMU Design Automation System - An Example of Automated Data Path DesignPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Proving and applying program transformations expressed with second-order patternsActa Informatica, 1978
- Program Improvement by Source-to-Source TransformationJournal of the ACM, 1977
- Proof Theory of Partial Correctness Verification SystemsSIAM Journal on Computing, 1976
- The denotational semantics of programming languagesCommunications of the ACM, 1976
- A formal approach to code optimizationACM SIGPLAN Notices, 1970
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967
- High speed compilation of efficient object codeCommunications of the ACM, 1965