User Tools

Site Tools


help:backend:mpsat

MPSat command line options

Usage:
  mpsat mode [options] inputfilename [outputfilename]

Modes:
  Reachability-like properties checking modes:
    -D    Deadlock checking.
    -F    Find a reachable marking satisfying a given REACH predicate.
    -Fs   Find a reachable STG state satisfying a given REACH predicate.
    -Fa   Check an SVA-like assertion (a global invariant).
  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).

Options:
  -! - 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.
  -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