Publications:Static Consistency Checking for Verilog Wire Interconnects : Using dependent types to check the sanity of verilog descriptions
From CERES
| Title | Static Consistency Checking for Verilog Wire Interconnects : Using dependent types to check the sanity of verilog descriptions |
|---|---|
| Author | Cherif Salama and Gregory Malecha and Walid Taha and John O'Leary and Jim Grundy |
| Year | 2009 |
| PublicationType | Conference Paper |
| Journal | |
| HostPublication | PEPM '09 : Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation |
| DOI | http://dx.doi.org/10.1145/1480945.1480963 |
| Conference | PEPM '09 Partial Evaluation and Program Manipulation (co-located with POPL 2009) Savannah, GA, USA. January 19 - 20, 2009 |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:396152 |
| Abstract | The Verilog hardware description language has padding semanticsthat allow designers to write descriptions where wires of differentbit widths can be interconnected. However, many of theseconnections are nothing more than bugs inadvertently introducedby the designer and often result in circuits that behave incorrectlyor use more resources than required. A similar problem occurswhen wires are incorrectly indexed by values (or ranges) that exceedtheir bounds. These two problems are exacerbated by generateblocks. While desirable for reusability and conciseness, the use ofgenerate blocks to describe circuit families only makes the situationworse as it hides such inconsistencies making them harder todetect. Inconsistencies in the generated code are only exposed afterelaboration when the code is fully-expanded.In this paper we show that these inconsistencies can be pinneddown prior to elaboration using static analysis.We combine dependenttypes and constraint generation to reduce the problem of detectingthe aforementioned inconsistencies to a satisfiability problem.Once reduced, the problem can easily be solved with a standardsatisfiability modulo theories (SMT) solver. In addition, thistechnique allows us to detect unreachable code when it residesin a block guarded by an unsatisfiable set of constraints. To illustratethese ideas, we develop a type system for FeatherweightVerilog (FV), a core calculus of structural Verilog with generativeconstructs and previously defined elaboration semantics. Weprove that a well-typed FV description will always elaborate into aninconsistency-free description. We also provide a freely-availableimplementation demonstrating our approach. |
