Added read_verilog -norestrict -assume-asserts

4 files changed, 40 insertions, 5 deletions

diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 8ec347e89..894723c85 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -63,9 +63,15 @@ struct VerilogFrontend : public Frontend {
 		log("        of SystemVerilog is supported)\n");
 		log("\n");
 		log("    -formal\n");
-		log("        enable support for assert() and assume() from SystemVerilog\n");
+		log("        enable support for SystemVerilog assertions and some Yosys extensions\n");
 		log("        replace the implicit -D SYNTHESIS with -D FORMAL\n");
 		log("\n");
+		log("    -norestrict\n");
+		log("        ignore restrict() assertions\n");
+		log("\n");
+		log("    -assume-asserts\n");
+		log("        treat all assert() statements like assume() statements\n");
+		log("\n");
 		log("    -dump_ast1\n");
 		log("        dump abstract syntax tree (before simplification)\n");
 		log("\n");
@@ -190,6 +196,8 @@ struct VerilogFrontend : public Frontend {
 		frontend_verilog_yydebug = false;
 		sv_mode = false;
 		formal_mode = false;
+		norestrict_mode = false;
+		assume_asserts_mode = false;
 		lib_mode = false;
 		default_nettype_wire = true;
 
@@ -208,6 +216,14 @@ struct VerilogFrontend : public Frontend {
 				formal_mode = true;
 				continue;
 			}
+			if (arg == "-norestrict") {
+				norestrict_mode = true;
+				continue;
+			}
+			if (arg == "-assume-asserts") {
+				assume_asserts_mode = true;
+				continue;
+			}
 			if (arg == "-dump_ast1") {
 				flag_dump_ast1 = true;
 				continue;
diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index 3801aed4a..606ec20a2 100644
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -54,6 +54,12 @@ namespace VERILOG_FRONTEND
 	// running in -formal mode
 	extern bool formal_mode;
 
+	// running in -norestrict mode
+	extern bool norestrict_mode;
+
+	// running in -assume-asserts mode
+	extern bool assume_asserts_mode;
+
 	// running in -lib mode
 	extern bool lib_mode;
 
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 0c974d392..cf9456fc5 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -177,7 +177,7 @@ YOSYS_NAMESPACE_END
 
 "assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
 "assume"   { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
-"restrict" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
+"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
 "predict"  { if (formal_mode) return TOK_PREDICT; NON_KEYWORD(); }
 "property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
 "logic"    { SV_KEYWORD(TOK_REG); }
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index d0d6a5fe1..c3f61c557 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -58,6 +58,7 @@ namespace VERILOG_FRONTEND {
 	bool do_not_require_port_stubs;
 	bool default_nettype_wire;
 	bool sv_mode, formal_mode, lib_mode;
+	bool norestrict_mode, assume_asserts_mode;
 	std::istream *lexin;
 }
 YOSYS_NAMESPACE_END
@@ -113,7 +114,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %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_PREDICT TOK_PROPERTY
+%token TOK_RESTRICT TOK_PREDICT TOK_PROPERTY
 
 %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
@@ -995,22 +996,34 @@ opt_label:
 
 assert:
 	TOK_ASSERT '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3));
+		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $3));
 	} |
 	TOK_ASSUME '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
 	} |
+	TOK_RESTRICT '(' expr ')' ';' {
+		if (norestrict_mode)
+			delete $3;
+		else
+			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
+	} |
 	TOK_PREDICT '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_PREDICT, $3));
 	};
 
 assert_property:
 	TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $4));
+		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));
 	} |
+	TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
+		if (norestrict_mode)
+			delete $4;
+		else
+			ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
+	} |
 	TOK_PREDICT TOK_PROPERTY '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_PREDICT, $4));
 	};