Verification Techniques for System-Level Design

Chapter 5. Static Checking of Higher-Level Design Descriptions

So far, various techniques for analyzing Boolean logic functions have been introduced. Based on those methods, model-checking methods for finite state machine representations have also been presented. With model-checking methods, designs in various levels can be fully analyzed, although design size, in terms of the number of possible states in a design, is a critical issue. The so-called state explosion problem in model checking is where the number of states in a design are exponential with respect to the number of state variables. One variable in RTL could have a 32-bit width, which must be expanded into 32 Boolean variables if Boolean reasoning is applied. That is, if there are 100 ...