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.
