Using word-level ATPG and modular arithmetic constraint-solving techniquesfor assertion property checking

We present a new approach to checking assertion properties for register-tra nsfer level (RTL) design verification. Our approach combines structural wor d-level automatic test pattern generation (ATPG) and modular arithmetic con straint-solving techniques to solve the constraints imposed by the target a ssertion property, Our word-level ATPG and implication technique not only s olves the constraints on the control logic, but also propagates the logic i mplications to the datapath, A novel arithmetic constraint solver based on modular number system is then employed to solve the remaining constraints i n datapath, The advantages of the new method are threefold, First, the deci sion-making process of the word-level ATPG is confined to the selected cont rol 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 a cross the boundary of datapath and control logic and, therefore, efficientl y cut down the ATPG search space. Third, our arithmetic constraint solver i s based on modular instead of integral number system. It can thus avoid the false-negative effect resulting from the bit-vector value modulation A pro totype system has been built that consists of an industrial front-end hardw are description language (HDL) parser, a property-tu-constraint converter, and the ATPG/arithmetic constraint-solving engine. The experimental results on some public benchmark and industrial circuits demonstrate the efficienc y of our approach and its applicability to large industrial designs.