summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.github/issue_template.md2
-rw-r--r--Makefile2
-rw-r--r--backends/edif/edif.cc39
-rw-r--r--frontends/ast/genrtlil.cc3
-rw-r--r--frontends/ast/simplify.cc5
-rw-r--r--frontends/verific/verific.cc18
-rw-r--r--frontends/verilog/verilog_frontend.cc23
-rw-r--r--frontends/verilog/verilog_frontend.h9
-rw-r--r--frontends/verilog/verilog_parser.y35
-rw-r--r--kernel/celltypes.h2
-rw-r--r--manual/command-reference-manual.tex1340
-rw-r--r--techlibs/ecp5/dram.txt1
-rw-r--r--techlibs/xilinx/cells_xtra.sh4
-rw-r--r--techlibs/xilinx/cells_xtra.v13
14 files changed, 1229 insertions, 267 deletions
diff --git a/.github/issue_template.md b/.github/issue_template.md
index 4563a71d..24e91a4e 100644
--- a/.github/issue_template.md
+++ b/.github/issue_template.md
@@ -1,7 +1,7 @@
## Steps to reproduce the issue
*Provide instructions for reproducing the issue. Make sure to include
-all necessary source files. (You can simply drag&drop a .zip file into
+all neccessary source files. (You can simply drag&drop a .zip file into
the issue editor.)*
## Expected behavior
diff --git a/Makefile b/Makefile
index 365b92ea..d759b114 100644
--- a/Makefile
+++ b/Makefile
@@ -99,7 +99,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.7+$(shell cd $(YOSYS_SRC) && test -e .git && { git log --author=clifford@clifford.at --oneline 61f6811.. | wc -l; })
+YOSYS_VER := 0.8
GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
OBJS = kernel/version_$(GIT_REV).o
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index d4e56a9e..5f9ec54f 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -106,9 +106,6 @@ struct EdifBackend : public Backend {
log(" if the design contains constant nets. use \"hilomap\" to map to custom\n");
log(" constant drivers first)\n");
log("\n");
- log(" -attrprop\n");
- log(" create EDIF properties for cell attributes\n");
- log("\n");
log(" -pvector {par|bra|ang}\n");
log(" sets the delimiting character for module port rename clauses to\n");
log(" parentheses, square brackets, or angle brackets.\n");
@@ -124,7 +121,6 @@ struct EdifBackend : public Backend {
log_header(design, "Executing EDIF backend.\n");
std::string top_module_name;
bool port_rename = false;
- bool attr_properties = false;
std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
bool nogndvcc = false;
CellTypes ct(design);
@@ -141,10 +137,6 @@ struct EdifBackend : public Backend {
nogndvcc = true;
continue;
}
- if (args[argidx] == "-attrprop") {
- attr_properties = true;
- continue;
- }
if (args[argidx] == "-pvector" && argidx+1 < args.size()) {
std::string parray;
port_rename = true;
@@ -340,33 +332,24 @@ struct EdifBackend : public Backend {
*f << stringf(" (instance %s\n", EDIF_DEF(cell->name));
*f << stringf(" (viewRef VIEW_NETLIST (cellRef %s%s))", EDIF_REF(cell->type),
lib_cell_ports.count(cell->type) > 0 ? " (libraryRef LIB)" : "");
-
- auto add_prop = [&](IdString name, Const val) {
- if ((val.flags & RTLIL::CONST_FLAG_STRING) != 0)
- *f << stringf("\n (property %s (string \"%s\"))", EDIF_DEF(name), val.decode_string().c_str());
- else if (val.bits.size() <= 32 && RTLIL::SigSpec(val).is_fully_def())
- *f << stringf("\n (property %s (integer %u))", EDIF_DEF(name), val.as_int());
+ for (auto &p : cell->parameters)
+ if ((p.second.flags & RTLIL::CONST_FLAG_STRING) != 0)
+ *f << stringf("\n (property %s (string \"%s\"))", EDIF_DEF(p.first), p.second.decode_string().c_str());
+ else if (p.second.bits.size() <= 32 && RTLIL::SigSpec(p.second).is_fully_def())
+ *f << stringf("\n (property %s (integer %u))", EDIF_DEF(p.first), p.second.as_int());
else {
std::string hex_string = "";
- for (size_t i = 0; i < val.bits.size(); i += 4) {
+ for (size_t i = 0; i < p.second.bits.size(); i += 4) {
int digit_value = 0;
- if (i+0 < val.bits.size() && val.bits.at(i+0) == RTLIL::State::S1) digit_value |= 1;
- if (i+1 < val.bits.size() && val.bits.at(i+1) == RTLIL::State::S1) digit_value |= 2;
- if (i+2 < val.bits.size() && val.bits.at(i+2) == RTLIL::State::S1) digit_value |= 4;
- if (i+3 < val.bits.size() && val.bits.at(i+3) == RTLIL::State::S1) digit_value |= 8;
+ if (i+0 < p.second.bits.size() && p.second.bits.at(i+0) == RTLIL::State::S1) digit_value |= 1;
+ if (i+1 < p.second.bits.size() && p.second.bits.at(i+1) == RTLIL::State::S1) digit_value |= 2;
+ if (i+2 < p.second.bits.size() && p.second.bits.at(i+2) == RTLIL::State::S1) digit_value |= 4;
+ if (i+3 < p.second.bits.size() && p.second.bits.at(i+3) == RTLIL::State::S1) digit_value |= 8;
char digit_str[2] = { "0123456789abcdef"[digit_value], 0 };
hex_string = std::string(digit_str) + hex_string;
}
- *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(name), GetSize(val.bits), hex_string.c_str());
+ *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(p.first), GetSize(p.second.bits), hex_string.c_str());
}
- };
-
- for (auto &p : cell->parameters)
- add_prop(p.first, p.second);
- if (attr_properties)
- for (auto &p : cell->attributes)
- add_prop(p.first, p.second);
-
*f << stringf(")\n");
for (auto &p : cell->connections()) {
RTLIL::SigSpec sig = sigmap(p.second);
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index c9345ff0..0f7e910f 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -985,8 +985,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
use_const_chunk:
if (children.size() != 0) {
- if (children[0]->type != AST_RANGE)
- log_file_error(filename, linenum, "Single range expected.\n");
+ log_assert(children[0]->type == AST_RANGE);
int source_width = id2ast->range_left - id2ast->range_right + 1;
int source_offset = id2ast->range_right;
if (!children[0]->range_valid) {
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 71eba547..aa3b982d 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1836,7 +1836,7 @@ skip_dynamic_range_lvalue_expansion:;
goto apply_newNode;
}
- if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell" || str == "\\$changed")
+ if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell")
{
if (GetSize(children) != 1)
log_file_error(filename, linenum, "System function %s got %d arguments, expected 1.\n",
@@ -1853,9 +1853,6 @@ skip_dynamic_range_lvalue_expansion:;
if (str == "\\$stable")
newNode = new AstNode(AST_EQ, past, present);
- else if (str == "\\$changed")
- newNode = new AstNode(AST_NE, past, present);
-
else if (str == "\\$rose")
newNode = new AstNode(AST_LOGIC_AND, new AstNode(AST_LOGIC_NOT, past), present);
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index dba3b0f0..c5fa5831 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -118,18 +118,6 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
return net_map.at(net);
}
-bool is_blackbox(Netlist *nl)
-{
- if (nl->IsBlackBox())
- return true;
-
- const char *attr = nl->GetAttValue("blackbox");
- if (attr != nullptr && strcmp(attr, "0"))
- return true;
-
- return false;
-}
-
void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
{
MapIter mi;
@@ -721,7 +709,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
netlist = nl;
if (design->has(module_name)) {
- if (!nl->IsOperator() && !is_blackbox(nl))
+ if (!nl->IsOperator())
log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
return;
}
@@ -730,7 +718,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
module->name = module_name;
design->add(module);
- if (is_blackbox(nl)) {
+ if (nl->IsBlackBox()) {
log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
module->set_bool_attribute("\\blackbox");
} else {
@@ -1688,7 +1676,6 @@ YOSYS_NAMESPACE_END
PRIVATE_NAMESPACE_BEGIN
-#ifdef YOSYS_ENABLE_VERIFIC
bool check_noverific_env()
{
const char *e = getenv("YOSYS_NOVERIFIC");
@@ -1698,7 +1685,6 @@ bool check_noverific_env()
return false;
return true;
}
-#endif
struct VerificPass : public Pass {
VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index aeea36a2..8dcc7c5a 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -66,21 +66,12 @@ struct VerilogFrontend : public Frontend {
log(" enable support for SystemVerilog assertions and some Yosys extensions\n");
log(" replace the implicit -D SYNTHESIS with -D FORMAL\n");
log("\n");
- log(" -noassert\n");
- log(" ignore assert() statements\n");
- log("\n");
- log(" -noassume\n");
- log(" ignore assume() statements\n");
- log("\n");
log(" -norestrict\n");
- log(" ignore restrict() statements\n");
+ log(" ignore restrict() assertions\n");
log("\n");
log(" -assume-asserts\n");
log(" treat all assert() statements like assume() statements\n");
log("\n");
- log(" -assert-assumes\n");
- log(" treat all assume() statements like assert() statements\n");
- log("\n");
log(" -dump_ast1\n");
log(" dump abstract syntax tree (before simplification)\n");
log("\n");
@@ -238,14 +229,6 @@ struct VerilogFrontend : public Frontend {
formal_mode = true;
continue;
}
- if (arg == "-noassert") {
- noassert_mode = true;
- continue;
- }
- if (arg == "-noassume") {
- noassume_mode = true;
- continue;
- }
if (arg == "-norestrict") {
norestrict_mode = true;
continue;
@@ -254,10 +237,6 @@ struct VerilogFrontend : public Frontend {
assume_asserts_mode = true;
continue;
}
- if (arg == "-assert-assumes") {
- assert_assumes_mode = true;
- continue;
- }
if (arg == "-dump_ast1") {
flag_dump_ast1 = true;
continue;
diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index 523bbc89..16edc798 100644
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -54,21 +54,12 @@ namespace VERILOG_FRONTEND
// running in -formal mode
extern bool formal_mode;
- // running in -noassert mode
- extern bool noassert_mode;
-
- // running in -noassume mode
- extern bool noassume_mode;
-
// running in -norestrict mode
extern bool norestrict_mode;
// running in -assume-asserts mode
extern bool assume_asserts_mode;
- // running in -assert-assumes mode
- extern bool assert_assumes_mode;
-
// running in -lib mode
extern bool lib_mode;
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 16cac146..2389d7d3 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -58,8 +58,7 @@ namespace VERILOG_FRONTEND {
bool do_not_require_port_stubs;
bool default_nettype_wire;
bool sv_mode, formal_mode, lib_mode;
- bool noassert_mode, noassume_mode, norestrict_mode;
- bool assume_asserts_mode, assert_assumes_mode;
+ bool norestrict_mode, assume_asserts_mode;
bool current_wire_rand, current_wire_const;
std::istream *lexin;
}
@@ -882,15 +881,9 @@ param_decl_list:
single_param_decl:
TOK_ID '=' expr {
- AstNode *node;
- if (astbuf1 == nullptr) {
- if (!sv_mode)
- frontend_verilog_yyerror("syntax error");
- node = new AstNode(AST_PARAMETER);
- node->children.push_back(AstNode::mkconst_int(0, true));
- } else {
- node = astbuf1->clone();
- }
+ if (astbuf1 == nullptr)
+ frontend_verilog_yyerror("syntax error");
+ AstNode *node = astbuf1->clone();
node->str = *$1;
delete node->children[0];
node->children[0] = $3;
@@ -1282,28 +1275,16 @@ opt_stmt_label:
assert:
opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
- if (noassert_mode)
- delete $5;
- else
- ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+ ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
} |
opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
- if (noassume_mode)
- delete $5;
- else
- ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
+ ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
} |
opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
- if (noassert_mode)
- delete $6;
- else
- ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+ ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
} |
opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
- if (noassume_mode)
- delete $6;
- else
- ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
+ ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
} |
opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 6041168b..fcc4fcc4 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -157,7 +157,7 @@ struct CellTypes
IdString A = "\\A", B = "\\B", C = "\\C", D = "\\D";
IdString E = "\\E", F = "\\F", G = "\\G", H = "\\H";
IdString I = "\\I", J = "\\J", K = "\\K", L = "\\L";
- IdString M = "\\M", N = "\\N", O = "\\O", P = "\\P";
+ IdString M = "\\I", N = "\\N", O = "\\O", P = "\\P";
IdString S = "\\S", T = "\\T", U = "\\U", V = "\\V";
IdString Y = "\\Y";
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index fea2354e..bed6326e 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -23,45 +23,47 @@ library to a target architecture.
if no -script parameter is given, the following scripts are used:
for -liberty without -constr:
- strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f;
- map {D}
+ strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
+ &nf {D}; &put
for -liberty with -constr:
- strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f;
- map {D}; buffer; upsize {D}; dnsize {D}; stime -p
+ strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
+ &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p
for -lut/-luts (only one LUT size):
- strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs;
- lutpack
+ strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2;
+ lutpack {S}
for -lut/-luts (different LUT sizes):
- strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs
+ strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2
for -sop:
- strash; dc2; scorr; ifraig; retime -o; strash; dch -f;
+ strash; ifraig; scorr; dc2; dretime; strash; dch -f;
cover {I} {P}
otherwise:
- strash; dc2; scorr; ifraig; retime -o; strash; dch -f; map
+ strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f;
+ &nf {D}; &put
-fast
use different default scripts that are slightly faster (at the cost
of output quality):
for -liberty without -constr:
- retime -o {D}; map {D}
+ strash; dretime; map {D}
for -liberty with -constr:
- retime -o {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p
+ strash; dretime; map {D}; buffer; upsize {D}; dnsize {D};
+ stime -p
for -lut/-luts:
- retime -o; if
+ strash; dretime; if
for -sop:
- retime -o; cover -I {I} -P {P}
+ strash; dretime; cover -I {I} -P {P}
otherwise:
- retime -o; map
+ strash; dretime; map
-liberty <file>
generate netlists for the specified cell library (using the liberty
@@ -81,6 +83,8 @@ library to a target architecture.
-D <picoseconds>
set delay target. the string {D} in the default scripts above is
replaced by this option when used, and an empty string otherwise.
+ this also replaces 'dretime' with 'dretime; retime -o {D}' in the
+ default scripts above.
-I <num>
maximum number of SOP inputs.
@@ -90,6 +94,10 @@ library to a target architecture.
maximum number of SOP products.
(replaces {P} in the default scripts above)
+ -S <num>
+ maximum number of LUT inputs shared.
+ (replaces {S} in the default scripts above, default: -S 1)
+
-lut <width>
generate netlist using luts of (max) the specified width.
@@ -107,10 +115,21 @@ library to a target architecture.
map to sum-of-product cells and inverters
-g type1,type2,...
- Map the the specified list of gate types. Supported gates types are:
- AND, NAND, OR, NOR, XOR, XNOR, MUX, AOI3, OAI3, AOI4, OAI4.
+ Map to the specified list of gate types. Supported gates types are:
+ AND, NAND, OR, NOR, XOR, XNOR, ANDNOT, ORNOT, MUX, AOI3, OAI3, AOI4, OAI4.
(The NOT gate is always added to this list automatically.)
+ The following aliases can be used to reference common sets of gate types:
+ simple: AND OR XOR MUX
+ cmos2: NAND NOR
+ cmos3: NAND NOR AOI3 OAI3
+ cmos4: NAND NOR AOI3 OAI3 AOI4 OAI4
+ gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT
+ aig: AND NAND OR NOR ANDNOT ORNOT
+
+ Prefix a gate type with a '-' to remove it from the list. For example
+ the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent.
+
-dff
also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many
clock domains are automatically partitioned in clock domains and each
@@ -140,8 +159,12 @@ library to a target architecture.
When neither -liberty nor -lut is used, the Yosys standard cell library is
loaded into ABC before the ABC script is executed.
-This pass does not operate on modules with unprocessed processes in it.
-(I.e. the 'proc' pass should be used first to convert processes to netlists.)
+Note that this is a logic optimization pass within Yosys that is calling ABC
+internally. This is not going to "run ABC on your design". It will instead run
+ABC on logic snippets extracted from your design. You will not get any useful
+output when passing an ABC script that writes a file. Instead write your full
+design as BLIF file with write_blif and the load that into ABC externally if
+you want to use ABC to convert your design into another format.
[1] http://www.eecs.berkeley.edu/~alanmi/abc/
\end{lstlisting}
@@ -206,6 +229,22 @@ This command adds asserts to the design that assert that all parallel muxes
additional constrained and check the $pmux condition always.
\end{lstlisting}
+\section{async2sync -- convert async FF inputs to sync circuits}
+\label{cmd:async2sync}
+\begin{lstlisting}[numbers=left,frame=single]
+ async2sync [options] [selection]
+
+This command replaces async FF inputs with sync circuits emulating the same
+behavior for when the async signals are actually synchronized to the clock.
+
+This pass assumes negative hold time for the async FF inputs. For example when
+a reset deasserts with the clock edge, then the FF output will still drive the
+reset value in the next cycle regardless of the data-in value at the time of
+the clock edge.
+
+Currently only $adff cells are supported by this pass.
+\end{lstlisting}
+
\section{attrmap -- renaming attributes}
\label{cmd:attrmap}
\begin{lstlisting}[numbers=left,frame=single]
@@ -268,6 +307,15 @@ Move or copy attributes on wires to the cells driving them.
multiple times.
\end{lstlisting}
+\section{blackbox -- change type of cells in the design}
+\label{cmd:blackbox}
+\begin{lstlisting}[numbers=left,frame=single]
+ blackbox [options] [selection]
+
+Convert modules into blackbox modules (remove contents and set the blackbox
+module attribute).
+\end{lstlisting}
+
\section{cd -- a shortcut for 'select -module <name>'}
\label{cmd:cd}
\begin{lstlisting}[numbers=left,frame=single]
@@ -284,6 +332,12 @@ to 'cd <celltype>'.
cd ..
+Remove trailing substrings that start with '.' in current module name until
+the name of a module in the current design is generated, then switch to that
+module. Otherwise clear the current selection.
+
+ cd
+
This is just a shortcut for 'select -clear'.
\end{lstlisting}
@@ -303,10 +357,49 @@ This pass identifies the following problems in the current design:
When called with -noinit then this command also checks for wires which have
the 'init' attribute set.
+When called with -initdrv then this command also checks for wires which have
+the 'init' attribute set and aren't driven by a FF cell type.
+
When called with -assert then the command will produce an error if any
problems are found in the current design.
\end{lstlisting}
+\section{chformal -- change formal constraints of the design}
+\label{cmd:chformal}
+\begin{lstlisting}[numbers=left,frame=single]
+ chformal [types] [mode] [options] [selection]
+
+Make changes to the formal constraints of the design. The [types] options
+the type of constraint to operate on. If none of the folling options is given,
+the command will operate on all constraint types:
+
+ -assert $assert cells, representing assert(...) constraints
+ -assume $assume cells, representing assume(...) constraints
+ -live $live cells, representing assert(s_eventually ...)
+ -fair $fair cells, representing assume(s_eventually ...)
+ -cover $cover cells, representing cover() statements
+
+Exactly one of the following modes must be specified:
+
+ -remove
+ remove the cells and thus constraints from the design
+
+ -early
+ bypass FFs that only delay the activation of a constraint
+
+ -delay <N>
+ delay activation of the constraint by <N> clock cycles
+
+ -skip <N>
+ ignore activation of the constraint in the first <N> clock cycles
+
+ -assert2assume
+ -assume2assert
+ -live2fair
+ -fair2live
+ change the roles of cells as indicated. this options can be combined
+\end{lstlisting}
+
\section{chparam -- re-evaluate modules with new parameters}
\label{cmd:chparam}
\begin{lstlisting}[numbers=left,frame=single]
@@ -321,6 +414,20 @@ passed in double quotes (").
List the available parameters of the selected modules.
\end{lstlisting}
+\section{chtype -- change type of cells in the design}
+\label{cmd:chtype}
+\begin{lstlisting}[numbers=left,frame=single]
+ chtype [options] [selection]
+
+Change the types of cells in the design.
+
+ -set <type>
+ set the cell type to the given type
+
+ -map <old_type> <new_type>
+ change cells types that match <old_type> to <new_type>
+\end{lstlisting}
+
\section{clean -- remove unused cells and wires}
\label{cmd:clean}
\begin{lstlisting}[numbers=left,frame=single]
@@ -376,7 +483,7 @@ be selected or an active module must be set using the 'cd' command.
This command does not operate on module with processes.
\end{lstlisting}
-\section{connwrappers -- replace undef values with defined constants}
+\section{connwrappers -- match width of input-output port pairs}
\label{cmd:connwrappers}
\begin{lstlisting}[numbers=left,frame=single]
connwrappers [options] [selection]
@@ -397,6 +504,14 @@ the driving cell.
The options -signed, -unsigned, and -port can be specified multiple times.
\end{lstlisting}
+\section{coolrunner2\_sop -- break \$sop cells into ANDTERM/ORTERM cells}
+\label{cmd:coolrunner2_sop}
+\begin{lstlisting}[numbers=left,frame=single]
+ coolrunner2_sop [options] [selection]
+
+Break $sop cells into ANDTERM/ORTERM cells.
+\end{lstlisting}
+
\section{copy -- copy modules in the design}
\label{cmd:copy}
\begin{lstlisting}[numbers=left,frame=single]
@@ -519,6 +634,19 @@ evaluated in the other design.
design -copy-to <name> [-as <new_mod_name>] [selection]
Copy modules from the current design into the specified one.
+
+
+ design -import <name> [-as <new_top_name>] [selection]
+
+Import the specified design into the current design. The source design must
+either have a selected top module or the selection must contain exactly one
+module that is then used as top module for this command.
+
+
+ design -reset-vlog
+
+The Verilog front-end remembers defined macros and top-level declarations
+between calls to 'read_verilog'. This command resets this memory.
\end{lstlisting}
\section{dff2dffe -- transform \$dff cells to \$dffe cells}
@@ -546,8 +674,18 @@ $_DFF_P_, $_DFF_N_ and $_MUX_.
-direct-match <pattern>
like -direct for all DFF cell types matching the expression.
this will use $__DFFE_* as <external_gate_type> matching the
- internal gate type $_DFF_*_, except for $_DFF_[NP]_, which is
- converted to $_DFFE_[NP]_.
+ internal gate type $_DFF_*_, and $__DFFSE_* for those matching
+ $_DFFS_*_, except for $_DFF_[NP]_, which is converted to
+ $_DFFE_[NP]_.
+\end{lstlisting}
+
+\section{dff2dffs -- process sync set/reset with SR over CE priority}
+\label{cmd:dff2dffs}
+\begin{lstlisting}[numbers=left,frame=single]
+ dff2dffs [options] [selection]
+
+Merge synchronous set/reset $_MUX_ cells to create $__DFFS_[NP][NP][01], to be run before
+dff2dffe for SR over CE priority.
\end{lstlisting}
\section{dffinit -- set INIT param on FF cells}
@@ -561,6 +699,11 @@ drives. (This is primarily used in FPGA flows.)
-ff <cell_name> <output_port> <init_param>
operate on the specified cell type. this option can be used
multiple times.
+
+ -highlow
+ use the string values "high" and "low" to represent a single-bit
+ initial value of 1 or 0. (multi-bit values are not supported in this
+ mode.)
\end{lstlisting}
\section{dfflibmap -- technology mapping of flip-flops}
@@ -767,6 +910,10 @@ This command tries to prove $equiv cells using a simple direct SAT approach.
-undef
enable modelling of undef states
+ -short
+ create shorter input cones that stop at shared nodes. This yields
+ simpler SAT problems but sometimes fails to prove equivalence.
+
-nogroup
disabling grouping of $equiv cells by output wire
@@ -852,6 +999,10 @@ outputs.
when exposing a wire, create an input/output pair and cut the internal
signal path at that wire.
+ -input
+ when exposing a wire, create an input port and disconnect the internal
+ driver.
+
-shared
only expose those signals that are shared among the selected modules.
this is useful for preparing modules for equivalence checking.
@@ -956,6 +1107,64 @@ tries to map the modules to the design (ascending, default value is 0).
See 'help techmap' for a pass that does the opposite thing.
\end{lstlisting}
+\section{extract\_counter -- Extract GreenPak4 counter cells}
+\label{cmd:extract_counter}
+\begin{lstlisting}[numbers=left,frame=single]
+ extract_counter [options] [selection]
+
+This pass converts non-resettable or async resettable down counters to
+counter cells. Use a target-specific 'techmap' map file to convert those cells
+to the actual target cells.
+
+ -maxwidth N
+ Only extract counters up to N bits wide
+
+ -pout X,Y,...
+ Only allow parallel output from the counter to the listed cell types
+ (if not specified, parallel outputs are not restricted)
+\end{lstlisting}
+
+\section{extract\_fa -- find and extract full/half adders}
+\label{cmd:extract_fa}
+\begin{lstlisting}[numbers=left,frame=single]
+ extract_fa [options] [selection]
+
+This pass extracts full/half adders from a gate-level design.
+
+ -fa, -ha
+ Enable cell types (fa=full adder, ha=half adder)
+ All types are enabled if none of this options is used
+
+ -d <int>
+ Set maximum depth for extracted logic cones (default=20)
+
+ -b <int>
+ Set maximum breadth for extracted logic cones (default=6)
+
+ -v
+ Verbose output
+\end{lstlisting}
+
+\section{extract\_reduce -- converts gate chains into \$reduce\_* cells}
+\label{cmd:extract_reduce}
+\begin{lstlisting}[numbers=left,frame=single]
+ extract_reduce [options] [selection]
+
+converts gate chains into $reduce_* cells
+
+This command finds chains of $_AND_, $_OR_, and $_XOR_ cells and replaces them
+with their corresponding $reduce_* cells. Because this command only operates on
+these cell types, it is recommended to map the design to only these cell types
+using the `abc -g` command. Note that, in some cases, it may be more effective
+to map the design to only $_AND_ cells, run extract_reduce, map the remaining
+parts of the design to AND/OR/XOR cells, and run extract_reduce a second time.
+
+ -allow-off-chain
+ Allows matching of cells that have loads outside the chain. These cells
+ will be replicated and folded into the $reduce_* cell, but the original
+ cell will remain, driving its original loads.
+\end{lstlisting}
+
\section{flatten -- flatten design}
\label{cmd:flatten}
\begin{lstlisting}[numbers=left,frame=single]
@@ -1155,21 +1364,12 @@ one-hot encoding and binary encoding is supported.
.map <old_bitpattern> <new_bitpattern>
\end{lstlisting}
-\section{greenpak4\_counters -- Extract GreenPak4 counter cells}
-\label{cmd:greenpak4_counters}
-\begin{lstlisting}[numbers=left,frame=single]
- greenpak4_counters [options] [selection]
-
-This pass converts non-resettable or async resettable down counters to GreenPak4
-counter cells (All other GreenPak4 counter modes must be instantiated manually.)
-\end{lstlisting}
-
-\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFFs}
+\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFF/latches}
\label{cmd:greenpak4_dffinv}
\begin{lstlisting}[numbers=left,frame=single]
greenpak4_dffinv [options] [selection]
-Merge GP_INV cells with GP_DFF* cells.
+Merge GP_INV cells with GP_DFF* and GP_DLATCH* cells.
\end{lstlisting}
\section{help -- display help messages}
@@ -1199,6 +1399,10 @@ needed.
also check the design hierarchy. this generates an error when
an unknown module is used as cell type.
+ -simcheck
+ like -check, but also thow an error if blackbox modules are
+ instantiated, and throw an error if the design has no top module
+
-purge_lib
by default the hierarchy command will not remove library (blackbox)
modules. use this option to also remove unused blackbox modules.
@@ -1212,6 +1416,11 @@ needed.
per default this pass also converts positional arguments in cells
to arguments using port names. this option disables this behavior.
+ -keep_portwidths
+ per default this pass adjusts the port width on cells that are
+ module instances when the width does not match the module port. this
+ option disables this behavior.
+
-nokeep_asserts
per default this pass sets the "keep" attribute on all modules
that directly or indirectly contain one or more $assert cells. this
@@ -1416,6 +1625,18 @@ When no active module is selected, this prints a list of modules.
When an active module is selected, this prints a list of objects in the module.
\end{lstlisting}
+\section{ltp -- print longest topological path}
+\label{cmd:ltp}
+\begin{lstlisting}[numbers=left,frame=single]
+ ltp [options] [selection]
+
+This command prints the longest topological path in the design. (Only considers
+paths within a single module, so the design must be flattened.)
+
+ -noff
+ automatically exclude FF cell types
+\end{lstlisting}
+
\section{lut2mux -- convert \$lut to \$\_MUX\_}
\label{cmd:lut2mux}
\begin{lstlisting}[numbers=left,frame=single]
@@ -1582,6 +1803,15 @@ This pass adds additional circuitry that emulates the Verilog simulation
behavior for out-of-bounds memory reads and writes.
\end{lstlisting}
+\section{memory\_nordff -- extract read port FFs from memories}
+\label{cmd:memory_nordff}
+\begin{lstlisting}[numbers=left,frame=single]
+ memory_nordff [options] [selection]
+
+This pass extracts FFs from memory read ports. This results in a netlist
+similar to what one would get from calling memory_dff with -nordff.
+\end{lstlisting}
+
\section{memory\_share -- consolidate memory ports}
\label{cmd:memory_share}
\begin{lstlisting}[numbers=left,frame=single]
@@ -1745,6 +1975,15 @@ This pass only operates on completely selected modules without processes.
also remove internal nets if they have a public name
\end{lstlisting}
+\section{opt\_demorgan -- Optimize reductions with DeMorgan equivalents}
+\label{cmd:opt_demorgan}
+\begin{lstlisting}[numbers=left,frame=single]
+ opt_demorgan [selection]
+
+This pass pushes inverters through $reduce_* cells if this will reduce the
+overall gate count of the circuit
+\end{lstlisting}
+
\section{opt\_expr -- perform const folding and simple expression rewriting}
\label{cmd:opt_expr}
\begin{lstlisting}[numbers=left,frame=single]
@@ -1884,15 +2123,16 @@ on partly selected designs.
-memx
simulate verilog simulation behavior for out-of-bounds memory accesses
- using the 'memory_memx' pass. This option implies -nordff.
+ using the 'memory_memx' pass.
-nomem
do not run any of the memory_* passes
- -nordff
- passed to 'memory_dff'. prohibits merging of FFs into memory read ports
+ -rdff
+ do not pass -nordff to 'memory_dff'. This enables merging of FFs into
+ memory read ports.
- -nokeepdc
+ -nokeepdc
do not call opt_* with -keepdc
-run <from_label>[:<to_label>]
@@ -2058,6 +2298,38 @@ Note: This implementation of a quadratic wirelength placer uses exact
dense matrix operations. It is only a toy-placer for small circuits.
\end{lstlisting}
+\section{read -- load HDL designs}
+\label{cmd:read}
+\begin{lstlisting}[numbers=left,frame=single]
+ 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|-vhdl} <vhdl-file>..
+
+Load the specified VHDL files. (Requires Verific.)
+
+
+ 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.
+\end{lstlisting}
+
\section{read\_blif -- read BLIF file}
\label{cmd:read_blif}
\begin{lstlisting}[numbers=left,frame=single]
@@ -2067,6 +2339,10 @@ 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'.
\end{lstlisting}
\section{read\_ilang -- read modules from ilang file}
@@ -2078,6 +2354,15 @@ Load modules from an ilang file to the current design. (ilang is a text
representation of a design in yosys's internal format.)
\end{lstlisting}
+\section{read\_json -- read JSON file}
+\label{cmd:read_json}
+\begin{lstlisting}[numbers=left,frame=single]
+ read_json [filename]
+
+Load modules from a JSON file into the current design See "help write_json"
+for a description of the file format.
+\end{lstlisting}
+
\section{read\_liberty -- read cells from liberty file}
\label{cmd:read_liberty}
\begin{lstlisting}[numbers=left,frame=single]
@@ -2088,9 +2373,13 @@ Read cells from liberty file as modules into current design.
-lib
only create empty blackbox modules
- -ignore_redef
+ -nooverwrite
ignore re-definitions of modules. (the default behavior is to
- create an error message.)
+ 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
@@ -2099,6 +2388,9 @@ Read cells from liberty file as modules into current design.
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
+
-setattr <attribute_name>
set the specified attribute (to the value 1) on all loaded modules
\end{lstlisting}
@@ -2131,6 +2423,9 @@ Verilog-2005 is supported.
-dump_ast2
dump abstract syntax tree (after simplification)
+ -no_dump_ptr
+ do not include hex memory addresses in dump (easier to diff dumps)
+
-dump_vlog
dump ast as Verilog code (after simplification)
@@ -2190,9 +2485,13 @@ Verilog-2005 is supported.
-icells
interpret cell types starting with '$' as internal cell types
- -ignore_redef
+ -nooverwrite
ignore re-definitions of modules. (the default behavior is to
- create an error message.)
+ 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
@@ -2221,6 +2520,10 @@ 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. 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.
\end{lstlisting}
@@ -2251,6 +2554,15 @@ with public names. This ignores all selected ports.
Rename top module.
\end{lstlisting}
+\section{rmports -- remove module ports with no connections}
+\label{cmd:rmports}
+\begin{lstlisting}[numbers=left,frame=single]
+ rmports [selection]
+
+This pass identifies ports in the selected modules which are not used or
+driven and removes them.
+\end{lstlisting}
+
\section{sat -- solve a SAT problem in the circuit}
\label{cmd:sat}
\begin{lstlisting}[numbers=left,frame=single]
@@ -2457,11 +2769,9 @@ design.
are assumed to be bidirectional 'inout' ports.
-set_attr <name> <value>
- -set_cell_attr <name> <value>
- -set_wire_attr <name> <value>
- set the specified attribute on all cells and/or wires that are part of
- a logic loop. the special token {} in the value is replaced with a
- unique identifier for the logic loop.
+ set the specified attribute on all cells that are part of a logic
+ loop. the special token {} in the value is replaced with a unique
+ identifier for the logic loop.
-select
replace the current selection with a selection of all cells and wires
@@ -2497,7 +2807,7 @@ of the design to operate on. This command can be used to modify and view this
list of selected objects.
Note that many commands support an optional [selection] argument that can be
-used to override the global selection for the command. The syntax of this
+used to YS_OVERRIDE the global selection for the command. The syntax of this
optional argument is identical to the syntax of the <selection> argument
described here.
@@ -2728,17 +3038,29 @@ The -type option can be used to change the cell type of the selected cells.
\begin{lstlisting}[numbers=left,frame=single]
setundef [options] [selection]
-This command replaced undef (x) constants with defined (0/1) constants.
+This command replaces undef (x) constants with defined (0/1) constants.
-undriven
also set undriven nets to constant values
+ -expose
+ also expose undriven nets as inputs (use with -undriven)
+
-zero
replace with bits cleared (0)
-one
replace with bits set (1)
+ -undef
+ replace with undef (x) bits, may be used with -undriven
+
+ -anyseq
+ replace with $anyseq drivers (for formal)
+
+ -anyconst
+ replace with $anyconst drivers (for formal)
+
-random <seed>
replace with random bits using the specified integer als seed
value for the random number generator.
@@ -2821,6 +3143,7 @@ to a graphics file (usually SVG or PostScript).
-viewer <viewer>
Run the specified command with the graphics file as parameter.
+ On Windows, this pauses yosys until the viewer exits.
-format <format>
Generate a graphics file in the specified format. Use 'dot' to just
@@ -2882,7 +3205,7 @@ to a graphics file (usually SVG or PostScript).
do not add the module name as graph title to the dot file
When no <format> is specified, 'dot' is used. When no <format> and <viewer> is
-specified, 'xdot' is used to display the schematic.
+specified, 'xdot' is used to display the schematic (POSIX systems only).
The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
unless another prefix is specified using -prefix <prefix>.
@@ -2949,6 +3272,47 @@ will use the same interface as the original $_DFF_*_ cells. The cell parameter
map to greenpak4 shift registers.
\end{lstlisting}
+\section{sim -- simulate the circuit}
+\label{cmd:sim}
+\begin{lstlisting}[numbers=left,frame=single]
+ sim [options] [top-level]
+
+This command simulates the circuit using the given top-level module.
+
+ -vcd <filename>
+ write the simulation results to the given VCD file
+
+ -clock <portname>
+ name of top-level clock input
+
+ -clockn <portname>
+ name of top-level clock input (inverse polarity)
+
+ -reset <portname>
+ name of top-level reset input (active high)
+
+ -resetn <portname>
+ name of top-level inverted reset input (active low)
+
+ -rstlen <integer>
+ number of cycles reset should stay active (default: 1)
+
+ -zinit
+ zero-initialize all uninitialized regs and memories
+
+ -n <integer>
+ number of cycles to simulate (default: 20)
+
+ -a
+ include all nets in VCD output, not just those with public names
+
+ -w
+ writeback mode: use final simulation state as new init state
+
+ -d
+ enable debug output
+\end{lstlisting}
+
\section{simplemap -- mapping simple coarse-grain cells}
\label{cmd:simplemap}
\begin{lstlisting}[numbers=left,frame=single]
@@ -2963,22 +3327,6 @@ primitives. The following internal cell types are mapped by this pass:
$sr, $ff, $dff, $dffsr, $adff, $dlatch
\end{lstlisting}
-\section{singleton -- create singleton modules}
-\label{cmd:singleton}
-\begin{lstlisting}[numbers=left,frame=single]
- singleton [selection]
-
-By default, a module that is instantiated by several other modules is only
-kept once in the design. This preserves the original modularity of the design
-and reduces the overall size of the design in memory. But it prevents certain
-optimizations and other operations on the design. This pass creates singleton
-modules for all selected cells. The created modules are marked with the
-'singleton' attribute.
-
-This commands only operates on modules that by themself have the 'singleton'
-attribute set (the 'top' module is a singleton implicitly).
-\end{lstlisting}
-
\section{splice -- create explicit splicing cells}
\label{cmd:splice}
\begin{lstlisting}[numbers=left,frame=single]
@@ -3122,6 +3470,9 @@ on partly selected designs.
-nordff
passed to 'memory'. prohibits merging of FFs into memory read ports
+ -noshare
+ do not run SAT-based resource sharing
+
-run <from_label>[:<to_label>]
only run the commands between the labels (see below). an empty
from label is synonymous to 'begin', and empty to label is
@@ -3164,6 +3515,344 @@ The following commands are executed by this synthesis command:
check
\end{lstlisting}
+\section{synth\_achronix -- synthesis for Acrhonix Speedster22i FPGAs.}
+\label{cmd:synth_achronix}
+\begin{lstlisting}[numbers=left,frame=single]
+ synth_achronix [options]
+
+This command runs synthesis for Achronix Speedster eFPGAs. This work is still experimental.
+
+ -top <module>
+ use the specified module as top module (default='top')
+
+ -vout <file>
+ write the design to the specified Verilog netlist file. writing of an
+ output file is omitted if this parameter is not specified.
+
+ -run <from_label>:<to_label>
+ only run the commands between the labels (see below). an empty
+ from label is synonymous to 'begin', and empty to label is
+ synonymous to the end of the command list.
+
+ -noflatten
+ do not flatten design before synthesis
+
+ -retime
+ run 'abc' with -dff option
+
+
+The following commands are executed by this synthesis command:
+
+ begin:
+ read_verilog -sv -lib +/achronix/speedster22i/cells_sim.v
+ hierarchy -check -top <top>
+
+ flatten: (unless -noflatten)
+ proc
+ flatten
+ tribuf -logic
+ deminout
+
+ coarse:
+ synth -run coarse
+
+ fine:
+ opt -fast -mux_undef -undriven -fine -full
+ memory_map
+ opt -undriven -fine
+ dffsr2dff
+ dff2dffe -direct-match $_DFF_*
+ opt -fine
+ techmap -map +/techmap.v
+ opt -full
+ clean -purge
+ setundef -undriven -zero
+ abc -markgroups -dff (only if -retime)
+
+ map_luts:
+ abc -lut 4
+ clean
+
+ map_cells:
+ iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I
+ techmap -map +/achronix/speedster22i/cells_map.v
+ clean -purge
+
+ check:
+ hierarchy -check
+ stat
+ check -noinit
+
+ vout:
+ write_verilog -nodec -attr2comment -defparam -renameprefix syn_ <file-name>
+\end{lstlisting}
+
+\section{synth\_coolrunner2 -- synthesis for Xilinx Coolrunner-II CPLDs}
+\label{cmd:synth_coolrunner2}
+\begin{lstlisting}[numbers=left,frame=single]
+ synth_coolrunner2 [options]
+
+This command runs synthesis for Coolrunner-II CPLDs. This work is experimental.
+It is intended to be used with https://github.com/azonenberg/openfpga as the
+place-and-route.
+
+ -top <module>
+ use the specified module as top module (default='top')
+
+ -json <file>
+ write the design to the specified JSON file. writing of an output file
+ is omitted if this parameter is not specified.
+
+ -run <from_label>:<to_label>
+ only run the commands between the labels (see below). an empty
+ from label is synonymous to 'begin', and empty to label is
+ synonymous to the end of the command list.
+
+ -noflatten
+ do not flatten design before synthesis
+
+ -retime
+ run 'abc' with -dff option
+
+
+The following commands are executed by this synthesis command:
+
+ begin:
+ read_verilog -lib +/coolrunner2/cells_sim.v
+ hierarchy -check -top <top>
+
+ flatten: (unless -noflatten)
+ proc
+ flatten
+ tribuf -logic
+
+ coarse:
+ synth -run coarse
+
+ fine:
+ opt -fast -full
+ techmap
+ techmap -map +/coolrunner2/cells_latch.v
+ dfflibmap -prepare -liberty +/coolrunner2/xc2_dff.lib
+
+ map_tff:
+ abc -g AND,XOR
+ clean
+ extract -map +/coolrunner2/tff_extract.v
+
+ map_pla:
+ abc -sop -I 40 -P 56
+ clean
+
+ map_cells:
+ dfflibmap -liberty +/coolrunner2/xc2_dff.lib
+ dffinit -ff FDCP Q INIT
+ dffinit -ff FDCP_N Q INIT
+ dffinit -ff FTCP Q INIT
+ dffinit -ff FTCP_N Q INIT
+ dffinit -ff LDCP Q INIT
+ dffinit -ff LDCP_N Q INIT
+ coolrunner2_sop
+ iopadmap -bits -inpad IBUF O:I -outpad IOBUFE I:IO -inoutpad IOBUFE O:IO -toutpad IOBUFE E:I:IO -tinoutpad IOBUFE E:O:I:IO
+ attrmvcp -attr src -attr LOC t:IOBUFE n:*
+ attrmvcp -attr src -attr LOC -driven t:IBUF n:*
+ splitnets
+ clean
+
+ check:
+ hierarchy -check
+ stat
+ check -noinit
+
+ json:
+ write_json <file-name>
+\end{lstlisting}
+
+\section{synth\_easic -- synthesis for eASIC platform}
+\label{cmd:synth_easic}
+\begin{lstlisting}[numbers=left,frame=single]
+ synth_easic [options]
+
+This command runs synthesis for eASIC platform.
+
+ -top <module>
+ use the specified module as top module
+
+ -vlog <file>
+ write the design to the specified structural Verilog file. writing of
+ an output file is omitted if this parameter is not specified.
+
+ -etools <path>
+ set path to the eTools installation. (default=/opt/eTools)
+
+ -run <from_label>:<to_label>
+ only run the commands between the labels (see below). an empty
+ from label is synonymous to 'begin', and empty to label is
+ synonymous to the end of the command list.
+
+ -noflatten
+ do not flatten design before synthesis
+
+ -retime
+ run 'abc' with -dff option
+
+
+The following commands are executed by this synthesis command:
+
+ begin:
+ read_liberty -lib <etools_phys_clk_lib>
+ read_liberty -lib <etools_logic_lut_lib>
+ hierarchy -check -top <top>
+
+ flatten: (unless -noflatten)
+ proc
+ flatten
+
+ coarse:
+ synth -run coarse
+
+ fine:
+ opt -fast -mux_undef -undriven -fine
+ memory_map
+ opt -undriven -fine
+ techmap
+ opt -fast
+ abc -dff (only if -retime)
+ opt_clean (only if -retime)
+
+ map:
+ dfflibmap -liberty <etools_phys_clk_lib>
+ abc -liberty <etools_logic_lut_lib>
+ opt_clean
+
+ check:
+ hierarchy -check
+ stat
+ check -noinit
+
+ vlog:
+ write_verilog -noexpr -attr2comment <file-name>
+\end{lstlisting}
+
+\section{synth\_ecp5 -- synthesis for ECP5 FPGAs}
+\label{cmd:synth_ecp5}
+\begin{lstlisting}[numbers=left,frame=single]
+ synth_ecp5 [options]
+
+This command runs synthesis for ECP5 FPGAs.
+
+ -top <module>
+ use the specified module as top module
+
+ -blif <file>
+ write the design to the specified BLIF file. writing of an output file
+ is omitted if this parameter is not specified.
+
+ -edif <file>
+ write the design to the specified EDIF file. writing of an output file
+ is omitted if this parameter is not specified.
+
+ -json <file>
+ write the design to the specified JSON file. writing of an output file
+ is omitted if this parameter is not specified.
+
+ -run <from_label>:<to_label>
+ only run the commands between the labels (see below). an empty
+ from label is synonymous to 'begin', and empty to label is
+ synonymous to the end of the command list.
+
+ -noflatten
+ do not flatten design before synthesis
+
+ -retime
+ run 'abc' with -dff option
+
+ -noccu2
+ do not use CCU2 cells in output netlist
+
+ -nodffe
+ do not use flipflops with CE in output netlist
+
+ -nobram
+ do not use BRAM cells in output netlist
+
+ -nodram
+ do not use distributed RAM cells in output netlist
+
+ -nomux
+ do not use PFU muxes to implement LUTs larger than LUT4s
+
+ -abc2
+ run two passes of 'abc' for slightly improved logic density
+
+ -vpr
+ generate an output netlist (and BLIF file) suitable for VPR
+ (this feature is experimental and incomplete)
+
+
+The following commands are executed by this synthesis command:
+
+ begin:
+ read_verilog -lib +/ecp5/cells_sim.v
+ hierarchy -check -top <top>
+
+ flatten: (unless -noflatten)
+ proc
+ flatten
+ tribuf -logic
+ deminout
+
+ coarse:
+ synth -run coarse
+
+ bram: (skip if -nobram)
+
+ dram: (skip if -nodram)
+ memory_bram -rules +/ecp5/dram.txt
+ techmap -map +/ecp5/drams_map.v
+
+ fine:
+ opt -fast -mux_undef -undriven -fine
+ memory_map
+ opt -undriven -fine
+ techmap -map +/techmap.v -map +/ecp5/arith_map.v
+ abc -dff (only if -retime)
+
+ map_ffs:
+ dffsr2dff
+ dff2dffs
+ opt_clean
+ dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
+ techmap -D NO_LUT -map +/ecp5/cells_map.v
+ opt_expr -mux_undef
+ simplemap
+
+ map_luts:
+ abc (only if -abc2)
+ abc -lut 4:7
+ clean
+
+ map_cells:
+ techmap -map +/ecp5/cells_map.v (with -D NO_LUT in vpr mode)
+ clean
+
+ check:
+ hierarchy -check
+ stat
+ check -noinit
+
+ blif:
+ opt_clean -purge (vpr mode)
+ write_blif -attr -cname -conn -param <file-name> (vpr mode)
+ write_blif -gates -attr -param <file-name> (non-vpr mode)
+
+ edif:
+ write_edif <file-name>
+
+ json:
+ write_json <file-name>
+\end{lstlisting}
+
\section{synth\_gowin -- synthesis for Gowin FPGAs}
\label{cmd:synth_gowin}
\begin{lstlisting}[numbers=left,frame=single]
@@ -3228,7 +3917,7 @@ The following commands are executed by this synthesis command:
check -noinit
vout:
- write_verilog -attr2comment -defparam -renameprefix gen <file-name>
+ write_verilog -nodec -attr2comment -defparam -renameprefix gen <file-name>
\end{lstlisting}
\section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs}
@@ -3237,6 +3926,8 @@ The following commands are executed by this synthesis command:
synth_greenpak4 [options]
This command runs synthesis for GreenPAK4 FPGAs. This work is experimental.
+It is intended to be used with https://github.com/azonenberg/openfpga as the
+place-and-route.
-top <module>
use the specified module as top module (default='top')
@@ -3276,12 +3967,13 @@ The following commands are executed by this synthesis command:
synth -run coarse
fine:
- greenpak4_counters
+ extract_counter -pout GP_DCMP,GP_DAC -maxwidth 14
clean
opt -fast -mux_undef -undriven -fine
memory_map
opt -undriven -fine
techmap
+ techmap -map +/greenpak4/cells_latch.v
dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib
opt -fast
abc -dff (only if -retime)
@@ -3323,14 +4015,18 @@ The following commands are executed by this synthesis command:
This command runs synthesis for iCE40 FPGAs.
-top <module>
- use the specified module as top module (default='top')
+ use the specified module as top module
-blif <file>
write the design to the specified BLIF file. writing of an output file
is omitted if this parameter is not specified.
-edif <file>
- write the design to the specified edif file. writing of an output file
+ write the design to the specified EDIF file. writing of an output file
+ is omitted if this parameter is not specified.
+
+ -json <file>
+ write the design to the specified JSON file. writing of an output file
is omitted if this parameter is not specified.
-run <from_label>:<to_label>
@@ -3347,12 +4043,19 @@ This command runs synthesis for iCE40 FPGAs.
-nocarry
do not use SB_CARRY cells in output netlist
+ -nodffe
+ do not use SB_DFFE* cells in output netlist
+
-nobram
do not use SB_RAM40_4K* cells in output netlist
-abc2
run two passes of 'abc' for slightly improved logic density
+ -vpr
+ generate an output netlist (and BLIF file) suitable for VPR
+ (this feature is experimental and incomplete)
+
The following commands are executed by this synthesis command:
@@ -3384,7 +4087,7 @@ The following commands are executed by this synthesis command:
map_ffs:
dffsr2dff
dff2dffe -direct-match $_DFF_*
- techmap -map +/ice40/cells_map.v
+ techmap -D NO_LUT -map +/ice40/cells_map.v
opt_expr -mux_undef
simplemap
ice40_ffinit
@@ -3399,7 +4102,7 @@ The following commands are executed by this synthesis command:
clean
map_cells:
- techmap -map +/ice40/cells_map.v
+ techmap -map +/ice40/cells_map.v (with -D NO_LUT in vpr mode)
clean
check:
@@ -3408,10 +4111,116 @@ The following commands are executed by this synthesis command:
check -noinit
blif:
- write_blif -gates -attr -param <file-name>
+ opt_clean -purge (vpr mode)
+ write_blif -attr -cname -conn -param <file-name> (vpr mode)
+ write_blif -gates -attr -param <file-name> (non-vpr mode)
edif:
write_edif <file-name>
+
+ json:
+ write_json <file-name>
+\end{lstlisting}
+
+\section{synth\_intel -- synthesis for Intel (Altera) FPGAs.}
+\label{cmd:synth_intel}
+\begin{lstlisting}[numbers=left,frame=single]
+ synth_intel [options]
+
+This command runs synthesis for Intel FPGAs.
+
+ -family < max10 | a10gx | cyclone10 | cyclonev | cycloneiv | cycloneive>
+ generate the synthesis netlist for the specified family.
+ MAX10 is the default target if not family argument specified.
+ For Cyclone GX devices, use cycloneiv argument; For Cyclone E, use cycloneive.
+ Cyclone V and Arria 10 GX devices are experimental, use it with a10gx argument.
+
+ -top <module>
+ use the specified module as top module (default='top')
+
+ -vqm <file>
+ write the design to the specified Verilog Quartus Mapping File. Writing of an
+ output file is omitted if this parameter is not specified.
+
+ -vpr <file>
+ write BLIF files for VPR flow experiments. The synthesized BLIF output file is not
+ compatible with the Quartus flow. Writing of an
+ output file is omitted if this parameter is not specified.
+
+ -run <from_label>:<to_label>
+ only run the commands between the labels (see below). an empty
+ from label is synonymous to 'begin', and empty to label is
+ synonymous to the end of the command list.
+
+ -noiopads
+ do not use altsyncram cells in output netlist
+
+ -nobram
+ do not use altsyncram cells in output netlist
+
+ -noflatten
+ do not flatten design before synthesis
+
+ -retime
+ run 'abc' with -dff option
+
+The following commands are executed by this synthesis command:
+
+ begin:
+
+ family:
+ read_verilog -sv -lib +/intel/max10/cells_sim.v
+ read_verilog -sv -lib +/intel/common/m9k_bb.v
+ read_verilog -sv -lib +/intel/common/altpll_bb.v
+ hierarchy -check -top <top>
+
+ flatten: (unless -noflatten)
+ proc
+ flatten
+ tribuf -logic
+ deminout
+
+ coarse:
+ synth -run coarse
+
+ bram: (skip if -nobram)
+ memory_bram -rules +/intel/common/brams.txt
+ techmap -map +/intel/common/brams_map.v
+
+ fine:
+ opt -fast -mux_undef -undriven -fine -full
+ memory_map
+ opt -undriven -fine
+ dffsr2dff
+ dff2dffe -direct-match $_DFF_*
+ opt -fine
+ techmap -map +/techmap.v
+ opt -full
+ clean -purge
+ setundef -undriven -zero
+ abc -markgroups -dff (only if -retime)
+
+ map_luts:
+ abc -lut 4
+ clean
+
+ map_cells:
+ iopadmap -bits -outpad $__outpad I:O -inpad $__inpad O:I (unless -noiopads)
+ techmap -map +/intel/max10/cells_map.v
+ dffinit -highlow -ff dffeas q power_up
+ clean -purge
+
+ check:
+ hierarchy -check
+ stat
+ check -noinit
+
+ vqm:
+ write_verilog -attr2comment -defparam -nohex -decimal -renameprefix syn_ <file-name>
+
+ vpr:
+ opt_clean -purge
+ write_blif <file-name>
\end{lstlisting}
\section{synth\_xilinx -- synthesis for Xilinx FPGAs}
@@ -3430,6 +4239,14 @@ compatible with 7-Series Xilinx devices.
write the design to the specified edif file. writing of an output file
is omitted if this parameter is not specified.
+ -blif <file>
+ write the design to the specified BLIF file. writing of an output file
+ is omitted if this parameter is not specified.
+
+ -vpr
+ generate an output netlist (and BLIF file) suitable for VPR
+ (this feature is experimental and incomplete)
+
-run <from_label>:<to_label>
only run the commands between the labels (see below). an empty
from label is synonymous to 'begin', and empty to label is
@@ -3448,7 +4265,6 @@ The following commands are executed by this synthesis command:
read_verilog -lib +/xilinx/cells_sim.v
read_verilog -lib +/xilinx/cells_xtra.v
read_verilog -lib +/xilinx/brams_bb.v
- read_verilog -lib +/xilinx/drams_bb.v
hierarchy -check -top <top>
flatten: (only if -flatten)
@@ -3480,7 +4296,7 @@ The following commands are executed by this synthesis command:
clean
map_cells:
- techmap -map +/xilinx/cells_map.v
+ techmap -map +/xilinx/cells_map.v (with -D NO_LUT in vpr mode)
dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT
clean
@@ -3491,6 +4307,9 @@ The following commands are executed by this synthesis command:
edif: (only if -edif)
write_edif <file-name>
+
+ blif: (only if -blif)
+ write_blif <file-name>
\end{lstlisting}
\section{tcl -- execute a TCL script file}
@@ -3502,9 +4321,9 @@ This command executes the tcl commands in the specified file.
Use 'yosys cmd' to run the yosys command 'cmd' from tcl.
The tcl command 'yosys -import' can be used to import all yosys
-commands directly as tcl commands to the tcl shell. The yosys
-command 'proc' is wrapped using the tcl command 'procs' in order
-to avoid a name collision with the tcl builtin command 'proc'.
+commands directly as tcl commands to the tcl shell. Yosys commands
+'proc' and 'rename' are wrapped to tcl commands 'procs' and 'renames'
+in order to avoid a name collision with the built in commands.
\end{lstlisting}
\section{techmap -- generic technology mapper}
@@ -3548,7 +4367,7 @@ file.
-D <define>, -I <incdir>
this options are passed as-is to the Verilog frontend for loading the
map file. Note that the Verilog frontend is also called with the
- '-ignore_redef' option set.
+ '-nooverwrite' option set.
When a module in the map file has the 'techmap_celltype' attribute set, it will
match cells with a type that match the text value of this attribute. Otherwise
@@ -3629,7 +4448,7 @@ the design is connected to a constant value. The parameter is then set to the
constant value.
A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name
-of the cell that is being replaced.
+and attributes of the cell that is being replaced.
See 'help extract' for a pass that does the opposite thing.
@@ -3795,24 +4614,134 @@ This pass transforms $mux cells with 'z' inputs to tristate buffers.
to non-tristate logic. this option implies -merge.
\end{lstlisting}
+\section{uniquify -- create unique copies of modules}
+\label{cmd:uniquify}
+\begin{lstlisting}[numbers=left,frame=single]
+ uniquify [selection]
+
+By default, a module that is instantiated by several other modules is only
+kept once in the design. This preserves the original modularity of the design
+and reduces the overall size of the design in memory. But it prevents certain
+optimizations and other operations on the design. This pass creates unique
+modules for all selected cells. The created modules are marked with the
+'unique' attribute.
+
+This commands only operates on modules that by themself have the 'unique'
+attribute set (the 'top' module is unique implicitly).
+\end{lstlisting}
+
\section{verific -- load Verilog and VHDL designs using Verific}
\label{cmd:verific}
\begin{lstlisting}[numbers=left,frame=single]
- verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>..
+ 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 SYNTHESIS and VERIFIC are defined implicitly.
+
+
+ verific -formal <verilog-file>..
- verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-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 -import [-gates] {-all | <top-module>..}
+ 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 -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. A gate-level netlist is created
-when called with -gates.
+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.
+
+ -autocover
+ Generate automatic cover statements for all asserts
+
+ -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):
+
+ -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.
+
+ -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.
Visit http://verific.com/ for more information on Verific.
\end{lstlisting}
@@ -3837,40 +4766,19 @@ Push or pop the list of default options to a stack. Note that -push does
not imply -clear.
\end{lstlisting}
-\section{vhdl2verilog -- importing VHDL designs using vhdl2verilog}
-\label{cmd:vhdl2verilog}
+\section{verilog\_defines -- define and undefine verilog defines}
+\label{cmd:verilog_defines}
\begin{lstlisting}[numbers=left,frame=single]
- vhdl2verilog [options] <vhdl-file>..
-
-This command reads VHDL source files using the 'vhdl2verilog' tool and the
-Yosys Verilog frontend.
-
- -out <out_file>
- do not import the vhdl2verilog output. instead write it to the
- specified file.
-
- -vhdl2verilog_dir <directory>
- do use the specified vhdl2verilog installation. this is the directory
- that contains the setup_env.sh file. when this option is not present,
- it is assumed that vhdl2verilog is in the PATH environment variable.
+ verilog_defines [options]
- -top <top-entity-name>
- The name of the top entity. This option is mandatory.
+Define and undefine verilog preprocessor macros.
-The following options are passed as-is to vhdl2verilog:
-
- -arch <architecture_name>
- -unroll_generate
- -nogenericeval
- -nouniquify
- -oldparser
- -suppress <list>
- -quiet
- -nobanner
- -mapfile <file>
+ -Dname[=definition]
+ define the preprocessor symbol 'name' and set its optional value
+ 'definition'
-vhdl2verilog can be obtained from:
-http://www.edautils.com/vhdl2verilog.html
+ -Uname[=definition]
+ undefine the preprocessor symbol 'name'
\end{lstlisting}
\section{wreduce -- reduce the word size of operations if possible}
@@ -3892,6 +4800,38 @@ Options:
flows that use the 'memory_memx' pass.
\end{lstlisting}
+\section{write\_aiger -- write design to AIGER file}
+\label{cmd:write_aiger}
+\begin{lstlisting}[numbers=left,frame=single]
+ write_aiger [options] [filename]
+
+Write the current design to an AIGER file. The design must be flattened and
+must not contain any cell types except $_AND_, $_NOT_, simple FF types,
+$assert and $assume cells, and $initstate cells.
+
+$assert and $assume cells are converted to AIGER bad state properties and
+invariant constraints.
+
+ -ascii
+ write ASCII version of AGIER format
+
+ -zinit
+ convert FFs to zero-initialized FFs, adding additional inputs for
+ uninitialized FFs.
+
+ -miter
+ design outputs are AIGER bad state properties
+
+ -symbols
+ include a symbol table in the generated AIGER file
+
+ -map <filename>
+ write an extra file with port and latch symbols
+
+ -vmap <filename>
+ like -map, but more verbose
+\end{lstlisting}
+
\section{write\_blif -- write design to BLIF file}
\label{cmd:write_blif}
\begin{lstlisting}[numbers=left,frame=single]
@@ -3949,6 +4889,11 @@ file *.blif when any of this options is used.
-cname
use the non-standard .cname statement to write cell names
+ -iname, -iattr
+ enable -cname and -attr functionality for .names statements
+ (the .cname and .attr statements will be included in the BLIF
+ output after the truth table for the .names statement)
+
-blackbox
write blackbox cells with .blackbox statement.
@@ -3959,9 +4904,15 @@ file *.blif when any of this options is used.
\section{write\_btor -- write design to BTOR file}
\label{cmd:write_btor}
\begin{lstlisting}[numbers=left,frame=single]
- write_btor [filename]
+ write_btor [options] [filename]
+
+Write a BTOR description of the current design.
-Write the current design to an BTOR file.
+ -v
+ Add comments and indentation to BTOR output file
+
+ -s
+ Output only a single bad property for all asserts
\end{lstlisting}
\section{write\_edif -- write design to EDIF netlist file}
@@ -3979,6 +4930,10 @@ Write the current design to an EDIF netlist file.
if the design contains constant nets. use "hilomap" to map to custom
constant drivers first)
+ -pvector {par|bra|ang}
+ sets the delimiting character for module port rename clauses to
+ parentheses, square brackets, or angle brackets.
+
Unfortunately there are different "flavors" of the EDIF file format. This
command generates EDIF files for the Xilinx place&route tools. It might be
necessary to make small modifications to this command when a different tool
@@ -4003,6 +4958,14 @@ Inside a script the input file can also can a here-document:
EOT
\end{lstlisting}
+\section{write\_firrtl -- write design to a FIRRTL file}
+\label{cmd:write_firrtl}
+\begin{lstlisting}[numbers=left,frame=single]
+ write_firrtl [options] [filename]
+
+Write a FIRRTL netlist of the current design.
+\end{lstlisting}
+
\section{write\_ilang -- write design to ilang file}
\label{cmd:write_ilang}
\begin{lstlisting}[numbers=left,frame=single]
@@ -4123,6 +5086,10 @@ values referenced above are vectors of this integers. Signal bits that are
connected to a constant driver are denoted as string "0" or "1" instead of
a number.
+Numeric parameter and attribute values up to 32 bits are written as decimal
+values. Numbers larger than that are written as string holding the binary
+representation of the value.
+
For example the following Verilog code:
module test(input x, y);
@@ -4242,43 +5209,109 @@ Future version of Yosys might add support for additional fields in the JSON
format. A program processing this format must ignore all unknown fields.
\end{lstlisting}
-\section{write\_smt2 -- write design to SMT-LIBv2 file}
-\label{cmd:write_smt2}
+\section{write\_simplec -- convert design to simple C code}
+\label{cmd:write_simplec}
\begin{lstlisting}[numbers=left,frame=single]
- write_smt2 [options] [filename]
+ write_simplec [options] [filename]
-Write a SMT-LIBv2 [1] description of the current design. For a module with name
-'<mod>' this will declare the sort '<mod>_s' (state of the module) and the
-functions operating on that state.
+Write simple C code for simulating the design. The C code writen can be used to
+simulate the design in a C environment, but the purpose of this command is to
+generate code that works well with C-based formal verification.
-The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions
-are provided that can be used to access the values of the signals in the module.
-By default only ports, registers, and wires with the 'keep' attribute set are
-made available via such functions. With the -nobv option, multi-bit wires are
-exported as separate functions of type Bool for the individual bits. Without
--nobv multi-bit wires are exported as single functions of type BitVec.
+ -verbose
+ this will print the recursive walk used to export the modules.
-The '<mod>_t' function evaluates to 'true' when the given pair of states
-describes a valid state transition.
+ -i8, -i16, -i32, -i64
+ set the maximum integer bit width to use in the generated code.
-The '<mod>_a' function evaluates to 'true' when the given state satisfies
-the asserts in the module.
+THIS COMMAND IS UNDER CONSTRUCTION
+\end{lstlisting}
-The '<mod>_u' function evaluates to 'true' when the given state satisfies
-the assumptions in the module.
+\section{write\_smt2 -- write design to SMT-LIBv2 file}
+\label{cmd:write_smt2}
+\begin{lstlisting}[numbers=left,frame=single]
+ write_smt2 [options] [filename]
-The '<mod>_i' function evaluates to 'true' when the given state conforms
-to the initial state. Furthermore the '<mod>_is' function should be asserted
-to be true for initial states in addition to '<mod>_i', and should be
-asserted to be false for non-initial states.
+Write a SMT-LIBv2 [1] description of the current design. For a module with name
+'<mod>' this will declare the sort '<mod>_s' (state of the module) and will
+define and declare functions operating on that state.
+
+The following SMT2 functions are generated for a module with name '<mod>'.
+Some declarations/definitions are printed with a special comment. A prover
+using the SMT2 files can use those comments to collect all relevant metadata
+about the design.
+
+ ; yosys-smt2-module <mod>
+ (declare-sort |<mod>_s| 0)
+ The sort representing a state of module <mod>.
+
+ (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))
+ This function must be asserted for each state to establish the
+ design hierarchy.
+
+ ; yosys-smt2-input <wirename> <width>
+ ; yosys-smt2-output <wirename> <width>
+ ; yosys-smt2-register <wirename> <width>
+ ; yosys-smt2-wire <wirename> <width>
+ (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))
+ (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)
+ For each port, register, and wire with the 'keep' attribute set an
+ accessor function is generated. Single-bit wires are returned as Bool,
+ multi-bit wires as BitVec.
+
+ ; yosys-smt2-cell <submod> <instancename>
+ (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)
+ There is a function like that for each hierarchical instance. It
+ returns the sort that represents the state of the sub-module that
+ implements the instance.
+
+ (declare-fun |<mod>_is| (|<mod>_s|) Bool)
+ This function must be asserted 'true' for initial states, and 'false'
+ otherwise.
+
+ (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))
+ This function must be asserted 'true' for initial states. For
+ non-initial states it must be left unconstrained.
+
+ (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))
+ This function evaluates to 'true' if the states 'state' and
+ 'next_state' form a valid state transition.
+
+ (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))
+ This function evaluates to 'true' if all assertions hold in the state.
+
+ (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))
+ This function evaluates to 'true' if all assumptions hold in the state.
+
+ ; yosys-smt2-assert <id> <filename:linenum>
+ (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))
+ Each $assert cell is converted into one of this functions. The function
+ evaluates to 'true' if the assert statement holds in the state.
+
+ ; yosys-smt2-assume <id> <filename:linenum>
+ (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))
+ Each $assume cell is converted into one of this functions. The function
+ evaluates to 'true' if the assume statement holds in the state.
+
+ ; yosys-smt2-cover <id> <filename:linenum>
+ (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))
+ Each $cover cell is converted into one of this functions. The function
+ evaluates to 'true' if the cover statement is activated in the state.
-For hierarchical designs, the '<mod>_h' function must be asserted for each
-state to establish the design hierarchy. The '<mod>_h <cellname>' function
-evaluates to the state corresponding to the given cell within <mod>.
+Options:
-verbose
this will print the recursive walk used to export the modules.
+ -stbv
+ Use a BitVec sort to represent a state instead of an uninterpreted
+ sort. As a side-effect this will prevent use of arrays to model
+ memories.
+
+ -stdt
+ Use SMT-LIB 2.6 style datatypes to represent a state instead of an
+ uninterpreted sort.
+
-nobv
disable support for BitVec (FixedSizeBitVectors theory). without this
option multi-bit wires are represented using the BitVec sort and
@@ -4394,6 +5427,25 @@ Write the current design to an SPICE netlist file.
set the specified module as design top module
\end{lstlisting}
+\section{write\_table -- write design as connectivity table}
+\label{cmd:write_table}
+\begin{lstlisting}[numbers=left,frame=single]
+ write_table [options] [filename]
+
+Write the current design as connectivity table. The output is a tab-separated
+ASCII table with the following columns:
+
+ module name
+ cell name
+ cell type
+ cell port
+ direction
+ signal
+
+module inputs and outputs are output using cell type and port '-' and with
+'pi' (primary input) or 'po' (primary output) or 'pio' as direction.
+\end{lstlisting}
+
\section{write\_verilog -- write design to Verilog file}
\label{cmd:write_verilog}
\begin{lstlisting}[numbers=left,frame=single]
@@ -4424,6 +5476,14 @@ Write the current design to a Verilog file.
not bit pattern. This option deactivates this feature and instead
will write out all constants in binary.
+ -decimal
+ dump 32-bit constants in decimal and without size and radix
+
+ -nohex
+ constant values that are compatible with hex output are usually
+ dumped as hex values. This option deactivates this feature and
+ instead will write out all constants in binary.
+
-nostr
Parameters and attributes that are specified as strings in the
original input will be output as strings by this back-end. This
diff --git a/techlibs/ecp5/dram.txt b/techlibs/ecp5/dram.txt
index b9435742..b3252fa9 100644
--- a/techlibs/ecp5/dram.txt
+++ b/techlibs/ecp5/dram.txt
@@ -13,5 +13,4 @@ endbram
match $__TRELLIS_DPR16X4
make_outreg
- min wports 1
endmatch
diff --git a/techlibs/xilinx/cells_xtra.sh b/techlibs/xilinx/cells_xtra.sh
index e7c7d17b..c7ad1604 100644
--- a/techlibs/xilinx/cells_xtra.sh
+++ b/techlibs/xilinx/cells_xtra.sh
@@ -1,13 +1,13 @@
#!/bin/bash
set -e
-libdir="/opt/Xilinx/Vivado/2018.1/data/verilog/src"
+libdir="/opt/Xilinx/Vivado/2015.4/data/verilog/src"
function xtract_cell_decl()
{
for dir in $libdir/xeclib $libdir/retarget; do
[ -f $dir/$1.v ] || continue
- egrep '^\s*((end)?module|parameter|input|inout|output|(end)?function|(end)?task)' $dir/$1.v |
+ egrep '^\s*((end)?module|parameter|input|output|(end)?function|(end)?task)' $dir/$1.v |
sed -re '/UNPLACED/ d; /^\s*function/,/endfunction/ d; /^\s*task/,/endtask/ d;
s,//.*,,; s/#?\(.*/(...);/; s/^(input|output|parameter)/ \1/;
s/\s+$//; s/,$/;/; /input|output|parameter/ s/[^;]$/&;/; s/\s+/ /g;
diff --git a/techlibs/xilinx/cells_xtra.v b/techlibs/xilinx/cells_xtra.v
index 69e54233..a2dd01ad 100644
--- a/techlibs/xilinx/cells_xtra.v
+++ b/techlibs/xilinx/cells_xtra.v
@@ -2225,7 +2225,6 @@ module IOBUF (...);
parameter IOSTANDARD = "DEFAULT";
parameter SLEW = "SLOW";
output O;
- inout IO;
input I, T;
endmodule
@@ -2237,7 +2236,6 @@ module IOBUF_DCIEN (...);
parameter SLEW = "SLOW";
parameter USE_IBUFDISABLE = "TRUE";
output O;
- inout IO;
input DCITERMDISABLE;
input I;
input IBUFDISABLE;
@@ -2252,7 +2250,6 @@ module IOBUF_INTERMDISABLE (...);
parameter SLEW = "SLOW";
parameter USE_IBUFDISABLE = "TRUE";
output O;
- inout IO;
input I;
input IBUFDISABLE;
input INTERMDISABLE;
@@ -2266,7 +2263,6 @@ module IOBUFDS (...);
parameter IOSTANDARD = "DEFAULT";
parameter SLEW = "SLOW";
output O;
- inout IO, IOB;
input I, T;
endmodule
@@ -2279,8 +2275,6 @@ module IOBUFDS_DCIEN (...);
parameter SLEW = "SLOW";
parameter USE_IBUFDISABLE = "TRUE";
output O;
- inout IO;
- inout IOB;
input DCITERMDISABLE;
input I;
input IBUFDISABLE;
@@ -2294,8 +2288,6 @@ module IOBUFDS_DIFF_OUT (...);
parameter IOSTANDARD = "DEFAULT";
output O;
output OB;
- inout IO;
- inout IOB;
input I;
input TM;
input TS;
@@ -2310,8 +2302,6 @@ module IOBUFDS_DIFF_OUT_DCIEN (...);
parameter USE_IBUFDISABLE = "TRUE";
output O;
output OB;
- inout IO;
- inout IOB;
input DCITERMDISABLE;
input I;
input IBUFDISABLE;
@@ -2328,8 +2318,6 @@ module IOBUFDS_DIFF_OUT_INTERMDISABLE (...);
parameter USE_IBUFDISABLE = "TRUE";
output O;
output OB;
- inout IO;
- inout IOB;
input I;
input IBUFDISABLE;
input INTERMDISABLE;
@@ -2393,7 +2381,6 @@ module ISERDESE2 (...);
endmodule
module KEEPER (...);
- inout O;
endmodule
module LDCE (...);