Implication of arithmetic operations with multibit operands for verification tests generation

The range method of data representation of the different formats, namely of completely undefined and partially defined vectors, is introduced. Its unified nature permits to speed up processing of operands while performing implication procedures. To hold the verification it is useful to use multidigit path sensitization, which consists of two steps: propagation and satisfaction. These steps require execution of direct implication and backtracing. Algorithms for execution of direct implication and backtracing of arithmetic operations using range representation of operands are proposed.