From: Miodrag Milanovic <mmicko@gmail.com>
Date: Fri, 22 Apr 2022 09:53:41 +0000 (+0200)
Subject: Fix multiclock for btor2 witness
X-Git-Tag: yosys-0.17~23^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fa2f3b26036499945c8a7b27d2972ebc1322e01;p=yosys.git

Fix multiclock for btor2 witness
---

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 9c431ab25..e12701817 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -1313,8 +1313,10 @@ struct SimWorker : SimShared
 	void run_cosim_btor2_witness(Module *topmod)
 	{
 		log_assert(top == nullptr);
-		if ((clock.size()+clockn.size())==0)
+		if (!multiclock && (clock.size()+clockn.size())==0)
 			log_error("Clock signal must be specified.\n");
+		if (multiclock && (clock.size()+clockn.size())>0)
+			log_error("For multiclock witness there should be no clock signal.\n");
 		std::ifstream f;
 		f.open(sim_filename.c_str());
 		if (f.fail() || GetSize(sim_filename) == 0)
@@ -1347,10 +1349,12 @@ struct SimWorker : SimShared
 					set_inports(clockn, State::S0);
 					update();
 					register_output_step(10*cycle+0);
-					set_inports(clock, State::S0);
-					set_inports(clockn, State::S1);
-					update();
-					register_output_step(10*cycle+5);
+					if (!multiclock) {
+						set_inports(clock, State::S0);
+						set_inports(clockn, State::S1);
+						update();
+						register_output_step(10*cycle+5);
+					}
 					cycle++;
 					prev_cycle = curr_cycle;
 				}