Advertisement

Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units

  • Miroslav N. Velev
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

Presented is a highly automatic approach for proving bounded liveness of pipelined processors with multicycle functional units, without the need for the user to set up an inductive argument. Multicycle functional units are abstracted with a placeholder that is suitable for proving both safety and liveness. Abstracting the branch targets and directions with arbitrary terms and formulas, respectively, that are associated with each instruction, made the branch targets and directions independent of the data operands. The observation that the term variables abstracting branch targets of newly fetched instructions can be considered to be in the same equivalence class, allowed the use of a dedicated fresh term variable for all such branch targets and the abstraction of the Instruction Memory with a generator of arbitrary values. To further improve the scaling, the multicycle ALU was abstracted with a placeholder without feedback loops. Also, the equality comparison between the terms written to the PC and the dedicated fresh term variable for branch targets of new instructions was implemented as part of the circuit, thus avoiding the need to apply the abstraction function along the specification side of the commutative diagram for liveness. This approach resulted in 4 orders of magnitude speedup for a 5-stage pipelined DLX processor with a 32-cycle ALU, compared to a previous method for indirect proof of bounded liveness, and scaled for a 5-stage pipelined DLX with a 2048-cycle ALU.

Keywords

Formal Verification Program Counter Indirect Proof Magnitude Speedup Abstraction Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Aagaard, M.D., Day, N.A., Lou, M.: Relating multi-step and single-step microprocessor correctness statements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for superscalar microprocessor correctness statements. Software Tools for Technology Transfer (STTT) 4(3) (May 2003)Google Scholar
  3. 3.
    Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science 66 (2002)Google Scholar
  4. 4.
    Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. International Journal on Software Tools for Technology Transfer (STTT) 5(2–3) (March 2004)Google Scholar
  5. 5.
    Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic (TOCL) 2(1) (2001)Google Scholar
  6. 6.
    Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Transactions on Computational Logic (TOCL) 3(4), 604–627 (2002)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Burch, J.R., Dill, D.L.: Automated verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818. Springer, Heidelberg (1994)Google Scholar
  8. 8.
    Burch, J.R.: Techniques for verifying superscalar microprocessors. In: 33rd Design Automation Conference (DAC 1996) (June 1996)Google Scholar
  9. 9.
    Damm, W., Pnueli, A., Ruah, S.: Herbrand Automata for Hardware Verification. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 67–83. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  10. 10.
    Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 244–255. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Goldberg, E., Novikov, Y.: BerkMin: A fast and robust sat-solver. In: DATE 2002, March 2002, pp. 142–149 (2002)Google Scholar
  12. 12.
    Goldberg, E., Novikov, Y.: SAT-solver BerkMin621 (June 2003)Google Scholar
  13. 13.
    Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 3rd edn. Morgan Kaufmann, San Francisco (2002)zbMATHGoogle Scholar
  14. 14.
    Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Decomposing refinement proofs using assume-guarantee reasoning. In: International Conference on Computer-Aided Design, ICCAD 2000 (2000)Google Scholar
  15. 15.
    Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 47–59. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Jacobi, C., Kröning, D.: Proving the correctness of a complete microprocessor. In: 30. Jahrestagung der Gesellshaft für Informatik. Springer, Heidelberg (2000)Google Scholar
  17. 17.
    Kröning, D., Paul, W.J.: Automated pipeline design. In: Design Automation Conference (DAC 2001) (June 2001)Google Scholar
  18. 18.
    Lahiri, S., Pixley, C., Albin, K.: Experience with term level modeling and verification of the M∙CORETM microprocessor core. In: International Workshop on High Level Design, Validation and Test (HLDVT 2001) (November 2001)Google Scholar
  19. 19.
    Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  20. 20.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering 3(2) (1977)Google Scholar
  21. 21.
    Le Berre, D., Simon, L.: Results from the SAT’03 solver competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004), http://www.lri.fr/~simon/contest03/results/ Google Scholar
  22. 22.
    Malik, S., Wang, A.R., Brayton, R.K., Sangiovani-Vincentelli, A.: Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment. In: International Conference on Computer-Aided Design (November 1988)Google Scholar
  23. 23.
    Manolios, P.: Mechanical verification of reactive systems. Ph.D. Thesis, Computer Sciences, Univ. of Texas at Austin (2001)Google Scholar
  24. 24.
    Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for XScale-like processor models using WEB refinements. In: Design, Automation and Test in Europe (DATE 2004), February 2004, vol. 1 (2004)Google Scholar
  25. 25.
    Matthews, J., Launchbury, J.: Elementary microarchitecture algebra. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 288–300. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  26. 26.
    Matthews, J.R.: Algebraic specification and verification of processor microarchitectures. Ph.D. Thesis, Department of Computer Science and Engineering, Oregon Graduate Institute of Science and Technology (October 2000)Google Scholar
  27. 27.
    McMillan, K.L.: Circular compositional reasoning about liveness. Technical Report, Cadence Berkeley Labs (1999)Google Scholar
  28. 28.
    Müller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)zbMATHGoogle Scholar
  29. 29.
    Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, infinity)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 107. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  30. 30.
    Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The small model property: how small can it be? Journal of Information and Computation 178(1), 279–293 (2002)zbMATHMathSciNetGoogle Scholar
  31. 31.
    Ryan, L.: Siege SAT Solver v.4, http://www.cs.sfu.ca/~loryan/personal/
  32. 32.
    Sawada, J.: Verification of a simple pipelined machine model. In: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Boston (2000)Google Scholar
  33. 33.
    Sharangpani, H., Arora, K.: Itanium processor microarchitecture. IEEE Micro 20(5) (2000)Google Scholar
  34. 34.
    Srivas, M.K., Miller, S.P.: Formal verification of an avionics microprocessor. Tech. Report CSL-95-4, SRI International (1995)Google Scholar
  35. 35.
    Velev, M.N., Bryant, R.E.: Exploiting positive equality and partial non-consistency in the formal verification of pipelined microprocessors. In: 36th Design Automation Conference (DAC 1999) (June 1999)Google Scholar
  36. 36.
    Velev, M.N., Bryant, R.E.: Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 37–53. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  37. 37.
    Velev, M.N., Bryant, R.E.: Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction. In: 37th Design Automation Conference (DAC 2000) (June 2000)Google Scholar
  38. 38.
    Velev, M.N.: Formal verification of VLIW microprocessors with speculative execution. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  39. 39.
    Velev, M.N.: Automatic abstraction of memories in the formal verification of superscalar microprocessors. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 252–267. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  40. 40.
    Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. Journal of Symbolic Computation (JSC) 35(2) (February 2003)Google Scholar
  41. 41.
    Velev, M.N.: Automatic abstraction of equations in a logic of equality. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol. 2796. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  42. 42.
    Velev, M.N.: Using positive equality to prove liveness for pipelined microprocessors. In: Asia and South Pacific Design Automation Conference (ASP-DAC 2004) (January 2004)Google Scholar
  43. 43.
    Velev, M.N.: Efficient translation of Boolean formulas to CNF in formal verification of microprocessors. In: Asia and South Pacific Design Automation Conference (ASP-DAC 2004) (January 2004)Google Scholar
  44. 44.
    Velev, M.N.: Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors. In: Design, Automation and Test in Europe (DATE 2004) (February 2004)Google Scholar
  45. 45.
    Velev, M.N.: Comparative Study of Strategies for Formal Verification of High-Level Processors. In: 22nd International Conference on Computer Design (ICCD 2004), October 2004, pp. 119–124.Google Scholar
  46. 46.
    Velev, M.N., Bryant, R.E.: TLSim and EVC: A term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories. International Journal of Embedded Systems (IJES), Special Issue on Hardware-Software Codesign for Systems-on-Chip (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Miroslav N. Velev

There are no affiliations available

Personalised recommendations