EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations

1. R.E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Surveys, Vol. 24No. 3 (September 1992), pp. 293–318.

   Article  Google Scholar 

2. R.E. Bryant, S. German, and M.N. Velev, “Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,” ACM Transactions on Computational Logic (TOCL), Vol. 2,No. 1 (January 2001). Available from: http://www.ece.cmu.edu/~mvelev.

3. R.E. Bryant, and M.N. Velev, “Boolean Satisfiability with Transitivity Constraints, Computer-Aided Verification (CAV’00), E.A. Emerson and A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 86–98. Available from: http://www.ece.cmu.edu/~mvelev.

   Chapter  Google Scholar 

4. J.R. Burch, and D.L. Dill, “Automated Verification of Pipelined Microprocessor Control,” Computer-Aided Verification (CAV’94), D.L. Dill, ed., LNCS 818, Springer-Verlag, June 1994, pp. 68–80. http://sprout.stanford.edu/papers.html.

   Google Scholar 

5. J.R. Burch, “Techniques for Verifying Superscalar Microprocessors,” 33rd Design Automation Conference (DAC’ 96), June 1996, pp. 552–557.

   Google Scholar 

6. CUDD-2.3.0, http://vlsi.colorado.edu/~fabio.

7. A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal, “BDD Based Procedures for a Theory of Equality with Uninterpreted Functions,” Computer-Aided Verification (CAV’ 98), A.J. Hu and M.Y. Vardi, eds., LNCS 1427, Springer-Verlag, June 1998, pp. 244–255.

   Chapter  Google Scholar 

8. J.L. Hennessy, and D.A. Patterson, Computer Architecture: A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, San Francisco, CA, 1996.

   MATH  Google Scholar 

9. R. Hosabettu, “Systematic Verification of Pipelined Microprocessors,” Ph.D. thesis, Department of Computer Science, University of Utah, August 2000.

   Google Scholar 

10. M. Kaufmann, P. Manolios, J.S. Moore, Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, Boston/Dordrecht/London, 2000.

    Google Scholar 

11. M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” 38th Design Automation Conference (DAC’01), June 2001.

    Google Scholar 

12. A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel, “Deciding Equality Formulas by Small-Domain Instantiations,” Computer-Aided Verification (CAV’99), N. Halbwachs and D. Peled, eds., LNCS 1633, Springer-Verlag, June 1999, pp. 455–469.

    Chapter  Google Scholar 

13. PVS Specification and Verification System (PVS), http://pvs.csl.sri.com.

14. G. Ritter, H. Eveking, and H. Hinrichsen, “Formal Verification of Designs with Complex Control by Symbolic Simulation,” Correct Hardware Design and Verification Methods (CHARME’99), L. Pierre and T. Kropf, eds., LNCS 1703, Springer-Verlag, September 1999, pp. 234–249.

    Google Scholar 

15. J. Sawada, “Formal Verification of an Advanced Pipelined Machine,” Ph.D. thesis, Department of Computer Science, University of Texas at Austin, December 1999.

    Google Scholar 

16. Stanford Validity Checker (SVC), http://sprout.stanford.edu.

17. D.E. Thomas, and P.R. Moorby, The Verilog*R Hardware Description Language, 4th edition, Kluwer Academic Publishers, Boston/Dordrecht/London, 1998.

    Google Scholar 

18. M.N. Velev, and R.E. Bryant, “Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic,” Correct Hardware Design and Verification Methods (CHARME’99), L. Pierre and T. Kropf, eds., LNCS 1703, Springer-Verlag, September 1999, pp. 37–53. Available from: http://www.ece.cmu.edu/~mvelev.

    Google Scholar 

19. M.N. Velev, and R.E. Bryant, “Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction,” 37th Design Automation Conference (DAC’00), June 2000, pp. 112–117. Available from: http://www.ece.cmu.edu/~mvelev.

20. M.N. Velev, “Formal Verification of VLIW Microprocessors with Speculative Execution,” Computer-Aided Verification (CAV’00), E.A. Emerson and A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 296–311. Available from: http://www.ece.cmu.edu/~mvelev.

    Chapter  Google Scholar 

21. M.N. Velev, “Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors,” Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), T. Margaria and W. Yi, eds., LNCS, Springer-Verlag, April 2001, pp. 252–267. Available from: http://www.ece.cmu.edu/~mvelev.

    Chapter  Google Scholar 

22. M.N. Velev, and R.E. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,” 38th Design Automation Conference (DAC’01), June 2001. Available from: http://www.ece.cmu.edu/~mvelev.

23. P.F. cWilliams, “Formal Verification Based on Boolean Expression Diagrams,” Ph.D. thesis, Department of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000.

    Google Scholar 

24. P.J. Windley, and J.R. Burch, “Mechanically Checking a Lemma Used in an Automatic Verification Tool,” Formal Methods in Computer-Aided Design (FMCAD’96), M. Srivas and A. Camilleri, eds., LNCS 1166, Springer-Verlag, November 1996, pp. 362–376.

    Chapter  Google Scholar 

Download references