Result: CLP based static property checking

We present a novel approach to static check properties for RT-Level design verification. Our approach combines program-slicing based static design extraction, word-level SAT solving and dynamic searching techniques. The design extraction makes property-checking concentrate on the design parts related to the given properties, thus large practical designs can be handled. Constraint Logic Programming (CLP) naturally models mixed bit-level and word-level constraints, and word-level SAT technique effectively solves the mixed constraints in a unified framework, which greatly improves the performance of property checking. Initial searching states derived from dynamic simulation dramatically accelerate the searching process of property checking. A prototype system has been built, and the experimental results on some public benchmark and industrial circuits demonstrate the efficiency of our approach and its applicability to large practical designs.