Skip to main content

Debugging Contradictory Constraints in Constraint-Based Random Simulation

  • Chapter
  • 780 Accesses

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 36))

Abstract

Constraint-based random simulation is state-of-the-art in verification of multi-million gate industrial designs. This method is based on stimulus generation by constraint solving. The resulting stimuli will particularly cover corner case test scenarios which are usually hard to identify manually by the verification engineer. Consequently, constraint-based random simulation will catch corner case bugs that would remain undetected otherwise. Therefore, the quality of design verification is increased significantly. However, in the process of constraint specification for a specific test scenario, the verification engineer is faced with the problem of over-constraining, i.e. the overall constraint specified for a test scenario has no solution. In this case the root cause of the contradiction has to be identified and resolved. Given the complexity of constraints used to describe test scenarios, this can be a very time-consuming process.

In this chapter we propose a fully automated contradiction analysis method. Our method determines all “nonrelevant” constraints and computes all reasons that lead to the over-constraining. Thus, we pinpoint the verification engineer to exactly the sets of constraints that have to be considered to resolve the over-constraining. Experiments have been conducted in a real-life SystemC-based verification environment at AMD Dresden Design Center. They demonstrate a significant reduction of the constraint contradiction debug time.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R.R. Bakker, F. Dikker, F. Tempelman, and P.M. Wognum. Diagnosing and solving over-determined constraint satisfaction problems. In International Joint Conference on Artificial Intelligence, pages 276–281, 1993.

    Google Scholar 

  2. J. Bergeron. Writing Testbenches Using SystemVerilog. Springer, Berlin, 2006.

    Google Scholar 

  3. R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp., 35(8):677–691, 1986.

    Article  MATH  Google Scholar 

  4. R. Dechter, K. Kask, E. Bin, and R. Emek. Generating random solutions for constraint satisfaction problems. In Eighteenth National Conference on Artificial Intelligence, pages 15–21, 2002.

    Google Scholar 

  5. E. Goldberg and Y. Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Design, Automation and Test in Europe, pages 10886–10891, 2003.

    Google Scholar 

  6. D. Große, R. Ebendt, and R. Drechsler. Improvements for constraint solving in the SystemC verification library. In ACM Great Lakes Symposium on VLSI, pages 493–496, 2007.

    Google Scholar 

  7. J. Huang. Mup: a minimal unsatisfiability prover. In ASP Design Automation Conf., pages 432–437, 2005.

    Google Scholar 

  8. IEEE Std. 1666. IEEE Standard SystemC Language Reference Manual, 2005.

    Google Scholar 

  9. IEEE Std. 1800. IEEE SystemVerilog, 2005.

    Google Scholar 

  10. C.N. Ip and S. Swan. A tutorial introduction on the new SystemC verification standard. White paper, 2003.

    Google Scholar 

  11. M.A. Iyer. Race: A word-level ATPG-based constraints solver system for smart random simulation. In Int’l Test Conf., pages 299–308, 2003.

    Google Scholar 

  12. N. Kitchen and A. Kuehlmann. Stimulus generation for constrained random simulation. In Int’l Conf. on CAD, pages 258–265, 2007.

    Google Scholar 

  13. M.H. Liffiton and K.A. Sakallah. On finding all minimally unsatisfiable subformulas. In Theory and Applications of Satisfiability Testing, pages 173–186, 2005.

    Google Scholar 

  14. M.N. Mneimneh, I. Lynce, Z.S. Andraus, J.P. Marques-Silva, and K.A. Sakallah. A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas. In Theory and Applications of Satisfiability Testing, pages 467–474, 2005.

    Google Scholar 

  15. Y. Oh, M. Mneimneh, Z. Andraus, K. Sakallah, and I. Markov. Amuse: A minimally-unsatisfiable subformula extractor. In Design Automation Conf., pages 518–523, 2004.

    Google Scholar 

  16. T. Petit, J.-C. Régin, and C. Bessière. Specific filtering algorithms for over-constrained problems. In International Conference on Principles and Practice of Constraint Programming, pages 451–463, 2001.

    Google Scholar 

  17. J. Rose and S. Swan. SCV randomization version 1.0. 2003.

    Google Scholar 

  18. F. Somenzi. CUDD: CU Decision Diagram Package Release 2.3.0. University of Colorado at Boulder, Boulder, 1998.

    Google Scholar 

  19. Synopsys Inc., CoWare Inc., and Frontier Design Inc. Functional Specification for SystemC 2.0. http://www.systemc.org.

  20. SystemC Verification Working Group. SystemC Verification Standard Specification Version 1.0e. http://www.systemc.org.

  21. J. Yuan, A. Aziz, C. Pixley, and K. Albin. Simplifying boolean constraint solving for random simulation-vector generation. IEEE Trans. on CAD of Integrated Circuits and Systems, 23(3):412–420, 2004.

    Article  Google Scholar 

  22. J. Yuan, C. Pixley, and A. Aziz. Constraint-Based Verification. Springer, Berlin, 2006.

    MATH  Google Scholar 

  23. J. Yuan, K. Shultz, C. Pixley, H. Miller, and A. Aziz. Modeling design constraints and biasing in simulation using BDDs. In Int’l Conf. on CAD, pages 584–590, 1999.

    Google Scholar 

  24. L. Zhang and S. Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Design, Automation and Test in Europe, pages 10880–10885, 2003.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Daniel Große .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Große, D., Wille, R., Siegmund, R., Drechsler, R. (2009). Debugging Contradictory Constraints in Constraint-Based Random Simulation. In: Radetzki, M. (eds) Languages for Embedded Systems and their Applications. Lecture Notes in Electrical Engineering, vol 36. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-9714-0_18

Download citation

  • DOI: https://doi.org/10.1007/978-1-4020-9714-0_18

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-9713-3

  • Online ISBN: 978-1-4020-9714-0

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics