The current NUSMV input language [19] is essentially the same as the CMU SMV input language [47,26]. The NUSMV input language is designed to allow for the description of finite state systems. The only data types provided by the language are booleans, bounded integer subranges, and symbolic enumerated types. Moreover, NUSMV allows for the definitions of bounded arrays of basic data types.

The description of a complex system can be decomposed into modules, and each of them can be instantiated many times. This provides the user with a modular and hierarchical description, and supports the definition of reusable components. Each module defines a finite state machine. Modules can be composed either synchronously or asynchronously using interleaving. In synchronous composition a single step in the composition corresponds to a single step in each of the components. In asynchronous composition with interleaving a single step of the composition corresponds to a single step performed by exactly one component. The NUSMV input language allows to describe deterministic and non deterministic systems.

A NUSMV program can describe both the model and the specification. Figure 4 gives a small example of a NUSMV program. The example in Figure 4 is a model of a 3 bit binary counter circuit. It illustrates the definition of reusable modules and expressions.

The module `counter_cell` is instantiated three times, with names
`bit0`, `bit1` and `bit2`. The module
`counter_cell` has a formal parameter `carry_in`. In the
instantiation of the module, actual signals (`1` for the instance
`bit0`, `bit0.carry_out` for the instance `bit1` and
`bit1.carry_out` for the instance `bit2`) are plugged in for
the formal parameters, thus linking the module instance to the program (a
module can be seen as a subroutine). The property that we want to check is
``invariantly eventually the counter count till 8'' which is expressed in
CTL using the design state variables as ```AG AF bit2.carry_out`''.

It is also possible to specify the transition relation and the set of initial
states of a module by means of propositional formulas, using the keywords
`TRANS`, and `INIT` respectively. This provides the user with a lot of freedom
in designing systems. In Figure 5 there is an equivalent
definition of module `counter_cell` using propositional formulas.

With respect to CMU SMV, the input language of NUSMV has been extended to allow for the specification of properties expressed in LTL and the specifications of invariants [19].

NuSMV <>