Difference between revisions of "Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions"
From CERES
(Created page with "<div style='display: none'> == Do not edit this section == </div> {{PublicationSetupTemplate|Author=Cherif Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O’Leary |PID...") |
(No difference)
|
Latest revision as of 04:44, 26 June 2014
| 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 Jim Grundy and John O’Leary |
| Year | 2011 |
| PublicationType | Conference Paper |
| Journal | |
| HostPublication | |
| DOI | http://dx.doi.org/10.1007/s10990-011-9072-1 |
| 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:588241 |
| Abstract | The Verilog hardware description language has padding semantics that allow designers to write descriptions where wires of different bit widths can be interconnected. However, many such connections are nothing more than bugs inadvertentlyintroduced by the designer and often result in circuits that behave incorrectly or usemore resources than required. A similar problem occurs when wires are incorrectlyindexed by values (or ranges) that exceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the useof generate blocks to describe circuit families only makes the situation worse as ithides such inconsistencies. 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 pinned down prior to elaboration using static analysis. We combine dependent types and constraint generationto reduce the problem of detecting the aforementioned inconsistencies to a satisfiabilityproblem. Once reduced, the problem can easily be solved with a standard satisfiabilitymodulo 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 illustrate these ideas, we develop a type system for Featherweight Verilog (FV), acore calculus of structural Verilog with generative constructs and previously definedelaboration semantics. We prove that a well-typed FV description will always elaborateinto an inconsistency-free description. We also provide an open-source implementationdemonstrating our approach. |
