Merge branch 'master' into xaig

15 files changed, 500 insertions, 142 deletions

diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h
index 42c87a298..39757545f 100644
--- a/frontends/aiger/aigerparse.h
+++ b/frontends/aiger/aigerparse.h
@@ -2,6 +2,7 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *                      Eddie Hung <eddie@fpgeh.com>
  *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 5a1bae7a7..d48996167 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -45,7 +45,7 @@ namespace AST {
 
 // instantiate global variables (private API)
 namespace AST_INTERNAL {
-	bool flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit;
+	bool flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog1, flag_dump_vlog2, flag_dump_rtlil, flag_nolatches, flag_nomeminit;
 	bool flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire;
 	AstNode *current_ast, *current_ast_mod;
 	std::map<std::string, AstNode*> current_scope;
@@ -431,9 +431,12 @@ void AstNode::dumpVlog(FILE *f, std::string indent) const
 		break;
 
 	case AST_RANGE:
-		if (range_valid)
-			fprintf(f, "[%d:%d]", range_left, range_right);
-		else {
+		if (range_valid) {
+			if (range_swapped)
+				fprintf(f, "[%d:%d]", range_right, range_left);
+			else
+				fprintf(f, "[%d:%d]", range_left, range_right);
+		} else {
 			for (auto child : children) {
 				fprintf(f, "%c", first ? '[' : ':');
 				child->dumpVlog(f, "");
@@ -562,7 +565,8 @@ void AstNode::dumpVlog(FILE *f, std::string indent) const
 
 	case AST_CONCAT:
 		fprintf(f, "{");
-		for (auto child : children) {
+		for (int i = GetSize(children)-1; i >= 0; i--) {
+			auto child = children[i];
 			if (!first)
 				fprintf(f, ", ");
 			child->dumpVlog(f, "");
@@ -926,23 +930,28 @@ static AstModule* process_module(AstNode *ast, bool defer, AstNode *original_ast
 		ast_before_simplify = ast->clone();
 
 	if (flag_dump_ast1) {
-		log("Dumping Verilog AST before simplification:\n");
+		log("Dumping AST before simplification:\n");
 		ast->dumpAst(NULL, "    ");
 		log("--- END OF AST DUMP ---\n");
 	}
+	if (flag_dump_vlog1) {
+		log("Dumping Verilog AST before simplification:\n");
+		ast->dumpVlog(NULL, "    ");
+		log("--- END OF AST DUMP ---\n");
+	}
 
 	if (!defer)
 	{
 		while (ast->simplify(!flag_noopt, false, false, 0, -1, false, false)) { }
 
 		if (flag_dump_ast2) {
-			log("Dumping Verilog AST after simplification:\n");
+			log("Dumping AST after simplification:\n");
 			ast->dumpAst(NULL, "    ");
 			log("--- END OF AST DUMP ---\n");
 		}
 
-		if (flag_dump_vlog) {
-			log("Dumping Verilog AST (as requested by dump_vlog option):\n");
+		if (flag_dump_vlog2) {
+			log("Dumping Verilog AST after simplification:\n");
 			ast->dumpVlog(NULL, "    ");
 			log("--- END OF AST DUMP ---\n");
 		}
@@ -1016,14 +1025,15 @@ static AstModule* process_module(AstNode *ast, bool defer, AstNode *original_ast
 }
 
 // create AstModule instances for all modules in the AST tree and add them to 'design'
-void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool no_dump_ptr, bool dump_vlog, bool dump_rtlil,
+void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool no_dump_ptr, bool dump_vlog1, bool dump_vlog2, bool dump_rtlil,
 		bool nolatches, bool nomeminit, bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool nooverwrite, bool overwrite, bool defer, bool autowire)
 {
 	current_ast = ast;
 	flag_dump_ast1 = dump_ast1;
 	flag_dump_ast2 = dump_ast2;
 	flag_no_dump_ptr = no_dump_ptr;
-	flag_dump_vlog = dump_vlog;
+	flag_dump_vlog1 = dump_vlog1;
+	flag_dump_vlog2 = dump_vlog2;
 	flag_dump_rtlil = dump_rtlil;
 	flag_nolatches = nolatches;
 	flag_nomeminit = nomeminit;
@@ -1357,7 +1367,8 @@ std::string AstModule::derive_common(RTLIL::Design *design, dict<RTLIL::IdString
 	current_ast = NULL;
 	flag_dump_ast1 = false;
 	flag_dump_ast2 = false;
-	flag_dump_vlog = false;
+	flag_dump_vlog1 = false;
+	flag_dump_vlog2 = false;
 	flag_nolatches = nolatches;
 	flag_nomeminit = nomeminit;
 	flag_nomem2reg = nomem2reg;
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index 08f91c9c3..ddd59d4be 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;
@@ -279,7 +282,7 @@ namespace AST
 	};
 
 	// process an AST tree (ast must point to an AST_DESIGN node) and generate RTLIL code
-	void process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool no_dump_ptr, bool dump_vlog, bool dump_rtlil, bool nolatches, bool nomeminit,
+	void process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool no_dump_ptr, bool dump_vlog1, bool dump_vlog2, bool dump_rtlil, bool nolatches, bool nomeminit,
 			bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool nooverwrite, bool overwrite, bool defer, bool autowire);
 
 	// parametric modules are supported directly by the AST library
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 2d591b29d..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:
@@ -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) {
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 46013544b..63b71b800 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;
 
@@ -137,9 +138,15 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 				int mem_width, mem_size, addr_bits;
 				node->meminfo(mem_width, mem_size, addr_bits);
 
+				int data_range_left = node->children[0]->range_left;
+				int data_range_right = node->children[0]->range_right;
+
+				if (node->children[0]->range_swapped)
+					std::swap(data_range_left, data_range_right);
+
 				for (int i = 0; i < mem_size; i++) {
 					AstNode *reg = new AstNode(AST_WIRE, new AstNode(AST_RANGE,
-							mkconst_int(mem_width-1, true), mkconst_int(0, true)));
+							mkconst_int(data_range_left, true), mkconst_int(data_range_right, true)));
 					reg->str = stringf("%s[%d]", node->str.c_str(), i);
 					reg->is_reg = true;
 					reg->is_signed = node->is_signed;
@@ -325,6 +332,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)
@@ -938,7 +954,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 			}
 		}
 		if (current_scope.count(str) == 0) {
-			if (flag_autowire) {
+			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);
@@ -966,6 +982,9 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		int data_range_left = id2ast->children[0]->range_left;
 		int data_range_right = id2ast->children[0]->range_right;
 
+		if (id2ast->children[0]->range_swapped)
+			std::swap(data_range_left, data_range_right);
+
 		std::stringstream sstr;
 		sstr << "$mem2bits$" << str << "$" << filename << ":" << linenum << "$" << (autoidx++);
 		std::string wire_id = sstr.str();
@@ -1499,6 +1518,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;
@@ -1579,14 +1599,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);
@@ -2169,6 +2181,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;
 			}
 
@@ -2210,6 +2224,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)
 		{
@@ -2334,8 +2350,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);
@@ -2357,13 +2373,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);
 				}
 			}
 
