User Tools

Site Tools


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

Copyright © 2014-2021