Formal verification of digital systems

A formal verifier is an automated decision procedure that can prove or disprove a set of statements in some logical system of reasoning. Problems informal verification have been posed and studied in a variety of disciplines for many years. However the last ten years have produced significant advances in both the theory and practical art of building formal verifiers. Various formal proof techniques available today include language containment, model checking, equivalence checking, symbolic simulation and theorem proving. In this tutorial, we will be restricting ourselves to the formal finite state machine based techniques: language containment, model checking and equivalence checking. A brief introduction to the technologies that underly these techniques will be presented as well. The tutorial will conclude with some examples of how formal methods can be employed in the verification of hardware systems