Verifying sequential behavior with model checking

The design of state-of-the-art digital circuits often involves interacting state machines with very complex control flow. As consequence functional verification of sequential designs is becoming a major bottleneck in the design process. Model checking techniques, the topic of this tutorial, promise to speed up verification time by checking high level temporal properties. Model checking is best used in early design phases where it may help to catch fundamental design flaws and errors as early as possible