Date: Tue, 29 Jun 2004 02:06:18 -0500 (CDT)
From: "Erik H. Reeber" <reeber@cs.utexas.edu>
To: acl2-mtg@lists.cc.utexas.edu
Subject: This week in ACL2
Content-Type: TEXT/PLAIN; charset=US-ASCII
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=-4.9 required=5.0
X-UTCS-Spam-Status: No, hits=-458 required=180


Hello everyone,

   At this week's ACL2 meeting I will be restarting my description of
the DE hardware description language (which I began a month ago).  Here's
the abstract for my talk, which I sent out last time:

   DE evolved from DUAL-EVAL, which was used by Warren and Bishop to
verify the FM9001 microprocessor.  Like DUAL-EVAL, DE is embedded in ACL2.
Also like DUAL-EVAL, a cycle is evaluated by running two passes through a
netlist (once to update the wires and once to update state).

   I will focus on the differences between DUAL-EVAL and DE.  These
primarily consist of increased separation of primitives from the language
definition and the existence of a parameterized type system (where
every wire is a bit-vector).  If time permits, I will also discuss our
planned verification strategy and how we will integrate DE with verilog.

   DE is a work in progress.  I hope to get feedback from y'all on
user-friendliness, anticipated difficulty of verification, and
expressiveness issues.

Thanks,
Erik