Add "setundef -anyseq"

2 files changed, 44 insertions, 3 deletions

diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index 03a5a123f..9827ac0b1 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -30,6 +30,7 @@ struct SetundefWorker
 {
 	int next_bit_mode;
 	uint32_t next_bit_state;
+	vector<SigSpec*> siglist;
 
 	RTLIL::State next_bit()
 	{
@@ -50,6 +51,11 @@ struct SetundefWorker
 
 	void operator()(RTLIL::SigSpec &sig)
 	{
+		if (next_bit_mode == 2) {
+			siglist.push_back(&sig);
+			return;
+		}
+
 		for (auto &bit : sig)
 			if (bit.wire == NULL && bit.data > RTLIL::State::S1)
 				bit = next_bit();
@@ -75,6 +81,9 @@ struct SetundefPass : public Pass {
 		log("    -one\n");
 		log("        replace with bits set (1)\n");
 		log("\n");
+		log("    -anyseq\n");
+		log("        replace with $anyseq drivers (for formal)\n");
+		log("\n");
 		log("    -random <seed>\n");
 		log("        replace with random bits using the specified integer als seed\n");
 		log("        value for the random number generator.\n");
@@ -109,13 +118,18 @@ struct SetundefPass : public Pass {
 				worker.next_bit_mode = 1;
 				continue;
 			}
+			if (args[argidx] == "-anyseq") {
+				got_value = true;
+				worker.next_bit_mode = 2;
+				continue;
+			}
 			if (args[argidx] == "-init") {
 				init_mode = true;
 				continue;
 			}
 			if (args[argidx] == "-random" && !got_value && argidx+1 < args.size()) {
 				got_value = true;
-				worker.next_bit_mode = 2;
+				worker.next_bit_mode = 3;
 				worker.next_bit_state = atoi(args[++argidx].c_str()) + 1;
 				for (int i = 0; i < 10; i++)
 					worker.next_bit();
@@ -126,7 +140,7 @@ struct SetundefPass : public Pass {
 		extra_args(args, argidx, design);
 
 		if (!got_value)
-			log_cmd_error("One of the options -zero, -one, or -random <seed> must be specified.\n");
+			log_cmd_error("One of the options -zero, -one, -anyseq, or -random <seed> must be specified.\n");
 
 		for (auto module : design->selected_modules())
 		{
@@ -241,6 +255,32 @@ struct SetundefPass : public Pass {
 			}
 
 			module->rewrite_sigspecs(worker);
+
+			if (worker.next_bit_mode == 2)
+			{
+				vector<SigSpec*> siglist;
+				siglist.swap(worker.siglist);
+
+				for (auto sigptr : siglist)
+				{
+					SigSpec &sig = *sigptr;
+					int cursor = 0;
+
+					while (cursor < GetSize(sig))
+					{
+						int width = 0;
+						while (cursor+width < GetSize(sig) && sig[cursor+width] == State::Sx)
+							width++;
+
+						if (width > 0) {
+							sig.replace(cursor, module->Anyseq(NEW_ID, width));
+							cursor += width;
+						} else {
+							cursor++;
+						}
+					}
+				}
+			}
 		}
 	}
 } SetundefPass;
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 77263f6a2..a3028bfce 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -687,7 +687,8 @@ struct FreduceWorker
 		}
 
 		std::map<RTLIL::SigBit, int> bitusage;
-		module->rewrite_sigspecs(CountBitUsage(sigmap, bitusage));
+		CountBitUsage bitusage_worker(sigmap, bitusage);
+		module->rewrite_sigspecs(bitusage_worker);
 
 		if (!dump_prefix.empty())
 			dump();