Some Papers on Microprocessor and Hardware Verification
Note: This list is evolving. Whenever I read a paper
that I like, I tend to put it here. If you see an interesting paper
on the topic missing from the list or if you find errors in the
information on any of the papers provided here, then I will appreciate
if you let me know.
- S. Beyer, C. Jacobi, D. Kröning, D. Leinenbach, and
W. J. Paul. Putting It All Together --- Formal Verification of the
VAMP. International Journal on Software Tools and Technology
Transfer, volume 8(4-5), pages 411-430, 2006.
- P. Manolios and S. Srinivasan. A Framework for Verifying
Pipelined Machines Based on Automated Deduction and Decision
Procedures. Journal of Automated Reasoning, volume 37(1-2), pages
- E. Reeber and W. A. Hunt, Jr. A SAT-Based Decision
Procedure for the Subclass of Unrollable List Formulas in ACL2
(SULFA). In U. Furbach and N. Shankar, editors, Proceedings of
the 3rd International Joint Conference on Automated Reasoning (IJCAR
2006), Seattle, WA, August 2006, volume 4130 of LNCS, pages 453-467.
- W. A. Hunt, Jr. Mechanical Mathematical Methods for
Microprocessor Verification. In R. Alur and D. A. Peled, editors,
Proceedings of the 16th International Conference on Computer-aided
Verification (CAV 2004), Boston, MA, July 2004, volume 3117 of LNCS,
pages 523-533. Springer-Verlag.
- S. Ray and W. A. Hunt, Jr. Deductive Verification of
Pipelined Machines Using First-order Quantification. In R. Alur
and D. A. Peled, editors, Proceedings of the 16th International
Conference on Computer-aided Verification (CAV 2004), Boston, MA, July
2004, volume 3117 of LNCS, pages 31-43. Springer-Verlag.
- M. Aagaard, B. Cook, N. Day, and R. B. Jones. A Framework
for Superscalar Microprocessor Correctness Statements.
International Journal on Software Tools and Technology Transfer,
volume 4(3), pages 293-312, 2003.
- W. Adams, W. A. Hunt, Jr., and D. Jamsek. Verisym:
Verifying Circuits by Symbolic Simulation. Formal Methods in
Systems Design, volume 22(2), pages 163-203. 2003.
- S. K. Lahiri and R. E. Bryant. Deductive Verification of
Advanced Out-of-Order Microprocessors. In W. A. Hunt, Jr. and
F. Somenzi, editors, Proceedings of the 15th International Conference
on Computer-Aided Verification (CAV 2003), Boulder, CO, July 2003,
volume 2725 of LNCS, pages 154-166. Springer-Verlag.
- M. N. Velev and R. E. Bryant. Effective Use of Boolean
Satisfiability Procedures in the Formal Verification of Superscalar
and VLIW Microprocessors. Journal of Symbolic Computation, volume
35(2), pages 75-106, 2003.
- J. Sawada and W. A. Hunt, Jr. Verification of FM9801: An
Out-of-order Microprocessor Model with Speculative Execution,
Exceptions, and Program Modification Capability. Formal Methods
in Systems Design, volume 20(2), pages 187-222. 2002.
- M. Aagaard, B. Cook, N. Day, and R. B. Jones. A Framework
for Microprocessor Correctness Statements. In T. Margaria and
T. Melham, editors, Proceedings of Correct Hardware Design and
Verification Methods, 11th IFIP WG 10.5 Advanced Research Working
Conference (CHARME 2001), Scotland, UK, September 2001, volume 2144 of
LNCS, pages 433-448. Springer-Verlag.
- R. B. Jones, J. W. O'Leary, C. H. Seger, M. Aagaard, and
T. Melham. Practical Formal Verification in Microprocessor
Design. IEEE Design & Test of Computers, volume 18(4), pages
- D. A. Greve, M. Wilding, and D. Hardin. High-Speed,
Analyzable Simulators. In M. Kaufmann, P. Manolios, and J
S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, 2000.
Kluwer Academic Publishers.
- R. Hosabettu, G. Gopalakrishnan, and M. Srivas. Verifying
Advanced Microarchitectures that Support Speculation and
Exceptions. In E. A. Emerson and A. P. Sistla, editors,
Proceedings of the 12th International Conference on Computer-Aided
verification (CAV 2000), Chicago, IL, July 2000, volume 1855 of LNCS,
pages 521-537. Springer-Verlag.
- C. Kern and M. R. Greenstreet. Formal Verification in
Hardware Design: A Survey. ACM Transactions on Design Automation
of Electronic Systems, volume 4(2), pages 123-199, 1999.
- B. Brock and W. A. Hunt, Jr. The DUAL-EVAL Hardware
Description Language and Its Use in the Formal Specification and
Verification of the FM9001 Microprocessor. Formal Methods in
Systems Design, volume 11(1), pages 71-104. 1997.
- B. Brock and W. A. Hunt, Jr. Formally Specifying and
Mechanically Verifying Programs on the Motorola Complex Arithmetic
Processor DSP. In Proceedings of the International Conference on
Computer Design: VLSI in Computers and Processors (ICCD 1997), Austin,
TX, October 1997, pages 31-36. IEEE Computer Society
- R. P. Kurshan. Formal Verification in a Commercial
Setting. In Proceedings of the 34th Design Automation Conference
(DAC 1997), Anaheim, CA, June 1997, pages 258-262. ACM
- J. Sawada and W. A. Hunt, Jr. Trace Table Based Approach
for Pipeline Processor Verification. In O. Grumberg, editor,
Proceedings of the 9th International Conference on Computer-Aided
Verification (CAV 1997), Haifa, Israel, June 1997, volume 1254 of
LNCS, pages 364-375. Springer-Verlag.
- B. Brock, M. Kaufmann, and J S. Moore. ACL2 Theorems about
Commercial Microprocessors. In M. Srivas and A. Camilleri,
editors, Proceedings of the 1st International Conference of
Computer-Aided Design (FMCAD 1996), Palo Alto, CA, November 1996,
volume 1166 of LNCS, pages 275-293. Springer-Verlag.
- J. R. Burch and D. L. Dill. Automatic Verification of
Pipelined Microprocessor Control. In D. Dill, editor, Proceedings
of the 6th International Conference on Computer-Aided Verification
(CAV 1994), Stanford, CA, June 1994, volume 818 of LNCS, pages
- W. A. Hunt, Jr. FM8501: A Verified Microprocessor.
Volume 795 of LNAI, 1994. Springer.
- M. C. McFarland. Formal Verification of Sequential
Hardware: A Tutorial. IEEE Transactions on Computer-Aided Design
of Integrated Circuits and Systems, volume 12(5), pages 633-654,
- A. Gupta. Formal Hardware Verification Methods: A
Survey. Formal Methods in Systems Design, volume 1, pages
- M. Srivas and M. Bickford. Formal Verification of a
Pipelined Microprocessor. IEEE Software, pages 52-64, September
- W. R. Bevier, W. A. Hunt, Jr., J S. Moore, and W. D. Young.
An Approach to Systems verification. Journal of Automated
Reasoning, volume 5(4), pages 411-428. 1989.
- W. A.Hunt, Jr. Microprocessor Design
verification. Journal of Automated Reasoning, volume 5(4), pages