Computing One-to-One Minimum-Width Abstractions of Digital Designs for RTL Property Checking

Peer Johannsen

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems