Variable ordering on multiway decision graphs

The paper presents variable (re)ordering methods for Multiway Decision Graphs (MDG). MDGs have proved to be a powerful tool for automated hardware verification of RTL designs. To reduce the effects of the state explosion problem, we explore automatic static and dynamic variable ordering algorithms for MDG. Compared with ROBDDs, the situation is complicated by the presence of first order terms in MDGs. The static variable ordering algorithm is based on several heuristic rules, and the dynamic reordering algorithm that minimizes the size of the MDGs during the verification process combines the merits of symmetry and state group sifting. Experimental results on benchmarks show the effectiveness of our method.