An ACL2 model of VHDL for symbolic simulation and formal verification

We define the semantics of a synthesizable VHDL subset in a quantifier-free, first-order logic, and translate a VHDL description in the input format of the ACL2 theorem prover. We can use the same model for value simulation, symbolic simulation, and to prove properties expressed as theorems. The last two cases replace large or infinite number of simulation runs. Proofs are compositional: system properties follow from component properties, without flattening the design