Digital circuit designs are usually given as Register-Transfer-Level (RTL)
specifications, but most of today's hardware verification tools are based on
bit-level methods, using SAT or BDD-based techniques. RTL specifications
contain more explicite structural information than bit-level descriptions.
This paper presents a new approach to scale down design sizes by exploiting
word-level information. Word-level signals represent vectors of bits. We
introduce a one-to-one abstraction technique for RTL property checking which
computes a scaled-down abstract model of a given digital circuit in which
signal widths are reduced. For each signal, its original width n is shrunken
to the minimum m <= n such that the property, which is to be checked, holds
for the reduced model if and only if it holds for the original
design. If the property fails, general counterexamples can be computed from
counterexamples found on the reduced model. The verification task can be
completely carried out on the scaled-down version of the design;
false-negatives cannot occur. Linear signal width reductions result
in exponentially smaller state spaces and have a significant impact on the
runtimes of verification tools. Experimental results on large
industrial circuits have demonstrated the applicability and efficiency of our
method.
