Formal Verification of a Microprocessor Using Equational Techniques

This paper develops a method for formally proving the correctness of a microprocessor using an equational method. The behavioral and structural specifications of the processor are expressed in a functional language. The asynchronous interaction between the memory and CPU is expressed in the specification by using a nondeterministic function random. This makes our specification more direct and natural than previous efforts based on a functional formalism. The previous efforts have had to encode in the specification the anticipated asynchronous interaction between the memory and the CPU.