The Semantics of Verilog Using Transition System Combinators

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

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Gordon J. Pace
• Keywords: FMCAD 2000, Formal Methods, Model Checking, Semantics, Transition System