Added non-std verilog assume() statement

diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 0de24013c6730fbd79698f0e7a7d67e50dcef916..0b63248d839170edd7d7df144e71f87b0f9420ad 100644 (file)
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -90,6 +90,7 @@ std::string AST::type2str(AstNodeType type)
        X(AST_IDENTIFIER)
        X(AST_PREFIX)
        X(AST_ASSERT)
+       X(AST_ASSUME)
        X(AST_FCALL)
        X(AST_TO_BITS)
        X(AST_TO_SIGNED)

diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index 0c1135620d611f5c137b08b9f49502975c723b0f..d57e91e5a85b97de9c540d831f338185632031fe 100644 (file)
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -64,6 +64,7 @@ namespace AST
                AST_IDENTIFIER,
                AST_PREFIX,
                AST_ASSERT,
+               AST_ASSUME,
 
                AST_FCALL,
                AST_TO_BITS,

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 4a84e0a9e735232d6c16dd66e3b0b182f226b4a8..c421364a3aec8c46aa011797b1289e435cdb2106 100644 (file)
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1265,19 +1265,22 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 
        // generate $assert cells
        case AST_ASSERT:
+       case AST_ASSUME:
                {
                        log_assert(children.size() == 2);
 
                        RTLIL::SigSpec check = children[0]->genRTLIL();
-                       log_assert(check.size() == 1);
+                       if (GetSize(check) != 1)
+                               check = current_module->ReduceBool(NEW_ID, check);
 
                        RTLIL::SigSpec en = children[1]->genRTLIL();
-                       log_assert(en.size() == 1);
+                       if (GetSize(en) != 1)
+                               en = current_module->ReduceBool(NEW_ID, en);
 
                        std::stringstream sstr;
-                       sstr << "$assert$" << filename << ":" << linenum << "$" << (autoidx++);
+                       sstr << (type == AST_ASSERT ? "$assert$" : "$assume$") << filename << ":" << linenum << "$" << (autoidx++);
 
-                       RTLIL::Cell *cell = current_module->addCell(sstr.str(), "$assert");
+                       RTLIL::Cell *cell = current_module->addCell(sstr.str(), type == AST_ASSERT ? "$assert" : "$assume");
                        cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
 
                        for (auto &attr : attributes) {

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 404dab4e86e7a773fb33235fd439100b17fec384..a65d2dbb119db02b182678d7746fedbbcc48e83d 100644 (file)
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1211,7 +1211,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
        }
 skip_dynamic_range_lvalue_expansion:;
 
-       if (stage > 1 && type == AST_ASSERT && current_block != NULL)
+       if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && current_block != NULL)
        {
                std::stringstream sstr;
                sstr << "$assert$" << filename << ":" << linenum << "$" << (autoidx++);
@@ -1255,7 +1255,7 @@ skip_dynamic_range_lvalue_expansion:;
                newNode->children.push_back(assign_check);
                newNode->children.push_back(assign_en);
 
-               AstNode *assertnode = new AstNode(AST_ASSERT);
+               AstNode *assertnode = new AstNode(type);
                assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
                assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
                assertnode->children[0]->str = id_check;
@@ -1266,9 +1266,8 @@ skip_dynamic_range_lvalue_expansion:;
                goto apply_newNode;
        }
 
-       if (stage > 1 && type == AST_ASSERT && children.size() == 1)
+       if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && children.size() == 1)
        {
-               children[0] = new AstNode(AST_REDUCE_BOOL, children[0]->clone());
                children.push_back(mkconst_int(1, false, 1));
                did_something = true;
        }

diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 41561e80c60545b651f4af46e67b120f4f4b2f1b..635c9ce4789c83961a3f138aa3a54110350292fa 100644 (file)
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -54,6 +54,10 @@ struct VerilogFrontend : public Frontend {
                log("        enable support for SystemVerilog features. (only a small subset\n");
                log("        of SystemVerilog is supported)\n");
                log("\n");
+               log("    -formal\n");
+               log("        enable support for assert() and assume() statements\n");
+               log("        (assert support is also enabled with -sv)\n");
+               log("\n");
                log("    -dump_ast1\n");
                log("        dump abstract syntax tree (before simplification)\n");
                log("\n");
@@ -164,6 +168,7 @@ struct VerilogFrontend : public Frontend {
 
                frontend_verilog_yydebug = false;
                sv_mode = false;
+               formal_mode = false;
 
                log_header("Executing Verilog-2005 frontend.\n");
 
@@ -176,6 +181,10 @@ struct VerilogFrontend : public Frontend {
                                sv_mode = true;
                                continue;
                        }
+                       if (arg == "-formal") {
+                               formal_mode = true;
+                               continue;
+                       }
                        if (arg == "-dump_ast1") {
                                flag_dump_ast1 = true;
                                continue;
@@ -271,7 +280,8 @@ struct VerilogFrontend : public Frontend {
                }
                extra_args(f, filename, args, argidx);
 
-               log("Parsing %s input from `%s' to AST representation.\n", sv_mode ? "SystemVerilog" : "Verilog", filename.c_str());
+               log("Parsing %s%s input from `%s' to AST representation.\n",
+                               formal_mode ? "formal " : "", sv_mode ? "SystemVerilog" : "Verilog", filename.c_str());
 
                AST::current_filename = filename;
                AST::set_line_num = &frontend_verilog_yyset_lineno;

diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index e277f3e3ce03ad9391440f292adbbf6783e51cb9..5561f54cd5caad5c54610048b3efd5e493b37c5c 100644 (file)
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -51,6 +51,9 @@ namespace VERILOG_FRONTEND
        // running in SystemVerilog mode
        extern bool sv_mode;
 
+       // running in -formal mode
+       extern bool formal_mode;
+
        // lexer input stream
        extern std::istream *lexin;
 }

diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 13b3e2bfc7012d3cc7470fe398606705ef1945b8..3a57514aa2ccab0d15f21c21d383481b3d07aba4 100644 (file)
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -166,8 +166,9 @@ YOSYS_NAMESPACE_END
 "always_ff"    { SV_KEYWORD(TOK_ALWAYS); }
 "always_latch" { SV_KEYWORD(TOK_ALWAYS); }
 
-"assert"   { SV_KEYWORD(TOK_ASSERT); }
-"property" { SV_KEYWORD(TOK_PROPERTY); }
+"assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
+"assume"   { if (formal_mode) return TOK_ASSUME; return TOK_ID; }
+"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
 "logic"    { SV_KEYWORD(TOK_REG); }
 "bit"      { SV_KEYWORD(TOK_REG); }
 

diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index fee438a9f6de067c5cfdc2780616ded33167df2e..d935cab377cd22a82c0c830124a63fc06bb3692a 100644 (file)
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -57,7 +57,7 @@ namespace VERILOG_FRONTEND {
        std::vector<char> case_type_stack;
        bool do_not_require_port_stubs;
        bool default_nettype_wire;
-       bool sv_mode;
+       bool sv_mode, formal_mode;
        std::istream *lexin;
 }
 YOSYS_NAMESPACE_END
@@ -111,7 +111,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_GENERATE TOK_ENDGENERATE TOK_GENVAR TOK_REAL
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
-%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_PROPERTY
+%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME TOK_PROPERTY
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
@@ -934,11 +934,17 @@ opt_label:
 assert:
        TOK_ASSERT '(' expr ')' ';' {
                ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3));
+       } |
+       TOK_ASSUME '(' expr ')' ';' {
+               ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
        };
 
 assert_property:
        TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
                ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $4));
+       } |
+       TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
+               ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
        };
 
 simple_behavioral_stmt:

diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index e9f653e5fac9be9c336c148ae53361df4d33d3ce..9d2a262a11224ab62917994d98e3efb0377e8b9e 100644 (file)
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -47,7 +47,7 @@ void rmunused_module_cells(Module *module, bool verbose)
                                        if (bit.wire != nullptr)
                                                wire2driver[bit].insert(cell);
                }
-               if (cell->type.in("$memwr", "$meminit", "$assert") || cell->has_keep_attr())
+               if (cell->type.in("$memwr", "$meminit", "$assert", "$assume") || cell->has_keep_attr())
                        queue.insert(cell);
                else
                        unused.insert(cell);

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 79d1ec8600c892007a2917e9d75ed15cc827e96c..9e5cc9e91d855afde264029204d6adc9fbf699a5 100644 (file)
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -51,7 +51,7 @@ struct SatHelper
        std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
        std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
        std::map<int, std::vector<std::string>> unsets_at;
