Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions

From CERES
Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

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.