Using the ACL2 theorem prover to reason about VHDL components

Abstract

ACLZ is a theorem prover which uses an applicative subset of Common Lisp as specification language. and employs a quantil'ier-free first order logic to reason about these specifications. \Ve define how to build an ACL‘Z model of a design described in a svnthesizable VHDL. Using this single model. we may execute the design (which corresponds to standard simulation). perform a svmbolic 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 ACLQ 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.