Zobair, Md Hasan (2001) Modeling and formal verification of a telecom system block using MDGs. Masters thesis, Concordia University.
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.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering|
|Item Type:||Thesis (Masters)|
|Authors:||Zobair, Md Hasan|
|Pagination:||ix, 94 leaves : ill. ; 29 cm.|
|Degree Name:||Theses (M.A.Sc.)|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Tahar, Sofiene|
|Deposited By:||Concordia University Libraries|
|Deposited On:||27 Aug 2009 17:18|
|Last Modified:||08 Dec 2010 15:20|
Repository Staff Only: item control page