Specifying and verifying imprecise sequential datapaths by Arithmetic Transforms

ABSTRACT

We address verification of imprecise datapath circuits with sequential elements. Using Arithmetic Transform (AT) and its extensions, we verify the sequential datapath circuits with finite precision. An efficient formulation of the precision verification is presented as a polynomial maximization search over Boolean inputs. Using a branch-and-bound search for the precision error and the block-level composition of ATs, we verify the approximated, rounded and truncated pipelined datapaths.

REFERENCES

• 1: Randal E. Bryant , Yirng-An Chen, Verification of arithmetic circuits with binary moment diagrams, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.535-541, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217583]
• 2: M. Huhn , K. Schneider , Th. Kropf , G. Logothetis, Verifying imprecisely working arithmetic circuits, Proceedings of the conference on Design, automation and test in Europe, p.13-es, January 1999, Munich, Germany [doi>10.1145/307418.307451]
• 3: Shinji Kimura, Residue BDD and its application to the verification of arithmetic circuits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.542-545, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217584]
• 4: Armita Peymandoust , Giovanni De Micheli, Symbolic algebra and timing driven data-flow synthesis, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 5: Katarzyna Radecka , Zeljko Zilic, Using Arithmetic Transform for Verification of Datapath Circuits via Error Modeling, Proceedings of the 18th IEEE VLSI Test Symposium (VTS'00), p.271, April 30-May 04, 2000
• 6: Arithmetic Transforms for Verifying Compositions of Sequential Datapaths, Proceedings of the International Conference on Computer Design: VLSI in Computers & Processors, p.348, September 23-26, 2001
• 7: James Smith , Giovanni De Micheli, Polynomial circuit models for component matching in high-level synthesis, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.9 n.6, p.783-800, 12/1/2001 [doi>10.1109/92.974892]
• 8: Synopsys Inc, "Co-centric Fixed Point Designer Datasheet", 2002.
• 9: Zeljko Zilic , Katarzyna Radecka, On feasible multivariate polynomial interpolations over arbitrary fields, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.67-74, July 28-31, 1999, Vancouver, British Columbia, Canada [doi>10.1145/309831.309863]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Sequential circuits

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.1 Numerical Algorithms and Problems
          Subjects: Computation of transforms (e.g., fast Fourier transform)

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Analysis of algorithms

General Terms:
Algorithms, Design, Theory