Advertisement

The Role of a Symbolic Programming Language in Hardware Verification: The Case of Maple

  • Farhad Mavaddat

Abstract

There is some reluctance towards the use of formal verification methods by the design community. One factor contri­buting 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 pro­gramming 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 program­ming techniques for implementing the model in the symbolic programming language Maple. Given a Maple model (a program) of a design, we execute the pro­gram 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 para­digm, and the ensuing facility for reason­ing about certain designs.

Keywords

High Order Logic Combinational Design Denotational Semantic Sequential Circuit Combinational Circuit 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Fitch, J., “Solving Algebraic Problems with REDUCE,” Journal of Symbolic Computation, 1 pp. 211–217 (1985).MATHCrossRefGoogle Scholar
  2. 2.
    Pavelle, R. and Wang, P. S., “MACSYMA from F to G,” Journal of Symbolic Computation, 1 pp. 69–100 (1985).MathSciNetMATHCrossRefGoogle Scholar
  3. 3.
    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).CrossRefGoogle Scholar
  4. 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. 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
  6. 6.
    Gordon, M. J. C., “The Denotational Semantics of Sequential Machines,” Information Processing Letters, 10 (1) pp. 1–3 (February 1980).MathSciNetMATHCrossRefGoogle Scholar
  7. 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. 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. 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. 10.
    Landin, P. J., “The Mechanical Evaluation of Expressions,” Computer Journal, 6 (4) pp. 308–320 (Jan. 1984).Google Scholar
  11. 11.
    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).MATHCrossRefGoogle Scholar
  12. 12.
    Geddes, K.O., Gzapor, C., and Labahn, G., Algorithms for Computer Algebra, Kluwer Academic Publisher, Boston (1992).MATHCrossRefGoogle Scholar
  13. 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. 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
  15. 15.
    Boyer, R. S. and Moore, J. S., A Computational Logic, Academic Press, New York (1979).MATHGoogle Scholar
  16. 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

Copyright information

© Springer Science+Business Media New York 1993

Authors and Affiliations

  • Farhad Mavaddat
    • 1
  1. 1.VLSI Group, Dept. of Computer ScienceUniversity of WaterlooWaterlooCanada

Personalised recommendations