Bit-level partial evaluation of synchronous circuits

ABSTRACT

Partial evaluation has been known for some time to be very effective when applied to software; in this paper we demonstrate that it can also be usefully applied to hardware. We present a bit-level algorithm that supports the offline partial evaluation of synchronous digital circuits. Full PE of combinational logic is noted to be equivalent to Boolean minimisation. A loop unrolling technique, supporting both partial and full unrolling, is described. Experimental results are given, showing that partial evaluation of a simple micro-processor against a ROM image is equivalent to compiling the ROM program directly into low level hardware.

REFERENCES

• 1: Excalibur Device Overview Data Sheet, V2.0. Altera, 2002. DS-EXCARM-2.0.
• 2: Quartus II Development Software Handbook, V4.0. Altera, 2004.
• 3: Arvind, Bluespec: A language for hardware design, simulation, synthesis and verification Invited Talk, Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'03), p.249, June 24-26, 2003
• 4: Per Bjesse , Koen Claessen , Mary Sheeran , Satnam Singh, Lava: hardware design in Haskell, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.174-184, September 26-29, 1998, Baltimore, Maryland, United States
• 5: Celoxica. Handel-C language reference manual. Available from http://www.celoxica.com/.
• 6: Jason Cong , Chang Wu, FPGA synthesis with retiming and pipelining for clock period minimization of sequential circuits, Proceedings of the 34th annual conference on Design automation, p.644-649, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266309]
• 7: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 8: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 9: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 10: Futamura, Y. Partial evaluation of computation process -- an approach to a compiler-compiler. In Systems, Computers, Control (1971), vol. 2 issue 5, pp. 45--50.
• 11: Charles Hymans, Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation, Proceedings of the 9th International Symposium on Static Analysis, p.444-460, September 17-20, 2002
• 12: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 13: Lombardi, L. Incremental computation. In Advances in Computers, vol. 8, F. Alt and M. Rubinoff, Eds. New York: Academic Press, 1967, pp. 247--333.
• 14: Lombardi, L., and Raphael, B. Lisp as the language for an incremental computer. In The Programming Language Lisp: Its Operation and Applications (1964), E. Berkeley and D. Bobrow, Eds., Cambridge, MA: MIT Press, pp. 204--219.
• 15: N. McKay , T. Melham , K. W. Susanto , S. Singh, Dynamic Specialization of XC6200 FPGAs by Partial Evaluation, Proceedings of the IEEE Symposium on FPGAs for Custom Computing Machines, p.308, April 15-17, 1998
• 16: Nicholas McKay , Satnam Singh, Dynamic Specialisation of XC6200 FPGAs by Parial Evaluation, Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications, From FPGAs to Computing Paradigm, p.298-307, August 31-September 03, 1998
• 17: Mealy, G. H. A method for synthesizing sequential circuits. In Bell System Technical Journal (1955), vol. 34, pp. 1045--1079.
• 18: Mycroft, A., and Jones, N. D. A relational framework for abstract interpretation. In Lecture Notes in Computer Science: Proc. Copenhagen workshop on programs as data objects (1984), vol. 215, Springer-Verlag.
• 19: Alan Mycroft , Richard Sharp, Hardware Synthesis Using SAFL and Application to Processor Design, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.13-39, September 04-07, 2001
• 20: Page, I., and Luk, W. Compiling Occam into FPGAs. In FPGAs, W. Moore and W. Luk, Eds. Abingdon EE&CS Books, 1991, pp. 271--283.
• 21: Bjarne Stroustrup, The C++ programming language (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1991
• 22: Thompson, S. Hardware web site. http://harpe.findatlantis.com/.
• 23: Thompson, S. Hardware compilation as an alternative computation architecture. Master's thesis, University of Teesside, 1991.
• 24: Thompson, S., and Mycroft, A. Abstract interpretation of combinational asynchronous circuits. In 11th International Static Analysis Symposium (SAS'04) (2004), R. Giacobazzi, Ed., vol. 3148 of Lecture Notes in Computer Science, Springer-Verlag, pp. 181--196.
• 25: Thompson, S., and Mycroft, A. Sliding window logic simulation. In 15th UK Asynchronous Forum (2004), Cambridge. Available from http://findatlantis.com/.
• 26: Thompson, S., Mycroft, A., Brat, G., and Venet, A. Automatic in-flight repair of FPGA cosmic ray damage. In Proc. 1st Disruption in Space Symposium (July 2005).
• 27: Veldhuizen, T. Using C++ template metaprograms. C++ Report 7, 4 (May 1995), 36--43. Reprinted in C++ Gems, ed. Stanley Lippman.
• 28: Veldhuizen, T. L. C++ templates as partial evaluation. In Proceedings of PEPM'99. The ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, ed. O. Danvy, San Antonio (Jan. 1999), University of Aarhus, Dept. of Computer Science, pp. 13--18.

INDEX TERMS

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

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Sequential circuits
  B.8 Performance and Reliability
      B.8.1 Reliability, Testing, and Fault-Tolerance

General Terms:
Design, Verification

Keywords:
loop unrolling, partial evaluation, synchronous circuits