This is a comparative analysis of Petrify and MPSat approaches to synthesis of speed-independent circuits.

The number of reachable states is generally exponential in the size of the STG, which is a fundamental problem known as State Space Explosion (or just State Explosion). There is no general solution, but there are various heuristics and data structures allowing one to mitigate this problem in some practical cases.

The main difference between Petrify and MPSat is in the data structure used to represent the set of reachable states. Petrify uses Binary Decision Diagrams (BDD) while MPSat uses Petri net unfolding prefix (or just Unfolding) generated by PUNF. Unfoldings tend to be more efficient for “practical” STGs as these tend to have a lot of concurrency but rather few choices. However, there are no hard guarantees – one can always find examples where one technique dies and the other excels.

This part of design flow requires inserting new signals and so a lot of creativity is required from the tool. It relies on complicated heuristics and so it is easy to find examples where one tool dies while the other completes, or when both tools complete but the quality of the results differs significantly, so there is no clear winner. Hence the advice is to try both tools and choose the better solution. There is a tutorial about CSC resolution.

Logic synthesis requires CSC to be already resolved. If the STG has CSC conflicts, Petrify will silently resolve them before proceeding to the synthesis, whereas MPSat will output an error. The gate library is completely ignored, i.e. no mapping is performed at this stage.

Always verify the derived circuits – though they are meant to be correct by construction, MPSat and Petrify are complex tools and may have bugs.

Generally, logic synthesis is relatively straightforward (apart from the computational complexity) and no creative decisions (like how to insert new signals) have to be made at this stage. In almost all practical cases MPSat will be significantly faster, and will deliver solutions of similar or better quality to Petrify's. Also Petrify occasionally produces wrong solutions in the gC and stdC modes. Hence, the advice is to use MPSat in the following three logic synthesis modes:

• Complex-gate – each signal is implemented as a Boolean function of arbitrary complexity.

• Generalised C-element synthesis – each signal is implemented by a state-holding “keeper” (two inverters as in the usual C-element) with pull-up and pull-down networks of transistors, which are not necessarily complementary. These are obtained from the Boolean set and reset functions of arbitrary complexity derived by the tools in this mode. Petrify is known occasionally to derive wrong implementations in this mode, so always verify!

• Standard C-element synthesis – each signal is implemented by a C-element controlled by two combinational gates implementing “monotonic” set and reset functions (these are bigger than the gC set/reset functions due to the extra monotonicity constraint). Petrify is VERY BUGGY in this mode, so Workcraft does not have the corresponding entry for Petrify in its synthesis menu to discourage its use.

CSC is required to be already resolved. If the STG has CSC conflicts, Petrify will silently resolve them before proceeding, whereas MPSat will output an error.

In this mode the tools try to map the implementation to the gate library. This is the most complicated step in the flow, which often fails. It involves inserting new signals, and so much creativity is required from the tool. Hence the advice is to try both tools and choose the better solution.

Note that:

• Zero delay inverters are often created in this mode for technical reasons.

• Petrify is known occasionally to derive wrong implementations in this mode, so always verify!

• The final optimisation step involving pushing the bubbles around (with the view to reduce the number of inverters and make as many gates negative as possible) and gluing smaller gates into a bigger one wherever possible is not implemented in MPSat, so often one can manually improve the resulting circuit by doing such transformations.

Petrify supports relative timing assumptions. These are not implemented in MPSat, and are not supported via Workcraft GUI (apart from zero delay inverters and buffers), and disrupt the speed-independent design flow. If timing assumptions are required, one has to fall back on Petrify's command-line interface.