Strongly-typed theory of structures and behaviours

  • Keith Hanna
  • Neil Daeche
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


This paper describes an approach to capturing the relation between circuits and their behaviours within a formal theory. The method exploits dependent types to achieve a rigorous yet theoretically simple connection between circuits (treated as graphs) and their behavioural specifications (treated as predicates). An example is given of a behavioural extraction function and it is shown how a type for modules can be defined that is sufficiently fine to guarantee that the behaviour of a module will satisfy its behavioural specification. The method is discussed in relation to VHDL and in relation to formal synthesis, (a process whereby one starts with a behavioural specification and, using an interactive goal-directed approach, ends up with a circuit and a formal proof that it satisfies the given behavioural specification).


Output Port Formal Verification Dependent Type Hardware Description Language Behavioural Specification 
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. [B92]
    R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, J. Van Tassel. Experience with Embedding Hardware Description Languages in HOL, pp 129–156, IFIP Trans. Vol A-10, Theorem Provers in Circuit Design, North Holland, 1992.Google Scholar
  2. [BHY92]
    B. C. Brock, W. A. Hunt, W. D. Young, Introduction to a Formally Defined Hardware Description Language, pp 3–35, IFIP Trans. Vol A-10, Theorem Provers in Circuit Design, North Holland, 1992.Google Scholar
  3. [C86]
    R. L. Constable, et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986.Google Scholar
  4. [F90]
    M. P. Fourman, Formal System Design, pp 191–235, in Formal Methods for VLSI Design, ed J. Staunstrup, North Holland, 1990.Google Scholar
  5. [HD86]
    F. K. Hanna, N. Daeche Specification and Verification of Digital Systems using Higher-order Predicate Logic, pp 242–254, Proc IEE, Vol 133, Pt E, No 5, Sept 1986.Google Scholar
  6. [HLD89]
    F. K. Hanna, M. Longley, N. Daeche, Formal Synthesis of Digital Systems, in pp. 153–169 L. J. M. Claesen (Ed), Applied formal methods for correct VLSI design, North-Holland, 1989.Google Scholar
  7. [HDL90]
    F. K. Hanna, N. Daeche, M. Longley, Specification and Verification using Dependent Types, pp949–964, IEEE Trans on SE, Vol. 16, No. 9, Sept 1990.Google Scholar
  8. [HDH92]
    F. K. Hanna, N. Daeche, G. Howells, Implementation of the Veritas Design Logic, pp 77–94, IFIP Trans. Vol A-10, Theorem Provers in Circuit Design, North Holland, 1992.Google Scholar
  9. [HD92]
    F. K. Hanna and N. Daeche, Dependent Types and Formal Synthesis, pp121–135, Phil Trans. Royal Soc, Series A, (1992), Vol 339.Google Scholar
  10. [JM92]
    B. Jacobs, T. Melham, Translating Dependent Type Theory into Higher Order Logic, Tech. Rep., University of Cambridge, Computer Laboratory, 1992.Google Scholar
  11. [PT90]
    L. Paulson, T. Nipkow, Isabelle tutorial and user's manual, Tech. Rep., University of Cambridge, Computer Laboratory, 1990.Google Scholar
  12. [VHDL87]
    VHDL Language Reference Manual, IEEE standard 1076–1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Keith Hanna
    • 1
  • Neil Daeche
    • 1
  1. 1.University of KentCanterburyUK

Personalised recommendations