A graph-based method for timing diagrams representation and verification

  • Viktor Cingel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


A graph-based approach to the verification of timing constraints in timing diagrams is described. Timing diagrams as a specification tool together with a specialized theorem prover for inequalities are used to support the timing design process. The method for automatically proving the consistency of a designed timing diagram works over a graph representing the timing diagram and constraints. It is based on the detection of cycles in this graph. A simple extension of this method enables the generation of a set of timing constraints which have to be fulfilled in the given timing diagram.


Timing Constraint Timing Parameter Timing Diagram Propositional Variant Cycle Detection 
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. 1.
    Antoine,C.-Goff,B.L.: Timing Diagrams for Writing and Checking Logical and Behavioural Properties of Integrated Circuits. In. Proc.of Advanced Research Workshop on Correct Hardware Design Methodologies, Turin, June 1991.Google Scholar
  2. 2.
    Borriello,G.-Katz,R.H.: Synthesizing Transducers from Interface Specifications. In. Proc. of VLSI'87 (C.H.Sequin edt.), Elsevier Sc. Publisher, 1988, pp.403–418.Google Scholar
  3. 3.
    Cingel,V.: Specification and Verification of Timing in Digital Systems. Ph.D. Thesis, Department of Computer Science and Engineering, Slovak Technical University, Bratislava, Jan 1991, 175 pp (in Slovak).Google Scholar
  4. 4.
    Claesen,L. et al.: Efficient False Path Elimination Algorithm for Timing Verification by Event Graph Preprocessing. Integration, the VLSI journal, Vol.2, 1989, pp.173–188.Google Scholar
  5. 5.
    Dagenais,M.R.-Rumin,N.C.: Automatic Determination of Optimal Clocking Parameters in Synchronous MOS VLSI Circuits. In. Advanced in CAD for VLSI, Vol.5, 1987, pp.20–33.Google Scholar
  6. 6.
    Eveking,H.-Mai,Ch.: Formal Verification of Timing Conditions. In. Proc. of 1st EDAC, Glasgow, 1990, pp.512–517.Google Scholar
  7. 7.
    Herbert,J.: Formal Verification of Basic Memory Devices. In. Formal VLSI Correctness Verification, (L.Claesen edt.), Elsevier Sc. Publisher, 1990.Google Scholar
  8. 8.
    Jahanian,F.-Mok,A.K.L.: A Graph-Theoretic Approach for Timing Analysis and its Implementation. IEEE Tr. on Computers, C-36, No.8, Aug 1987, pp.961–975.Google Scholar
  9. 9.
    Jouppi,N.P.: Timing analysis and Performance Improvement of MOS VLSI Designs. IEEE Tr. on CAD, No.4, 1987, pp.650–665.Google Scholar
  10. 10.
    Loveland,D.W.: Automated theorem proving: A logical basis. Fundamental studies in Computer Science Vol.6., North-Holland, 1978.Google Scholar
  11. 11.
    Reed,G.M.-Roscoe,A.W.: A Timed Model of Communicating Sequential Processes. In. ICALP-86, LNCS-226, Springer Verlag, 1986.Google Scholar
  12. 12.
    Reingold,M.E.: Combinatorial Algorithms. Theory and Practice. Prentice Hall, 1977, 441 pp.Google Scholar
  13. 13.
    Salem,A.: Formal Reasoning on Timing Constructs in VHDL. (Lecture Notes), presented at Advanced Research Workshop on Correct Hardware Design Methodologies, Turin, June 1991.Google Scholar
  14. 14.
    Seger,C.J.-Bryant,R.E.: Modeling of Circuit Delays in Symbolic Simulation. In. Formal VLSI Correctness Verification (L.Claesen edt.), Elsevier Sc. Publisher, 1990, pp. 23–37.Google Scholar
  15. 15.
    Subrahmanyam,P.A.: What's in Timing Discipline ? Considerations in the Specification and Synthesis of Systems with Interacting Asynchronous and Synchronous Components. In. Hardware Specification, Verification and Synthesis: Mathematical Aspects. (eds. M.Leeser, G.Brown), LNCS-408, Springer Verlag, 1990, pp.202–223.Google Scholar
  16. 16.
    Unger,S.H.-Tan,C.J.: Clocking Schemes for High-Speed Digital Systems. IEEE Tr. on Computers, C-35, No.10, Oct 1986, pp.880–895.Google Scholar
  17. 17.
    Wallace,D.E.-Sequin,C.H.: ATV: An Abstract Timing Verifier.In. Proc. of 26th ACM/IEEE Design Automation Conference, 1989, pp.655–661.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Viktor Cingel
    • 1
  1. 1.Department of Computer Science and EngineeringSlovak Technical UniversityBratislavaSlovakia

Personalised recommendations