Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions

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 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.

REFERENCES

• 1: B. Dutertre and L. de Moura. The Yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf, August 2006.
• 2: Jennifer Gillenwater , Gregory Malecha , Cherif Salama , Angela Yun Zhu , Walid Taha , Jim Grundy , John O'Leary, Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA [doi>10.1145/1328408.1328416]
• 3: Carsten K. Gomard and Neil D. Jones. A partial evaluator for the untyped lambda-calculus. Journal of Functional Programming, 1(1):21--69, 1991.
• 4: Brian Hackett , Manuvir Das , Daniel Wang , Zhe Yang, Modular checking for buffer overflows in the large, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134319]
• 5: IEEE Standards Board. IEEE Standard Verilog Hardware Description Language. Number 1364-2001 in IEEE Standards. IEEE, 2001.
• 6: IEEE Standards Board. IEEE Standard for Verilog Hardware Description Language. Number 1364-2005 in IEEE Standards. IEEE, 2005.
• 7: David Larochelle , David Evans, Statically detecting likely buffer overflow vulnerabilities, Proceedings of the 10th conference on USENIX Security Symposium, p.14-14, August 13-17, 2001, Washington, D.C.
• 8: Flemming Nielson , Hanne Riis Nielson, Two-level semantics and code generation, Theoretical Computer Science, v.56 n.1, p.59-133, Jan. 1988 [doi>10.1016/0304-3975(86)90006-X]
• 9: Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000, USA. Available online from: ftp://cse.ogi.edu/pub/tech-reports/README.html.
• 10: Cherif Salama, Gregory Malecha, Walid Taha, Jim Grundy, and John O'Leary. Static consistency checking for Verilog wire interconnects. Technical report, Rice University and Intel Strategic CAD Labs, http://www.resource-aware.org/twiki/pub/RAP/VPP/FVTR2.pdf, 2008.
• 11: Walid Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, Oregon Graduate Institute of Science and Technology, 1999
• 12: Walid Taha , Patricia Johann, Staged notational definitions, Proceedings of the 2nd international conference on Generative programming and component engineering, p.97-116, September 22-25, 2003, Erfurt, Germany
• 13: PolySpace Technologies. http://www.polyspace.com.
• 14: Arnaud Venet , Guillaume Brat, Precise and efficient static array bound checking for large embedded C programs, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 15: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Preprocessors

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

General Terms:
Languages, Standardization, Theory, Verification

Keywords:
dead code elimination, dependent types, static array bounds checking, verilog elaboration, verilog wire width consistency