Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability
Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability
复制标题
可综合的高级硬件描述：使用静态类型的两级语言来保证verilog可综合性
DOI：
10.1145/1328408.1328416
复制
发表时间：
2008
影响因子：
7.4
通讯作者：
J. O'Leary
中科院分区：
文献类型：
--
作者：
Jennifer Gillenwater;G. Malecha;Cherif R. Salama;A. Zhu;Walid M. Taha;J. Grundy;J. O'Leary
现代硬件描述语言支持代码生成结构，如Verilog中的generate/endgenerate。这些构造旨在描述常规或参数化的硬件设计，并且当有效使用时，可以使硬件描述更短，更易于理解和更可重用。然而，在实践中，设计人员避免使用这些构造，因为很难理解和预测生成代码的属性。生成的代码是类型安全的吗？它是可合成的吗？它需要什么物理资源（例如组合门和触发器）？如果不首先生成完全扩展的代码，通常不可能回答这些问题。在Verilog和VHDL社区中，这个生成过程被称为细化。
本文提出了一种规范的方法，在Verilog的阐述。通过将Verilog看作一种静态类型的两级语言，我们能够反映出在详细描述时已知的值和作为电路计算一部分的值之间的区别。这种区别对于确定诸如迭代和模块参数之类的抽象是否以可综合的方式使用至关重要。为了说明这个想法，我们开发了一个Verilog的核心演算，我们称之为Featherweight Verilog（FV）和相关的静态类型系统。我们正式定义了一个类似于Verilog的细化阶段的预处理步骤，以及在此阶段可能发生的错误类型。最后，我们表明，一个良好的类型的设计不会导致预处理错误，其扩展的结果总是一个可合成的电路。
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.