Reading input files¶

connect_rpc - connect to RPC frontend¶

yosys> help connect_rpc¶

connect_rpc -exec <command> [args...]¶

connect_rpc -path <path>¶

Load modules using an out-of-process frontend.

-exec <command> [args...]

run <command> with arguments [args...]. send requests on stdin, read
responses from stdout.

-path <path>

connect to Unix domain socket at <path>. (Unix)
connect to bidirectional byte-type named pipe at <path>. (Windows)

A simple JSON-based, newline-delimited protocol is used for communicating with
the frontend. Yosys requests data from the frontend by sending exactly 1 line
of JSON. Frontend responds with data or error message by replying with exactly
1 line of JSON as well.

    -> {"method": "modules"}
    <- {"modules": ["<module-name>", ...]}
    <- {"error": "<error-message>"}
        request for the list of modules that can be derived by this frontend.
        the 'hierarchy' command will call back into this frontend if a cell
        with type <module-name> is instantiated in the design.

    -> {"method": "derive", "module": "<module-name">, "parameters": {
        "<param-name>": {"type": "[unsigned|signed|string|real]",
                           "value": "<param-value>"}, ...}}
    <- {"frontend": "[rtlil|verilog|...]","source": "<source>"}}
    <- {"error": "<error-message>"}
        request for the module <module-name> to be derived for a specific set of
        parameters. <param-name> starts with \ for named parameters, and with $
        for unnamed parameters, which are numbered starting at 1.<param-value>
        for integer parameters is always specified as a binary string of
        unlimited precision. the <source> returned by the frontend is
        hygienically parsedby a built-in Yosys <frontend>, allowing the RPC
        frontend to return anyconvenient representation of the module. the
        derived module is cached,so the response should be the same whenever the
        same set of parameters is provided.

Note

Help text automatically generated from frontends/rpc/rpc_frontend.cc:348

read - load HDL designs¶

yosys> help read¶

read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..¶

Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support
is only available via Verific.)

Additional -D<macro>[=<value>] options may be added after the option indicating
the language version (and before file names) to set additional verilog defines.

read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl2019|-vhdl} <vhdl-file>..¶

Load the specified VHDL files. (Requires Verific.)

read {-edif} <edif-file>..¶

Load the specified EDIF files. (Requires Verific.)

read {-liberty} <liberty-file>..¶

Load the specified Liberty files.

-lib

only create empty blackbox modules

read {-f|-F} <command-file>¶

Load and execute the specified command file.
Check verific command for more information about supported commands in file.

read -define <macro>[=<value>]..¶

Set global Verilog/SystemVerilog defines.

read -undef <macro>..¶

Unset global Verilog/SystemVerilog defines.

read -incdir <directory>¶

Add directory to global Verilog/SystemVerilog include directories.

read -verific¶

read -noverific¶

Subsequent calls to 'read' will either use or not use Verific. Calling 'read'
with -verific will result in an error on Yosys binaries that are built without
Verific support. The default is to use Verific if it is available.

Note

Help text automatically generated from frontends/verific/verific.cc:4471

read_aiger - read AIGER file¶

yosys> help read_aiger¶

read_aiger [options] [filename]¶

Load module from an AIGER file into the current design.

-module_name <module_name>

name of module to be created (default: <filename>)

-clk_name <wire_name>

if specified, AIGER latches to be transformed into $_DFF_P_ cells
clocked by wire of this name. otherwise, $_FF_ cells will be used

-map <filename>

read file with port and latch symbols

-wideports

merge ports that match the pattern 'name[int]' into a single
multi-bit port 'name'

-xaiger

read XAIGER extensions

Note

Help text automatically generated from frontends/aiger/aigerparse.cc:1065

read_blif - read BLIF file¶

yosys> help read_blif¶

read_blif [options] [filename]¶

Load modules from a BLIF file into the current design.

-sop

Create $sop cells instead of $lut cells

-wideports

Merge ports that match the pattern 'name[int]' into a single
multi-bit port 'name'.

Note

Help text automatically generated from frontends/blif/blifparse.cc:650

read_json - read JSON file¶

yosys> help read_json¶

read_json [filename]¶

Load modules from a JSON file into the current design See "help write_json"
for a description of the file format.

Note

Help text automatically generated from frontends/json/jsonparse.cc:626

