Skip to main content
SpringerLink
Log in
Book cover

Formal System Verification pp 37–72Cite as

Verification of Incomplete Designs

  • Chapter
  • First Online:

  • 1258 Accesses

Abstract

We consider the verification of digital systems which are incomplete in the sense that for some modules only their interfaces (i.e., the signals entering and leaving the module) are known, but not their implementations. For such designs, we study realizability (“Is it possible to implement the missing modules such that the complete design has certain properties?”) and validity (“Does a property hold no matter how the missing parts are implemented?”).

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   99.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   129.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

Notes

  1. 1.

    In the following, we denote individual signals or variables in italic font (like x, y, z) and vectors in upright bold font (like \(\mathbf {x}, \mathbf {y},\mathbf {z}\)).

  2. 2.

    In this example we assume that the inputs of the black boxes are directly connected to the primary inputs. Thus we do not need to introduce separate vectors \(\mathbf {I}_1\) and \(\mathbf {I}_2\) for the black box inputs.

  3. 3.

    Black boxes with a bounded amount of memory are reduced to the case of combinational black boxes by adding the memory of the black boxes to the surrounding circuit as mentioned above.

  4. 4.

    In general the property can also check the primary inputs and outputs, but for sake of convenience, we omit details here.

  5. 5.

    Here, we assume to have exactly one initial state; it is trivial to extend the following to sets of initial states.

  6. 6.

    Since all types of gates can be expressed using two-input \( and _2\) gates, two-input \(or_2\) gates and inv gates, we can assume w. l. o. g. that the gates have types \( and _2\), \( or _2\) or \( inv \).

  7. 7.

    Remember that \(\mathbf {s}^0\) is the initial state of the circuit.

