In this chapter we first studied ways to specify a property and discussed property specification using finite-state automata and temporal logic. Along the way, we introduced the computational tree, the Kripke structure, and the fairness condition.
Then we examined graph-based algorithms for checking properties. The cases we considered were checking safety property, checking property using language containment, and checking properties specified in CTL formulas. We also examined the situations when fairness constraints were incorporated.
Once the property-checking algorithms had been introduced we studied symbolic model-checking algorithms using BDDs. First we showed how state traversal and image computation could be accomplished using BDDs. Then we applied these techniques to checking the functional equivalence of sequential circuits, language containment, and CTL formulas, with and without fairness constraints.
Finally, we discussed commonly used techniques for improving symbolic computation: early quantification and generalized cofactor. We concluded by addressing issues encountered in verifying industrial designs using model-checking tools.