Auxiliary programs

Besides the main yosys executable, the Yosys distribution contains a set of additional helper programs.


The yosys-config tool (an auto-generated shell-script) can be used to query compiler options and other information needed for building loadable modules for Yosys. See Writing extensions for details.

Usage: ./yosys-config [--exec] [--prefix pf] args..
       ./yosys-config --build cppsources..

Replacement args:
    --cxx         ccache clang++
    --cxxflags    -Wall -Wextra -ggdb -I"/usr/local/share/yosys/include" \
                      -MD -MP -D_YOSYS_ -fPIC -I/usr/local/include -std=c++11 \
                      -I/usr/include/tcl8.6 -DYOSYS_ENABLE_TCL -DYOSYS_ENABLE_ABC \
    --linkflags   -rdynamic
    --ldflags     (alias of --linkflags)
    --libs        -lstdc++ -lm -lrt -lreadline -lffi -ldl -lz -ltcl8.6 -ltclstub8.6
    --ldlibs      (alias of --libs)
    --bindir      /usr/local/bin
    --datdir      /usr/local/share/yosys

All other args are passed through as they are.

Use --exec to call a command instead of generating output. Example usage:

  ./yosys-config --exec --cxx --cxxflags --ldflags -o -shared --libs

The above command can be abbreviated as:

  ./yosys-config --build

Use --prefix to change the prefix for the special args from '--' to
something else. Example:

  ./yosys-config --prefix @ bindir: @bindir

The args --bindir and --datdir can be directly followed by a slash and
additional text. Example:

  ./yosys-config --datdir/simlib.v


The yosys-filterlib tool is a small utility that can be used to strip or extract information from a Liberty file. This can be useful for removing sensitive or proprietary information such as timing or other trade secrets.

Usage: filterlib [rules-file [liberty-file]]
   or: filterlib -verilogsim [liberty-file]


This is a fork of ABC with a small set of custom modifications that have not yet been accepted upstream. Not all versions of Yosys work with all versions of ABC. So Yosys comes with its own yosys-abc to avoid compatibility issues between the two.

