Speeding up hardware verification by automated data path scaling
The main obstacle for formal hardware verification of digital circuits is formed by ever increasing design sizes and circuit complexity. Therefore, reducing runtimes and the amount of memory needed for verification computations is a major requirement in order to successfully apply formal verification techniques to industrial circuit designs. This thesis presents a new abstraction technique for Bounded Model Checking of digital circuits. The proposed technique reduces the sizes of design models before verification by implementing a fully automated scaling of data path widths. Digital circuit designs are usually given as Register-Transfer-Level (RTL) specifications, but most industrial hardware verification tools are based on bit-level methods such as SAT or BDD techniques. RTL specifications contain explicit structural information about high-level data flow and about the widths of data path signals. We introduce a one-to-one abstraction technique for RTL property checking which exploits such high-level information. Given an RTL circuit description, a scaled-down abstract model is computed in which signal widths are reduced with respect to an additionally given formal property. For each data path and each signal accessing the data path, the original width n is shrunken to the minimum width m<=n such that the property which is to be checked holds for the scaled model if and only if it holds for the original design. We furthermore provide a technique which, if the property does not hold, computes counterexamples for the original design from counterexamples found on the reduced model. Thus, the verification task can be completely carried out on the scaled-down version of the design; false-negatives cannot occur. The complexity of SAT and BDD based model checking often depends on the number of bits occurring in a design and therefore depends on the widths of the data path signals. Linear signal width reductions result in exponentially smaller state spaces. Hence, automated data path scaling can significantly speed up the runtimes of verification tools and allows larger design sizes to be handled. Experimental results on large industrial circuits demonstrate the applicability and efficiency of the proposed method.