[Next]
[Up]
[Previous]
Next:
SMV language overview
Up:
The SMV language
Previous:
The SMV language
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 ...
Ken McMillan
Sat Jun 6 21:41:59 PDT 1998