Merge pull request #858 from YosysHQ/clifford/svalabels

Add support for using SVA labels in yosys-smtbmc console output

6 files changed, 203 insertions, 58 deletions

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 7f3cc94ca..a26bff57b 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -887,8 +887,8 @@ struct Smt2Worker
 
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
-				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
-						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+				string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
 
 				if (cell->type == "$cover")
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 13383845a..d7da6fb40 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1413,10 +1413,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 d0274cf78..ae7dec88d 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1511,6 +1511,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;
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..e51a12f76 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -189,10 +189,57 @@ YOSYS_NAMESPACE_END
 "always_ff"    { SV_KEYWORD(TOK_ALWAYS); }
 "always_latch" { SV_KEYWORD(TOK_ALWAYS); }
 
-"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); }
-"restrict"   { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
+ /* parse labels on assert, assume, cover, and restrict right here because it's insanley complex
+    to do it in the parser (because we force the parser too early to reduce when parsing cells..) */
+([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(yytext);
+	auto &str = *frontend_verilog_yylval.string;
+	std::string keyword;
+	int cursor = 0;
+
+	while (1) {
+		if (cursor == GetSize(str)) {
+			keyword = str;
+			delete frontend_verilog_yylval.string;
+			frontend_verilog_yylval.string = nullptr;
+			goto sva_without_label;
+		}
+		char c = str[cursor];
+		if (c != ' ' && c != '\t' && c != '\r' && c != '\n' && c != ':') {
+			cursor++;
+			continue;
+		}
+
+		keyword = str.substr(cursor);
+		str = "\\" + str.substr(0, cursor);
+		break;
+	}
+
+	cursor = 0;
+	while (1) {
+		log_assert(cursor < GetSize(keyword));
+		char c = keyword[cursor];
+		if (c != ' ' && c != '\t' && c != '\r' && c != '\n' && c != ':') {
+			keyword = keyword.substr(cursor);
+			break;
+		}
+		cursor++;
+	}
+
+	if      (keyword == "assert")     { return TOK_ASSERT;   }
+	else if (keyword == "assume")     { return TOK_ASSUME;   }
+	else if (keyword == "cover")      { return TOK_COVER;    }
+	else if (keyword == "restrict")   { return TOK_RESTRICT; }
+	else log_abort();
+
+sva_without_label:
+	if      (keyword == "assert")     { if (formal_mode) return TOK_ASSERT;   SV_KEYWORD(TOK_ASSERT);   }
+	else if (keyword == "assume")     { if (formal_mode) return TOK_ASSUME;   SV_KEYWORD(TOK_ASSUME);   }
+	else if (keyword == "cover")      { if (formal_mode) return TOK_COVER;    SV_KEYWORD(TOK_COVER);    }
+	else if (keyword == "restrict")   { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
+	else log_abort();
+}
+
 "property"   { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
 "rand"       { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
 "const"      { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
@@ -303,7 +350,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..649dd384f 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -106,6 +106,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 }
 
 %token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
+%token <string> 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,8 +120,7 @@ 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
 
@@ -1337,9 +1337,6 @@ opt_property:
 		$$ = false;
 	};
 
-opt_stmt_label:
-	TOK_ID ':' | /* empty */;
-
 modport_stmt:
     TOK_MODPORT TOK_ID {
         AstNode *modport = new AstNode(AST_MODPORT);
@@ -1376,83 +1373,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)
-			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+	TOK_ASSERT opt_property '(' expr ')' ';' {
+		if (noassert_mode) {
+			delete $4;
+		} else {
+			AstNode *node = new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $4);
+			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)
-			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
+	TOK_ASSUME opt_property '(' expr ')' ';' {
+		if (noassume_mode) {
+			delete $4;
+		} else {
+			AstNode *node = new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $4);
+			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)
-			delete $6;
-		else
-			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+	TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
+		if (noassert_mode) {
+			delete $5;
+		} else {
+			AstNode *node = new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $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 '(' 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));
+	TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
+		if (noassume_mode) {
+			delete $5;
+		} else {
+			AstNode *node = new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $5);
+			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));
+	TOK_COVER opt_property '(' expr ')' ';' {
+		AstNode *node = new AstNode(AST_COVER, $4);
+		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)));
+	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)));
+	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)
-			delete $5;
-		else
-			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
-		if (!$3)
+	TOK_RESTRICT opt_property '(' expr ')' ';' {
+		if (norestrict_mode) {
+			delete $4;
+		} else {
+			AstNode *node = new AstNode(AST_ASSUME, $4);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
+		if (!$2)
 			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)
-			delete $6;
-		else
-			ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
-		if (!$3)
+	TOK_RESTRICT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
+		if (norestrict_mode) {
+			delete $5;
+		} else {
+			AstNode *node = new AstNode(AST_FAIR, $5);
+			if ($1 != nullptr)
+				node->str = *$1;
+			ast_stack.back()->children.push_back(node);
+		}
+		if (!$2)
 			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));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
 	TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
+		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));
+		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));
+		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));
+		if ($1 != nullptr) {
+			ast_stack.back()->children.back()->str = *$1;
+			delete $1;
+		}
 	} |
 	TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
-		if (norestrict_mode)
+		if (norestrict_mode) {
 			delete $4;
-		else
+		} else {
 			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
+			if ($1 != nullptr) {
+				ast_stack.back()->children.back()->str = *$1;
+				delete $1;
+			}
+		}
 	} |
 	TOK_RESTRICT TOK_PROPERTY '(' TOK_EVENTUALLY expr ')' ';' {
-		if (norestrict_mode)
+		if (norestrict_mode) {
 			delete $5;
-		else
+		} else {
 			ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $5));
+			if ($1 != nullptr) {
+				ast_stack.back()->children.back()->str = *$1;
+				delete $1;
+			}
+		}
 	};
 
 simple_behavioral_stmt: