On Timing Analysis of Combinational Circuits

  • Ramzi Ben Salah
  • Marius Bozga
  • Oded Maler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


In this paper we report some progress in applying timed automata technology to large-scale problems. We focus on the problem of finding maximal stabilization time for combinational circuits whose inputs change only once and hence they can be modeled using acyclic timed automata. We develop a “divide-and-conquer” methodology based on decomposing the circuit into sub-circuits and using timed automata analysis tools to build conservative low-complexity approximations of the sub-circuits to be used as inputs for the rest of the system. Some preliminary results of this methodology are reported.


Boolean Function Stabilization Time Delay Operator Symbolic State Reachability Graph 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [A99]
    Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. [AD94]
    Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [AIKY95]
    Alur, R., Itai, A., Kurshan, R.P., Yanakakis, M.: Timing Verification by Successive Approximation. Information and Computation 118, 142–157 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  4. [B96]
    Balarin, F.: Approximate Reachability Analysis of Timed Automata. In: Proc. RTSS 1996, pp. 52–61. IEEE, Los Alamitos (1996)Google Scholar
  5. [BGM02]
    Bozga, M., Graf, S., Mounier, L.: IF-2.0: A Validation Environment for Component-Based Real-Time Systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 343. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. [D89]
    Dill, D.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, Springer, Heidelberg (1990)Google Scholar
  7. [BFKM97]
    Bozga, M., Fernandez, J.-C., Kerbrat, A., Mounier, L.: Protocol Verification with the Aldebaran Toolset. Software Tools for Technology Transfer 1, 166–183 (1997)zbMATHCrossRefGoogle Scholar
  8. [BDM+98]
    Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a Model-Checking Tool for Real-Time Systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. [BJMY02]
    Bozga, M., Jianmin, H., Maler, O., Yovine, S.: Verification of Asynchronous Circuits using Timed Automata. ENTCS, vol. 65 (2002)Google Scholar
  10. [BFG+91]
    Bouajjani, A., Fernandez, J.-C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, Springer, Heidelberg (1991)Google Scholar
  11. [BMPY97]
    Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some Progress in the Symbolic Verification of Timed Automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 179–190. Springer, Heidelberg (1997)Google Scholar
  12. [BMT99]
    Bozga, M., Maler, O., Tripakis, S.: Efficient Verification of Timed Automata using Dense and Discrete Time Semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. [BS94]
    Brzozowski, J.A., Seger, C.-J.H.: Asynchronous Circuits. Springer, Heidelberg (1994)Google Scholar
  14. [HNSY94]
    Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Modelchecking for Real-time Systems. Information and Computation 111, 193–244 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  15. [L89]
    Lewis, H.R.: Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University (1989)Google Scholar
  16. [LPY97]
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Software Tools for Technology Transfer 1/2 (1997)Google Scholar
  17. [MP95]
    Maler, O., Pnueli, A.: Timing Analysis of Asynchronous Circuits using Timed Automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 189–205. Springer, Heidelberg (1995)Google Scholar
  18. [MY96]
    Maler, O., Yovine, S.: Hardware Timing Verification using KRONOS. In: Proc. 7th Israeli Conference on Computer Systems and Software Engineering (1996)Google Scholar
  19. [PCKP00]
    Pena, M.A., Cortadella, J., Kondratyev, A., Pastor, E.: Formal Verification of Safety Properties in Timed Circuits. In: Proc. Async 2000, pp. 2–11. IEEE Press, Los Alamitos (2000)Google Scholar
  20. [TAKB96]
    Tasiran, S., Alur, R., Kurshan, R.P., Brayton, R.: Verifying Abstractions of Timed Systems. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 546–562. Springer, Heidelberg (1996)Google Scholar
  21. [TB97]
    Tasiran, S., Brayton, R.K.: STARI: A Case Study in Compositional and Hierarchical Timing Verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 191–201. Springer, Heidelberg (1997)Google Scholar
  22. [TKB97]
    Tasiran, S., Kukimoto, Y., Brayton, R.K.: Computing Delay with Coupling using Timed Automata. In: Proc. TAU 1997 (1997)Google Scholar
  23. [TKY+98]
    Tasiran, S., Khatri, S.P., Yovine, S., Brayton, R.K., Sangiovanni- Vincentelli, A.: A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 149–166. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  24. [WD94]
    Wong-Toi, H., Dill, D.L.: Approximations for Verifying Timing Properties. In: Theories and Experiences for Real-Time System Development, World Scientific Publishing, Singapore (1994)Google Scholar
  25. [Y97]
    Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1 (1997)Google Scholar
  26. [ZMM03]
    Zheng, H., Mercer, E., Myers, C.: Modular Verification of Timed Circuits using Automatic Abstraction. IEEE Trans. on CAD (2003) (to appear)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Ramzi Ben Salah
    • 1
  • Marius Bozga
    • 1
  • Oded Maler
    • 1
  1. 1.Verimag

Personalised recommendations