An ACL2 model of VHDL for symbolic simulation and formalverification

摘要

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