Approximate model checking

In the past few years, formal verification has gained attention from the digital circuit design community. However, formal verification methods are still not considered as the mainstream verification methodology in practice. We believe this is because the algorithms of the formal methods, in general, require heavy computational power which make them infeasible to be applied in the daily verification tasks.; This thesis focuses on making formal verification feasible for the real life designs. We use {dollar}rm forall CTL{dollar} and CTL model checking to formally verify the system. The introduction of the symbolic approach (BDD) has significantly improved model checking; however the method alone still cannot handle production level circuits. We rely on conservative verification algorithm to reduce the computational complexity of the given problem. Our conservative verification algorithm contains two sub-algorithms: conservative positive and conservative negative verification algorithm. Conservative positive (negative) algorithm is responsible for proving true positive (negative) of a given formula.; We introduce two distinct approximation strategies for conservative verification: tearing abstraction and BDD abstraction. The tearing based abstraction technique abstracts the system from the circuit level. The BDD abstraction technique directly applies abstraction to the structure of BDDs. The two methods are combined into a single verification framework to improve the quality of approximations.; The verification process starts from a coarse approximation and refines it until a reliable result is produced. The refinement strategy is based on the theory of the lattice of approximations. The theory of the lattice of approximations provides a systematic way to generate successive refinements. The lattice contains two sub-lattices, one for the over-approximations and the other for the under-approximations. The exact system is located in the middle and the lattice of over-approximations above it and the lattice of underapproximations beneath the exact system.; The study indicates that the formal method is applicable to the industrial strength circuits. We used a state-of-the-art 2x2 scalable ATM switching fabric circuit to test the new algorithms.