From 8fa2f3b26036499945c8a7b27d2972ebc1322e01 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 11:53:41 +0200 Subject: [PATCH 1/8] Fix multiclock for btor2 witness --- passes/sat/sim.cc | 14 +++++++++----- 1 file 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; } From 75032a565d22506ae7910bfa00e2b71558a30e26 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 11:57:39 +0200 Subject: [PATCH 2/8] Set init state for all wires from FST and set past --- passes/sat/sim.cc | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index e12701817..967f7f227 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -782,22 +782,21 @@ struct SimInstance bool setInitState() { bool did_something = false; + for(auto &item : fst_handles) { + if (item.second==0) continue; // Ignore signals not found + std::string v = shared->fst->valueOf(item.second); + did_something |= set_state(item.first, Const::from_string(v)); + } for (auto &it : ff_database) { ff_state_t &ff = it.second; - SigSpec qsig = it.second.data.sig_q; - if (qsig.is_wire()) { - IdString name = qsig.as_wire()->name; - fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(name)); - if (id==0 && name.isPublic()) - log_warning("Unable to find wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(name)).c_str()); - if (id!=0) { - Const fst_val = Const::from_string(shared->fst->valueOf(id)); - ff.past_d = fst_val; - if (ff.data.has_aload) - ff.past_ad = fst_val; - did_something = set_state(qsig, fst_val); - } + SigSpec dsig = it.second.data.sig_d; + Const value = get_state(dsig); + if (dsig.is_wire()) { + ff.past_d = value; + if (ff.data.has_aload) + ff.past_ad = value; + did_something |= true; } } for (auto child : children) From c989adcc2d466bb3e2e83cf67ad0a193f6628fa6 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 12:03:39 +0200 Subject: [PATCH 3/8] If not multiclock, output only on clock edges --- passes/sat/sim.cc | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 967f7f227..73e03067b 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1782,6 +1782,12 @@ struct AIWWriter : public OutputWriter log_error("Index %d for wire %s is out of range\n", index, log_signal(w)); if (type == "input") { aiw_inputs[variable] = SigBit(w,index-w->start_offset); + if (worker->clock.count(escaped_s)) { + clocks[variable] = true; + } + if (worker->clockn.count(escaped_s)) { + clocks[variable] = false; + } } else if (type == "init") { aiw_inits[variable] = SigBit(w,index-w->start_offset); } else if (type == "latch") { @@ -1823,6 +1829,17 @@ struct AIWWriter : public OutputWriter first = false; } + bool skip = false; + for (auto it : clocks) + { + auto val = it.second ? State::S1 : State::S0; + SigBit bit = aiw_inputs.at(it.first); + auto v = current[mapping[bit.wire]].bits.at(bit.offset); + if (v == val) + skip = true; + } + if (skip) + continue; for (int i = 0;; i++) { if (aiw_inputs.count(i)) { @@ -1852,6 +1869,7 @@ struct AIWWriter : public OutputWriter std::ofstream aiwfile; dict> aiw_latches; dict aiw_inputs, aiw_inits; + dict clocks; std::map mapping; }; From 83cad82b295255d59e2162d599bbd4485b688c6a Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 12:04:05 +0200 Subject: [PATCH 4/8] latches are always set to zero --- passes/sat/sim.cc | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 73e03067b..f480168bd 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1815,12 +1815,7 @@ struct AIWWriter : public OutputWriter for (int i = 0;; i++) { if (aiw_latches.count(i)) { - SigBit bit = aiw_latches.at(i).first; - auto v = current[mapping[bit.wire]].bits.at(bit.offset); - if (v == State::S1) - aiwfile << (aiw_latches.at(i).second ? '0' : '1'); - else - aiwfile << (aiw_latches.at(i).second ? '1' : '0'); + aiwfile << '0'; continue; } aiwfile << '\n'; From 33f4009bb559eefaabd19b3dde06639889eb1eed Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 13:46:11 +0200 Subject: [PATCH 5/8] Last sample from input does not represent change --- passes/sat/sim.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index f480168bd..345ca3494 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1805,8 +1805,9 @@ struct AIWWriter : public OutputWriter std::map current; bool first = true; - for(auto& d : worker->output_data) + for (auto iter = worker->output_data.begin(); iter != std::prev(worker->output_data.end()); ++iter) { + auto& d = *iter; for (auto &data : d.second) { current[data.first] = data.second; From 9c7deabf9476939e0766fe6bd69b9a7adfeeb48b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 15:24:02 +0200 Subject: [PATCH 6/8] Ignore change on last edge --- kernel/fstdata.cc | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc index c99bc61c3..2bec58bcf 100644 --- a/kernel/fstdata.cc +++ b/kernel/fstdata.cc @@ -201,10 +201,11 @@ void FstData::reconstructAllAtTimes(std::vector &signal, uint64_t sta fstReaderSetUnlimitedTimeRange(ctx); fstReaderSetFacProcessMaskAll(ctx); fstReaderIterBlocks2(ctx, reconstruct_clb_attimes, reconstruct_clb_varlen_attimes, this, nullptr); - past_data = last_data; - callback(last_time); - if (last_time!=end_time) - callback(end_time); + if (last_time!=end_time) { + past_data = last_data; + callback(last_time); + } + callback(end_time); } std::string FstData::valueOf(fstHandle signal) From 4d80bc24c714f700519a2191a8929fe2136e45a3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 16:23:39 +0200 Subject: [PATCH 7/8] Treat $anyseq as input from FST --- passes/sat/sim.cc | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 345ca3494..5a36f87ec 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -804,6 +804,25 @@ struct SimInstance return did_something; } + void addAdditionalInputs(std::map &inputs) + { + for (auto cell : module->cells()) + { + if (cell->type.in(ID($anyseq))) { + SigSpec sig_y= cell->getPort(ID::Y); + if (sig_y.is_wire()) { + Wire *wire = sig_y.as_wire(); + fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name)); + if (id==0) + log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str()); + inputs[wire] = id; + } + } + } + for (auto child : children) + child.second->addAdditionalInputs(inputs); + } + void setState(dict> bits, std::string values) { for(auto bit : bits) { @@ -1065,6 +1084,8 @@ struct SimWorker : SimShared } } + top->addAdditionalInputs(inputs); + uint64_t startCount = 0; uint64_t stopCount = 0; if (start_time==0) { From bbfdea2f8a200f40f82600b48afddb66e5f0e1d2 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 22 Apr 2022 17:20:17 +0200 Subject: [PATCH 8/8] Match $anyseq input if connected to public wire --- passes/sat/sim.cc | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 5a36f87ec..5f795e94c 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -809,13 +809,19 @@ struct SimInstance for (auto cell : module->cells()) { if (cell->type.in(ID($anyseq))) { - SigSpec sig_y= cell->getPort(ID::Y); + SigSpec sig_y = sigmap(cell->getPort(ID::Y)); if (sig_y.is_wire()) { - Wire *wire = sig_y.as_wire(); - fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name)); - if (id==0) - log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str()); - inputs[wire] = id; + bool found = false; + for(auto &item : fst_handles) { + if (item.second==0) continue; // Ignore signals not found + if (sig_y == sigmap(item.first)) { + inputs[sig_y.as_wire()] = item.second; + found = true; + break; + } + } + if (!found) + log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(sig_y.as_wire()->name)).c_str()); } } }