The SMV System

Abstract

In order to apply symbolic model checking to real problems, we need expressive languages that we can use to describe our model at a suitably high level (eg., a gate level schematic is probably not a high enough level). For our purposes, this means the language must provide operations on suitable high level types (such as symbolic enumerated types), and must allow us to conveniently describe non-deterministic choices, so that we can describe high level protocols without being concerned with implementation details. The language must have a precise mathematical semantics that defines the translation from a program in the langauge to a form suitable for symbolic model checking (ie., a Boolean formula representing the transition relation). For reasons that will be clarified in chapter 7, the semantics should be syntax-directed (defining the meaning of a language construct in terms of the meanings of its syntactic parts), so that we may infer properties of a program from properties of its parts. Ideally, it should also be possible to translate at least a useful subset of the language (not including, for example, non-deterministic choice) into hardware descriptions suitable for synthesis into real hardware. Constructs should be provided to allow us to use most common styles of system design.