New upstream version 0.7+20181007git9850de4

8 files changed, 97 insertions, 16 deletions

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 0f7e910f..c9345ff0 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -985,7 +985,8 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 
 		use_const_chunk:
 			if (children.size() != 0) {
-				log_assert(children[0]->type == AST_RANGE);
+				if (children[0]->type != AST_RANGE)
+					log_file_error(filename, linenum, "Single range expected.\n");
 				int source_width = id2ast->range_left - id2ast->range_right + 1;
 				int source_offset = id2ast->range_right;
 				if (!children[0]->range_valid) {
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 04c429f7..71eba547 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1781,7 +1781,7 @@ skip_dynamic_range_lvalue_expansion:;
 				if (GetSize(children) == 2)
 				{
 					AstNode *buf = children[1]->clone();
-					while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { }
+					while (buf->simplify(true, false, false, stage, -1, false, false)) { }
 					if (buf->type != AST_CONSTANT)
 						log_file_error(filename, linenum, "Failed to evaluate system function `%s' with non-constant value.\n", str.c_str());
 
@@ -1836,7 +1836,7 @@ skip_dynamic_range_lvalue_expansion:;
 				goto apply_newNode;
 			}
 
-			if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell")
+			if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell" || str == "\\$changed")
 			{
 				if (GetSize(children) != 1)
 					log_file_error(filename, linenum, "System function %s got %d arguments, expected 1.\n",
@@ -1853,6 +1853,9 @@ skip_dynamic_range_lvalue_expansion:;
 				if (str == "\\$stable")
 					newNode = new AstNode(AST_EQ, past, present);
 
+				else if (str == "\\$changed")
+					newNode = new AstNode(AST_NE, past, present);
+
 				else if (str == "\\$rose")
 					newNode = new AstNode(AST_LOGIC_AND, new AstNode(AST_LOGIC_NOT, past), present);
 
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 1dd6d7e2..dba3b0f0 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -64,6 +64,7 @@ YOSYS_NAMESPACE_BEGIN
 int verific_verbose;
 bool verific_import_pending;
 string verific_error_msg;
+int verific_sva_fsm_limit;
 
 vector<string> verific_incdirs, verific_libdirs;
 
@@ -117,6 +118,18 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
 	return net_map.at(net);
 }
 
+bool is_blackbox(Netlist *nl)
+{
+	if (nl->IsBlackBox())
+		return true;
+
+	const char *attr = nl->GetAttValue("blackbox");
+	if (attr != nullptr && strcmp(attr, "0"))
+		return true;
+
+	return false;
+}
+
 void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
 {
 	MapIter mi;
@@ -708,7 +721,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	netlist = nl;
 
 	if (design->has(module_name)) {
-		if (!nl->IsOperator())
+		if (!nl->IsOperator() && !is_blackbox(nl))
 			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
 		return;
 	}
@@ -717,7 +730,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	module->name = module_name;
 	design->add(module);
 
-	if (nl->IsBlackBox()) {
+	if (is_blackbox(nl)) {
 		log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
 		module->set_bool_attribute("\\blackbox");
 	} else {
@@ -1618,6 +1631,8 @@ struct VerificExtNets
 
 void verific_import(Design *design, std::string top)
 {
+	verific_sva_fsm_limit = 16;
+
 	std::set<Netlist*> nl_todo, nl_done;
 
 	{
@@ -1673,6 +1688,7 @@ YOSYS_NAMESPACE_END
 
 PRIVATE_NAMESPACE_BEGIN
 
+#ifdef YOSYS_ENABLE_VERIFIC
 bool check_noverific_env()
 {
 	const char *e = getenv("YOSYS_NOVERIFIC");
@@ -1682,6 +1698,7 @@ bool check_noverific_env()
 		return false;
 	return true;
 }
+#endif
 
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
@@ -1789,6 +1806,9 @@ struct VerificPass : public Pass {
 		log("  -nosva\n");
 		log("    Ignore SVA properties, do not infer checker logic.\n");
 		log("\n");
+		log("  -L <int>\n");
+		log("    Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
+		log("\n");
 		log("  -n\n");
 		log("    Keep all Verific names on instances and nets. By default only\n");
 		log("    user-declared names are preserved.\n");
@@ -1830,6 +1850,7 @@ struct VerificPass : public Pass {
 		}
 
 		verific_verbose = 0;
+		verific_sva_fsm_limit = 16;
 
 		const char *release_str = Message::ReleaseString();
 		time_t release_time = Message::ReleaseDate();
@@ -2036,6 +2057,10 @@ struct VerificPass : public Pass {
 					mode_nosva = true;
 					continue;
 				}
+				if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
+					verific_sva_fsm_limit = atoi(args[++argidx].c_str());
+					continue;
+				}
 				if (args[argidx] == "-n") {
 					mode_names = true;
 					continue;
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index cbd9314d..334a436a 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -101,6 +101,8 @@ void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst
 void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
 bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net);
 
+extern int verific_sva_fsm_limit;
+
 YOSYS_NAMESPACE_END
 
 #endif
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 85b84218..cdc9ece8 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -466,13 +466,14 @@ struct SvaFsm
 
 		dnode.ctrl.sort_and_unify();
 
-		if (GetSize(dnode.ctrl) > 16) {
+		if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
 			if (verific_verbose >= 2) {
 				log("    detected state explosion in DFSM generation:\n");
 				dump();
 				log("      ctrl signal: %s\n", log_signal(dnode.ctrl));
 			}
-			log_error("SVA DFSM state ctrl signal has %d (>16) bits. Stopping to prevent exponential design size explosion.\n", GetSize(dnode.ctrl));
+			log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
+					GetSize(dnode.ctrl), verific_sva_fsm_limit);
 		}
 
 		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 8dcc7c5a..aeea36a2 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -66,12 +66,21 @@ struct VerilogFrontend : public Frontend {
 		log("        enable support for SystemVerilog assertions and some Yosys extensions\n");
 		log("        replace the implicit -D SYNTHESIS with -D FORMAL\n");
 		log("\n");
+		log("    -noassert\n");
+		log("        ignore assert() statements\n");
+		log("\n");
+		log("    -noassume\n");
+		log("        ignore assume() statements\n");
+		log("\n");
 		log("    -norestrict\n");
-		log("        ignore restrict() assertions\n");
+		log("        ignore restrict() statements\n");
 		log("\n");
 		log("    -assume-asserts\n");
 		log("        treat all assert() statements like assume() statements\n");
 		log("\n");
+		log("    -assert-assumes\n");
+		log("        treat all assume() statements like assert() statements\n");
+		log("\n");
 		log("    -dump_ast1\n");
 		log("        dump abstract syntax tree (before simplification)\n");
 		log("\n");
@@ -229,6 +238,14 @@ struct VerilogFrontend : public Frontend {
 				formal_mode = true;
 				continue;
 			}
+			if (arg == "-noassert") {
+				noassert_mode = true;
+				continue;
+			}
+			if (arg == "-noassume") {
+				noassume_mode = true;
+				continue;
+			}
 			if (arg == "-norestrict") {
 				norestrict_mode = true;
 				continue;
@@ -237,6 +254,10 @@ struct VerilogFrontend : public Frontend {
 				assume_asserts_mode = true;
 				continue;
 			}
+			if (arg == "-assert-assumes") {
+				assert_assumes_mode = true;
+				continue;
+			}
 			if (arg == "-dump_ast1") {
 				flag_dump_ast1 = true;
 				continue;
diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index 16edc798..523bbc89 100644
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -54,12 +54,21 @@ namespace VERILOG_FRONTEND
 	// running in -formal mode
 	extern bool formal_mode;
 
+	// running in -noassert mode
+	extern bool noassert_mode;
+
+	// running in -noassume mode
+	extern bool noassume_mode;
+
 	// running in -norestrict mode
 	extern bool norestrict_mode;
 
 	// running in -assume-asserts mode
 	extern bool assume_asserts_mode;
 
+	// running in -assert-assumes mode
+	extern bool assert_assumes_mode;
+
 	// running in -lib mode
 	extern bool lib_mode;
 
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 2389d7d3..16cac146 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -58,7 +58,8 @@ namespace VERILOG_FRONTEND {
 	bool do_not_require_port_stubs;
 	bool default_nettype_wire;
 	bool sv_mode, formal_mode, lib_mode;
-	bool norestrict_mode, assume_asserts_mode;
+	bool noassert_mode, noassume_mode, norestrict_mode;
+	bool assume_asserts_mode, assert_assumes_mode;
 	bool current_wire_rand, current_wire_const;
 	std::istream *lexin;
 }
@@ -881,9 +882,15 @@ param_decl_list:
 
 single_param_decl:
 	TOK_ID '=' expr {
-		if (astbuf1 == nullptr)
-			frontend_verilog_yyerror("syntax error");
-		AstNode *node = astbuf1->clone();
+		AstNode *node;
+		if (astbuf1 == nullptr) {
+			if (!sv_mode)
+				frontend_verilog_yyerror("syntax error");
+			node = new AstNode(AST_PARAMETER);
+			node->children.push_back(AstNode::mkconst_int(0, true));
+		} else {
+			node = astbuf1->clone();
+		}
 		node->str = *$1;
 		delete node->children[0];
 		node->children[0] = $3;
@@ -1275,16 +1282,28 @@ opt_stmt_label:
 
 assert:
 	opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+		if (noassert_mode)
+			delete $5;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
 	} |
 	opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
+		if (noassume_mode)
+			delete $5;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
 	} |
 	opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+		if (noassert_mode)
+			delete $6;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
 	} |
 	opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
+		if (noassume_mode)
+			delete $6;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
 	} |
 	opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));