Term ordering problem on MDG

10 years 11 months ago
Term ordering problem on MDG
As an efficient representation of Extended Finite State Machines, Multiway Decision Graphs (MDG) are suitable for automatic hardware verification of Register Transfer Level (RTL) designs. However, in some cases, MDG-based verification suffers from the state explosion problem. Some of cases are caused by the standard order used by MDG to order cross-terms that have the same toplevel function symbol. These terms usually label decision nodes and must be ordered. We call this kind of state explosion the standard term ordering problem. A solution based on function renaming and cross-term rewriting is proposed in this paper. Experimental results show that this solution can solve the problem completely and thus increase the range of circuits that can be verified by MDG. Categories and Subject Descriptors B.5.2 [Register-Transfer-Level Implementation]: Design Aids – verification. General Terms Verification. Keywords Multiway Decision Graphs, Standard term ordering, Variable Ordering, First-...
Yi Feng, Eduard Cerny
Added 14 Jul 2010
Updated 14 Jul 2010
Type Conference
Year 2002
Authors Yi Feng, Eduard Cerny
Comments (0)