Towards first-order symbolic trajectory evaluation using MDGs

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