summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGELOG38
-rw-r--r--Makefile4
-rw-r--r--backends/ilang/ilang_backend.cc2
-rw-r--r--backends/verilog/verilog_backend.cc14
-rw-r--r--frontends/ast/ast.cc4
-rw-r--r--frontends/ast/ast.h2
-rw-r--r--frontends/ast/genrtlil.cc18
-rw-r--r--frontends/ast/simplify.cc19
-rw-r--r--frontends/verilog/lexer.l4
-rw-r--r--frontends/verilog/parser.y10
-rw-r--r--frontends/verilog/preproc.cc122
-rw-r--r--kernel/calc.cc37
-rw-r--r--kernel/celltypes.h6
-rw-r--r--kernel/log.h54
-rw-r--r--kernel/rtlil.cc20
-rw-r--r--kernel/rtlil.h3
-rw-r--r--kernel/satgen.h85
-rw-r--r--manual/CHAPTER_CellLib.tex12
-rw-r--r--manual/command-reference-manual.tex142
-rw-r--r--passes/abc/Makefile.inc1
-rw-r--r--passes/abc/abc.cc281
-rw-r--r--passes/abc/blifparse.cc77
-rw-r--r--passes/abc/blifparse.h2
-rw-r--r--passes/abc/vlparse.cc227
-rw-r--r--passes/abc/vlparse.h28
-rw-r--r--passes/cmds/rename.cc45
-rw-r--r--passes/cmds/select.cc20
-rw-r--r--passes/extract/extract.cc2
-rw-r--r--passes/memory/memory_collect.cc21
-rw-r--r--passes/opt/opt_const.cc36
-rw-r--r--passes/proc/proc_arst.cc4
-rw-r--r--passes/sat/eval.cc2
-rw-r--r--passes/sat/freduce.cc689
-rw-r--r--passes/sat/sat.cc239
-rw-r--r--passes/techmap/dfflibmap.cc55
-rw-r--r--passes/techmap/simplemap.cc19
-rw-r--r--techlibs/common/simlib.v36
-rw-r--r--techlibs/common/stdcells.v150
-rw-r--r--tests/simple/macros.v237
-rw-r--r--tests/simple/memory.v17
-rw-r--r--tests/simple/multiplier.v132
-rw-r--r--tests/simple/undef_eqx_nex.v11
-rwxr-xr-xtests/tools/autotest.sh16
43 files changed, 2070 insertions, 873 deletions
diff --git a/CHANGELOG b/CHANGELOG
index fe0534c0..fa2c9b08 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -6,6 +6,40 @@ List of incompatible changes and major milestones between releases
Yosys 0.1.0 .. Yoys 0.1.0+
--------------------------
- - Tighter integration of ABC build with Yosys build. The make
- targets 'make abc' and 'make install-abc' are now obsolete.
+ * Improvements in Verilog frontend:
+ - Added support for local registers in named blocks
+ - Added support for "case" in "generate" blocks
+ - Added support for $clog2 system function
+ - Added preprocessor support for macro arguments
+ - Added preprocessor support for `elsif statement
+
+ * Improvements in technology mapping:
+ - The "dfflibmap" command now strongly prefers solutions with
+ no inverters in clock paths
+ - The "dfflibmap" command now prefers cells with smaller area
+
+ * Integration with ABC:
+ - Updated ABC to hg rev 57517e81666b
+ - Tighter integration of ABC build with Yosys build. The make
+ targets 'make abc' and 'make install-abc' are now obsolete.
+ - Added support for passing FFs from one clock domain through ABC
+ - Now always use BLIF as exchange format with ABC
+
+ * Improvements to "eval" and "sat" framework:
+ - Added support for "0" and "~0" in right-hand side -set expressions
+ - Added "eval -set-undef" and "eval -table"
+ - Added "sat -set-init" support for sequential problems
+ - Added undef support to SAT solver, incl. various new "sat" options
+ - Added correct support for === and !== for "eval" and "sat"
+
+ * Added "abbreviated IDs":
+ - Now $<something>$foo can be abbriviated as $foo.
+ - Usually this last part is a unique id (from RTLIL::autoidx)
+ - This abbreviated IDs are now also used in "show" output
+
+ * Various other changes to commands and options:
+ - The "ls" command now supports wildcards
+ - Added "show -pause" and "show -format dot"
+ - Added "dump -m" and "dump -n"
+ - Added "history" command
diff --git a/Makefile b/Makefile
index e4d2e510..c1af9c55 100644
--- a/Makefile
+++ b/Makefile
@@ -31,13 +31,13 @@ YOSYS_VER := 0.1.0+
GIT_REV := $(shell git rev-parse --short HEAD || echo UNKOWN)
OBJS = kernel/version_$(GIT_REV).o
-# set 'ABC = default' to use abc/ as it is
+# set 'ABCREV = default' to use abc/ as it is
#
# Note: If you do ABC development, make sure that 'abc' in this directory
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
-ABCREV = 9241719523f6
+ABCREV = 57517e81666b
ABCPULL = 1
-include Makefile.conf
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 66775b2a..924e316b 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -402,7 +402,7 @@ struct DumpPass : public Pass {
log("ilang format.\n");
log("\n");
log(" -m\n");
- log(" also dump the module headers, even if only parts of a single");
+ log(" also dump the module headers, even if only parts of a single\n");
log(" module is selected\n");
log("\n");
log(" -n\n");
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index ff41c2e3..d8160c97 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -506,12 +506,14 @@ bool dump_cell_expr(FILE *f, std::string indent, RTLIL::Cell *cell)
HANDLE_BINOP("$sshl", "<<<")
HANDLE_BINOP("$sshr", ">>>")
- HANDLE_BINOP("$lt", "<")
- HANDLE_BINOP("$le", "<=")
- HANDLE_BINOP("$eq", "==")
- HANDLE_BINOP("$ne", "!=")
- HANDLE_BINOP("$ge", ">=")
- HANDLE_BINOP("$gt", ">")
+ HANDLE_BINOP("$lt", "<")
+ HANDLE_BINOP("$le", "<=")
+ HANDLE_BINOP("$eq", "==")
+ HANDLE_BINOP("$ne", "!=")
+ HANDLE_BINOP("$eqx", "===")
+ HANDLE_BINOP("$nex", "!==")
+ HANDLE_BINOP("$ge", ">=")
+ HANDLE_BINOP("$gt", ">")
HANDLE_BINOP("$add", "+")
HANDLE_BINOP("$sub", "-")
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 0e65f1cb..20158488 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -103,6 +103,8 @@ std::string AST::type2str(AstNodeType type)
X(AST_LE)
X(AST_EQ)
X(AST_NE)
+ X(AST_EQX)
+ X(AST_NEX)
X(AST_GE)
X(AST_GT)
X(AST_ADD)
@@ -539,6 +541,8 @@ void AstNode::dumpVlog(FILE *f, std::string indent)
if (0) { case AST_LE: txt = "<="; }
if (0) { case AST_EQ: txt = "=="; }
if (0) { case AST_NE: txt = "!="; }
+ if (0) { case AST_EQX: txt = "==="; }
+ if (0) { case AST_NEX: txt = "!=="; }
if (0) { case AST_GE: txt = ">="; }
if (0) { case AST_GT: txt = ">"; }
if (0) { case AST_ADD: txt = "+"; }
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index f8e27927..22853d0f 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -82,6 +82,8 @@ namespace AST
AST_LE,
AST_EQ,
AST_NE,
+ AST_EQX,
+ AST_NEX,
AST_GE,
AST_GT,
AST_ADD,
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 269752df..e44b2d36 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -728,6 +728,8 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint)
case AST_LE:
case AST_EQ:
case AST_NE:
+ case AST_EQX:
+ case AST_NEX:
case AST_GE:
case AST_GT:
width_hint = std::max(width_hint, 1);
@@ -1113,12 +1115,14 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
}
// generate cells for binary operations: $lt, $le, $eq, $ne, $ge, $gt
- if (0) { case AST_LT: type_name = "$lt"; }
- if (0) { case AST_LE: type_name = "$le"; }
- if (0) { case AST_EQ: type_name = "$eq"; }
- if (0) { case AST_NE: type_name = "$ne"; }
- if (0) { case AST_GE: type_name = "$ge"; }
- if (0) { case AST_GT: type_name = "$gt"; }
+ if (0) { case AST_LT: type_name = "$lt"; }
+ if (0) { case AST_LE: type_name = "$le"; }
+ if (0) { case AST_EQ: type_name = "$eq"; }
+ if (0) { case AST_NE: type_name = "$ne"; }
+ if (0) { case AST_EQX: type_name = "$eqx"; }
+ if (0) { case AST_NEX: type_name = "$nex"; }
+ if (0) { case AST_GE: type_name = "$ge"; }
+ if (0) { case AST_GT: type_name = "$gt"; }
{
int width = std::max(width_hint, 1);
width_hint = -1, sign_hint = true;
@@ -1267,6 +1271,8 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
cell->parameters["\\CLK_ENABLE"] = RTLIL::Const(0);
cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(0);
+
+ cell->parameters["\\PRIORITY"] = RTLIL::Const(RTLIL::autoidx-1);
}
break;
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index f6df0c17..9b8ed760 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -299,6 +299,8 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
case AST_LE:
case AST_EQ:
case AST_NE:
+ case AST_EQX:
+ case AST_NEX:
case AST_GE:
case AST_GT:
width_hint = -1;
@@ -495,8 +497,9 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
if (width != int(children[0]->bits.size())) {
RTLIL::SigSpec sig(children[0]->bits);
sig.extend_u0(width, children[0]->is_signed);
- delete children[0];
+ AstNode *old_child_0 = children[0];
children[0] = mkconst_bits(sig.as_const().bits, children[0]->is_signed);
+ delete old_child_0;
}
children[0]->is_signed = is_signed;
}
@@ -1258,12 +1261,14 @@ skip_dynamic_range_lvalue_expansion:;
newNode = mkconst_bits(y.bits, sign_hint);
}
break;
- if (0) { case AST_LT: const_func = RTLIL::const_lt; }
- if (0) { case AST_LE: const_func = RTLIL::const_le; }
- if (0) { case AST_EQ: const_func = RTLIL::const_eq; }
- if (0) { case AST_NE: const_func = RTLIL::const_ne; }
- if (0) { case AST_GE: const_func = RTLIL::const_ge; }
- if (0) { case AST_GT: const_func = RTLIL::const_gt; }
+ if (0) { case AST_LT: const_func = RTLIL::const_lt; }
+ if (0) { case AST_LE: const_func = RTLIL::const_le; }
+ if (0) { case AST_EQ: const_func = RTLIL::const_eq; }
+ if (0) { case AST_NE: const_func = RTLIL::const_ne; }
+ if (0) { case AST_EQX: const_func = RTLIL::const_eqx; }
+ if (0) { case AST_NEX: const_func = RTLIL::const_nex; }
+ if (0) { case AST_GE: const_func = RTLIL::const_ge; }
+ if (0) { case AST_GT: const_func = RTLIL::const_gt; }
if (children[0]->type == AST_CONSTANT && children[1]->type == AST_CONSTANT) {
int cmp_width = std::max(children[0]->bits.size(), children[1]->bits.size());
bool cmp_signed = children[0]->is_signed && children[1]->is_signed;
diff --git a/frontends/verilog/lexer.l b/frontends/verilog/lexer.l
index a0deb755..9e606d90 100644
--- a/frontends/verilog/lexer.l
+++ b/frontends/verilog/lexer.l
@@ -232,8 +232,8 @@ supply1 { return TOK_SUPPLY1; }
"<=" { return OP_LE; }
">=" { return OP_GE; }
-"===" { return OP_EQ; }
-"!==" { return OP_NE; }
+"===" { return OP_EQX; }
+"!==" { return OP_NEX; }
"~&" { return OP_NAND; }
"~|" { return OP_NOR; }
diff --git a/frontends/verilog/parser.y b/frontends/verilog/parser.y
index f47d1785..874482d6 100644
--- a/frontends/verilog/parser.y
+++ b/frontends/verilog/parser.y
@@ -117,7 +117,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
%left '|' OP_NOR
%left '^' OP_XNOR
%left '&' OP_NAND
-%left OP_EQ OP_NE
+%left OP_EQ OP_NE OP_EQX OP_NEX
%left '<' OP_LE OP_GE '>'
%left OP_SHL OP_SHR OP_SSHL OP_SSHR
%left '+' '-'
@@ -1161,6 +1161,14 @@ basic_expr:
$$ = new AstNode(AST_NE, $1, $4);
append_attr($$, $3);
} |
+ basic_expr OP_EQX attr basic_expr {
+ $$ = new AstNode(AST_EQX, $1, $4);
+ append_attr($$, $3);
+ } |
+ basic_expr OP_NEX attr basic_expr {
+ $$ = new AstNode(AST_NEX, $1, $4);
+ append_attr($$, $3);
+ } |
basic_expr OP_GE attr basic_expr {
$$ = new AstNode(AST_GE, $1, $4);
append_attr($$, $3);
diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index 8d435d94..5cfa0f24 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -76,8 +76,9 @@ static char next_char()
return ch == '\r' ? next_char() : ch;
}
-static void skip_spaces()
+static std::string skip_spaces()
{
+ std::string spaces;
while (1) {
char ch = next_char();
if (ch == 0)
@@ -86,7 +87,9 @@ static void skip_spaces()
return_char(ch);
break;
}
+ spaces += ch;
}
+ return spaces;
}
static std::string next_token(bool pass_newline = false)
@@ -170,13 +173,14 @@ static std::string next_token(bool pass_newline = false)
else
{
const char *ok = "abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ$0123456789";
- while ((ch = next_char()) != 0) {
- if (strchr(ok, ch) == NULL) {
- return_char(ch);
- break;
+ if (ch == '`' || strchr(ok, ch) != NULL)
+ while ((ch = next_char()) != 0) {
+ if (strchr(ok, ch) == NULL) {
+ return_char(ch);
+ break;
+ }
+ token += ch;
}
- token += ch;
- }
}
return token;
@@ -200,8 +204,10 @@ static void input_file(FILE *f, std::string filename)
std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::map<std::string, std::string> pre_defines_map, const std::list<std::string> include_dirs)
{
+ std::set<std::string> defines_with_args;
std::map<std::string, std::string> defines_map(pre_defines_map);
int ifdef_fail_level = 0;
+ bool in_elseif = false;
output_code.clear();
input_buffer.clear();
@@ -218,17 +224,29 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
if (tok == "`endif") {
if (ifdef_fail_level > 0)
ifdef_fail_level--;
+ if (ifdef_fail_level == 0)
+ in_elseif = false;
continue;
}
if (tok == "`else") {
if (ifdef_fail_level == 0)
ifdef_fail_level = 1;
- else if (ifdef_fail_level == 1)
+ else if (ifdef_fail_level == 1 && !in_elseif)
ifdef_fail_level = 0;
continue;
}
+ if (tok == "`elsif") {
+ skip_spaces();
+ std::string name = next_token(true);
+ if (ifdef_fail_level == 0)
+ ifdef_fail_level = 1, in_elseif = true;
+ else if (ifdef_fail_level == 1 && defines_map.count(name) != 0)
+ ifdef_fail_level = 0, in_elseif = true;
+ continue;
+ }
+
if (tok == "`ifdef") {
skip_spaces();
std::string name = next_token(true);
@@ -289,32 +307,58 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
if (tok == "`define") {
std::string name, value;
+ std::map<std::string, int> args;
skip_spaces();
name = next_token(true);
- skip_spaces();
int newline_count = 0;
+ int state = 0;
+ if (skip_spaces() != "")
+ state = 3;
while (!tok.empty()) {
tok = next_token();
- if (tok == "\n") {
- return_char('\n');
- break;
- }
- if (tok == "\\") {
- char ch = next_char();
- if (ch == '\n') {
- value += " ";
- newline_count++;
- } else {
- value += std::string("\\");
- return_char(ch);
- }
+ if (state == 0 && tok == "(") {
+ state = 1;
+ skip_spaces();
} else
- value += tok;
+ if (state == 1) {
+ if (tok == ")")
+ state = 2;
+ else if (tok != ",") {
+ int arg_idx = args.size()+1;
+ args[tok] = arg_idx;
+ }
+ skip_spaces();
+ } else {
+ if (state != 2)
+ state = 3;
+ if (tok == "\n") {
+ return_char('\n');
+ break;
+ }
+ if (tok == "\\") {
+ char ch = next_char();
+ if (ch == '\n') {
+ value += " ";
+ newline_count++;
+ } else {
+ value += std::string("\\");
+ return_char(ch);
+ }
+ } else
+ if (args.count(tok) > 0)
+ value += stringf("`macro_%s_arg%d", name.c_str(), args.at(tok));
+ else
+ value += tok;
+ }
}
while (newline_count-- > 0)
return_char('\n');
// printf("define: >>%s<< -> >>%s<<\n", name.c_str(), value.c_str());
defines_map[name] = value;
+ if (state == 2)
+ defines_with_args.insert(name);
+ else
+ defines_with_args.erase(name);
continue;
}
@@ -324,6 +368,7 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
name = next_token(true);
// printf("undef: >>%s<<\n", name.c_str());
defines_map.erase(name);
+ defines_with_args.erase(name);
continue;
}
@@ -338,8 +383,35 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
}
if (tok.size() > 1 && tok[0] == '`' && defines_map.count(tok.substr(1)) > 0) {
- // printf("expand: >>%s<< -> >>%s<<\n", tok.c_str(), defines_map[tok.substr(1)].c_str());
- insert_input(defines_map[tok.substr(1)]);
+ std::string name = tok.substr(1);
+ // printf("expand: >>%s<< -> >>%s<<\n", name.c_str(), defines_map[name].c_str());
+ std::string skipped_spaces = skip_spaces();
+ tok = next_token(true);
+ if (tok == "(" && defines_with_args.count(name) > 0) {
+ int level = 1;
+ std::vector<std::string> args;
+ args.push_back(std::string());
+ while (1)
+ {
+ tok = next_token(true);
+ if (tok == ")" || tok == "}" || tok == "]")
+ level--;
+ if (level == 0)
+ break;
+ if (level == 1 && tok == ",")
+ args.push_back(std::string());
+ else
+ args.back() += tok;
+ if (tok == "(" || tok == "{" || tok == "[")
+ level++;
+ }
+ for (size_t i = 0; i < args.size(); i++)
+ defines_map[stringf("macro_%s_arg%d", name.c_str(), i+1)] = args[i];
+ } else {
+ insert_input(tok);
+ insert_input(skipped_spaces);
+ }
+ insert_input(defines_map[name]);
continue;
}
diff --git a/kernel/calc.cc b/kernel/calc.cc
index 61025104..a56db93a 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -386,6 +386,35 @@ RTLIL::Const RTLIL::const_ne(const RTLIL::Const &arg1, const RTLIL::Const &arg2,
return result;
}
+RTLIL::Const RTLIL::const_eqx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+ RTLIL::Const arg1_ext = arg1;
+ RTLIL::Const arg2_ext = arg2;
+ RTLIL::Const result(RTLIL::State::S0, result_len);
+
+ int width = std::max(arg1_ext.bits.size(), arg2_ext.bits.size());
+ extend_u0(arg1_ext, width, signed1 && signed2);
+ extend_u0(arg2_ext, width, signed1 && signed2);
+
+ for (size_t i = 0; i < arg1_ext.bits.size(); i++) {
+ if (arg1_ext.bits.at(i) != arg2_ext.bits.at(i))
+ return result;
+ }
+
+ result.bits.front() = RTLIL::State::S1;
+ return result;
+}
+
+RTLIL::Const RTLIL::const_nex(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+ RTLIL::Const result = RTLIL::const_eqx(arg1, arg2, signed1, signed2, result_len);
+ if (result.bits.front() == RTLIL::State::S0)
+ result.bits.front() = RTLIL::State::S1;
+ else if (result.bits.front() == RTLIL::State::S1)
+ result.bits.front() = RTLIL::State::S0;
+ return result;
+}
+
RTLIL::Const RTLIL::const_ge(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
{
int undef_bit_pos = -1;
@@ -514,6 +543,14 @@ RTLIL::Const RTLIL::const_pos(const RTLIL::Const &arg1, const RTLIL::Const&, boo
return arg1_ext;
}
+RTLIL::Const RTLIL::const_bu0(const RTLIL::Const &arg1, const RTLIL::Const&, bool signed1, bool, int result_len)
+{
+ RTLIL::Const arg1_ext = arg1;
+ extend_u0(arg1_ext, result_len, signed1);
+
+ return arg1_ext;
+}
+
RTLIL::Const RTLIL::const_neg(const RTLIL::Const &arg1, const RTLIL::Const&, bool signed1, bool, int result_len)
{
RTLIL::Const arg1_ext = arg1;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index e59f74d6..2f311c82 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -60,6 +60,7 @@ struct CellTypes
{
cell_types.insert("$not");
cell_types.insert("$pos");
+ cell_types.insert("$bu0");
cell_types.insert("$neg");
cell_types.insert("$and");
cell_types.insert("$or");
@@ -78,6 +79,8 @@ struct CellTypes
cell_types.insert("$le");
cell_types.insert("$eq");
cell_types.insert("$ne");
+ cell_types.insert("$eqx");
+ cell_types.insert("$nex");
cell_types.insert("$ge");
cell_types.insert("$gt");
cell_types.insert("$add");
@@ -237,6 +240,8 @@ struct CellTypes
HANDLE_CELL_TYPE(le)
HANDLE_CELL_TYPE(eq)
HANDLE_CELL_TYPE(ne)
+ HANDLE_CELL_TYPE(eqx)
+ HANDLE_CELL_TYPE(nex)
HANDLE_CELL_TYPE(ge)
HANDLE_CELL_TYPE(gt)
HANDLE_CELL_TYPE(add)
@@ -246,6 +251,7 @@ struct CellTypes
HANDLE_CELL_TYPE(mod)
HANDLE_CELL_TYPE(pow)
HANDLE_CELL_TYPE(pos)
+ HANDLE_CELL_TYPE(bu0)
HANDLE_CELL_TYPE(neg)
#undef HANDLE_CELL_TYPE
diff --git a/kernel/log.h b/kernel/log.h
index d88dda88..5ee6b565 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -93,4 +93,58 @@ struct PerformanceTimer
#endif
};
+// simple API for quickly dumping values when debugging
+
+static inline void log_dump_val_worker(int v) { log("%d", v); }
+static inline void log_dump_val_worker(size_t v) { log("%zd", v); }
+static inline void log_dump_val_worker(long int v) { log("%ld", v); }
+static inline void log_dump_val_worker(long long int v) { log("%lld", v); }
+static inline void log_dump_val_worker(char c) { log(c >= 32 && c < 127 ? "'%c'" : "'\\x%02x'", c); }
+static inline void log_dump_val_worker(bool v) { log("%s", v ? "true" : "false"); }
+static inline void log_dump_val_worker(double v) { log("%f", v); }
+static inline void log_dump_val_worker(const char *v) { log("%s", v); }
+static inline void log_dump_val_worker(std::string v) { log("%s", v.c_str()); }
+static inline void log_dump_val_worker(RTLIL::SigSpec v) { log("%s", log_signal(v)); }
+static inline void log_dump_args_worker(const char *p) { log_assert(*p == 0); }
+
+template <typename T, typename ... Args>
+void log_dump_args_worker(const char *p, T first, Args ... args)
+{
+ int next_p_state = 0;
+ const char *next_p = p;
+ while (*next_p && (next_p_state != 0 || *next_p != ',')) {
+ if (*next_p == '"')
+ do {
+ next_p++;
+ while (*next_p == '\\' && *(next_p + 1))
+ next_p += 2;
+ } while (*next_p && *next_p != '"');
+ if (*next_p == '\'') {
+ next_p++;
+ if (*next_p == '\\')
+ next_p++;
+ if (*next_p)
+ next_p++;
+ }
+ if (*next_p == '(' || *next_p == '[' || *next_p == '{')
+ next_p_state++;
+ if ((*next_p == ')' || *next_p == ']' || *next_p == '}') && next_p_state > 0)
+ next_p_state--;
+ next_p++;
+ }
+ log("\n\t%.*s => ", int(next_p - p), p);
+ if (*next_p == ',')
+ next_p++;
+ while (*next_p == ' ' || *next_p == '\t' || *next_p == '\r' || *next_p == '\n')
+ next_p++;
+ log_dump_val_worker(first);
+ log_dump_args_worker(next_p, args ...);
+}
+
+#define log_dump(...) do { \
+ log("DEBUG DUMP IN %s AT %s:%d:", __PRETTY_FUNCTION__, __FILE__, __LINE__); \
+ log_dump_args_worker(#__VA_ARGS__, __VA_ARGS__); \
+ log("\n"); \
+} while (0)
+
#endif
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 9dfe196d..1311f31c 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -337,7 +337,7 @@ namespace {
expected_ports.insert(name);
}
- void check_expected()
+ void check_expected(bool check_matched_sign = true)
{
for (auto &para : cell->parameters)
if (expected_params.count(para.first) == 0)
@@ -345,6 +345,13 @@ namespace {
for (auto &conn : cell->connections)
if (expected_ports.count(conn.first) == 0)
error(__LINE__);
+
+ if (expected_params.count("\\A_SIGNED") != 0 && expected_params.count("\\B_SIGNED") && check_matched_sign) {
+ bool a_is_signed = param("\\A_SIGNED") != 0;
+ bool b_is_signed = param("\\B_SIGNED") != 0;
+ if (a_is_signed != b_is_signed)
+ error(__LINE__);
+ }
}
void check_gate(const char *ports)
@@ -370,7 +377,7 @@ namespace {
void check()
{
- if (cell->type == "$not" || cell->type == "$pos" || cell->type == "$neg") {
+ if (cell->type == "$not" || cell->type == "$pos" || cell->type == "$bu0" || cell->type == "$neg") {
param("\\A_SIGNED");
port("\\A", param("\\A_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
@@ -403,12 +410,12 @@ namespace {
port("\\A", param("\\A_WIDTH"));
port("\\B", param("\\B_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
- check_expected();
+ check_expected(false);
return;
}
if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
- cell->type == "$ge" || cell->type == "$gt") {
+ cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt") {
param("\\A_SIGNED");
param("\\B_SIGNED");
port("\\A", param("\\A_WIDTH"));
@@ -425,7 +432,7 @@ namespace {
port("\\A", param("\\A_WIDTH"));
port("\\B", param("\\B_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
- check_expected();
+ check_expected(cell->type != "$pow");
return;
}
@@ -443,7 +450,7 @@ namespace {
port("\\A", param("\\A_WIDTH"));
port("\\B", param("\\B_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
- check_expected();
+ check_expected(false);
return;
}
@@ -560,6 +567,7 @@ namespace {
param("\\MEMID");
param("\\CLK_ENABLE");
param("\\CLK_POLARITY");
+ param("\\PRIORITY");
port("\\CLK", 1);
port("\\EN", 1);
port("\\ADDR", param("\\ABITS"));
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index fbdab53e..8e3b78ee 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -174,6 +174,8 @@ namespace RTLIL
RTLIL::Const const_le (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_eq (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_ne (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+ RTLIL::Const const_eqx (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+ RTLIL::Const const_nex (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_ge (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_gt (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
@@ -185,6 +187,7 @@ namespace RTLIL
RTLIL::Const const_pow (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_pos (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+ RTLIL::Const const_bu0 (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_neg (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
};
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 35e15aa6..208ae165 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -35,21 +35,19 @@ typedef ezSAT ezDefaultSAT;
struct SatGen
{
ezSAT *ez;
- RTLIL::Design *design;
SigMap *sigmap;
std::string prefix;
SigPool initial_state;
bool ignore_div_by_zero;
bool model_undef;
- SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
- ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
+ SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
+ ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
{
}
- void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string())
+ void setContext(SigMap *sigmap, std::string prefix = std::string())
{
- this->design = design;
this->sigmap = sigmap;
this->prefix = prefix;
}
@@ -121,11 +119,10 @@ struct SatGen
return ez->expression(ezSAT::OpAnd, eq_bits);
}
- void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool undef_mode = false)
+ void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool forced_signed = false)
{
- log_assert(!undef_mode || model_undef);
- bool is_signed = undef_mode;
- if (!undef_mode && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
+ bool is_signed = forced_signed;
+ if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
@@ -133,18 +130,16 @@ struct SatGen
vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
}
- void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool undef_mode = false)
+ void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
{
- log_assert(!undef_mode || model_undef);
- extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), undef_mode);
+ extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), forced_signed);
while (vec_y.size() < vec_a.size())
vec_y.push_back(ez->literal());
}
- void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool undef_mode = false)
+ void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
{
- log_assert(!undef_mode || model_undef);
- bool is_signed = undef_mode || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
+ bool is_signed = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
while (vec_a.size() < vec_y.size())
vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
while (vec_y.size() < vec_a.size())
@@ -161,7 +156,6 @@ struct SatGen
{
bool arith_undef_handled = false;
bool is_arith_compare = cell->type == "$lt" || cell->type == "$le" || cell->type == "$ge" || cell->type == "$gt";
- int arith_undef_result = ez->FALSE;
if (model_undef && (cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || cell->type == "$mod" || is_arith_compare))
{
@@ -191,7 +185,6 @@ struct SatGen
ez->assume(ez->vec_eq(undef_y_bits, undef_y));
}
- arith_undef_result = undef_y_bit;
arith_undef_handled = true;
}
@@ -224,7 +217,7 @@ struct SatGen
std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
- extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
if (cell->type == "$and" || cell->type == "$_AND_") {
std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
@@ -306,6 +299,9 @@ struct SatGen
std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
std::vector<int> s = importDefSigSpec(cell->connections.at("\\S"), timestep);
std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
std::vector<int> tmp = a;
for (size_t i = 0; i < s.size(); i++) {
std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
@@ -313,12 +309,24 @@ struct SatGen
}
if (cell->type == "$safe_pmux")
tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
- ez->assume(ez->vec_eq(tmp, y));
+ ez->assume(ez->vec_eq(tmp, yy));
- if (model_undef) {
- log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type));
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+ std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
- ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y)));
+
+ tmp = a;
+ for (size_t i = 0; i < s.size(); i++) {
+ std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
+ tmp = ez->vec_ite(s.at(i), part_of_undef_b, tmp);
+ }
+ tmp = ez->vec_ite(ez->onehot(s, true), tmp, cell->type == "$safe_pmux" ? a : std::vector<int>(tmp.size(), ez->TRUE));
+ tmp = ez->vec_ite(ez->expression(ezSAT::OpOr, undef_s), std::vector<int>(tmp.size(), ez->TRUE), tmp);
+ ez->assume(ez->vec_eq(tmp, undef_y));
+ undefGating(y, yy, undef_y);
}
return true;
}
@@ -451,7 +459,7 @@ struct SatGen
return true;
}
- if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt")
+ if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt")
{
bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
@@ -461,13 +469,21 @@ struct SatGen
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+ a = ez->vec_or(a, undef_a);
+ b = ez->vec_or(b, undef_b);
+ }
+
if (cell->type == "$lt")
ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
if (cell->type == "$le")
ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
- if (cell->type == "$eq")
+ if (cell->type == "$eq" || cell->type == "$eqx")
ez->SET(ez->vec_eq(a, b), yy.at(0));
- if (cell->type == "$ne")
+ if (cell->type == "$ne" || cell->type == "$nex")
ez->SET(ez->vec_ne(a, b), yy.at(0));
if (cell->type == "$ge")
ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
@@ -476,7 +492,24 @@ struct SatGen
for (size_t i = 1; i < y.size(); i++)
ez->SET(ez->FALSE, yy.at(i));
- if (model_undef && (cell->type == "$eq" || cell->type == "$ne"))
+ if (model_undef && (cell->type == "$eqx" || cell->type == "$nex"))
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+
+ if (cell->type == "$eqx")
+ yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+ else
+ yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
+
+ for (size_t i = 0; i < y.size(); i++)
+ ez->SET(ez->FALSE, undef_y.at(i));
+
+ ez->assume(ez->vec_eq(y, yy));
+ }
+ else if (model_undef && (cell->type == "$eq" || cell->type == "$ne"))
{
std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index 09be0870..b84e1b30 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -97,6 +97,12 @@ The width of the output port \B{Y}.
Table~\ref{tab:CellLib_binary} lists all cells for binary RTL operators.
+The additional cell type {\tt \$bu0} is similar to {\tt \$pos}, but always
+extends unsigned arguments with zeros. ({\tt \$pos} extends unsigned arguments
+with {\tt x}-bits if the most significant bit is {\tt x}.) This is used
+internally to correctly implement the {\tt ==} and {\tt !=} operators for
+constant arguments.
+
\subsection{Multiplexers}
Multiplexers are generated by the Verilog HDL frontend for {\tt
@@ -147,6 +153,9 @@ Verilog & Cell Type \\
\hline
\lstinline[language=Verilog]; Y = A && B; & {\tt \$logic\_and} \\
\lstinline[language=Verilog]; Y = A || B; & {\tt \$logic\_or} \\
+\hline
+\lstinline[language=Verilog]; Y = A === B; & {\tt \$eqx} \\
+\lstinline[language=Verilog]; Y = A !== B; & {\tt \$nex} \\
\end{tabular}
\hfil
\begin{tabular}[t]{ll}
@@ -263,6 +272,9 @@ the \B{CLK} input is not used.
\item \B{CLK\_POLARITY} \\
Clock is active on positive edge if this parameter has the value {\tt 1'b1} and on the negative
edge if this parameter is {\tt 1'b0}.
+
+\item \B{PRIORITY} \\
+The cell with the higher integer value in this parameter wins a write conflict.
\end{itemize}
The HDL frontend models a memory using RTLIL::Memory objects and asynchronous
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index 1c91cb66..54fec542 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -131,6 +131,13 @@ first run this pass and then map the logic paths to the target technology.
Write the selected parts of the design to the console or specified file in
ilang format.
+ -m
+ also dump the module headers, even if only parts of a single
+ module is selected
+
+ -n
+ only dump the module headers if the entire module is selected
+
-outfile <filename>
Write to the specified file.
\end{lstlisting}
@@ -146,6 +153,12 @@ inputs.
-set <signal> <value>
set the specified signal to the specified value.
+ -set-undef
+ set all unspecified source signals to undef (x)
+
+ -table <signal>
+ create a truth table using the specified input signals
+
-show <signal>
show the value for the specified signal. if no -show option is passed
then all output ports of the current module are used.
@@ -423,6 +436,10 @@ needed.
use the specified top module to built a design hierarchy. modules
outside this tree (unused modules) are removed.
+ when the -top option is used, the 'top' attribute will be set on the
+ specified top module. otherwise a module with the 'top' attribute set
+ will implicitly be used as top module, if such a module exists.
+
In -generate mode this pass generates blackbox modules for the given cell
types (wildcards supported). For this the design is searched for cells that
match the given types and then the given port declarations are used to
@@ -440,6 +457,16 @@ This pass ignores the current selection and always operates on all modules
in the current design.
\end{lstlisting}
+\section{history -- show last interactive commands}
+\label{cmd:history}
+\begin{lstlisting}[numbers=left,frame=single]
+ history
+
+This command prints all commands in the shell history buffer. This are
+all commands executed in an interactive session, but not the commands
+from executed scripts.
+\end{lstlisting}
+
\section{iopadmap -- technology mapping of i/o pads (or buffers)}
\label{cmd:iopadmap}
\begin{lstlisting}[numbers=left,frame=single]
@@ -469,11 +496,17 @@ the resulting cells to more sophisticated PAD cells.
\section{ls -- list modules or objects in modules}
\label{cmd:ls}
\begin{lstlisting}[numbers=left,frame=single]
- ls
+ ls [pattern]
-When no active module is selected, this prints a list of all module.
+When no active module is selected, this prints a list of all modules.
When an active module is selected, this prints a list of objects in the module.
+
+If a pattern is given, the objects matching the pattern are printed
+
+Note that this command does not use the selection mechanism and always operates
+on the whole design or whole active module. Use 'select -list' to show a list
+of currently selected objects.
\end{lstlisting}
\section{memory -- translate memories to basic cells}
@@ -761,6 +794,10 @@ Verilog-2005 is supported.
don't perform basic optimizations (such as const folding) in the
high-level front-end.
+ -ignore_redef
+ ignore re-definitions of modules. (the default behavior is to
+ create an error message.)
+
-Dname[=definition]
define the preprocessor symbol 'name' and set its optional value
'definition'
@@ -800,9 +837,29 @@ and additional constraints passed as parameters.
-max <N>
like -all, but limit number of solutions to <N>
+ -enable_undef
+ enable modeling of undef value (aka 'x-bits')
+ this option is implied by -set-def, -set-undef et. cetera
+
+ -max_undef
+ maximize the number of undef bits in solutions, giving a better
+ picture of which input bits are actually vital to the solution.
+
-set <signal> <value>
set the specified signal to the specified value.
+ -set-def <signal>
+ add a constraint that all bits of the given signal must be defined
+
+ -set-any-undef <signal>
+ add a constraint that at least one bit of the given signal is undefined
+
+ -set-all-undef <signal>
+ add a constraint that all bits of the given signal are undefined
+
+ -set-def-inputs
+ add -set-def constraints for all module inputs
+
-show <signal>
show the model for the specified signal. if no -show option is
passed then a set of signals to be shown is automatically selected.
@@ -821,6 +878,17 @@ The following options can be used to set up a sequential problem:
set or unset the specified signal to the specified value in the
given timestep. this has priority over a -set for the same signal.
+ -set-def-at <N> <signal>
+ -set-any-undef-at <N> <signal>
+ -set-all-undef-at <N> <signal>
+ add undef contraints in the given timestep.
+
+ -set-init <signal> <value>
+ set the initial value for the register driving the signal to the value
+
+ -set-init-undef
+ set all initial states (not set using -set-init) to undef
+
The following additional options can be used to set up a proof. If also -seq
is passed, a temporal induction proof is performed.
@@ -829,6 +897,10 @@ is passed, a temporal induction proof is performed.
induction proof it is proven that the condition holds forever after
the number of time steps passed using -seq.
+ -prove-x <signal> <value>
+ Like -prove, but an undef (x) bit in the lhs matches any value on
+ the right hand side. Useful for equivialence checking.
+
-maxsteps <N>
Set a maximum length for the induction.
@@ -1108,6 +1180,15 @@ to a graphics file (usually SVG or PostScript).
stretch the graph so all inputs are on the left side and all outputs
(including inout ports) are on the right side.
+ -pause
+ wait for the use to press enter to before returning
+
+ -enum
+ enumerate objects with internal ($-prefixed) names
+
+ -long
+ do not abbeviate objects with internal ($-prefixed) names
+
When no <format> is specified, SVG is used. When no <format> and <viewer> is
specified, 'yosys-svgviewer' is used to display the schematic.
@@ -1115,6 +1196,20 @@ The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
unless another prefix is specified using -prefix <prefix>.
\end{lstlisting}
+\section{simplemap -- mapping simple coarse-grain cells}
+\label{cmd:simplemap}
+\begin{lstlisting}[numbers=left,frame=single]
+ simplemap [selection]
+
+This pass maps a small selection of simple coarse-grain cells to yosys gate
+primitives. The following internal cell types are mapped by this pass:
+
+ $not, $pos, $bu0, $and, $or, $xor, $xnor
+ $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool
+ $logic_not, $logic_and, $logic_or, $mux
+ $sr, $dff, $dffsr, $adff, $dlatch
+\end{lstlisting}
+
\section{splitnets -- split up multi-bit nets}
\label{cmd:splitnets}
\begin{lstlisting}[numbers=left,frame=single]
@@ -1131,6 +1226,20 @@ This command splits multi-bit nets into single-bit nets.
also split module ports. per default only internal signals are split.
\end{lstlisting}
+\section{stat -- print some statistics}
+\label{cmd:stat}
+\begin{lstlisting}[numbers=left,frame=single]
+ stat [options] [selection]
+
+Print some statistics (number of objects) on the selected portion of the
+design.
+
+ -top <module>
+ print design hierarchy with this module as top. if the design is fully
+ selected and a module has the 'top' attribute set, this module is used
+ default value for this option.
+\end{lstlisting}
+
\section{submod -- moving part of a module to a new submodule}
\label{cmd:submod}
\begin{lstlisting}[numbers=left,frame=single]
@@ -1202,7 +1311,7 @@ The following commands are executed by this synthesis command:
clean
map_cells:
- techmap -map <share_dir>/xilinx/cells.v
+ techmap -share_map xilinx/cells.v
clean
clkbuf:
@@ -1214,7 +1323,7 @@ The following commands are executed by this synthesis command:
iopadmap -outpad OBUF I:O -inpad IBUF O:I @xilinx_nonclocks
edif:
- write_edif -top <top> synth.edif
+ write_edif synth.edif
\end{lstlisting}
\section{tcl -- execute a TCL script file}
@@ -1246,12 +1355,26 @@ file.
transforms the internal RTL cells to the internal gate
library.
+ -share_map filename
+ like -map, but look for the file in the share directory (where the
+ yosys data files are). this is mainly used internally when techmap
+ is called from other commands.
+
+ -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.
+
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.
+match cells with a type that match the text value of this attribute. Otherwise
+the module name will be used to match the cell.
+
+When a module in the map file has the 'techmap_simplemap' attribute set, techmap
+will use 'simplemap' (see 'help simplemap') to map cells matching the module.
All wires in the modules from the map file matching the pattern _TECHMAP_*
or *._TECHMAP_* are special wires that are used to pass instructions from
-the mapping module to the techmap command. At the moment the following spoecial
+the mapping module to the techmap command. At the moment the following special
wires are supported:
_TECHMAP_FAIL_
@@ -1273,6 +1396,13 @@ wires are supported:
wire to start out as non-constant and evaluate to a constant value
during processing of other _TECHMAP_DO_* commands.
+In addition to this special wires, techmap also supports special parameters in
+modules in the map file:
+
+ _TECHMAP_CELLTYPE_
+ When a parameter with this name exists, it will be set to the type name
+ of the cell that matches the module.
+
When a module in the map file has a parameter where the according cell in the
design has a port, the module from the map file is only used if the port in
the design is connected to a constant value. The parameter is then set to the
diff --git a/passes/abc/Makefile.inc b/passes/abc/Makefile.inc
index dbb7496c..a7c5b02c 100644
--- a/passes/abc/Makefile.inc
+++ b/passes/abc/Makefile.inc
@@ -1,7 +1,6 @@
ifeq ($(ENABLE_ABC),1)
OBJS += passes/abc/abc.o
-OBJS += passes/abc/vlparse.o
OBJS += passes/abc/blifparse.o
endif
diff --git a/passes/abc/abc.cc b/passes/abc/abc.cc
index e37f896f..efba4359 100644
--- a/passes/abc/abc.cc
+++ b/passes/abc/abc.cc
@@ -21,6 +21,10 @@
// Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification
// http://www.eecs.berkeley.edu/~alanmi/abc/
+// [[CITE]] Berkeley Logic Interchange Format (BLIF)
+// University of California. Berkeley. July 28, 1992
+// http://www.ece.cmu.edu/~ee760/760docs/blif.pdf
+
// [[CITE]] Kahn's Topological sorting algorithm
// Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558–562, doi:10.1145/368996.369025
// http://en.wikipedia.org/wiki/Topological_sorting
@@ -36,7 +40,6 @@
#include <dirent.h>
#include <sstream>
-#include "vlparse.h"
#include "blifparse.h"
struct gate_t
@@ -54,6 +57,9 @@ static RTLIL::Module *module;
static std::vector<gate_t> signal_list;
static std::map<RTLIL::SigSpec, int> signal_map;
+static bool clk_polarity;
+static RTLIL::SigSpec clk_sig;
+
static int map_signal(RTLIL::SigSpec sig, char gate_type = -1, int in1 = -1, int in2 = -1, int in3 = -1)
{
assert(sig.width == 1);
@@ -100,6 +106,26 @@ static void mark_port(RTLIL::SigSpec sig)
static void extract_cell(RTLIL::Cell *cell)
{
+ if (cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")
+ {
+ if (clk_polarity != (cell->type == "$_DFF_P_"))
+ return;
+ if (clk_sig != assign_map(cell->connections["\\C"]))
+ return;
+
+ RTLIL::SigSpec sig_d = cell->connections["\\D"];
+ RTLIL::SigSpec sig_q = cell->connections["\\Q"];
+
+ assign_map.apply(sig_d);
+ assign_map.apply(sig_q);
+
+ map_signal(sig_q, 'f', map_signal(sig_d));
+
+ module->cells.erase(cell->name);
+ delete cell;
+ return;
+ }
+
if (cell->type == "$_INV_")
{
RTLIL::SigSpec sig_a = cell->connections["\\A"];
@@ -135,7 +161,7 @@ static void extract_cell(RTLIL::Cell *cell)
else if (cell->type == "$_XOR_")
map_signal(sig_y, 'x', mapped_a, mapped_b);
else
- abort();
+ log_abort();
module->cells.erase(cell->name);
delete cell;
@@ -217,20 +243,21 @@ static void handle_loops()
// dot_f = fopen("test.dot", "w");
for (auto &g : signal_list) {
- if (g.type == -1) {
+ if (g.type == -1 || g.type == 'f') {
workpool.insert(g.id);
- }
- if (g.in1 >= 0) {
- edges[g.in1].insert(g.id);
- in_edges_count[g.id]++;
- }
- if (g.in2 >= 0 && g.in2 != g.in1) {
- edges[g.in2].insert(g.id);
- in_edges_count[g.id]++;
- }
- if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
- edges[g.in3].insert(g.id);
- in_edges_count[g.id]++;
+ } else {
+ if (g.in1 >= 0) {
+ edges[g.in1].insert(g.id);
+ in_edges_count[g.id]++;
+ }
+ if (g.in2 >= 0 && g.in2 != g.in1) {
+ edges[g.in2].insert(g.id);
+ in_edges_count[g.id]++;
+ }
+ if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
+ edges[g.in3].insert(g.id);
+ in_edges_count[g.id]++;
+ }
}
}
@@ -327,7 +354,8 @@ static void handle_loops()
fclose(dot_f);
}
-static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file, std::string liberty_file, std::string constr_file, bool cleanup, int lut_mode)
+static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
+ std::string liberty_file, std::string constr_file, bool cleanup, int lut_mode, bool dff_mode, std::string clk_str)
{
module = current_module;
map_autoidx = RTLIL::autoidx++;
@@ -336,14 +364,56 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
signal_list.clear();
assign_map.set(module);
+ clk_polarity = true;
+ clk_sig = RTLIL::SigSpec();
+
char tempdir_name[] = "/tmp/yosys-abc-XXXXXX";
if (!cleanup)
tempdir_name[0] = tempdir_name[4] = '_';
char *p = mkdtemp(tempdir_name);
- log_header("Extracting gate netlist of module `%s' to `%s/input.v'..\n", module->name.c_str(), tempdir_name);
+ log_header("Extracting gate netlist of module `%s' to `%s/input.blif'..\n", module->name.c_str(), tempdir_name);
if (p == NULL)
log_error("For some reason mkdtemp() failed!\n");
+ if (clk_str.empty()) {
+ if (clk_str[0] == '!') {
+ clk_polarity = false;
+ clk_str = clk_str.substr(1);
+ }
+ if (module->wires.count(RTLIL::escape_id(clk_str)) != 0)
+ clk_sig = assign_map(RTLIL::SigSpec(module->wires.at(RTLIL::escape_id(clk_str)), 1));
+ }
+
+ if (dff_mode && clk_sig.width == 0)
+ {
+ int best_dff_counter = 0;
+ std::map<std::pair<bool, RTLIL::SigSpec>, int> dff_counters;
+
+ for (auto &it : module->cells)
+ {
+ RTLIL::Cell *cell = it.second;
+ if (cell->type != "$_DFF_N_" && cell->type != "$_DFF_P_")
+ continue;
+
+ std::pair<bool, RTLIL::SigSpec> key(cell->type == "$_DFF_P_", assign_map(cell->connections.at("\\C")));
+ if (++dff_counters[key] > best_dff_counter) {
+ best_dff_counter = dff_counters[key];
+ clk_polarity = key.first;
+ clk_sig = key.second;
+ }
+ }
+ }
+
+ if (dff_mode || !clk_str.empty()) {
+ if (clk_sig.width == 0)
+ log("No (matching) clock domain found. Not extracting any FF cells.\n");
+ else
+ log("Found (matching) %s clock domain: %s\n", clk_polarity ? "posedge" : "negedge", log_signal(clk_sig));
+ }
+
+ if (clk_sig.width != 0)
+ mark_port(clk_sig);
+
std::vector<RTLIL::Cell*> cells;
cells.reserve(module->cells.size());
for (auto &it : module->cells)
@@ -363,60 +433,75 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
handle_loops();
- if (asprintf(&p, "%s/input.v", tempdir_name) < 0) abort();
+ if (asprintf(&p, "%s/input.blif", tempdir_name) < 0) log_abort();
FILE *f = fopen(p, "wt");
if (f == NULL)
log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
free(p);
- fprintf(f, "module netlist (");
- bool first = true;
+ fprintf(f, ".model netlist\n");
+
+ int count_input = 0;
+ fprintf(f, ".inputs");
for (auto &si : signal_list) {
- if (!si.is_port)
+ if (!si.is_port || si.type >= 0)
continue;
- if (!first)
- fprintf(f, ", ");
- fprintf(f, "n%d", si.id);
- first = false;
+ fprintf(f, " n%d", si.id);
+ count_input++;
}
- fprintf(f, "); // %s\n", module->name.c_str());
+ fprintf(f, "\n");
- int count_input = 0, count_output = 0;
+ int count_output = 0;
+ fprintf(f, ".outputs");
for (auto &si : signal_list) {
- if (si.is_port) {
- if (si.type >= 0)
- count_output++;
- else
- count_input++;
- }
- fprintf(f, "%s n%d; // %s\n", si.is_port ? si.type >= 0 ?
- "output" : "input" : "wire", si.id, log_signal(si.sig));
+ if (!si.is_port || si.type < 0)
+ continue;
+ fprintf(f, " n%d", si.id);
+ count_output++;
}
+ fprintf(f, "\n");
+
+ for (auto &si : signal_list)
+ fprintf(f, "# n%-5d %s\n", si.id, log_signal(si.sig));
+
for (auto &si : signal_list) {
assert(si.sig.width == 1 && si.sig.chunks.size() == 1);
- if (si.sig.chunks[0].wire == NULL)
- fprintf(f, "assign n%d = %c;\n", si.id, si.sig.chunks[0].data.bits[0] == RTLIL::State::S1 ? '1' : '0');
+ if (si.sig.chunks[0].wire == NULL) {
+ fprintf(f, ".names n%d\n", si.id);
+ if (si.sig.chunks[0].data.bits[0] == RTLIL::State::S1)
+ fprintf(f, "1\n");
+ }
}
int count_gates = 0;
for (auto &si : signal_list) {
- if (si.type == 'n')
- fprintf(f, "not (n%d, n%d);\n", si.id, si.in1);
- else if (si.type == 'a')
- fprintf(f, "and (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
- else if (si.type == 'o')
- fprintf(f, "or (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
- else if (si.type == 'x')
- fprintf(f, "xor (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
- else if (si.type == 'm')
- fprintf(f, "assign n%d = n%d ? n%d : n%d;\n", si.id, si.in3, si.in2, si.in1);
- else if (si.type >= 0)
- abort();
+ if (si.type == 'n') {
+ fprintf(f, ".names n%d n%d\n", si.in1, si.id);
+ fprintf(f, "0 1\n");
+ } else if (si.type == 'a') {
+ fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+ fprintf(f, "11 1\n");
+ } else if (si.type == 'o') {
+ fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+ fprintf(f, "-1 1\n");
+ fprintf(f, "1- 1\n");
+ } else if (si.type == 'x') {
+ fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+ fprintf(f, "01 1\n");
+ fprintf(f, "10 1\n");
+ } else if (si.type == 'm') {
+ fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
+ fprintf(f, "1-0 1\n");
+ fprintf(f, "-11 1\n");
+ } else if (si.type == 'f') {
+ fprintf(f, ".latch n%d n%d\n", si.in1, si.id);
+ } else if (si.type >= 0)
+ log_abort();
if (si.type >= 0)
count_gates++;
}
- fprintf(f, "endmodule\n");
+ fprintf(f, ".end\n");
fclose(f);
log("Extracted %d gates and %zd wires to a netlist network with %d inputs and %d outputs.\n",
@@ -427,7 +512,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
{
log_header("Executing ABC.\n");
- if (asprintf(&p, "%s/stdcells.genlib", tempdir_name) < 0) abort();
+ if (asprintf(&p, "%s/stdcells.genlib", tempdir_name) < 0) log_abort();
f = fopen(p, "wt");
if (f == NULL)
log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -443,7 +528,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
free(p);
if (lut_mode) {
- if (asprintf(&p, "%s/lutdefs.txt", tempdir_name) < 0) abort();
+ if (asprintf(&p, "%s/lutdefs.txt", tempdir_name) < 0) log_abort();
f = fopen(p, "wt");
if (f == NULL)
log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -457,7 +542,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
int buffer_pos = 0;
if (!liberty_file.empty()) {
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; read_lib %s; ",
+ "%s -s -c 'read_blif %s/input.blif; read_lib %s; ",
exe_file.c_str(), tempdir_name, liberty_file.c_str());
if (!constr_file.empty())
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
@@ -470,21 +555,18 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
} else
if (!script_file.empty())
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; source %s; ",
+ "%s -s -c 'read_blif %s/input.blif; source %s; ",
exe_file.c_str(), tempdir_name, script_file.c_str());
else
if (lut_mode)
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; read_lut %s/lutdefs.txt; strash; balance; dch; if; ",
+ "%s -s -c 'read_blif %s/input.blif; read_lut %s/lutdefs.txt; strash; balance; dch; if; ",
exe_file.c_str(), tempdir_name, tempdir_name);
else
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
+ "%s -s -c 'read_blif %s/input.blif; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
exe_file.c_str(), tempdir_name, tempdir_name);
- if (lut_mode)
- buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
- else
- buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_verilog %s/output.v' 2>&1", tempdir_name);
+ buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
errno = ENOMEM; // popen does not set errno if memory allocation fails, therefore set it by hand
f = popen(buffer, "r");
@@ -504,16 +586,14 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
}
}
- if (asprintf(&p, "%s/%s", tempdir_name, lut_mode ? "output.blif" : "output.v") < 0) abort();
+ if (asprintf(&p, "%s/%s", tempdir_name, "output.blif") < 0) log_abort();
f = fopen(p, "rt");
if (f == NULL)
log_error("Can't open ABC output file `%s'.\n", p);
-#if 0
- RTLIL::Design *mapped_design = new RTLIL::Design;
- frontend_register["verilog"]->execute(f, p, std::vector<std::string>(), mapped_design);
-#else
- RTLIL::Design *mapped_design = lut_mode ? abc_parse_blif(f) : abc_parse_verilog(f);
-#endif
+
+ bool builtin_lib = liberty_file.empty() && script_file.empty() && !lut_mode;
+ RTLIL::Design *mapped_design = abc_parse_blif(f, builtin_lib ? "\\DFF" : "\\_dff_");
+
fclose(f);
free(p);
@@ -530,11 +610,11 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
}
std::map<std::string, int> cell_stats;
- if (liberty_file.empty() && script_file.empty() && !lut_mode)
+ if (builtin_lib)
{
for (auto &it : mapped_mod->cells) {
RTLIL::Cell *c = it.second;
- cell_stats[c->type.substr(1)]++;
+ cell_stats[RTLIL::unescape_id(c->type)]++;
if (c->type == "\\ZERO" || c->type == "\\ONE") {
RTLIL::SigSig conn;
conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Y"].chunks[0].wire->name)]);
@@ -582,21 +662,46 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
design->select(module, cell);
continue;
}
- assert(0);
+ if (c->type == "\\DFF") {
+ log_assert(clk_sig.width == 1);
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->type = clk_polarity ? "$_DFF_P_" : "$_DFF_N_";
+ cell->name = remap_name(c->name);
+ cell->connections["\\D"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\D"].chunks[0].wire->name)]);
+ cell->connections["\\Q"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Q"].chunks[0].wire->name)]);
+ cell->connections["\\C"] = clk_sig;
+ module->cells[cell->name] = cell;
+ design->select(module, cell);
+ continue;
+ }
+ log_abort();
}
}
else
{
- for (auto &it : mapped_mod->cells) {
+ for (auto &it : mapped_mod->cells)
+ {
RTLIL::Cell *c = it.second;
- cell_stats[c->type.substr(1)]++;
- if (c->type == "$_const0_" || c->type == "$_const1_") {
+ cell_stats[RTLIL::unescape_id(c->type)]++;
+ if (c->type == "\\_const0_" || c->type == "\\_const1_") {
RTLIL::SigSig conn;
- conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Y"].chunks[0].wire->name)]);
- conn.second = RTLIL::SigSpec(c->type == "$_const0_" ? 0 : 1, 1);
+ conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections.begin()->second.chunks[0].wire->name)]);
+ conn.second = RTLIL::SigSpec(c->type == "\\_const0_" ? 0 : 1, 1);
module->connections.push_back(conn);
continue;
}
+ if (c->type == "\\_dff_") {
+ log_assert(clk_sig.width == 1);
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->type = clk_polarity ? "$_DFF_P_" : "$_DFF_N_";
+ cell->name = remap_name(c->name);
+ cell->connections["\\D"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\D"].chunks[0].wire->name)]);
+ cell->connections["\\Q"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Q"].chunks[0].wire->name)]);
+ cell->connections["\\C"] = clk_sig;
+ module->cells[cell->name] = cell;
+ design->select(module, cell);
+ continue;
+ }
RTLIL::Cell *cell = new RTLIL::Cell;
cell->type = c->type;
cell->parameters = c->parameters;
@@ -663,7 +768,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
assert(n >= 0);
for (int i = 0; i < n; i++) {
if (strcmp(namelist[i]->d_name, ".") && strcmp(namelist[i]->d_name, "..")) {
- if (asprintf(&p, "%s/%s", tempdir_name, namelist[i]->d_name) < 0) abort();
+ if (asprintf(&p, "%s/%s", tempdir_name, namelist[i]->d_name) < 0) log_abort();
log("Removing `%s'.\n", p);
remove(p);
free(p);
@@ -708,6 +813,16 @@ struct AbcPass : public Pass {
log(" -lut <width>\n");
log(" generate netlist using luts of (max) the specified width.\n");
log("\n");
+ log(" -dff\n");
+ log(" also pass $_DFF_?_ cells through ABC (only one clock domain, if many\n");
+ log(" clock domains are present in a module, the one with the largest number\n");
+ log(" of $dff cells in it is used)\n");
+ log("\n");
+ log(" -clk [!]<signal-name>\n");
+ log(" use the specified clock domain. (when this option is used in combination\n");
+ log(" with -dff, then it falls back to the automatic dection of clock domain\n");
+ log(" if the specified clock is not found in a module.)\n");
+ log("\n");
log(" -nocleanup\n");
log(" when this option is used, the temporary files created by this pass\n");
log(" are not removed. this is useful for debugging.\n");
@@ -724,8 +839,8 @@ struct AbcPass : public Pass {
log_push();
std::string exe_file = rewrite_yosys_exe("yosys-abc");
- std::string script_file, liberty_file, constr_file;
- bool cleanup = true;
+ std::string script_file, liberty_file, constr_file, clk_str;
+ bool dff_mode = false, cleanup = true;
int lut_mode = 0;
size_t argidx;
@@ -758,6 +873,14 @@ struct AbcPass : public Pass {
lut_mode = atoi(args[++argidx].c_str());
continue;
}
+ if (arg == "-dff") {
+ dff_mode = true;
+ continue;
+ }
+ if (arg == "-clk" && argidx+1 < args.size() && lut_mode == 0) {
+ clk_str = args[++argidx];
+ continue;
+ }
if (arg == "-nocleanup") {
cleanup = false;
continue;
@@ -772,7 +895,7 @@ struct AbcPass : public Pass {
if (mod_it.second->processes.size() > 0)
log("Skipping module %s as it contains processes.\n", mod_it.second->name.c_str());
else
- abc_module(design, mod_it.second, script_file, exe_file, liberty_file, constr_file, cleanup, lut_mode);
+ abc_module(design, mod_it.second, script_file, exe_file, liberty_file, constr_file, cleanup, lut_mode, dff_mode, clk_str);
}
assign_map.clear();
diff --git a/passes/abc/blifparse.cc b/passes/abc/blifparse.cc
index 17acc843..2d46d1a8 100644
--- a/passes/abc/blifparse.cc
+++ b/passes/abc/blifparse.cc
@@ -22,29 +22,35 @@
#include <stdio.h>
#include <string.h>
-static bool read_next_line(char *buffer, int &line_count, FILE *f)
+static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, FILE *f)
{
+ int buffer_len = 0;
buffer[0] = 0;
while (1)
{
- int buffer_len = strlen(buffer);
+ buffer_len += strlen(buffer + buffer_len);
while (buffer_len > 0 && (buffer[buffer_len-1] == ' ' || buffer[buffer_len-1] == '\t' ||
buffer[buffer_len-1] == '\r' || buffer[buffer_len-1] == '\n'))
buffer[--buffer_len] = 0;
+ if (buffer_size-buffer_len < 4096) {
+ buffer_size *= 2;
+ buffer = (char*)realloc(buffer, buffer_size);
+ }
+
if (buffer_len == 0 || buffer[buffer_len-1] == '\\') {
if (buffer[buffer_len-1] == '\\')
buffer[--buffer_len] = 0;
line_count++;
- if (fgets(buffer+buffer_len, 4096-buffer_len, f) == NULL)
+ if (fgets(buffer+buffer_len, buffer_size-buffer_len, f) == NULL)
return false;
} else
return true;
}
}
-RTLIL::Design *abc_parse_blif(FILE *f)
+RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name)
{
RTLIL::Design *design = new RTLIL::Design;
RTLIL::Module *module = new RTLIL::Module;
@@ -56,12 +62,13 @@ RTLIL::Design *abc_parse_blif(FILE *f)
module->name = "\\netlist";
design->modules[module->name] = module;
- char buffer[4096];
+ size_t buffer_size = 4096;
+ char *buffer = (char*)malloc(buffer_size);
int line_count = 0;
while (1)
{
- if (!read_next_line(buffer, line_count, f))
+ if (!read_next_line(buffer, buffer_size, line_count, f))
goto error;
continue_without_read:
@@ -83,8 +90,10 @@ RTLIL::Design *abc_parse_blif(FILE *f)
if (!strcmp(cmd, ".model"))
continue;
- if (!strcmp(cmd, ".end"))
+ if (!strcmp(cmd, ".end")) {
+ free(buffer);
return design;
+ }
if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) {
char *p;
@@ -101,6 +110,58 @@ RTLIL::Design *abc_parse_blif(FILE *f)
continue;
}
+ if (!strcmp(cmd, ".latch"))
+ {
+ char *d = strtok(NULL, " \t\r\n");
+ char *q = strtok(NULL, " \t\r\n");
+
+ if (module->wires.count(RTLIL::escape_id(d)) == 0) {
+ RTLIL::Wire *wire = new RTLIL::Wire;
+ wire->name = RTLIL::escape_id(d);
+ module->add(wire);
+ }
+
+ if (module->wires.count(RTLIL::escape_id(q)) == 0) {
+ RTLIL::Wire *wire = new RTLIL::Wire;
+ wire->name = RTLIL::escape_id(q);
+ module->add(wire);
+ }
+
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->name = NEW_ID;
+ cell->type = dff_name;
+ cell->connections["\\D"] = module->wires.at(RTLIL::escape_id(d));
+ cell->connections["\\Q"] = module->wires.at(RTLIL::escape_id(q));
+ module->add(cell);
+ continue;
+ }
+
+ if (!strcmp(cmd, ".gate"))
+ {
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->name = NEW_ID;
+ module->add(cell);
+
+ char *p = strtok(NULL, " \t\r\n");
+ if (p == NULL)
+ goto error;
+ cell->type = RTLIL::escape_id(p);
+
+ while ((p = strtok(NULL, " \t\r\n")) != NULL) {
+ char *q = strchr(p, '=');
+ if (q == NULL || !q[0] || !q[1])
+ goto error;
+ *(q++) = 0;
+ if (module->wires.count(RTLIL::escape_id(q)) == 0) {
+ RTLIL::Wire *wire = new RTLIL::Wire;
+ wire->name = RTLIL::escape_id(q);
+ module->add(wire);
+ }
+ cell->connections[RTLIL::escape_id(p)] = module->wires.at(RTLIL::escape_id(q));
+ }
+ continue;
+ }
+
if (!strcmp(cmd, ".names"))
{
char *p;
@@ -122,7 +183,7 @@ RTLIL::Design *abc_parse_blif(FILE *f)
if (input_sig.width == 0) {
RTLIL::State state = RTLIL::State::Sa;
while (1) {
- if (!read_next_line(buffer, line_count, f))
+ if (!read_next_line(buffer, buffer_size, line_count, f))
goto error;
for (int i = 0; buffer[i]; i++) {
if (buffer[i] == ' ' || buffer[i] == '\t')
diff --git a/passes/abc/blifparse.h b/passes/abc/blifparse.h
index 98afedac..272e4e64 100644
--- a/passes/abc/blifparse.h
+++ b/passes/abc/blifparse.h
@@ -22,7 +22,7 @@
#include "kernel/rtlil.h"
-extern RTLIL::Design *abc_parse_blif(FILE *f);
+extern RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name);
#endif
diff --git a/passes/abc/vlparse.cc b/passes/abc/vlparse.cc
deleted file mode 100644
index fe10f57b..00000000
--- a/passes/abc/vlparse.cc
+++ /dev/null
@@ -1,227 +0,0 @@
-/*
- * yosys -- Yosys Open SYnthesis Suite
- *
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
- * Permission to use, copy, modify, and/or distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include "vlparse.h"
-#include "kernel/log.h"
-#include <stdio.h>
-#include <string>
-
-static int lex_line, lex_tok;
-static std::string lex_str;
-
-static int token(int tok)
-{
- lex_tok = tok;
-#if 0
- if (lex_tok == 256)
- fprintf(stderr, "STR in line %d: >>%s<<\n", lex_line, lex_str.c_str());
- else if (tok >= 32 && tok < 255)
- fprintf(stderr, "CHAR in line %d: >>%c<<\n", lex_line, lex_tok);
- else
- fprintf(stderr, "CHAR in line %d: %d\n", lex_line, lex_tok);
-#endif
- return tok;
-}
-
-static int lex(FILE *f)
-{
- int ch = getc(f);
-
- while (ch == ' ' || ch == '\t' || ch == '\n') {
- if (ch == '\n')
- lex_line++;
- ch = getc(f);
- }
-
- if (ch <= 0 || 255 < ch)
- return token(lex_tok);
-
- if (('a' <= ch && ch <= 'z') || ('A' <= ch && ch <= 'Z') ||
- ('0' <= ch && ch <= '9') || ch == '_' || ch == '\'') {
- lex_str = char(ch);
- while (1) {
- ch = getc(f);
- if (('a' <= ch && ch <= 'z') || ('A' <= ch && ch <= 'Z') ||
- ('0' <= ch && ch <= '9') || ch == '_' || ch == '\'') {
- lex_str += char(ch);
- continue;
- }
- break;
- }
- ungetc(ch, f);
- return token(256);
- }
-
- if (ch == '/') {
- ch = getc(f);
- if (ch == '/') {
- while (ch != '\n')
- ch = getc(f);
- ungetc(ch, f);
- return lex(f);
- }
- ungetc(ch, f);
- return token('/');
- }
-
- return token(ch);
-}
-
-RTLIL::Design *abc_parse_verilog(FILE *f)
-{
- RTLIL::Design *design = new RTLIL::Design;
- RTLIL::Module *module;
- RTLIL::Wire *wire;
- RTLIL::Cell *cell;
-
- int port_count = 1;
- lex_line = 1;
-
- // parse module header
- if (lex(f) != 256 || lex_str != "module")
- goto error;
- if (lex(f) != 256)
- goto error;
-
- module = new RTLIL::Module;
- module->name = "\\" + lex_str;
- design->modules[module->name] = module;
-
- if (lex(f) != '(')
- goto error;
- while (lex(f) != ')') {
- if (lex_tok != 256 && lex_tok != ',')
- goto error;
- }
- if (lex(f) != ';')
- goto error;
-
- // parse module body
- while (1)
- {
- if (lex(f) != 256)
- goto error;
-
- if (lex_str == "endmodule")
- return design;
-
- if (lex_str == "input" || lex_str == "output" || lex_str == "wire")
- {
- std::string mode = lex_str;
- while (lex(f) != ';') {
- if (lex_tok != 256 && lex_tok != ',')
- goto error;
- if (lex_tok == 256) {
- // printf("%s [%s]\n", mode.c_str(), lex_str.c_str());
- wire = new RTLIL::Wire;
- wire->name = "\\" + lex_str;
- if (mode == "input") {
- wire->port_id = port_count++;
- wire->port_input = true;
- }
- if (mode == "output") {
- wire->port_id = port_count++;
- wire->port_output = true;
- }
- module->wires[wire->name] = wire;
- }
- }
- }
- else if (lex_str == "assign")
- {
- std::string lhs, rhs;
-
- if (lex(f) != 256)
- goto error;
- lhs = lex_str;
-
- if (lex(f) != '=')
- goto error;
- if (lex(f) != 256)
- goto error;
- rhs = lex_str;
-
- if (lex(f) != ';')
- goto error;
-
- if (module->wires.count(RTLIL::escape_id(lhs)) == 0)
- goto error;
-
- if (rhs == "1'b0")
- module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), RTLIL::SigSpec(0, 1)));
- else if (rhs == "1'b1")
- module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), RTLIL::SigSpec(1, 1)));
- else if (module->wires.count(RTLIL::escape_id(rhs)) > 0)
- module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), module->wires.at(RTLIL::escape_id(rhs))));
- else
- goto error;
- }
- else
- {
- std::string cell_type = lex_str;
-
- if (lex(f) != 256)
- goto error;
-
- std::string cell_name = lex_str;
-
- if (lex(f) != '(')
- goto error;
-
- // printf("cell [%s] [%s]\n", cell_type.c_str(), cell_name.c_str());
- cell = new RTLIL::Cell;
- cell->type = "\\" + cell_type;
- cell->name = "\\" + cell_name;
- module->cells[cell->name] = cell;
-
- lex(f);
- while (lex_tok != ')')
- {
- if (lex_tok != '.' || lex(f) != 256)
- goto error;
-
- std::string cell_port = lex_str;
-
- if (lex(f) != '(' || lex(f) != 256)
- goto error;
-
- std::string wire_name = lex_str;
-
- // printf(" [%s] <- [%s]\n", cell_port.c_str(), wire_name.c_str());
- if (module->wires.count("\\" + wire_name) == 0)
- goto error;
- cell->connections["\\" + cell_port] = RTLIL::SigSpec(module->wires["\\" + wire_name]);
-
- if (lex(f) != ')' || (lex(f) != ',' && lex_tok != ')'))
- goto error;
- while (lex_tok == ',')
- lex(f);
- }
-
- if (lex(f) != ';')
- goto error;
- }
- }
-
-error:
- log_error("Syntax error in line %d!\n", lex_line);
- // delete design;
- // return NULL;
-}
-
diff --git a/passes/abc/vlparse.h b/passes/abc/vlparse.h
deleted file mode 100644
index 9514c419..00000000
--- a/passes/abc/vlparse.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/*
- * yosys -- Yosys Open SYnthesis Suite
- *
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
- * Permission to use, copy, modify, and/or distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#ifndef ABC_VLPARSE
-#define ABC_VLPARSE
-
-#include "kernel/rtlil.h"
-
-extern RTLIL::Design *abc_parse_verilog(FILE *f);
-
-#endif
-
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index a582de56..519dce45 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -69,17 +69,30 @@ struct RenamePass : public Pass {
log("Assign short auto-generated names to all selected wires and cells with private\n");
log("names.\n");
log("\n");
+ log(" rename -hide [selection]\n");
+ log("\n");
+ log("Assign private names (the ones with $-prefix) to all selected wires and cells\n");
+ log("with public names. This ignores all selected ports.\n");
+ log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
bool flag_enumerate = false;
+ bool flag_hide = false;
+ bool got_mode = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
std::string arg = args[argidx];
- if (arg == "-enumerate") {
+ if (arg == "-enumerate" && !got_mode) {
flag_enumerate = true;
+ got_mode = true;
+ continue;
+ }
+ if (arg == "-hide" && !got_mode) {
+ flag_hide = true;
+ got_mode = true;
continue;
}
break;
@@ -117,6 +130,36 @@ struct RenamePass : public Pass {
}
}
else
+ if (flag_hide)
+ {
+ extra_args(args, argidx, design);
+
+ for (auto &mod : design->modules)
+ {
+ RTLIL::Module *module = mod.second;
+ if (!design->selected(module))
+ continue;
+
+ std::map<RTLIL::IdString, RTLIL::Wire*> new_wires;
+ for (auto &it : module->wires) {
+ if (design->selected(module, it.second))
+ if (it.first[0] == '\\' && it.second->port_id == 0)
+ it.second->name = NEW_ID;
+ new_wires[it.second->name] = it.second;
+ }
+ module->wires.swap(new_wires);
+
+ std::map<RTLIL::IdString, RTLIL::Cell*> new_cells;
+ for (auto &it : module->cells) {
+ if (design->selected(module, it.second))
+ if (it.first[0] == '\\')
+ it.second->name = NEW_ID;
+ new_cells[it.second->name] = it.second;
+ }
+ module->cells.swap(new_cells);
+ }
+ }
+ else
{
if (argidx+2 != args.size())
log_cmd_error("Invalid number of arguments!\n");
diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc
index 137f8618..ec560772 100644
--- a/passes/cmds/select.cc
+++ b/passes/cmds/select.cc
@@ -272,6 +272,21 @@ static int select_op_expand(RTLIL::Design *design, RTLIL::Selection &lhs, std::v
if (lhs.selected_member(mod_it.first, it.first) && limits.count(it.first) == 0)
selected_wires.insert(it.second);
+ for (auto &conn : mod->connections)
+ {
+ std::vector<RTLIL::SigBit> conn_lhs = conn.first.to_sigbit_vector();
+ std::vector<RTLIL::SigBit> conn_rhs = conn.second.to_sigbit_vector();
+
+ for (size_t i = 0; i < conn_lhs.size(); i++) {
+ if (conn_lhs[i].wire == NULL || conn_rhs[i].wire == NULL)
+ continue;
+ if (mode != 'i' && selected_wires.count(conn_rhs[i].wire) && lhs.selected_members[mod->name].count(conn_lhs[i].wire->name) == 0)
+ lhs.selected_members[mod->name].insert(conn_lhs[i].wire->name), sel_objects++, max_objects--;
+ if (mode != 'o' && selected_wires.count(conn_lhs[i].wire) && lhs.selected_members[mod->name].count(conn_rhs[i].wire->name) == 0)
+ lhs.selected_members[mod->name].insert(conn_rhs[i].wire->name), sel_objects++, max_objects--;
+ }
+ }
+
for (auto &cell : mod->cells)
for (auto &conn : cell.second->connections)
{
@@ -514,7 +529,10 @@ static void select_stmt(RTLIL::Design *design, std::string arg)
} else {
size_t pos = arg.find('/');
if (pos == std::string::npos) {
- arg_mod = arg;
+ if (arg.find(':') == std::string::npos)
+ arg_mod = arg;
+ else
+ arg_mod = "*", arg_memb = arg;
} else {
arg_mod = arg.substr(0, pos);
arg_memb = arg.substr(pos+1);
diff --git a/passes/extract/extract.cc b/passes/extract/extract.cc
index 0c639aed..aa21e573 100644
--- a/passes/extract/extract.cc
+++ b/passes/extract/extract.cc
@@ -499,6 +499,8 @@ struct ExtractPass : public Pass {
solver.addSwappablePorts("$xnor", "\\A", "\\B");
solver.addSwappablePorts("$eq", "\\A", "\\B");
solver.addSwappablePorts("$ne", "\\A", "\\B");
+ solver.addSwappablePorts("$eqx", "\\A", "\\B");
+ solver.addSwappablePorts("$nex", "\\A", "\\B");
solver.addSwappablePorts("$add", "\\A", "\\B");
solver.addSwappablePorts("$mul", "\\A", "\\B");
solver.addSwappablePorts("$logic_and", "\\A", "\\B");
diff --git a/passes/memory/memory_collect.cc b/passes/memory/memory_collect.cc
index ca1a3666..ad4df228 100644
--- a/passes/memory/memory_collect.cc
+++ b/passes/memory/memory_collect.cc
@@ -20,9 +20,19 @@
#include "kernel/register.h"
#include "kernel/log.h"
#include <sstream>
+#include <algorithm>
#include <stdlib.h>
#include <assert.h>
+static bool memcells_cmp(RTLIL::Cell *a, RTLIL::Cell *b)
+{
+ if (a->type == "$memrd" && b->type == "$memrd")
+ return a->name < b->name;
+ if (a->type == "$memrd" || b->type == "$memrd")
+ return (a->type == "$memrd") < (b->type == "$memrd");
+ return a->parameters.at("\\PRIORITY").as_int() < b->parameters.at("\\PRIORITY").as_int();
+}
+
static void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory)
{
log("Collecting $memrd and $memwr for memory `%s' in module `%s':\n",
@@ -48,11 +58,18 @@ static void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory)
RTLIL::SigSpec sig_rd_data;
std::vector<std::string> del_cell_ids;
+ std::vector<RTLIL::Cell*> memcells;
- for (auto &cell_it : module->cells)
- {
+ for (auto &cell_it : module->cells) {
RTLIL::Cell *cell = cell_it.second;
+ if ((cell->type == "$memwr" || cell->type == "$memrd") && cell->parameters["\\MEMID"].decode_string() == memory->name)
+ memcells.push_back(cell);
+ }
+
+ std::sort(memcells.begin(), memcells.end(), memcells_cmp);
+ for (auto cell : memcells)
+ {
if (cell->type == "$memwr" && cell->parameters["\\MEMID"].decode_string() == memory->name)
{
wr_ports++;
diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index b7b361e9..0ead97b4 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -17,8 +17,6 @@
*
*/
-#undef MUX_UNDEF_SEL_TO_UNDEF_RESULTS
-
#include "opt_status.h"
#include "kernel/register.h"
#include "kernel/sigtools.h"
@@ -133,18 +131,19 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
ACTION_DO("\\Y", input.extract(2, 1));
if (input.match(" 0")) ACTION_DO("\\Y", input.extract(2, 1));
if (input.match(" 1")) ACTION_DO("\\Y", input.extract(1, 1));
-#ifdef MUX_UNDEF_SEL_TO_UNDEF_RESULTS
if (input.match("01 ")) ACTION_DO("\\Y", input.extract(0, 1));
- // TODO: "10 " -> replace with "!S" gate
- // TODO: "0 " -> replace with "B AND S" gate
- // TODO: " 1 " -> replace with "A OR S" gate
- // TODO: "1 " -> replace with "B OR !S" gate (?)
- // TODO: " 0 " -> replace with "A AND !S" gate (?)
- if (input.match(" *")) ACTION_DO_Y(x);
-#endif
+ if (input.match("10 ")) {
+ cell->type = "$_INV_";
+ cell->connections["\\A"] = input.extract(0, 1);
+ cell->connections.erase("\\B");
+ cell->connections.erase("\\S");
+ goto next_cell;
+ }
+ if (input.match("01*")) ACTION_DO_Y(x);
+ if (input.match("10*")) ACTION_DO_Y(x);
}
- if (cell->type == "$eq" || cell->type == "$ne")
+ if (cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex")
{
RTLIL::SigSpec a = cell->connections["\\A"];
RTLIL::SigSpec b = cell->connections["\\B"];
@@ -160,22 +159,27 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
assert(a.chunks.size() == b.chunks.size());
for (size_t i = 0; i < a.chunks.size(); i++) {
- if (a.chunks[i].wire == NULL && a.chunks[i].data.bits[0] > RTLIL::State::S1)
- continue;
- if (b.chunks[i].wire == NULL && b.chunks[i].data.bits[0] > RTLIL::State::S1)
+ if (a.chunks[i].wire == NULL && b.chunks[i].wire == NULL && a.chunks[i].data.bits[0] != b.chunks[i].data.bits[0] &&
+ a.chunks[i].data.bits[0] <= RTLIL::State::S1 && b.chunks[i].data.bits[0] <= RTLIL::State::S1) {
+ RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ? RTLIL::State::S0 : RTLIL::State::S1);
+ new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
+ replace_cell(module, cell, "empty", "\\Y", new_y);
+ goto next_cell;
+ }
+ if (a.chunks[i] == b.chunks[i])
continue;
new_a.append(a.chunks[i]);
new_b.append(b.chunks[i]);
}
if (new_a.width == 0) {
- RTLIL::SigSpec new_y = RTLIL::SigSpec(cell->type == "$eq" ? RTLIL::State::S1 : RTLIL::State::S0);
+ RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ? RTLIL::State::S1 : RTLIL::State::S0);
new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
replace_cell(module, cell, "empty", "\\Y", new_y);
goto next_cell;
}
- if (new_a.width != a.width) {
+ if (new_a.width < a.width || new_b.width < b.width) {
new_a.optimize();
new_b.optimize();
cell->connections["\\A"] = new_a;
diff --git a/passes/proc/proc_arst.cc b/passes/proc/proc_arst.cc
index 65dc97bd..57194657 100644
--- a/passes/proc/proc_arst.cc
+++ b/passes/proc/proc_arst.cc
@@ -47,7 +47,7 @@ static bool check_signal(RTLIL::Module *mod, RTLIL::SigSpec signal, RTLIL::SigSp
polarity = !polarity;
return check_signal(mod, cell->connections["\\A"], ref, polarity);
}
- if (cell->type == "$eq" && cell->connections["\\Y"] == signal) {
+ if ((cell->type == "$eq" || cell->type == "$eqx") && cell->connections["\\Y"] == signal) {
if (cell->connections["\\A"].is_fully_const()) {
if (!cell->connections["\\A"].as_bool())
polarity = !polarity;
@@ -59,7 +59,7 @@ static bool check_signal(RTLIL::Module *mod, RTLIL::SigSpec signal, RTLIL::SigSp
return check_signal(mod, cell->connections["\\A"], ref, polarity);
}
}
- if (cell->type == "$ne" && cell->connections["\\Y"] == signal) {
+ if ((cell->type == "$ne" || cell->type == "$nex") && cell->connections["\\Y"] == signal) {
if (cell->connections["\\A"].is_fully_const()) {
if (cell->connections["\\A"].as_bool())
polarity = !polarity;
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 5d0d35b6..5d36b474 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -148,7 +148,7 @@ struct VlogHammerReporter
ezDefaultSAT ez;
SigMap sigmap(module);
- SatGen satgen(&ez, design, &sigmap);
+ SatGen satgen(&ez, &sigmap);
satgen.model_undef = model_undef;
for (auto &c : module->cells)
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index d57fdd32..4b868b3c 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -28,337 +28,466 @@
#include <string.h>
#include <algorithm>
-#define NUM_INITIAL_RANDOM_TEST_VECTORS 10
-
namespace {
-struct FreduceHelper
+bool inv_mode;
+int verbose_level;
+typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
+
+struct equiv_bit_t
{
- RTLIL::Design *design;
- RTLIL::Module *module;
- bool try_mode;
+ int depth;
+ bool inverted;
+ RTLIL::Cell *drv;
+ RTLIL::SigBit bit;
+
+ bool operator<(const equiv_bit_t &other) const {
+ if (depth != other.depth)
+ return depth < other.depth;
+ if (inverted != other.inverted)
+ return inverted < other.inverted;
+ if (drv != other.drv)
+ return drv < other.drv;
+ return bit < other.bit;
+ }
+};
+
+struct FindReducedInputs
+{
+ SigMap &sigmap;
+ drivers_t &drivers;
ezDefaultSAT ez;
- SigMap sigmap;
- CellTypes ct;
+ std::set<RTLIL::Cell*> ez_cells;
SatGen satgen;
- ConstEval ce;
- SigPool inputs, nodes;
- RTLIL::SigSpec input_sigs;
-
- SigSet<RTLIL::SigSpec> source_signals;
- std::vector<RTLIL::Const> test_vectors;
- std::map<RTLIL::SigSpec, RTLIL::Const> node_to_data;
- std::map<RTLIL::SigSpec, RTLIL::SigSpec> node_result;
-
- uint32_t xorshift32_state;
-
- uint32_t xorshift32() {
- xorshift32_state ^= xorshift32_state << 13;
- xorshift32_state ^= xorshift32_state >> 17;
- xorshift32_state ^= xorshift32_state << 5;
- return xorshift32_state;
+ FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
+ sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
+ {
+ satgen.model_undef = true;
}
- FreduceHelper(RTLIL::Design *design, RTLIL::Module *module, bool try_mode) :
- design(design), module(module), try_mode(try_mode),
- sigmap(module), satgen(&ez, design, &sigmap), ce(module)
+ void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
{
- ct.setup_internals();
- ct.setup_stdcells();
+ if (out.wire == NULL)
+ return;
+ if (sigdone.count(out) != 0)
+ return;
+ sigdone.insert(out);
+
+ if (drivers.count(out) != 0) {
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+ if (ez_cells.count(drv.first) == 0) {
+ satgen.setContext(&sigmap, "A");
+ if (!satgen.importCell(drv.first))
+ log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+ satgen.setContext(&sigmap, "B");
+ if (!satgen.importCell(drv.first))
+ log_abort();
+ ez_cells.insert(drv.first);
+ }
+ for (auto &bit : drv.second)
+ register_cone_worker(pi, sigdone, bit);
+ } else
+ pi.insert(out);
+ }
- xorshift32_state = 123456789;
- xorshift32();
- xorshift32();
- xorshift32();
+ void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out)
+ {
+ std::set<RTLIL::SigBit> pi_set, sigdone;
+ register_cone_worker(pi_set, sigdone, out);
+ pi.clear();
+ pi.insert(pi.end(), pi_set.begin(), pi_set.end());
}
- bool run_test(RTLIL::SigSpec test_vec)
+ void analyze(std::vector<RTLIL::SigBit> &reduced_inputs, RTLIL::SigBit output)
{
- ce.clear();
- ce.set(input_sigs, test_vec.as_const());
-
- for (auto &bit : nodes.bits) {
- RTLIL::SigSpec nodesig(bit.first, 1, bit.second), nodeval = nodesig;
- if (!ce.eval(nodeval)) {
- if (!try_mode)
- log_error("Evaluation of node %s failed!\n", log_signal(nodesig));
- log("FAILED: Evaluation of node %s failed!\n", log_signal(nodesig));
- return false;
+ if (verbose_level >= 1)
+ log(" Analyzing input cone for signal %s:\n", log_signal(output));
+
+ std::vector<RTLIL::SigBit> pi;
+ register_cone(pi, output);
+
+ if (verbose_level >= 1)
+ log(" Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size()));
+
+ satgen.setContext(&sigmap, "A");
+ int output_a = satgen.importSigSpec(output).front();
+ int output_undef_a = satgen.importUndefSigSpec(output).front();
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+ satgen.setContext(&sigmap, "B");
+ int output_b = satgen.importSigSpec(output).front();
+ int output_undef_b = satgen.importUndefSigSpec(output).front();
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+ for (size_t i = 0; i < pi.size(); i++)
+ {
+ RTLIL::SigSpec test_sig(pi[i]);
+ RTLIL::SigSpec rest_sig(pi);
+ rest_sig.remove(i, 1);
+
+ int test_sig_a, test_sig_b;
+ std::vector<int> rest_sig_a, rest_sig_b;
+
+ satgen.setContext(&sigmap, "A");
+ test_sig_a = satgen.importSigSpec(test_sig).front();
+ rest_sig_a = satgen.importSigSpec(rest_sig);
+
+ satgen.setContext(&sigmap, "B");
+ test_sig_b = satgen.importSigSpec(test_sig).front();
+ rest_sig_b = satgen.importSigSpec(rest_sig);
+
+ if (ez.solve(ez.vec_eq(rest_sig_a, rest_sig_b), ez.XOR(output_a, output_b), ez.XOR(test_sig_a, test_sig_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) {
+ if (verbose_level >= 2)
+ log(" Result for input %s: pass\n", log_signal(test_sig));
+ reduced_inputs.push_back(pi[i]);
+ } else {
+ if (verbose_level >= 2)
+ log(" Result for input %s: strip\n", log_signal(test_sig));
}
- node_to_data[nodesig].bits.push_back(nodeval.as_const().bits.at(0));
}
- return true;
+ if (verbose_level >= 1)
+ log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
}
+};
- void dump_node_data()
- {
- int max_node_len = 20;
- for (auto &it : node_to_data)
- max_node_len = std::max(max_node_len, int(strlen(log_signal(it.first))));
- log(" full node fingerprints:\n");
- for (auto &it : node_to_data)
- log(" %-*s %s\n", max_node_len+5, log_signal(it.first), log_signal(it.second));
- }
+struct PerformReduction
+{
+ SigMap &sigmap;
+ drivers_t &drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
- bool check(RTLIL::SigSpec sig1, RTLIL::SigSpec sig2)
+ ezDefaultSAT ez;
+ SatGen satgen;
+
+ std::vector<int> sat_pi, sat_out, sat_def;
+ std::vector<RTLIL::SigBit> out_bits, pi_bits;
+ std::vector<bool> out_inverted;
+ std::vector<int> out_depth;
+
+ int register_cone_worker(std::set<RTLIL::Cell*> &celldone, std::map<RTLIL::SigBit, int> &sigdepth, RTLIL::SigBit out)
{
- log(" performing SAT proof: %s == %s ->", log_signal(sig1), log_signal(sig2));
-
- std::vector<int> vec1 = satgen.importSigSpec(sig1);
- std::vector<int> vec2 = satgen.importSigSpec(sig2);
- std::vector<int> model = satgen.importSigSpec(input_sigs);
- std::vector<bool> testvect;
-
- if (ez.solve(model, testvect, ez.vec_ne(vec1, vec2))) {
- RTLIL::SigSpec testvect_sig;
- for (int i = 0; i < input_sigs.width; i++)
- testvect_sig.append(testvect.at(i) ? RTLIL::State::S1 : RTLIL::State::S0);
- testvect_sig.optimize();
- log(" failed: %s\n", log_signal(testvect_sig));
- test_vectors.push_back(testvect_sig.as_const());
- if (!run_test(testvect_sig))
- return false;
+ if (out.wire == NULL)
+ return 0;
+ if (sigdepth.count(out) != 0)
+ return sigdepth.at(out);
+ sigdepth[out] = 0;
+
+ if (drivers.count(out) != 0) {
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+ if (celldone.count(drv.first) == 0) {
+ if (!satgen.importCell(drv.first))
+ log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+ celldone.insert(drv.first);
+ }
+ int max_child_dept = 0;
+ for (auto &bit : drv.second)
+ max_child_dept = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_dept);
+ sigdepth[out] = max_child_dept + 1;
} else {
- log(" success.\n");
- if (!sig1.is_fully_const())
- node_result[sig1].append(sig2);
- if (!sig2.is_fully_const())
- node_result[sig2].append(sig1);
+ pi_bits.push_back(out);
+ sat_pi.push_back(satgen.importSigSpec(out).front());
+ ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
}
- return true;
+
+ return sigdepth[out];
}
- bool analyze_const()
+ PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits) :
+ sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits)
{
- for (auto &it : node_to_data)
- {
- if (node_result.count(it.first))
- continue;
- if (it.second == RTLIL::Const(RTLIL::State::S0, it.second.bits.size()))
- if (!check(it.first, RTLIL::SigSpec(RTLIL::State::S0)))
- return false;
- if (it.second == RTLIL::Const(RTLIL::State::S1, it.second.bits.size()))
- if (!check(it.first, RTLIL::SigSpec(RTLIL::State::S1)))
- return false;
+ satgen.model_undef = true;
+
+ std::set<RTLIL::Cell*> celldone;
+ std::map<RTLIL::SigBit, int> sigdepth;
+
+ for (auto &bit : bits) {
+ out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
+ sat_out.push_back(satgen.importSigSpec(bit).front());
+ sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
}
- return true;
+
+ if (inv_mode) {
+ if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
+ log_error("Solving for initial model failed!\n");
+ for (size_t i = 0; i < sat_out.size(); i++)
+ if (out_inverted.at(i))
+ sat_out[i] = ez.NOT(sat_out[i]);
+ } else
+ out_inverted = std::vector<bool>(sat_out.size(), false);
}
- bool analyze_alias()
+ void analyze(std::vector<std::set<int>> &results, std::map<int, int> &results_map, std::vector<int> &bucket, int level)
{
- restart:
- std::map<RTLIL::Const, RTLIL::SigSpec> reverse_map;
+ if (bucket.size() <= 1)
+ return;
- for (auto &it : node_to_data) {
- if (node_result.count(it.first) && node_result.at(it.first).is_fully_const())
- continue;
- reverse_map[it.second].append(it.first);
+ if (verbose_level == 1)
+ log("%*s Trying to shatter bucket with %d signals.\n", 2*level, "", int(bucket.size()));
+
+ if (verbose_level > 1) {
+ std::vector<RTLIL::SigBit> bucket_sigbits;
+ for (int idx : bucket)
+ bucket_sigbits.push_back(out_bits[idx]);
+ RTLIL::SigSpec bucket_sig(bucket_sigbits);
+ bucket_sig.optimize();
+ log("%*s Trying to shatter bucket with %d signals: %s\n", 2*level, "", int(bucket.size()), log_signal(bucket_sig));
}
- for (auto &it : reverse_map)
- {
- if (it.second.width <= 1)
- continue;
+ std::vector<int> sat_list, sat_inv_list;
+ for (int idx : bucket) {
+ sat_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
+ sat_inv_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+ }
- it.second.expand();
- for (int i = 0; i < it.second.width; i++)
- for (int j = i+1; j < it.second.width; j++) {
- RTLIL::SigSpec sig1 = it.second.chunks.at(i), sig2 = it.second.chunks.at(j);
- if (node_result.count(sig1) && node_result.count(sig2))
- continue;
- if (node_to_data.at(sig1) != node_to_data.at(sig2))
- goto restart;
- if (!check(it.second.chunks.at(i), it.second.chunks.at(j)))
- return false;
+ std::vector<int> modelVars = sat_out;
+ std::vector<bool> model;
+
+ modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
+ if (verbose_level >= 2)
+ modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
+
+ if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_list), ez.expression(ezSAT::OpOr, sat_inv_list)))
+ {
+ if (verbose_level >= 2) {
+ for (size_t i = 0; i < pi_bits.size(); i++)
+ log("%*s -> PI %c == %s\n", 2*level, "", model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i]));
+ for (int idx : bucket)
+ log("%*s -> OUT %c == %s%s\n", 2*level, "", model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x',
+ out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx]));
}
- }
- return true;
- }
- bool toproot_helper(RTLIL::SigSpec cursor, RTLIL::SigSpec stoplist, RTLIL::SigSpec &donelist, int level)
- {
- // log(" %*schecking %s: %s\n", level*2, "", log_signal(cursor), log_signal(stoplist));
+ std::vector<int> buckets_a;
+ std::vector<int> buckets_b;
- if (stoplist.extract(cursor).width != 0) {
- // log(" %*s STOP\n", level*2, "");
- return false;
+ for (int idx : bucket) {
+ if (!model[sat_out.size() + idx] || model[idx])
+ buckets_a.push_back(idx);
+ if (!model[sat_out.size() + idx] || !model[idx])
+ buckets_b.push_back(idx);
+ }
+ analyze(results, results_map, buckets_a, level+1);
+ analyze(results, results_map, buckets_b, level+1);
}
+ else
+ {
+ std::vector<int> undef_slaves;
+
+ for (int idx : bucket) {
+ std::vector<int> sat_def_list;
+ for (int idx2 : bucket)
+ if (idx != idx2)
+ sat_def_list.push_back(sat_def[idx2]);
+ if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+ undef_slaves.push_back(idx);
+ }
+
+ if (undef_slaves.size() == bucket.size()) {
+ if (verbose_level >= 1)
+ log("%*s Complex undef overlap. None of the signals covers the others.\n", 2*level, "");
+ // FIXME: We could try to further shatter a group with complex undef overlaps
+ return;
+ }
- if (donelist.extract(cursor).width != 0)
- return true;
+ for (int idx : undef_slaves)
+ out_depth[idx] = std::numeric_limits<int>::max();
- stoplist.append(cursor);
- std::set<RTLIL::SigSpec> next = source_signals.find(cursor);
+ if (verbose_level >= 1) {
+ log("%*s Found %d equivialent signals:", 2*level, "", int(bucket.size()));
+ for (int idx : bucket)
+ log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx]));
+ log("\n");
+ }
- for (auto &it : next)
- if (!toproot_helper(it, stoplist, donelist, level+1))
- return false;
+ int result_idx = -1;
+ for (int idx : bucket) {
+ if (results_map.count(idx) == 0)
+ continue;
+ if (result_idx == -1) {
+ result_idx = results_map.at(idx);
+ continue;
+ }
+ int result_idx2 = results_map.at(idx);
+ results[result_idx].insert(results[result_idx2].begin(), results[result_idx2].end());
+ for (int idx2 : results[result_idx2])
+ results_map[idx2] = result_idx;
+ results[result_idx2].clear();
+ }
- donelist.append(cursor);
- return true;
- }
+ if (result_idx == -1) {
+ result_idx = results.size();
+ results.push_back(std::set<int>());
+ }
- // KISS topological sort of bits in signal. return one element of sig
- // without dependencies to the others (or empty if input is not a DAG).
- RTLIL::SigSpec toproot(RTLIL::SigSpec sig)
- {
- sig.expand();
- // log(" finding topological root in %s:\n", log_signal(sig));
- for (auto &c : sig.chunks) {
- RTLIL::SigSpec stoplist = sig, donelist;
- stoplist.remove(c);
- // log(" testing %s as root:\n", log_signal(c));
- if (toproot_helper(c, stoplist, donelist, 0))
- return c;
+ results[result_idx].insert(bucket.begin(), bucket.end());
}
- return RTLIL::SigSpec();
}
- void update_design_for_group(RTLIL::SigSpec root, RTLIL::SigSpec rest)
+ void analyze(std::vector<std::vector<equiv_bit_t>> &results)
{
- SigPool unlink;
- unlink.add(rest);
+ std::vector<int> bucket;
+ for (size_t i = 0; i < sat_out.size(); i++)
+ bucket.push_back(i);
+
+ std::vector<std::set<int>> results_buf;
+ std::map<int, int> results_map;
+ analyze(results_buf, results_map, bucket, 1);
- for (auto &cell_it : module->cells) {
- RTLIL::Cell *cell = cell_it.second;
- if (!ct.cell_known(cell->type))
+ for (auto &r : results_buf)
+ {
+ if (r.size() <= 1)
continue;
- for (auto &conn : cell->connections)
- if (ct.cell_output(cell->type, conn.first)) {
- RTLIL::SigSpec sig = sigmap(conn.second);
- sig.expand();
- bool did_something = false;
- for (auto &c : sig.chunks) {
- if (c.wire == NULL || !unlink.check_any(c))
- continue;
- c.wire = new RTLIL::Wire;
- c.wire->name = NEW_ID;
- module->add(c.wire);
- assert(c.width == 1);
- c.offset = 0;
- did_something = true;
- }
- if (did_something) {
- sig.optimize();
- conn.second = sig;
- }
- }
- }
- rest.expand();
- for (auto &c : rest.chunks) {
- if (c.wire != NULL && !root.is_fully_const()) {
- source_signals.erase(c);
- source_signals.insert(c, root);
+ std::vector<equiv_bit_t> result;
+
+ for (int idx : r) {
+ equiv_bit_t bit;
+ bit.depth = out_depth[idx];
+ bit.inverted = out_inverted[idx];
+ bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
+ bit.bit = out_bits[idx];
+ result.push_back(bit);
}
- module->connections.push_back(RTLIL::SigSig(c, root));
+
+ std::sort(result.begin(), result.end());
+
+ if (result.front().inverted)
+ for (auto &bit : result)
+ bit.inverted = !bit.inverted;
+
+ for (size_t i = 1; i < result.size(); i++) {
+ std::pair<RTLIL::SigBit, RTLIL::SigBit> p(result[0].bit, result[i].bit);
+ if (inv_pairs.count(p) != 0)
+ result.erase(result.begin() + i);
+ }
+
+ if (result.size() > 1)
+ results.push_back(result);
}
}
+};
- void analyze_groups()
+struct FreduceWorker
+{
+ RTLIL::Module *module;
+
+ SigMap sigmap;
+ drivers_t drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> inv_pairs;
+
+ FreduceWorker(RTLIL::Module *module) : module(module), sigmap(module)
{
- SigMap to_group_major;
- for (auto &it : node_result) {
- it.second.expand();
- for (auto &c : it.second.chunks)
- to_group_major.add(it.first, c);
- }
+ }
- std::map<RTLIL::SigSpec, RTLIL::SigSpec> major_to_rest;
- for (auto &it : node_result)
- major_to_rest[to_group_major(it.first)].append(it.first);
+ int run()
+ {
+ log("Running functional reduction on module %s:\n", RTLIL::id2cstr(module->name));
- for (auto &it : major_to_rest)
- {
- RTLIL::SigSig group = it;
+ CellTypes ct;
+ ct.setup_internals();
+ ct.setup_stdcells();
- if (!it.first.is_fully_const()) {
- group.first = toproot(it.second);
- if (group.first.width == 0) {
- log("Operating on non-DAG input: failed to find topological root for `%s'.\n", log_signal(it.second));
- return;
+ std::vector<std::set<RTLIL::SigBit>> batches;
+ for (auto &it : module->wires)
+ if (it.second->port_input)
+ batches.push_back(sigmap(it.second).to_sigbit_set());
+ for (auto &it : module->cells) {
+ if (ct.cell_known(it.second->type)) {
+ std::set<RTLIL::SigBit> inputs, outputs;
+ for (auto &port : it.second->connections) {
+ std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
+ if (ct.cell_output(it.second->type, port.first))
+ outputs.insert(bits.begin(), bits.end());
+ else
+ inputs.insert(bits.begin(), bits.end());
}
- group.second.remove(group.first);
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> drv(it.second, inputs);
+ for (auto &bit : outputs)
+ drivers[bit] = drv;
+ batches.push_back(outputs);
}
+ if (inv_mode && it.second->type == "$_INV_")
+ inv_pairs.insert(std::pair<RTLIL::SigBit, RTLIL::SigBit>(sigmap(it.second->connections.at("\\A")), sigmap(it.second->connections.at("\\Y"))));
+ }
+
+ int bits_count = 0;
+ std::map<std::vector<RTLIL::SigBit>, std::vector<RTLIL::SigBit>> buckets;
+ buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S0));
+ buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S1));
+ for (auto &batch : batches)
+ {
+ RTLIL::SigSpec batch_sig(std::vector<RTLIL::SigBit>(batch.begin(), batch.end()));
+ batch_sig.optimize();
- group.first.optimize();
- group.second.sort_and_unify();
+ log(" Finding reduced input cone for signal batch %s%c\n", log_signal(batch_sig), verbose_level ? ':' : '.');
- log(" found group: %s -> %s\n", log_signal(group.first), log_signal(group.second));
- update_design_for_group(group.first, group.second);
+ FindReducedInputs infinder(sigmap, drivers);
+ for (auto &bit : batch) {
+ std::vector<RTLIL::SigBit> inputs;
+ infinder.analyze(inputs, bit);
+ buckets[inputs].push_back(bit);
+ bits_count++;
+ }
}
- }
+ log(" Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size()));
- void run()
- {
- log("\nFunctionally reduce module %s:\n", RTLIL::id2cstr(module->name));
-
- // find inputs and nodes (nets driven by internal cells)
- // add all internal cells to sat solver
-
- for (auto &cell_it : module->cells) {
- RTLIL::Cell *cell = cell_it.second;
- if (!ct.cell_known(cell->type))
+ std::vector<std::vector<equiv_bit_t>> equiv;
+ for (auto &bucket : buckets)
+ {
+ if (bucket.second.size() == 1)
continue;
- RTLIL::SigSpec cell_inputs, cell_outputs;
- for (auto &conn : cell->connections)
- if (ct.cell_output(cell->type, conn.first)) {
- nodes.add(sigmap(conn.second));
- cell_outputs.append(sigmap(conn.second));
- } else {
- inputs.add(sigmap(conn.second));
- cell_inputs.append(sigmap(conn.second));
- }
- cell_inputs.sort_and_unify();
- cell_outputs.sort_and_unify();
- cell_inputs.expand();
- for (auto &c : cell_inputs.chunks)
- if (c.wire != NULL)
- source_signals.insert(cell_outputs, c);
- if (!satgen.importCell(cell))
- log_error("Failed to import cell to SAT solver: %s (%s)\n",
- RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
- }
- inputs.del(nodes);
- nodes.add(inputs);
- log(" found %d nodes (%d inputs).\n", int(nodes.size()), int(inputs.size()));
-
- // initialise input_sigs and add all-zero, all-one and a few random test vectors
-
- input_sigs = inputs.export_all();
- test_vectors.push_back(RTLIL::SigSpec(RTLIL::State::S0, input_sigs.width).as_const());
- test_vectors.push_back(RTLIL::SigSpec(RTLIL::State::S1, input_sigs.width).as_const());
-
- for (int i = 0; i < NUM_INITIAL_RANDOM_TEST_VECTORS; i++) {
- RTLIL::SigSpec sig;
- for (int j = 0; j < input_sigs.width; j++)
- sig.append(xorshift32() % 2 ? RTLIL::State::S1 : RTLIL::State::S0);
- sig.optimize();
- assert(sig.width == input_sigs.width);
- test_vectors.push_back(sig.as_const());
- }
- for (auto &test_vec : test_vectors)
- if (!run_test(test_vec))
- return;
+ RTLIL::SigSpec bucket_sig(bucket.second);
+ bucket_sig.optimize();
- // run the analysis and update design
+ log(" Trying to shatter bucket %s%c\n", log_signal(bucket_sig), verbose_level ? ':' : '.');
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second);
+ worker.analyze(equiv);
+ }
- if (!analyze_const())
- return;
+ log(" Rewiring %d equivialent groups:\n", int(equiv.size()));
+ int rewired_sigbits = 0;
+ for (auto &grp : equiv)
+ {
+ log(" Using as master for group: %s\n", log_signal(grp.front().bit));
+
+ RTLIL::SigSpec inv_sig;
+ for (size_t i = 1; i < grp.size(); i++)
+ {
+ log(" Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit));
+
+ RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
+ RTLIL::Wire *dummy_wire = module->new_wire(1, NEW_ID);
+ for (auto &port : drv->connections)
+ sigmap(port.second).replace(grp[i].bit, dummy_wire, &port.second);
+
+ if (grp[i].inverted)
+ {
+ if (inv_sig.width == 0)
+ {
+ inv_sig = module->new_wire(1, NEW_ID);
+
+ RTLIL::Cell *inv_cell = new RTLIL::Cell;
+ inv_cell->name = NEW_ID;
+ inv_cell->type = "$_INV_";
+ inv_cell->connections["\\A"] = grp[0].bit;
+ inv_cell->connections["\\Y"] = inv_sig;
+ module->add(inv_cell);
+ }
- if (!analyze_alias())
- return;
+ module->connections.push_back(RTLIL::SigSig(grp[i].bit, inv_sig));
+ }
+ else
+ module->connections.push_back(RTLIL::SigSig(grp[i].bit, grp[0].bit));
- log(" input vector: %s\n", log_signal(input_sigs));
- for (auto &test_vec : test_vectors)
- log(" test vector: %s\n", log_signal(test_vec));
+ rewired_sigbits++;
+ }
+ }
- dump_node_data();
- analyze_groups();
+ log(" Rewired a total of %d signal bits in module %s.\n", rewired_sigbits, RTLIL::id2cstr(module->name));
+ return rewired_sigbits;
}
};
@@ -374,43 +503,51 @@ struct FreducePass : public Pass {
log("\n");
log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n");
log("equivialent, they are merged to one node and one of the redundant drivers is\n");
- log("removed.\n");
+ log("unconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
+ log("\n");
+ log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
+ log("equivialent nodes.\n");
log("\n");
- log(" -try\n");
- log(" do not issue an error when the analysis fails.\n");
- log(" (usually beacause of logic loops in the design)\n");
+ log(" -v, -vv\n");
+ log(" enable verbose or very verbose output\n");
+ log("\n");
+ log(" -inv\n");
+ log(" enable explicit handling of inverted signals\n");
log("\n");
- // log(" -enable_invert\n");
- // log(" also detect nodes that are inverse to each other.\n");
- // log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
- bool enable_invert = false;
- bool try_mode = false;
+ verbose_level = 0;
+ inv_mode = false;
log_header("Executing FREDUCE pass (perform functional reduction).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
- if (args[argidx] == "-enable_invert") {
- enable_invert = true;
+ if (args[argidx] == "-v") {
+ verbose_level = 1;
continue;
}
- if (args[argidx] == "-try") {
- try_mode = true;
+ if (args[argidx] == "-vv") {
+ verbose_level = 2;
+ continue;
+ }
+ if (args[argidx] == "-inv") {
+ inv_mode = true;
continue;
}
break;
}
extra_args(args, argidx, design);
- for (auto &mod_it : design->modules)
- {
+ int bitcount = 0;
+ for (auto &mod_it : design->modules) {
RTLIL::Module *module = mod_it.second;
if (design->selected(module))
- FreduceHelper(design, module, try_mode).run();
+ bitcount += FreduceWorker(module).run();
}
+
+ log("Rewired a total of %d signal bits.\n", bitcount);
}
} FreducePass;
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e330dfa6..fef99dfc 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -44,14 +44,14 @@ struct SatHelper
SatGen satgen;
// additional constraints
- std::vector<std::pair<std::string, std::string>> sets, prove, sets_init;
+ std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at;
// undef constraints
bool enable_undef, set_init_undef;
- std::vector<std::string> sets_def, sets_undef, sets_all_undef;
- std::map<int, std::vector<std::string>> sets_def_at, sets_undef_at, sets_all_undef_at;
+ std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
// model variables
std::vector<std::string> shows;
@@ -61,7 +61,7 @@ struct SatHelper
bool gotTimeout;
SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
- design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
+ design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
@@ -202,6 +202,71 @@ struct SatHelper
check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ // 0 = sets_def
+ // 1 = sets_any_undef
+ // 2 = sets_all_undef
+ std::set<RTLIL::SigSpec> sets_def_undef[3];
+
+ for (auto &s : sets_def) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ }
+
+ for (auto &s : sets_any_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[1].insert(sig);
+ }
+
+ for (auto &s : sets_all_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (auto &s : sets_def_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_any_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].insert(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_all_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (int t = 0; t < 3; t++)
+ for (auto &sig : sets_def_undef[t]) {
+ log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+ std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
+ if (t == 0)
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+ if (t == 1)
+ ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+ if (t == 2)
+ ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+ }
+
int import_cell_counter = 0;
for (auto &c : module->cells)
if (design->selected(module, c.second)) {
@@ -219,34 +284,75 @@ struct SatHelper
int setup_proof(int timestep = -1)
{
- assert(prove.size() > 0);
+ assert(prove.size() + prove_x.size() > 0);
RTLIL::SigSpec big_lhs, big_rhs;
+ std::vector<int> prove_bits;
- for (auto &s : prove)
+ if (prove.size() > 0)
{
- RTLIL::SigSpec lhs, rhs;
+ for (auto &s : prove)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.width != rhs.width)
+ log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+ log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
- log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
- if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
- log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
- show_signal_pool.add(sigmap(lhs));
- show_signal_pool.add(sigmap(rhs));
+ log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+ check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+ prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ }
- if (lhs.width != rhs.width)
- log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
- s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+ if (prove_x.size() > 0)
+ {
+ for (auto &s : prove_x)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.width != rhs.width)
+ log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+ log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
- log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
- big_lhs.remove2(lhs, &big_rhs);
- big_lhs.append(lhs);
- big_rhs.append(rhs);
+ log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+
+ std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
+ std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
+
+ std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
+ std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
+
+ for (size_t i = 0; i < value_lhs.size(); i++)
+ prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
}
- log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
- check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
- return satgen.signals_eq(big_lhs, big_rhs, timestep);
+ return ez.expression(ezSAT::OpAnd, prove_bits);
}
void force_unique_state(int timestep_from, int timestep_to)
@@ -567,17 +673,18 @@ struct SatPass : public Pass {
log(" -set <signal> <value>\n");
log(" set the specified signal to the specified value.\n");
log("\n");
- #if 0
log(" -set-def <signal>\n");
log(" add a constraint that all bits of the given signal must be defined\n");
log("\n");
- log(" -set-undef <signal>\n");
+ log(" -set-any-undef <signal>\n");
log(" add a constraint that at least one bit of the given signal is undefined\n");
log("\n");
log(" -set-all-undef <signal>\n");
log(" add a constraint that all bits of the given signal are undefined\n");
log("\n");
- #endif
+ log(" -set-def-inputs\n");
+ log(" add -set-def constraints for all module inputs\n");
+ log("\n");
log(" -show <signal>\n");
log(" show the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
@@ -596,13 +703,11 @@ struct SatPass : public Pass {
log(" set or unset the specified signal to the specified value in the\n");
log(" given timestep. this has priority over a -set for the same signal.\n");
log("\n");
- #if 0
- log(" -set-def <N> <signal>\n");
- log(" -set-undef <N> <signal>\n");
- log(" -set-all-undef <N> <signal>\n");
+ log(" -set-def-at <N> <signal>\n");
+ log(" -set-any-undef-at <N> <signal>\n");
+ log(" -set-all-undef-at <N> <signal>\n");
log(" add undef contraints in the given timestep.\n");
log("\n");
- #endif
log(" -set-init <signal> <value>\n");
log(" set the initial value for the register driving the signal to the value\n");
log("\n");
@@ -617,6 +722,10 @@ struct SatPass : public Pass {
log(" induction proof it is proven that the condition holds forever after\n");
log(" the number of time steps passed using -seq.\n");
log("\n");
+ log(" -prove-x <signal> <value>\n");
+ log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
+ log(" the right hand side. Useful for equivialence checking.\n");
+ log("\n");
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
@@ -632,13 +741,13 @@ struct SatPass : public Pass {
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
- std::vector<std::pair<std::string, std::string>> sets, sets_init, prove;
+ std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
- std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at;
- std::vector<std::string> shows, sets_def, sets_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
+ std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
- bool verify = false, fail_on_timeout = false, enable_undef = false;
- bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true;
+ bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+ bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -682,23 +791,28 @@ struct SatPass : public Pass {
max_undef = true;
continue;
}
+ if (args[argidx] == "-set-def-inputs") {
+ enable_undef = true;
+ set_def_inputs = true;
+ continue;
+ }
if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
continue;
}
- if (args[argidx] == "-set-def" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
sets_def.push_back(args[++argidx]);
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-undef" && argidx+2 < args.size()) {
- sets_undef.push_back(args[++argidx]);
+ if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
+ sets_any_undef.push_back(args[++argidx]);
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-all-undef" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
sets_all_undef.push_back(args[++argidx]);
enable_undef = true;
continue;
@@ -709,6 +823,13 @@ struct SatPass : public Pass {
prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
continue;
}
+ if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ enable_undef = true;
+ continue;
+ }
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
seq_len = atoi(args[++argidx].c_str());
continue;
@@ -731,9 +852,9 @@ struct SatPass : public Pass {
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-undef-at" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
int timestep = atoi(args[++argidx].c_str());
- sets_undef_at[timestep].push_back(args[++argidx]);
+ sets_any_undef_at[timestep].push_back(args[++argidx]);
enable_undef = true;
continue;
}
@@ -773,10 +894,16 @@ struct SatPass : public Pass {
if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n");
- if (prove.size() == 0 && verify)
+ if (prove.size() + prove_x.size() == 0 && verify)
log_cmd_error("Got -verify but nothing to prove!\n");
- if (prove.size() > 0 && seq_len > 0)
+ if (set_def_inputs) {
+ for (auto &it : module->wires)
+ if (it.second->port_input)
+ sets_def.push_back(it.second->name);
+ }
+
+ if (prove.size() + prove_x.size() > 0 && seq_len > 0)
{
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -786,15 +913,16 @@ struct SatPass : public Pass {
basecase.sets = sets;
basecase.prove = prove;
+ basecase.prove_x = prove_x;
basecase.sets_at = sets_at;
basecase.unsets_at = unsets_at;
basecase.shows = shows;
basecase.timeout = timeout;
basecase.sets_def = sets_def;
- basecase.sets_undef = sets_undef;
+ basecase.sets_any_undef = sets_any_undef;
basecase.sets_all_undef = sets_all_undef;
basecase.sets_def_at = sets_def_at;
- basecase.sets_undef_at = sets_undef_at;
+ basecase.sets_any_undef_at = sets_any_undef_at;
basecase.sets_all_undef_at = sets_all_undef_at;
basecase.sets_init = sets_init;
basecase.set_init_undef = set_init_undef;
@@ -806,16 +934,12 @@ struct SatPass : public Pass {
inductstep.sets = sets;
inductstep.prove = prove;
+ inductstep.prove_x = prove_x;
inductstep.shows = shows;
inductstep.timeout = timeout;
inductstep.sets_def = sets_def;
- inductstep.sets_undef = sets_undef;
+ inductstep.sets_any_undef = sets_any_undef;
inductstep.sets_all_undef = sets_all_undef;
- inductstep.sets_def_at = sets_def_at;
- inductstep.sets_undef_at = sets_undef_at;
- inductstep.sets_all_undef_at = sets_all_undef_at;
- inductstep.sets_init = sets_init;
- inductstep.set_init_undef = set_init_undef;
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
inductstep.setup(1);
@@ -896,15 +1020,16 @@ struct SatPass : public Pass {
sathelper.sets = sets;
sathelper.prove = prove;
+ sathelper.prove_x = prove_x;
sathelper.sets_at = sets_at;
sathelper.unsets_at = unsets_at;
sathelper.shows = shows;
sathelper.timeout = timeout;
sathelper.sets_def = sets_def;
- sathelper.sets_undef = sets_undef;
+ sathelper.sets_any_undef = sets_any_undef;
sathelper.sets_all_undef = sets_all_undef;
sathelper.sets_def_at = sets_def_at;
- sathelper.sets_undef_at = sets_undef_at;
+ sathelper.sets_any_undef_at = sets_any_undef_at;
sathelper.sets_all_undef_at = sets_all_undef_at;
sathelper.sets_init = sets_init;
sathelper.set_init_undef = set_init_undef;
@@ -912,7 +1037,7 @@ struct SatPass : public Pass {
if (seq_len == 0) {
sathelper.setup();
- if (sathelper.prove.size() > 0)
+ if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
} else {
for (int timestep = 1; timestep <= seq_len; timestep++)
@@ -939,7 +1064,7 @@ struct SatPass : public Pass {
sathelper.maximize_undefs();
}
- if (prove.size() == 0) {
+ if (prove.size() + prove_x.size() == 0) {
log("SAT solving finished - model found:\n");
} else {
log("SAT proof finished - model found: FAIL!\n");
@@ -965,7 +1090,7 @@ struct SatPass : public Pass {
goto timeout;
if (rerun_counter)
log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
- else if (prove.size() == 0)
+ else if (prove.size() + prove_x.size() == 0)
log("SAT solving finished - no model found.\n");
else {
log("SAT proof finished - no model found: SUCCESS!\n");
diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index 0324afa8..40caf780 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -106,6 +106,7 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
LibertyAst *best_cell = NULL;
std::map<std::string, char> best_cell_ports;
int best_cell_pins = 0;
+ float best_cell_area = 0;
if (ast->id != "library")
log_error("Format error in liberty file.\n");
@@ -141,6 +142,11 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
this_cell_ports[cell_rst_pin] = 'R';
this_cell_ports[cell_next_pin] = 'D';
+ float area = 0;
+ LibertyAst *ar = cell->find("area");
+ if (ar != NULL && !ar->value.empty())
+ area = atof(ar->value.c_str());
+
int num_pins = 0;
bool found_output = false;
for (auto pin : cell->children)
@@ -174,14 +180,18 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
if (!found_output || (best_cell != NULL && num_pins > best_cell_pins))
continue;
+ if (best_cell != NULL && num_pins == best_cell_pins && area > best_cell_area)
+ continue;
+
best_cell = cell;
best_cell_pins = num_pins;
+ best_cell_area = area;
best_cell_ports.swap(this_cell_ports);
continue_cell_loop:;
}
if (best_cell != NULL) {
- log(" cell %s is a direct match for cell type %s.\n", best_cell->args[0].c_str(), cell_type.substr(1).c_str());
+ log(" cell %s (pins=%d, area=%.2f) is a direct match for cell type %s.\n", best_cell->args[0].c_str(), best_cell_pins, best_cell_area, cell_type.substr(1).c_str());
cell_mappings[cell_type].cell_name = best_cell->args[0];
cell_mappings[cell_type].ports = best_cell_ports;
}
@@ -192,6 +202,7 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
LibertyAst *best_cell = NULL;
std::map<std::string, char> best_cell_ports;
int best_cell_pins = 0;
+ float best_cell_area = 0;
if (ast->id != "library")
log_error("Format error in liberty file.\n");
@@ -223,6 +234,11 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
this_cell_ports[cell_clr_pin] = 'R';
this_cell_ports[cell_next_pin] = 'D';
+ float area = 0;
+ LibertyAst *ar = cell->find("area");
+ if (ar != NULL && !ar->value.empty())
+ area = atof(ar->value.c_str());
+
int num_pins = 0;
bool found_output = false;
for (auto pin : cell->children)
@@ -256,14 +272,18 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
if (!found_output || (best_cell != NULL && num_pins > best_cell_pins))
continue;
+ if (best_cell != NULL && num_pins == best_cell_pins && area > best_cell_area)
+ continue;
+
best_cell = cell;
best_cell_pins = num_pins;
+ best_cell_area = area;
best_cell_ports.swap(this_cell_ports);
continue_cell_loop:;
}
if (best_cell != NULL) {
- log(" cell %s is a direct match for cell type %s.\n", best_cell->args[0].c_str(), cell_type.substr(1).c_str());
+ log(" cell %s (pins=%d, area=%.2f) is a direct match for cell type %s.\n", best_cell->args[0].c_str(), best_cell_pins, best_cell_area, cell_type.substr(1).c_str());
cell_mappings[cell_type].cell_name = best_cell->args[0];
cell_mappings[cell_type].ports = best_cell_ports;
}
@@ -399,6 +419,7 @@ static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module)
if (port.second == '0' || port.second == '1') {
sig = RTLIL::SigSpec(port.second == '0' ? 0 : 1, 1);
} else
+ if (port.second != 0)
log_abort();
new_cell->connections["\\" + port.first] = sig;
}
@@ -473,16 +494,26 @@ struct DfflibmapPass : public Pass {
find_cell_sr(libparser.ast, "$_DFFSR_PPN_", true, true, false);
find_cell_sr(libparser.ast, "$_DFFSR_PPP_", true, true, true);
- bool keep_running = true;
- while (keep_running) {
- keep_running = false;
- keep_running |= expand_cellmap("$_DFF_*_", "C");
- keep_running |= expand_cellmap("$_DFF_*??_", "C");
- keep_running |= expand_cellmap("$_DFF_?*?_", "R");
- keep_running |= expand_cellmap("$_DFF_??*_", "DQ");
- keep_running |= expand_cellmap("$_DFFSR_*??_", "C");
- keep_running |= expand_cellmap("$_DFFSR_?*?_", "S");
- keep_running |= expand_cellmap("$_DFFSR_??*_", "R");
+ // try to implement as many cells as possible just by inverting
+ // the SET and RESET pins. If necessary, implement cell types
+ // by inverting both D and Q. Only invert clock pins if there
+ // is no other way of implementing the cell.
+ while (1)
+ {
+ if (expand_cellmap("$_DFF_?*?_", "R") ||
+ expand_cellmap("$_DFFSR_?*?_", "S") ||
+ expand_cellmap("$_DFFSR_??*_", "R"))
+ continue;
+
+ if (expand_cellmap("$_DFF_??*_", "DQ"))
+ continue;
+
+ if (expand_cellmap("$_DFF_*_", "C") ||
+ expand_cellmap("$_DFF_*??_", "C") ||
+ expand_cellmap("$_DFFSR_*??_", "C"))
+ continue;
+
+ break;
}
map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN0_");
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index fbd86d59..e06a80bb 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -60,16 +60,28 @@ static void simplemap_pos(RTLIL::Module *module, RTLIL::Cell *cell)
module->connections.push_back(RTLIL::SigSig(sig_y, sig_a));
}
+static void simplemap_bu0(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+ int width = cell->parameters.at("\\Y_WIDTH").as_int();
+
+ RTLIL::SigSpec sig_a = cell->connections.at("\\A");
+ sig_a.extend_u0(width, cell->parameters.at("\\A_SIGNED").as_bool());
+
+ RTLIL::SigSpec sig_y = cell->connections.at("\\Y");
+
+ module->connections.push_back(RTLIL::SigSig(sig_y, sig_a));
+}
+
static void simplemap_bitop(RTLIL::Module *module, RTLIL::Cell *cell)
{
int width = cell->parameters.at("\\Y_WIDTH").as_int();
RTLIL::SigSpec sig_a = cell->connections.at("\\A");
- sig_a.extend(width, cell->parameters.at("\\A_SIGNED").as_bool());
+ sig_a.extend_u0(width, cell->parameters.at("\\A_SIGNED").as_bool());
sig_a.expand();
RTLIL::SigSpec sig_b = cell->connections.at("\\B");
- sig_b.extend(width, cell->parameters.at("\\B_SIGNED").as_bool());
+ sig_b.extend_u0(width, cell->parameters.at("\\B_SIGNED").as_bool());
sig_b.expand();
RTLIL::SigSpec sig_y = cell->connections.at("\\Y");
@@ -454,6 +466,7 @@ void simplemap_get_mappers(std::map<std::string, void(*)(RTLIL::Module*, RTLIL::
{
mappers["$not"] = simplemap_not;
mappers["$pos"] = simplemap_pos;
+ mappers["$bu0"] = simplemap_bu0;
mappers["$and"] = simplemap_bitop;
mappers["$or"] = simplemap_bitop;
mappers["$xor"] = simplemap_bitop;
@@ -485,7 +498,7 @@ struct SimplemapPass : public Pass {
log("This pass maps a small selection of simple coarse-grain cells to yosys gate\n");
log("primitives. The following internal cell types are mapped by this pass:\n");
log("\n");
- log(" $not, $pos, $and, $or, $xor, $xnor\n");
+ log(" $not, $pos, $bu0, $and, $or, $xor, $xnor\n");
log(" $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n");
log(" $logic_not, $logic_and, $logic_or, $mux\n");
log(" $sr, $dff, $dffsr, $adff, $dlatch\n");
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index b4440ea8..034244ca 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -376,6 +376,42 @@ endmodule
// --------------------------------------------------------
+module \$eqx (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 0;
+parameter B_WIDTH = 0;
+parameter Y_WIDTH = 0;
+
+`INPUT_A
+`INPUT_B
+output [Y_WIDTH-1:0] Y;
+
+assign Y = A_BUF.val === B_BUF.val;
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$nex (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 0;
+parameter B_WIDTH = 0;
+parameter Y_WIDTH = 0;
+
+`INPUT_A
+`INPUT_B
+output [Y_WIDTH-1:0] Y;
+
+assign Y = A_BUF.val !== B_BUF.val;
+
+endmodule
+
+// --------------------------------------------------------
+
module \$ge (A, B, Y);
parameter A_SIGNED = 0;
diff --git a/techlibs/common/stdcells.v b/techlibs/common/stdcells.v
index ef4b96f7..4e764078 100644
--- a/techlibs/common/stdcells.v
+++ b/techlibs/common/stdcells.v
@@ -44,6 +44,12 @@ endmodule
// --------------------------------------------------------
+(* techmap_simplemap *)
+module \$bu0 ;
+endmodule
+
+// --------------------------------------------------------
+
module \$neg (A, Y);
parameter A_SIGNED = 0;
@@ -109,7 +115,6 @@ endmodule
module \$reduce_xor ;
endmodule
-
// --------------------------------------------------------
(* techmap_simplemap *)
@@ -212,7 +217,7 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
+localparam WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -265,7 +270,7 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = Y_WIDTH;
+localparam WIDTH = Y_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -318,7 +323,7 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
+localparam WIDTH = A_WIDTH > Y_WIDTH ? A_WIDTH : Y_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -381,11 +386,11 @@ output X, Y;
// {t1, t2} = A + B
wire t1, t2, t3;
- \$_AND_ gate1 ( .A(A), .B(B), .Y(t1) );
- \$_XOR_ gate2 ( .A(A), .B(B), .Y(t2) );
- \$_AND_ gate3 ( .A(t2), .B(C), .Y(t3) );
- \$_XOR_ gate4 ( .A(t2), .B(C), .Y(Y) );
- \$_OR_ gate5 ( .A(t1), .B(t3), .Y(X) );
+\$_AND_ gate1 ( .A(A), .B(B), .Y(t1) );
+\$_XOR_ gate2 ( .A(A), .B(B), .Y(t2) );
+\$_AND_ gate3 ( .A(t2), .B(C), .Y(t3) );
+\$_XOR_ gate4 ( .A(t2), .B(C), .Y(Y) );
+\$_OR_ gate5 ( .A(t1), .B(t3), .Y(X) );
endmodule
@@ -432,7 +437,7 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -440,8 +445,8 @@ output [Y_WIDTH-1:0] Y;
wire carry, carry_sign;
wire [WIDTH-1:0] A_buf, B_buf, Y_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
\$__alu #(
.WIDTH(WIDTH)
@@ -481,7 +486,7 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -489,8 +494,8 @@ output [Y_WIDTH-1:0] Y;
wire carry, carry_sign;
wire [WIDTH-1:0] A_buf, B_buf, Y_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
\$__alu #(
.WIDTH(WIDTH)
@@ -530,7 +535,7 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -538,8 +543,8 @@ output [Y_WIDTH-1:0] Y;
wire carry, carry_sign;
wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$bu0 #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$bu0 #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
assign Y = ~|(A_buf ^ B_buf);
@@ -555,7 +560,57 @@ parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;
-parameter WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+
+input [A_WIDTH-1:0] A;
+input [B_WIDTH-1:0] B;
+output [Y_WIDTH-1:0] Y;
+
+wire carry, carry_sign;
+wire [WIDTH-1:0] A_buf, B_buf;
+\$bu0 #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$bu0 #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+
+assign Y = |(A_buf ^ B_buf);
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$eqx (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 1;
+parameter B_WIDTH = 1;
+parameter Y_WIDTH = 1;
+
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
+
+input [A_WIDTH-1:0] A;
+input [B_WIDTH-1:0] B;
+output [Y_WIDTH-1:0] Y;
+
+wire carry, carry_sign;
+wire [WIDTH-1:0] A_buf, B_buf;
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+
+assign Y = ~|(A_buf ^ B_buf);
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$nex (A, B, Y);
+
+parameter A_SIGNED = 0;
+parameter B_SIGNED = 0;
+parameter A_WIDTH = 1;
+parameter B_WIDTH = 1;
+parameter Y_WIDTH = 1;
+
+localparam WIDTH = A_WIDTH > B_WIDTH ? A_WIDTH : B_WIDTH;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
@@ -563,8 +618,8 @@ output [Y_WIDTH-1:0] Y;
wire carry, carry_sign;
wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
assign Y = |(A_buf ^ B_buf);
@@ -641,8 +696,8 @@ input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;
wire [Y_WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
\$__alu #(
.WIDTH(Y_WIDTH)
@@ -670,8 +725,8 @@ input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;
wire [Y_WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
\$__alu #(
.WIDTH(Y_WIDTH)
@@ -719,8 +774,8 @@ input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;
wire [Y_WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf));
\$__arraymul #(
.WIDTH(Y_WIDTH)
@@ -781,12 +836,12 @@ input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y, R;
wire [WIDTH-1:0] A_buf, B_buf;
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
-\$pos #(.A_SIGNED(A_SIGNED && B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
+\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(WIDTH)) A_conv (.A(A), .Y(A_buf));
+\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(WIDTH)) B_conv (.A(B), .Y(B_buf));
wire [WIDTH-1:0] A_buf_u, B_buf_u, Y_u, R_u;
-assign A_buf_u = A_SIGNED && B_SIGNED && A_buf[WIDTH-1] ? -A_buf : A_buf;
-assign B_buf_u = A_SIGNED && B_SIGNED && B_buf[WIDTH-1] ? -B_buf : B_buf;
+assign A_buf_u = A_SIGNED && A_buf[WIDTH-1] ? -A_buf : A_buf;
+assign B_buf_u = B_SIGNED && B_buf[WIDTH-1] ? -B_buf : B_buf;
\$__div_mod_u #(
.WIDTH(WIDTH)
@@ -816,9 +871,6 @@ input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;
-wire [Y_WIDTH-1:0] Y_buf;
-wire [Y_WIDTH-1:0] Y_div_zero;
-
\$__div_mod #(
.A_SIGNED(A_SIGNED),
.B_SIGNED(B_SIGNED),
@@ -828,20 +880,9 @@ wire [Y_WIDTH-1:0] Y_div_zero;
) div_mod (
.A(A),
.B(B),
- .Y(Y_buf)
+ .Y(Y)
);
-// explicitly force the division-by-zero behavior found in other synthesis tools
-generate begin
- if (A_SIGNED && B_SIGNED) begin:make_div_zero
- assign Y_div_zero = A[A_WIDTH-1] ? {Y_WIDTH{1'b0}} | 1'b1 : {Y_WIDTH{1'b1}};
- end else begin:make_div_zero
- assign Y_div_zero = {A_WIDTH{1'b1}};
- end
-end endgenerate
-
-assign Y = B ? Y_buf : Y_div_zero;
-
endmodule
// --------------------------------------------------------
@@ -858,9 +899,6 @@ input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;
-wire [Y_WIDTH-1:0] Y_buf;
-wire [Y_WIDTH-1:0] Y_div_zero;
-
\$__div_mod #(
.A_SIGNED(A_SIGNED),
.B_SIGNED(B_SIGNED),
@@ -870,21 +908,9 @@ wire [Y_WIDTH-1:0] Y_div_zero;
) div_mod (
.A(A),
.B(B),
- .R(Y_buf)
+ .R(Y)
);
-// explicitly force the division-by-zero behavior found in other synthesis tools
-localparam div_zero_copy_a_bits = A_WIDTH < B_WIDTH ? A_WIDTH : B_WIDTH;
-generate begin
- if (A_SIGNED && B_SIGNED) begin:make_div_zero
- assign Y_div_zero = $signed(A[div_zero_copy_a_bits-1:0]);
- end else begin:make_div_zero
- assign Y_div_zero = $unsigned(A[div_zero_copy_a_bits-1:0]);
- end
-end endgenerate
-
-assign Y = B ? Y_buf : Y_div_zero;
-
endmodule
/****
diff --git a/tests/simple/macros.v b/tests/simple/macros.v
new file mode 100644
index 00000000..cda46cb4
--- /dev/null
+++ b/tests/simple/macros.v
@@ -0,0 +1,237 @@
+
+module test_def(a, y);
+
+`define MSB_LSB_SEP :
+`define get_msb(off, len) ((off)+(len)-1)
+`define get_lsb(off, len) (off)
+`define sel_bits(offset, len) `get_msb(offset, len) `MSB_LSB_SEP `get_lsb(offset, len)
+
+input [31:0] a;
+output [7:0] y;
+
+assign y = a[`sel_bits(16, 8)];
+
+endmodule
+
+// ---------------------------------------------------
+
+module test_ifdef(a, y);
+
+input [2:0] a;
+output reg [31:0] y;
+
+always @* begin
+ y = 0;
+
+ `undef X
+ `ifdef X
+ y = y + 42;
+ `else
+ `undef A
+ `undef B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `undef A
+ `define B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `undef B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `define B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ // ------------------------------------
+ `undef A
+ `undef B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `undef A
+ `define B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `undef B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `define B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ // ------------------------------------
+ `undef A
+ `ifdef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `ifdef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ // ------------------------------------
+ `undef A
+ `ifndef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `ifndef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `endif
+
+ `define X
+ `ifdef X
+ `undef A
+ `undef B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `undef A
+ `define B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `undef B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `define B
+ `ifdef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ // ------------------------------------
+ `undef A
+ `undef B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `undef A
+ `define B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `undef B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `define B
+ `ifndef A
+ y = (y << 1) | a[0];
+ `elsif B
+ y = (y << 1) | a[1];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ // ------------------------------------
+ `undef A
+ `ifdef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `ifdef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ // ------------------------------------
+ `undef A
+ `ifndef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `define A
+ `ifndef A
+ y = (y << 1) | a[0];
+ `else
+ y = (y << 1) | a[2];
+ `endif
+ `else
+ y = y + 42;
+ `endif
+end
+
+endmodule
diff --git a/tests/simple/memory.v b/tests/simple/memory.v
index aea014a2..eaeee01d 100644
--- a/tests/simple/memory.v
+++ b/tests/simple/memory.v
@@ -1,4 +1,21 @@
+module test00(clk, setA, setB, y);
+
+input clk, setA, setB;
+output y;
+reg mem [1:0];
+
+always @(posedge clk) begin
+ if (setA) mem[0] <= 0; // this is line 9
+ if (setB) mem[0] <= 1; // this is line 10
+end
+
+assign y = mem[0];
+
+endmodule
+
+// ----------------------------------------------------------
+
module test01(clk, wr_en, wr_addr, wr_value, rd_addr, rd_value);
input clk, wr_en;
diff --git a/tests/simple/multiplier.v b/tests/simple/multiplier.v
new file mode 100644
index 00000000..3c0aa1fc
--- /dev/null
+++ b/tests/simple/multiplier.v
@@ -0,0 +1,132 @@
+
+// Via http://www.edaplayground.com/s/6/591
+// stackoverflow 20556634
+// http://stackoverflow.com/questions/20556634/how-can-i-iteratively-create-buses-of-parameterized-size-to-connect-modules-also
+
+// Code your design here
+`define macro_args
+`define indexed_part_select
+
+module Multiplier_flat #(parameter M = 4, parameter N = 4)(
+input [M-1:0] A, //Input A, size M
+input [N-1:0] B, //Input B, size N
+output [M+N-1:0] P ); //Output P (product), size M+N
+
+/* Calculate LSB using Wolfram Alpha
+ N==3 : http://www.wolframalpha.com/input/?i=0%2C+4%2C+9%2C+15%2C+...
+ N==4 : http://www.wolframalpha.com/input/?i=0%2C+5%2C+11%2C+18%2C+26%2C+35%2C+...
+ N==5 : http://www.wolframalpha.com/input/?i=0%2C+6%2C+13%2C+21%2C+30%2C+...
+ */
+`ifdef macro_args
+// initial $display("Use Macro Args");
+`define calc_pp_lsb(n) (((n)-1)*((n)+2*M)/2)
+//`define calc_pp_msb(n) (`calc_pp_lsb(n+1)-1)
+`define calc_pp_msb(n) ((n**2+(2*M+1)*n-2)/2)
+//`define calc_range(n) `calc_pp_msb(n):`calc_pp_lsb(n)
+`define calc_pp_range(n) `calc_pp_lsb(n) +: (M+n)
+
+wire [`calc_pp_msb(N):0] PP;
+assign PP[`calc_pp_range(1)] = { 1'b0 , { A & {M{B[0]}} } };
+assign P = PP[`calc_pp_range(N)];
+`elsif indexed_part_select
+// initial $display("Use Indexed Part Select");
+localparam MSB = (N**2+(2*M+1)*N-2)/2;
+wire [MSB:0] PP;
+assign PP[M:0] = { 1'b0 , { A & {M{B[0]}} } };
+assign P = PP[MSB -: M+N];
+`else
+// initial $display("Use Worst Case");
+localparam MSB = (N**2+(2*M+1)*N-2)/2;
+wire [MSB:0] PP;
+assign PP[M:0] = { 1'b0 , { A & {M{B[0]}} } };
+assign P = PP[MSB : MSB+1-M-N];
+`endif
+
+genvar i;
+generate
+for (i=1; i < N; i=i+1)
+begin: addPartialProduct
+ wire [M+i-1:0] gA,gB,gS;
+ wire Cout;
+ assign gA = { A & {M{B[i]}} , {i{1'b0}} };
+ `ifdef macro_args
+ assign gB = PP[`calc_pp_range(i)];
+ assign PP[`calc_pp_range(i+1)] = {Cout,gS};
+ `elsif indexed_part_select
+ assign gB = PP[(i-1)*(i+2*M)/2 +: M+i];
+ assign PP[i*((i+1)+2*M)/2 +: M+i+1] = {Cout,gS};
+ `else
+ localparam LSB = (i-1)*(i+2*M)/2;
+ localparam MSB = (i**2+(2*M+1)*i-2)/2;
+ localparam MSB2 = ((i+1)**2+(2*M+1)*(i+1)-2)/2;
+ assign gB = PP[MSB : LSB];
+ assign PP[ MSB2 : MSB+1] = {Cout,gS};
+ `endif
+ RippleCarryAdder#(M+i) adder( .A(gA), .B(gB), .S(gS), .Cin (1'b0), .Cout(Cout) );
+end
+endgenerate
+
+`ifdef macro_args
+// Cleanup global space
+`undef calc_pp_range
+`undef calc_pp_msb
+`undef calc_pp_lsb
+`endif
+endmodule
+
+module Multiplier_2D #(parameter M = 4, parameter N = 4)(
+input [M-1:0] A, //Input A, size M
+input [N-1:0] B, //Input B, size N
+output [M+N-1:0] P ); //Output P (product), size M+N
+
+wire [M+N-1:0] PP [N-1:0];
+
+// Note: bits PP[0][M+N-1:M+1] are never used. Unused bits are optimized out during synthesis
+//assign PP[0][M:0] = { {1'b0} , { A & {M{B[0]}} } };
+//assign PP[0][M+N-1:M+1] = {(N-1){1'b0}}; // uncomment to make probing readable
+assign PP[0] = { {N{1'b0}} , { A & {M{B[0]}} } };
+assign P = PP[N-1];
+
+genvar i;
+generate
+for (i=1; i < N; i=i+1)
+begin: addPartialProduct
+ wire [M+i-1:0] gA,gB,gS; wire Cout;
+ assign gA = { A & {M{B[i]}} , {i{1'b0}} };
+ assign gB = PP[i-1][M+i-1:0];
+ //assign PP[i][M+i:0] = {Cout,gS};
+ //if (i+1<N) assign PP[i][M+N-1:M+i+1] = {(N-i){1'b0}}; // uncomment to make probing readable
+ assign PP[i] = { {(N-i){1'b0}}, Cout, gS};
+ RippleCarryAdder#(M+i) adder(
+ .A(gA), .B(gB), .S(gS), .Cin(1'b0), .Cout(Cout) );
+end
+endgenerate
+
+//always@* foreach(S[i]) $display("S[%0d]:%b",i,S[i]);
+
+endmodule
+
+module RippleCarryAdder#(parameter N = 4)(A,B,Cin,S,Cout);
+
+input [N-1:0] A;
+input [N-1:0] B;
+input Cin;
+output [N-1:0] S;
+output Cout;
+wire [N:0] CC;
+
+assign CC[0] = Cin;
+assign Cout = CC[N];
+genvar i;
+generate
+for (i=0; i < N; i=i+1)
+begin: addbit
+ FullAdder unit(A[i],B[i],CC[i],S[i],CC[i+1]);
+end
+endgenerate
+
+endmodule
+
+module FullAdder(input A,B,Cin, output wire S,Cout);
+assign {Cout,S} = A+B+Cin;
+endmodule
diff --git a/tests/simple/undef_eqx_nex.v b/tests/simple/undef_eqx_nex.v
new file mode 100644
index 00000000..63912a2f
--- /dev/null
+++ b/tests/simple/undef_eqx_nex.v
@@ -0,0 +1,11 @@
+module test(y);
+output [7:0] y;
+assign y[0] = 0/0;
+assign y[1] = 0/1;
+assign y[2] = 0/0 == 32'bx;
+assign y[3] = 0/0 != 32'bx;
+assign y[4] = 0/0 === 32'bx;
+assign y[5] = 0/0 !== 32'bx;
+assign y[6] = 0/1 === 32'bx;
+assign y[7] = 0/1 !== 32'bx;
+endmodule
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 5a302bcd..b1c330d8 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -9,13 +9,14 @@ keeprunning=false
backend_opts="-noattr -noexpr"
kompare_xst=false
scriptfiles=""
+scriptopt=""
toolsdir="$(cd $(dirname $0); pwd)"
if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdata ]; then
( set -ex; gcc -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1
fi
-while getopts iml:wkvrxs: opt; do
+while getopts iml:wkvrxs:p: opt; do
case "$opt" in
i)
use_isim=true ;;
@@ -30,14 +31,16 @@ while getopts iml:wkvrxs: opt; do
v)
verbose=true ;;
r)
- backend_opts="$backend_opts norename" ;;
+ backend_opts="$backend_opts -norename" ;;
x)
kompare_xst=true ;;
s)
[[ "$OPTARG" == /* ]] || OPTARG="$PWD/$OPTARG"
scriptfiles="$scriptfiles $OPTARG" ;;
+ p)
+ scriptopt="$OPTARG" ;;
*)
- echo "Usage: $0 [-i] [-w] [-k] [-v] [-r] [-x] [-l libs] [-s script] verilog-files\n" >&2
+ echo "Usage: $0 [-i] [-w] [-k] [-v] [-r] [-x] [-l libs] [-s script] [-p cmdstring] verilog-files\n" >&2
exit 1
esac
done
@@ -147,10 +150,11 @@ do
if [ -n "$scriptfiles" ]; then
test_passes
+ elif [ -n "$scriptopt" ]; then
+ test_passes -p "$scriptopt"
else
- test_passes -p "hierarchy; proc; memory; opt; fsm; opt"
- test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap; opt"
- # test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap -opt; opt; abc; opt"
+ test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt"
+ test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt; techmap; opt; abc -dff; opt"
fi
touch ../${bn}.log
}