Formally verifying a microprocessor using a simulation methodology
Derek L. Beatty, Randal E. Bryant · 1994
Formal verification is becoming a useful means of validating designs. We have developed a methodology for formally verifying dataintensive circuits (e.g., processors) with sophisticated timing (e.g., pipelining) against high-level declarative specifications. Previously, formally verifying a microprocessor required the use of an automatic theorem prover, but our technique requires little more than a symbolic simulator. We have formally verified a pre-existing 16-bit CISC microprocessor circuit extracted from the fabricated layout. Introduction Previously, symbolic switch-level simulation has been used to verify some small or simple data-intensive circuits (RAMs, stacks, register files, ALUs, and simple pipelines) [2, 3]. In doing so, the necessary simulation patterns were developed by hand or by using ad-hoc techniques, and it was then argued that the patterns were sufficient, and that their generation could be automated. We have developed sufficient theory to fully support such claims...