Circuit designers can efficiently verify designs at the bit and word levels in one graph-based data structure. The authors present the representation technique, manipulation algorithms for K*BMDs, and experimental results comparing them with other data structures.