Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor

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
+ * Improvements in Verilog frontend:
-   targets 'make abc' and 'make install-abc' are now obsolete.
+     - 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
 

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

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");

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("$lt",  "<")
-	HANDLE_BINOP("$le", "<=")
+	HANDLE_BINOP("$le",  "<=")
-	HANDLE_BINOP("$eq", "==")
+	HANDLE_BINOP("$eq",  "==")
-	HANDLE_BINOP("$ne", "!=")
+	HANDLE_BINOP("$ne",  "!=")
-	HANDLE_BINOP("$ge", ">=")
+	HANDLE_BINOP("$eqx", "===")
-	HANDLE_BINOP("$gt", ">")
+	HANDLE_BINOP("$nex", "!==")
+	HANDLE_BINOP("$ge",  ">=")
+	HANDLE_BINOP("$gt",  ">")
 
 	HANDLE_BINOP("$add", "+")
 	HANDLE_BINOP("$sub", "-")

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 = "+";   }

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,

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_LT:  type_name = "$lt"; }
-	if (0) { case AST_LE: type_name = "$le"; }
+	if (0) { case AST_LE:  type_name = "$le"; }
-	if (0) { case AST_EQ: type_name = "$eq"; }
+	if (0) { case AST_EQ:  type_name = "$eq"; }
-	if (0) { case AST_NE: type_name = "$ne"; }
+	if (0) { case AST_NE:  type_name = "$ne"; }
-	if (0) { case AST_GE: type_name = "$ge"; }
+	if (0) { case AST_EQX: type_name = "$eqx"; }
-	if (0) { case AST_GT: type_name = "$gt"; }
+	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;
 

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_LT:  const_func = RTLIL::const_lt; }
-		if (0) { case AST_LE: const_func = RTLIL::const_le; }
+		if (0) { case AST_LE:  const_func = RTLIL::const_le; }
-		if (0) { case AST_EQ: const_func = RTLIL::const_eq; }
+		if (0) { case AST_EQ:  const_func = RTLIL::const_eq; }
-		if (0) { case AST_NE: const_func = RTLIL::const_ne; }
+		if (0) { case AST_NE:  const_func = RTLIL::const_ne; }
-		if (0) { case AST_GE: const_func = RTLIL::const_ge; }
+		if (0) { case AST_EQX: const_func = RTLIL::const_eqx; }
-		if (0) { case AST_GT: const_func = RTLIL::const_gt; }
+		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;

frontends/verilog/lexer.l

@@ -232,8 +232,8 @@ supply1 { return TOK_SUPPLY1; }
 "<=" { return OP_LE; }
 ">=" { return OP_GE; }
 
-"===" { return OP_EQ; }
+"===" { return OP_EQX; }
-"!==" { return OP_NE; }
+"!==" { return OP_NEX; }
 
 "~&" { return OP_NAND; }
 "~|" { return OP_NOR;  }

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

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 (ch == '`' || strchr(ok, ch) != NULL)
-			if (strchr(ok, ch) == NULL) {
+			while ((ch = next_char()) != 0) {
-				return_char(ch);
+				if (strchr(ok, ch) == NULL) {
-				break;
+					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") {
+				if (state == 0 && tok == "(") {
-					return_char('\n');
+					state = 1;
-					break;
+					skip_spaces();
-				}
-				if (tok == "\\") {
-					char ch = next_char();
-					if (ch == '\n') {
-						value += " ";
-						newline_count++;
-					} else {
-						value += std::string("\\");
-						return_char(ch);
-					}
 				} 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());
+			std::string name = tok.substr(1);
-			insert_input(defines_map[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;
 		}
 

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;

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
 

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

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"));

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);
 };
 

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()) :
+	SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
-			ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
+			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 = forced_signed;
-		bool is_signed = undef_mode;
+		if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
-		if (!undef_mode && 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(), forced_signed);
-		extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), undef_mode);
 		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 = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
