Prototyping time- and space-efficient computations of algebraic operations over dynamically reconfigurable systems modeled by rewriting-logic

Abstract

Many algebraic operations can be efficiently implemented as pipe networks in arrays of functional units such as systolic arrays that provide a large amount of parallelism. However, the applicability of classical systolic arrays is restricted to problems with strictly regular data dependencies yielding only arrays with uniform linear pipes. This limitation can be circumvented by using reconfigurable systolic arrays or reconfigurable data path arrays, where the node interconnections and operations can be redefined even at run time. In this context, several alternative reconfigurable systolic architectures can be explored and powerful tools are needed to model and evaluate them. Well-known rewriting-logic environments such as ELAN and Maude can be used to specify and simulate complex application-specific integrated systems. In this article we propose a methodology based on rewriting-logic which is adequate to quickly model and evaluate reconfigurable architectures (RA) in general and, in particular, reconfigurable systolic architectures. As an interesting case study we apply this rewriting-logic modeling methodology to the space-efficient treatment of the Fast-Fourier Transform (FFT). The FFT prototype conceived in this way, has been specified and validated in VHDL using the Quartus II system.

References

1. Abnous, A., Seno, K., Ichikawa, Y., Wan, M., and Rabaey, J. M. 1998. Evaluation of a low-power reconfigurable DSP architecture. In Proceedings of the 5th Reconfigurable Architectures Workshop (IPPS/SPDP '98 Orlando, Fl.). 55--60.]]
2. Acquah, J. and Rice, M. D. 1987. Constant geometry algorithms for computing Fourier Transforms on transputer arrays. Tech. rep. Melpar---E-Systems Division, Fairfax, VA.]]
3. Akl, S. G. 1997. Parallel Computation: Models and Methods. Prentice-Hall, Englewood Cliffs, NJ.]]
4. Altera® Corporation. 2004. Quartus II User Guide. Available online at http://www.altera.com.]]
5. Amor, M., Martin, M. J., Blanco, D., Plata, O., Rivera, F. F., and Arguello, F. 1994. Vectorization of the radix r self-sorting FFT. In Proceedings of Parallel Processing: CONPAR94/ VAPP VI, Linz, Austria, September 6--8, B. Buchberger and J. Volkert, Eds. Lecture Notes in Computer Science, vol. 894. Springer-Verlag, Berlin, Germany, 208--217.]]
6. Arguello, F., Amor, M., and Zapata, E. L. 1996. FFTs on mesh connected computers. Parall. Comput. 22, 1, 19--39.]]
7. Arvind and Shen, X. 1999. Using term rewriting systems to design and verify processors. IEEE Micro 19, 3, 36--46.]]
8. Ayala-Rincón, M., Neto, R. M., Jacobi, R. P., Llanos, C. H., and Hartenstein, R. W. 2002. Applying ELAN strategies in simulating processors over simple architectures. In Proceedings 2nd Conference on Reduction Strategies in Rewriting and Programming. Electron. Notes Theoret. Comput. Sci. 70, 6, 1--16.]]
9. Ayala-Rincón, M., Nogueira, R. B., Jacobi, R. P., Llanos, C. H., and Hartenstein, R. W. 2003. Modeling a reconfigurable system for computing the FFT in place via rewriting-logic. In Proceedings of the 16th Symposium on Integrated Circuits and System Design (SBCCI'03). IEEE Computer Science Press, Los Alamitos, CA, 205--210.]]
10. Ayala-Rincón, M., Jacobi, R. P., Carvalho, L. G. A., Llanos, C. H., and Hartenstein, R. 2004. Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic. In Proceedings of the 17th Symposium on Integrated Circuits and System Design (SBCCI'04). ACM Press, New York, NY, 248--253. Journal version in Genetic and Molecular Research 4, 3, 543--552 (2005).]]
11. Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press, Cambridge, U.K.]]
12. Baase, S. and Van Gelder, A. 1999. Computer Algorithms: Introduction to Design and Analysis. Addison-Wesley, Reading, MA.]]
13. Becker, J. and Hartenstein, R. W. 2003. Configware and morphware going mainstream. J. Syst. Architect. 49, 127--142.]]
14. Becker, J., Hartenstein, R. W., Herz, M., and Nageldinger, U. 1998. Parallelization in co-compilation for configurable accelerators. In Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC, Yokohama, Japan). 23--33.]]
15. Bjesse, P., Claessen, K., Sheeran, M., and Singh, S. 1998. Lava: Hardware design in Haskell. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming(ICFP '98). SIGPLAN Not. 34, 1, 174--184.]]
16. Borovanský, P., Kirchner, C., Kirchner, H., and Moreau, P.-E. 2002. ELAN from a rewriting logic point of view. Theoret. Comput. Sci. 285, 2, 155--185.]]
17. Caspi, P., Sangiovanni-Vincentelli, A., et al. 2005. Guidelines for a graduate curriculum on embedded software and systems. ACM Trans. Embedd. Comput. Syst. 4, 3, 587--611.]]
18. Catthoor, F., Wuytack, S. W., Degreef, E., Balasa, F., Nachtergaele, L., and Vandecappelle, A. 1998. Custom Management Methodology Kluwer, Boston, MA, (now part of Springer).]]
19. Cirstea, H. and Kirchner, C. 2000. Combining higher-order and first-order computation using rho-calculus: Towards a semantics of ELAN. In Frontiers of Combining Systems 2. Studies on Logic and Computation, vol. 7, D. M. Gabbay and M. De Rijke, Eds. Research Studies Press/Wiley, Letchworth, Herts. U.K./New York, NY, 95--121.]]
20. Clavel, M., Duran, F., Eker, S., Lincoln, P., Marti-Oliet, N., Meseguer, J. and Quesada, J. F. 2002. Maude: Specification and programming in rewriting logic. Theoret. Comput. Sci. 285, 2, 187--243.]]
21. Cooley, J. W. and Tukey, J. W. 1965. An algorithm for the machine calculation of complex Fourier series. Math. Comput. 19, 4, 297--391.]]
22. Cormen, T. H., Leiserson, C. E., Rivest, R. L., and Stein, C. 2001. Introduction to Algorithms, MIT Press, Cambridge, MA.]]
23. Diaconescu, R. and Futatsugi, K. 2002. Logical foundations of CafeOBJ. Theoret. Comput. Sci. 285, 2, 289--318.]]
24. Edwards, C. 2006. Intel inside. Business Week (European Edition), Jan. (cover story).]]
25. Hartenstein, R., Hirschbiel, A. G., Riedmueller, M., Schmidt, K., and Weber, M. 1991. A high performance machine paradigm based on auto-sequencing data memory. In Proceedings of the 24th Hawaii International Conference on System Sciences (HICSS' 24, Koloa, Hawaii) (2nd Best Paper Award).]]
26. Hartenstein, R., Kress, R., and Reinig, H. 1995. A scalable, parallel and reconfigurable datapath architecture. InProceedings of the 6th Int. Symposium on IC Technology, Systems and Applications (ISIC'95, Singapore).]]
27. Hartenstein, R. 2001. Coarse grain reconfigurable architecture. In Proceedings of the Asia and South Pacific Design Automation Conference 2001 (ASP-DAC 01, Jan. 30--Feb. 2, Yokohama, Japan) (invited embedded tutorial).]]
28. Hartenstein, R. 2002. Trends in reconfigurable logic and reconfigurable computing. In Proceedings of the 9th IEEE International Conference on Electronics, Circuits and Systems (ICECS'02, Sept. 15--18, Dubrovnik, Croatia) (invited paper).]]
29. Hartenstein, R. 2004. The digital divide of computing. In Proceedings of the 2004 ACM International Conference on Computing Frontiers (CF'04, April, Ischia, Italy) (invited paper) 14--18.]]
30. Hartenstein, R. 2005. Overdue CS, CE, and ECE curriculum innovations. In Proceedings of the 1st International Workshop on Reconfigurable Computing Education (Karlsruhe, Germany, Mar. 1) (chairman's opening remarks (draft)). Available online at http://hartenstein.de/CurriculumInnovations.pdf.]]
31. Hartenstein, R. 2006a. Reconfigurable supercomputing: Hurdles and chances. In Proceedings of the 2006 International Supercomputer Conference (ICS'06 June 28--30, Dresden, Germany) (invited article).]]
32. Hartenstein, R. 2006b. (keytone panel contribution): The transdisciplinary responsibility of CS curricula. In Proceedings of the 8th World Conference on Integrated Design & Process Technology (June 25--29, San Diego, CA) (keynote panel contribution).]]
33. Herz, M., Miranda, S., Brockmeyer, M., Catthoor, F., and Hartenstein, R. 2002. Memory organization for stream-based reconfigurable computing. In Proceedings of the 9th IEEE International Conference on Electronics, Circuits and Systems (ICECS'02, Sept. 15--18, Dubrovnik, Croatia) (invited article).]]
34. Hoe, J. C. and Arvind. 1999. Hardware synthesis from term rewriting systems. In Proceedings of the 10th IFIP International Conference on VLSI---VLSI'99. Kluwer, Dordricht, The Netherlands, (now part of Springer), 595--619.]]
35. Kapur, D. 2000. Theorem proving support for hardware verification. In Proceedings of the 3rd International Workshop on First-Order Theorem Proving, (St. Andrews, Scotland) (Invited talk).]]
36. Kapur, D. and Subramaniam, M. 1997. Mechanizing verification of arithmetic circuits: SRT division. In Proceedings of the 7th Foundations of Software Technology & Theoretical Computer Science (FST&TCS). Lecture Notes in Computer Science, vol. 1346, Springer-Verlag, Berlin, Germany, 103--122.]]
37. Kapur, D. and Subramaniam, M. 2000. Using an induction prover for verifying arithmetic circuits. J. Softw. Tools Tech. Trans. 3, 1, 32--65.]]
38. Kirchner, H. and Moreau, P.-E. 2001. Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories. J. Funct. Programm. 11, 2, 207--251.]]
39. Knuth, D. E. and Bendix, P. B. 1970. Computational problems in abstract algebra. In Simple Word Problems in Universal Algebras, J. Leech, Ed. Pergamon Press, Oxford, U.K. 263--297.]]
40. Kress, R. and Hartenstein, R. 1995. A datapath synthesis system for the reconfigurable datapath architecture. In Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC'95, August/September, Chiba, Japan) (CD-ROM article No. 77).]]
41. Kung, H. T. and Leiserson, C. E. 1979. Systolic arrays for VLSI. In Sparse Matrix Proceedings 1978. Society for Industrial and Applied Mathematics, Philadalphis, PA, 256--282.]]
42. Kung, S. Y. 1987. VLSI Array Processors. Prentice-Hall, Englewood Cliffs, NJ, 1987.]]
43. Martí-Oliet, N. and Meseguer, J. eds. 2002a. Special issue on rewriting logic and its applications. Theoret. Comput. Sci. 285, 2, 119--564.]]
44. Martí-Oliet, N. and Meseguer, J. 2002b. Rewriting logic: Roadmap and bibliography. Theoret. Comput. Sci. 285 2, 121--154.]]
45. Meseguer, J. 2000. Rewriting logic and Maude: Concepts and applications. In Eleventh International Conference on Rewriting Techniques and Applications (RTA'00), L. Bachmair Ed. Lecture Notes in Computer Science, vol. 1833. Springer-Verlag, Berlin, Germany, 1--26.]]
46. Meseguer, J. 2003. Executable computational logics: Combining formal methods and programming language based system design. In Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'03). IEEE Computer Society Press, Los Alamitos, CA, 3--12.]]
47. Morra, C., Becker, J., Ayala-Rincon, M., and Hartenstein, R. 2005. FELIX: Using rewriting-logic for generating functionally equivalent implementations. In Proceedings of the 15th International Conference on Field-Programmable Logic and Applications (FPL'05). IEEE Compter Society Press, Los Alamitos, CA, 25--30.]]
48. Nageldinger, U. 2001. Coarse-grained reconfigurable architecture design space exploration. Ph.D. dissertation, Technische Universität, Kaiserslautern, Kaiserslautern, Germany.]]
49. Nageldinger, U., Hartenstein, R., Herz, M., and Hoffmann, T. 2000. Kress array explorer: A new CAD environment to optimize reconfigurable datapath array architectures. In Proceedings of the 5th Asia and South Pacific Design Automation Conference (ASPDAC'00, Yokohama, Japan). 163--168.]]
50. NN. 2004. Computing curricula 2004; Joint Task Force for Computing Curricula 2004, 22 November 2004. Available online at http://www.acm.org/education/Overview_Draft_11-22-04.pdf.]]
51. Owre, S., Rushby, J. M., Shankar, N., and Srivas, M. K. 1995. A tutorial on using PVS for hardware verification. In Theorem Provers in Circuit Design: Theory, Practice, and Experience. Lecture Notes in Computer Science, vol. 901. Springer-Verlag, Berlin, Germany, 258--279.]]
52. Paulson, L. D. 2005. News briefs: Researchers build reconfigurable supercomputer. COMPUTER 38, 8(Aug.), 27--28.]]
53. PACTCORP. 2005. http://pactcorp.com.]]
54. Shen, X. and Arvind. 1998a. Design and verification of speculative processors. Tech. rep. 400A. Laboratory for Computer Science, MIT, Cambridge, MA. Also in Proceedings of the Workshop on Formal Techniques for Hardware and Hardware-Like Systems. (June, Marstrand, Sweden).]]
55. Shen, X. and Arvind. 1998b. Modeling and verification of ISA implementations. Tech. rep. Laboratory for Computer Science, MIT, Cambridge, MA. Also in Proceedings of the Australasian Computer Architecture Conference (February, Perth, Australia).]]
56. Shen, X., Arvind, and Rudolph, L. 1999. CACHET: An adaptive cache coherence protocol for distributed shared-memory systems. In Proceedings of the ACM International Conference on Supercomputing ACM Press, New York, NY, 135--144.]]
57. Shirazi, N., Luk, W., and Cheung, P. Y. K. 2000. Framework and tools for run-time reconfigurable designs. In IEE Proceed. Comput. Digital Tech. 147, 3, 147--152.]]
58. Steiger, C., Herbert Walder, H., and Platzner, M. 2004. Operating systems for reconfigurable embedded platforms: Online scheduling of real-time tasks. IEEE Trans. Comput. 53, 11 (Nov.), 1392--1407.]]
59. Swartztrauber, P. N. 1987. Multiprocessor FFTs. Parall. Comput. 5, 197--210.]]
60. Vergara, M., Strum, M., Eberle, W., and Gyselinckx, B. 1998. A 195KFFT/s (256-points) high performance FFT/IFFT processor for OFDM applications. In Proceedings of the International Telecommunications Symposium (ITS'98). vol. 1. SBT/IEEE Computer Society Press, Los Alamitos, CA, 273--278.]]

Index Terms

• Computer systems organization

  • Architectures

    • Other architectures

• Hardware

  • Integrated circuits

    • Logic circuits

• Theory of computation

  • Formal languages and automata theory

    • Formalisms

      • Rewrite systems

    • Grammars and context-free languages