It is common to use handshakes for the communication between modules in asynchronous systems. This tutorial discusses the common pitfalls in using handshakes, and explains how to use the Handshake Wizard in Workcraft to formally verify handshakes. It focuses on control handshakes, and so does not deal with the data validity.

On the surface, the handshake protocol seems rather trivial – why would one want to verify it? Besides the generic remark that everything that can be verified must be verified, it turns out that the handshake protocol does have a number of pitfalls. As an example, consider a Decoupler: It communicates with two modules, Left and Right, by the handshakes rl / al and rr / ar, respectively. The idea is that Left can quickly complete its handshake with Decoupler and continue its execution, while Decoupler takes care of completing the (potentially slow) handshake with Right.

Consider the following simple STG describing the Decoupler component buggy-decoupler.stg.work (3 KiB). Setting aside the issues of data validity (let's assume it is a purely control handshake) and efficiency (one can remove the negative signal edges from the critical path), can you spot the problem in this specification?

The problem here is that Left can attempt to send another request before Decoupler completes its handshake with Right – indeed, Left has no way of knowing whether that handshake is completed. However, the specification does not capture this possibility, and assumes that Left will wait for the handshake between Decoupler and Right to complete. In other words, the assumptions about the environment's behaviour are incorrect: To fix this, one must enable rl+ immediately after al-, e.g. as follows decoupler.stg.work (3 KiB):

The above bug can be caught if one verifies the N-way conformation property of the overall system (Left can send an unexpected input to Decoupler, so the N-way conformation is violated), but it would be much better to catch such bugs at the level of a module – this would make the verification much simpler, and also will help with debugging (a violation trace for the N-way conformation will likely include activity in other modules, which is largely irrelevant but can make the trace very long).

Below we discuss potential complications with handshakes, including the described receptiveness pitfall.

It is possible (in fact, common) that more than two signals participate in a handshake. For example, there can be a dual-rail (or, in general, multiple-rail 1-hot) request (e.g. to specify the mode of operation) with a single-rail acknowledgement. Alternatively, the acknowledgement can be dual-rail (or, in general, multiple-rail 1-hot) to return some information to the caller. E.g. the VME bus controller has a handshake {dsr, dsw} / dtack with a dual-rail request (to specify the mode of operation – read or write) and a single-rail acknowledgement.

In general, let REQ and ACK be two non-empty sets of signals. We assume that the signals in each set have the same type (either input or output), and the type of requests is opposite to the type of acknowledgements. The handshake is called active if REQ contains outputs (i.e. the module initiates the handshake) and passive if REQ contains inputs (i.e. another module initiates the handshake). Moreover, at most one request is allowed to be asserted at any time, and similarly for acknowledgements; in other words, the signals in sets REQ and ACK are mutually exclusive (i.e. 1-hot).

For a handshake r / a (it does not matter if it is passive or active), suppose the initial values of r and a are 0. The handshake protocol requires that these signals follow the order r+ a+ r- a-. That is, there are four different states in a handshake, uniquely determined by the values of signals r and a, with the following requirements:

• r=0 & a=0:   r-, a+, a- must be disabled;
• r=1 & a=0:   r+, r-, a- must be disabled;
• r=1 & a=1:   r+, a+, a- must be disabled;
• r=0 & a=1:   r+, r-, a+ must be disabled.

These conditions can be generalised to handshakes comprising multiple requests and/or acknowledgements in a natural way, as we assume that at most one request and at most one acknowledgement can be asserted at any time.

Note that these properties only require certain signal edges to be disabled. The receptiveness property discussed below imposes some enabledness requirements.

The pitfall in the Decoupler example discussed above illustrates an important receptiveness property that should normally hold for handshakes. Suppose there is a single request and a single acknowledgement, and their initial values are 0.

Then for a passive handshake r / a:

• if r=0 & a=0 then r+ must be enabled;
• if r=1 & a=1 then r- must be enabled;

and for an active handshake r / a:

• if r=1 & a=0 then a+ must be enabled;
• if r=0 & a=1 then a- must be enabled.

These conditions can be generalised to handshakes comprising multiple requests and/or acknowledgements in a natural way, as we assume that at most one request and at most one acknowledgement can be asserted at any time.

There are, however, some exceptions, in particular when there are dependencies between different handshakes. In the following STG call-final.stg.work (4 KiB), the two passive handshakes r1 / a1 and r2 / a2 are mutually exclusive, as r1+ and r2+ disable each other. Hence, e.g., in a state with r1=0 & a1=0, edge r1+ is not necessarily enabled as r2+ can fire and disable r1+.

In such a situation it would be reasonable to skip the receptiveness checks for r1+ and r2+ (while still keeping them for r1- and r2-). This, however, is not perfect – it would be reasonable in this case to modify these checks, e.g. to require that r1+ is enabled whenever r1=0 & a1=0 & r2=0 & a2=0, but this is not supported in Workcraft yet.

Alternatively, since the handshakes are mutually exclusive, one can treat these two handshakes as a single handshake {r1, r2} / {a1, a2}, which would satisfy the receptiveness property. However, this is not perfect either, as one may want to ensure that r1 is acknowledged specifically by a1 rather than either a1 or a2. Hence, one can combine this check with the ones for simple handshakes with relaxed receptiveness.

Note that if both r1 / a1 and r2 / a2 handshakes are with the same module in the environment, it would be advantageous to re-design the system by sharing the acknowledgement signal (by collapsing a1 and a2 into one signal a12), resulting in a handshake {r1, r2} / a12 with a dual-rail request and a single-rail acknowledgement call-final-a12.stg.work (4 KiB) (the STG can be simplified by merging the corresponding signal edges of a12). This STG passes the receptiveness checks and results in a simpler circuit. However, this modification is not possible when r1 / a1 and r2 / a2 handshakes are with different modules.

In some situations it may be convenient to initialise the circuit in a state that is different from the conventional initial state with both request and acknowledgement withdrawn – this may help to remove the initialisation logic from a critical path. However, one has to be very careful when doing so – the pitfall is that the handshake may progress further than intended during the initialisation. One practical situation we observed was the initialisation of a module interacting with a WAIT element in a state with request ctrl being high. It may happen that sig becomes high during initialisation, causing WAIT to raise acknowledgement san. If the module relies on san being low during its initialisation, it may be wrongly initialised; in fact, in such a situation it would be wrong to rely on either possible initial value of san, as one has to control the initialisation of sig to raise san reliably, which is unlikely.

One can often optimise the circuit implementation by changing the polarity of some signals – this may allow one to remove some inverters and/or replace positive logic gates by negative ones (note that CMOS logic is naturally inverting, and positive gates are usually obtained from their negative counterparts by appending an inverter, which increases the area and delay). Consider the following implementation of the above STG with mutually exclusive handshakes.

By changing the polarity of a, one can get rid of the two inverters with zero delay assumptions (it is possible to optimise this circuit by using a single inverter for a, whose output is then forked into the C-elements – the zero delay assumption would not be necessary in such a case; however, changing polarity still results in a smaller and faster circuit). Furthermore, by changing the polarity of r one can turn the OR-gate into a NOR-gate that is likely to be smaller and faster. (Of course, these transformations should be reflected in the design of the environment, and the achieved savings may sometimes be offset by the overheads introduced in the environment, so one should be careful.)

Workcraft's handshake wizard helps the user to formulate and verify the necessary handshake properties. It can be accessed via the Verification→Handshake wizard [MPSat]… menu item, and opens the following dialog (its appearance depends on whether the handshake is passive or active):

Handshake wizard for passive handshake

Handshake wizard for active handshake

First, the user specifies whether the handshake is passive or active. For passive handshakes, all inputs are listed as potential requests, and outputs as potential acknowledgements, and vice versa for active handshakes.

Then the user can select the requests and acknowledgements – as explained above, there can be multiple requests and/or multiple acknowledgements. Note that at least one request and at least acknowledgement must be selected, as otherwise the   OK   button will be disabled.

There are two receptiveness checks which depend on the type of the handshake, as explained above. They are enabled by default, but the user can disable one or both of them by un-checking the corresponding checkbox(es).

The user can also change the initial state of the handshake – the radio buttons and their labels are arranged to resemble a Petri net where a token shows the initial state.

If the polarity of at least one signal in a handshake differs from the default one, the user must also tick the “Allow arbitrary inversions of signals” checkbox. Note that the polarities can be deduced automatically, from the initial state of the handshake and the initial values of the signals participating in the handshake, so this checkbox is just a safety feature to inform the tool that the polarity changes are intentional rather than accidental.

Download all the Workcraft models discussed in this tutorial here:

All STGs and circuits (17 KiB)