This is a summary of command line options for some of Workcraft backend tools.
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
Usage: mpsat <mode> [<options>] [<in_file>] [<out_file>] The <mode> is one of the following: -D Deadlock checking. Reachability-like properties checking modes: -F Find a configuration satisfying a given REACH predicate. -Fa Check an SVA-like assertion (a global invariant). -Fe Like -F but assumes an STG unfolding and enabledness via dummies. -Fs Like -Fe, but considers only configurations without maximal dummies. Encoding conflicts detection and resolution modes: -C CSC conflict detection. -N Normalcy property checking mode. -R Resolve encoding conflicts. -U USC conflict detection. Synthesis modes: -E Derive complex-gate implementation. -G Derive gC-elements implementation. -S Derive standard-C implementation. -T Logic decomposition and technology mapping (experimental). The <options> are as follows: -! - Disable branching on auxiliary variables. -$N - Switch to SAT solver N (0-1). -@ - Output configurations rather than traces. -a[N] - Compute all solutions (might be slow). -b - Generate backward conflict constraints. -c(s|l|COEFF=EXPR) - Specifies the coefficients for the cost function. -d string - Specifies additional mode-dependent data. -f - Looking for a solution minimising the cost function (might be slow). -g[[!][N]] - Specifies gates/latches used for logic decomposition. -l[+|-] - Specifies whether to generate inclusion constraints. -mN - Using method N (1-9). -pN - Controls the use of parallel (concurrent) inserions. -q - Quit early, after checking the predicate syntax. -r - Allows to use concurrency reduction for encoding conflict resolution. -s - Store the CNF formula for an external SAT solver. -t - Perform logic decomposition down to the gate/latch level. -vN - The verbosity level (0<=N<=9, the default is 0). -w[N] - Wait for user input before exiting (prevents the window from closing). -x - Saves the results in mpsat.xml.
Usage: punf [options] [-f=]filename Options (may be given in any order): -h Help. -# Using non-local configuration as cut-off correspondents. The current implementation is VERY INEFFICIENT. This option is not currently supported in the LTL mode. -$n Switch to SAT solver n (0-1). If n=0 then zChaff is used. If n=1 then MiniSAT is used (default). -@[n] Using adequate order n (0-4). Specifies the adequate order on configurations of the unfolding. If n is not specified or -@ is not used then the default value n=3 (for prefixes) or n=4 (for merged processes) is used. If n=0 then the set inclusion is used. If n=1 then the McMillan's order is used. If n=2 then the size-lexicographical order is used. If n=3 then the total Esparza/Roemer/Vogler (ERV) order is used. If n=4 then the total order with an efficient SAT encoding is used. Only the ERV order is currently supported in the LTL mode. -! Do not optimize preset trees (cheap optimization is performed anyway). (Ignored if -M is specified.) -c Do not store cut-off events (except the successful terminals in the LTL mode). -d When unfolding an STG, allow dummy cut-off events. If this option is not specified, a dummy event e can only be declared cut-off if its corresponding configuration C is a subset of [e], and [e]\C contains only dummies. This option has effect only when unfolding an STG. It is automatically specified if the STG contains only dummy signals. (Currently ignored if -M is specified.) [-f=]filename Specifies the input file. It must be in either FORMAT_N or FORMAT_N2 format (produced by the PEP tool). Alternatively, it must have the suffix `.g' and be in the STG format; then an STG unfolding prefix (which may differ from the underlying Petri net's unfolding prefix) is produced. Aa an experimental feature, high-level nets are supported. For now, only strictly safe nets are allowed, and there are some further restrictions, described in the manual. -L=filename Switches on the LTL-X verification mode. The file must be in the HOA format (http://adl.github.io/hoaf/) and specify a Buechi automaton for an LTL-X property. The adequate order must be -@3. -m[=filename] Specifies the name of the resulting file, whose extension also specifies the format. It can be either the legacy *.mci format for prefixes, the legacy *.mp format for merged processes (if -M is specified), or the new PNML-based *.pnml or *.pnml.gz format. If this option is not specified then the filename for the result is obtained by removing from the input filename the suffix `.ll_net', `.g' or `.hl_net' (if present), and appending the suffix `.pnml.gz', and the resulting prefix or merged process is stored in the new PNML-based format. If the filename is not specified (i.e. just -m is given) then no output file is created. -N=n Specifies the number of working threads (by default, it is equal to the number of processors). (Currently ignored if -M is specified.) -n=n Abandon the concurrency relation and switch to a slower algorithm after the specified number of non-cut-off events is generated. The default value is 50000. If your computer has a lot of memory, increase it to improve the performance. If the value is 0, the concurrency relation is not created. (Ignored if -M is specified.) -p Print running statistics as multiple lines (to estimate progress). -q Print running statistics (to estimate progress). -r Replicate places with multiple self-loops, so that each transition reading a particular place gets its own copy of that place. This transformation can significantly reduce the prefix size for nets with many self-loops. -s Print final statistics. -t Print the running time. -vN Verbosity level (0<=N<=9). The default is 0. -w[N] Wait for user input before exiting (prevents the window from closing). The possible values of N: 0 - do not wait for user input, exit immediately; 1 - wait for user input only if there are errors; 2 - wait for user input only if there are errors or warnings; 3 - always wait for user input. The default is -w0, and -w is equivalent to -w3.
Usage: pcomp [options] [@]file... The files in the command line are interpreted as STG files, except when prefixed with `@', in which case the file should contain a list of STG files, one per line (useful for avoiding the shell restriction on the length of the command line when composing many STGs). All the STGs, both in the command line and in the `@'-prefixed files, are used for composition. * The output signals of the STGs must be disjoint (this constraint can be waived with the -o option), and their union comprises the output signals of the composition. On the other hand, the input signals can be shared by several STGs, and also an output signal of some STG can be an input signal of zero or more other STGs. * The internal and dummy signals, as well as places, are renamed whenever necessary to avoid name clashes. * The composed STG is simplified by removing duplicate places. * 2-phase, 4-phase and mixed-phase STGs can be liberally composed. Options: -d Convert the common interface signals into dummy signals (useful for composing handshake components). -f[file] Stores the composed STG in file rather than standard output. The extension (.g, .pnml, or .pnml.gz) determines the format. If file is not specified, pcomp.g is used. -h Print this help message and exit. -i Convert the common interface signals into internal signals (useful for composing handshake components). -l[file] If the file name is not provided then `pcomp.xml.gz' is used. If the file name ends with `.xml' or `xml.gz' then the correspondence between the places and transitions of the component STGs and those of the composed STG is stored. Otherwise place names of the composed STG are stored, so that the i-th line corresponds to the places of i-th component STG Note that the same place can occur in several lines - this happens when some duplicate place is removed, and some equivalent place is listed instead. -o Allow the STGs to share outputs. -p Before doing the parallel composition, remove places whose presets do not contain dummy transitions and whose postsets contain only shared input signals on which the labelling is injective. This transformation results in a composed STG with fewer places, which has bisimilar behaviour provided the composition is free from computational interference. This option is incompatible with -o. -r Rename all dummy transitions, so that their names do not contain '+', '-', or '/'. (Needed for compatibility with tools that do not allow dummy transitions to have signs, e.g. Petrify.) -u Keep unused signal transition phases. This option considers e.g. x+ and x- as independent transition labels. By default, if two STGs are composed, and one of them has x+ but no x-, while the other has x- but no x+, the composed STG will have no transitions labelled by either x+ or x-. However, if this option is specified, both labels will occur in the composed STG.