Timing analysis of asynchronous circuits using timed automata

  • Oded Maler
  • Amir Pnueli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)


In this paper we present a method for modeling asynchronous digital circuits by timed automata. The constructed timed automata serve as “mechanical” and verifiable objects for asynchronous sequential machines in the same sense that (untimed) automata do for synchronous machines. These results, combined with recent results concerning the analysis and synthesis of timed automata provide for the systematic Treatment of a large class of problems that could be treated by conventional simulation methods only in an ad-hoc fashion. The problems that can be solved due to the results presented in this paper include: the reachability analysis of a circuit with uncertainties in gate delays and input arrival times, inferring the necessary timing constraints on input signals that guarantee a proper functioning of a circuit and calculating the delay characteristics of the components required in order to meet some given behavioral specifications.

Notwithstanding the existence of negative theoretical results concerning the worst-case complexity of timed automata analysis algorithms, initial experimentation with the Kronos tool for timing analysis suggest that timed automata derived from circuits might not be so hard to analyze in practice.


Boolean Function Hide Variable Internal Clock Delay Equation Reachability Analysis 
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.


  1. [ACD93]
    R. Alur, C. Courcoubetis, and D.L. Dill, Model Checking in Dense Real Time, Information and Computation 104, 2–34, 1993.Google Scholar
  2. [ACH+95]
    R. Alur, C. Courconbetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine, The Algorithmic Analysis of Hybrid Systems, Theoretical Computer Science 138, 3–34, 1995.Google Scholar
  3. [AD94]
    R. Alur and D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183–235, 1994.Google Scholar
  4. [AMP95-a]
    A. Asarin, O. Maler and A. Pnueli, Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives, Theoretical Computer Science 138, 35–66, 1995.Google Scholar
  5. [AMP95-b]
    A. Asarin, O. Maler and A. Pnueli, Symbolic Synthesis of Discrete and Timed Systems, in A. Nerode (Ed.), Hybrid Systems II, Springer LNCS, to appear, 1995.Google Scholar
  6. [BD91]
    B. Berthomieu and M. Diaz, Modeling and Verification of Time Dependent Systems using Time Petri Nets, IEEE Trans. on Software Engineering 17, 259–273, 1991.Google Scholar
  7. [BM83]
    B. Berthomieu and M. Menasche, An Enumerative Approach for Analyzing Time Petri Nets, in R.E.A. Mason (Ed.) Information Processing 83, North-Holland, 1983.Google Scholar
  8. [BS91]
    J.A. Brzozowski and C-J.H. Seger, Advances in Asynchronous circuit theory Part II: Bounded Inertial Delay Model, MOS Circuits, Design Techniques, EATCS Bulletin 43, 199–263, 1991.Google Scholar
  9. [DOY94]
    C. Daws, A. Olivero and S. Yovine, Verifying et-lotos Programs with Kronos, Proc. FORTE'94, Bern, 1994.Google Scholar
  10. [D89]
    D. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, in J. Sifakis (Ed.), Automatic Verification Methods for Finite State Systems, LNCS 407, Springer, 1989.Google Scholar
  11. [HNSY94]
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Modelchecking for Real-time Systems, Information and Computation 111, 193–244, 1994.Google Scholar
  12. [HWT92]
    G. Hoffmann and H. Wong-Toi, The Input-Output Control of Real-Time Discrete Event Systems, Proc. Real-Time Systems Symposium, IEEE, 1992.Google Scholar
  13. [KM91]
    R.P. Kurshan and K.L. McMillan, Analysis of Digital Circuits Through Symbolic Reduction, IEEE Trans. on Computer-Aided Design, 10, 1350–1371, 1991.Google Scholar
  14. [LB94]
    W.K.C. Lam and R.K. Brayton, Timed Boolean Functions, Kluwer, 1994.Google Scholar
  15. [L89]
    H.R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989.Google Scholar
  16. [LL94]
    M. Linderman and M. Lesser, Simulation of Digital Circuits in the Presence of Uncertainty, TR EE-CEG-94-2, School of EE, Cornell University, 1994.Google Scholar
  17. [ML93]
    A. Martello and S.P. Levitan, Temporal Analysis of Time Bounded Digital Systems, in G.J. Milne and L. Pierre (Eds), Proceedings of Charme'93, LNCS 683, 27–38, Springer, 1993.Google Scholar
  18. [MPS95]
    A. Maler, O. Pnueli and J. Sifakis. On the Synthesis of Discrete Controllers for Timed Systems, in E.W. Mayr and C. Puech (Eds), Proceedings of STACS'95, LNCS 900, 229–242, Springer, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Oded Maler
    • 1
  • Amir Pnueli
    • 2
  1. 1.Spectre-VerimagMiniparc-zirstMontbonnotFrance
  2. 2.Dept. of Computer ScienceWeizmann InstRehovotIsrael

Personalised recommendations