From: Matt Kaufmann
Subject: This week in ACL2

Hello --

I asked Warren Hunt if he'd be willing to talk this week instead of
next, and he graciously agreed (so perhaps we will hear from John next
week).

NOTE!  The talk will start promptly at 4pm today because Warren needs
to leave shortly before 5pm.  The talk will be followed by a
roundtable.

			    The E Language
	       Robert S. Boyer and Warren A. Hunt, Jr.


We are developing the {\bf E} hardware description language; this HDL
is an evolution of the {\bf DE2} language, but with several
restrictions removed.  {\bf E} is a hierarchical, occurrence-oriented,
HDL that is deeply embedded inside of ACL2.  We use {\bf E} to
represent circuits, and we verify such representations using ACL2.
{\bf E} may be used to directly specify gate-array and FPGAs designs;
we verify transistor-level circuits by preprocessing such circuits
into {\bf E} modules.  We can verify Lava-style circuit generator
functions, either by symbolic simulation or by induction.

The semantics of {\bf E} are specified by an interpreter written in
the ACL2 logic.  Our semantics includes a crude delay estimator, which
may be used to help manage wire delays.  We have generalized our
hardware specification approach to permit signal variables to
represent equations; these specification functions contain a flag that
indicates the equation type (Boolean, four-valued, delay, etc.) of
their input arguments and output results.