[Next] [Up] [Previous] [Contents]

The SMV language

K. L. McMillan

• Contents
• SMV language overview
  • Data types and type declarations
    • Boolean, enumerated and subrange types
    • Arrays
    • Multidimensional arrays
    • Generic arrays
    • Binary numbers
    • Structs
  • Signals and assignments
    • Operations on signals
    • Assignments
    • Unit delay assignments - the ``next'' operator
    • State machines
  • Rules for assignments
    • The single assignment rule
    • The circular dependency rule
    • Range violations and unknown values
  • Nondeterministic assignments
    • Order of assignments and declarations
  • Modules
    • Module declarations
    • Instantiations
    • Input and output declarations
    • Instance hierarchies
    • Structured data types
    • Defined types
  • Conditionals
    • Simple conditionals
    • Defaults
    • Complex conditionals - switch and case
  • Constructor loops
    • Basic for-loops
    • Creating arrays of instances
    • Creating parameterized modules
    • Chained constructor loops
  • Expressions
    • Parentheses and precedence
    • Integer constants
    • Symbolic constants
    • Boolean operators
    • Conditional operators (``if'', ``case'' and ``switch'')
    • Representing state machines using conditionals
    • Arithmetic operators
    • Comparison operators
    • Set expressions
      • The set inclusion operator
      • Extension of operators to sets
      • Comprehension expressions
  • Vectors and vector operators
    • The concatenation operator
    • Extension of operators to vectors
    • Vector coersion operator
    • Arithmetic on vectors
    • Comparison operators on vectors
    • Vector sets
    • Coercion of scalars to vectors
    • Explicit coercion operators
    • Coercion of array variables to vectors
    • Binary subranges
    • Vector assignments
    • Assignments to arrays
    • Vectors as inputs and outputs
    • Iteratively constructing vectors
    • Reduction operators
  • Assertions
    • Temporal formulas
    • The assert declaration
    • Using...Prove declarations
  • Refinements
    • The refinement relation
      • Circular assignments
    • Compositional verification
    • The using...prove declaration
    • Abstract signals
• Language definition
  • Syntax
    • Lexical tokens
    • Identifiers
    • Expressions
    • Types
    • Statements
    • Module definitions
    • Programs
• About this document ...