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 97-136, 2006.

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. Springer-Verlag.

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 16-25, 2001.

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 Press.

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 Press.

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 68-80. Springer-Verlag.

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, 1993.

A. Gupta. Formal Hardware Verification Methods: A Survey. Formal Methods in Systems Design, volume 1, pages 151-238, 1992.

M. Srivas and M. Bickford. Formal Verification of a Pipelined Microprocessor. IEEE Software, pages 52-64, September 1990.

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 429-460. 1989.