@@ -2377,14 +2390,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) {
@@ -2855,7 +2872,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);
 	}
 
@@ -2910,7 +2931,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)
 	{
@@ -2936,6 +2957,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))
@@ -2948,7 +2979,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)
@@ -2991,12 +3022,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;
 
@@ -3048,6 +3090,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) {
@@ -3277,6 +3352,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/ilang/ilang_frontend.cc b/frontends/ilang/ilang_frontend.cc
index 6b302a796..30d9ff79d 100644
--- a/frontends/ilang/ilang_frontend.cc
+++ b/frontends/ilang/ilang_frontend.cc
@@ -47,16 +47,20 @@ struct IlangFrontend : public Frontend {
 		log("    -nooverwrite\n");
 		log("        ignore re-definitions of modules. (the default behavior is to\n");
 		log("        create an error message if the existing module is not a blackbox\n");
-		log("        module, and overwrite the existing module if it is  a blackbox module.)\n");
+		log("        module, and overwrite the existing module if it is a blackbox module.)\n");
 		log("\n");
 		log("    -overwrite\n");
 		log("        overwrite existing modules with the same name\n");
 		log("\n");
+		log("    -lib\n");
+		log("        only create empty blackbox modules\n");
+		log("\n");
 	}
 	void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
 		ILANG_FRONTEND::flag_nooverwrite = false;
 		ILANG_FRONTEND::flag_overwrite = false;
+		ILANG_FRONTEND::flag_lib = false;
 
 		log_header(design, "Executing ILANG frontend.\n");
 
@@ -73,6 +77,10 @@ struct IlangFrontend : public Frontend {
 				ILANG_FRONTEND::flag_overwrite = true;
 				continue;
 			}
+			if (arg == "-lib") {
+				ILANG_FRONTEND::flag_lib = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
diff --git a/frontends/ilang/ilang_frontend.h b/frontends/ilang/ilang_frontend.h
index 052dd4cb2..f8a152841 100644
--- a/frontends/ilang/ilang_frontend.h
+++ b/frontends/ilang/ilang_frontend.h
@@ -34,6 +34,7 @@ namespace ILANG_FRONTEND {
 	extern RTLIL::Design *current_design;
 	extern bool flag_nooverwrite;
 	extern bool flag_overwrite;
+	extern bool flag_lib;
 }
 
 YOSYS_NAMESPACE_END
diff --git a/frontends/ilang/ilang_parser.y b/frontends/ilang/ilang_parser.y
index 5bcc01f42..f83824088 100644
--- a/frontends/ilang/ilang_parser.y
+++ b/frontends/ilang/ilang_parser.y
@@ -37,7 +37,7 @@ namespace ILANG_FRONTEND {
 	std::vector<std::vector<RTLIL::SwitchRule*>*> switch_stack;
 	std::vector<RTLIL::CaseRule*> case_stack;
 	dict<RTLIL::IdString, RTLIL::Const> attrbuf;
-	bool flag_nooverwrite, flag_overwrite;
+	bool flag_nooverwrite, flag_overwrite, flag_lib;
 	bool delete_current_module;
 }
 using namespace ILANG_FRONTEND;
@@ -98,7 +98,7 @@ module:
 		delete_current_module = false;
 		if (current_design->has($2)) {
 			RTLIL::Module *existing_mod = current_design->module($2);
-			if (!flag_overwrite && attrbuf.count("\\blackbox") && attrbuf.at("\\blackbox").as_bool()) {
+			if (!flag_overwrite && (flag_lib || (attrbuf.count("\\blackbox") && attrbuf.at("\\blackbox").as_bool()))) {
 				log("Ignoring blackbox re-definition of module %s.\n", $2);
 				delete_current_module = true;
 			} else if (!flag_nooverwrite && !flag_overwrite && !existing_mod->get_bool_attribute("\\blackbox")) {
@@ -124,6 +124,8 @@ module:
 		current_module->fixup_ports();
 		if (delete_current_module)
 			delete current_module;
+		else if (flag_lib)
+			current_module->makeblackbox();
 		current_module = nullptr;
 	} EOL;
 
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 8ee951d20..ed9727b88 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1619,30 +1619,35 @@ struct VerificExtNets
 	int portname_cnt = 0;
 
 	// a map from Net to the same Net one level up in the design hierarchy
-	std::map<Net*, Net*> net_level_up;
+	std::map<Net*, Net*> net_level_up_drive_up;
+	std::map<Net*, Net*> net_level_up_drive_down;
 
-	Net *get_net_level_up(Net *net)
+	Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr)
 	{
+		auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down;
+
 		if (net_level_up.count(net) == 0)
 		{
 			Netlist *nl = net->Owner();
 
 			// Simply return if Netlist is not unique
-			if (nl->NumOfRefs() != 1)
-				return net;
+			log_assert(nl->NumOfRefs() == 1);
 
 			Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
 			Netlist *up_nl = up_inst->Owner();
 
 			// create new Port
 			string name = stringf("___extnets_%d", portname_cnt++);
-			Port *new_port = new Port(name.c_str(), DIR_OUT);
+			Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN);
 			nl->Add(new_port);
 			net->Connect(new_port);
 
 			// create new Net in up Netlist
-			Net *new_net = new Net(name.c_str());
-			up_nl->Add(new_net);
+			Net *new_net = final_net;
+			if (new_net == nullptr || new_net->Owner() != up_nl) {
+				new_net = new Net(name.c_str());
+				up_nl->Add(new_net);
+			}
 			up_inst->Connect(new_port, new_net);
 
 			net_level_up[net] = new_net;
@@ -1651,6 +1656,39 @@ struct VerificExtNets
 		return net_level_up.at(net);
 	}
 
+	Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr)
+	{
+		while (net->Owner() != dest)
+			net = route_up(net, drive_up, final_net);
+		if (final_net != nullptr)
+			log_assert(net == final_net);
+		return net;
+	}
+
+	Netlist *find_common_ancestor(Netlist *A, Netlist *B)
+	{
+		std::set<Netlist*> ancestors_of_A;
+
+		Netlist *cursor = A;
+		while (1) {
+			ancestors_of_A.insert(cursor);
+			if (cursor->NumOfRefs() != 1)
+				break;
+			cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
+		}
+
+		cursor = B;
+		while (1) {
+			if (ancestors_of_A.count(cursor))
+				return cursor;
+			if (cursor->NumOfRefs() != 1)
+				break;
+			cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
+		}
+
+		log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A).c_str(), get_full_netlist_name(B).c_str());
+	}
+
 	void run(Netlist *nl)
 	{
 		MapIter mi, mi2;
@@ -1674,19 +1712,37 @@ struct VerificExtNets
 			if (verific_verbose)
 				log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
 
-			while (net->IsExternalTo(nl))
-			{
-				Net *newnet = get_net_level_up(net);
-				if (newnet == net) break;
+			Netlist *ext_nl = net->Owner();
+
+			if (verific_verbose)
+				log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str());
 
+			Netlist *ca_nl = find_common_ancestor(nl, ext_nl);
+
+			if (verific_verbose)
+				log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str());
+
+			Net *ca_net = route_up(net, !port->IsOutput(), ca_nl);
+			Net *new_net = ca_net;
+
+			if (ca_nl != nl)
+			{
 				if (verific_verbose)
-					log("  external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
-				net = newnet;
+					log(" net in common ancestor: %s\n", ca_net->Name());
+
+				string name = stringf("___extnets_%d", portname_cnt++);
+				new_net = new Net(name.c_str());
+				nl->Add(new_net);
+
+				Net *n = route_up(new_net, port->IsOutput(), ca_nl, ca_net);
+				log_assert(n == ca_net);
 			}
 
 			if (verific_verbose)
-				log("  final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
-			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
+				log(" new local net: %s\n", new_net->Name());
+
+			log_assert(!new_net->IsExternalTo(nl));
+			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net));
 		}
 
 		for (auto it : todo_connect) {
@@ -1855,6 +1911,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");
@@ -2109,6 +2172,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") {
@@ -2147,6 +2211,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;
@@ -2180,7 +2253,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;
 
@@ -2217,7 +2290,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;
 
@@ -2313,21 +2386,43 @@ struct ReadPass : public Pass {
 		log("\n");
 		log("Add directory to global Verilog/SystemVerilog include directories.\n");
 		log("\n");
+		log("\n");
+		log("    read -verific\n");
+		log("    read -noverific\n");
+		log("\n");
+		log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
+		log("with -verific will result in an error on Yosys binaries that are built without\n");
+		log("Verific support. The default is to use Verific if it is available.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		if (args.size() < 2)
+#ifdef YOSYS_ENABLE_VERIFIC
+		static bool verific_available = !check_noverific_env();
+#else
+		static bool verific_available = false;
+#endif
+		static bool use_verific = verific_available;
+
+		if (args.size() < 2 || args[1][0] != '-')
 			log_cmd_error("Missing mode parameter.\n");
 
+		if (args[1] == "-verific" || args[1] == "-noverific") {
+			if (args.size() != 2)
+				log_cmd_error("Additional arguments to -verific/-noverific.\n");
+			if (args[1] == "-verific") {
+				if (!verific_available)
+					log_cmd_error("This version of Yosys is built without Verific support.\n");
+				use_verific = true;
+			} else {
+				use_verific = false;
+			}
+			return;
+		}
+
 		if (args.size() < 3)
 			log_cmd_error("Missing file name parameter.\n");
 
-#ifdef YOSYS_ENABLE_VERIFIC
-		bool use_verific = !check_noverific_env();
-#else
-		bool use_verific = false;
-#endif
-
 		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
 			if (use_verific) {
 				args[0] = "verific";
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/Makefile.inc b/frontends/verilog/Makefile.inc
index dbaace585..0a1f97ac0 100644
--- a/frontends/verilog/Makefile.inc
+++ b/frontends/verilog/Makefile.inc
@@ -14,6 +14,8 @@ frontends/verilog/verilog_lexer.cc: frontends/verilog/verilog_lexer.l
 	$(Q) mkdir -p $(dir $@)
 	$(P) flex -o frontends/verilog/verilog_lexer.cc $<
 
+frontends/verilog/verilog_parser.tab.o: CXXFLAGS += -DYYMAXDEPTH=100000
+
 OBJS += frontends/verilog/verilog_parser.tab.o
 OBJS += frontends/verilog/verilog_lexer.o
 OBJS += frontends/verilog/preproc.o
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index aeea36a2b..504f8b3f3 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -81,6 +81,9 @@ struct VerilogFrontend : public Frontend {
 		log("    -assert-assumes\n");
 		log("        treat all assume() statements like assert() statements\n");
 		log("\n");
+		log("    -debug\n");
+		log("        alias for -dump_ast1 -dump_ast2 -dump_vlog1 -dump_vlog2 -yydebug\n");
+		log("\n");
 		log("    -dump_ast1\n");
 		log("        dump abstract syntax tree (before simplification)\n");
 		log("\n");
@@ -90,7 +93,10 @@ struct VerilogFrontend : public Frontend {
 		log("    -no_dump_ptr\n");
 		log("        do not include hex memory addresses in dump (easier to diff dumps)\n");
 		log("\n");
-		log("    -dump_vlog\n");
+		log("    -dump_vlog1\n");
+		log("        dump ast as Verilog code (before simplification)\n");
+		log("\n");
+		log("    -dump_vlog2\n");
 		log("        dump ast as Verilog code (after simplification)\n");
 		log("\n");
 		log("    -dump_rtlil\n");
@@ -197,7 +203,8 @@ struct VerilogFrontend : public Frontend {
 		bool flag_dump_ast1 = false;
 		bool flag_dump_ast2 = false;
 		bool flag_no_dump_ptr = false;
-		bool flag_dump_vlog = false;
+		bool flag_dump_vlog1 = false;
+		bool flag_dump_vlog2 = false;
 		bool flag_dump_rtlil = false;
 		bool flag_nolatches = false;
 		bool flag_nomeminit = false;
@@ -258,6 +265,14 @@ struct VerilogFrontend : public Frontend {
 				assert_assumes_mode = true;
 				continue;
 			}
+			if (arg == "-debug") {
+				flag_dump_ast1 = true;
+				flag_dump_ast2 = true;
+				flag_dump_vlog1 = true;
+				flag_dump_vlog2 = true;
+				frontend_verilog_yydebug = true;
+				continue;
+			}
 			if (arg == "-dump_ast1") {
 				flag_dump_ast1 = true;
 				continue;
@@ -270,8 +285,12 @@ struct VerilogFrontend : public Frontend {
 				flag_no_dump_ptr = true;
 				continue;
 			}
-			if (arg == "-dump_vlog") {
-				flag_dump_vlog = true;
+			if (arg == "-dump_vlog1") {
+				flag_dump_vlog1 = true;
+				continue;
+			}
+			if (arg == "-dump_vlog2") {
+				flag_dump_vlog2 = true;
 				continue;
 			}
 			if (arg == "-dump_rtlil") {
@@ -410,7 +429,7 @@ struct VerilogFrontend : public Frontend {
 		if (flag_nodpi)
 			error_on_dpi_function(current_ast);
 
-		AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, lib_mode, flag_noopt, flag_icells, flag_nooverwrite, flag_overwrite, flag_defer, default_nettype_wire);
+		AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog1, flag_dump_vlog2, flag_dump_rtlil, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, lib_mode, flag_noopt, flag_icells, flag_nooverwrite, flag_overwrite, flag_defer, default_nettype_wire);
 
 		if (!flag_nopp)
 			delete lexin;
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);
 	} |