====== Handshakes Verification ======

It is common to use [[wp>Asynchronous_circuit#Protocols|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.

===== Why handshake verification? =====

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 ''<color red>rl</color>'' / ''<color blue>al</color>'' and ''<color blue>rr</color>'' / ''<color red>ar</color>'', 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.

{{ decoupler-interface.circuit.svg?50%,nolink |Decoupler interface}}

Consider the following simple STG describing the Decoupler component <wrap download>{{buggy-decoupler.stg.work}}</wrap>. 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? 

<WRAP center round alert 40%>
{{ buggy-decoupler.stg.svg?35%,nolink |Buggy decoupler}}
</WRAP>

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 ''<color red>rl+</color>'' immediately after ''<color blue>al-</color>'', e.g. as follows <wrap download>{{decoupler.stg.work}}</wrap>:

{{ decoupler.stg.svg?35%,nolink |Fixed decoupler}}

The above bug can be caught if one verifies the [[help:verification|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.

==== Multi-signal requests and acknowledgements ====

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 [[tutorial:design:vme_bus:start|VME bus controller]] has a handshake {''<color red>dsr</color>'', ''<color red>dsw</color>''} / ''<color blue>dtack</color>'' 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).

==== Signal order ====

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.

==== Receptiveness ====

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 ''<color red>r</color>'' / ''<color blue>a</color>'': 
  * if ''<color red>r</color>=0 & <color blue>a</color>=0'' then ''<color red>r+</color>'' must be enabled;
  * if ''<color red>r</color>=1 & <color blue>a</color>=1'' then ''<color red>r-</color>'' must be enabled;

and for an active handshake ''<color blue>r</color>'' / ''<color red>a</color>'':
  * if ''<color blue>r</color>=1 & <color red>a</color>=0'' then ''<color red>a+</color>'' must be enabled;
  * if ''<color blue>r</color>=0 & <color red>a</color>=1'' then ''<color red>a-</color>'' 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 <wrap download>{{call-final.stg.work}}</wrap>, the two passive handshakes ''<color red>r1</color>'' / ''<color blue>a1</color>'' and ''<color red>r2</color>'' / ''<color blue>a2</color>'' are mutually exclusive, as ''<color red>r1+</color>'' and ''<color red>r2+</color>'' disable each other. Hence, e.g., in a state with ''<color red>r1</color>=0 & <color blue>a1</color>=0'', edge ''<color red>r1+</color>'' is not necessarily enabled as ''<color red>r2+</color>'' can fire and disable ''<color red>r1+</color>''.

{{ call-final.stg.svg?35%,nolink |STG with mutually exclusive handshakes}}

In such a situation it would be reasonable to skip the receptiveness checks
for ''<color red>r1+</color>'' and ''<color red>r2+</color>''
(while still keeping them for ''<color red>r1-</color>'' and ''<color red>r2-</color>''). This, however, is not perfect -- it would be reasonable in this case to modify these checks, e.g. to require that ''<color red>r1+</color>'' is enabled whenever ''<color red>r1</color>=0 & <color blue>a1</color>=0 & <color red>r2</color>=0 & <color blue>a2</color>=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 {''<color red>r1</color>'', ''<color red>r2</color>''} / {''<color blue>a1</color>'', ''<color blue>a2</color>''}, which would satisfy the receptiveness property. However, this is not perfect either, as one may want to ensure that ''<color red>r1</color>'' is acknowledged specifically by ''<color blue>a1</color>'' rather than either ''<color blue>a1</color>'' or ''<color blue>a2</color>''. Hence, one can combine this check with the ones for simple handshakes with relaxed receptiveness.

Note that if both ''<color red>r1</color>'' / ''<color blue>a1</color>'' and ''<color red>r2</color>'' / ''<color blue>a2</color>'' 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 ''<color blue>a1</color>'' and ''<color blue>a2</color>'' into one signal ''<color blue>a12</color>''), resulting in a handshake {''<color red>r1</color>'', ''<color red>r2</color>''} / ''<color blue>a12</color>'' with a dual-rail request and a single-rail acknowledgement <wrap download>{{call-final-a12.stg.work}}</wrap> (the STG can be simplified by merging the corresponding signal edges of ''<color blue>a12</color>''). This STG passes the receptiveness checks and results in a simpler circuit. However, this modification is not possible when ''<color red>r1</color>'' / ''<color blue>a1</color>'' and ''<color red>r2</color>'' / ''<color blue>a2</color>'' handshakes are with different modules.

{{ call-final-a12.stg.svg?35%,nolink |STG with mutually exclusive handshakes and shared acknowledgement}}

==== Initial state of handshake ====

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 [[a2a:start|WAIT element]] in a state with request ''<color blue>ctrl</color>'' being high. It may happen that ''<color red>sig</color>'' becomes high during initialisation, causing WAIT to raise acknowledgement ''<color red>san</color>''. If the module relies on ''<color red>san</color>'' 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 ''<color red>san</color>'', as one has to control the initialisation of ''<color red>sig</color>'' to raise ''<color red>san</color>'' reliably, which is unlikely.

{{ wait-interface.circuit.svg?50%,nolink |WAIT element interface}}

==== Signal inversions ====

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. 

{{ call-final.circuit.svg?50%,nolink |Circuit for the STG with mutually exclusive handshakes}}

By changing the polarity of ''<color red>a</color>'', 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 ''<color red>a</color>'', 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 ''<color blue>r</color>'' 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.)

===== Handshake wizard =====

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):

<WRAP group>
<WRAP column half>
|  {{ handshake_wizard-passive.png?nolink |}}  |
|  Handshake wizard for //passive// handshake  |
</WRAP>
<WRAP column half>
|  {{ handshake_wizard-active.png?nolink |}}  |
|  Handshake wizard for //active// handshake  |
</WRAP>
</WRAP>

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 <key>''\ \ OK\ \ ''</key> 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.

===== Solutions =====

Download all the Workcraft models discussed in this tutorial here:

<wrap download>{{handshake_wizard.zip|All STGs and circuits}}</wrap>

====== ======
{{page>:tutorial:feedback&inline}}