Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

Abstract: A formal verification method is presented to verify the loop ordering of a high level transformed description against its original specification. The verification is done in an automatic way and its complexity is independent on the sizes of the loops bounds. Any practical structure of loop nests can be handled. The method is especially suited for applications in the area of speech, image and video processing, front-end telecom and numerical computing systems which exhibit many loops and complex multi-dimensional signals. The efficiency of the approach is demonstrated on several realistic examples.

REFERENCES

• 1: B.J.S. De Loore, P. Crombez, A. Delaruelle, P. Sheridan, R. Woudsma, C. Niessen, 3. Biesterbos, W. Gubbels, and W. Repko. The design of a competitive asic for the consumer market using the PIRAMID design system. In Proc. IEEE ASIC 92 Conference, pages 520-524, 1992.
• 2: P. E. R. Lippens , J. L. van Meerbergen , A. van der Werf , W. F. J. Verhaegh , B. T. McSweeney , J. O. Huisken , O. P. McArdle, PHIDEO: a silicon compiler for high speed algorithms, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
• 3: F. Franssen, F. Balasa, M. van Swaaij, F. Catthoor, and H. De Man. Modeling multi-dimensional data and control flow. IEEE Trans. on VLSI systems, 1(3):319- 327, Sept. 1993.
• 4: Utpal K. Banerjee, Loop Transformations for Restructuring Compilers: The Foundations, Kluwer Academic Publishers, Norwell, MA, 1993
• 5: M. E. Wolf , M. S. Lam, A Loop Transformation Theory and an Algorithm to Maximize Parallelism, IEEE Transactions on Parallel and Distributed Systems, v.2 n.4, p.452-471, October 1991 [doi>10.1109/71.97902]
• 6: F.Franssen, L.Nachtergaele, H.Samsom, F.Catthoor, and H.De Man. Control flow optimization for fast system simulation and storage minimization. In Proc. EDAC, pages 20-24, Paris, March 1994.
• 7: L. Claesen, F. Proesmans, E. Verlind, and H. De Man. SFG-tracing: A methodology for the automatic verification of MOS transistor level implementations from high level behavioral specifications. In Int. Workshop on Formal Methods in VLSI Design, 9- 11 Jan. 1991.
• 8: P. Quinton and Y. Robert (eds.). Algorithms and parallel VLSI architectures II. Elsevier, 1992.
• 9: Lars Svensson , Francky Catthoor, Application-Driven Architecture Synthesis, Kluwer Academic Publishers, Norwell, MA, 1993
• 10: Z. Chamski, H. Le Verge, C. Mauras, and P. Quinton. Interactive design of parallel algorithms using the ALPHA du Centaur environment. In Int. Workshop on Compilers for Parallel Computers, pages 399-410, Paris, Dec. 1990.
• 11: Simon Finn, Michael P. Fourman, Michael Francis, and Robert Harris. Formal system design- interactive synthesis based on computer-assisted formal reasoning. In Int. Workshop on Applied Formal Methods for Correct VLSI Design, pages 97-110, Nov. 1989.
• 12: Michael C. McFarland, Formal analysis of correctness of behavioral transformations, Formal Methods in System Design, v.2 n.3, p.231-257, June 1993 [doi>10.1007/BF01384133]
• 13: P.F.A. Middelhoek. Transformational design of digital circuits. In Proc. of the Seventh Computersystems Workshop, pages 57-69, Eindhoven, Nov. 1993.
• 14: P. Feautrier. Dataflow analysis of array and scalar references. Int. Journal of Parallel Programming, 20:23-53, 1991.
• 15: H. Samsom, F. Franssen, F. Catthoor, and H. De Man. Verification of loop transformations for real time signal processing applications. In VLSI Signal Processing VII, pages 208-217. IEEE, Oct. 1994.
• 16: Mentor Graphics Corp. DSP Architect DFL User's and Reference Manual, Software Version 8.2_5, 1993.
• 17: William Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.4-13, November 18-22, 1991, Albuquerque, New Mexico, United States [doi>10.1145/125826.125848]
• 18: Paul Le Guernic, The SIGNAL programming environment, Proceedings of the international workshop on Algorithms and parallel VLSI architectures II, p.347-358, January 1992, Gers, France

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Systems specification methodology

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Reliability, availability, and serviceability

  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Design, Languages, Verification

Keywords:
complexity, computational complexity, formal specification, formal verification, formal verification method, front-end telecom, image processing, image processing specifications, loop ordering, numerical computing, system level verification, video processing