Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Using macros to mimic VHDL in ACL2

The purpose of our work is to verify systems written in VHDL, using symbolic simulation and theorem proving techniques. As a first step, we restrict ourselves to a synthesizable behavioral subset of the language, for which we provide a formal definition in the ACL2 logic. Our research is still at a very early stage. In the talk, we shall present the definition of the primitive type constructors: interval, enumerated type, constrained and unconstrained array; the definition is given as a macro, which recognizes a VHDL key-word, and constructs the type recognizer, and some basic theorems, for each user-defined type. The types and functions of two standard VHDL packages are also defined. We then propose a first notion of "model state" associated with a VHDL description, and define how signal and variable declarations are implemented in the state. We end the presentation with the macro that defines how the "model state" is altered by the variable and signal assignment statements.

In the long term, the systematic use of macros to define the semantics of the VHDL statements should make it possible to easily translate a synthesizable VHDL description in such a way that the resulting ACL2 script should be easily readable, and recognized as being in one to one correspondance with the original VHDL.

Slides (use "Portrait" when in ghostview)

• One slide per page (pdf, recommended)
• One slide per page (ps)

Dominique Borrione and Philippe Georgelin