hh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Static Consistency Checking for Verilog Wire Interconnects: Using dependent types to check the sanity of Verilog descriptions
Rice University, Houston, TX, USA.
Rice University, Houston, TX, USA.
Rice University, Houston, TX, USA.
Intel Strategic CAD Labs, Hillsboro, OR, USA.
Visa övriga samt affilieringar
2011 (Engelska)Ingår i: Higher-Order and Symbolic Computation, ISSN 1388-3690, E-ISSN 2212-0793, Vol. 24, nr 1-2, s. 81-114Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

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 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 exceed 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 situation 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 dependent types and constraint generation to reduce the problem of detecting the aforementioned inconsistencies to a satisfiability problem. Once reduced, the problem can easily be solved with a standard 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 illustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with generative 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. © 2011 Springer Science+Business Media, LLC.

Ort, förlag, år, upplaga, sidor
New York, NY: Springer-Verlag New York, 2011. Vol. 24, nr 1-2, s. 81-114
Nyckelord [en]
Verilog elaboration, Static array bounds checking, Verilog wire width consistency, Dead code elimination, Dependent types
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:hh:diva-25010DOI: 10.1007/s10990-011-9072-1Scopus ID: 2-s2.0-84861683753Libris ID: 12440293OAI: oai:DiVA.org:hh-25010DiVA, id: diva2:711469
Konferens
PEPM '09 – Partial Evaluation and Program Manipulation (co-located with POPL 2009), Savannah, GA, USA, January 19-20, 2009
Anmärkning

An earlier version was presented at PEPM’09. This manuscript includes an extended set of examples, performance evaluation, complete proofs, and various improvements. This work was supported by the National Science Foundation (NSF) SoD award 0439017, and the Semiconductor Research Consortium (SRC) Task ID: 1403.001 (Intel custom project).

Tillgänglig från: 2014-04-10 Skapad: 2014-04-10 Senast uppdaterad: 2018-03-22Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Taha, Walid

Sök vidare i DiVA

Av författaren/redaktören
Taha, Walid
I samma tidskrift
Higher-Order and Symbolic Computation
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 94 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf