From: John Conover <john@email.johncon.com>
Subject: Re: BNF/YACC'able state machine verification
Date: Wed, 5 Jun 1996 22:23:11 -0700
Hi Rick. If you recall, sometime last year, I suggested that what we
really, really, needed was some kind of a BNF/YACC verification gizmo
for digital circuits. It was in reference to the complexity of state
machine design in a contemporary microprocessor. The idea being that a
high level state machine definition language, similar to BNF but
instead of a stack implementation language, it would be a state
machine language, and a suitable grammar checker, something like YACC,
could be used to verify the "correctness" of design of multiply
coupled state machines, or something to that effect.
In the new IEEE spectrum is an article from someone at Compass that
uses TAG files to come pretty close to that, with an RTL language, and
state machine register checking algorithm that detects dead, (or
non-attainable), and terminal states. It is a two page article, and is
thus pretty sparse with information, but might have some practical
uses. I had looked at TAG several years ago, but my feeling, at least
at the time, was that the concept was not very extensible. FYI.
John
--
John Conover, john@email.johncon.com, http://www.johncon.com/