Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability

ABSTRACT

Modern hardware description languages support code-generation constructs like generate/endgenerate in Verilog. These constructs are intended to describe regular or parameterized hardware designs and, when used effectively, can make hardware descriptions shorter, more understandable, and more reusable. In practice, however, designers avoid these constructs because it is difficult to understand and predict the properties of the generated code. Is the generated code even type safe? Is it synthesizable? What physical resources (e.g. combinatorial gates and flip-flops) does it require? It is often impossible to answer these questions without first generating the fully-expanded code. In the Verilog and VHDL communities, this generation process is referred to as elaboration.

This paper proposes a disciplined approach to elaboration in Verilog. By viewing Verilog as a statically typed two-level language, we are able to reflect the distinction between values that are known at elaboration time and values that are part of the circuit computation. This distinction is crucial for determining whether abstractions such as iteration and module parameters are used in a synthesizable manner. To illustrate this idea, we develop a core calculus for Verilog that we call Featherweight Verilog (FV) and an associated static type system. We formally define a preprocessing step analogous to the elaboration phase of Verilog, and the kinds of errors that can occur during this phase. Finally, we show that a well-typed design cannot cause preprocessing errors, and that the result of its expansion is always a synthesizable circuit.

REFERENCES

• 1: Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984.
• 2: Bluespec, Inc. Bluespec SystemVerilog Version 3.8 Reference Guide, 2006.
• 3: Jennifer Gillenwater, Gregory Malecha, Cherif Salama, Angela Yun Zhu, Walid Taha, Jim Grundy, and John O'Leary. Synthesizable High Level Hardware Descriptions. Technical report, Rice University and Intel Strategic CAD Labs, http://www.resourceaware.org/twiki/pub/RAP/VPP/FV-TR.pdf, 2007.
• 4: Carsten K. Gomard and Neil D. Jones. A partial evaluator for the untyped lambda-calculus. Journal of Functional Programming, 1(1):21--69, 1991.
• 5: IEEE Standards Board. IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. Number 1364--1995 in IEEE Standards. IEEE, 1995.
• 6: IEEE Standards Board. IEEE Standard Verilog Hardware Description Language. Number 1364--2001 in IEEE Standards. IEEE, 2001.
• 7: IEEE Standards Board. IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language. Number 1800--2005 in IEEE Standards. IEEE, 2005.
• 8: IEEE Standards Board. IEEE Standard for Verilog Hardware Description Language. Number 1364--2005 in IEEE Standards. IEEE, 2005.
• 9: IEEE Standards Board. IEEE Standard for Verilog Register Transfer Level Synthesis. Number 1364.1--2002 (IEC 62142:2005) in IEEE Standards. IEEE, 2005.
• 10: Oleg Kiselyov , Kedar N. Swadi , Walid Taha, A methodology for generating verified combinatorial circuits, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy [doi>10.1145/1017753.1017794]
• 11: Eugene Kohlbecker , Daniel P. Friedman , Matthias Felleisen , Bruce Duba, Hygienic macro expansion, Proceedings of the 1986 ACM conference on LISP and functional programming, p.151-161, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319859]
• 12: Sun Microsystems. Opensparc t1 processor file: mul64.v. http://opensparc-t1.sunsource.net/nonav/source/verilog/html/mul64.v.
• 13: Flemming Nielson , Hanne Riis Nielson, Two-level semantics and code generation, Theoretical Computer Science, v.56 n.1, p.59-133, Jan. 1988 [doi>10.1016/0304-3975(86)90006-X]
• 14: Opencores.org. Or1200's 32x32 multiply for asic. http://www.opencores.org/cvsweb.shtml/or1k/or1200/rtl/verilog/or1200 amultp2 32x32.v.
• 15: Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291--1000, USA. Available online from: ftp://cse.ogi.edu/pub/tech-reports/README.html.
• 16: Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. available from {15}.
• 17: Walid Taha, Stephan Ellner, and Hongwei Xi. Generating imperative, heap--bounded programs in a functional setting. In Proceedings of the Third International Conference on Embedded Software, Philadelphia, PA, 2003.
• 18: Walid Taha and Patricia Johann. Staged notational definitions. In Krzysztof Czarnecki, Frank Pfenning, and Yannis Smaragdakis, editors, Generative Programming and Component Engineering (GPCE), Lecture Notes in Computer Science. Springer-Verlag, 2003.
• 19: Terese. Term Rewriting Systems. Cambridge University Press, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Preprocessors

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

General Terms:
Languages, Standardization, Theory, Verification

Keywords:
code generation, hardware description languages, statically typed two-level languages, synthesizability, verilog elaboration