Coquet: a Coq library for verifying hardware

Abstract : We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently typed) data-type that models the architecture of circuits, and a meaning function. We propose tactics that ease the reasoning about the behavior of the circuits, and we demonstrate that our approach is practicable by proving the correctness of various circuits: a text-book divide and conquer adder of parametric size, some higher-order combinators of circuits, and some sequential circuits: a buffer, and a register.
Type de document :
Pré-publication, Document de travail
2011
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00611757
Contributeur : Thomas Braibant <>
Soumis le : lundi 22 août 2011 - 08:54:08
Dernière modification le : jeudi 11 octobre 2018 - 08:48:01
Document(s) archivé(s) le : lundi 12 novembre 2012 - 15:25:37

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00611757, version 1
  • ARXIV : 1108.4253

Collections

Citation

Thomas Braibant. Coquet: a Coq library for verifying hardware. 2011. 〈inria-00611757〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

283