Normalization at the arithmetic bit level

ABSTRACT

We propose a normalization technique for verifying arithmetic circuits in a bounded model checking environment. Our technique operates on the arithmetic bit level (ABL) description of the arithmetic circuit parts and the property. The ABL description can easily be provided by the front-end of an RTL property checker. The proposed normalization greatly simplifies the SAT instances to be solved for arithmetic circuit verification. Our approach has been applied successfully to verify the integer pipeline of an industrial microprocessor with advanced DSP capabilities.

REFERENCES

• 1: Infineon TriCore 2 Architecural Manual. http://www.infineon.com/tricore.
• 2: Gilles Audemard , Piergiorgio Bertoli , Alessandro Cimatti , Artur Kornilowicz , Roberto Sebastiani, A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions, Proceedings of the 18th International Conference on Automated Deduction, p.195-210, July 27-30, 2002
• 3: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 4: 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
• 5: Donald Chai , Andreas Kuehlmann, A fast pseudo-boolean constraint solver, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776041]
• 6: N. Een and N. Sörensson. An extensible SAT-solver. In Proc. 6. Intl. Conf. on Theory and Applications of Satisfiability Testing(SAT 2003), May 2003.
• 7: F. Fallah, S. Devadas, and K. Keutzer. Functional vector generation for HDL models using linear programming and boolean satisfiability. IEEE Transactions on CAD, CAD-20(8), 2001.
• 8: Peer Johannsen, BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction, Proceedings of the 13th International Conference on Computer Aided Verification, p.373-377, July 18-22, 2001
• 9: P. Johannsen and R. Drechsler. Formal verification on the RT level computing one-to-one design abstractions by signal width reduction. In Proc. IFIP International Conference on Very Large Scale Integration(IFIP VLSI-SOC 2001), Montpellier, France, 2001.
• 10: Dominik Stoffel , Wolfgang Kunz, Verification of integer multipliers on the arithmetic bit level, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 11: Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Arithmetic Reasoning in DPLL-Based SAT Solving, Proceedings of the conference on Design, automation and test in Europe, p.10030, February 16-20, 2004
• 12: Klaus Winkelmann , Hans-Joachim Trylus , Dominik Stoffel , Görschwin Fey, Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor, Proceedings of the conference on Design, automation and test in Europe, p.10162, February 16-20, 2004
• 13: Zhihong Zeng , Maciej J. Ciesielski , Bruno Rouzeyre, Functional Test Generation using Constraint Logic Programming, Proceedings of the IFIP TC10/WG10.5 Eleventh International Conference on Very Large Scale Integration of Systems-on/Chip: SOC Design Methodologies, p.375-387, December 03-05, 2001
• 14: 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

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Verification

Keywords:
SAT, arithmetic bit level normalization, property checking