-		bool is_signed = undef_mode || (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) {
+			if (model_undef)
-				log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type));
+			{
+				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);

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

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

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
 

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);
-		}
+		} else {
-		if (g.in1 >= 0) {
+			if (g.in1 >= 0) {
-			edges[g.in1].insert(g.id);
+				edges[g.in1].insert(g.id);
-			in_edges_count[g.id]++;
+				in_edges_count[g.id]++;
-		}
+			}
-		if (g.in2 >= 0 && g.in2 != g.in1) {
+			if (g.in2 >= 0 && g.in2 != g.in1) {
-			edges[g.in2].insert(g.id);
+				edges[g.in2].insert(g.id);
-			in_edges_count[g.id]++;
+				in_edges_count[g.id]++;
-		}
+			}
-		if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
+			if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
-			edges[g.in3].insert(g.id);
+				edges[g.in3].insert(g.id);
-			in_edges_count[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 (");
+	fprintf(f, ".model netlist\n");
-	bool first = true;
-	for (auto &si : signal_list) {
-		if (!si.is_port)
-			continue;
-		if (!first)
-			fprintf(f, ", ");
-		fprintf(f, "n%d", si.id);
-		first = false;
-	}
-	fprintf(f, "); // %s\n", module->name.c_str());
 
-	int count_input = 0, count_output = 0;
+	int count_input = 0;
+	fprintf(f, ".inputs");
 	for (auto &si : signal_list) {
-		if (si.is_port) {
+		if (!si.is_port || si.type >= 0)
-			if (si.type >= 0)
+			continue;
-				count_output++;
+		fprintf(f, " n%d", si.id);
-			else
+		count_input++;
-				count_input++;
-		}
-		fprintf(f, "%s n%d; // %s\n", si.is_port ? si.type >= 0 ?
-				"output" : "input" : "wire", si.id, log_signal(si.sig));
 	}
+	fprintf(f, "\n");
+
+	int count_output = 0;
+	fprintf(f, ".outputs");
+	for (auto &si : signal_list) {
+		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)
+		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');
+			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')
+		if (si.type == 'n') {
-			fprintf(f, "not (n%d, n%d);\n", si.id, si.in1);
+			fprintf(f, ".names n%d n%d\n", si.in1, si.id);
-		else if (si.type == 'a')
+			fprintf(f, "0 1\n");
-			fprintf(f, "and (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
+		} else if (si.type == 'a') {
-		else if (si.type == 'o')
+			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
-			fprintf(f, "or (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
+			fprintf(f, "11 1\n");
-		else if (si.type == 'x')
+		} else if (si.type == 'o') {
-			fprintf(f, "xor (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
+			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
-		else if (si.type == 'm')
+			fprintf(f, "-1 1\n");
-			fprintf(f, "assign n%d = n%d ? n%d : n%d;\n", si.id, si.in3, si.in2, si.in1);
+			fprintf(f, "1- 1\n");
-		else if (si.type >= 0)
+		} else if (si.type == 'x') {
-			abort();
+			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);
-			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);
 
 		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;
+		bool builtin_lib = liberty_file.empty() && script_file.empty() && !lut_mode;
-		frontend_register["verilog"]->execute(f, p, std::vector<std::string>(), mapped_design);
+		RTLIL::Design *mapped_design = abc_parse_blif(f, builtin_lib ? "\\DFF" : "\\_dff_");
-#else
+
-		RTLIL::Design *mapped_design = lut_mode ? abc_parse_blif(f) : abc_parse_verilog(f);
-#endif
 		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)]++;
+				cell_stats[RTLIL::unescape_id(c->type)]++;
-				if (c->type == "$_const0_" || c->type == "$_const1_") {
+				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.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);
+					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;
+		std::string script_file, liberty_file, constr_file, clk_str;
-		bool cleanup = true;
+		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();

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

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
 

passes/abc/vlparse.cc

@@ -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;
-}
-

passes/abc/vlparse.h

@@ -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
-

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");

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

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");

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++;

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
+			if (input.match("10 ")) {
-			// TODO: "0  " -> replace with "B AND S" gate
+				cell->type = "$_INV_";
-			// TODO: " 1 " -> replace with "A OR S" gate
+				cell->connections["\\A"] = input.extract(0, 1);
-			// TODO: "1  " -> replace with "B OR !S" gate (?)
+				cell->connections.erase("\\B");
-			// TODO: " 0 " -> replace with "A AND !S" gate (?)
+				cell->connections.erase("\\S");
-			if (input.match("  *")) ACTION_DO_Y(x);
+				goto next_cell;
-#endif
+			}
+			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)
+				if (a.chunks[i].wire == NULL && b.chunks[i].wire == NULL && a.chunks[i].data.bits[0] != b.chunks[i].data.bits[0] &&
-					continue;
+						a.chunks[i].data.bits[0] <= RTLIL::State::S1 && b.chunks[i].data.bits[0] <= RTLIL::State::S1) {
-				if (b.chunks[i].wire == NULL && 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;

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;

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)

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;
+	int depth;
-	RTLIL::Module *module;
+	bool inverted;
-	bool try_mode;
+	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;
+	std::set<RTLIL::Cell*> ez_cells;
-	CellTypes ct;
 	SatGen satgen;
-	ConstEval ce;
 
-	SigPool inputs, nodes;
+	FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
-	RTLIL::SigSpec input_sigs;
+			sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
-
+	{
-	SigSet<RTLIL::SigSpec> source_signals;
+		satgen.model_undef = true;
-	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;
 	}
 
-	FreduceHelper(RTLIL::Design *design, RTLIL::Module *module, bool try_mode) :
+	void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
-			design(design), module(module), try_mode(try_mode),
-			sigmap(module), satgen(&ez, design, &sigmap), ce(module)
 	{
+		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);
+	}
+
+	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());
+	}
+
+	void analyze(std::vector<RTLIL::SigBit> &reduced_inputs, RTLIL::SigBit output)
+	{
+		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));
+			}
+		}
+
+		if (verbose_level >= 1)
+			log("      Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
+	}
+};
+
+struct PerformReduction
+{
+	SigMap &sigmap;
+	drivers_t &drivers;
+	std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
+
+	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)
+	{
+		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 {
+			pi_bits.push_back(out);
+			sat_pi.push_back(satgen.importSigSpec(out).front());
+			ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
+		}
+
+		return sigdepth[out];
+	}
+
+	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)
+	{
+		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()));
+		}
+
+		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);
+	}
+
+	void analyze(std::vector<std::set<int>> &results, std::map<int, int> &results_map, std::vector<int> &bucket, int level)
+	{
+		if (bucket.size() <= 1)
+			return;
+
+		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));
+		}
+
+		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]));
+		}
+
+		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]));
+			}
+
+			std::vector<int> buckets_a;
+			std::vector<int> buckets_b;
+
+			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;
+			}
+
+			for (int idx : undef_slaves)
+				out_depth[idx] = std::numeric_limits<int>::max();
+
+			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");
+			}
+
+			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();
+			}
+
+			if (result_idx == -1) {
+				result_idx = results.size();
+				results.push_back(std::set<int>());
+			}
+
+			results[result_idx].insert(bucket.begin(), bucket.end());
+		}
+	}
+
+	void analyze(std::vector<std::vector<equiv_bit_t>> &results)
+	{
+		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 &r : results_buf)
+		{
+			if (r.size() <= 1)
+				continue;
+
+			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);
+			}
+
+			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);
+		}
+	}
+};
+
+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)
+	{
+	}
+
+	int run()
+	{
+		log("Running functional reduction on module %s:\n", RTLIL::id2cstr(module->name));
+
+		CellTypes ct;
 		ct.setup_internals();
 		ct.setup_stdcells();
 
-		xorshift32_state = 123456789;
+		std::vector<std::set<RTLIL::SigBit>> batches;
-		xorshift32();
+		for (auto &it : module->wires)
-		xorshift32();
+			if (it.second->port_input)
-		xorshift32();
+				batches.push_back(sigmap(it.second).to_sigbit_set());
-	}
+		for (auto &it : module->cells) {
-
+			if (ct.cell_known(it.second->type)) {
-	bool run_test(RTLIL::SigSpec test_vec)
+				std::set<RTLIL::SigBit> inputs, outputs;
-	{
+				for (auto &port : it.second->connections) {
-		ce.clear();
+					std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
-		ce.set(input_sigs, test_vec.as_const());
+					if (ct.cell_output(it.second->type, port.first))
-
+						outputs.insert(bits.begin(), bits.end());
-		for (auto &bit : nodes.bits) {
+					else
-			RTLIL::SigSpec nodesig(bit.first, 1, bit.second), nodeval = nodesig;
+						inputs.insert(bits.begin(), bits.end());
-			if (!ce.eval(nodeval)) {
+				}
-				if (!try_mode)
+				std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> drv(it.second, inputs);
-					log_error("Evaluation of node %s failed!\n", log_signal(nodesig));
+				for (auto &bit : outputs)
-				log("FAILED: Evaluation of node %s failed!\n", log_signal(nodesig));
+					drivers[bit] = drv;
-				return false;
+				batches.push_back(outputs);
 			}
-			node_to_data[nodesig].bits.push_back(nodeval.as_const().bits.at(0));
+			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"))));
 		}
 
-		return true;
+		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));
-	void dump_node_data()
+		buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S1));
-	{
+		for (auto &batch : batches)
-		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));
-	}
-
-	bool check(RTLIL::SigSpec sig1, RTLIL::SigSpec sig2)
-	{
-		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;
-		} else {
-			log(" success.\n");
-			if (!sig1.is_fully_const())
-				node_result[sig1].append(sig2);
-			if (!sig2.is_fully_const())
-				node_result[sig2].append(sig1);
-		}
-		return true;
-	}
-
-	bool analyze_const()
-	{
-		for (auto &it : node_to_data)
 		{
-			if (node_result.count(it.first))
+			RTLIL::SigSpec batch_sig(std::vector<RTLIL::SigBit>(batch.begin(), batch.end()));
-				continue;
+			batch_sig.optimize();
-			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;
-		}
-		return true;
-	}
 
