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

On Specifications and Proofs of Timed Circuits

  • Chapter
  • First Online:
Principles of Systems Design

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

  • 826 Accesses

Abstract

Given a discrete-state continuous-time reactive system, like a digital circuit, the classical approach is to first model it as a state transition system and then prove its properties. Our contribution advocates a different approach: to directly operate on the input-output behavior of such systems, without identifying states and their transitions in the first place. We discuss the benefits of this approach at hand of some examples, which demonstrate that it nicely integrates with concepts of self-stabilization and fault-tolerance. We also elaborate on some unexpected artefacts of module composition in our framework, and conclude with some open research questions.

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement 716562). The work was also supported by the Austrian Science Fund project DMAC (P32431) and by the ANR project DREAMY (ANR-21-CE48-0003).

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

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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

Similar content being viewed by others

Notes

  1. 1.

    Metastable upsets can occur in any state-holding device with discrete stable states, such as memory cells. If a new state transition is triggered before the state change caused by the previous one has settled, an intermediate output value may be observed arbitrarily late. Even Byzantine (i.e., “worst-case”) fault-tolerance techniques are incapable of containing the effects of metastable upsets perfectly [22], since a signal outside the (discrete) value domain is not just an arbitrary regular signal. Metastability is not restricted to electrical systems. For example, an engineered genetic toggle switch [28], acting as a memory cell storing 0 or 1, was observed to exhibit metastable behavior besides its two stable states.

  2. 2.

    Consensus [42], a basic fault-tolerance task, can be solved deterministically in synchronous systems, but not in asynchronous systems [21].

  3. 3.

    Whereas one could extend our framework to restrict the adversary here, e.g., to capture probabilistic choice, we will not consider this possibility in this work.

  4. 4.

    Since we can consider the inertial delay channel to be a basic module here, we need not care about implementability at that point.

