• Using the ACL2 theorem prover to reason about VHDL components 

      Rodrigues, Vanderlei Moraes; Borrione, Dominique; Georgelin, Philippe (2000) [Artigo de periódico]
      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 ...