Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Certifying circuits in Type Theory

Abstract

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.

Author information

Correspondence to Solange Coupet-Grimal.

Additional information

Accepted in revised form 29 February 2004 by C.B. Jones

Rights and permissions

Reprints and Permissions

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

Download citation

Keywords

  • Formal methods
  • Hardware verification
  • Type theory
  • Dependent types
  • Co-induction
  • Extraction