Advertisement

Hardware Verification Using Co-induction in COQ

  • Solange Coupet-Grimal
  • Line Jakubiec
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1690)

Abstract

This paper presents a toolbox implemented in Coq and dedicated to the specification and verification of synchronous sequential devices. The use of Coq co-inductive types underpins our methodology and leads to elegant and uniform descriptions of the circuits and their behaviours as well as clear and short proofs. An application to a non trivial circuit is given as an illustration.

Keywords

Output Port Input Port Asynchronous Transfer Mode Parallel Composition Output Stream 
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]
    B. Barras and al. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report 0203, INRIA-Rocquencourt, CNRS-ENS Lyon, France, Dec. 1997.Google Scholar
  2. [2]
    D. Cachera. Verification of Arithmetic Circuits using a Functional Language and PVS. Technical Report 97-48, ENS-Lyon, LIP, Dec. 1997.Google Scholar
  3. [3]
    T. Coquand. Une Théorie des Constructions. PhD thesis, Université Paris 7, Janvier 1989.Google Scholar
  4. [4]
    T. Coquand and G. Huet. Constructions: A Higher Order Proof System for Mechanizing Mathematics. EUROCAL 85, Linz Springer-Verlag LNCS 203, 1985.Google Scholar
  5. [5]
    S. Coupet-Grimal and L. Jakubiec. Coq and Hardware Verification: a Case Study. In J. G. J. vonWright and J. Harrison, editors, TPHOLs’96, LCNS 1125, pages 125–139, Turku (Finlande), 27–30th August 1996. Springer-Verlag.Google Scholar
  6. [6]
    P. Curzon. The Formal Verification of the Fairisle ATM Switching Element. Technical Report 329, University of Cambridge, Mar. 1994.Google Scholar
  7. [7]
    P. Curzon. The Formal Verification of the Fairisle ATM Switching Element: an Overview. Technical Report 328, University of Cambridge, Mar. 1994.Google Scholar
  8. [8]
    E. Garcez and W. Rosenstiel. The Verification of an ATM Switching Fabric using the HSIS Tool. IX Brazilian Symposium on the Design of Integrated Circuits, 1996.Google Scholar
  9. [9]
    E. Giménez. Un calcul de constructions in finies et son application à la vèrication de systèmes communicants. PhD thesis, Ecole Normale Superieure de Lyon, 1996.Google Scholar
  10. [10]
    I. Leslie and D. McAuley. Fairisle: A General Topology ATM LAN. http://www.cl.cam.ac.uk/Research/SRG/fairpap.html, Dec. 1990.
  11. [11]
    I. Leslie and D. McAuley. Fairisle: An ATM Network for the Local Area. ACM Communication Review, 4(19):327–336, September 1991.CrossRefGoogle Scholar
  12. [12]
    J. Lu and S. Tahar. Practical Approaches to the Automatic Verification of an ATM Switch using VIS. In IEEE 8th Great Lakes Symposium on VLSI (GLS-VLSI’98), pages 368–373, Lafayette, Louisiana, USA, Feb. 1998. IEEE Computer Society Press.Google Scholar
  13. [13]
    P. S. Miner and S. D. Johnson. Verification of an Optimized Fault-Tolerant Clock Synchronization Circuit. In Designing Correct Circuits. Bästad, 1996.Google Scholar
  14. [14]
    C. Paulin-Mohring. Inductive Definition in the System Coq: Rules and Properties. Typed Lambda Calculi and Applications (Also Research Report 92-49, LIPENS Lyon), Dec. 1993.Google Scholar
  15. [15]
    C. Paulin-Mohring. Circuits as Streams in Coq. Verification of a Sequential Multiplier. Basic Research Action “Types”, July 1995.Google Scholar
  16. [16]
    S. Tahar and P. Curzon. A Comparison of MDG and HOL for Hardware Verification. In J. G. J. von Wright and J. Harrison, editors, TPHOLs’96, LCNS 1125, pages 415–430, Turku (Finlande), 27–30th August 1996. Springer-Verlag.Google Scholar
  17. [17]
    S. Tahar, P. Curzon, and Lu. J. Three Approaches to Hardware Verification: HOL, MDG and VIS Compared. In G. Gopalakrishnan and P. Windley, editors, Formal Methods in Computer-Aided Design, LNCS 1522, pages 433–450, FMCAD’98, Palo Alto, California, USA, Nov. 1998. Springer-Verlag.CrossRefGoogle Scholar
  18. [18]
    S. Tahar, Z. Zhou, X. Song, E. Cerny, and M. Langevin. Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs. In Proc. of the Great Lakes Symp. on VLSI, IEEE Computer Society Press, pages 106–111, Mar. 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Solange Coupet-Grimal
    • 1
  • Line Jakubiec
    • 1
  1. 1.Laboratoire d’Informatique de Marseille - URA CNRS 1787MarseilleFrance

Personalised recommendations