Use SVA label in smt export if available

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

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 2fb6d4da9c5258743274fda0ea8e66c69ee12f7a..a26bff57b05f29b0ce685f4a9c7d23efe63d0dfc 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -554,7 +554,9 @@ struct Smt2Worker
 
                        if (cell->type.in("$shift", "$shiftx")) {
                                if (cell->getParam("\\B_SIGNED").as_bool()) {
-                                       /* FIXME */
+                                       return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+                                                       "(bvlshr A B) (bvlshr A (bvneg B)))",
+                                                       GetSize(cell->getPort("\\B")), 0), 's');
                                } else {
                                        return export_bvop(cell, "(bvlshr A B)", 's');
                                }
@@ -766,7 +768,7 @@ struct Smt2Worker
 
                        if (statebv)
                                makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
-                       if (statedt)
+                       else if (statedt)
                                dtmembers.push_back(stringf("  (|%s_h %s| |%s_s|)\n",
                                                get_id(module), get_id(cell->name), get_id(cell->type)));
                        else
@@ -885,8 +887,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",
@@ -1101,20 +1103,27 @@ struct Smt2Worker
                                                        break;
 
                                                Const initword = init_data.extract(i*width, width, State::Sx);
+                                               Const initmask = initword;
                                                bool gen_init_constr = false;
 
-                                               for (auto bit : initword.bits)
-                                                       if (bit == State::S0 || bit == State::S1)
+                                               for (int k = 0; k < GetSize(initword); k++) {
+                                                       if (initword[k] == State::S0 || initword[k] == State::S1) {
                                                                gen_init_constr = true;
+                                                               initmask[k] = State::S1;
+                                                       } else {
+                                                               initmask[k] = State::S0;
+                                                               initword[k] = State::S0;
+                                                       }
+                                               }
 
                                                if (gen_init_constr)
                                                {
                                                        if (statebv)
                                                                /* FIXME */;
                                                        else
-                                                               init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+                                                               init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
                                                                                get_id(module), arrayid, Const(i, abits).as_string().c_str(),
-                                                                               initword.as_string().c_str(), get_id(cell), i));
+                                                                               initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
                                                }
                                        }
                                }
@@ -1251,7 +1260,7 @@ struct Smt2Worker
 
 struct Smt2Backend : public Backend {
        Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
-       virtual void help()
+       void help() YS_OVERRIDE
        {
                //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
                log("\n");
@@ -1407,7 +1416,7 @@ struct Smt2Backend : public Backend {
                log("from non-zero to zero in the test design.\n");
                log("\n");
        }
-       virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+       void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
        {
                std::ifstream template_f;
                bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;