Formal Timing Analysis of Digital Circuits

  • Qurat Ul AinEmail author
  • Osman Hasan
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1008)


Formal verification provides complete and sound analysis results and has widely been advocated for the functional verification of digital circuits. Besides the functional verification, a very important aspect of digital circuit design process is their timing analysis. However, despite its importance and critical nature, timing analysis is usually performed using traditional techniques, like gate-level simulation or static timing analysis, which provide approximate results due to their in-exhaustive nature and thus may lead to an undesired functional behavior as well. To overcome these issues, we propose a generic framework to conduct the formal timing analysis using the Uppaal model checker in this paper. The first step in the proposed framework is to represent the timing characteristics of the given digital circuit using a state transition diagram in Uppaal. In this model, delays are integrated using the corresponding technology parameters and the information about timing paths is added using Quratus Prime Pro, which is used as a path extracting tool. The Uppaal timing model is then verified through TCTL properties to obtain timing related information, like maximum delay. For illustration purposes, we present the analysis of a number of real-world digital circuits, like Full Adder, 4-Bit Ripple Carry Adder, Shift Registers as well as C17, S27, S208, and S386 benchmark circuits.


Timed automata Uppaal Formal verification Timing analysis Model checking 


  1. 1.
    Abbasi, I.H., Lodhi, F.K., Kamboh, A.M., Hasan, O.: Formal verification of gate-level multiple side channel parameters to detect hardware Trojans. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 75–92. Springer, Cham (2017). Scholar
  2. 2.
    Ul Ain, Q.: Formal Timing Analysis of Digital Circuits (2018).
  3. 3.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Logic in Computer Science, pp. 414–425. IEEE (1990)Google Scholar
  4. 4.
    Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of verilog models. In: Proceedings of 41st Design Automation Conference, pp. 218–223 (2004)Google Scholar
  5. 5.
    Bara, A., Bazargan-Sabet, P., Chevallier, R., Ledu, D., Encrenaz, E., Renault, P.: Formal verification of timed VHDL programs. In: Forum on Specification Design Languages, pp. 80–85. IET (2010)Google Scholar
  6. 6.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal 4.0 (2006)Google Scholar
  7. 7.
    Bérard, B., et al.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2013). Scholar
  8. 8.
    Bozga, M., Jianmin, H., Maler, O., Yovine, S.: Verification of asynchronous circuits using timed automata. Electron. Notes Theor. Comput. Sci. 65(6), 47–59 (2002)CrossRefGoogle Scholar
  9. 9.
    Braibant, T.: Coquet: a Coq library for verifying hardware. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 330–345. Springer, Heidelberg (2011). Scholar
  10. 10.
    Brglez, F., Bryan, D., Kozminski, K.: Notes on the ISCAS 1989 benchmark circuits. North-Carolina State University (1989)Google Scholar
  11. 11.
    Bryan, D.: The ISCAS 1985 benchmark circuits and netlist format. North Carolina State University, vol. 25 (1985)Google Scholar
  12. 12.
    Chevallier, R., Encrenaz-Tiphene, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Form. Methods Syst. Des. 34(1), 59–81 (2009)CrossRefGoogle Scholar
  13. 13.
    Clarisó, R., Cortadella, J.: Verification of timed circuits with symbolic delays. In: Asia and South Pacific Design Automation Conference, pp. 628–633. IEEE (2004)Google Scholar
  14. 14.
    Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, Third Edition, pp. 7162–7170. IGI Global (2015)Google Scholar
  15. 15.
    Irfan, A., Cimatti, A., Griggio, A., Roveri, M., Sebastiani, R.: Verilog2SMV: a tool for word-level verification. In: Design Automation Test in Europe Conference Exhibition, pp. 1156–1159 (2016)Google Scholar
  16. 16.
    Kilts, S.: Static Timing Analysis. Advanced FPGA Design: Architecture, Implementation, and Optimization, pp. 269–278 (2007)Google Scholar
  17. 17.
    Mano, M.M., Kime, C.R.: Logic and Computer Design Fundamentals, vol. 3. Prentice Hall, Upper Saddle River (2008)Google Scholar
  18. 18.
    Maxfield, C.: Bebop to the Boolean Boogie: An Unconventional Guide to Electronics. Newnes, Oxford (2008)Google Scholar
  19. 19.
    Mukhopadhyay, D., Chakraborty, R.S.: Hardware Security: Design, Threats, and Safeguards. Chapman and Hall/CRC, Boca Raton (2014)CrossRefGoogle Scholar
  20. 20.
    Patterson, D.A., Hennessy, J.L.: Computer Organization and Design. zadnje izdanje (1994)CrossRefGoogle Scholar
  21. 21.
    Quartus prime standard edition handbook (2015)Google Scholar
  22. 22.
    Rabaey, J.M., Chandrakasan, A.P., Nikolic, B.: Digital Integrated Circuits, vol. 2. Prentice hall Englewood Cliffs, New Jersey (2002)Google Scholar
  23. 23.
    Razavi, B.: Design of Analog CMOS Integrated Circuits. Tata McGraw-Hill Education, New York City (2002)Google Scholar
  24. 24.
    Salah, R.B., Bozga, M., Maler, O.: On timing analysis of combinational circuits. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 204–218. Springer, Heidelberg (2004). Scholar
  25. 25.
    Saleh, R., Jou, S.J., Newton, A.R.: Gate-level simulation. In: Saleh, R., Jou, S.J., Newton, A.R. (eds.) Mixed-Mode Simulation and Analog Multilevel Simulation, pp. 123–152. Springer, Heidelberg (1994). Scholar
  26. 26.
  27. 27.
    Shiraz, S., Hasan, O.: A library for combinational circuit verification using the hol theorem prover. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 37(2), 512–516 (2018)CrossRefGoogle Scholar
  28. 28.
    Takan, S., Guler, B., Ayav, T.: Model checker-based delay fault testing of sequential circuits. In: Architecture of Computing Systems, pp. 1–7. VDE (2015)Google Scholar
  29. 29.
    Wei, S., Meguerdichian, S., Potkonjak, M.: Malicious circuitry detection using thermal conditioning. IEEE Trans. Inf. Forensics Secur. 6(3), 1136–1145 (2011)CrossRefGoogle Scholar
  30. 30.
    Weste, N.H., Harris, D.: CMOS VLSI Design: A Circuits and Systems Perspective. Pearson Education, London (2015)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST)IslamabadPakistan

Personalised recommendations