Hierarchical constraint solving in the parametric form with applications to efficient symbolic simulation based verification

We consider the language of constraint formula involving Boolean connectives, and relational, logical, and arithmetic operations on bit vectors. An example of a formula in this language is F=((A+B)<C)∧(A+D)∧((A+D)⩽E)∧(<(G&H)) where A through H are bit vectors, and & denotes bit-wise and. We address the problem of generating the satisfying set of formulas such as F in the parametric form; in other words, corresponding to the Boolean variable υ_i (O⩽i<N) used in F, we seek to find an expression ε_i over new variables p_i (O⩽i<N+log₂(M)), where M is the cardinality of the satisfying set of F. The p_i are called parametric variables, and for each value assignment to them, the vector of ε_is satisfy F when substituted for υ_i (O⩽i<N). This problem arises in a number of occasions, typically during the generation of symbolic vectors for use in symbolic simulation based verification. We propose a new method to obtain the parametric solutions ε_i such that both their sizes as well as variations in their sizes is small. Small sizes and small variations in sizes of parametric expressions prove to be important for verifying many practical examples through symbolic simulation