read_liberty - read cells from liberty file¶

yosys> help read_liberty¶

read_liberty [filename]¶

Read cells from liberty file as modules into current design.

-lib

only create empty blackbox modules

-wb

mark imported cells as whiteboxes

-nooverwrite

ignore re-definitions of modules. (the default behavior is to
create an error message if the existing module is not a blackbox
module, and overwrite the existing module if it is  a blackbox module.)

-overwrite

overwrite existing modules with the same name

-ignore_miss_func

ignore cells with missing function specification of outputs

-ignore_miss_dir

ignore cells with a missing or invalid direction
specification on a pin

-ignore_miss_data_latch

ignore latches with missing data and/or enable pins

-ignore_buses

ignore cells with bus interfaces (wide ports)

-setattr <attribute_name>

set the specified attribute (to the value 1) on all loaded modules

-unit_delay

import combinational timing arcs under the unit delay model

Note

Help text automatically generated from frontends/liberty/liberty.cc:482

read_rtlil - read modules from RTLIL file¶

yosys> help read_rtlil¶

read_rtlil [filename]¶

Load modules from an RTLIL file to the current design. (RTLIL is a text
representation of a design in yosys's internal format.)

-nooverwrite

ignore re-definitions of modules. (the default behavior is to
create an error message if the existing module is not a blackbox
module, and overwrite the existing module if it is a blackbox module.)

-overwrite

overwrite existing modules with the same name

-lib

only create empty blackbox modules

-legalize

prevent semantic errors (e.g. reference to unknown wire, redefinition of wire/cell)
by deterministically rewriting the input into something valid. Useful when using
fuzzing to generate random but valid RTLIL.

Note

Help text automatically generated from frontends/rtlil/rtlil_frontend.cc:880

read_slang - read SystemVerilog (slang)¶

yosys> help read_slang¶

read_slang [options] [filename]¶

Read SystemVerilog sources and elaborate a design hierarchy into word-level
netlist form.

--std (1364-2005 | 1800-2017 | 1800-2023 | latest)

The version of the Verilog or SystemVerilog language to use

-I,--include-directory,+incdir <dir-pattern>[,...]

Additional include search paths

--isystem <dir-pattern>[,...]

Additional system include search paths

--disable-local-includes

Disables "local" include path lookup, where include directives search
relative to the file containing the directive first

--incdir-first

Search user-specified include directories (+incdir/-I) before the
local directory of the file containing the include directive. This
matches the behavior of VCS and similar simulators

-D,--define-macro,+define <macro>=<value>

Define <macro> to <value> (or 1 if <value> ommitted) in all source
files

-U,--undefine-macro <macro>

Undefine macro name at the start of all source files

--max-include-depth <depth>

Maximum depth of nested include files allowed

--libraries-inherit-macros

If true, library files will inherit macro definitions from the primary
source files. --single-unit must also be passed when this option is
used.

--enable-legacy-protect

If true, the preprocessor will support legacy protected envelope
directives, for compatibility with old Verilog tools

--translate-off-format <common>,<start>,<end>

Set a format for comment directives that mark a region of disabled
source text. The format is a common keyword, a start word, and an end
word, each separated by commas. For example,
'pragma,translate_off,translate_on'

--map-keyword-version <keyword-version>+<file-pattern>[,...].

Indicates that any files used during parsing which match the given
patterns should be parsed using the provided language keywords
version, as if they contained a `begin_keywords directive. For example
'1364-2005+*.v,*.vh'

--allow-macro-trailing-space

If true, the preprocessor will allow trailing whitespaces after the
continuation character in a macro definition

--show-parsed-files

Print the name and kind of each file as it is parsed.

--allow-missing-protected-scope-end

If true, the preprocessor will assume that a missing end of scope
keyword for a module/program/package/class inside an include file with
protected code has the end of scope keyword inside the protected code.
This only works if the include file with protected code does not
include any other files.

--cmd-ignore <vendor_cmd>,<N>

Define rule to ignore vendor command <vendor_cmd> with its following
<N> parameters. A command of the form +xyz will also match any vendor
command of the form +xyz+abc, as +abc is the command's argument, and
doesn't need to be matched.

--cmd-rename <vendor_cmd>,<slang_cmd>

Define rule to rename vendor command <vendor_cmd> into existing
<slang_cmd>

--ignore-directive <directive>

Ignore preprocessor directive and all its arguments until EOL

--max-parse-depth <depth>

Maximum depth of nested language constructs allowed

--max-lexer-errors <count>

Maximum number of errors that can occur during lexing before the rest
of the file is skipped

-j,--threads <count>

The number of threads to use to parallelize parsing

-C <file-pattern>[,...]

One or more files containing independent compilation unit listings.
The files accept a subset of options that pertain specifically to
parsing that unit and optionally including it in a library.

--max-hierarchy-depth <depth>

Maximum depth of the design hierarchy

--max-generate-steps <steps>

Maximum number of steps that can occur during generate block
evaluation before giving up

--max-constexpr-depth <depth>

Maximum depth of a constant evaluation call stack

--max-constexpr-steps <steps>

Maximum number of steps that can occur during constant evaluation
before giving up

--max-constant-size <bits>

Maximum number of bits a single constant value can occupy during
constant evaluation before giving up

--constexpr-backtrace-limit <limit>

Maximum number of frames to show when printing a constant evaluation
backtrace; the rest will be abbreviated

--max-instance-array <limit>

Maximum number of instances allowed in a single instance array

--max-enum-values <limit>

Maximum number of members allowed in a single enum declaration

--max-udp-coverage-notes <limit>

Maximum number of UDP coverage notes that will be generated for a
single warning about missing edge transitions

--compat <mode>

Attempt to increase compatibility with the specified tool. Valid
options: 'default', 'vcs', 'all'

-T,--timing min|typ|max

Select which value to consider in min:typ:max expressions. Valid
options: 'min', 'typ', 'max'

--timescale <base>/<precision>

Default time scale to use for design elements that don't specify one
explicitly

--allow-use-before-declare

Don't issue an error for use of names before their declarations

--ignore-unknown-modules

Don't issue an error for instantiations of unknown modules, interface,
and programs

--relax-enum-conversions

Allow all integral types to convert implicitly to enum types

--relax-string-conversions

Allow string types to convert implicitly to integral types

--allow-hierarchical-const

Allow hierarchical references in constant expressions

--allow-toplevel-iface-ports

Allow top-level modules to have interface ports

--allow-recursive-implicit-call

Allow implicit call expressions to be recursive function calls

--allow-bare-value-param-assigment

Allow module parameter assignments to elide the parentheses

--allow-self-determined-stream-concat

Allow self-determined streaming concatenation expressions

--allow-merging-ansi-ports

Allow merging ANSI port declarations with nets and variables declared
in the instance body

--lint-only

Only perform linting of code, don't try to elaborate a full hierarchy

--disable-instance-caching

Disable the use of instance caching, which normally allows skipping
duplicate instance bodies to save time when elaborating

--disallow-refs-to-unknown-instances

When using --ignore-unknown-modules, explicitly disallow references to
ignored module instances by issuing an error

--allow-genblk-reference

Allow references to unnamed generate blocks via their external names
(e.g. genblk1)

--allow-virtual-iface-with-override

Allow interface instances that are bind/defparam targets to be
assigned to virtual interfaces

--allow-array-concat-assign-pattern

Allow assignment pattern expressions to be used in unpacked array
concatenations. The LRM states that these are not assignment-like
contexts but some tools allow it anyway.

--allow-lib-module-redef

Allow multiple definitions of the same module, interface, program, or
primitive at the root scope within the same library when the
conflicting definition comes from a library file (-v / --libfile); the
first definition is kept and subsequent library-file redefinitions are
silently discarded

--allow-cross-auto-bin-max

Allow the legacy SystemVerilog 3.1a cross_auto_bin_max coverage option
to be set on covergroups and crosses. The option is accepted and
ignored.

--infer-input-ports-as-vars

Infer ANSI input ports that have an explicit data type as variables
instead of nets. By default such ports are treated as nets, following
the LRM.

--top <name>

One or more top-level modules to instantiate (instead of figuring it
out automatically)

-G <name>=<value>

One or more parameter overrides to apply when instantiating top-level
modules

-L <library>

A list of library names that controls the priority order for module
lookup

--defaultLibName <name>

Sets the name of the default library

--define-system-task <prototype>

Define a custom system task or function. The subroutine name must
start with '$'. Optionally include a port list and, for functions, a
return type using standard SystemVerilog syntax (e.g. 'function int
$my_func(int a, string b)'). If neither a port list nor a return type
is specified the subroutine accepts any number of arguments and is
treated as a task.

-W <warning>

Control the specified warning

--waiver-file <file>

Path to TOML file containing diagnostic waiver rules (repeatable)

--color-diagnostics

Always print diagnostics in color. If this option is unset, colors
will be enabled if a color-capable terminal is detected.

--diag-column

Show column numbers in diagnostic output

--diag-column-unit <unit>

Unit for column numbers in diagnostics. Valid options: 'byte',
'display'

--diag-location

Show location information in diagnostic output

--diag-source

Show source line or caret info in diagnostic output

--diag-option

Show option names in diagnostic output

--diag-include-stack

Show include stacks in diagnostic output

--diag-macro-expansion

Show macro expansion backtraces in diagnostic output

--diag-abs-paths

Display absolute paths to files in diagnostic output

--diag-hierarchy always|never|auto

Show hierarchy locations in diagnostic output. Valid options: 'auto',
'always', 'never'

--print-unused-waivers

Print detailed information about unused diagnostic waivers

--diag-json <file>

Dump all diagnostics in JSON format to the specified file, or '-' for
stdout

--error-limit <limit>

Limit on the number of errors that will be printed. Setting this to
zero will disable the limit.

--suppress-warnings <file-pattern>[,...]

One or more paths in which to suppress warnings

--suppress-macro-warnings <file-pattern>[,...]

One or more paths in which to suppress warnings that originate in
macro expansions

--single-unit

Treat all input files as a single compilation unit

-v,--libfile <file-pattern>[,...]

One or more library files, which are separate compilation units where
modules are not automatically instantiated

--libmap <file-pattern>[,...]

One or more library map files to parse for library name mappings and
file lists

-y,--libdir <dir-pattern>[,...]

Library search paths, which will be searched for missing modules

--dir-prefix <prefix>

Directory prefix to prepend to source file paths when the file is not
found at the listed path. Multiple prefixes are tried in the order
they are specified. Must be specified before the source files that may
need it.

-Y,--libext,+libext <ext>

Additional library file extensions to search

--exclude-ext <ext>

Exclude provided source files with these extensions

-f <file-pattern>[,...]

One or more command files containing additional program options. Paths
in the file are considered relative to the current directory.

-F <file-pattern>[,...]

One or more command files containing additional program options. Paths
in the file are considered relative to the file itself.

--depfile-target

Output depfile lists in makefile format, creating the file with
`<target>:` as the make target

--Mall,--all-deps <file>

Generate dependency file list of all files used during parsing

--Minclude,--include-deps <file>

Generate dependency file list of just include files that were used
during parsing

--Mmodule,--module-deps <file>

Generate dependency file list of source files parsed, excluding
include files

--depfile-trim

Trim unreferenced files before generating dependency lists (also
implies --depfile-sort)

--depfile-sort

Topologically sort the emitted files in dependency lists

--dfa-unique-priority

Respect the 'unique' and 'priority' keywords when analyzing data flow
through case statements

--dfa-four-state

Require that case items cover X and Z bits to assume full coverage in
data flow analysis

--allow-multi-driven-locals

Allow subroutine local variables to be driven from multiple
always_comb/_ff blocks

--allow-dup-initial-drivers

Allow signals driven in an always_comb or always_ff block to also be
driven by initial blocks

--max-case-analysis-steps <steps>

Maximum number of steps that can occur during case analysis before
giving up

--max-loop-analysis-steps <steps>

Maximum number of steps that can occur during loop analysis before
giving up

--dump-ast

Dump the AST

--no-proc

Disable lowering of processes

--keep-hierarchy

Keep hierarchy (experimental; may crash)

--best-effort-hierarchy

Keep hierarchy in a 'best effort' mode

--ignore-timing

Ignore delays for synthesis

--ignore-initial

Ignore initial blocks for synthesis

--ignore-assertions

Ignore assertions and formal statements in input

--unroll-limit <limit>

Set unrolling limit (default: 4000)

--no-implicit-memories

Disable implicit memory inference. Without this option used, all
variables with at least one unpacked dimension are candidates for
memory inference. With this option used, inference will be restricted
to those variables annotated with one of the following memory style
attributes: ram_block, rom_block, ram_style, rom_style, ramstyle,
romstyle, syn_ramstyle, syn_romstyle

--empty-blackboxes

Assume empty modules are blackboxes

--ast-compilation-only

For developers: stop after the AST is fully compiled

--no-default-translate-off-format

Do not interpret any comment directives marking disabled input unless
specified with '--translate-off-format'

--allow-dual-edge-ff

Allow synthesis of dual-edge flip-flops (@(edge))

--no-synthesis-define

Don't add implicit -D SYNTHESIS

--blackboxed-module

Mark the named module for blackboxing. Whenever an instance of the
given module is found in the designhierarchy, its content will not be
elaborated and instead the instance will be imported as a black box.

--udp-handling

Set the processing mode for user defined primitives. When set to
'blackboxes' the UDP is treated as a blackboxed instance. When set to
'error', an error is emitted if a UDP is encountered. By default, the
frontend emits an error.. Valid options: 'error', 'blackboxes'

--compat-mode

Deprecated option which is effectively always on. The old help message
was "Be relaxed about the synthesis semantics of some language
constructs"

--extern-modules

Deprecated option which is effectively always on. The old help message
was "Import as an instantiable blackbox any module which was
previously loaded into the current design with a Yosys command; this
allows composing hierarchy of SystemVerilog and non-SystemVerilog
modules"

Note

Help text automatically generated from frontends/slang/lib/src/slang_frontend.cc:3550

read_verilog - read modules from Verilog file¶

yosys> help read_verilog¶

read_verilog [options] [filename]¶

Load modules from a Verilog file to the current design. A large subset of
Verilog-2005 is supported.

-sv

enable support for SystemVerilog features. (only a small subset
of SystemVerilog is supported)

-formal

enable support for SystemVerilog assertions and some Yosys extensions
replace the implicit -D SYNTHESIS with -D FORMAL

-nosynthesis

don't add implicit -D SYNTHESIS

-noassert

ignore assert() statements

-noassume

ignore assume() statements

-norestrict

ignore restrict() statements

-assume-asserts

treat all assert() statements like assume() statements

-assert-assumes

treat all assume() statements like assert() statements

-nodisplay

suppress output from display system tasks ($display et. al).
This does not affect the output from a later 'sim' command.

-debug

alias for -dump_ast1 -dump_ast2 -dump_vlog1 -dump_vlog2 -yydebug

-dump_ast1

dump abstract syntax tree (before simplification)

-dump_ast2

dump abstract syntax tree (after simplification)

-no_dump_ptr

do not include hex memory addresses in dump (easier to diff dumps)

-dump_vlog1

dump ast as Verilog code (before simplification)

-dump_vlog2

dump ast as Verilog code (after simplification)

-dump_rtlil

dump generated RTLIL netlist

-yydebug

enable parser debug output

-nolatches

usually latches are synthesized into logic loops
this option prohibits this and sets the output to 'x'
in what would be the latches hold condition

this behavior can also be achieved by setting the
'nolatches' attribute on the respective module or
always block.

-nomem2reg

under certain conditions memories are converted to registers
early during simplification to ensure correct handling of
complex corner cases. this option disables this behavior.

this can also be achieved by setting the 'nomem2reg'
attribute on the respective module or register.

This is potentially dangerous. Usually the front-end has good
reasons for converting an array to a list of registers.
Prohibiting this step will likely result in incorrect synthesis
results.

-mem2reg

always convert memories to registers. this can also be
achieved by setting the 'mem2reg' attribute on the respective
module or register.

-nomeminit

do not infer $meminit cells and instead convert initialized
memories to registers directly in the front-end.

-ppdump

dump Verilog code after pre-processor

-nopp

do not run the pre-processor

-nodpi

disable DPI-C support

-noblackbox

do not automatically add a (* blackbox *) attribute to an
empty module.

-lib

only create empty blackbox modules. This implies -DBLACKBOX.
modules with the (* whitebox *) attribute will be preserved.
(* lib_whitebox *) will be treated like (* whitebox *).

-nowb

delete (* whitebox *) and (* lib_whitebox *) attributes from
all modules.

-specify

parse and import specify blocks

-noopt

don't perform basic optimizations (such as const folding) in the
high-level front-end.

-icells

interpret cell types starting with '$' as internal cell types

-pwires

add a wire for each module parameter

-nooverwrite

ignore re-definitions of modules. (the default behavior is to
create an error message if the existing module is not a black box
module, and overwrite the existing module otherwise.)

-overwrite

overwrite existing modules with the same name

-defer

only read the abstract syntax tree and defer actual compilation
to a later 'hierarchy' command. Useful in cases where the default
parameters of modules yield invalid or not synthesizable code.

-noautowire

make the default of `default_nettype be "none" instead of "wire".

-setattr <attribute_name>

set the specified attribute (to the value 1) on all loaded modules

-Dname[=definition]

define the preprocessor symbol 'name' and set its optional value
'definition'

-Idir

add 'dir' to the directories which are used when searching include
files

-relativeshare

use paths relative to share directory for source locations
where possible (experimental).

The command 'verilog_defaults' can be used to register default options for
subsequent calls to 'read_verilog'.

Note that the Verilog frontend does a pretty good job of processing valid
verilog input, but has not very good error reporting. It generally is
recommended to use a simulator (for example Icarus Verilog) for checking
the syntax of the code, rather than to rely on read_verilog for that.

Depending on if read_verilog is run in -formal mode, either the macro
SYNTHESIS or FORMAL is defined automatically, unless -nosynthesis is used.
In addition, read_verilog always defines the macro YOSYS.

See the Yosys README file for a list of non-standard Verilog features
supported by the Yosys Verilog front-end.

Note

Help text automatically generated from frontends/verilog/verilog_frontend.cc:73

read_verilog_file_list - parse a Verilog file list¶

yosys> help read_verilog_file_list¶

read_verilog_file_list [options]¶

Parse a Verilog file list, and pass the list of Verilog files to read_verilog
command

-F file_list_path

File list file contains list of Verilog files to be parsed, any path is
treated relative to the file list file

-f file_list_path

File list file contains list of Verilog files to be parsed, any path is
treated relative to current working directroy

Note

Help text automatically generated from frontends/verilog/verilog_frontend.cc:747

read_xaiger2 - (experimental) read XAIGER file¶

yosys> help read_xaiger2¶

Warning

This command is experimental

read_xaiger2 -sc_mapping [options] <filename>¶

Read a standard cell mapping from a XAIGER file into an existing module.

-module_name <name>

name of the target module

-map2 <filename>

read file with symbol information

Note

Help text automatically generated from frontends/aiger2/xaiger.cc:41

slang_defaults - set default options for read_slang¶

yosys> help slang_defaults¶

slang_defaults -add [options]¶

Add default options for subsequent calls to read_slang.

slang_defaults -clear¶

Clear the list of default options to read_slang.

slang_defaults -push¶

slang_defaults -pop¶

Push or pop the default option list to a stack. On -push the list isn't cleared.

Note

Help text automatically generated from frontends/slang/lib/src/slang_frontend.cc:3838

slang_version - display revision of slang frontend¶

yosys> help slang_version¶

slang_version¶

Display git revisions of the slang frontend.

Note

Help text automatically generated from frontends/slang/lib/src/slang_frontend.cc:3450

test_slangdiag - test diagnostics emission by the slang frontend¶

yosys> help test_slangdiag¶

Perform internal test of the slang frontend.

Note

Help text automatically generated from frontends/slang/lib/src/slang_frontend.cc:3893

test_slangexpr - test expression evaluation within slang frontend¶

yosys> help test_slangexpr¶

Perform internal test of the slang frontend.

Note

Help text automatically generated from frontends/slang/lib/src/slang_frontend.cc:3943

verific - load Verilog and VHDL designs using Verific¶

yosys> help verific¶

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

Load the specified Verilog/SystemVerilog files into Verific.
Note that -sv option will use latest supported SystemVerilog standard.

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|-vhdl2019|-vhdl} <vhdl-file>..¶

