diff options
| author | Miodrag Milanovic <mmicko@gmail.com> | 2022-04-22 11:53:41 +0200 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2022-04-22 11:53:41 +0200 |
| commit | 8fa2f3b26036499945c8a7b27d2972ebc1322e01 (patch) | |
| tree | 35a7da70d6769aafc0ba7eec3e58ce4c29d6e67f /passes/sat | |
| parent | 29c0a595892f36ca8755386c448105f8e2f499d6 (diff) | |
| download | yosys-8fa2f3b26036499945c8a7b27d2972ebc1322e01.tar.gz yosys-8fa2f3b26036499945c8a7b27d2972ebc1322e01.tar.bz2 yosys-8fa2f3b26036499945c8a7b27d2972ebc1322e01.zip | |
Fix multiclock for btor2 witness
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/sim.cc | 14 |
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; } |