-	bool analyze_alias()
+			log("  Finding reduced input cone for signal batch %s%c\n", log_signal(batch_sig), verbose_level ? ':' : '.');
-	{
-	restart:
-		std::map<RTLIL::Const, RTLIL::SigSpec> reverse_map;
 
-		for (auto &it : node_to_data) {
+			FindReducedInputs infinder(sigmap, drivers);
-			if (node_result.count(it.first) && node_result.at(it.first).is_fully_const())
+			for (auto &bit : batch) {
-				continue;
+				std::vector<RTLIL::SigBit> inputs;
-			reverse_map[it.second].append(it.first);
+				infinder.analyze(inputs, bit);
-		}
+				buckets[inputs].push_back(bit);
-
+				bits_count++;
-		for (auto &it : reverse_map)
-		{
-			if (it.second.width <= 1)
-				continue;
-
-			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;
 			}
 		}
-		return true;
+		log("  Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size()));
-	}
 
-	bool toproot_helper(RTLIL::SigSpec cursor, RTLIL::SigSpec stoplist, RTLIL::SigSpec &donelist, int level)
+		std::vector<std::vector<equiv_bit_t>> equiv;
-	{
+		for (auto &bucket : buckets)
-		// log("    %*schecking %s: %s\n", level*2, "", log_signal(cursor), log_signal(stoplist));
+		{
-
+			if (bucket.second.size() == 1)
-		if (stoplist.extract(cursor).width != 0) {
-			// log("    %*s  STOP\n", level*2, "");
-			return false;
-		}
-
-		if (donelist.extract(cursor).width != 0)
-			return true;
-
-		stoplist.append(cursor);
-		std::set<RTLIL::SigSpec> next = source_signals.find(cursor);
-
-		for (auto &it : next)
-			if (!toproot_helper(it, stoplist, donelist, level+1))
-				return false;
-
-		donelist.append(cursor);
-		return true;
-	}
-
-	// 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;
-		}
-		return RTLIL::SigSpec();
-	}
-
-	void update_design_for_group(RTLIL::SigSpec root, RTLIL::SigSpec rest)
-	{
-		SigPool unlink;
-		unlink.add(rest);
-
-		for (auto &cell_it : module->cells) {
-			RTLIL::Cell *cell = cell_it.second;
-			if (!ct.cell_known(cell->type))
 				continue;
-			for (auto &conn : cell->connections)
+
-				if (ct.cell_output(cell->type, conn.first)) {
+			RTLIL::SigSpec bucket_sig(bucket.second);
-					RTLIL::SigSpec sig = sigmap(conn.second);
+			bucket_sig.optimize();
-					sig.expand();
+
-					bool did_something = false;
+			log("  Trying to shatter bucket %s%c\n", log_signal(bucket_sig), verbose_level ? ':' : '.');
-					for (auto &c : sig.chunks) {
+			PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second);
-						if (c.wire == NULL || !unlink.check_any(c))
+			worker.analyze(equiv);
-							continue;
+		}
-						c.wire = new RTLIL::Wire;
+
-						c.wire->name = NEW_ID;
+		log("  Rewiring %d equivialent groups:\n", int(equiv.size()));
-						module->add(c.wire);
+		int rewired_sigbits = 0;
-						assert(c.width == 1);
+		for (auto &grp : equiv)
-						c.offset = 0;
+		{
-						did_something = true;
+			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 (did_something) {
-						sig.optimize();
-						conn.second = sig;
-					}
-				}
-		}
 
-		rest.expand();
+					module->connections.push_back(RTLIL::SigSig(grp[i].bit, inv_sig));
-		for (auto &c : rest.chunks) {
+				}
-			if (c.wire != NULL && !root.is_fully_const()) {
+				else
-				source_signals.erase(c);
+					module->connections.push_back(RTLIL::SigSig(grp[i].bit, grp[0].bit));
-				source_signals.insert(c, root);
+
+				rewired_sigbits++;
 			}
-			module->connections.push_back(RTLIL::SigSig(c, root));
-		}
-	}
-
-	void analyze_groups()
-	{
-		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;
+		log("  Rewired a total of %d signal bits in module %s.\n", rewired_sigbits, RTLIL::id2cstr(module->name));
-		for (auto &it : node_result)
+		return rewired_sigbits;
-			major_to_rest[to_group_major(it.first)].append(it.first);
-
-		for (auto &it : major_to_rest)
-		{
-			RTLIL::SigSig group = it;
-
-			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;
-				}
-				group.second.remove(group.first);
-			}
-
-			group.first.optimize();
-			group.second.sort_and_unify();
-
-			log("  found group: %s -> %s\n", log_signal(group.first), log_signal(group.second));
-			update_design_for_group(group.first, group.second);
-		}
-	}
-
-	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))
-				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;
-
-		// run the analysis and update design
-
-		if (!analyze_const())
-			return;
-
-		if (!analyze_alias())
-			return;
-
-		log("  input vector: %s\n", log_signal(input_sigs));
-		for (auto &test_vec : test_vectors)
-			log("  test vector: %s\n", log_signal(test_vec));
-
-		dump_node_data();
-		analyze_groups();
 	}
 };
 
