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 such RTL variables, 3,200 Boolean variables must be manipulated, which can easily become infeasible. The actual design descriptions in a C/C++-language-based design can easily comprise more than 100,000 lines of code, which may have over 10,000 variables. Therefore, in general, it is largely impossible to apply model-checking-type state-based analysis methods to such design descriptions. What we need in such cases are methods that approximately analyze the design and try to detect as many design bugs as possible. In this chapter, we discuss one such method: static analysis of high-level design descriptions in C/C++-based languages.

There have been many other works on software program analysis that have sought this same goal. In this chapter, we begin by targeting C/C++-based design languages for hardware/software co-designs, such as SpecC [1] and SystemC [2]. We review static-checking methods used in software analysis fields, starting with program slicing and the system dependence graph (SDG) that is used as the basic representation of the program descriptions to be checked. Here SDG and its extensions for hardware/software (HW/SW) co-designs are introduced. Then they are expanded so that concurrent processes and their communications can be processed as well, which is essential for hardware/software co-designs. Performance on those static analysis techniques and their application to hardware/software co-designs are also considered.