From 41754b4207f9c695049757955d85c6bbadbe8ac3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 18 Feb 2022 15:04:02 +0100 Subject: [PATCH 1/3] Added AIGER witness file co simulation --- passes/sat/sim.cc | 94 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 93 insertions(+), 1 deletion(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 57df0f929..c8d5adb06 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -802,6 +802,18 @@ struct SimInstance child.second->setInitState(); } + void setState(std::vector> bits, std::string values) + { + for(size_t i=0;i clock, clockn, reset, resetn; std::string timescale; std::string sim_filename; + std::string map_filename; std::string scope; ~SimWorker() @@ -1147,6 +1160,73 @@ struct SimWorker : SimShared top->writeback(wbmods); } } + + void run_cosim_witness(Module *topmod) + { + log_assert(top == nullptr); + std::ifstream mf(map_filename); + std::string type, symbol; + int variable, index; + std::vector> inputs; + std::vector> latches; + while (mf >> type >> variable >> index >> symbol) { + RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); + Wire *w = topmod->wire(escaped_s); + if (!w) + log_error("Wire %s not present in module %s\n",log_signal(w),log_id(topmod)); + if (index < w->start_offset || index > w->start_offset + w->width) + log_error("Index %d for wire %s is out of range\n", index, log_signal(w)); + if (type == "input") { + inputs.emplace_back(SigBit(w,index),false); + } else if (type == "latch") { + latches.emplace_back(SigBit(w,index),false); + } else if (type == "invlatch") { + latches.emplace_back(SigBit(w,index),true); + } + } + + std::ifstream f; + f.open(sim_filename.c_str()); + if (f.fail() || GetSize(sim_filename) == 0) + log_error("Can not open file `%s`\n", sim_filename.c_str()); + + bool init = true; + int cycle = 0; + top = new SimInstance(this, scope, topmod); + while (!f.eof()) + { + std::string line; + std::getline(f, line); + if (line.size()==0 || line[0]=='#') continue; + log("Simulating cycle %d.\n", cycle); + if (init) { + if (line.size()!=latches.size()) + log_error("Wrong number of initialization bits in file.\n"); + write_output_header(); + top->setState(latches, line); + set_inports(clock, State::S0); + set_inports(clockn, State::S1); + update(); + write_output_step(0); + init = false; + } else { + if (line.size()!=inputs.size()) + log_error("Wrong number of input data bits in file.\n"); + top->setState(inputs, line); + set_inports(clock, State::S1); + set_inports(clockn, State::S0); + update(); + write_output_step(10*cycle); + set_inports(clock, State::S0); + set_inports(clockn, State::S1); + update(); + write_output_step(10*cycle + 5); + } + cycle++; + } + write_output_step(10*cycle); + write_output_end(); + } }; struct SimPass : public Pass { @@ -1198,6 +1278,9 @@ struct SimPass : public Pass { log(" -r\n"); log(" read simulation results file (file formats supported: FST)\n"); log("\n"); + log(" -map \n"); + log(" read file with port and latch symbols, needed for AIGER witness input\n"); + log("\n"); log(" -scope\n"); log(" scope of simulation top model\n"); log("\n"); @@ -1299,6 +1382,12 @@ struct SimPass : public Pass { worker.sim_filename = sim_filename; continue; } + if (args[argidx] == "-map" && argidx+1 < args.size()) { + std::string map_filename = args[++argidx]; + rewrite_filename(map_filename); + worker.map_filename = map_filename; + continue; + } if (args[argidx] == "-scope" && argidx+1 < args.size()) { worker.scope = args[++argidx]; continue; @@ -1360,7 +1449,10 @@ struct SimPass : public Pass { if (worker.sim_filename.empty()) worker.run(top_mod, numcycles); else - worker.run_cosim(top_mod, numcycles); + if (worker.map_filename.empty()) + worker.run_cosim(top_mod, numcycles); + else + worker.run_cosim_witness(top_mod); } } SimPass; From 5f918803de539a2ef6fbfe80de4acb379c20f472 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 18 Feb 2022 15:06:49 +0100 Subject: [PATCH 2/3] Changed error message --- kernel/fstdata.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc index 1386a3300..2e1000178 100644 --- a/kernel/fstdata.cc +++ b/kernel/fstdata.cc @@ -27,7 +27,7 @@ FstData::FstData(std::string filename) : ctx(nullptr) const std::vector g_units = { "s", "ms", "us", "ns", "ps", "fs", "as", "zs" }; ctx = (fstReaderContext *)fstReaderOpen(filename.c_str()); if (!ctx) - log_error("Error opening '%s'\n", filename.c_str()); + log_error("Error opening '%s' as FST file\n", filename.c_str()); int scale = (int)fstReaderGetTimescale(ctx); timescale = pow(10.0, scale); timescale_str = ""; From 1aa9ad25d0c062e2202b81de4193b161984e83fb Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Fri, 18 Feb 2022 16:27:41 +0100 Subject: [PATCH 3/3] Fix cycle 0 in aiger witness co-simulation Signed-off-by: Claire Xenia Wolf --- passes/sat/sim.cc | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index c8d5adb06..9ee5d219c 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1198,31 +1198,34 @@ struct SimWorker : SimShared std::string line; std::getline(f, line); if (line.size()==0 || line[0]=='#') continue; - log("Simulating cycle %d.\n", cycle); if (init) { if (line.size()!=latches.size()) log_error("Wrong number of initialization bits in file.\n"); write_output_header(); top->setState(latches, line); - set_inports(clock, State::S0); - set_inports(clockn, State::S1); - update(); - write_output_step(0); init = false; } else { + log("Simulating cycle %d.\n", cycle); if (line.size()!=inputs.size()) log_error("Wrong number of input data bits in file.\n"); top->setState(inputs, line); - set_inports(clock, State::S1); - set_inports(clockn, State::S0); + if (cycle) { + set_inports(clock, State::S1); + set_inports(clockn, State::S0); + } else { + set_inports(clock, State::S0); + set_inports(clockn, State::S1); + } update(); write_output_step(10*cycle); - set_inports(clock, State::S0); - set_inports(clockn, State::S1); - update(); - write_output_step(10*cycle + 5); + if (cycle) { + set_inports(clock, State::S0); + set_inports(clockn, State::S1); + update(); + write_output_step(10*cycle + 5); + } + cycle++; } - cycle++; } write_output_step(10*cycle); write_output_end();