| With the increasing complexity of large scale Application-Specific Integrated Circuit (ASIC) designs, simulation cannot cover all the corner cases in a reasonable time frame. Formal verification is emerging as a supplementary approach to main-stream simulation. Among various formal verification approaches, model checking is a fully automatic approach to verify a finite state machine against its temporal specifications. It has been successfully used in several industrial verification projects. However, its application is limited by the size of the system to be verified due to state space explosion. There are two main methods to tackle this problem: compositional verification and model reduction. Compositional verification is to verify each partition in the system separately and then derive the system specification from the partial proofs. Model reduction is to reduce the size of the system such that it can be handled by a model checking tool. In this thesis, we integrate these two approaches to perform model checking.; In a compositional verification, properties are only true under certain environments. One of the problems in the compositional reasoning approach is to generate the environment assumption, i.e., stimulus for the module (partition) under verification. In our approach, we provide the environment assumptions as temporal logic formulas and then synthesize an executable hardware description language module from it. Compared with existing related work, the proposed environment has a smaller state space, which is a key factor in compositional verification. The synthesized modules are composed with the design block under verification and then fed into a model checking tool.; However, in case the size of the composed module is still beyond the capability of model checking, we use a novel syntactic model reduction algorithm, which analyzes the source code and removes the redundant variables and values. The reduction we propose in this thesis is based on the static analysis of control flow diagram of the program. The values of state variables in the program are partitioned into active values, and deactive values according to their dependency to the properties. and thus the value domains of the variables are much smaller than the original ones. Compared with existing related work, the proposed approach is automatic and has better performance in the reduction of datapath intensive designs.; In order to demonstrate the application of the proposed techniques, we verified an industrial size ATM (Asynchronous Transfer Mode) switch fabric from Nortel Networks which complexity is beyond the capability of plain model checking tools. |
