This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Formal Description and Verification of Hardware Timing
July 1991 (vol. 40 no. 7)
pp. 811-826

A formalism in which timing properties of digital hardware may be specified, derived, and formally verified is introduced as a rigorous theory for hardware timing. A rigorous modeling framework has been used to create a family of related verification techniques rather than a single timing analysis tool. This framework is based on a model of interacting finite state machines called CIRCAL, a formalism developed for the purpose of describing and validating complex concurrent systems. In this approach to hardware timing analysis, the presence of a composition operator is all-pervasive. It provides a single, uniform mechanism for describing the behavior of interacting hardware modules and for establishing and describing the timing properties of such modules.

[1] R. E. Bryant, "Symbolic verification of MOS circuits," inProc. 1985 Chapel Hill Conf. VLSI, H. Fuchs, Ed. Rockville, MD: Computer Science Press, 1985.
[2] B. Davie,Formal Specification and Verification in VLSI Design. Edinburgh, Scotland: Edinburgh University Press, 1990.
[3] M. Gordon, "Why higher-order logic is a good formalism for specifying and verifying hardware," inFormal Aspects of VLSI Design. Proc. 1985 Edinburgh Workshop VLSI, G. J. Milne and P. A. Subrahmanyam, Eds. Amsterdam, The Netherlands: North-Holland, 1986.
[4] K. Hanna, "Specification and verification using higher-order logic,"Proc. 7th Int. Conf. Comput. Hardware Description Languages Appl. (CHDL '85), Tokyo, C. J. Koomen&T. Moto-oka, Eds. Amsterdam, The Netherlands: North Holland, 1985.
[5] R. B. Hitchcock, "Timing verification and the timing analysis problem," inProc. 19th Design Automat. Conf., IEEE Computer Society Press, 1982.
[6] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[7] J.E. Hopcroft and J.D. Ullman,Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Mass., 1979.
[8] IEEE,IEEE Standard VHDL Reference Manual, 1988.
[9] G. J. Milne, "CIRCAL: A calculus for circuit description,"Integration, VLSI J.vol. 1, nos. 2&3, 1983.
[10] G. J. Milne, "CIRCAL and the representation of communication, concurrency and time,"ACM Trans. Prog. Lang. Sys., vol. 7, no. 2, Apr. 1985.
[11] G. J. Milne, "Simulation and verification: Related techniques for hardware analysis," inProc. 7th Int. Conf. Comput. Hardware Description Languages Appls (CHDL'85), Tokyo, C. J. Koomen and T. Moto-oka, Eds. Amsterdam, The Netherlands: North-Holland, 1985.
[12] G. J. Milne, "Describing and simulating complex systems," Res. Rep. HDV- 6-89, Dep. Comput. Sci., Univ. of Strathclyde, Glasgow, Scotland, U.K. Dec. 1989.
[13] R. Milner, "Process constructors and interpretations," inProc. Inform. Processing 86, IFIP, North-Holland, 1986.
[14] R. Milner,Communication and Concurrency, Englewood Cliffs, NJ: Prentice-Hall, 1989.
[15] F. Moller, "The semantics of CIRCAL," Res. Rep. HDV-3-89, Dep. Comput. Sci., Univ. of Strathclyde, Glasgow, Scotland, Mar. 1989.
[16] B. Moszkowski, "A temporal logic for reasoning about hardware," inProc. 6th Int. Conf. Comput. Hardware Description Languages Appl., Pittsburgh, PA, T. Uehara and M. Barbacci, Eds. North-Holland, 1983.
[17] J. S. Ostroff, "Deciding properties of timed transition models,"IEEE Trans. Parallel Distributed Syst., vol. 1, no. 2, Apr. 1990.
[18] N. Traub, "A formal approach to hardware analysis," Ph.D. dissertation, Dep. Comput. Sci., Univ. of Edinburgh, Scotland, U.K. 1987.

Index Terms:
formal description; verification; hardware timing; modeling framework; verification techniques; finite state machines; CIRCAL; finite automata; logic design.
Citation:
G.J. Milne, "The Formal Description and Verification of Hardware Timing," IEEE Transactions on Computers, vol. 40, no. 7, pp. 811-826, July 1991, doi:10.1109/12.83619
Usage of this product signifies your acceptance of the Terms of Use.