From 546de7fa4fbd1b54e125fac06b588dbecfb033e0 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 13 Dec 2017 00:15:44 +0100
Subject: [PATCH] Add "write_btor -s" mode

---
 backends/btor/btor.cc | 56 ++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 50 insertions(+), 6 deletions(-)

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 56d17c6e9..b5e6ae96c 100644
--- 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");
 	}
-- 
2.30.2