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:
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.
petrify.libto much larger
workcraft.lib); this will be fixed eventually.
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.