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
WAIT0 according to the polarity of its ctrl input.
W2C is captured by the following STG.
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:
Proceed to synthesis and technology mapping with either MPSat or Petrify backend. The result should look similar to this:
Experiment with reset strategies using Initialisation analyser tool. One can notice that
ctr input is initially set to
CYCLE module, also C-element
U2 can be explicitly reset. These lead to initialisation of
0, which reset
san_0 (outputs of