Electronic Design Automation

9.5.2. Model checking (property checking)

Given a property and a design, a model checking tool allows a user to check whether the property holds true on the design. To develop such a tool, one needs to ask two basic questions: how to specify or describe a property and how to efficiently prove that a property holds true or is violated. The first question concerns the language used to express properties. Such a language determines what properties can be described and what properties cannot be described and, hence, limits the applicability of a model checking tool. The second question concerns the computation engine used to prove properties. Like equivalence checking described previously, OBDD and SAT are two prevalent methods that are used to ...