In this report, we investigate the ability of MDGs (Multiway Decision Graphs) to carry out a verification process of a large industrial Telecom hardware which is commercialized by PMC-Sierra Inc. Until recently, the Cambridge Fairisle ATM switch fabric with 4200 equiva-lent gates was the largest industrial like design verified with the MDG tools. The design we con-sider in this study is a Telecom System Block (TSB), called RASE, containing 11400 equivalent gates. For the formal verification, we adopted a hierarchical proof methodology to handle the complexity of the design. We then carried out MDG based equivalence checking as well as model checking. To measure the performance of the MDG verification, we also conducted the verifica-tion of the same TSB with Cadence FormalCheck. The experimental results showed that in some cases, the MDG model checker was more efficient due to the ability with MDGs to use abstract state variables and uninterpreted function symbols rather than simply a Boolean modeling as in FormalCheck.

Download postscript file (PS File)

Download PDF file (PDF File)

Send comments and suggestions to: tahar@ece.concordia.ca