Higher-Order and Symbolic Computation

, Volume 24, Issue 1–2, pp 81–114 | Cite as

Static consistency checking for Verilog wire interconnects

Using dependent types to check the sanity of Verilog descriptions
  • Cherif Salama
  • Gregory Malecha
  • Walid Taha
  • Jim Grundy
  • John O’Leary


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 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. 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 an open-source implementation demonstrating our approach.


Verilog elaboration Static array bounds checking Verilog wire width consistency Dead code elimination Dependent types 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Dutertre, B., De Moura, L.: A fast linear-arithmetic solver for DPLL(T). Comput. Aided Verif. 4144, 81–94 (2006) CrossRefGoogle Scholar
  2. 2.
    Gillenwater, J., Malecha, G., Salama, C., Zhu, A.Y., Taha, W., Grundy, J., O’Leary, J.: Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee Verilog synthesizability. In: PEPM ’08: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, New York, NY, USA, pp. 41–50. ACM, New York (2008) CrossRefGoogle Scholar
  3. 3.
    Gomard, C.K., Jones, N.D.: A partial evaluator for the untyped lambda-calculus. J. Funct. Program. 1(1), 21–69 (1991) MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    Hackett, B., Das, M., Wang, D., Yang, Z.: Modular checking for buffer overflows in the large. In: ICSE ’06: Proceedings of the 28th International Conference on Software Engineering, New York, NY, USA, pp. 232–241. ACM, New York (2006) CrossRefGoogle Scholar
  5. 5.
    IEEE Standards Board. IEEE standard Verilog hardware description language. Number 1364-2001 in IEEE Standards. IEEE Press, New York (2001) Google Scholar
  6. 6.
    IEEE Standards Board. IEEE standard for Verilog hardware description language. Number 1364-2005 in IEEE Standards. IEEE Press, New York (2005) Google Scholar
  7. 7.
    Larochelle, D., Evans, D.: Statically detecting likely buffer overflow vulnerabilities. In: SSYM’01: Proceedings of the 10th Conference on USENIX Security Symposium, Berkeley, CA, USA. USENIX Association, Berkeley (2001). 14 pages Google Scholar
  8. 8.
    Nielson, F., Nielson, H.R.: Two-level semantics and code generation. Theor. Comput. Sci. 56(1), 59–133 (1988) MathSciNetMATHCrossRefGoogle Scholar
  9. 9.
    Pierce, B.C. (ed.): Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005) MATHGoogle Scholar
  10. 10.
    Taha, W.: Multi-stage programming: its theory and applications. PhD thesis, Oregon Graduate Institute of Science and Technology (1999) Google Scholar
  11. 11.
    Taha, W., Johann, P.: Staged notational definitions. In: Czarnecki, K., Pfenning, F., Smaragdakis, Y. (eds.) Generative Programming and Component Engineering (GPCE). Lecture Notes in Computer Science. Springer, Berlin (2003) Google Scholar
  12. 12.
    PolySpace Technologies. http://www.polyspace.com, 1999
  13. 13.
    Venet, A., Brat, G.P.: Precise and efficient static array bound checking for large embedded C programs. In: Pugh, W., Chambers, C. (eds.) PLDI, pp. 231–242. ACM, New York (2004) CrossRefGoogle Scholar
  14. 14.
    Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Montreal, June 1998, pp. 249–257 (1998) Google Scholar
  15. 15.
    Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL ’99: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA, pp. 214–227. ACM, New York (1999) CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2011

Authors and Affiliations

  • Cherif Salama
    • 1
  • Gregory Malecha
    • 1
  • Walid Taha
    • 1
  • Jim Grundy
    • 2
  • John O’Leary
    • 2
  1. 1.Rice UniversityHoustonUS
  2. 2.Intel Strategic CAD LabsHillsboroUSA

Personalised recommendations