@@ -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("    -try\n");
+		log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
-		log("        do not issue an error when the analysis fails.\n");
+		log("equivialent nodes.\n");
-		log("        (usually beacause of logic loops in the design)\n");
+		log("\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;
+		verbose_level = 0;
-		bool try_mode = false;
+		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") {
+			if (args[argidx] == "-v") {
-				enable_invert = true;
+				verbose_level = 1;
 				continue;
 			}
-			if (args[argidx] == "-try") {
+			if (args[argidx] == "-vv") {
-				try_mode = true;
+				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;
  

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::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
-	std::map<int, std::vector<std::string>> sets_def_at, sets_undef_at, sets_all_undef_at;
+	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))
+				if (!RTLIL::SigSpec::parse(lhs, module, s.first))
-				log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
+					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))
+				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());
+					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(lhs));
-			show_signal_pool.add(sigmap(rhs));
+				show_signal_pool.add(sigmap(rhs));
 
-			if (lhs.width != rhs.width)
+				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",
+					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);
+						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));
+				log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
-			big_lhs.remove2(lhs, &big_rhs);
+				big_lhs.remove2(lhs, &big_rhs);
-			big_lhs.append(lhs);
+				big_lhs.append(lhs);
-			big_rhs.append(rhs);
+				big_rhs.append(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));
 		}
 