References

  1. A. Biere, Resolve and expand, in International Conference on Theory and Applications of Satisfiability Testing (SAT), Vancouver, BC, Canada (2004)

    Google Scholar 

  2. A. Biere, M. Heule, H. van Maaren, T. Walsh (ed.), in Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185 (IOS Press, 2008)

    Google Scholar 

  3. R. Bloem, U. Egly, P. Klampfl, R. Könighofer, F. Lonsing, SAT-based methods for circuit synthesis, in International Conference on Formal Methods in Computer Aided Design (FMCAD), Lausanne, Switzerland (IEEE, 2014), pp. 31–34

    Google Scholar 

  4. R. Bloem, R. Könighofer, M. Seidl, SAT-based synthesis methods for safety specs, in International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), ed. By K.L. McMillan, X. Rival. LNCS, vol. 8318 (Springer, San Diego, CA, USA, 2014), pp. 1–20

    Google Scholar 

  5. A.R. Bradley, SAT-based model checking without unrolling, in International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 6538 (Springer, 2011), pp. 70–87

    Google Scholar 

  6. R.E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. Aided Des. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  7. R.E. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24, 293–318 (1992)

    Article  Google Scholar 

  8. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  9. E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  10. S.A. Cook, The complexity of theorem-proving procedures, in Annual ACM Symposium on Theory of Computing (STOC) (ACM Press, 1971), pp. 151–158

    Google Scholar 

  11. N. Eén, A. Mishchenko, R.K. Brayton, Efficient implementation of property directed reachability, in International Conference on Formal Methods in Computer Aided Design (FMCAD) (FMCAD Inc., 2011), pp. 125–134

    Google Scholar 

  12. A. Fröhlich, G. Kovásznai, A. Biere, H. Veith, iDQ: Instantiation-based DQBF solving, in International Workshop on Pragmatics of SAT (POS), ed. By D.L. Berre. EPiC Series, vol. 27 (EasyChair, Vienna, Austria, 2014), pp. 103–116

    Google Scholar 

  13. K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, B. Becker, Equivalence checking for partial implementations revisited, in Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), ed. By C. Haubelt, D. Timmermann (Universität Rostock, ITMZ, Rostock, Germany, 2013), pp. 61–70

    Google Scholar 

  14. K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, B. Becker, Equivalence checking of partial designs using dependency quantified Boolean formulae, in IEEE International Conference on Computer Design (ICCD), Asheville, NC, USA (IEEE Computer Society, 2013), pp. 396–403

    Google Scholar 

  15. K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, B. Becker, Solving DQBF through quantifier elimination, in International Conference on Design, Automation and Test in Europe (DATE), Grenoble, France (IEEE, 2015)

    Google Scholar 

  16. E. Giunchiglia, P. Marin, M. Narizzano, sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning, in International Conference on Theory and Applications of Satisfiability Testing (SAT), ed. By O. Strichman, S. Szeider. LNCS, vol. 6175 (Springer, Edinburgh, UK, 2010), pp. 85–98

    Google Scholar 

  17. A. Jain, V. Boppana, R. Mukherjee, J. Jain, M. Fujita, M.S. Hsiao, Testing, verification, and diagnosis in the presence of unknowns, in IEEE VLSI Test Symposium (VTS) (IEEE Computer Society, Montreal, Canada, 2000), pp. 263–270

    Google Scholar 

  18. S. Jo, A.M. Gharehbaghi, T. Matsumoto, M. Fujita, Debugging processors with advanced features by reprogramming LUTs on FPGA, in International Conference on Field-Programmable Technology (FPT) (IEEE, Kyoto, Japan, 2013), pp. 50–57

    Google Scholar 

  19. S. Jo, T. Matsumoto, M. Fujita, Sat-based automatic rectification and debugging of combinational circuits with LUT insertions. IPSJ Trans. Syst. LSI Des. Methodol. 7, 46–55 (2014)

    Article  Google Scholar 

  20. K.L. McMillan, Symbolic Model Checking (Kluwer Academic Publisher, 1993)

    Google Scholar 

  21. A.R. Meyer, L.J. Stockmeyer, Word problems requiring exponential time: preliminary report, in Annual ACM Symposium on Theory of Computing (STOC) (ACM Press, 1973), pp. 1–9

    Google Scholar 

  22. C. Miller, S. Kupferschmid, M.D.T. Lewis, B. Becker, Encoding techniques, Craig interpolants and bounded model checking for incomplete designs, in International Conference on Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 6175 (Springer, 2010), pp. 194–208

    Google Scholar 

  23. C. Miller, C. Scholl, B. Becker, Proving QBF-hardness in bounded model checking for incomplete designs, in International Workshop on Microprocessor Test and Verification (MTV) (IEEE Computer Society, Austin, TX, USA, 2013)

    Google Scholar 

  24. T. Nopper, C. Scholl, Symbolic model checking for incomplete designs with flexible modeling of unknowns. IEEE Trans. Comput. 62(6), 1234–1254 (2013)

    Article  MathSciNet  Google Scholar 

  25. G. Peterson, J. Reif, S. Azhar, Lower bounds for multiplayer non-cooperative games of incomplete information. Comput. Math. Appl. 41(7–8), 957–992 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  26. A. Pnueli, R. Rosner, Distributed systems are hard to synthesize, in IEEE Symposium on Foundations of Computer, Science (1990), pp. 746–757

    Google Scholar 

  27. C. Scholl, B. Becker, Checking equivalence for partial implementations, in ACM/IEEE Design Automation Conference (DAC) (ACM Press, Las Vegas, NV, USA, 2001), pp. 238–243

    Google Scholar 

  28. A. Smith, A.G. Veneris, M.F. Ali, A. Viglas, Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. CAD Integr. Circuits Syst. 24(10), 1606–1621 (2005)

    Article  Google Scholar 

  29. A. Sülflow, G. Fey, R. Drechsler, Using QBF to increase accuracy of SAT-based debugging, in International Symposium on Circuits and Systems (ISCAS) (IEEE, Paris, France, 2010), pp. 641–644

    Google Scholar 

  30. G.S. Tseitin, On the complexity of derivation in propositional calculus. Stud. Constr. Math. Math. Logic Part 2, 115–125 (1970)

    Article  Google Scholar 

  31. K. Wimmer, R. Wimmer, C. Scholl, B. Becker, Skolem functions for DQBF, in International Symposium on Automated Technology for Verification and Analysis (ATVA), ed. By C. Artho, A. Legay, D. Peled. LNCS, vol. 9938 (Springer, Chiba, Japan, 2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Albert-Ludwigs-Universität Freiburg, Freiburg im Breisgau, Germany

    Bernd Becker, Christoph Scholl & Ralf Wimmer

Authors
  1. Bernd Becker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Scholl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ralf Wimmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bernd Becker .

Editor information

Editors and Affiliations

  1. DFKI, University of Bremen, Bremen, Germany

    Rolf Drechsler

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this chapter

Cite this chapter

Becker, B., Scholl, C., Wimmer, R. (2018). Verification of Incomplete Designs. In: Drechsler, R. (eds) Formal System Verification. Springer, Cham. https://doi.org/10.1007/978-3-319-57685-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57685-5_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57683-1

  • Online ISBN: 978-3-319-57685-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation