Date: Mon, 3 Nov 2003 19:30:44 -0600 (CST)
From: "Erik H. Reeber"
Subject: This week in ACL2


Hello,

   This week I will give an informal overview of my ongoing work with DE
and zChaff.

   The DE language is an HDL deeply embedded in ACL2.  I am building tools
that use decision procedures (at the moment case analysis and SAT
solving) to prove the equivalence of two DE circuits.  These tools then
automatically produce ACL2 rewrite rules involving these circuits.

    Our plan is to prove useful properties about parts of the TRIPS
processor (a grid processor currently being designed a UT) using a
mixture of ACL2 and decision procedures.

-Erik