## Department of Computer Sciences## 1999 ACL2 WorkshopMarch 29 - March 31, 1999 |

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.

Dominique Borrione and Philippe Georgelin

Last updated March 1999 pete@cs.utexas.edu |
Computer Sciences
Department University of Texas at Austin |