diff options
| -rw-r--r-- | README.md | 10 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 8 | ||||
| -rw-r--r-- | frontends/verilog/verilog_parser.y | 6 |
3 files changed, 16 insertions, 8 deletions
@@ -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; |