Verification Techniques for System-Level Design

Chapter 7. Model Checking on Higher-Level Design Descriptions

Introduction

The basic model-checking algorithms were introduced in Chapter 4. Basically they traverse finite state machines (FSMs) generated from design descriptions exhaustively in explicit or implicit ways. In general, the number of states in an FSM is exponential with respect to the number of state variables (flip-flops in the case of logic circuits). This is the so-called state explosion problem in model checking, which makes it very difficult to apply model checking to large design descriptions. In the case of high-level design descriptions, the number of state variables can be very large in the sense that there are many word-level variables in the descriptions. There have been ...