Load the specified VHDL files into Verific.

verific {-edif} <edif-file>..¶

Load the specified EDIF files into Verific.

verific {-liberty} <liberty-file>..¶

Load the specified Liberty files into Verific.
Default library when -work is not present is one specified in liberty file.
To use from SystemVerilog or VHDL use -L to specify liberty library.

-lib

only create empty blackbox modules

verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl2019|-vhdl|-sv2012|-sv2017|-sv|-formal] <command-file>¶

Load and execute the specified command file.
Override verilog parsing mode can be set.
The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.

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

    analysis mode:
        -ams
        +v2k
        -sverilog

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-libext <extension>..¶

Add Verilog library extensions, used when searching in library directories.

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.
Also errors, warnings, infos and comments could be used to set new severity for
all messages of certain type.

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

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

Import options:

-all

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

-gates

Create a gate-level netlist.

-flatten

Flatten the design in Verific before importing.

-extnets

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

-no-split-complex-ports

Complex ports (structs or arrays) are not split and remain packed as a single port.

-autocover

Generate automatic cover statements for all asserts

-fullinit

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

-cells

Import all cell definitions from Verific loaded libraries even if they are
unused in design. Useful with "-edif" and "-liberty" option.

-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.)

-pp <filename>

Pretty print design after elaboration to specified file.

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

