[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Timed Verification of Asynchronous Circuits

  • Chapter
  • First Online:
Concurrency and Hardware Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2549))

Abstract

We describe a methodology for analyzing timed systems symbolically. Given a formula representing a set of timed states, we describe howto determine a new formula that represents the set of states reachable by taking a discrete transition or by advancing time. The symbolic representations are given as formulae expressed in a simple first-order logic over constraints of the form x-y ≤ d which can be combined with Boolean operators and existentially quantified. The main contribution is a way of advancing time symbolically essentially by quantifying out a special variable z which is used to represent the current zero point in time. We describe howt o model asynchronous circuits using timed guarded commands and provide examples that demonstrate the potential of the symbolic analysis.

Financially supported by a grant from the Danish Technical Research Council.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. R. Alur. Techniques for Automatic Verication of Real-Time Systems. PhD thesis, Department of Computer Science, Stanford University, 1991. 299

    Google Scholar 

  2. R. Alur and D. Dill. The theory of timed automata. In Proc. Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 28–73. Springer-Verlag, 1991. 275, 278, 279, 285

    Chapter  Google Scholar 

  3. E. Asarin, M. Bozga, A. Kerbrat, O. Maler, M. Pnueli, and A. Rasse. Data structures for the verification of timed automata. In O. Maler, editor, Proc. International Workshop on Hybrid and Real-Time Systems, volume 1201 of Lecture Notes in Computer Science, pages 346–360, Grenoble, France, 1997. Springer-Verlag. 278

    Google Scholar 

  4. F. Balarin. Approximate reachability analysis of timed automata. In Proc. Real-Time Systems Symposium, pages 52–61. IEEE Computer Society Press, 1996. 278

    Google Scholar 

  5. E. Balas. Disjunctive programming. Annals of Discrete Mathematics, 5:3–51, 1979. 300

    Article  MATH  MathSciNet  Google Scholar 

  6. G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient timed reachability analysis using clock difference diagrams. Technical Report 99/105, DoCS, Uppsala University, 1999. 277

    Google Scholar 

  7. W. Belluomini and C. J. Myers. Efficient timing analysis algorithms for timed state space exploration. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 88–100, April 1997. 278

    Google Scholar 

  8. W. Belluomini and C. J. Myers. Verification of timed systems using POSETs. In Proc. Tenth International Conference on Computer-Aided Verification, pages 403–415, June 1998. 278

    Google Scholar 

  9. B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259–273, 1991. 275, 276, 278, 279

    Article  MathSciNet  Google Scholar 

  10. A. Blass and Y. Gurevich. Fixed-choice and independent-choice logics. Technical Report TR-369-98, University of Michigan, August 1998. 280

    Google Scholar 

  11. P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In Proc. 12th International Conference on Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 464–479. Springer-Verlag, July 2000. 299

    Google Scholar 

  12. M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In O. Grumberg, editor, Proc. Ninth International Conference on Computer-Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 179–190, 1997. 278

    Google Scholar 

  13. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986. 274, 302

    Article  Google Scholar 

  14. J. R. Burch. Trace Algebra for Automatic Verification of Real-Time Concurrent Systems. PhD thesis, Carnegie Mellon, August 1992. 278

    Google Scholar 

  15. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, 1990. 274

    Google Scholar 

  16. S. V. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Proc. Real-Time Systems Symposium, pages 266–70. IEEE Computer Society Press, December 1994. 278

    Google Scholar 

  17. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, May 1981. 274, 297

    Google Scholar 

  18. G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proc. Second GI Conference, volume 33 of Lecture Notes in Computer Science, pages 134–183. Springer-Verlag, 1975. 301

    Google Scholar 

  19. S. A. Cook. The complexity of theorem-proving procedures. In Proc. Third Annual ACM Symposium on Theory of Computing, pages 151–158, Shaker Heights, Ohio, 1971. 301

    Google Scholar 

  20. D. C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91–99, 1972. 300, 301

    MATH  Google Scholar 

  21. T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT Press, 1994. 277, 300

    Google Scholar 

  22. E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453–457, August 1975. 275

    Article  MATH  MathSciNet  Google Scholar 

  23. D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer-Verlag, 1989. 276, 277, 278, 301

    Google Scholar 

  24. J. Ferrante and J. R. Geiser. An efficient decision procedure for the theory of rational order. Theoretical Computer Science, 4(2):227–233, 1977. 301

    Article  MATH  MathSciNet  Google Scholar 

  25. J. Ferrante and C. Rackoff. A decision procedure for the first order theory of real addition with order. SIAM Journal of Computing, 4(1):69–76, 1975. 301

    Article  MATH  MathSciNet  Google Scholar 

  26. M. J. Fischer and M. O. Rabin. Super-exponential complexity of presburger arithmetic. In Proc. SIAM-AMS Symposium in Applied Mathematics, volume 7, pages 27–41, 1974. 300

    MathSciNet  Google Scholar 

  27. J. B. J. Fourier. Second extrait. In G. Darboux, editor, Oeuvres, pages 325–328, Paris, 1890. Gauthiers-Villars. 301, 303

    Google Scholar 

  28. K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter System (On formal undecidable theorems in Principia Mathematica and related systems). In Monatshefte für Mathematik und Physik, volume 38, pages 173–198, 1931. 300

    Article  MATH  Google Scholar 

  29. M. R. Greenstreet and T. Ono-Tesfaye. A fast, ASP*, RGD arbiter. In Proc. Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems, pages 173–185, Barcelona, Spain, April 1999. IEEE. 307

    Google Scholar 

  30. T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994. 275, 278, 297, 300

    Article  MATH  MathSciNet  Google Scholar 

  31. D. Hilbert and P. Bernays. Grundlagen der Mathematik, volume 2. Springer-Verlag, 1939. 280

    Google Scholar 

  32. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. 300, 301

    Google Scholar 

  33. N. K. Karmarkar. A newp olynomial-time algorithm for linear programming. Proc. 16th Annual ACM Symposium on Theory of Computing, pages 302–311, 1984. 300

    Google Scholar 

  34. M. Koubarakis. Complexity results for first-order theories of temporal constraints. In J. Doyle, E. Sandewall, and P. Torasso, editors, Proc. Fourth Internatinal Conference on Principles of Knowledge Representation and Reasoning, pages 379–390, San Francisco, California, 1994. Morgan Kaufmann. 300, 301

    Google Scholar 

  35. K. G. Larsen, P. Pettersson, and W. Yi. Model-checking for real-time systems. In Proc. Tenth International Conference on Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 62–88, August 1995. 276, 278

    Google Scholar 

  36. K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1–2):134–152, 1997. 302

    MATH  Google Scholar 

  37. O. Maler and A. Pnueli. Timing analysis of asynchronous circuits using timed automata. In P. E. Camurati and H. Eveking, editors, Proc. Eighth International Conference on Correct Hardware Design and Verification Methods, volume 987 of Lecture Notes in Computer Science, pages 189–205. Springer-Verlag, 1995. 286

    Google Scholar 

  38. J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proc. 13th International Conference on Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111–125, Madrid, Spain, September 1999. 277, 302

    Google Scholar 

  39. J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Fully symbolic model checking of timed systems using difference decision diagrams. In Proc. First International Workshop on Symbolic Model Checking, volume 23–2 of Electronic Notes in Theoretical Computer Science, pages 89–108, Trento, Italy, July 1999. 279

    Google Scholar 

  40. D. Oppen. A 22 2 pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16:323–332, 1978. 301

    Article  MATH  MathSciNet  Google Scholar 

  41. C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. 300

    Google Scholar 

  42. M. Presburger. Über die vollständigkeit eines gewissen systems der arithmetik ganzer zählen, in welchem die addition als einzige operation hervortritt. Comptes-Rendus du I Congres de Mathematiciens des pays Slaves, pages 92–101, 1929. 300

    Google Scholar 

  43. T. G. Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993. 276, 278

    Google Scholar 

  44. T. G. Rokicki and C. J. Myers. Automatic verification of timed circuits. In D. L. Dill, editor, Proc. Sixth International Conference on Computer-Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 468–480, 1994. 278

    Google Scholar 

  45. S. Bornot and J. Sifakis. An algebraic framework for urgency. Information and Computation, 163(1):172–202, 2000. 281

    Article  MATH  MathSciNet  Google Scholar 

  46. R. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 4(24):529–543, October 1977. 300

    Article  MathSciNet  Google Scholar 

  47. A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA, 2nd edition, 1951. 300, 301

    MATH  Google Scholar 

  48. E. Verlind, G. de Jong, and B. Lin. Efficient partial enumeration for timing analysis of asynchronous systems. In Proc. ACM/IEEE Design Automation Conference, pages 55–58, June 1996. 278

    Google Scholar 

  49. H. Wong-Toi and D. L. Dill. Approximations for verifying timing properties. In Theories and Experiences for Real-Time Systems Development, chapter 7, pages 177–204. World Scientific Publishing, 1994. 278

    Google Scholar 

  50. S. Yovine. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1(1–2):123–133, October 1997. 276, 278, 302

    MATH  Google Scholar 

  51. S. Yovine. Model checking timed automata. In Embedded Systems, volume 1494 of Lecture Notes in Computer Science, pages 114–152. Springer-Verlag, October 1998. 278

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Innovation, The IT University of Copenhagen, Denmark

    Jesper Møller, Henrik Hulgaard & Henrik Reif Andersen

Authors
  1. Jesper Møller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Henrik Hulgaard
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Henrik Reif Andersen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Software, Technical University of Catalonia, Campus Nord, Mòdul C5, Jordi Girona Salgado 1-3, 08034, Barcelona, Spain

    Jordi Cortadella

  2. School of Electrical, Electronic and Computer Engineering, University of Newcastle, Newcastle upon Tyne, NE1 7RU, UK

    Alex Yakovlev

  3. Center for Natural Computing, Leiden University, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Møller, J., Hulgaard, H., Reif Andersen, H. (2002). Timed Verification of Asynchronous Circuits. In: Cortadella, J., Yakovlev, A., Rozenberg, G. (eds) Concurrency and Hardware Design. Lecture Notes in Computer Science, vol 2549. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36190-1_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-36190-1_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00199-7

  • Online ISBN: 978-3-540-36190-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation