Merge remote-tracking branch 'origin/master' into eddie/cleanup

[yosys.git] / backends / smt2 / smt2.cc

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 7f3cc94cadbcb33063f248306ffe8b078c6b3aab..db849882e734501cf9f254a6486b77d96e2b31bb 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -416,6 +416,7 @@ struct Smt2Worker
                for (char ch : expr) {
                        if (ch == 'A') processed_expr += get_bv(sig_a);
                        else if (ch == 'B') processed_expr += get_bv(sig_b);
+                       else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
                        else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
                        else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
                        else processed_expr += ch;
@@ -509,6 +510,7 @@ struct Smt2Worker
                if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
                if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
                if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
+               if (cell->type == "$_NMUX_") return export_gate(cell, "(not (ite S B A))");
                if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
                if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
                if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
@@ -554,7 +556,7 @@ struct Smt2Worker
 
                        if (cell->type.in("$shift", "$shiftx")) {
                                if (cell->getParam("\\B_SIGNED").as_bool()) {
-                                       return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+                                       return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
                                                        "(bvlshr A B) (bvlshr A (bvneg B)))",
                                                        GetSize(cell->getPort("\\B")), 0), 's');
                                } else {
@@ -599,7 +601,7 @@ struct Smt2Worker
                        if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
                        if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
 
-                       if (cell->type == "$mux" || cell->type == "$pmux")
+                       if (cell->type.in("$mux", "$pmux"))
                        {
                                int width = GetSize(cell->getPort("\\Y"));
                                std::string processed_expr = get_bv(cell->getPort("\\A"));
@@ -887,8 +889,8 @@ struct Smt2Worker
 
                                string name_a = get_bool(cell->getPort("\\A"));
                                string name_en = get_bool(cell->getPort("\\EN"));
-                               decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
-                                               cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+                               string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+                               decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
 
                                if (cell->type == "$cover")
                                        decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1542,7 +1544,7 @@ struct Smt2Backend : public Backend {
 
                for (auto module : sorted_modules)
                {
-                       if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
+                       if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn())
                                continue;
 
                        log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));