Contents

• SMV language overview
• Data types and type declarations
  • Boolean, enumerated and subrange types
  • Arrays
  • Multidimensional arrays
  • Generic arrays
  • Structure
  
  
• 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
  • Order of assignments and declarations
  
  
• Nondeterministic assignments
  • Assignments to arrays of signals
  
  
• 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
  
  
• Vectors and vector operators
  • The concatenation operator
  • Extension of operators to vectors
  • Vector coercion operator
  • Arithmetic on vectors
  • Comparison operators on vectors
  • Vector sets
  • Coercion of scalars to vectors
  • Explicit coercion operators
  • Coercion of array variables to vectors
  • Generic arrays and vector coercion
  • Array subranges
  • Assignments to vectors
  • Assignments to arrays
  • Vectors as inputs and outputs
  • Iteratively constructing vectors
  • Reduction operators
  • Vectors as conditions
  • Coercion of structures to vectors
  • Resolving ambiguities between array and structure references
  
  
• Assertions
  • Temporal formulas
  • The assert declaration
  • Using...Prove declarations
  
  
• Refinements
  • The refinement relation
  • Compositional verification
  • The using...prove declaration
  • Abstract signals
  
  
• Syntax
  • Lexical tokens
  • Identifiers
  • Expressions
  • Types
  • Statements
  • Module definitions
  • Programs
  
  
• About this document ...