4 files changed, 25 insertions, 5 deletions
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 41561e80c..635c9ce47 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -54,6 +54,10 @@ struct VerilogFrontend : public Frontend {
 		log("        enable support for SystemVerilog features. (only a small subset\n");
 		log("        of SystemVerilog is supported)\n");
 		log("\n");
+		log("    -formal\n");
+		log("        enable support for assert() and assume() statements\n");
+		log("        (assert support is also enabled with -sv)\n");
+		log("\n");
 		log("    -dump_ast1\n");
 		log("        dump abstract syntax tree (before simplification)\n");
 		log("\n");
@@ -164,6 +168,7 @@ struct VerilogFrontend : public Frontend {
 
 		frontend_verilog_yydebug = false;
 		sv_mode = false;
+		formal_mode = false;
 
 		log_header("Executing Verilog-2005 frontend.\n");
 
@@ -176,6 +181,10 @@ struct VerilogFrontend : public Frontend {
 				sv_mode = true;
 				continue;
 			}
+			if (arg == "-formal") {
+				formal_mode = true;
+				continue;
+			}
 			if (arg == "-dump_ast1") {
 				flag_dump_ast1 = true;
 				continue;
@@ -271,7 +280,8 @@ struct VerilogFrontend : public Frontend {
 		}
 		extra_args(f, filename, args, argidx);
 
-		log("Parsing %s input from `%s' to AST representation.\n", sv_mode ? "SystemVerilog" : "Verilog", filename.c_str());
+		log("Parsing %s%s input from `%s' to AST representation.\n",
+				formal_mode ? "formal " : "", sv_mode ? "SystemVerilog" : "Verilog", filename.c_str());
 
 		AST::current_filename = filename;
 		AST::set_line_num = &frontend_verilog_yyset_lineno;
diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index e277f3e3c..5561f54cd 100644
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -51,6 +51,9 @@ namespace VERILOG_FRONTEND
 	// running in SystemVerilog mode
 	extern bool sv_mode;
 
+	// running in -formal mode
+	extern bool formal_mode;
+
 	// lexer input stream
 	extern std::istream *lexin;
 }
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 13b3e2bfc..3a57514aa 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -166,8 +166,9 @@ YOSYS_NAMESPACE_END
 "always_ff"    { SV_KEYWORD(TOK_ALWAYS); }
 "always_latch" { SV_KEYWORD(TOK_ALWAYS); }
 
-"assert"   { SV_KEYWORD(TOK_ASSERT); }
-"property" { SV_KEYWORD(TOK_PROPERTY); }
+"assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
+"assume"   { if (formal_mode) return TOK_ASSUME; return TOK_ID; }
+"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
 "logic"    { SV_KEYWORD(TOK_REG); }
 "bit"      { SV_KEYWORD(TOK_REG); }
 
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index fee438a9f..d935cab37 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -57,7 +57,7 @@ namespace VERILOG_FRONTEND {
 	std::vector<char> case_type_stack;
 	bool do_not_require_port_stubs;
 	bool default_nettype_wire;
-	bool sv_mode;
+	bool sv_mode, formal_mode;
 	std::istream *lexin;
 }
 YOSYS_NAMESPACE_END
@@ -111,7 +111,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_PROPERTY
+%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME 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
@@ -934,11 +934,17 @@ opt_label:
 assert:
 	TOK_ASSERT '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3));
+	} |
+	TOK_ASSUME '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
 	};
 
 assert_property:
 	TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $4));
+	} |
+	TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
 	};
 
 simple_behavioral_stmt: