wallacerm@afwal-aaa.UUCP.UUCP (12/29/86)
I N T E R O F F I C E M E M O R A N D U M
Date: 29-Dec-1986 04:31pm EST
From: Richard M. Wallace
WALLACERM
Dept: AADE
Tel No: 513-255-8654 (58654)
TO: Remote Addressee ( _MAILER! )
Subject: Material and Information on Proof of Correctness Contacts
Hello,
[...]
I am currently trying to find any work that has been done or is going on in
the areas of Formal Verification, Proof of Correctness, and Functional
Correcness for descriptive grammars in a LALR(1) form. My interest is focused
on analysis of only the descriptive LALR(1) grammar -- which includes
assertions and bounds -- without any annotation to the descriptive grammar.
The particular LALR(1) descriptive grammar that I am using is the Very High
Speed Integrated Circuit Hardware Description Language (VHDL) version 7.2.
This grammar is descriptive, it must be translated to another language that
can be compiled to executable form. VHDL is a structural/behavioral
simulation language for digital circuits. This is an overly brief description
of the language.
I have run across a lot of material on uses of prologs and frame-based shells
for structural circuit analysis, but have not seen any on text analysis for
grammars like the VHDL.
Any help would be appreciated.
Richard Wallace
AFWAL/AADE
WPAFB, OH 45433
513-255-8654
------