Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques

We present a new approach to checking assertion proper tics for RTL design verification. Our approach combines structural, word-level automatic test pattern generation (ATPG) and modular arithmetic constraint-solving techniques to solve the constraints imposed by the target assertion property. Our word-level ATPG and implication technique not only solves the constraints on the control logic, but also propagates the logic implications to the datapath. A novel arithmetic constraint solver based on modular number system is then employed to solve the remaining constraints in datapath. The advantages of the new method are threefold. First, the decision-making process of the word-level ATPG is confirmed to the selected control signals only Therefore, the enumeration of enormous number of choices at the datapath signals is completely avoided. Second, our new implication translation techniques allow word-level logic implication being performed across the boundary of datapath and control logic, and therefore, efficiently cut down the ATPG search space. Third, our arithmetic constraint solver is based on modular instead of integral number system. it can thus avoid the false negative effect resulting from the bit-vector value modulation. A prototype system has been built which consists of an industrial front-end HDL parser a property-to-constraint co,verter and the ATPG/arithmetic constraint-solving engine. The experimental results on some public benchmark and industrial circuits demonstrate the efficiency of our approach and its applicability to large industrial designs.