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.

The directive rand_init is used to let the simulator know that a signal might be undefined on power-up, but will initialize to either 0 or 1 at random. The directive hazard is used to let the simulator know that a particular signal can have a switching hazard.

Timing constraints in ACT are specified using timing forks. Timing forks are used to specify a point of divergence constraint. The constraint

spec {
  timing a+ : b- < c+
}

states that after a makes a zero-to-one transition, b makes a one-to-zero transition before c makes a zero-to-one transition. a+ is the root of the timing fork, b- is the fast leg of the fork, and c+ is the slow leg of the fork.

spec {
  timing a+ : b- < [15] c+
}

This specifies that the timing fork has a margin of 15 delay units. The conversion from delay units to actual time uses the prs2net.conf configuration parameter net.delay.

Asynchronous circuits oscillate, and each oscillation can be viewed as an iteration of the circuit. For timing analysis, it is important to indicate connections from one iteration to the next—i.e. when a signal transition from the current indication leads to a transition from the next iteration. Such directives can be computed during logic synthesis, and ACT expects all logic synthesis tools to emit these directives along with the gate-level implementation.

spec {
   timing a+ -> c-
 }

This directive says that a+ on a particular iteration directly leads to c- in the next iteration. (Sometimes these are called ticked edges in the timing graph.¹⁾²⁾

Finally, timing forks may relate transitions from adjacent iterations.

spec {
  timing a+ : b*- < c+
}

The * indicates that the b- transition is from the following iteration. The * indicator can appear on any signal except the root of the timing fork (in this case a+).