Efficient decision method for real non-linear arithmetic constraints

1. A method for solving a decision problem having Boolean combinations of linear and non-linear operations, comprising:

translating the non-linear real operations using a COordinate Rotation DIgital Computer (CORDIC) method programmed on a computer device into linear operations maintaining a given accuracy;

combining linear and translated linear operations into a formula; and

solving satisfiability of the formula using a decision procedure for Boolean combinations of linear operations over integers and reals.

2. The method as recited in claim 1 , wherein translating includes normalizing one or more non-linear inputs with respect to corresponding variable interval bounds.

3. The method as recited in claim 2 , wherein the variable interval bounds on the non-linear inputs have a fixed ratio of upper to lower bounds.

4. The method as recited in claim 1 , wherein the decision procedure includes an interval search procedure that determines whether the formula is satisfiability or not based on whether a feasible combination of interval bounds exists or not, respectively.

5. The method as recited in claim 4 , wherein the interval search procedure determines the feasibility of interval combinations of the non-linear inputs by searching over lower and upper bounds of the interval iteratively, by employing results from previous iterations.

6. The method as recited in claim 4 , wherein the interval search procedure includes employing a lazy bound refinement that employs refinement-based reasoning iteratively to explore combinations of interval bounds.

7. The method as recited in claim 6 , wherein the lazy bound refinement uses a branch and bound-style interval search wherein infeasible interval combinations are learned from previous iterations, and not visited in a subsequent search.

8. The method as recited in claim 7 , wherein the lazy bound refinement uses a branch and bound-style interval search wherein partial feasible interval combinations from previous iterations are used in guiding the subsequent search.

9. The method as recited in claim 1 , further comprising accounting for inaccuracies in the CORDIC method by computing error correction and including error correction terms in the translating step.

10. The method as recited in claim 1 , wherein the non-linear operations include transcendental and algebraic functions over real numbers with a given precision.

11. The method as recited in claim 1 , wherein the decision procedure includes employing a Satisfiability Modulo Theory for Linear Arithmetic solver (SMT(LA)).

12. The method as recited in claim 1 , further comprising verifying the linear and non-linear operations in computer software.

13. The method as recited in claim 1 , wherein method includes checking a model with linear and non-linear operations and specified properties by Bounded Model Checking, by unrolling the model for a pre-determined depth; translating the unrolled model and properties into a formula with linear and non-linear operations; performing a satisfiability check on the formula; and verifying correctness of the model with respect to the specified properties.

14. The method as recited in claim 1 , further comprising handling non-linear arithmetic for at least one of hardware and software verification.

15. A computer readable storage medium comprising a computer readable program for solving a decision problem having Boolean combinations of linear and non-linear real operations, wherein the computer readable program when executed on a computer causes the computer perform the steps of:

translating the non-linear real operations using a COordinate Rotation DIgital Computer (CORDIC) method programmed on a computer device into linear operations maintaining a given accuracy;

combining linear and translated linear operations into a formula; and

solving satisfiability of the formula using a decision procedure for Boolean combinations of linear operations over integers and reals.

16. A system for solving a decision problem having Boolean combinations of linear and non-linear operations, comprising:

a computer configured to translate non-linear real operations using a COordinate Rotation DIgital Computer (CORDIC) method programmed on the computer into linear operations maintaining a given accuracy, the computer configured to combine linear and translated linear operations into a formula; and

a Satisfiability Modulo Theory for Linear Arithmetic solver (SMT(LA)) configured to solve satisfiability of the formula wherein the solving includes at least one of normalizing one or more non-linear inputs with respect to corresponding variable interval bounds and solving the formula by an interval search procedure that determines whether the formula is satisfiable or not based on whether a feasible combination of interval bounds exists or not, respectively.

17. The system as recited in claim 16 , further comprising error correction terms to account for inaccuracies in the CORDIC method.

18. The system as recited in claim 16 , wherein the interval search includes a lazy bound refinement that employs refinement-based reasoning to explore combinations of interval bounds.