Description and Verification of RTL Designs Using Multiway Decision Graphs

Traditional OBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. Multiway Decision Graphs (MDGs) [5] combine the advantages of OBDD techniques with those of abstract types. RTL designs can be compactly described by MDGs using abstract data values and uninterpreted function symbols. We have developed MDGbased techniques for combinational verification, reachability analysis, verification of behavioral equivalence, and verification of a microprocessor against its instruction set architecture. We report on the results of several verification experiments using our MDG package. I. Introduction Bryant's Reduced and Ordered Binary Decision Diagrams (OBDDs) [1] have proved to be a powerful tool for automated hardware verification [2, 6, 12]. OBDDs, however, have a drawback: they require a binary representation of the circuit even if the design is given at the Register Transfer Level. Every individual bit of every data ..