Integrating MDG variable ordering in a VHDL-MDG design verification system

Formal verification methods involve the use of analytical techniques to prove that the implementation of a system conforms to the specification. As an efficient representation of Extended Finite State Machines, Multiway Decision Graphs (MDG) are suitable for automatic hardware formal verification of Register Transfer Level (RTL) designs.; To reduce the effects of the state explosion problem in the MDG-based system, we explore automatic static and dynamic variable ordering algorithms. Compared with ROBDDs, the situation is complicated by the presence of first order terms in MDGs.; The static variable ordering algorithm generates a variable order before an MDG is built and the order is chosen using information about the circuit topology. The dynamic reordering algorithm minimizes the size of the MDG during the verification process and allows a verification task to finish when the task may not complete with a fixed order due to insufficient memory or execution time. We also identify a standard term ordering problem caused by the standard term order used in MDG to order some specific terms. A solution based on function renaming and term rewriting is presented.; The MDG system has become more efficient with the development of automatic variable ordering. However, the system only accepts MDG-HDL and most of designs in industry are described in VHDL or Verilog. We present a translator which can accept a VHDL model given at the synthesizable RTL level and produce the required representation by the MDG system.; We integrated the translation and the (re)ordering algorithms into the MDG design verification system. Efficient variable ordering is essential for good functioning of the verification system and automatic translation from VHDL to MDG-HDL makes possible the verification of industrial designs. Experimental results proved that this updated system can handle a larger class of designs than before, thus alleviating the effects of the state exploration problem and increasing the range of the circuits that can be verified.