User Tools

Site Tools


Command line options of backend tools

This is a summary of command line options for some of Workcraft backend tools.

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

MPSat command line options

    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.

Detailed help

Punf command line options

     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.)
       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.
       Switches on the LTL-X verification mode. The file must be in
       the HOA format ( and specify a Buechi
       automaton for an LTL-X property. The adequate order must be -@3.
       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.

PComp command line options

    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.

  -d  Convert the common interface signals into dummy signals
      (useful for composing handshake components).
      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).
      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.
Copyright © 2014-2021