Formally Verifying a Microprocessor Using a Simulation Methodology

摘要: Formal verification is becoming a useful means of validating designs. We have developed methodology for formally verifying dataintensive circuits (e.g., processors) with sophisticated timing pipelining) against high-level declarative specifications. Previously, microprocessor required the use an automatic theorem prover, but our technique requires little more than symbolic simulator. verified pre-existing 16-bit CISC circuit extracted from fabricated layout.