Efficient decision procedure for non-linear arithmetic constraints using CORDIC

In verification of hybrid discrete-continuous and embedded control systems, one encounters decision problems involving non-linear constraints. We propose an efficient decision procedure (CORD) for such decisions problems using CORDIC algorithms, and an off-the-shelf SMT(LA) (Satisfiability Modulo Theory for Linear Arithmetic) solver, for given precision requirements. We first translate the non-linear part of the decision problem to a SMT(LA) formula using CORDIC algorithms, accounting for all the inaccuracies safely. In the translation, we use a normalization scheme, combined with interval bounds to obtain a linearized formula without compromising the precision requirements. On such a linearized formula, we devise a DPLL-style Interval Search Engine (DISE) that explores various combinations of interval bounds using a SMT(LA) solver. In our experiments, we demonstrate the efficacy of our approach, and compare it with a latest state-of-the-art decision procedure.