The Role of a Symbolic Programming Language in Hardware Verification: The Case of Maple
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.
Unable to display preview. Download preview PDF.
- 4.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).Google Scholar
- 5.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 ).Google Scholar
- 7.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).Google Scholar
- 8.Mavaddat, F., “Designing and Modeling VLSI Systems at Register Transfer Level,” International Journal of Computer Aided VLSI Design, 2 pp. 281–314 (1990).Google Scholar
- 9.Mavaddat, F., “A Functional Model of Register-Transfer Designs,” Proceedings of Twentieth Annual Pittsburgh Conference on Modeling and Simulation, (May 1989).Google Scholar
- 10.Landin, P. J., “The Mechanical Evaluation of Expressions,” Computer Journal, 6 (4) pp. 308–320 (Jan. 1984).Google Scholar
- 13.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).Google Scholar
- 14.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).Google Scholar
- 16.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).Google Scholar