Symbolic Simulation for Correct Machine Design
- 1 January 1979
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Program verification techniques which manipulate symbolic rather than actual values have been used successfully to find errors in implementations of computer designs. This paper describes symbolic simulation, a method similar to symbolic execution of programs, and its use in proving the correctness of machine architectures implemented in microcode. The procedure requires formal descriptions of machines at both the architectural and register transfer levels, but has been used to detect errors in implementation which often elude the standard test case approach.Keywords
This publication has 5 references indexed in Scilit:
- Verification of protocols using symbolic executionComputer Networks (1976), 1978
- Modeling and Digital Simulation for Design Verification and DiagnosisIEEE Transactions on Computers, 1976
- Automated proofs of microprogram correctnessPublished by Association for Computing Machinery (ACM) ,1976
- A new approach to program testingPublished by Association for Computing Machinery (ACM) ,1975
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967