A Case Study: Formal Verification of Processor Critical Properties

  • Emmanuel Zarpas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Over the past ten years, the Formal Methods group at the IBM Haifa Research Lab has made steady progress developing tools and techniques that bring the power of model checking to the community of hardware designers and verification engineers, making it an integral part of the design cycle for many projects. Several IBM and non-IBM design teams have successfully integrated RuleBase [2], the IBM formal methods tool, into their design cycles. In this paper we present a case study describing the formal verification of critical properties in a recent processor. Because the details of the design and the specifications are highly proprietary, this paper focuses on the process, techniques and experience involved in the formal verification of the critical properties. We report here experiences on two units, named here for confidentiality reasons unit A and B.


  1. 1.
    Accelera. PSL LRM,
  2. 2.
    Ben-David, S., et al.: Model Checking in IBM. Formal Methods in System Design 22 (2003)Google Scholar
  3. 3.
    Biere, A., et al.: Symbolic Model Checking Without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    McMillan, K.L.: Interpolation and SAT-based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 58. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Emmanuel Zarpas
    • 1
  1. 1.IBM Haifa Research Laboratory 

Personalised recommendations