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