Add "setundef -anyseq"

kernel/rtlil.h

@@ -911,7 +911,7 @@ public:
 	std::vector<RTLIL::IdString> ports;
 	void fixup_ports();
 
-	template<typename T> void rewrite_sigspecs(T functor);
+	template<typename T> void rewrite_sigspecs(T &functor);
 	void cloneInto(RTLIL::Module *new_mod) const;
 	virtual RTLIL::Module *clone() const;
 
@@ -1201,7 +1201,7 @@ public:
 				module->design->module(type)->get_bool_attribute("\\keep"));
 	}
 
-	template<typename T> void rewrite_sigspecs(T functor);
+	template<typename T> void rewrite_sigspecs(T &functor);
 };
 
 struct RTLIL::CaseRule
@@ -1213,7 +1213,7 @@ struct RTLIL::CaseRule
 	~CaseRule();
 	void optimize();
 
-	template<typename T> void rewrite_sigspecs(T functor);
+	template<typename T> void rewrite_sigspecs(T &functor);
 	RTLIL::CaseRule *clone() const;
 };
 
@@ -1224,7 +1224,7 @@ struct RTLIL::SwitchRule : public RTLIL::AttrObject
 
 	~SwitchRule();
 
-	template<typename T> void rewrite_sigspecs(T functor);
+	template<typename T> void rewrite_sigspecs(T &functor);
 	RTLIL::SwitchRule *clone() const;
 };
 
@@ -1234,7 +1234,7 @@ struct RTLIL::SyncRule
 	RTLIL::SigSpec signal;
 	std::vector<RTLIL::SigSig> actions;
 
-	template<typename T> void rewrite_sigspecs(T functor);
+	template<typename T> void rewrite_sigspecs(T &functor);
 	RTLIL::SyncRule *clone() const;
 };
 
@@ -1246,7 +1246,7 @@ struct RTLIL::Process : public RTLIL::AttrObject
 
 	~Process();
 
-	template<typename T> void rewrite_sigspecs(T functor);
+	template<typename T> void rewrite_sigspecs(T &functor);
 	RTLIL::Process *clone() const;
 };
 
@@ -1295,7 +1295,7 @@ inline RTLIL::SigBit::SigBit(const RTLIL::SigSpec &sig) {
 }
 
 template<typename T>
-void RTLIL::Module::rewrite_sigspecs(T functor)
+void RTLIL::Module::rewrite_sigspecs(T &functor)
 {
 	for (auto &it : cells_)
 		it.second->rewrite_sigspecs(functor);
@@ -1308,13 +1308,13 @@ void RTLIL::Module::rewrite_sigspecs(T functor)
 }
 
 template<typename T>
-void RTLIL::Cell::rewrite_sigspecs(T functor) {
+void RTLIL::Cell::rewrite_sigspecs(T &functor) {
 	for (auto &it : connections_)
 		functor(it.second);
 }
 
 template<typename T>
-void RTLIL::CaseRule::rewrite_sigspecs(T functor) {
+void RTLIL::CaseRule::rewrite_sigspecs(T &functor) {
 	for (auto &it : compare)
 		functor(it);
 	for (auto &it : actions) {
@@ -1326,7 +1326,7 @@ void RTLIL::CaseRule::rewrite_sigspecs(T functor) {
 }
 
 template<typename T>
-void RTLIL::SwitchRule::rewrite_sigspecs(T functor)
+void RTLIL::SwitchRule::rewrite_sigspecs(T &functor)
 {
 	functor(signal);
 	for (auto it : cases)
@@ -1334,7 +1334,7 @@ void RTLIL::SwitchRule::rewrite_sigspecs(T functor)
 }
 
 template<typename T>
-void RTLIL::SyncRule::rewrite_sigspecs(T functor)
+void RTLIL::SyncRule::rewrite_sigspecs(T &functor)
 {
 	functor(signal);
 	for (auto &it : actions) {
@@ -1344,7 +1344,7 @@ void RTLIL::SyncRule::rewrite_sigspecs(T functor)
 }
 
 template<typename T>
-void RTLIL::Process::rewrite_sigspecs(T functor)
+void RTLIL::Process::rewrite_sigspecs(T &functor)
 {
 	root_case.rewrite_sigspecs(functor);
 	for (auto it : syncs)

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;

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();