Using Macros to Mimic VHDL

Abstract

The purpose of this project is to define in ACL2 the semantics of a small synthesizable behavioral subset of VHDL. The intention is to preserve, as much as possible, the syntactic flavor of VHDL, and to facilitate the verification of a circuit design by symbolic simulation and theorem proving techniques. The definition is written with macros, which recognize VHDL keywords and construct semantic functions and some basic theorems, for each main statement of the language. This project introduces type definitions, signal and variable declarations, and simple processes. Declarations define the initial state of a system. Statements and processes are functions that map states to (next) states. The systematic use of macros helps by introducing infix notation, employing keywords that strongly resemble corresponding VHDL syntax.