Symbolic simulation for correct machine design

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.