Abstract
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.
This research was supported in part by the European Community projects BRA-REACT (6021) and HYBRID EC-US-043. Verimag is a joint laboratory of cnrs, inpg, ujf and verilog sa. spectre is a project of inria.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
R. Alur, C. Courcoubetis, and D.L. Dill, Model Checking in Dense Real Time, Information and Computation 104, 2–34, 1993.
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.
R. Alur and D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183–235, 1994.
A. Asarin, O. Maler and A. Pnueli, Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives, Theoretical Computer Science 138, 35–66, 1995.
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.
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.
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.
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.
C. Daws, A. Olivero and S. Yovine, Verifying et-lotos Programs with Kronos, Proc. FORTE'94, Bern, 1994.
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.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Modelchecking for Real-time Systems, Information and Computation 111, 193–244, 1994.
G. Hoffmann and H. Wong-Toi, The Input-Output Control of Real-Time Discrete Event Systems, Proc. Real-Time Systems Symposium, IEEE, 1992.
R.P. Kurshan and K.L. McMillan, Analysis of Digital Circuits Through Symbolic Reduction, IEEE Trans. on Computer-Aided Design, 10, 1350–1371, 1991.
W.K.C. Lam and R.K. Brayton, Timed Boolean Functions, Kluwer, 1994.
H.R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maler, O., Pnueli, A. (1995). Timing analysis of asynchronous circuits using timed automata. In: Camurati, P.E., Eveking, H. (eds) Correct Hardware Design and Verification Methods. CHARME 1995. Lecture Notes in Computer Science, vol 987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60385-9_12
Download citation
DOI: https://doi.org/10.1007/3-540-60385-9_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60385-6
Online ISBN: 978-3-540-45516-5
eBook Packages: Springer Book Archive