Using the ACL2 theorem prover to reason about VHDL components

National audienceACL2 is a theorem prover which uses an applicative subset of Common Lisp as specification language, and employs a quantifier-free first order logic to reason about these specifications. We define how to build an ACL2 model of a design described in a synthesizable VHDL. Using this single model, we may execute the design (which corresponds to standard simulation), perform a symbolic simulation of this design, and formally verify its properties. To handle designs employing components, we use abstract functions to represent an unspecified surrounding environment. This environment stands for the (unknown system) where the component is inserted. The ACL2 construction encapsulate is used to introduce such abstract functions. This technique allows for compositional reasoning, since component properties became available to the surrounding environment without the need to repeat the proofs for each component instance