Advertisement

Exploiting Constraints in Transformation-Based Verification

  • Hari Mony
  • Jason Baumgartner
  • Adnan Aziz
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

The modeling of design environments using constraints has gained widespread industrial application, and most verification languages include constructs for specifying constraints. It is therefore critical for verification tools to intelligently leverage constraints to enhance the overall verification process. However, little prior research has addressed the applicability of transformation algorithms to designs with constraints. Even when addressed, prior work lacks optimality and in cases violates constraint semantics. In this paper, we introduce the theory and practice of transformation-based verification in the presence of constraints. We discuss how various existing transformations, such as redundancy removal and retiming, may be optimally applied while preserving constraint semantics, including dead-end states. We additionally introduce novel constraint elimination, introduction, and simplification techniques that preserve property checking. We have implemented all of the techniques proposed in this paper, and have found their synergistic application to be critical to the automated solution of many complex verification problems with constraints.

Keywords

Constraint Semantic Constraint Cone Property Check Gate Type Redundancy Removal 
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.
    Pixley, C.: Integrating model checking into the semiconductor design flow. Electronic Systems Technology & Design (1999)Google Scholar
  2. 2.
    Accelera. PSL LRM, http://www.eda.org/vfv
  3. 3.
    Kaufmann, M., Martin, A., Pixley, C.: Design constraints in symbolic model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Hollander, Y., Morley, M., Noy, A.: The e language: A fresh separation of concerns. In: Technology of Object-Oriented Languages and Systems (2001)Google Scholar
  5. 5.
    Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Transactions on CAD (April 1994)Google Scholar
  6. 6.
    Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Formal verification using parametric representations of Boolean constraints. In: Design Automation Conference (June 1999)Google Scholar
  7. 7.
    Kuehlmann, A., Baumgartner, J.: Transformation-based verification using generalized retiming. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 104. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 159–173. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on CAD (December 2002)Google Scholar
  10. 10.
    Yuan, J., Shultz, K., Pixley, C., Miller, H., Aziz, A.: Modeling design constraints and biasing in simulation using BDDs. In: ICCAD (1999)Google Scholar
  11. 11.
    Yuan, J., Albin, K., Aziz, A., Pixley, C.: Constraint synthesis for environment modeling in functional verification. In: Design Automation Conference (2003)Google Scholar
  12. 12.
    Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Design Automation Conference (2005)Google Scholar
  13. 13.
    Leiserson, C., Saxe, J.: Retiming synchronous circuitry. Algorithmica 6 (1991)Google Scholar
  14. 14.
    Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 151. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Baumgartner, J., Mony, H.: Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 222–237. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: An abstraction algorithm for the verification of level-sensitive latch-based netlists. Formal Methods in System Design (23) (2003)Google Scholar
  17. 17.
    Baumgartner, J., Tripp, A., Aziz, A., Singhal, V., Andersen, F.: An abstraction algorithm for the verification of generalized C-slow designs. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 265. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  19. 19.
    McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. 20.
    Bjesse, P., Kukula, J.: Using counter example guided abstraction refinement to find complex bugs. In: Design Automation and Test in Europe (2004)Google Scholar
  21. 21.

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Hari Mony
    • 1
    • 2
  • Jason Baumgartner
    • 1
  • Adnan Aziz
    • 2
  1. 1.IBM Systems & Technology Group 
  2. 2.The University of Texas at Austin 

Personalised recommendations