Design of WAIT2 component

Decompose the WAIT2 component into WAIT for waiting the high level of non-persistent signal sig and WAIT0 for its low level. The control module W2C toggles between WAIT and WAIT0 according to the polarity of its ctrl input.

Schematic of WAIT2 component|

Behaviour of W2C is captured by the following STG.

STG of W2C control|

Verify the STG for consistency, deadlocks, output-persistency and input-properness.

Note that this STG has CSC conflicts. Resolve them either automatically or manually, e.g. by concurrency reduction, as follows:

STG of W2C control with concurrency reduction to resolve CSC conflicts|

Proceed to synthesis and technology mapping with either MPSat or Petrify backend. The result should look similar to this:

Implementation of W2C control|

Experiment with reset strategies using Initialisation analyser tool. One can notice that ctr input is initially set to 0 by CYCLE module, also C-element U2 can be explicitly reset. These lead to initialisation of ctrl_1 and ctrl_0 to 0, which reset san_1 and san_0 (outputs of WAIT and WAIT0).