-		log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+		if (prove_x.size() > 0)
-		check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+		{
-		return satgen.signals_eq(big_lhs, big_rhs, timestep);
+			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("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))))));
+		}
+
+		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-at <N> <signal>\n");
-		log("    -set-def <N> <signal>\n");
+		log("    -set-any-undef-at <N> <signal>\n");
-		log("    -set-undef <N> <signal>\n");
+		log("    -set-all-undef-at <N> <signal>\n");
-		log("    -set-all-undef <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::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_undef, sets_all_undef;
+		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 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 = true;
+		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()) {
+			if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
-				sets_undef.push_back(args[++argidx]);
+				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");

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;
+		// try to implement as many cells as possible just by inverting
-		while (keep_running) {
+		// the SET and RESET pins. If necessary, implement cell types
-			keep_running = false;
+		// by inverting both D and Q. Only invert clock pins if there
-			keep_running |= expand_cellmap("$_DFF_*_", "C");
+		// is no other way of implementing the cell.
-			keep_running |= expand_cellmap("$_DFF_*??_", "C");
+		while (1)
-			keep_running |= expand_cellmap("$_DFF_?*?_", "R");
+		{
-			keep_running |= expand_cellmap("$_DFF_??*_", "DQ");
+			if (expand_cellmap("$_DFF_?*?_", "R") ||
-			keep_running |= expand_cellmap("$_DFFSR_*??_", "C");
+					expand_cellmap("$_DFFSR_?*?_", "S") ||
-			keep_running |= expand_cellmap("$_DFFSR_?*?_", "S");
+					expand_cellmap("$_DFFSR_??*_", "R"))
-			keep_running |= 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_");

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");

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;

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) );
+\$_AND_ gate1 ( .A(A),  .B(B),  .Y(t1) );
- \$_XOR_ gate2 ( .A(A),  .B(B),  .Y(t2) );
+\$_XOR_ gate2 ( .A(A),  .B(B),  .Y(t2) );
- \$_AND_ gate3 ( .A(t2), .B(C),  .Y(t3) ); 
+\$_AND_ gate3 ( .A(t2), .B(C),  .Y(t3) ); 
- \$_XOR_ gate4 ( .A(t2), .B(C),  .Y(Y)  );
+\$_XOR_ gate4 ( .A(t2), .B(C),  .Y(Y)  );
- \$_OR_  gate5 ( .A(t1), .B(t3), .Y(X)  );
+\$_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), .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(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), .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(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));
+\$bu0 #(.A_SIGNED(A_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(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,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;
@@ -563,8 +568,58 @@ 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));
+\$bu0 #(.A_SIGNED(A_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(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;
+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);
 
@@ -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), .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(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), .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(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), .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(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), .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(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 A_buf_u = A_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 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
 
 /****

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

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;

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

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

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; opt; memory; opt; fsm; opt"
-			test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap; opt"
+			test_passes -p "hierarchy; proc; opt; memory; opt; fsm; opt; techmap; opt; abc -dff; opt"
-			# test_passes -p "hierarchy; proc; memory; opt; fsm; opt; techmap -opt; opt; abc; opt"
 		fi
 		touch ../${bn}.log
 	}