Further improve cover() support

README.md

@@ -46,7 +46,7 @@ Getting Started
 
 You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is
 recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make.
-TCL, readline and libffi are optional (see ENABLE_* settings in Makefile).
+TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile).
 Xdot (graphviz) is used by the ``show`` command in yosys to display schematics.
 For example on Ubuntu Linux 16.04 LTS the following commands will install all
 prerequisites for building yosys:
@@ -372,8 +372,8 @@ Verilog Attributes and non-standard features
 Non-standard or SystemVerilog features for formal verification
 ==============================================================
 
-- Support for ``assert``, ``assume``, and ``restrict`` is enabled when
+- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' is enabled
-  ``read_verilog`` is called with ``-formal``.
+  when ``read_verilog`` is called with ``-formal``.
 
 - The system task ``$initstate`` evaluates to 1 in the initial state and
   to 0 otherwise.
@@ -400,8 +400,8 @@ from SystemVerilog:
   form. In module context: ``assert property (<expression>);`` and within an
   always block: ``assert(<expression>);``. It is transformed to a $assert cell.
 
-- The ``assume`` and ``restrict`` statements from SystemVerilog are also
+- The ``assume``, ``restrict``, and ``cover`` statements from SystemVerilog are
-  supported. The same limitations as with the ``assert`` statement apply.
+  also supported. The same limitations as with the ``assert`` statement apply.
 
 - The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
   and ``bit`` are supported.

backends/smt2/smt2.cc

@@ -662,9 +662,9 @@ struct Smt2Worker
 
 		if (verbose) log("=> export logic driving asserts\n");
 
-		vector<string> assert_list, assume_list;
+		vector<string> assert_list, assume_list, cover_list;
 		for (auto cell : module->cells())
-			if (cell->type.in("$assert", "$assume")) {
+			if (cell->type.in("$assert", "$assume", "$cover")) {
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
@@ -673,8 +673,10 @@ struct Smt2Worker
 						get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				if (cell->type == "$assert")
 					assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
-				else
+				else if (cell->type == "$assume")
 					assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
+				else if (cell->type == "$cover")
+					cover_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
 			}
 
 		for (int iter = 1; !registers.empty(); iter++)

frontends/verilog/verilog_parser.y

@@ -1003,6 +1003,12 @@ assert:
 	TOK_COVER '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3));
 	} |
+	TOK_COVER '(' ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
+	TOK_COVER ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
 	TOK_RESTRICT '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $3;