From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 16:02:13 +0000 (+0100)
Subject: Further improve cover() support
X-Git-Tag: yosys-0.8~521
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6abf79eb280a645f5896f307dca7afb92d75d25e;p=yosys.git

Further improve cover() support
---

diff --git a/README.md b/README.md
index 9b9f72cc0..221bb0ce1 100644
--- a/README.md
+++ b/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
-  ``read_verilog`` is called with ``-formal``.
+- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' is enabled
+  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
-  supported. The same limitations as with the ``assert`` statement apply.
+- The ``assume``, ``restrict``, and ``cover`` statements from SystemVerilog are
+  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.
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e0daae728..02661f1cf 100644
--- a/backends/smt2/smt2.cc
+++ b/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++)
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 0f823a082..4fedff5cf 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/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;