Add "read_verilog -noassert -noassume -assert-assumes"

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 8dcc7c5aa0fb5e07800df852a3e6d22c791ed132..aeea36a2b7e24289690e032be22ada374b229d54 100644 (file)
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -66,12 +66,21 @@ struct VerilogFrontend : public Frontend {
                log("        enable support for SystemVerilog assertions and some Yosys extensions\n");
                log("        replace the implicit -D SYNTHESIS with -D FORMAL\n");
                log("\n");
+               log("    -noassert\n");
+               log("        ignore assert() statements\n");
+               log("\n");
+               log("    -noassume\n");
+               log("        ignore assume() statements\n");
+               log("\n");
                log("    -norestrict\n");
-               log("        ignore restrict() assertions\n");
+               log("        ignore restrict() statements\n");
                log("\n");
                log("    -assume-asserts\n");
                log("        treat all assert() statements like assume() statements\n");
                log("\n");
+               log("    -assert-assumes\n");
+               log("        treat all assume() statements like assert() statements\n");
+               log("\n");
                log("    -dump_ast1\n");
                log("        dump abstract syntax tree (before simplification)\n");
                log("\n");
@@ -229,6 +238,14 @@ struct VerilogFrontend : public Frontend {
                                formal_mode = true;
                                continue;
                        }
+                       if (arg == "-noassert") {
+                               noassert_mode = true;
+                               continue;
+                       }
+                       if (arg == "-noassume") {
+                               noassume_mode = true;
+                               continue;
+                       }
                        if (arg == "-norestrict") {
                                norestrict_mode = true;
                                continue;
@@ -237,6 +254,10 @@ struct VerilogFrontend : public Frontend {
                                assume_asserts_mode = true;
                                continue;
                        }
+                       if (arg == "-assert-assumes") {
+                               assert_assumes_mode = true;
+                               continue;
+                       }
                        if (arg == "-dump_ast1") {
                                flag_dump_ast1 = true;
                                continue;

diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index 16edc79855b34ea73c8a7f4c79d650c7b3b21783..523bbc89786defa4166302fda5c405850ca476d6 100644 (file)
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -54,12 +54,21 @@ namespace VERILOG_FRONTEND
        // running in -formal mode
        extern bool formal_mode;
 
+       // running in -noassert mode
+       extern bool noassert_mode;
+
+       // running in -noassume mode
+       extern bool noassume_mode;
+
        // running in -norestrict mode
        extern bool norestrict_mode;
 
        // running in -assume-asserts mode
        extern bool assume_asserts_mode;
 
+       // running in -assert-assumes mode
+       extern bool assert_assumes_mode;
+
        // running in -lib mode
        extern bool lib_mode;
 

diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 63cf646e9f1fea11acaaf17b8f0b70cdff3e8cc1..16cac14609db3dcdc25707b196fbc60c5d4ff63e 100644 (file)
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -58,7 +58,8 @@ namespace VERILOG_FRONTEND {
        bool do_not_require_port_stubs;
        bool default_nettype_wire;
        bool sv_mode, formal_mode, lib_mode;
-       bool norestrict_mode, assume_asserts_mode;
+       bool noassert_mode, noassume_mode, norestrict_mode;
+       bool assume_asserts_mode, assert_assumes_mode;
        bool current_wire_rand, current_wire_const;
        std::istream *lexin;
 }
@@ -1281,16 +1282,28 @@ opt_stmt_label:
 
 assert:
        opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
-               ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+               if (noassert_mode)
+                       delete $5;
+               else
+                       ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
        } |
        opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
-               ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
+               if (noassume_mode)
+                       delete $5;
+               else
+                       ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
        } |
        opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-               ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+               if (noassert_mode)
+                       delete $6;
+               else
+                       ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
        } |
        opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-               ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
+               if (noassume_mode)
+                       delete $6;
+               else
+                       ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
        } |
        opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
                ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));