PETRIFY - A TOOL FOR MANIPULATING CONCURRENT SPECIFICATIONS AND SYNTHESIS OF ASYNCHRONOUS CONTROLLERS

Petrify is a tool for (1) manipulating concurrent specifications and ( 2) synthesis and optimization of asynchronous control circuits. Given a Petri Net (PN), a Signal Transition Graph (STG), or a Transition Sys tem (TS) it (1) generates another PN or STG which is simpler than the original description and (2) produces an optimized net-list of an asy nchronous controller in the target gate library while preserving the s pecified input-output behavior. An ability of back-annotating to the s pecification level helps the designer to control the design process. F or transforming a specification petrify performs a token flow analysis of the initial PN and produces a transition system (TS). In the initi al TS, all transitions with the same label are considered as one event . The TS is then transformed and transitions relabeled to fulfill the conditions required to obtain a safe irredundant PN. For synthesis of an asynchronous circuit petrify performs state assignment by solving t he Complete State Coding problem. State assignment is coupled with log ic minimization and speed-independent technology mapping to a target l ibrary. The final net-list is guaranteed to be speed-independent, i.e. , hazard-free under any distribution of gate delays and multiple input changes satisfying the initial specification. The tool has been used for synthesis of PNs and PNs composition, synthesis and re-synthesis o f asynchronous controllers and can be also applied in areas related wi th the analysis of concurrent programs. This paper provides an overvie w of petrify and the theory behind its main functions.