Li, Donglin (2006) Towards first-order symbolic trajectory evaluation using MDGs. Masters thesis, Concordia University.
MR14270.pdf - Accepted Version
SoC design becomes more complex with the increasing amount of different kinds of IPs on the chip. How to ensure correctness of functionality in an SoC chip is one of the biggest challenges in SoC designs. Traditional BDD-based symbolic model checking techniques are an attractive subset of formal verification methods because of their high automation and little requirement for human effort to guide the proof process, whereas they usually suffer from the state explosion problem. Symbolic Trajectory Evaluation (STE) technique and MDG-based model checking technique improve the traditional BDD-based symbolic model checking approaches in two different ways. In this thesis, we investigate the possibility of combining STE and MDGs, for each of which we study the underlying theory and methodology, discuss the verification tool, and provide a detailed case study. The main purpose of these two case studies is to obtain an in-depth understanding of the underlying theories and methodologies of these two model checking techniques, which may facilitate the achievement of their combination.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering|
|Item Type:||Thesis (Masters)|
|Pagination:||xiii, 110 leaves : ill. ; 29 cm.|
|Degree Name:||M.A. Sc.|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Ait Mohamed, Otmane|
|Deposited By:||Concordia University Libraries|
|Deposited On:||18 Aug 2011 18:45|
|Last Modified:||05 Nov 2016 01:28|
Repository Staff Only: item control page