-       bool prove_asserts;
+       bool prove_asserts, set_assumes;
 
        // undef constraints
        bool enable_undef, set_init_def, set_init_undef, set_init_zero, ignore_unknown_cells;
@@ -319,20 +319,28 @@ struct SatHelper
                }
 
                int import_cell_counter = 0;
-               for (auto &c : module->cells_)
-                       if (design->selected(module, c.second)) {
-                               // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
-                               if (satgen.importCell(c.second, timestep)) {
-                                       for (auto &p : c.second->connections())
-                                               if (ct.cell_output(c.second->type, p.first))
-                                                       show_drivers.insert(sigmap(p.second), c.second);
+               for (auto cell : module->cells())
+                       if (design->selected(module, cell)) {
+                               // log("Import cell: %s\n", RTLIL::id2cstr(cell->name));
+                               if (satgen.importCell(cell, timestep)) {
+                                       for (auto &p : cell->connections())
+                                               if (ct.cell_output(cell->type, p.first))
+                                                       show_drivers.insert(sigmap(p.second), cell);
                                        import_cell_counter++;
                                } else if (ignore_unknown_cells)
-                                       log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+                                       log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
                                else
-                                       log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+                                       log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
                }
                log("Imported %d cells to SAT database.\n", import_cell_counter);
+
+               if (set_assumes) {
+                       RTLIL::SigSpec assumes_a, assumes_en;
+                       satgen.getAssumes(assumes_a, assumes_en, timestep);
+                       for (int i = 0; i < GetSize(assumes_a); i++)
+                               log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
+                       ez->assume(satgen.importAssumes(timestep));
+               }
        }
 
        int setup_proof(int timestep = -1)
@@ -948,6 +956,9 @@ struct SatPass : public Pass {
                log("        set or unset the specified signal to the specified value in the\n");
                log("        given timestep. this has priority over a -set for the same signal.\n");
                log("\n");
+               log("    -set-assumes\n");
+               log("        set all assumptions provided via $assume cells\n");
+               log("\n");
                log("    -set-def-at <N> <signal>\n");
                log("    -set-any-undef-at <N> <signal>\n");
                log("    -set-all-undef-at <N> <signal>\n");
@@ -1054,7 +1065,7 @@ struct SatPass : public Pass {
                bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
                bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
                bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
-               bool tempinduct_baseonly = false, tempinduct_inductonly = false;
+               bool tempinduct_baseonly = false, tempinduct_inductonly = false, set_assumes = false;
                int tempinduct_skip = 0, stepsize = 1;
                std::string vcd_file_name, json_file_name, cnf_file_name;
 
@@ -1143,6 +1154,10 @@ struct SatPass : public Pass {
                                enable_undef = true;
                                continue;
                        }
+                       if (args[argidx] == "-set-assumes") {
+                               set_assumes = true;
+                               continue;
+                       }
                        if (args[argidx] == "-tempinduct") {
                                tempinduct = true;
                                continue;
@@ -1328,6 +1343,7 @@ struct SatPass : public Pass {
                        bool basecase_setup_init = true;
 
                        basecase.sets = sets;
+                       basecase.set_assumes = set_assumes;
                        basecase.prove = prove;
                        basecase.prove_x = prove_x;
                        basecase.prove_asserts = prove_asserts;
@@ -1353,6 +1369,7 @@ struct SatPass : public Pass {
                                        basecase.setup(timestep);
 
                        inductstep.sets = sets;
+                       inductstep.set_assumes = set_assumes;
                        inductstep.prove = prove;
                        inductstep.prove_x = prove_x;
                        inductstep.prove_asserts = prove_asserts;
@@ -1517,6 +1534,7 @@ struct SatPass : public Pass {
                        SatHelper sathelper(design, module, enable_undef);
 
                        sathelper.sets = sets;
+                       sathelper.set_assumes = set_assumes;
                        sathelper.prove = prove;
                        sathelper.prove_x = prove_x;
                        sathelper.prove_asserts = prove_asserts;