Advertisement

A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems

  • Panagiotis Manolios
  • Sudarshan K. Srinivasan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

We present a parameterized suite of benchmark problems arising from our work on pipelined machine verification, in the hopes that they can be used to speed up decision procedures. While the existence of a large number of CNF benchmarks has spurred the development of efficient SAT solvers, the benchmarks available for more expressive logics are quite limited. Our work on pipelined machine verification has yielded many problems that not only have complex models, but also have complex correctness statements, involving invariants and symbolic simulations of the models for dozens of steps. Many of these proofs take hundreds of thousands of seconds to check using the UCLID decision procedure and SAT solvers such as Zchaff and Siege. More complex problems can be generated by using PiMaG, a Web application that we developed. PiMaG generates problems in UCLID, SVC, and CNF formats based on user-provided parameters specifying features of the pipelined machines and their correctness statements.

Keywords

Decision Procedure Benchmark Problem Data Cache Benchmark Suite Instruction Cache 
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.
    Barret, C., de Moura, L.M., Stump, A.: The satisfiability modulo theories competition, SMT-COMP 2005 (2005), See http://www.csl.sri.com/users/-demoura/smt-comp
  2. 2.
    Bryant, R.E., Lahiri, S.K., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)Google Scholar
  4. 4.
    de Moura, L.M., Rueß, H.: An experimental evaluation of ground decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 162–174. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Manolios, P.: Correctness of pipelined machines, pp. 161–178Google Scholar
  6. 6.
    Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (August 2001), See http://www.cc.gatech.edu/~manolios/-publications.html
  7. 7.
    Manolios, P., Srinivasan, S.: Automatic verification of safety and liveness for xscale-like processor models using web refinement. In: Design, Automation, and Test in Europe, DATE 2004 (2004)Google Scholar
  8. 8.
    Manolios, P., Srinivasan, S.K.: A computationally efficient method based on commitment refinement maps for verifying pipelined machines. In: Formal Methods and Models for Codesign (MEMOCODE) (July 2005) (accepted to appear)Google Scholar
  9. 9.
    Manolios, P., Srinivasan, S.K.: A parameterized benchmark suite of hard pipelined-machine-verification problems (2005), See http://www.cc.gatech.edu/-manolios/benchmarks/charme.html
  10. 10.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (DAC 2001), pp. 530–535 (2001)Google Scholar
  11. 11.
    Ryan, L.: Siege homepage, See http://www.cs.sfu.ca/~loryan/-personal

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Panagiotis Manolios
    • 1
  • Sudarshan K. Srinivasan
    • 2
  1. 1.College of Computing 
  2. 2.School of Electrical & Computer EngineeringGeorgia Institute of TechnologyAtlanta

Personalised recommendations