Induction-oriented verification of replicated architectures described in VHDL

This paper is concerned with the application of theorem proving techniques to the formal proof of hardware. More precisely, we aim at providing a meth odology for applying provers like Nqthm or Ac12 to the formal verification of parameterized replicated circuits. Nqthm (the Boyer-Moore theorem prover ) and its successor Ac12 are induction-based systems; their formalisms are respectively a simplified Lisp-like language and Common Lisp. Hence, the ci rcuits we consider must be given a purely functional representation. Moreov er, our work puts the emphasis on the integration of formal proof technique s in CAD (Computer Aided Design) environments which support Hardware Descri ption Languages in which replication is expressed by iteration. Therefore, we associate with the iterative statement of the VHDL language a functional semantics that guarantees an easy translation from VHDL to Nqthm/Acl2 whil e simplifying the subsequent inductive proofs. The approach has been succes sfully applied to one-dimensional as well as two-dimensional structures.