The Semantics of Verilog Using Transition System Combinators

Gordon J. Pace

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Since the advent of model checking it is becoming more common for languages to be given a semantics in terms of transition systems. Such semantics allow to model check properties of programs but are usually difficult to formally reason about, and thus do not provide a sufficiently abstract description of the semantics of a language. We present a set of transition system combinators that allow abstract and compositional means of expressing language semantics. These combinators are then used to express the semantics of a subset of the Verilog hardware description language. This approach allows reasoning about the language using both model checking and standard theorem proving techniques.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:37
Start Conference Manager
Conference Systems