Petrify command line options
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