As predicted by Gordon Moore, the number of transistors on a chip has been doubling every two years approximately. Microprocessors featuring over a billion transistors are no longer science fiction. For example, Intel's Itanium 9000 series and Intel's Xeon 7400 series of processors feature 1.7 and 1.9 billion transistors respectively. To keep up with the emerging needs of contemporary VLSI design, industrial hardware description languages (HDLs) like Verilog and VHDL must be significantly enhanced. We pinpoint some of the main shortcomings of the latest Verilog standard and show how to overcome them by extending the language in a backward compatible way.
To be able to cope with more complex circuits, well-understood higher-level abstraction mechanisms are needed. Verilog is already equipped with promising generative constructs making it possible to concisely describe a family of circuits as a parameterized module; however these constructs suffer from two problems: First, their expressivity is limited and second, they are not adequately supported by current tools. For instance, there are no static guarantees about the properties of the description generated as a result of instantiating a generic description with particular parameter values.
By formalizing a core subset of Verilog as a statically typed two-level language (STTL), we are able to address both problems while remaining backward compatible. In particular, we define a type system capable of: 1) checking the realizability of a description, 2) detecting bus width mismatches and array bounds violations, and 3) providing parametric guarantees on the resources required to realize a generic description. STTLs also allow us to extend the language with a new set of statically checked generative constructs designed to be expanded away when instantiated.