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:4342

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:981

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:628

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:623

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:432

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

Note

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

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:75

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:752

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

verific - load Verilog and VHDL designs using Verific¶

yosys> help 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|-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|-sv2012|-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:3106

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:582

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:640