aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--passes/sat/sim.cc14
1 files changed, 9 insertions, 5 deletions
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;
}