References

  1. Albert, R., Othmer, H.G.: The topology of the regulatory interactions predicts the expression pattern of the segment polarity genes in drosophila melanogaster. J. Theor. Biol. 223(1), 1–18 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  2. de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Sangiovanni-Vincentelli, A., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108–122. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45828-X_9

    Chapter  Google Scholar 

  3. Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000). https://doi.org/10.1109/5.871304

    Article  Google Scholar 

  4. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8. http://www.sciencedirect.com/science/article/pii/0304397594900108

  5. Awerbuch, B.: Complexity of network synchronization. JACM 32(4), 804–823 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164–177. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40708-6_13

    Chapter  Google Scholar 

  7. Baumann, R.: Radiation-induced soft errors in advanced semiconductor technologies. IEEE Trans. Device Mater. Reliab. 5(3), 305–316 (2005)

    Article  Google Scholar 

  8. Bellido-Diaz, M.J., Juan-Chico, J., Acosta, A., Valencia, M., Huertas, J.L.: Logical modelling of delay degradation effect in static CMOS gates. IEE Proc. Circuits Devices Syst. 147(2), 107–117 (2000)

    Article  Google Scholar 

  9. Broy, M., Stølen, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, New York (2001). https://doi.org/10.1007/978-1-4613-0091-5

    Book  MATH  Google Scholar 

  10. Constantinescu, C.: Trends and challenges in VLSI circuit reliability. IEEE Micro 23(4), 14–19 (2003)

    Article  Google Scholar 

  11. Daliot, A., Dolev, D., Parnas, H.: Self-stabilizing pulse synchronization inspired by biological pacemaker networks. In: Huang, S.-T., Herman, T. (eds.) SSS 2003. LNCS, vol. 2704, pp. 32–48. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45032-7_3

    Chapter  MATH  Google Scholar 

  12. Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. CACM 17(11), 643–644 (1974)

    Article  MATH  Google Scholar 

  13. Dixit, A., Wood, A.: The impact of new technology on soft error rates. In: Proceedings of IRPS, pp. 5B.4.1–5B.4.7 (2011)

    Google Scholar 

  14. Dolev, D., Dwork, C., Stockmeyer, L.: On the minimal synchronism needed for distributed consensus. JACM 34(1), 77–97 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  15. Dolev, D., Függer, M., Lenzen, C., Perner, M., Schmid, U.: HEX: scaling honeycombs is easier than scaling clock trees. In: Proceedings of the 25th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA 2013), pp. 164–175 (2013)

    Google Scholar 

  16. Dolev, D., Függer, M., Lenzen, C., Posch, M., Schmid, U., Steininger, A.: Rigorously modeling self-stabilizing fault-tolerant circuits: an ultra-robust clocking scheme for systems-on-chip. JCSS 80(4), 860–900 (2014)

    MathSciNet  MATH  Google Scholar 

  17. Dolev, D., Függer, M., Lenzen, C., Schmid, U.: Fault-tolerant algorithms for tick-generation in asynchronous logic: robust pulse generation. J. ACM 61(5), 30:1–30:74 (2014). https://doi.org/10.1145/2560561

  18. Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)

    Book  MATH  Google Scholar 

  19. Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. JACM 35(2), 288–323 (1988)

    Article  MathSciNet  Google Scholar 

  20. Fischer, M.J.: The consensus problem in unreliable distributed systems (a brief survey). In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 127–140. Springer, Heidelberg (1983). https://doi.org/10.1007/3-540-12689-9_99

    Chapter  Google Scholar 

  21. Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. JACM 32(2), 374–382 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  22. Friedrichs, S., Függer, M., Lenzen, C.: Metastability-containing circuits. IEEE Trans. Comput. 67(8), 1167–1183 (2018). https://doi.org/10.1109/TC.2018.2808185. https://doi.org/10.1109/TC.2018.2808185

  23. Fuchs, G., Steininger, A.: VLSI implementation of a distributed algorithm for fault-tolerant clock generation. J. Electr. Comput. Eng. 2011, 936712 (2011)

    Google Scholar 

  24. Függer, M., Najvirt, R., Nowak, T., Schmid, U.: A faithful binary circuit model. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(10), 2784–2797 (2020). https://doi.org/10.1109/TCAD.2019.2937748

    Article  Google Scholar 

  25. Függer, M., Kushwaha, M., Nowak, T.: Digital circuit design for biological and silicon computers. In: Singh, V. (ed.) Advances in Synthetic Biology, pp. 153–171. Springer, Singapore (2020). https://doi.org/10.1007/978-981-15-0081-7_9

    Chapter  Google Scholar 

  26. Függer, M., Nowak, T., Schmid, U.: Unfaithful glitch propagation in existing binary circuit models. IEEE Trans. Comput. 65(3), 964–978 (2016). https://doi.org/10.1109/TC.2015.2435791. http://ieeexplore.ieee.org/stamp/stamp.jsp?tp= &arnumber=7110587

  27. Függer, M., Schmid, U.: Reconciling fault-tolerant distributed computing and systems-on-chip. Distrib. Comput. 24(6), 323–355 (2012)

    Article  MATH  Google Scholar 

  28. Gardner, T.S., Cantor, C.R., Collins, J.J.: Construction of a genetic toggle switch in Escherichia coli. Nature 403, 339–342 (2000)

    Article  Google Scholar 

  29. Gorochowski, T.E., et al.: Genetic circuit characterization and debugging using RNA-SEQ. Mol. Syst. Biol. 13(11), 952 (2017)

    Article  Google Scholar 

  30. Hasty, J., McMillen, D., Collins, J.J.: Engineered gene circuits. Nature 420, 224–230 (2002)

    Article  Google Scholar 

  31. International Technology Roadmap for Semiconductors (2012). http://www.itrs.net

  32. Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I/O Automata. Morgan & Claypool Publishers, San Francisco (2006)

    Book  MATH  Google Scholar 

  33. Koren, I., Koren, Z.: Defect tolerance in VLSI circuits: techniques and yield analysis. Proc. IEEE 86(9), 1819–1838 (1998). https://doi.org/10.1109/5.705525

    Article  Google Scholar 

  34. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. CACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  35. Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  36. Lee, E.A., Varaiya, P.: Structure and Interpretation of Signals and Systems, 2nd edn. LeeVaraiya.org (2011)

    Google Scholar 

  37. Lynch, N., Vaandrager, F.: Forward and backward simulations, I: untimed systems. Inf. Comput. 121(2), 214–233 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  38. Lynch, N., Vaandrager, F.: Forward and backward simulations, II: timing-based systems. Inf. Comput. 128(1), 1–25 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  39. Marino, L.: General theory of metastable operation. IEEE Trans. Comput. C30(2), 107–115 (1981)

    Article  MATH  Google Scholar 

  40. Maza, M.S., Aranda, M.L.: Analysis of clock distribution networks in the presence of crosstalk and groundbounce. In: Proceedings of ICECS, pp. 773–776 (2001)

    Google Scholar 

  41. Nielsen, A.A., et al.: Genetic circuit design automation. Science 352(6281), aac7341 (2016)

    Google Scholar 

  42. Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. JACM 27, 228–234 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  43. Peercy, M., Banerjee, P.: Fault tolerant VLSI systems. Proc. IEEE 81(5), 745–758 (1993)

    Article  Google Scholar 

  44. Santos-Moreno, J., Tasiudi, E., Stelling, J., Schaerli, Y.: Multistable and dynamic CRISPRI-based synthetic circuits. Nat. Commun. 11(1), 1–8 (2020)

    Article  Google Scholar 

  45. Sivan, E., Parnas, H., Dolev, D.: Fault tolerance in the cardiac ganglion of the lobster. Biol. Cybern. 81(1), 11–23 (1999)

    Article  MATH  Google Scholar 

  46. Stricker, J., Cookson, S., Bennett, M.R., Mather, W.H., Tsimring, L.S., Hasty, J.: A fast, robust and tunable synthetic gene oscillator. Nature 456, 516–519 (2008)

    Article  Google Scholar 

  47. Sutherland, I.E.: Micropipelines. CACM 32(6), 720–738 (1989)

    Article  Google Scholar 

  48. Thomas, R.: Boolean formalization of genetic control circuits. J. Theor. Biol. 42(3), 563–585 (1973)

    Article  Google Scholar 

  49. Unger, S.H.: Asynchronous sequential switching circuits with unrestricted input changes. IEEE Trans. Comput. 20(12), 1437–1444 (1971)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, LMF, ENS Paris-Saclay, Université Paris-Saclay, Inria, Gif-sur-Yvette, France

    Matthias Függer

  2. CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

    Christoph Lenzen

  3. TU Wien, Vienna, Austria

    Ulrich Schmid

Authors
  1. Matthias Függer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Lenzen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ulrich Schmid
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ulrich Schmid .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Jean-François Raskin

  2. Institute of Science and Technology Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee

  3. École Normale Supérieure Paris-Saclay, Gif-sur-Yvette, France

    Laurent Doyen

  4. MPI for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Függer, M., Lenzen, C., Schmid, U. (2022). On Specifications and Proofs of Timed Circuits. In: Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds) Principles of Systems Design. Lecture Notes in Computer Science, vol 13660. Springer, Cham. https://doi.org/10.1007/978-3-031-22337-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-22337-2_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-22336-5

  • Online ISBN: 978-3-031-22337-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation