Verification of arithmetic datapaths using polynomial function models and congruence solving

ABSTRACT

This paper addresses the problem of solving finite word-length (bit-vector) arithmetic with applications to equivalence verification of arithmetic datapaths. Arithmetic datapath designs perform a sequence of Add, Mult, Shift, Compare, Concatenate, Extract, etc., operations over bit-vectors. We show that such arithmetic operations can be modeled, as constraints, using a system of polynomial functions of the type f: Z₂n₁ x Z₂n₂ x ··· x Z₂n_d → Z₂m. This enables the use of modulo-arithmetic based decision procedures for solving such problems in one unified domain. We devise a decision procedure using Newton's p-adic iteration to solve such arithmetic with composite moduli, while properly accounting for the word-sizes of the operands. We describe our implementation and show how the basic p-adic approach can be improved upon. Experiments are performed over some communication and signal processing designs that perform non-linear and polynomial arithmetic over word-level inputs. Results demonstrate the potential and limitations of our approach, when compared against SAT-based approaches.

REFERENCES

• 1: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 2: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 3: B. Dutertre and L. De Moura, "The YICES SMT Solver", http://yices.csl.sri.com/tool-paper.pdf, 2006.
• 4: Z. Zeng , P. Kalla , M. Ciesielski, LPSAT: a unified approach to RTL satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.398-402, March 2001, Munich, Germany
• 5: R. Bruttomesso, A. Cimmatti, and et al., "A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems", in Proc. CAV, LNCS, pp. 247--260. Springer-Verlag, 2007.
• 6: V. Ganesh and D. Dill, "A Decision Procedure for Bit-Vectors and Arrays", in Proc. (CAV), LNCS. Springer-Verlag, 2007.
• 7: David Cyrluk , M. Oliver Möller , Harald Rueß, An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors, Proceedings of the 9th International Conference on Computer Aided Verification, p.60-71, June 22-25, 1997
• 8: R. Brant, D. Kroening, and et al, "Deciding Bit-Vector Arithmetic with Abstraction", in Proc. TACAS, pp. 358--372, 2007.
• 9: N. Shekhar, P. Kalla, and F. Enescu, "Equivalence Verification of Polynomial Datapaths using Ideal Membership Testing", IEEE Trans. CAD, vol. 26, pp. 1320--1330, July 2007.
• 10: N. Shekhar, P. Kalla, M. B. Meredith, and F. Enescu, "Simulation Bounds for Equivalence Verification of Polynomial Datapaths using Finite Ring Algebra", IEEE Trans. VLSI, vol. 16, pp. 376--387, 2008.
• 11: N. Shekhar , P. Kalla , F. Enescu , S. Gopalakrishnan, Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.291-296, November 06-10, 2005, San Jose, CA
• 12: Zhibo Chen, On polynomial functions from Zn1×Zn2× &ldots;×Znr to Zm , Discrete Mathematics, v.162 n.1-3, p.67-76, Dec. 25, 1996 [doi>10.1016/0012-365X(95)00305-G]
• 13: R. Zippel, Effective Polynomial Computation, Kluwer Acad. Pub., 1993.
• 14: D. Babic and M. Musuvathi, "Modular Arithmetic Decision Procedure", Technical Report TR-2005-114, Microsoft Research, 2005.
• 15: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 16: Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Normalization at the arithmetic bit level, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065699]
• 17: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277186]
• 18: M. Oliver Möller , Harald Rueß, Solving Bit-Vector Equations, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.36-48, November 04-06, 1998
• 19: Farzan Fallah , Srinivas Devadas , Kurt Keutzer, Functional vector generation for HDL models using linear programming and 3-satisfiability, Proceedings of the 35th annual conference on Design automation, p.528-533, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277187]
• 20: Raik Brinkmann , Rolf Drechsler, RTL-Datapath Verification using Integer Linear Programming, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.741, January 07-11, 2002
• 21: C.-Y. Huang and K.-T. Cheng, "Using Word-Level ATPG and Modular Arithmetic Constraint Solving Techniques for Assertion Property Checking", IEEE Trans. CAD, vol. 20, pp. 381--391, 2001.
• 22: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 23: Manjul Bhargava, Congruence preservation and polynomial functions from Zn to Zm, Discrete Mathematics, v.173 n.1-3, p.15-21, Aug. 20, 1997 [doi>10.1016/S0012-365X(96)00093-3]
• 24: Markus Müller-Olm , Helmut Seidl, Analysis of modular arithmetic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.29-es, August 2007 [doi>10.1145/1275497.1275504]
• 25: A. K. Verma , P. Ienne, Improved use of the carry-save representation for the synthesis of complex arithmetic circuits, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.791-798, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382683]
• 26: M. R. Guthaus , J. S. Ringenberg , D. Ernst , T. M. Austin , T. Mudge , R. B. Brown, MiBench: A free, commercially representative embedded benchmark suite, Proceedings of the Workload Characterization, 2001. WWC-4. 2001 IEEE International Workshop, p.3-14, December 02-02, 2001 [doi>10.1109/WWC.2001.15]
• 27: A. Hosangadi , F. Fallah , R. Kastner, Factoring and eliminating common subexpressions in polynomial expressions, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.169-174, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382566]