CLP Based Static Property Checking

Abstract

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.

This work is supported by the National Science Foundation of China (NSFC) under grant No. 60303011 and 90207019.