The spec sublanguage is used to specify properties or requirements for the circuit. A standard spec directive has the following syntax:

spec {
    directive_name (sig1, sig2, ...)
    directive_name (sig1, sig2, ...)
    ...
}

There are four exclusive directives, two for exclusive high and two for exclusive low. The directive

 spec {
   exclhi (a,b)
 }

states that the signals a and b will not be true (high) simultaneously, and this is guaranteed by the production rules in the circuit.

To simplify modeling of arbiters that cannot be modeled purely at the digital level of abstraction, we include a specific directive that we call “make exclusive high”.

spec {
  mk_exclhi(a,b)
 }

This forces the signals a and b to be exclusive high in the digital simulation model.

There are symmetric variations (excllo and mk_excllo) for exclusive low constraints.