We present a hardware verification environment that integrates the ACL2 theorem prover and SixthSense, an IBM internal formal verification tool. In this environment, SixthSense is invoked through an ACL2 function acl2six that makes use of a general-purpose external interface added to the ACL2 theorem prover. This interface allows decision procedures and model-checkers to be connected to ACL2 by simply writing ACL2 functions. Our environment also exploits a unique approach to connect the logic of a general-purpose theorem prover with machine designs in VHDL without a language embedding. With an example of a pipelined multiplier, we show how our environment can be used to divide a large verification problem into a number of simpler problems, which can be verified using automated verification engines.
展开▼
