Abstract
A specification language, veritas +, based on type theory, is proposed as being an ideal notation for specifying and reasoning about digital systems. The development, within veritas +, of a formal theory of arithmetic and numerals is outlined and its application to the specification, at differing levels of abstraction, of arithmetic devices is illustrated. A significant theorem is established within this theory that describes the relationship between specifications and iterative implementations of arithmetic functions and thus provides a general approach to the synthesis and formal verification of arithmetic circuits.
A brief account is given of the computational implementation of the veritas + logic.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
7 References
Constable, R.L., et al., “Implementing Mathematics with the Nuprl Proof Development System”, Prentice-Hall, 1986
Gordon, M.J., “A Machine Oriented Formulation of Higher-Order Logic” Technical Report 68, Computer Laboratory, University of Cambridge, 1985.
Gordon, M.J., “Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware” in “Formal Aspects of VLSI Design”, ed. G.J. Milne and P.A. Subrahmanyam, North Holland, 1986.
Gordon, M.J., Milner, A.J., Wadsworth, C.P., “Edinburgh LCF — a Mechanised Logic of Computation”, Vol 78, LNCS, Springer-Verlag, 1979.
Hanna, F.K., “Overview of the Veritas Project”, Technical Report, University of Kent, 1983.
Hanna, F.K., Daeche, N., “Specification and Verification using Higher-Order Logic”, in Proc CHDL, ed. Koomen and Moto-oka, North Holland, 1985.
Hanna, F.K., Daeche, N., “Specification and Verification using Higher-Order Logic: A Case Study”, in “Formal Aspects of VLSI Design”, ed. G.J. Milne and P.A. Subrahmanyam, North Holland, 1986.
Hanna, F.K., Daeche, N., “Purely Functional Implementation of a Logic” 8th Intnl Conf on Automated Deduction, pp598–607, Vol 230, LNCS, Springer-Verlag, 1986.
Hanna, F.K., Daeche, N., “Computational Logic: An Algebraic Approach”, Technical Report (3 vols), University of Kent, 1988
Martin-Löf, P. “Constructive mathematics and computer programming”, pp501–518, Phil Trans R. Soc. London, A 312, 1984.
Sheeran, M., “Describing and Reasoning about Circuits using Relations”, in Proc 1986 Leeds workshop on Theoretical Aspects of VLSI Design.
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hanna, F.K., Daeche, N., Longley, M. (1990). Veritas+: A specification language based on type theory. In: Leeser, M., Brown, G. (eds) Hardware Specification, Verification and Synthesis: Mathematical Aspects. Lecture Notes in Computer Science, vol 408. Springer, New York, NY. https://doi.org/10.1007/0-387-97226-9_37
Download citation
DOI: https://doi.org/10.1007/0-387-97226-9_37
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-97226-8
Online ISBN: 978-0-387-34801-8
eBook Packages: Springer Book Archive