Multiway Decision Graphs (MDGs) represent and manipulate a subset of first-order logic formulas suitable for high-level hardware verification With MDGs, a data value is represented by a single variable of abstract type and a data operation is represented by an uninterpreted function symbol.

The MDG operators and verification procedures are packaged as MDG tools and implemented in Prolog. They currently run under Quintus Prolog Version 3.2. MDG provides the following features: 1) Verification of combinational circuits, 2) Safety property checking, 3) State enumeration 4) Equivalence checking of two state machines 5) Model checking