From a7b07696238dbfd8e4fb5fd41d597200abef4909 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 27 Jul 2016 15:40:17 +0200 Subject: [PATCH 1/5] Added "read_verilog -dump_rtlil" --- frontends/ast/ast.cc | 21 ++++++++++++++++----- frontends/ast/ast.h | 8 +++++--- frontends/verilog/verilog_frontend.cc | 10 +++++++++- kernel/log.cc | 7 +++++++ kernel/log.h | 1 + 5 files changed, 38 insertions(+), 9 deletions(-) diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 82b4edef..29795590 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -44,7 +44,8 @@ namespace AST { // instanciate global variables (private API) namespace AST_INTERNAL { - bool flag_dump_ast1, flag_dump_ast2, flag_dump_vlog, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire; + bool flag_dump_ast1, flag_dump_ast2, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit; + bool flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire; AstNode *current_ast, *current_ast_mod; std::map current_scope; const dict *genRTLIL_subst_ptr = NULL; @@ -175,7 +176,7 @@ bool AstNode::get_bool_attribute(RTLIL::IdString id) // create new node (AstNode constructor) // (the optional child arguments make it easier to create AST trees) -AstNode::AstNode(AstNodeType type, AstNode *child1, AstNode *child2) +AstNode::AstNode(AstNodeType type, AstNode *child1, AstNode *child2, AstNode *child3) { static unsigned int hashidx_count = 123456789; hashidx_count = mkhash_xorshift(hashidx_count); @@ -203,6 +204,8 @@ AstNode::AstNode(AstNodeType type, AstNode *child1, AstNode *child2) children.push_back(child1); if (child2) children.push_back(child2); + if (child3) + children.push_back(child3); } // create a (deep recursive) copy of a node @@ -969,16 +972,25 @@ static AstModule* process_module(AstNode *ast, bool defer) current_module->icells = flag_icells; current_module->autowire = flag_autowire; current_module->fixup_ports(); + + if (flag_dump_rtlil) { + log("Dumping generated RTLIL:\n"); + log_module(current_module); + log("--- END OF RTLIL DUMP ---\n"); + } + return current_module; } // create AstModule instances for all modules in the AST tree and add them to 'design' -void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool dump_vlog, bool nolatches, bool nomeminit, bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool ignore_redef, bool defer, bool autowire) +void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool dump_vlog, bool dump_rtlil, + bool nolatches, bool nomeminit, bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool ignore_redef, bool defer, bool autowire) { current_ast = ast; flag_dump_ast1 = dump_ast1; flag_dump_ast2 = dump_ast2; flag_dump_vlog = dump_vlog; + flag_dump_rtlil = dump_rtlil; flag_nolatches = nolatches; flag_nomeminit = nomeminit; flag_nomem2reg = nomem2reg; @@ -1023,9 +1035,8 @@ void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump design->add(process_module(*it, defer)); } - else if ((*it)->type == AST_PACKAGE){ + else if ((*it)->type == AST_PACKAGE) design->verilog_packages.push_back((*it)->clone()); - } else global_decls.push_back(*it); } diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index 5310bcad..530c11ba 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -187,7 +187,7 @@ namespace AST int linenum; // creating and deleting nodes - AstNode(AstNodeType type = AST_NONE, AstNode *child1 = NULL, AstNode *child2 = NULL); + AstNode(AstNodeType type = AST_NONE, AstNode *child1 = NULL, AstNode *child2 = NULL, AstNode *child3 = NULL); AstNode *clone(); void cloneInto(AstNode *other); void delete_children(); @@ -272,7 +272,8 @@ namespace AST }; // process an AST tree (ast must point to an AST_DESIGN node) and generate RTLIL code - void process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool dump_vlog, bool nolatches, bool nomeminit, bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool ignore_redef, bool defer, bool autowire); + void process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool dump_vlog, bool dump_rtlil, bool nolatches, bool nomeminit, + bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool ignore_redef, bool defer, bool autowire); // parametric modules are supported directly by the AST library // therefore we need our own derivate of RTLIL::Module with overloaded virtual functions @@ -302,7 +303,8 @@ namespace AST namespace AST_INTERNAL { // internal state variables - extern bool flag_dump_ast1, flag_dump_ast2, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire; + extern bool flag_dump_ast1, flag_dump_ast2, flag_dump_rtlil, flag_nolatches, flag_nomeminit; + extern bool flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire; extern AST::AstNode *current_ast, *current_ast_mod; extern std::map current_scope; extern const dict *genRTLIL_subst_ptr; diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc index 87ea8c6a..8ec347e8 100644 --- a/frontends/verilog/verilog_frontend.cc +++ b/frontends/verilog/verilog_frontend.cc @@ -75,6 +75,9 @@ struct VerilogFrontend : public Frontend { log(" -dump_vlog\n"); log(" dump ast as Verilog code (after simplification)\n"); log("\n"); + log(" -dump_rtlil\n"); + log(" dump generated RTLIL netlist\n"); + log("\n"); log(" -yydebug\n"); log(" enable parser debug output\n"); log("\n"); @@ -168,6 +171,7 @@ struct VerilogFrontend : public Frontend { bool flag_dump_ast1 = false; bool flag_dump_ast2 = false; bool flag_dump_vlog = false; + bool flag_dump_rtlil = false; bool flag_nolatches = false; bool flag_nomeminit = false; bool flag_nomem2reg = false; @@ -216,6 +220,10 @@ struct VerilogFrontend : public Frontend { flag_dump_vlog = true; continue; } + if (arg == "-dump_rtlil") { + flag_dump_rtlil = true; + continue; + } if (arg == "-yydebug") { frontend_verilog_yydebug = true; continue; @@ -342,7 +350,7 @@ struct VerilogFrontend : public Frontend { if (flag_nodpi) error_on_dpi_function(current_ast); - AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_dump_vlog, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, lib_mode, flag_noopt, flag_icells, flag_ignore_redef, flag_defer, default_nettype_wire); + AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, lib_mode, flag_noopt, flag_icells, flag_ignore_redef, flag_defer, default_nettype_wire); if (!flag_nopp) delete lexin; diff --git a/kernel/log.cc b/kernel/log.cc index fe84184a..12dc453d 100644 --- a/kernel/log.cc +++ b/kernel/log.cc @@ -427,6 +427,13 @@ const char *log_id(RTLIL::IdString str) return p+1; } +void log_module(RTLIL::Module *module, std::string indent) +{ + std::stringstream buf; + ILANG_BACKEND::dump_module(buf, indent, module, module->design, false); + log("%s", buf.str().c_str()); +} + void log_cell(RTLIL::Cell *cell, std::string indent) { std::stringstream buf; diff --git a/kernel/log.h b/kernel/log.h index 33e624dc..f830655c 100644 --- a/kernel/log.h +++ b/kernel/log.h @@ -85,6 +85,7 @@ template static inline const char *log_id(T *obj) { return log_id(obj->name); } +void log_module(RTLIL::Module *module, std::string indent = ""); void log_cell(RTLIL::Cell *cell, std::string indent = ""); #ifndef NDEBUG From 40563129872f5a2287f54cb0dbd79534b493a5d6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 27 Jul 2016 15:41:22 +0200 Subject: [PATCH 2/5] Added $anyconst and $aconst --- frontends/ast/genrtlil.cc | 45 ++++++++++++++++++++++++++++++ frontends/ast/simplify.cc | 4 +++ frontends/verilog/verilog_parser.y | 2 +- kernel/celltypes.h | 2 ++ kernel/rtlil.cc | 6 ++++ manual/CHAPTER_CellLib.tex | 2 +- techlibs/common/simlib.v | 24 ++++++++++++++++ 7 files changed, 83 insertions(+), 2 deletions(-) diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 2fb95ff5..04cdb941 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -750,6 +750,19 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun width_hint = max(width_hint, this_width); break; + case AST_FCALL: + if (str == "\\$anyconst" || str == "\\$aconst") { + if (GetSize(children) == 1) { + while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { } + if (children[0]->type != AST_CONSTANT) + log_error("System function %s called with non-const argument at %s:%d!\n", + RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); + width_hint = max(width_hint, int(children[0]->asInt(true))); + } + break; + } + /* fall through */ + // everything should have been handled above -> print error if not. default: for (auto f : log_files) @@ -1427,6 +1440,38 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) delete always; } break; + case AST_FCALL: { + if (str == "\\$anyconst" || str == "\\$aconst") + { + string myid = stringf("%s$%d", RTLIL::unescape_id(str).c_str(), autoidx++); + int width = width_hint; + + if (GetSize(children) > 1) + log_error("System function %s got %d arguments, expected 1 or 0 at %s:%d.\n", + RTLIL::unescape_id(str).c_str(), GetSize(children), filename.c_str(), linenum); + + if (GetSize(children) == 1) { + if (children[0]->type != AST_CONSTANT) + log_error("System function %s called with non-const argument at %s:%d!\n", + RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); + width = children[0]->asInt(true); + } + + if (width <= 0) + log_error("Failed to detect width of %s at %s:%d!\n", + RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); + + Cell *cell = current_module->addCell(myid, str.substr(1)); + cell->parameters["\\WIDTH"] = width; + + Wire *wire = current_module->addWire(myid + "_wire", width); + cell->setPort("\\Y", wire); + + is_signed = sign_hint; + return SigSpec(wire); + } + } /* fall through */ + // everything should have been handled above -> print error if not. default: for (auto f : log_files) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 9f88cddc..79dc3b7c 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1655,6 +1655,10 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } + // $anyconst and $aconst are mapped in AstNode::genRTLIL() + if (str == "\\$anyconst" || str == "\\$aconst") + return false; + if (str == "\\$clog2") { if (children.size() != 1) diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 4cb65a08..c2327011 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -1219,7 +1219,7 @@ rvalue: $$ = new AstNode(AST_IDENTIFIER, $2); $$->str = *$1; delete $1; - if ($2 == nullptr && $$->str == "\\$initstate") + if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst" || $$->str == "\\$aconst")) $$->type = AST_FCALL; } | hierarchical_id non_opt_multirange { diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 1eea0530..9eb1523e 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -118,6 +118,8 @@ struct CellTypes setup_type("$assume", {A, EN}, pool(), true); setup_type("$predict", {A, EN}, pool(), true); setup_type("$initstate", pool(), {Y}, true); + setup_type("$anyconst", pool(), {Y}, true); + setup_type("$aconst", pool(), {Y}, true); setup_type("$equiv", {A, B}, {Y}, true); } diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 2e5157e8..ad90965f 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1030,6 +1030,12 @@ namespace { return; } + if (cell->type.in("$aconst", "$anyconst")) { + port("\\Y", param("\\WIDTH")); + check_expected(); + return; + } + if (cell->type == "$equiv") { port("\\A", 1); port("\\B", 1); diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 0f113634..bff01d06 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -421,7 +421,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber using the {\tt abc} pass. \begin{fixme} -Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$predict}, {\tt \$equiv}, and {\tt \$initstate} cells. +Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$predict}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$aconst}, and {\tt \$anyconst} cells. \end{fixme} \begin{fixme} diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index 8ab12403..ac4269c9 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1330,6 +1330,30 @@ endmodule // -------------------------------------------------------- +module \$aconst (Y); + +parameter WIDTH = 0; + +output [WIDTH-1:0] Y; + +assign Y = 'bx; + +endmodule + +// -------------------------------------------------------- + +module \$anyconst (Y); + +parameter WIDTH = 0; + +output [WIDTH-1:0] Y; + +assign Y = 'bx; + +endmodule + +// -------------------------------------------------------- + module \$equiv (A, B, Y); input A, B; From 9540be1d45cce45d0008a4160bc4aa70ff0dfe1d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 27 Jul 2016 15:44:11 +0200 Subject: [PATCH 3/5] Removed $predict support from SatGen --- kernel/satgen.h | 9 --------- 1 file changed, 9 deletions(-) diff --git a/kernel/satgen.h b/kernel/satgen.h index 31b7a3e5..fdd2ce8b 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -69,7 +69,6 @@ struct SatGen SigPool initial_state; std::map asserts_a, asserts_en; std::map assumes_a, assumes_en; - std::map predict_a, predict_en; std::map> imported_signals; std::map, bool> initstates; bool ignore_div_by_zero; @@ -1374,14 +1373,6 @@ struct SatGen return true; } - if (cell->type == "$predict") - { - std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); - predict_a[pf].append((*sigmap)(cell->getPort("\\A"))); - predict_en[pf].append((*sigmap)(cell->getPort("\\EN"))); - return true; - } - // Unsupported internal cell types: $pow $lut // .. and all sequential cells except $dff and $_DFF_[NP]_ return false; From 8d88fcb27011a6f8f47a8615c30ab658fafab0f2 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 27 Jul 2016 15:52:20 +0200 Subject: [PATCH 4/5] Added SatGen support for $anyconst --- kernel/satgen.h | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/kernel/satgen.h b/kernel/satgen.h index fdd2ce8b..0a65b490 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -1319,6 +1319,28 @@ struct SatGen return true; } + if (cell->type == "$anyconst") + { + if (timestep < 2) + return true; + + std::vector d = importDefSigSpec(cell->getPort("\\Y"), timestep-1); + std::vector q = importDefSigSpec(cell->getPort("\\Y"), timestep); + + std::vector qq = model_undef ? ez->vec_var(q.size()) : q; + ez->assume(ez->vec_eq(d, qq)); + + if (model_undef) + { + std::vector undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1); + std::vector undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep); + + ez->assume(ez->vec_eq(undef_d, undef_q)); + undefGating(q, qq, undef_q); + } + return true; + } + if (cell->type == "$_BUF_" || cell->type == "$equiv") { std::vector a = importDefSigSpec(cell->getPort("\\A"), timestep); From da56a5bbc60e58c305227105b68654264738c241 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 27 Jul 2016 16:11:37 +0200 Subject: [PATCH 5/5] Added $initstate support to smtbmc flow --- backends/smt2/smt2.cc | 15 ++++++++++++++- backends/smt2/smtbmc.py | 3 +++ examples/smtbmc/demo1.v | 3 ++- 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 02d6f3fb..584a1df1 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -49,6 +49,7 @@ struct Smt2Worker regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0) { decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module))); + decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", log_id(module), log_id(module))); for (auto cell : module->cells()) for (auto &conn : cell->connections()) { @@ -324,6 +325,16 @@ struct Smt2Worker exported_cells.insert(cell); recursive_cells.insert(cell); + if (cell->type == "$initstate") + { + SigBit bit = sigmap(cell->getPort("\\Y").as_bit()); + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n", + log_id(module), idcounter, log_id(module), log_id(module), log_signal(bit))); + register_bool(bit, idcounter++); + recursive_cells.erase(cell); + return; + } + if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") { registers.insert(cell); @@ -755,7 +766,9 @@ struct Smt2Backend : public Backend { log("the assumptions in the module.\n"); log("\n"); log("The '_i' function evaluates to 'true' when the given state conforms\n"); - log("to the initial state.\n"); + log("to the initial state. Furthermore the '_is' function should be asserted\n"); + log("to be true for initial states in addition to '_i', and should be\n"); + log("asserted to be false for non-initial states.\n"); log("\n"); log("For hierarchical designs, the '_h' function must be asserted for each\n"); log("state to establish the design hierarchy. The '_h ' function\n"); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index f74908f8..0e94a167 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -130,6 +130,7 @@ if tempind: smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (%s_h s%d))" % (topmod, step)) + smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) if step == num_steps: smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) @@ -172,9 +173,11 @@ else: # not tempind if step == 0: smt.write("(assert (%s_i s0))" % (topmod)) + smt.write("(assert (%s_is s0))" % (topmod)) else: smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step)) + smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) if step < skip_steps: if assume_skipped is not None and step >= assume_skipped: diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v index 2e628b7d..b1e505bd 100644 --- a/examples/smtbmc/demo1.v +++ b/examples/smtbmc/demo1.v @@ -1,5 +1,5 @@ module demo1(input clk, input addtwo, output iseven); - reg [3:0] cnt = 0; + reg [3:0] cnt; wire [3:0] next_cnt; inc inc_inst (addtwo, iseven, cnt, next_cnt); @@ -8,6 +8,7 @@ module demo1(input clk, input addtwo, output iseven); cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt; assert property (cnt != 15); + initial assume (!cnt[3] && !cnt[0]); // initial predict ((iseven && addtwo) || cnt == 9); endmodule