Name
Title | ||
|---|---|---|
Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions |
Abstract | ||
|---|---|---|
The Verilog hardware description language has padding seman- tics that allow designers to write descriptions where wires of dif- ferent bit widths can be interconnected. However, many of these connections are nothing more than bugs inadvertently introduced by the designer and often result in circuits that behave incorrectly or use more resources than required. A similar problem occurs when wires are incorrectly indexed by values (or ranges) that ex- ceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the use of generate blocks to describe circuit families only makes the situ- ation worse as it hides such inconsistencies making them harder to detect. Inconsistencies in the generated code are only exposed after elaboration when the code is fully-expanded. In this paper we show that these inconsistencies can be pinned down prior to elaboration using static analysis. We combine depen- dent types and constraint generation to reduce the problem of de- tecting the aforementioned inconsistencies to a satisfiability prob- lem. Once reduced, the problem can easily be solved with a stan- dard satisfiability modulo theories (SMT) solver. In addition, this technique allows us to detect unreachable code when it resides in a block guarded by an unsatisfiable set of constraints. To il- lustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with genera- tive constructs and previously defined elaboration semantics. We prove that a well-typed FV description will always elaborate into an inconsistency-free description. We also provide a freely-available implementation demonstrating our approach. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/1480945.1480963 | Higher-Order and Symbolic Computation |
Keywords | DocType | Volume |
dependent types,indexation,satisfiability,static analysis,type system,satisfiability modulo theories,dead code elimination,computer and information science,hardware description language | Journal | 24 |
Issue | Citations | PageRank |
1-2 | 2 | 0.40 |
References | Authors | |
7 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cherif Salama | 1 | 35 | 5.25 |
| Gregory Malecha | 2 | 92 | 7.93 |
| Walid Taha | 3 | 1020 | 70.41 |
| Jim Grundy | 4 | 179 | 18.11 |
| John O'Leary | 5 | 14 | 2.11 |