usage: ./yosys-abc [-c cmd] [-q cmd] [-C cmd] [-Q cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [-b] [file]
    -c cmd	execute commands `cmd'
    -q cmd	execute commands `cmd' quietly
    -C cmd	execute commands `cmd', then continue in interactive mode
    -Q cmd	execute commands `cmd' quietly, then continue in interactive mode
    -F script	execute commands from a script file and echo commands
    -f script	execute commands from a script file
    -h		print the command usage
    -o file	specify output filename to store the result
    -s		do not read any initialization file
    -t type	specify input type (blif_mv (default), blif_mvs, blif, or none)
    -T type	specify output type (blif_mv (default), blif_mvs, blif, or none)
    -x		equivalent to '-t none -T none'
    -b		running in bridge mode


The yosys-smtbmc tool is a utility used by SBY for interacting with smt solvers.

yosys-smtbmc [options] <yosys_smt2_output>

    -h, --help
    	show this message

    -t <num_steps>
    -t <skip_steps>:<num_steps>
    -t <skip_steps>:<step_size>:<num_steps>
        default: skip_steps=0, step_size=1, num_steps=20

        generate an arbitrary trace that satisfies
        all assertions and assumptions.

        instead of BMC run temporal induction

        instead of regular BMC run cover analysis

    -m <module_name>
        name of the top module

    --smtc <constr_filename>
        read constraints file

    --cex <cex_filename>
        read cex file as written by ABC's "write_cex -n"

    --aig <prefix>
        read AIGER map file (as written by Yosys' "write_aiger -map")
        and AIGER witness file. The file names are <prefix>.aim for
        the map file and <prefix>.aiw for the witness file.

    --aig <aim_filename>:<aiw_filename>
        like above, but for map files and witness files that do not
        share a filename prefix (or use different file extensions).

        the AIGER witness file does not include the status and
        properties lines.

    --yw <yosys_witness_filename>
        read a Yosys witness.

    --btorwit <btor_witness_filename>
        read a BTOR witness.

        only run the core proof, do not collect and print any
        additional information (e.g. which assert failed)

        check if the design with assumptions but without assertions
        is SAT before checking if assertions are UNSAT. This will
        detect if there are contradicting assumptions. In some cases
        this will also help to "warm up" the solver, potentially
        yielding a speedup.

        only check final constraints, assume base case

    --assume-skipped <start_step>
        assume asserts in skipped steps in BMC.
        no assumptions are created for skipped steps
        before <start_step>.

    --dump-vcd <vcd_filename>
        write trace to this VCD file
        (hint: use 'write_smt2 -wires' for maximum
        coverage of signals in generated VCD file)

    --dump-yw <yw_filename>
        write trace as a Yosys witness trace

    --dump-vlogtb <verilog_filename>
        write trace as Verilog test bench

    --vlogtb-top <hierarchical_name>
        use the given entity as top module for the generated
        Verilog test bench. The <hierarchical_name> is relative
        to the design top module without the top module name.

    --dump-smtc <constr_filename>
        write trace as constraints file

        write just the last state as initial constraint to smtc file

    --smtc-top <old>[:<new>]
        replace <old> with <new> in constraints dumped to smtc
        file and only dump object below <old> in design hierarchy.

        do not assume initial conditions in state 0

        when using -g or -i, create a dump file for each
        step. The character '%' is replaced in all dump
        filenames with the step number.

    --append <num_steps>
        add <num_steps> time steps at the end of the trace
        when creating a counter example (this additional time
        steps will still be constrained by assumptions)

        dump anyconst values as raw bit strings

        continue BMC after the first failed assertion and report
        further failed assertions. To output multiple traces
        covering all found failed assertions, the character '%' is
        replaced in all dump filenames with an increasing number.
        In cover mode, don't stop when a cover trace contains a failed

        check that the used witness file contains sufficient
        constraints to force an assertion failure.

        check if states are unique in temporal induction counter examples
        (this feature is experimental and incomplete)

        run in incremental mode (experimental)

        track individual assumptions and report a subset of used
        assumptions that are sufficient for the reported outcome. This
        can be used to debug PREUNSAT failures as well as to find a
        smaller set of sufficient assumptions.

        when using --track-assumes, solve for a minimal set of sufficient assumptions.

    -s <solver>
        set SMT solver: z3, yices, boolector, bitwuzla, cvc4, mathsat, dummy
        default: yices

    -S <opt>
        pass <opt> as command line argument to the solver

    --timeout <value>
        set the solver timeout to the specified value (in seconds).

    --logic <smt2_logic>
        use the specified SMT2 logic (e.g. QF_AUFBV)

    --dummy <filename>
        if solver is "dummy", read solver output from that file
        otherwise: write solver output to that file

    --smt2-option <option>=<value>
        enable an SMT-LIBv2 option.

        enable debug output

        unroll uninterpreted functions

        don't use incremental solving, instead restart solver for
        each (check-sat). This also avoids (push) and (pop).

        disable timer display during solving
        (this option is set implicitly on Windows)

    --dump-smt2 <filename>
        write smt2 statements to file

    --info <smt2-info-stmt>
        include the specified smt2 info statement in the smt2 output

        strip all comments from the generated smt2 code


yosys-witness is a new tool to inspect and convert yosys witness traces. This is used in SBY and SCY for producing traces in a consistent format independent of the solver.

Usage: yosys-witness [OPTIONS] COMMAND [ARGS]...

  --help  Show this message and exit.

  aiw2yw   Convert an AIGER witness trace into a Yosys witness trace.
  display  Display a Yosys witness trace in a human readable format.
  stats    Display statistics of a Yosys witness trace.
  wit2yw   Convert a BTOR witness trace into a Yosys witness trace.
  yw2aiw   Convert a Yosys witness trace into an AIGER witness trace.
  yw2yw    Transform a Yosys witness trace.


yosys-witness requires click Python package for use.