X-IronPort-MID: 442365281
X-SBRS: 3.5
X-BrightmailFiltered: true
X-Ironport-AV: i="3.88,132,1102312800"; 
   d="scan'208"; a="442365281:sNHT14262780"
Date: Mon, 17 Jan 2005 16:03:16 -0600 (CST)
From: "Erik H. Reeber" <reeber@cs.utexas.edu>
To: acl2-mtg@lists.cc.utexas.edu
Subject: ACL2 Meeting
In-Reply-To: <41B628D2.2060806@cs.utexas.edu>
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Reply-To: acl2-mtg@lists.cc.utexas.edu
Sender: owner-acl2-mtg@lists.cc.utexas.edu
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-332 required=180


Hello everyone,

    I hope y'all had a good break.  There will be an ACL2 meeting this 
week.  In the meeting, I'll by presenting my work on integrating SAT 
solving with ACL2.  Here's an abstract of my talk:

    Satisfiability (SAT) solvers are programs for computing whether an 
expression of boolean variables in conjunctive normal form (CNF) is 
satisfiable.  While SAT solving is in theory NP-hard, in practice many 
of today's SAT solvers can solve problems involving hundreds of thousands 
of variables.  Thus they are often used today in fully-automated 
hardware verification tools as an alternative to binary decision diagrams 
(BDDs).
     I have created a tool within ACL2 that converts a well-defined 
fragment of ACL2 into boolean variables in CNF.  I use this tool along 
with external SAT solvers to prove or find counter examples for 
expressions in this fragment.  While our fragment of ACL2 is certainly 
limited, it is large enough to express hardware invariants of interest to 
me in my verification of components of a semi-industrial processor (the 
processor I'm working with is a prototype of future processors which
is being designed and fabricated by UT Austin and IBM).
     My current integration method is achieved by modifying the source 
code to ACL2.  I do not really expect anyone right-away to trust my 
conversion algorithm and I never expect us to fully trust external tools. 
Therefore I would like to discuss how we can integrate external decision 
procedures with ACL2 in such a way as to maintain a core trusted ACL2, but 
also allow people to use less-trusted techniques if they so wish.

-Erik