usage: ./petrify [flags] [infile] General options: ---------------- -v print version only -d[n] debug level (n=1,2) -o outfile STG output file (default: stdout) -no output file not generated -log logfile log filename (default: petrify.log) -err errfile error filename (default: stderr) -nolog no log file generated -ip show implicit (1-fanin 1-fanout) places -dead do not check for the existence of deadlock states -sis print SIS output style (~ for toggle transitions) Options for Petri net synthesis: -------------------------------- -all search for all minimal regions (even for irredundant nets) -sat generate a minimal satured Petri net -min generate a Petri net with minimal regions only (no place merging) -opt find the best result (may override other options) -noec generate a Petri net without label splitting (possibly without excitation closure) -hide list hide the signals in the list -bisim maintain bisimilarity after removing events -mints minimize the transition system before synthesis Options for Petri net properties: --------------------------------- -p generate a pure Petri net -fc generate a Free-Choice net -efc generate an Extended Free-Choice net -uc generate a Unique-Choice net (with no extended free choices) -euc generate a Unique-Choice net (with extended free choices) -er generate a different label for each excitation region -sm generate an SM-decomposable net Options for STG transformations: -------------------------------- -tog all +/- transitions are converted to toggle -untog all toggle and hatch transitions are converted to +/- -2ph expand channel events to 2-phase protocol (default) -4ph expand channel events to 4-phase protocol -redc concurrency reduction for logic optimization -redz concurrency reduction for RTZ events only -redn1 conservative concurrency reduction for noise isolation -redn2 concurrency reduction for noise isolation -noise noise analysis Options for synthesis of asynchronous circuits: ----------------------------------------------- -csc[n] solve CSC (with blocks of at most n intersecting regions) -icsc[n] same as -csc with iterative removal of internal signals -ncsc[n] maximum number of inserted state signals -tcsc solve CSC aiming at improving performance (default for timing optimization) -acsc solve CSC aiming at improving area (default if no timing optimization) -io preserve I/O interface (ignore slow input events) -cg generate complex gates -gc generate generalized C elements -gcm generate generalized C elements with monotonic covers -nosi generate complex gates even for a non-SI specification -mc generate monotonic covers -tm[n] technology mapping (n is the depth of search) -tm_ratio[x] area/delay ratio for technology mapping -stm sequential technology mapping (only latches are mapped) -nmap[n] maximum number of inserted signals for technology mapping -eqn file generate logic description in EQN format -blif file generate logic description in BLIF format -vl file generate logic description in Verilog format -rst0 generate reset pin active at 0 (only for Verilog netlists) -rst1 generate reset pin active at 1 (only for Verilog netlists) -lib file read gate library -selckt interactive selection of gates for each non-input signal -latch str define allowed latches for sequential decomposition -nolatch no latches used for technology mapping -lit[n] logic decomposition with gates with at most n literals -cgd[n] max number of complex gates for each gate decomposition -algd[n] max number of algebraic divisors for each gate decomposition -mcd[n] max number of monotonic covers for each signal decomposition -boold[n] max number of boolean decompositions for each gate -ed exhaustive decomposition -topt logic optimization using timing constraints -atopt logic optimization using automatic timing constraints -avg timing optimization for average case (default: worst-case) Advanced options: ----------------- -s[n] search depth for label splitting (def. -s3, infinite with -s) -rc[n] max number of non-essential regions for optimal irredundancy -cl[n] max size of compatibility graph for one-hot->log encoding -nice_csc CSC: attempts to find nice signal insertions -seq CSC: do not increase concurrency of new state signals -fr[n] CSC: frontier width for exploration of insertion blocks -cw[x] CSC: tune eagerness to solve conflicts -redfr[n] frontier width for exploration of concurrency reduction -trflat[n] BDD node limit to flatten partitioned transition relations -boolmin[n] define type of boolean minimization -notog No toggle changes in transition relations -noreord No dynamic variable reordering -reord[n] Reordering frequency