Further improve cover() support

diff --git a/README.md b/README.md
index 9b9f72cc07e8601e27a6787e9dc2eb53dbe68a82..221bb0ce1b5f150de6870d303b686b2374e70069 100644 (file)
--- 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 e0daae728964a6447dbb804380b803b54eb0c74a..02661f1cf2e5320d3e3042093b728ebd24164b42 100644 (file)
--- 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 0f823a0822a8aa6e46c110529f002d69a986ced7..4fedff5cf2bd2fb729d68190965643377f7d4bd8 100644 (file)
--- 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;