Formal verification ofVHDL using VHDL-Iike ACL2 models
D. Borrione, Philippe Georgelin · 2001
When a design reaches the register transfer level, essential architectural decisions have been taken; their validation required extensive simulation of the abstract behavioral specifications. We propose to introduce mechanically supported formal reasoning in the design flow, by producing a model of VHDL behavioral specifications in the logic of the ACL2 theorem prover. Written in Lisp, this model is executable as well as subject to symbolic manipulations. We define the semantics of VHDL data types and behavioral style statements in the logic. We use macros to generate names, function definitions and theorems automatically, by instantiation of model skeletons, while retaining an algorithmic syntactic flavor. This feature is particularly useful to translate VHDL statements into resembling ACL2 macros, so that the logic formalization remains readable.