Contribution: Multiplier
Proof of a multiplier circuit
Authors
- Christine Paulin
Description
Keywords
hardware verification, circuit
README
(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet Coq *)
(* *)
(* INRIA ENS-CNRS *)
(* Rocquencourt Lyon *)
(* *)
(* Coq V5.10 *)
(* July 1st 1995 *)
(* *)
(****************************************************************************)
Representation of circuits as streams.
Proof of a multiplier circuit.
Christine Paulin-Mohring June 95.
GFP.v : Impredicative representation of greatest
fixpoints of monotonic operators.
Streams.v : Representation of streams, invariant principle.
Circ.v : Generic represention of sequential circuits from the
updating and output functions.
Multiplier.v : proof of a multiplier.
This work is described in the following reference (file mult.ps.gz)
Research Report : RR 95-16
Title : Circuits as streams in Coq: Verification of a sequential multiplier.
Author : Christine Paulin-Mohring <Christine.Paulin@ens-lyon.fr>
LIP, ENS Lyon, 46 allee d'Italie, F-69364 Lyon Cedex 07, France
Date : September 95.
Abstract: This paper presents the proof of correctness of a
multiplier circuit formalized in the Calculus of Inductive
Constructions. It uses a representation of the circuit as a function
from the stream of inputs to the stream of outputs. We analyze the
computational aspect of the impredicative encoding of coinductive
types and show how it can be used to represent synchronous circuits.
We identify general proof principles that can be used to justify the
correctness of such a circuit. The example and the principles have
been formalized in the Coq proof assistant.