-k

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.

-V

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

-nosva

Ignore SVA properties, do not infer checker logic.

-sva-continue-on-err

Turns unsupported SVA from an error into a warning. Properties are imported
with their trigger condition replaced with 'x and with an `unsupported_sva'
attribute to produce a later error in SBY if they remain in the design.

-L <int>

Maximum number of ctrl bits for SVA checker FSMs (default=16).

-n

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:

-verilog

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

-vhdl

Save output for VHDL design units.

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

Get/set Verific runtime flags.

verific -assert-all-invariants¶

Executes code rewriter to assert all invariants.

verific -assert-used-properties-and-sequences¶

Executes code rewriter to assert all properties and sequences used in proofs.

verific -delete-all-invariants¶

Executes code rewriter to delete all invariants.

verific -delete-all-proofs¶

Executes code rewriter to delete all proofs.

verific [-work <libname>] -elaborate [options]..¶

Execute elaboration step and all registered rewriters.

-work <libname>

Use verilog sources from given library.
(default library when -work is not present: "work")

verific [-work <libname>] -ivy-json-export <filename> [options]..

Export IVY specific data to json file.

-work <libname>

Use verilog sources from given library.
(default library when -work is not present: "work")

-top <top>

Specify top module.

verific [-work <libname>] -rewrite [-clear][-list] <name> [options]..¶

