We investigate how to take advantage of the particular features of the calculus of inductive constructions in the framework of hardware verification. First, we emphasize in a short case study the use of dependent types and of the constructive aspect of the logic for specifying and synthesizing combinatorial circuits. Then, co-inductive types are introduced to model the temporal aspects of sequential synchronous devices. Moore and Mealy automata are co-inductively axiomatized and are used to represent uniformly both the structures and the behaviors of the circuits. This leads to clear, general and elegant proof processes as is illustrated on the example of a realistic circuit: the ATM Switch Fabric. All the proofs are carried out using Coq.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Accepted in revised form 29 February 2004 by C.B. Jones
About this article
Cite this article
Coupet-Grimal, S., Jakubiec, L. Certifying circuits in Type Theory. Formal Aspects of Computing 16, 352–373 (2004). https://doi.org/10.1007/s00165-004-0048-3
- Formal methods
- Hardware verification
- Type theory
- Dependent types