verific - load Verilog and VHDL designs using Verific

    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..

Load the specified Verilog/SystemVerilog files into Verific.

All files specified in one call to this command are one compilation unit.
Files passed to different calls to this command are treated as belonging to
different compilation units.

Additional -D<macro>[=<value>] options may be added after the option indicating
the language version (and before file names) to set additional verilog defines.
The macros YOSYS, SYNTHESIS, and VERIFIC are defined implicitly.

    verific -formal <verilog-file>..

Like -sv, but define FORMAL instead of SYNTHESIS.

    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..

Load the specified VHDL files into Verific.

    verific {-f|-F} <command-file>

Load and execute the specified command file.

Command file parser supports following commands:
    +define    - defines macro
    -u         - upper case all identifier (makes Verilog parser case insensitive)
    -v         - register library name (file)
    -y         - register library name (directory)
    +incdir    - specify include dir
    +libext    - specify library extension
    +liborder  - add library in ordered list
    +librescan - unresolved modules will be always searched starting with the first
                 library specified by -y/-v options.
    -f/-file   - nested -f option
    -F         - nested -F option

    parse mode:

    verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>

Load the specified Verilog/SystemVerilog/VHDL file into the specified library.
(default library when -work is not present: "work")

    verific [-L <libname>] {-sv|-vhdl|...} <hdl-file>

Look up external definitions in the specified library.
(-L may be used more than once)

    verific -vlog-incdir <directory>..

Add Verilog include directories.

    verific -vlog-libdir <directory>..

Add Verilog library directories. Verific will search in this directories to
find undefined modules.

    verific -vlog-define <macro>[=<value>]..

Add Verilog defines.

    verific -vlog-undef <macro>..

Remove Verilog defines previously set with -vlog-define.

    verific -set-error <msg_id>..
    verific -set-warning <msg_id>..
    verific -set-info <msg_id>..
    verific -set-ignore <msg_id>..

Set message severity. <msg_id> is the string in square brackets when a message
is printed, such as VERI-1209.

    verific -import [options] <top-module>..

Elaborate the design for the specified top modules, import to Yosys and
reset the internal state of Verific.

Import options:

    Elaborate all modules, not just the hierarchy below the given top
    modules. With this option the list of modules to import is optional.

    Create a gate-level netlist.

    Flatten the design in Verific before importing.

    Resolve references to external nets by adding module ports as needed.

    Generate automatic cover statements for all asserts

    Keep all register initializations, even those for non-FF registers.

  -chparam name value 
    Elaborate the specified top modules (all modules when -all given) using
    this parameter value. Modules on which this parameter does not exist will
    cause Verific to produce a VERI-1928 or VHDL-1676 message. This option
    can be specified multiple times to override multiple parameters.
    String values must be passed in double quotes (").

  -v, -vv
    Verbose log messages. (-vv is even more verbose than -v.)

The following additional import options are useful for debugging the Verific
bindings (for Yosys and/or Verific developers):

    Keep going after an unsupported verific primitive is found. The
    unsupported primitive is added as blockbox module to the design.
    This will also add all SVA related cells to the design parallel to
    the checker logic inferred by it.

    Import Verific netlist as-is without translating to Yosys cell types. 

    Ignore SVA properties, do not infer checker logic.

  -L <int>
    Maximum number of ctrl bits for SVA checker FSMs (default=16).

    Keep all Verific names on instances and nets. By default only
    user-declared names are preserved.

  -d <dump_file>
    Dump the Verific netlist as a verilog file.

    verific [-work <libname>] -pp [options] <filename> [<module>]..

Pretty print design (or just module) to the specified file from the
specified library. (default library when -work is not present: "work")

Pretty print options:

    Save output for Verilog/SystemVerilog design modules (default).

    Save output for VHDL design units.

    verific -app <application>..

Execute YosysHQ formal application on loaded Verilog files.

Application options:

    -module <module>
        Run formal application only on specified module.

    -blacklist <filename[:lineno]>
        Do not run application on modules from files that match the filename
        or filename and line number if provided in such format.
        Parameter can also contain comma separated list of file locations.

    -blfile <file>
        Do not run application on locations specified in file, they can represent filename
        or filename and location in file.


  WARNING: Applications only available in commercial build.

    verific -template <name> <top_module>..

Generate template for specified top module of loaded design.

Template options:

    Specifies output file for generated template, by default output is stdout

  -chparam name value 
    Generate template using this parameter value. Otherwise default parameter
    values will be used for templat generate functionality. This option
    can be specified multiple times to override multiple parameters.
    String values must be passed in double quotes (").


  WARNING: Templates only available in commercial build.

    verific -cfg [<name> [<value>]]

Get/set Verific runtime flags.

Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.

Contact for free evaluation
binaries of YosysHQ Tabby CAD Suite.