As predicted by Gordon Moore, the number of transistors on a chip has roughly
doubled every two years. 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 very large scale integration (VLSI)
design, industrial hardware description languages (HDLs) like Verilog and VHDL
must be significantly enhanced. This thesis pinpoints some of the main shortcomings
of the latest Verilog standard (IEEE 1364-2005) and shows 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.
Addressing both problems while remaining backward compatible led us to select a
statically typed two-level languages (STTL) formal framework. By formalizing a core
subset of Verilog as an STTL, we were able to define a static 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. The power of the chosen framework is once
more demonstrated as it also allows us to enrich the language with a new set of
constructs that are designed to be expanded away when instantiated.
To experiment with these ideas we implemented VPP, a Verilog Preprocessor
with a built-in type checker. VPP is an unobtrusive tool accepting extended Verilog
descriptions but generating descriptions compatible with any tool compliant with the
Verilog standard.
Our experience throughout this research showed that STTLs present a particularly
suitable framework to formalize and implement generative features of a language. / Rice University,
National Science Foundation (NSF) SoD award 0439017, Intel Corporation,
Semiconductor Research Corporation (SRC) Task ID 1403.001
| Identifer | oai:union.ndltd.org:RICE/oai:scholarship.rice.edu:1911/64203 |
| Date | 05 1900 |
| Creators | Salama, Cherif |
| Contributors | Walid Taha |
| Source Sets | Rice University |
| Language | en_US |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.0017 seconds