A practical model checking approach using FormalCheck

Verification of industrial designs is becoming more challenging as technology advances and demand for higher performance increases. One of the most suitable debugging aids is automatic formal verification, which tests behaviors under all possible executions of a system. However, automatic formal verification is limited by the state explosion problem. This thesis presents a practical verification approach using FormalCheck, which helps reducing the state space explosion problem when verifying the high level descriptions of practical systems. This approach relies on the design's built-in hierarchy as the mechanism to conquer its complexity during verification. Then an assume guarantee paradigm is used to verify functional units built on top of instantiated and previously verified modules. We applied this approach to an industrial design (Transmit Master/Receive Slave (TMRS) Telecom System Block) as a case study. The TMRS was thoroughly verified and in consistencies in the design with respect to its specification were uncovered through model checking. The main contributions of this thesis are, (1) the application of a variety of model checking techniques to a real size design and (2) proposing a number of improvements to the design flow which can accelerate the whole verification process