Petrify is a tool for the synthesis of bounded Petri nets and logic synthesis of asynchronous controllers. Petrify initially performs a token flow analysis of the Petri net and produces a finite transition system (TS). In the initial TS, all transitions with the same label are considered as one event. The TS is then transformed and transitions relabeled to fulfil the conditions required to obtain a Petri net with bisimilar or trace-equivalent behavior. Some properties for the synthesized Petri net can be imposed (e.g. free-choice, uniquechoice, pure, state-machine decomposable, etc.). Additionally, petrify can interpret the Petri net as a Signal Transition Graph (STG), in which events represent rising/falling transitions of digital signals. From an STG, petrify can synthesize a speed-independent circuit by solving the problems of state encoding, logic synthesis, logic decomposition and technology mapping onto a gate library. Petrify can also synthesize circuit under timing assumptions specified by the designer or automatically generated by the tool. Petrify reads the input description from stdin and writes the resulting STG to stdout unless otherwise specified