Modeling and formal verification of a telecom system block using MDGs

This thesis demonstrates the effectiveness of Multiway Decision Graphs (MDG) to carry out the formal verification of an industrial Telecom hardware which is commercialized by PMC-Sierra Inc. To handle the complexity of the design, we adopted a hierarchical proof methodology as well as a number of design, we followed a hierarchical approach for the equivalence checking of the TSB. We first verified that the RTL implementation of each module complies with the specification of its behavioral model. We also succeeded to verify the full RTL implementation of the TSB against its top level specification. Besides equivalence checking, we furthermore applied model checking to ascertain that both the specification and the implementation of the TSB satisfy some specific characteristics of the system. To measure the performance of the MDG verification, we also conducted the verification of the same TSB with Cadence FormalCheck. The experimental results show that in some cases, the MDG than that of the boolean modeling in FormalCheck