Add "write_btor -s" mode

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 56d17c6e91f2e7392dfd104a173463d3f5764b93..b5e6ae96c7bf9dba1c2ed72ec3af587d5590116a 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -33,6 +33,7 @@ struct BtorWorker
        SigMap sigmap;
        RTLIL::Module *module;
        bool verbose;
+       bool single_bad;
 
        int next_nid = 1;
        int initstate_nid = -1;
@@ -63,6 +64,7 @@ struct BtorWorker
 
        pool<Cell*> cell_recursion_guard;
        pool<string> output_symbols;
+       vector<int> bad_properties;
        dict<SigBit, bool> initbits;
        string indent;
 
@@ -705,8 +707,8 @@ struct BtorWorker
                return nid;
        }
 
-       BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
-                       f(f), sigmap(module), module(module), verbose(verbose)
+       BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad) :
+                       f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad)
        {
                btorf_push("inputs");
 
@@ -789,11 +791,16 @@ struct BtorWorker
                                int nid_en = get_sig_nid(cell->getPort("\\EN"));
                                int nid_not_a = next_nid++;
                                int nid_en_and_not_a = next_nid++;
-                               int nid = next_nid++;
 
                                btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
                                btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
-                               btorf("%d bad %d\n", nid, nid_en_and_not_a);
+
+                               if (single_bad) {
+                                       bad_properties.push_back(nid_en_and_not_a);
+                               } else {
+                                       int nid = next_nid++;
+                                       btorf("%d bad %d\n", nid, nid_en_and_not_a);
+                               }
 
                                btorf_pop(log_id(cell));
                        }
@@ -817,6 +824,36 @@ struct BtorWorker
                                btorf_pop(stringf("next %s", log_id(it.second)));
                        }
                }
+
+               while (!bad_properties.empty())
+               {
+                       vector<int> todo;
+                       bad_properties.swap(todo);
+
+                       int sid = get_bv_sid(1);
+                       int cursor = 0;
+
+                       while (cursor+1 < GetSize(todo))
+                       {
+                               int nid_a = todo[cursor++];
+                               int nid_b = todo[cursor++];
+                               int nid = next_nid++;
+
+                               bad_properties.push_back(nid);
+                               btorf("%d or %d %d %d\n", nid, sid, nid_a, nid_b);
+                       }
+
+                       if (!bad_properties.empty()) {
+                               if (cursor < GetSize(todo))
+                                       bad_properties.push_back(todo[cursor++]);
+                               log_assert(cursor == GetSize(todo));
+                       } else {
+                               int nid = next_nid++;
+                               log_assert(cursor == 0);
+                               log_assert(GetSize(todo) == 1);
+                               btorf("%d bad %d\n", nid, todo[cursor]);
+                       }
+               }
        }
 };
 
@@ -833,10 +870,13 @@ struct BtorBackend : public Backend {
                log("  -v\n");
                log("    Add comments and indentation to BTOR output file\n");
                log("\n");
+               log("  -s\n");
+               log("    Output only a single bad property for all asserts\n");
+               log("\n");
        }
        virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
        {
-               bool verbose = false;
+               bool verbose = false, single_bad = false;
 
                log_header(design, "Executing BTOR backend.\n");
 
@@ -847,6 +887,10 @@ struct BtorBackend : public Backend {
                                verbose = true;
                                continue;
                        }
+                       if (args[argidx] == "-s") {
+                               single_bad = true;
+                               continue;
+                       }
                        break;
                }
                extra_args(f, filename, args, argidx);
@@ -859,7 +903,7 @@ struct BtorBackend : public Backend {
                *f << stringf("; BTOR description generated by %s for module %s.\n",
                                yosys_version_str, log_id(topmod));
 
-               BtorWorker(*f, topmod, verbose);
+               BtorWorker(*f, topmod, verbose, single_bad);
 
                *f << stringf("; end of yosys output\n");
        }