Logic in Computer Science (LICS 1995)

Invited Talk: The Semantic Challenge of Verilog HDL (at LICS 1995)

Authors: Mike Gordon

Abstract

The Verilog hardware description language (HDL) is widely used to model the structure and behavior of digital systems ranging from simple hardware building blocks to complete systems. Its semantics is based on the scheduling of events and the propagation of changes. Different Verilog models of the same device are used during the design process and it is important that these be `equivalent'; formal methods for ensuring this could be commercially significant. Unfortunately, there is very little theory available to help. This self-contained tutorial paper explains the semantics of Verilog informally and poses a number of logical and semantic problems that are intended to provoke further research. Any theory developed to support Verilog is likely to be useful for the analysis of the similar (but more complex) language VHDL.

BibTeX

  @InProceedings{Gordon-TheSemanticChalleng,
    author = 	 {Mike Gordon},
    title = 	 {The Semantic Challenge of Verilog HDL},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {136-145},
    location =   {San Diego, CA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }