Semantics of a verification-oriented subset of VHDL

ISBN: 3540603859This paper gives operational semantics for a subset of VHDL in terms of abstract machines. Restrictions to the VHDL source code are the finiteness of data types, and the absence of quantitative timing informations. The abstract machine of a design unit is built by composition of the abstract machines for its embedded processes and blocks. The kernel process in our model is distributed among the composed machines. One transition of the final abstract machine models a VHDL delta cycle. This model can be used for symbolic model checking and equivalence verification