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

Module declarations

As an example, suppose we want to construct a binary counter, by designing a counter ``bit'', and then chaining the bits together to form a counter. In SMV, the counter bit might be declared as follows:

MODULE counter_bit(carry_in, clear, bit_out, carry_out)
{
  INPUT carry_in, clear : boolean;
  OUTPUT bit_out, carry_out : boolean;

  next(bit_out) := clear ? 0 : (carry_in ^ bit_out);

  carry_out := carry_in & bit_out;
}

The ``INPUT'' and ``OUTPUT'' declarations are specialized forms of type declarations, which also give the direction of signals being declared. These declarations must occur before any ordinary type declarations or assignments.