Register rewriter for execution on elaboration step.

-help

Displays help for specific rewriter.

-clear

Remove all rewriters from list, including default rewriters.

-list

Displays all rewriter in list in order of execution.

-module <module>

Run rewriter only on specified module.

-work <libname>

Use verilog sources from given library.
(default library when -work is not present: "work")

-blacklist <filename[:lineno]>

Do not run rewriter 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 rewriter on locations specified in file, they can
represent filename or filename and location in file.

-whitelist <filename[:lineno]>

Run rewriter 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.

-wlfile <file>

Run rewriter on locations specified in file, they can
represent filename or filename and location in file.

Available rewriters:
  bound-check          - Generate array out-of-bounds checks
  clear-formal         - Removes formal related AST
  gen-witness-covers   - Generate witness covers
  initial-assertions   - Generate initial block assertions (automatically added)
  remove-initial       - Remove initial blocks

Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.
https://www.yosyshq.com/

Contact office@yosyshq.com for free evaluation
binaries of YosysHQ Tabby CAD Suite.

Note

Help text automatically generated from frontends/verific/verific.cc:3168

verilog_defaults - set default options for read_verilog¶

yosys> help verilog_defaults¶

verilog_defaults -add [options]¶

Add the specified options to the list of default options to read_verilog.

verilog_defaults -clear¶

Clear the list of Verilog default options.

verilog_defaults -push¶

verilog_defaults -pop¶

Push or pop the list of default options to a stack. Note that -push does
not imply -clear.

Note

Help text automatically generated from frontends/verilog/verilog_frontend.cc:579

verilog_defines - define and undefine verilog defines¶

yosys> help verilog_defines¶

verilog_defines [options]¶

Define and undefine verilog preprocessor macros.

-Dname[=definition]

define the preprocessor symbol 'name' and set its optional value
'definition'

-Uname[=definition]

undefine the preprocessor symbol 'name'

-reset

clear list of defined preprocessor symbols

-list

list currently defined preprocessor symbols

Note

Help text automatically generated from frontends/verilog/verilog_frontend.cc:637