riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Fix multiclock for btor2 witness

This commit is contained in:
Miodrag Milanovic 2022-04-22 11:53:41 +02:00
parent 29c0a59589
commit 8fa2f3b260
1 changed files with 9 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
passes/sat/sim.cc
View File

@ -1313,8 +1313,10 @@ struct SimWorker : SimShared
void run_cosim_btor2_witness(Module *topmod) void run_cosim_btor2_witness(Module *topmod)
{ {
log_assert(top == nullptr); 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"); 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; std::ifstream f;
f.open(sim_filename.c_str()); f.open(sim_filename.c_str());
if (f.fail() || GetSize(sim_filename) == 0) if (f.fail() || GetSize(sim_filename) == 0)
@ -1347,10 +1349,12 @@ struct SimWorker : SimShared
set_inports(clockn, State::S0); set_inports(clockn, State::S0);
update(); update();
register_output_step(10*cycle+0); register_output_step(10*cycle+0);
if (!multiclock) {
set_inports(clock, State::S0); set_inports(clock, State::S0);
set_inports(clockn, State::S1); set_inports(clockn, State::S1);
update(); update();
register_output_step(10*cycle+5); register_output_step(10*cycle+5);
}
cycle++; cycle++;
prev_cycle = curr_cycle; prev_cycle = curr_cycle;
} }