Optimizing constraint solving by rewriting at least one modulo constraint
Methods and apparatuses are described for assigning random values to a set of random variables so that the assigned random values satisfy a set of constraints. A constraint solver can receive a set of constraints that is expected to cause performance problems when the system assigns random values to the set of random variables in a manner that satisfies the set of constraints. For example, modulo constraints and bit-slice constraints can cause the system to perform excessive backtracking when the system attempts to assign random values to the set of random variables in a manner that satisfies the set of constraints. The system can rewrite the set of constraints to obtain a new set of constraints that is expected to reduce and/or avoid the performance problems. The system can then assign random values to the set of random variables based on the new set of constraints.
1. In an electronic design automation (EDA) software tool in a computer, a method for assigning random values to a set of random variables, the method comprising:
the EDA software tool in the computer receiving a set of constraints, wherein each constraint is defined over one or more random variables from the set of random variables, wherein the set of constraints includes one or more modulo constraints that use a modulo operator;
the EDA software tool in the computer rewriting the set of constraints to obtain a new set of constraints, wherein said rewriting includes replacing at least one modulo constraint whose divisor is not equal to a power of two with one or more non-modulo constraints, wherein the one or more non-modulo constraints use only non-modulo operators, and wherein the one or more non-modulo constraints use at least one random variable other than those used in the modulo constraint; and
the EDA software tool in the computer assigning random values to the set of random variables based on the new set of constraints, wherein the EDA software tool in the computer uses the set of random variables to generate one or more random stimuli to perform functional verification on a circuit design under verification.
2. The method of claim 1 , wherein said rewriting includes replacing modulo expression “expr1% expr2” by expression “expr1 & (|expr2|−1)” if “expr2” is equal to a power of two, wherein “expr1” and “expr2” are expressions.
3. The method of claim 1 , wherein said rewriting includes replacing modulo constraint “expr1% expr2==expr3” by constraints “(expr1==q*expr2+r) && (|r|<|expr2|)” and “r==expr3,” wherein “expr1,” “expr2,” and “expr3” are expressions, and “q” and “r” are random variables.
4. The method of claim 1 , wherein rewriting the set of constraints includes:
determining multiple modulo constraints that each include a modulo expression with the same dividend and divisor; and
reusing a set of random variables to rewrite the modulo expression in the multiple modulo constraints.
5. The method of claim 1 , wherein rewriting the set of constraints includes not rewriting guarded modulo constraint “expr3→(expr1% expr2)==expr4” if expr3 is expected to evaluate to “FALSE,” wherein “expr1,” “expr2,” “expr3,” and “expr4” are expressions.
6. A non-transitory computer-readable storage medium storing instructions of an electronic design automation (EDA) software tool that, when executed by a computer, cause the computer to perform a method for assigning random values to a set of random variables, the method comprising:
the computer receiving a set of constraints, wherein each constraint is defined over one or more random variables from the set of random variables, wherein the set of constraints includes one or more modulo constraints that use a modulo operator;
the computer rewriting the set of constraints to obtain a new set of constraints, wherein said rewriting includes replacing at least one modulo constraint whose divisor is not equal to a power of two with one or more non-modulo constraints, wherein the one or more non-modulo constraints use only non-modulo operators, and wherein the one or more non-modulo constraints use at least one random variable other than those used in the modulo constraint; and
the computer assigning random values to the set of random variables based on the new set of constraints, wherein the EDA software tool uses the set of random variables to generate one or more random stimuli to perform functional verification on a circuit design under verification.
7. The non-transitory computer-readable storage medium of claim 6 , wherein said rewriting includes replacing modulo expression “expr1% expr2” by expression “expr1 & (|expr2|−1)” if “expr2” is equal to a power of two, wherein “expr1” and “expr2” are expressions.
8. The non-transitory computer-readable storage medium of claim 6 , wherein said rewriting includes replacing modulo constraint “expr1% expr2==expr3” by constraints “(expr1==q*expr2+r) && (|r<|expr2|)” and “r==expr3,” wherein “expr1,” “expr2,” and “expr3” are expressions, and “q” and “r” are random variables.
9. The non-transitory computer-readable storage medium of claim 6 , wherein rewriting the set of constraints includes:
determining multiple modulo constraints that each include a modulo expression with the same dividend and divisor; and
reusing a set of random variables to rewrite the modulo expression in the multiple modulo constraints.
10. The non-transitory computer-readable storage medium of claim 6 , wherein rewriting the set of constraints includes not rewriting guarded modulo constraint “expr3→(expr1% expr2)==expr4” if expr3 is expected to evaluate to “FALSE,” wherein “expr1,” “expr2,” “expr3,” and “expr4” are expressions.
11. A computer system, comprising:
a processor; and
a non-transitory computer-readable storage medium storing instructions of an electronic design automation (EDA) software tool that, when executed by the processor, cause the computer system to perform a method for assigning random values to a set of random variables, the instructions comprising:
instructions for receiving a set of constraints, wherein each constraint is defined over one or more random variables from the set of random variables, wherein the set of constraints includes one or more modulo constraints that use a modulo operator;
instructions for rewriting the set of constraints to obtain a new set of constraints, wherein said instructions for rewriting the set of constraints include instructions for replacing at least one modulo constraint whose divisor is not equal to a power of two with one or more non-modulo constraints, wherein the one or more non-modulo constraints use only non-modulo operators, and wherein the one or more non-modulo constraints use at least one random variable other than those used in the modulo constraint; and
instructions for assigning random values to the set of random variables based on the new set of constraints, wherein the EDA software tool uses the set of random variables to generate one or more random stimuli to perform functional verification on a circuit design under verification.
12. The computer system of claim 11 , wherein the instructions for said rewriting include instructions for replacing modulo expression “expr1% expr2” by expression “expr1 & (|expr2|−1)” if “expr2” is equal to a power of two, wherein “expr1” and “expr2” are expressions.
13. The computer system of claim 11 , wherein the instructions for said rewriting include instructions for replacing modulo constraint “expr1% expr2==expr3” by constraints “(expr1==q*expr2+r) && (|r<|expr2|)” and “r==expr3,” wherein “expr1,” “expr2,” and “expr3” are expressions, and “q” and “r” are random variables.
14. The computer system of claim 11 , wherein the instructions for rewriting the set of constraints include:
instructions for determining multiple modulo constraints that each include a modulo expression with the same dividend and divisor; and
instructions for reusing a set of random variables to rewrite the modulo expression in the multiple modulo constraints.
15. The computer system of claim 11 , wherein the instructions for rewriting the set of constraints include instructions for not rewriting guarded modulo constraint “expr3→(expr1% expr2)==expr4” if expr3 is expected to evaluate to “FALSE,” wherein “expr1,” “expr2,” “expr3,” “expr4” are expressions.
16. In an electronic design automation (EDA) software tool in a computer, a method for assigning random values to a set of random variables, the method comprising:
the EDA software tool in the computer receiving a set of constraints, wherein each constraint is defined over one or more random variables from the set of random variables, wherein the set of constraints includes multiple modulo constraints that use a modulo operator;
the EDA software tool in the computer rewriting the set of constraints to obtain a new set of constraints, wherein said rewriting comprises replacing multiple modulo constraints with one or more non-modulo constraints that use only non-modulo operators, and wherein said rewriting further comprises:
determining multiple modulo constraints that each include a modulo expression with the same dividend and divisor, and
reusing a set of random variables to rewrite the modulo expression in the multiple modulo constraints; and
the EDA software tool in the computer assigning random values to the set of random variables based on the new set of constraints, wherein the EDA software tool in the computer uses the set of random variables to generate one or more random stimuli to perform functional verification on a circuit design under verification.
17. A non-transitory computer-readable storage medium storing instructions of an electronic design automation (EDA) software tool that, when executed by a computer, cause the computer to perform a method for assigning random values to a set of random variables, the method comprising:
the computer receiving a set of constraints, wherein each constraint is defined over one or more random variables from the set of random variables, wherein the set of constraints includes multiple modulo constraints that use a modulo operator;
the computer rewriting the set of constraints to obtain a new set of constraints, wherein said rewriting comprises replacing multiple modulo constraints with one or more non-modulo constraints that use only non-modulo operators, and wherein said rewriting further comprises:
determining multiple modulo constraints that each include a modulo expression with the same dividend and divisor, and
reusing a set of random variables to rewrite the modulo expression in the multiple modulo constraints; and
the computer assigning random values to the set of random variables based on the new set of constraints, wherein the EDA software tool uses the set of random variables to generate one or more random stimuli to perform functional verification on a circuit design under verification.