Symbolic Simulation and Verification of VHDL with ACL2

Abstract

ACL2 is a theorem prover to reason about specifications written in a quantifier-free, first-order logic. The input langage is Common Lisp. We defined the semantics of a synthesizable VHDL subset in the logic, and describe an automatic method (and the corresponding tool) to build an ACL2 model of an abstract behavioral VHDL description. This model is executable and efficient, so the designer can simulate it on the same tests as with a conventional simulator, and get confidence in it. Using the theorem prover, we may prove properties that otherwise would require a large or infinite number of simulation runs. Finally, we may also perform symbolic simulation, i.e. we can execute the design on symbolic input data, which is another way to cope with excessively large or infinite sets. Symbolic simulation is an automatic process, so it is easier than theorem proving. We stress the fact that all three tasks are performed on the same representation of a VHDL design.