User Tools

Site Tools


help:backend:mpsat

MPSat command line options

Usage:
        mpsat [-h]
or
        mpsat <mode> [<options>] [<in_file>] [<out_file>]

The <mode> is one of the following:
  Unfolding/unravelling modes:
    -U[m|p] - Build a complete merged process (-Um) or unfolding prefix (-Up).
  Reachability-based formal verification modes:
    -D - Deadlock checking.
    -F[a|e|s]=<property_file> - Check a reachability-like property.
  Temporal property formal verification mode:
    -B=<property_file> - Check a stutter-invariant temporal property.
  Encoding conflicts detection and resolution modes:
    -C[c|n|u] - Check the CSC/normalcy/USC property.
    -R - Resolve CSC conflicts.
  Synthesis modes:
    -I[e|g|s] - Derive a complex-gate/gC/standard-C implementation.
    -T[=<gate_library>] - Logic decomposition and technology mapping.

The <options> are as follows:
  -# - Allow non-local configurations as cut-off correspondents.
  -! - Disable branching on auxiliary variables.
  -$N - Switch to SAT solver N (0-1).
  -@N - Use adequate order N (0-4).
  -a[N] - Compute all solutions (might be slow).
  -b - Generate backward conflict constraints.
  -c - Do not store cut-off events.
  -d - Allow dummy cut-off events when unfolding an STG.
  -e - Print out configurations rather than traces.
  -f[s|l|<COEFF>=<EXPR>] - Minimise (and perhaps specify) the cost function.
  -g[!][N] - Filter gates/latches used for logic decomposition.
  -i[+|-] - Specify whether to generate inclusion constraints.
  -jN - The number of working threads.
  -l - Replicate places with multiple self-loops.
  -mN - Use method N (1-9).
  -nN - Switch to memory efficient unfolding algorithm after N events.
  -pN - Controls the use of parallel (concurrent) inserions.
  -q - Quit early, after checking the property syntax.
  -r - Allows to use concurrency reduction for encoding conflict resolution.
  -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 before exiting (prevents the window from closing).

Detailed help

Copyright © 2014-2024 workcraft.org

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki