| Abstract
|
<p>The Verilog hardware description … <p>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.</p>ationdemonstrating our approach.</p>
|
| Author
|
Cherif Salama +
, Gregory Malecha +
, Walid Taha +
, Jim Grundy +
, John O’Leary +
|
| Conference
|
PEPM '09 Partial Evaluation and Program Manipulation (co-located with POPL 2009) Savannah, GA, USA, January 19-20, 2009
|
| DOI
|
http://dx.doi.org/10.1007/s10990-011-9072-1 +
|
| Diva
|
http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588241
|
| EndPage
|
114 +
|
| PublicationType
|
Conference Paper +
|
| Publisher
|
Springer-Verlag New York +
|
| Series
|
Higher-Order and Symbolic Computation ; 24:1-2 +
|
| StartPage
|
81 +
|
| Title
|
Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
|
| Year
|
2011 +
|
| Has queryThis property is a special property in this wiki.
|
Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
, Publications:Static Consistency Checking for Verilog Wire Interconnects : Using Dependent Types to Check the Sanity of Verilog Descriptions +
|
| Categories |
Publication +
|
| Modification dateThis property is a special property in this wiki.
|
26 June 2014 03:44:58 +
|
