Date: Mon, 17 May 2004 16:25:09 -0500 (CDT)
From: "Erik H. Reeber"
Subject: This week in ACL2


Hello everyone,

   I'm the main speaker for this week's ACL2 meeting.  At the meeting I
will describe the DE hardware description language.

   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