Transforming RTL Design to Counter Automaton

level (e.g., VHDL or Verilog) allow to specify a generic description.
Such a description contains one or more parameters which make the
generic nature of a design (e.g, the number of items in a buffer or the
width of inputs and output of arithmetic operation). A new approach to
formal verification of generic hardware designs will be presented. The
proposed approach is based on a translation of such designs to counter
automata. These main topics of modelling and the verification will be
discussed in more details: the translation of VHDL constructs to counter
automata, specification of an environment of modelled hardware
component, specification of safety properties over a design, and some
experimental results with ARMC and Blast.