Verification complexity reduction via range-preserving input-to-constant conversion

摘要

A logic verification program, method and system provide an efficient behavior when verifying large logic designs. The logic is partitioned by cut-nodes that dominate two or more RANDOMS and a check is performed for a given cut-node to determine whether any of the dominated RANDOMS can be merged to a constant by performing satisfiability checks with each RANDOM merged to a constant, to determine whether a range of output values for the given cut-node has been reduced by merging the RANDOM. If the range is not reduced, the RANDOM can be added to the set of merge-able RANDOMS along with the corresponding constant value. If the range has been reduced, the opposite constant value is tried for a node and if the range is reduced for both constants, then the cut-node is abandoned for merging that dominated RANDOM and the next dominated RANDOM is tried.