Abstract
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).
Keywords
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.
Download to read the full chapter text
Chapter PDF
References
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.
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.
R. L. Constable, et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986.
M. P. Fourman, Formal System Design, pp 191–235, in Formal Methods for VLSI Design, ed J. Staunstrup, North Holland, 1990.
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.
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.
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.
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.
F. K. Hanna and N. Daeche, Dependent Types and Formal Synthesis, pp121–135, Phil Trans. Royal Soc, Series A, (1992), Vol 339.
B. Jacobs, T. Melham, Translating Dependent Type Theory into Higher Order Logic, Tech. Rep., University of Cambridge, Computer Laboratory, 1992.
L. Paulson, T. Nipkow, Isabelle tutorial and user's manual, Tech. Rep., University of Cambridge, Computer Laboratory, 1990.
VHDL Language Reference Manual, IEEE standard 1076–1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hanna, K., Daeche, N. (1993). Strongly-typed theory of structures and behaviours. In: Milne, G.J., Pierre, L. (eds) Correct Hardware Design and Verification Methods. CHARME 1993. Lecture Notes in Computer Science, vol 683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021713
Download citation
DOI: https://doi.org/10.1007/BFb0021713
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56778-3
Online ISBN: 978-3-540-70655-7
eBook Packages: Springer Book Archive