Hardware Verification Using Co-induction in COQ
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.
KeywordsOutput Port Input Port Asynchronous Transfer Mode Parallel Composition Output Stream
Unable to display preview. Download preview PDF.
- 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
- D. Cachera. Verification of Arithmetic Circuits using a Functional Language and PVS. Technical Report 97-48, ENS-Lyon, LIP, Dec. 1997.Google Scholar
- T. Coquand. Une Théorie des Constructions. PhD thesis, Université Paris 7, Janvier 1989.Google Scholar
- T. Coquand and G. Huet. Constructions: A Higher Order Proof System for Mechanizing Mathematics. EUROCAL 85, Linz Springer-Verlag LNCS 203, 1985.Google Scholar
- 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
- P. Curzon. The Formal Verification of the Fairisle ATM Switching Element. Technical Report 329, University of Cambridge, Mar. 1994.Google Scholar
- P. Curzon. The Formal Verification of the Fairisle ATM Switching Element: an Overview. Technical Report 328, University of Cambridge, Mar. 1994.Google Scholar
- 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
- 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
- I. Leslie and D. McAuley. Fairisle: A General Topology ATM LAN. http://www.cl.cam.ac.uk/Research/SRG/fairpap.html, Dec. 1990.
- 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
- 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
- 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
- C. Paulin-Mohring. Circuits as Streams in Coq. Verification of a Sequential Multiplier. Basic Research Action “Types”, July 1995.Google Scholar
- 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
- 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
- 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