Coquet: a Coq library for verifying hardware

DOI10.1007/978-3-642-25379-9_24zbMATH Open1350.68226arXiv1108.4253OpenAlexW1483190703MaRDI QIDQ3100217FDOQ3100217

Authors: Thomas Braibant 

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1108.4253

Recommendations

• Certifying circuits in type theory
• Circuits as streams in Coq: verification of a sequential multiplier
• \(\Pi\)-Ware: hardware description and verification in Agda
• Modular deductive verification of multiprocessor hardware designs
• scientific article; zbMATH DE number 1696436

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Geometry of synthesis: a structured approach to VLSI design
• An introduction to small scale reflection in Coq
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Higher Order Logic and Hardware Verification
• Towards an algebraic theory of Boolean circuits.
• A formally verified compiler back-end
• Title not available (Why is that?)
• Mathematics of Program Construction
• Certifying circuits in type theory
• Proof producing synthesis of arithmetic and cryptographic hardware

Cited In (10)

• Coq and hardware verification: a case study
• Functional verification of high performance adders in \textsc{Coq}
• A Coq library for internal verification of running-times
• A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
• \(\Pi\)-Ware: hardware description and verification in Agda
• Modular verification of programs with effects and effect handlers in Coq
• Circuits as streams in Coq: verification of a sequential multiplier
• Certifying circuits in type theory
• Mathematical Knowledge Management
• Modular verification of programs with effects and effects handlers

Uses Software

• Coq
• Coq/SSReflect
• Coquet
• Lava

This page was built for publication: Coquet: a Coq library for verifying hardware

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100217)