Merge https://github.com/YosysHQ/yosys into read_aiger

8 files changed, 348 insertions, 110 deletions

diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index 08f91c9c3..8b185ff51 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -214,6 +214,8 @@ namespace AST
 			MEM2REG_FL_SET_ASYNC = 0x00000800,
 			MEM2REG_FL_EQ2       = 0x00001000,
 			MEM2REG_FL_CMPLX_LHS = 0x00002000,
+			MEM2REG_FL_CONST_LHS = 0x00004000,
+			MEM2REG_FL_VAR_LHS   = 0x00008000,
 
 			/* proc flags */
 			MEM2REG_FL_EQ1       = 0x01000000,
@@ -237,6 +239,7 @@ namespace AST
 		bool has_const_only_constructs(bool &recommend_const_eval);
 		void replace_variables(std::map<std::string, varinfo_t> &variables, AstNode *fcall);
 		AstNode *eval_const_function(AstNode *fcall);
+		bool is_simple_const_expr();
 
 		// create a human-readable text representation of the AST (for debugging)
 		void dumpAst(FILE *f, std::string indent) const;
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index e66625228..b3a2a84be 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -525,7 +525,16 @@ struct AST_INTERNAL::ProcessGenerator
 				}
 
 				if (last_generated_case != NULL && ast->get_bool_attribute("\\full_case") && default_case == NULL) {
+			#if 0
+					// this is a valid transformation, but as optimization it is premature.
+					// better: add a default case that assigns 'x' to everything, and let later
+					// optimizations take care of the rest
 					last_generated_case->compare.clear();
+			#else
+					default_case = new RTLIL::CaseRule;
+					addChunkActions(default_case->actions, this_case_eq_ltemp, SigSpec(State::Sx, GetSize(this_case_eq_rvalue)));
+					sw->cases.push_back(default_case);
+			#endif
 				} else {
 					if (default_case == NULL) {
 						default_case = new RTLIL::CaseRule;
@@ -544,7 +553,11 @@ struct AST_INTERNAL::ProcessGenerator
 			break;
 
 		case AST_WIRE:
-			log_file_error(ast->filename, ast->linenum, "Found wire declaration in block without label!\n");
+			log_file_error(ast->filename, ast->linenum, "Found reg declaration in block without label!\n");
+			break;
+
+		case AST_ASSIGN:
+			log_file_error(ast->filename, ast->linenum, "Found continous assignment in always/initial block!\n");
 			break;
 
 		case AST_PARAMETER:
@@ -644,7 +657,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
 				while (right_at_zero_ast->simplify(true, true, false, 1, -1, false, false)) { }
 				if (left_at_zero_ast->type != AST_CONSTANT || right_at_zero_ast->type != AST_CONSTANT)
 					log_file_error(filename, linenum, "Unsupported expression on dynamic range select on signal `%s'!\n", str.c_str());
-				this_width = left_at_zero_ast->integer - right_at_zero_ast->integer + 1;
+				this_width = abs(int(left_at_zero_ast->integer - right_at_zero_ast->integer)) + 1;
 				delete left_at_zero_ast;
 				delete right_at_zero_ast;
 			} else
@@ -792,7 +805,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
 	// everything should have been handled above -> print error if not.
 	default:
 		for (auto f : log_files)
-			current_ast->dumpAst(f, "verilog-ast> ");
+			current_ast_mod->dumpAst(f, "verilog-ast> ");
 		log_file_error(filename, linenum, "Don't know how to detect sign and width for %s node!\n", type2str(type).c_str());
 	}
 
@@ -1034,7 +1047,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 					while (right_at_zero_ast->simplify(true, true, false, 1, -1, false, false)) { }
 					if (left_at_zero_ast->type != AST_CONSTANT || right_at_zero_ast->type != AST_CONSTANT)
 						log_file_error(filename, linenum, "Unsupported expression on dynamic range select on signal `%s'!\n", str.c_str());
