Issue No. 03 - May/June (1999 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/40.768503
Designers use formal logic and a theorem prover to verify that a complex microarchitecture always implements its instruction set correctly. Hardware verification accounts for a considerable portion of the costs in the microprocessor design process. Traditionally, designers have verified microprocessor designs using simulation techniques that help find most design faults. However, simulation never guarantees the correct operation of the final product. Some design faults are very difficult to detect by simulation; they may slip through the verification process into manufactured chips, raising costs. We believe that verification costs can be reduced by the judicious application of formal methods, which should lower the overall costs of design.
W. A. Hunt, Jr. and J. Sawada, "Verifying the FM9801 Microarchitecture," in IEEE Micro, vol. 19, no. , pp. 47-55, 1999.