Hardware verification using co-induction in COQ

Abstract

This paper presents a toolbox implemented in Coq and dedicated to the specification and verification of synchronous sequential devices. The use of Coq co-inductive types underpins our methodology and leads to elegant and uniform descriptions of the circuits and their behaviours as well as clear and short proofs. An application to a non trivial circuit is given as an illustration.