Date: Tue, 9 Sep 2008 01:56:07 -0500
From: "Jared C. Davis"
Subject: This week in ACL2

Hi,

At this week's ACL2 seminar I'll give a talk about a Verilog parser I
wrote (in ACL2) at Centaur this summer.

The talk won't really be about Verilog, but instead will mainly be
about the architecture and supporting utilities I've developed, much
of which should be reusable in other parsers that you might be
thinking about writing, and which make writing parsers in ACL2 a
pretty reasonable thing to do.  In particular, I've implemented an
macro-based, embedded stream-processing language called SEQ which can
be used inside of ACL2 functions, and it provides exception-handling
and a way to implicitly update streams.  Backtracking and arbitrary
lookahead are supported in a trivial way, and error reporting is often
automatic and reasonably adequate.  Everything is well-suited for
inline unit testing without needing separate test files, and so I have
a lot of unit tests (which have saved me countless times).  I can also
do some minor theorem proving (e.g., to verify guards and show that
the parser generates a well-formed parse tree), and I have some macros
that really help to automate the "boilerplate" proofs.

The program has a bad case of memory-lust, but it can parse the chip
(half a million lines of Verilog) in about 2 minutes.  And probably
that could be improved without too much work.

Thanks,
Jared