-					int width = left_at_zero_ast->integer - right_at_zero_ast->integer + 1;
+					int width = abs(int(left_at_zero_ast->integer - right_at_zero_ast->integer)) + 1;
 					AstNode *fake_ast = new AstNode(AST_NONE, clone(), children[0]->children.size() >= 2 ?
 							children[0]->children[1]->clone() : children[0]->children[0]->clone());
 					fake_ast->children[0]->delete_children();
@@ -1409,10 +1422,16 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 			if (GetSize(en) != 1)
 				en = current_module->ReduceBool(NEW_ID, en);
 
-			std::stringstream sstr;
-			sstr << celltype << "$" << filename << ":" << linenum << "$" << (autoidx++);
+			IdString cellname;
+			if (str.empty()) {
+				std::stringstream sstr;
+				sstr << celltype << "$" << filename << ":" << linenum << "$" << (autoidx++);
+				cellname = sstr.str();
+			} else {
+				cellname = str;
+			}
 
-			RTLIL::Cell *cell = current_module->addCell(sstr.str(), celltype);
+			RTLIL::Cell *cell = current_module->addCell(cellname, celltype);
 			cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
 
 			for (auto &attr : attributes) {
@@ -1565,7 +1584,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 	// everything should have been handled above -> print error if not.
 	default:
 		for (auto f : log_files)
-			current_ast->dumpAst(f, "verilog-ast> ");
+			current_ast_mod->dumpAst(f, "verilog-ast> ");
 		type_name = type2str(type);
 		log_file_error(filename, linenum, "Don't know how to generate RTLIL code for %s node!\n", type_name.c_str());
 	}
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 83714f897..d525c6b8a 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -50,7 +50,6 @@ using namespace AST_INTERNAL;
 bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, int width_hint, bool sign_hint, bool in_param)
 {
 	static int recursion_counter = 0;
-	static pair<string, int> last_blocking_assignment_warn;
 	static bool deep_recursion_warning = false;
 
 	if (recursion_counter++ == 1000 && deep_recursion_warning) {
@@ -72,7 +71,6 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	if (stage == 0)
 	{
 		log_assert(type == AST_MODULE || type == AST_INTERFACE);
-		last_blocking_assignment_warn = pair<string, int>();
 
 		deep_recursion_warning = true;
 		while (simplify(const_fold, at_zero, in_lvalue, 1, width_hint, sign_hint, in_param)) { }
@@ -113,6 +111,9 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 				if (memflags & AstNode::MEM2REG_FL_CMPLX_LHS)
 					goto verbose_activate;
 
+				if ((memflags & AstNode::MEM2REG_FL_CONST_LHS) && !(memflags & AstNode::MEM2REG_FL_VAR_LHS))
+					goto verbose_activate;
+
 				// log("Note: Not replacing memory %s with list of registers (flags=0x%08lx).\n", mem->str.c_str(), long(memflags));
 				continue;
 
@@ -325,6 +326,15 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		for (size_t i = 0; i < children.size(); i++) {
 			AstNode *node = children[i];
 			if (node->type == AST_WIRE) {
+				if (node->children.size() == 1 && node->children[0]->type == AST_RANGE) {
+					for (auto c : node->children[0]->children) {
+						if (!c->is_simple_const_expr()) {
+							if (attributes.count("\\dynports"))
+								delete attributes.at("\\dynports");
+							attributes["\\dynports"] = AstNode::mkconst_int(1, true);
+						}
+					}
+				}
 				if (this_wire_scope.count(node->str) > 0) {
 					AstNode *first_node = this_wire_scope[node->str];
 					if (first_node->is_input && node->is_reg)
@@ -642,6 +652,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	// (iterate by index as e.g. auto wires can add new children in the process)
 	for (size_t i = 0; i < children.size(); i++) {
 		bool did_something_here = true;
+		bool backup_flag_autowire = flag_autowire;
 		if ((type == AST_GENFOR || type == AST_FOR) && i >= 3)
 			break;
 		if ((type == AST_GENIF || type == AST_GENCASE) && i >= 1)
@@ -652,6 +663,8 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 			break;
 		if (type == AST_PREFIX && i >= 1)
 			break;
+		if (type == AST_DEFPARAM && i == 0)
+			flag_autowire = true;
 		while (did_something_here && i < children.size()) {
 			bool const_fold_here = const_fold, in_lvalue_here = in_lvalue;
 			int width_hint_here = width_hint;
@@ -686,6 +699,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 			children.erase(children.begin() + (i--));
 			did_something = true;
 		}
+		flag_autowire = backup_flag_autowire;
 	}
 	for (auto &attr : attributes) {
 		while (attr.second->simplify(true, false, false, stage, -1, false, true))
@@ -934,12 +948,15 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 			}
 		}
 		if (current_scope.count(str) == 0) {
-			// log_warning("Creating auto-wire `%s' in module `%s'.\n", str.c_str(), current_ast_mod->str.c_str());
-			AstNode *auto_wire = new AstNode(AST_AUTOWIRE);
-			auto_wire->str = str;
-			current_ast_mod->children.push_back(auto_wire);
-			current_scope[str] = auto_wire;
-			did_something = true;
+			if (flag_autowire || str == "\\$global_clock") {
+				AstNode *auto_wire = new AstNode(AST_AUTOWIRE);
+				auto_wire->str = str;
+				current_ast_mod->children.push_back(auto_wire);
+				current_scope[str] = auto_wire;
+				did_something = true;
+			} else {
+				log_file_error(filename, linenum, "Identifier `%s' is implicitly declared and `default_nettype is set to none.\n", str.c_str());
+			}
 		}
 		if (id2ast != current_scope[str]) {
 			id2ast = current_scope[str];
@@ -1492,6 +1509,7 @@ skip_dynamic_range_lvalue_expansion:;
 		newNode->children.push_back(assign_en);
 
 		AstNode *assertnode = new AstNode(type);
+		assertnode->str = str;
 		assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
 		assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
 		assertnode->children[0]->str = id_check;
@@ -1572,14 +1590,6 @@ skip_dynamic_range_lvalue_expansion:;
 		sstr << "$memwr$" << children[0]->str << "$" << filename << ":" << linenum << "$" << (autoidx++);
 		std::string id_addr = sstr.str() + "_ADDR", id_data = sstr.str() + "_DATA", id_en = sstr.str() + "_EN";
 
-		if (type == AST_ASSIGN_EQ) {
-			pair<string, int> this_blocking_assignment_warn(filename, linenum);
-			if (this_blocking_assignment_warn != last_blocking_assignment_warn)
-				log_warning("Blocking assignment to memory in line %s:%d is handled like a non-blocking assignment.\n",
-						filename.c_str(), linenum);
-			last_blocking_assignment_warn = this_blocking_assignment_warn;
-		}
-
 		int mem_width, mem_size, addr_bits;
 		bool mem_signed = children[0]->id2ast->is_signed;
 		children[0]->id2ast->meminfo(mem_width, mem_size, addr_bits);
@@ -1689,7 +1699,7 @@ skip_dynamic_range_lvalue_expansion:;
 				while (right_at_zero_ast->simplify(true, true, false, 1, -1, false, false)) { }
 				if (left_at_zero_ast->type != AST_CONSTANT || right_at_zero_ast->type != AST_CONSTANT)
 					log_file_error(filename, linenum, "Unsupported expression on dynamic range select on signal `%s'!\n", str.c_str());
-				int width = left_at_zero_ast->integer - right_at_zero_ast->integer + 1;
+				int width = abs(int(left_at_zero_ast->integer - right_at_zero_ast->integer)) + 1;
 
 				assign_data = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER),
 						new AstNode(AST_SHIFT_LEFT, children[1]->clone(), offset_ast->clone()));
@@ -1778,7 +1788,7 @@ skip_dynamic_range_lvalue_expansion:;
 
 			if (str == "\\$past")
 			{
-				if (width_hint <= 0)
+				if (width_hint < 0)
 					goto replace_fcall_later;
 
 				int num_steps = 1;
@@ -2162,6 +2172,8 @@ skip_dynamic_range_lvalue_expansion:;
 				}
 
 				newNode = readmem(str == "\\$readmemh", node_filename->bitsAsConst().decode_string(), node_memory->id2ast, start_addr, finish_addr, unconditional_init);
+				delete node_filename;
+				delete node_memory;
 				goto apply_newNode;
 			}
 
@@ -2203,6 +2215,8 @@ skip_dynamic_range_lvalue_expansion:;
 		std::map<std::string, std::string> replace_rules;
 		vector<AstNode*> added_mod_children;
 		dict<std::string, AstNode*> wire_cache;
+		vector<AstNode*> new_stmts;
+		vector<AstNode*> output_assignments;
 
 		if (current_block == NULL)
 		{
@@ -2327,8 +2341,8 @@ skip_dynamic_range_lvalue_expansion:;
 					wire->port_id = 0;
 					wire->is_input = false;
 					wire->is_output = false;
-					if (!child->is_output)
-						wire->attributes["\\nosync"] = AstNode::mkconst_int(1, false);
+					wire->is_reg = true;
+					wire->attributes["\\nosync"] = AstNode::mkconst_int(1, false);
 					wire_cache[child->str] = wire;
 
 					current_ast_mod->children.push_back(wire);
@@ -2350,13 +2364,10 @@ skip_dynamic_range_lvalue_expansion:;
 							new AstNode(AST_ASSIGN_EQ, wire_id, arg) :
 							new AstNode(AST_ASSIGN_EQ, arg, wire_id);
 					assign->children[0]->was_checked = true;
-
-					for (auto it = current_block->children.begin(); it != current_block->children.end(); it++) {
-						if (*it != current_block_child)
-							continue;
-						current_block->children.insert(it, assign);
-						break;
-					}
+					if (child->is_input)
+						new_stmts.push_back(assign);
+					else
+						output_assignments.push_back(assign);
 				}
 			}
 
@@ -2370,14 +2381,18 @@ skip_dynamic_range_lvalue_expansion:;
 			{
 				AstNode *stmt = child->clone();
 				stmt->replace_ids(prefix, replace_rules);
+				new_stmts.push_back(stmt);
+			}
 
-				for (auto it = current_block->children.begin(); it != current_block->children.end(); it++) {
-					if (*it != current_block_child)
-						continue;
-					current_block->children.insert(it, stmt);
-					break;
-				}
+		new_stmts.insert(new_stmts.end(), output_assignments.begin(), output_assignments.end());
+
+		for (auto it = current_block->children.begin(); ; it++) {
+			log_assert(it != current_block->children.end());
+			if (*it == current_block_child) {
+				current_block->children.insert(it, new_stmts.begin(), new_stmts.end());
+				break;
 			}
+		}
 
 	replace_fcall_with_id:
 		if (type == AST_FCALL) {
@@ -2848,7 +2863,11 @@ void AstNode::expand_genblock(std::string index_var, std::string prefix, std::ma
 
 	for (size_t i = 0; i < children.size(); i++) {
 		AstNode *child = children[i];
-		if (child->type != AST_FUNCTION && child->type != AST_TASK && child->type != AST_PREFIX)
+		// AST_PREFIX member names should not be prefixed; a nested AST_PREFIX
+		// still needs to recursed-into
+		if (type == AST_PREFIX && i == 1 && child->type == AST_IDENTIFIER)
+			continue;
+		if (child->type != AST_FUNCTION && child->type != AST_TASK)
 			child->expand_genblock(index_var, prefix, name_map);
 	}
 
@@ -2903,7 +2922,7 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg
 		dict<AstNode*, uint32_t> &mem2reg_candidates, dict<AstNode*, uint32_t> &proc_flags, uint32_t &flags)
 {
 	uint32_t children_flags = 0;
-	int ignore_children_counter = 0;
+	int lhs_children_counter = 0;
 
 	if (type == AST_ASSIGN || type == AST_ASSIGN_LE || type == AST_ASSIGN_EQ)
 	{
@@ -2929,6 +2948,16 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg
 				proc_flags[mem] |= AstNode::MEM2REG_FL_EQ1;
 			}
 
+			// for proper (non-init) writes: remember if this is a constant index or not
+			if ((flags & MEM2REG_FL_INIT) == 0) {
+				if (children[0]->children.size() && children[0]->children[0]->type == AST_RANGE && children[0]->children[0]->children.size()) {
+					if (children[0]->children[0]->children[0]->type == AST_CONSTANT)
+						mem2reg_candidates[mem] |= AstNode::MEM2REG_FL_CONST_LHS;
+					else
+						mem2reg_candidates[mem] |= AstNode::MEM2REG_FL_VAR_LHS;
+				}
+			}
+
 			// remember where this is
 			if (flags & MEM2REG_FL_INIT) {
 				if (!(mem2reg_candidates[mem] & AstNode::MEM2REG_FL_SET_INIT))
@@ -2941,7 +2970,7 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg
 			}
 		}
 
-		ignore_children_counter = 1;
+		lhs_children_counter = 1;
 	}
 
 	if (type == AST_IDENTIFIER && id2ast && id2ast->type == AST_MEMORY)
@@ -2984,12 +3013,23 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg
 	log_assert((flags & ~0x000000ff) == 0);
 
 	for (auto child : children)
-		if (ignore_children_counter > 0)
-			ignore_children_counter--;
-		else if (proc_flags_p)
+	{
+		if (lhs_children_counter > 0) {
+			lhs_children_counter--;
+			if (child->children.size() && child->children[0]->type == AST_RANGE && child->children[0]->children.size()) {
+				for (auto c : child->children[0]->children) {
+					if (proc_flags_p)
+						c->mem2reg_as_needed_pass1(mem2reg_places, mem2reg_candidates, *proc_flags_p, flags);
+					else
+						c->mem2reg_as_needed_pass1(mem2reg_places, mem2reg_candidates, proc_flags, flags);
+				}
+			}
+		} else
+		if (proc_flags_p)
 			child->mem2reg_as_needed_pass1(mem2reg_places, mem2reg_candidates, *proc_flags_p, flags);
 		else
 			child->mem2reg_as_needed_pass1(mem2reg_places, mem2reg_candidates, proc_flags, flags);
+	}
 
 	flags &= ~children_flags | backup_flags;
 
@@ -3041,6 +3081,39 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
 	if (type == AST_FUNCTION || type == AST_TASK)
 		return false;
 
+	if (type == AST_MEMINIT && id2ast && mem2reg_set.count(id2ast))
+	{
+		log_assert(children[0]->type == AST_CONSTANT);
+		log_assert(children[1]->type == AST_CONSTANT);
+		log_assert(children[2]->type == AST_CONSTANT);
+
+		int cursor = children[0]->asInt(false);
+		Const data = children[1]->bitsAsConst();
+		int length = children[2]->asInt(false);
+
+		if (length != 0)
+		{
+			AstNode *block = new AstNode(AST_INITIAL, new AstNode(AST_BLOCK));
+			mod->children.push_back(block);
+			block = block->children[0];
+
+			int wordsz = GetSize(data) / length;
+
+			for (int i = 0; i < length; i++) {
+				block->children.push_back(new AstNode(AST_ASSIGN_EQ, new AstNode(AST_IDENTIFIER, new AstNode(AST_RANGE, AstNode::mkconst_int(cursor+i, false))), mkconst_bits(data.extract(i*wordsz, wordsz).bits, false)));
+				block->children.back()->children[0]->str = str;
+				block->children.back()->children[0]->id2ast = id2ast;
+				block->children.back()->children[0]->was_checked = true;
+			}
+		}
+
+		AstNode *newNode = new AstNode(AST_NONE);
+		newNode->cloneInto(this);
+		delete newNode;
+
+		did_something = true;
+	}
+
 	if (type == AST_ASSIGN && block == NULL && children[0]->mem2reg_check(mem2reg_set))
 	{
 		if (async_block == NULL) {
@@ -3270,6 +3343,16 @@ bool AstNode::has_const_only_constructs(bool &recommend_const_eval)
 	return false;
 }
 
+bool AstNode::is_simple_const_expr()
+{
+	if (type == AST_IDENTIFIER)
+		return false;
+	for (auto child : children)
+		if (!child->is_simple_const_expr())
+			return false;
+	return true;
+}
+
 // helper function for AstNode::eval_const_function()
 void AstNode::replace_variables(std::map<std::string, AstNode::varinfo_t> &variables, AstNode *fcall)
 {
diff --git a/frontends/verific/README b/frontends/verific/README
index c76cdd637..89584f2e8 100644
--- a/frontends/verific/README
+++ b/frontends/verific/README
@@ -21,7 +21,7 @@ Then run in the following command in this directory:
 
 	sby -f example.sby
 
-This will generate approximately one page of text outpout. The last lines
+This will generate approximately one page of text output. The last lines
 should be something like this:
 
 	SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 94138cdd6..c412cd3a3 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1855,6 +1855,13 @@ struct VerificPass : public Pass {
 		log("  -autocover\n");
 		log("    Generate automatic cover statements for all asserts\n");
 		log("\n");
+		log("  -chparam name value \n");
+		log("    Elaborate the specified top modules (all modules when -all given) using\n");
+		log("    this parameter value. Modules on which this parameter does not exist will\n");
+		log("    cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
+		log("    can be specified multiple times to override multiple parameters.\n");
+		log("    String values must be passed in double quotes (\").\n");
+		log("\n");
 		log("  -v, -vv\n");
 		log("    Verbose log messages. (-vv is even more verbose than -v.)\n");
 		log("\n");
@@ -1920,6 +1927,10 @@ struct VerificPass : public Pass {
 			// WARNING: instantiating unknown module 'XYZ' (VERI-1063)
 			Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
 
+#ifndef DB_PRESERVE_INITIAL_VALUE
+#  warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
+#endif
+
 			set_verific_global_flags = false;
 		}
 
@@ -2105,6 +2116,7 @@ struct VerificPass : public Pass {
 			bool mode_autocover = false;
 			bool flatten = false, extnets = false;
 			string dumpfile;
+			Map parameters(STRING_HASH);
 
 			for (argidx++; argidx < GetSize(args); argidx++) {
 				if (args[argidx] == "-all") {
@@ -2143,6 +2155,15 @@ struct VerificPass : public Pass {
 					mode_autocover = true;
 					continue;
 				}
+				if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
+                                        const std::string &key = args[++argidx];
+                                        const std::string &value = args[++argidx];
+					unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
+									           1 /* force_overwrite */);
+					if (!new_insertion)
+						log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
+					continue;
+				}
 				if (args[argidx] == "-V") {
 					mode_verific = true;
 					continue;
@@ -2176,7 +2197,7 @@ struct VerificPass : public Pass {
 				if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
 				if (veri_lib) veri_libs.InsertLast(veri_lib);
 
-				Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+				Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
 				Netlist *nl;
 				int i;
 
@@ -2213,7 +2234,7 @@ struct VerificPass : public Pass {
 				}
 
 				log("Running hier_tree::Elaborate().\n");
-				Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units);
+				Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
 				Netlist *nl;
 				int i;
 
@@ -2312,7 +2333,7 @@ struct ReadPass : public Pass {
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		if (args.size() < 2)
+		if (args.size() < 2 || args[1][0] != '-')
 			log_cmd_error("Missing mode parameter.\n");
 
 		if (args.size() < 3)
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 6681115df..8ea8372d3 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1666,7 +1666,20 @@ struct VerificSvaImporter
 				log("  importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
 						LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
 
-			RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+			bool is_user_declared = root->IsUserDeclared();
+
+			// FIXME
+			if (!is_user_declared) {
+				const char *name = root->Name();
+				for (int i = 0; name[i]; i++) {
+					if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
+						is_user_declared = true;
+						break;
+					}
+				}
+			}
+
+			RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
 
 			// parse SVA sequence into trigger signal
 
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 1b1873e24..6ef38252a 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -189,6 +189,14 @@ YOSYS_NAMESPACE_END
 "always_ff"    { SV_KEYWORD(TOK_ALWAYS); }
 "always_latch" { SV_KEYWORD(TOK_ALWAYS); }
 
+ /* use special token for labels on assert, assume, cover, and restrict because it's insanley complex
+    to fix parsing of cells otherwise. (the current cell parser forces a reduce very early to update some
+    global state.. its a mess) */
+[a-zA-Z_$][a-zA-Z0-9_$]*/[ \t\r\n]*:[ \t\r\n]*(assert|assume|cover|restrict)[^a-zA-Z0-9_$\.] {
+	frontend_verilog_yylval.string = new std::string(std::string("\\") + yytext);
+	return TOK_SVA_LABEL;
+}
+
 "assert"     { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
 "assume"     { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
 "cover"      { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
@@ -303,7 +311,7 @@ supply1 { return TOK_SUPPLY1; }
 
 [a-zA-Z_$][a-zA-Z0-9_$\.]* {
 	frontend_verilog_yylval.string = new std::string(std::string("\\") + yytext);
-    return TOK_ID;
+	return TOK_ID;
 }
 
 "/*"[ \t]*(synopsys|synthesis)[ \t]*translate_off[ \t]*"*/" {
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index a6718b020..52685f637 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -105,7 +105,8 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 	bool boolean;
 }
 
-%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
+%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE TOK_SVA_LABEL
+%token TOK_ASSERT TOK_ASSUME TOK_RESTRICT TOK_COVER
 %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END
 %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM
 %token TOK_PACKAGE TOK_ENDPACKAGE TOK_PACKAGESEP
@@ -119,14 +120,13 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_GENERATE TOK_ENDGENERATE TOK_GENVAR TOK_REAL
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
-%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
+%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
 %token TOK_RAND TOK_CONST TOK_CHECKER TOK_ENDCHECKER TOK_EVENTUALLY
 %token TOK_INCREMENT TOK_DECREMENT TOK_UNIQUE TOK_PRIORITY
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
-%type <string> opt_label tok_prim_wrapper hierarchical_id
+%type <string> opt_label opt_sva_label tok_prim_wrapper hierarchical_id
 %type <boolean> opt_signed opt_property unique_case_attr
 %type <al> attr case_attr
 
@@ -1329,6 +1329,14 @@ opt_label:
 		$$ = NULL;
 	};
 
+opt_sva_label:
+	TOK_SVA_LABEL ':' {
+		$$ = $1;
+	} |
+	/* empty */ {
+		$$ = NULL;
+	};
+
 opt_property:
 	TOK_PROPERTY {
 		$$ = true;
@@ -1337,9 +1345,6 @@ opt_property:
 		$$ = false;
 	};
 
-opt_stmt_label:
-	TOK_ID ':' | /* empty */;
-
 modport_stmt:
     TOK_MODPORT TOK_ID {
         AstNode *modport = new AstNode(AST_MODPORT);
@@ -1376,83 +1381,164 @@ modport_type_token:
     TOK_INPUT {current_modport_input = 1; current_modport_output = 0;} | TOK_OUTPUT {current_modport_input = 0; current_modport_output = 1;}
 
 assert:
-	opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
-		if (noassert_mode)
+	opt_sva_label TOK_ASSERT opt_property '(' expr ')' ';' {
+		if (noassert_mode) {
 			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+		} else {
+			AstNode *node = new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
+		if ($1 != nullptr)
+			delete $1;
 	} |
-	opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
-		if (noassume_mode)
+	opt_sva_label TOK_ASSUME opt_property '(' expr ')' ';' {
+		if (noassume_mode) {
 			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
+		} else {
+			AstNode *node = new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
+		if ($1 != nullptr)
+			delete $1;
 	} |
-	opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		if (noassert_mode)
+	opt_sva_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
+		if (noassert_mode) {
 			delete $6;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+		} else {
+			AstNode *node = new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
+		if ($1 != nullptr)
+			delete $1;
 	} |
-	opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		if (noassume_mode)
+	opt_sva_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
+		if (noassume_mode) {
 			delete $6;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
+		} else {
+			AstNode *node = new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
+		if ($1 != nullptr)
+			delete $1;
 	} |
-	opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));
+	opt_sva_label TOK_COVER opt_property '(' expr ')' ';' {
+		AstNode *node = new AstNode(AST_COVER, $5);
+		if ($1 != nullptr) {
+			node->str = *$1;
+			delete $1;
+		}
+		ast_stack.back()->children.push_back(node);
 	} |
-	opt_stmt_label TOK_COVER opt_property '(' ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	opt_sva_label TOK_COVER opt_property '(' ')' ';' {
+		AstNode *node = new AstNode(AST_COVER, AstNode::mkconst_int(1, false));
+		if ($1 != nullptr) {
+			node->str = *$1;
+			delete $1;
+		}
+		ast_stack.back()->children.push_back(node);
 	} |
-	opt_stmt_label TOK_COVER ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	opt_sva_label TOK_COVER ';' {
+		AstNode *node = new AstNode(AST_COVER, AstNode::mkconst_int(1, false));
+		if ($1 != nullptr) {
+			node->str = *$1;
+			delete $1;
+		}
+		ast_stack.back()->children.push_back(node);
 	} |
-	opt_stmt_label TOK_RESTRICT opt_property '(' expr ')' ';' {
-		if (norestrict_mode)
+	opt_sva_label TOK_RESTRICT opt_property '(' expr ')' ';' {
+		if (norestrict_mode) {
 			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
+		} else {
+			AstNode *node = new AstNode(AST_ASSUME, $5);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
 		if (!$3)
 			log_file_warning(current_filename, get_line_num(), "SystemVerilog does not allow \"restrict\" without \"property\".\n");
+		if ($1 != nullptr)
+			delete $1;
 	} |
-	opt_stmt_label TOK_RESTRICT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		if (norestrict_mode)
+	opt_sva_label TOK_RESTRICT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
+		if (norestrict_mode) {
 			delete $6;
-		else
-			ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
+		} else {
+			AstNode *node = new AstNode(AST_FAIR, $6);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
 		if (!$3)
 			log_file_warning(current_filename, get_line_num(), "SystemVerilog does not allow \"restrict\" without \"property\".\n");
+		if ($1 != nullptr)
+			delete $1;
 	};
 
 assert_property:
-	TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $4));
-	} |
-	TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
+	opt_sva_label TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
-	TOK_ASSERT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $5));
+	opt_sva_label TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
-	TOK_ASSUME TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
+	opt_sva_label TOK_ASSERT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
-	TOK_COVER TOK_PROPERTY '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4));
+	opt_sva_label TOK_ASSUME TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
-	TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
-		if (norestrict_mode)
-			delete $4;
-		else
-			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
+	opt_sva_label TOK_COVER TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
-	TOK_RESTRICT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
-		if (norestrict_mode)
+	opt_sva_label TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
+		if (norestrict_mode) {
 			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
+		} else {
+			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
+			if ($1 != nullptr) {
+				ast_stack.back()->children.back()->str = *$1;
+				delete $1;
+			}
+		}
+	} |
+	opt_sva_label TOK_RESTRICT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
+		if (norestrict_mode) {
+			delete $6;
+		} else {
+			ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
+			if ($1 != nullptr) {
+				ast_stack.back()->children.back()->str = *$1;
+				delete $1;
+			}
+		}
 	};
 
 simple_behavioral_stmt:
@@ -1670,6 +1756,11 @@ case_expr_list:
 	TOK_DEFAULT {
 		ast_stack.back()->children.push_back(new AstNode(AST_DEFAULT));
 	} |
+	TOK_SVA_LABEL {
+		ast_stack.back()->children.push_back(new AstNode(AST_IDENTIFIER));
+		ast_stack.back()->children.back()->str = *$1;
+		delete $1;
+	} |
 	expr {
 		ast_stack.back()->children.push_back($1);
 	} |