From 1f1deda888ea32ade2478fca9fcb510ada477606 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 26 Feb 2015 18:47:39 +0100 Subject: [PATCH] Added non-std verilog assume() statement --- frontends/ast/ast.cc | 1 + frontends/ast/ast.h | 1 + frontends/ast/genrtlil.cc | 11 +++++--- frontends/ast/simplify.cc | 7 ++--- frontends/verilog/verilog_frontend.cc | 12 +++++++- frontends/verilog/verilog_frontend.h | 3 ++ frontends/verilog/verilog_lexer.l | 5 ++-- frontends/verilog/verilog_parser.y | 10 +++++-- passes/opt/opt_clean.cc | 2 +- passes/sat/sat.cc | 40 +++++++++++++++++++-------- 10 files changed, 67 insertions(+), 25 deletions(-) diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 0de24013..0b63248d 100644 --- 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 0c113562..d57e91e5 100644 --- 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 4a84e0a9..c421364a 100644 --- 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 404dab4e..a65d2dbb 100644 --- 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 41561e80..635c9ce4 100644 --- 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 e277f3e3..5561f54c 100644 --- 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 13b3e2bf..3a57514a 100644 --- 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 fee438a9..d935cab3 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -57,7 +57,7 @@ namespace VERILOG_FRONTEND { std::vector 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 *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 range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int %type 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 e9f653e5..9d2a262a 100644 --- 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 79d1ec86..9e5cc9e9 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -51,7 +51,7 @@ struct SatHelper std::vector> sets, prove, prove_x, sets_init; std::map>> sets_at; std::map> 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"); log(" -set-any-undef-at \n"); log(" -set-all-undef-at \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;