Abstract
There is some reluctance towards the use of formal verification methods by the design community. One factor contributing to this lack of enthusiasm is the degree of user sophistication required in representing a design and reasoning about it in most systems, especially those involving theorem provers. To overcome this, we present the use of symbolic programming languages to prove several classes of hardware designs correct.
We start by defining a functional model for the specification of synchronous hardware. Next, we discuss the programming techniques for implementing the model in the symbolic programming language Maple. Given a Maple model (a program) of a design, we execute the program to derive its symbolic behaviour. The Maple system is also used to compare the derived and the reference behaviours. We end by presenting several Maple-based verification examples.
Our contribution to hardware verification is the development of a modeling method within a symbolic programming paradigm, and the ensuing facility for reasoning about certain designs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Fitch, J., “Solving Algebraic Problems with REDUCE,” Journal of Symbolic Computation, 1 pp. 211–217 (1985).
Pavelle, R. and Wang, P. S., “MACSYMA from F to G,” Journal of Symbolic Computation, 1 pp. 69–100 (1985).
B.W. Char, G.J. Fee, K.O. Geddes, G.H. Gonnet, and M.B. Monagan, “A Tutorial Introduction to Maple,” Journal of Symbolic Computation, 2 pp. 179–200 (1986).
Mavaddat, F., “Inductive Assertions on Algorithmic State Machines A Maple-Based Register-Transfer-Level Proof System,” pp. 257–266 in Formal VLSI Correctness Verification, VLSI Design Methods-II, ed. L.J.M. Claesen, North Holland, Amsterdam, Netherlands (1990).
Gordon M., “A Model of Register Transfer Systems with Application to Microcode and VLSI Correctness,” CSR-82–81, University of Edinburgh, Dept. of Computer Science, Edinburgh, Scotland (March 1981- revised May 1982 ).
Gordon, M. J. C., “The Denotational Semantics of Sequential Machines,” Information Processing Letters, 10 (1) pp. 1–3 (February 1980).
Milner, R., “Processes: A Mathematical Model of Computing Agents,” pp. 157–173 in Logic Colloquium ’73, ed. H.E Rose and J. C. Shepherdson, North Holland Publishing Company, Amsterdam, Holland (1975).
Mavaddat, F., “Designing and Modeling VLSI Systems at Register Transfer Level,” International Journal of Computer Aided VLSI Design, 2 pp. 281–314 (1990).
Mavaddat, F., “A Functional Model of Register-Transfer Designs,” Proceedings of Twentieth Annual Pittsburgh Conference on Modeling and Simulation, (May 1989).
Landin, P. J., “The Mechanical Evaluation of Expressions,” Computer Journal, 6 (4) pp. 308–320 (Jan. 1984).
Char, B. W., Geddes, K. O., Gonnet, G. H., Monagan, M. B., and Watt, S. M., MAPLE First Leaves: A Tutorial Introduction to Maple, Springer-Verlag, New York (1992).
Geddes, K.O., Gzapor, C., and Labahn, G., Algorithms for Computer Algebra, Kluwer Academic Publisher, Boston (1992).
Paillet, J. L., “A Functional Model for Description and Specification of Digital Devices,” pp. 21–42 in From HDL Descriptions to Guaranteed Correct Circuit Designs, ed. D. Borrione, Elsevier Science Publishers B. V. ( North Holland ), Amsterdam, netherlands (1987).
Gordon, M. J. C., “Why Higher Order Logic is a Good Formalism for Specifying and Verifying Hardware,” Technical Report No. 77, Computer Laboratory, University of Cambridge, Cambridge, England (September 1985).
Boyer, R. S. and Moore, J. S., A Computational Logic, Academic Press, New York (1979).
Gordon, M. J. C., “HOL A Machine Oriented Formulation of Higher Order Logic,” Technical Report No. 68, Computer Laboratory, University of Cambridge, Cambridge, UK (1985).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer Science+Business Media New York
About this chapter
Cite this chapter
Mavaddat, F. (1993). The Role of a Symbolic Programming Language in Hardware Verification: The Case of Maple. In: Lee, T. (eds) Mathematical Computation with Maple V: Ideas and Applications. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4612-0351-3_18
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0351-3_18
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4612-6720-1
Online ISBN: 978-1-4612-0351-3
eBook Packages: Springer Book Archive