Paper Info
Title
ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool
Abstract
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 modelcheckers 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.
Year
DOI
Venue
2006
10.1109/FMCAD.2006.3
FMCAD
Keywords
Field
DocType
automated verification tool,hardware verification environment,decision procedure,acl2 theorem prover,general-purpose external interface,acl2 function,large verification problem,ibm internal formal verification,automated verification engine,general-purpose theorem prover,acl2 function acl2six,theorem prover,formal logic,theorem proving,formal verification
Functional verification,Programming language,Intelligent verification,Computer science,Runtime verification,Theoretical computer science,Verification,SixthSense,ACL2,High-level verification,Software verification
Conference
ISBN
Citations 
PageRank 
0-7695-2707-8
8
0.55
References 
Authors
13
2
Name
Order
Citations
PageRank
Jun Sawada132521.16
Erik Reeber2865.58