From b6aca1d7435ebd1cb37fe777a8b8d9564b859a50 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 7 Mar 2022 13:59:36 +0100 Subject: btor2 witness co-simulation --- passes/sat/sim.cc | 131 ++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 123 insertions(+), 8 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index d15ae9b57..c669247e8 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -961,7 +961,7 @@ struct SimWorker : SimShared } } - void run_cosim(Module *topmod, int numcycles) + void run_cosim_fst(Module *topmod, int numcycles) { log_assert(top == nullptr); fst = new FstData(sim_filename); @@ -1092,7 +1092,7 @@ struct SimWorker : SimShared delete fst; } - void run_cosim_witness(Module *topmod) + void run_cosim_aiger_witness(Module *topmod) { log_assert(top == nullptr); std::ifstream mf(map_filename); @@ -1183,6 +1183,105 @@ struct SimWorker : SimShared register_output_step(10*cycle); write_output_files(); } + + std::vector split(std::string text, const char *delim) + { + std::vector list; + char *p = strdup(text.c_str()); + char *t = strtok(p, delim); + while (t != NULL) { + list.push_back(t); + t = strtok(NULL, delim); + } + free(p); + return list; + } + + std::string signal_name(std::string const & name) + { + size_t pos = name.find_first_of("@"); + if (pos==std::string::npos) { + pos = name.find_first_of("#"); + if (pos==std::string::npos) + log_error("Line does not contain proper signal name `%s`\n", name.c_str()); + } + return name.substr(0, pos); + } + + void run_cosim_btor2_witness(Module *topmod) + { + log_assert(top == nullptr); + 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()); + + int state = 0; + int cycle = 0; + top = new SimInstance(this, scope, topmod); + register_signals(); + int prev_cycle = 0; + int curr_cycle = 0; + std::vector parts; + while (!f.eof()) + { + std::string line; + std::getline(f, line); + if (line.size()==0) continue; + + if (line[0]=='#' || line[0]=='@' || line[0]=='.') { + if (line[0]!='.') + curr_cycle = atoi(line.c_str()+1); + else + curr_cycle = -1; // force detect change + + if (curr_cycle != prev_cycle) { + log("Simulating cycle %d %d.\n", cycle, cycle % 1); + set_inports(clock, State::S1); + 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); + cycle++; + prev_cycle = curr_cycle; + } + if (line[0]=='.') break; + continue; + } + + switch(state) + { + case 0: + if (line=="sat") + state = 1; + break; + case 1: + if (line[0]=='b' || line[0]=='j') + state = 2; + else + log_error("Line does not contain property.\n"); + break; + default: // set state or inputs + parts = split(line, " "); + if (parts.size()!=3) + log_error("Invalid set state line content.\n"); + + RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[2])); + Wire *w = topmod->wire(escaped_s); + if (!w) + log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(topmod)); + if ((int)parts[1].size() != w->width) + log_error("Size of wire %s is different than provided data.\n", log_signal(w)); + + top->set_state(w, Const(parts[1])); + break; + } + } + write_output_files(); + } }; struct VCDWriter : public OutputWriter @@ -1318,7 +1417,7 @@ struct AIWWriter : public OutputWriter RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); Wire *w = worker->top->module->wire(escaped_s); if (!w) - log_error("Wire %s not present in module %s\n",log_signal(w),log_id(worker->top->module)); + log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(worker->top->module)); 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") { @@ -1483,6 +1582,13 @@ struct SimPass : public Pass { log(" enable debug output\n"); log("\n"); } + + + static std::string file_base_name(std::string const & path) + { + return path.substr(path.find_last_of("/\\") + 1); + } + void execute(std::vector args, RTLIL::Design *design) override { SimWorker worker; @@ -1632,11 +1738,20 @@ struct SimPass : public Pass { if (worker.sim_filename.empty()) worker.run(top_mod, numcycles); - else - if (worker.map_filename.empty()) - worker.run_cosim(top_mod, numcycles); - else - worker.run_cosim_witness(top_mod); + else { + std::string filename_trim = file_base_name(worker.sim_filename); + if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) { + worker.run_cosim_fst(top_mod, numcycles); + } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) { + if (worker.map_filename.empty()) + log_cmd_error("For AIGER witness file map parameter is mandatory.\n"); + worker.run_cosim_aiger_witness(top_mod); + } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) { + worker.run_cosim_btor2_witness(top_mod); + } else { + log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); + } + } } } SimPass; -- cgit v1.2.3 From 1b1ecd4ab0c3924d1acbaa0ccc22bd1933cb347c Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 7 Mar 2022 15:00:14 +0100 Subject: Error checks for aiger witness --- passes/sat/sim.cc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index c669247e8..9771e83f3 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1099,6 +1099,8 @@ struct SimWorker : SimShared std::string type, symbol; int variable, index; dict> inputs, inits, latches; + if (mf.fail()) + log_cmd_error("Not able to read AIGER witness map file.\n"); while (mf >> type >> variable >> index >> symbol) { RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); Wire *w = topmod->wire(escaped_s); @@ -1410,9 +1412,14 @@ struct AIWWriter : public OutputWriter void write(std::map &) override { if (!aiwfile.is_open()) return; + if (worker->map_filename.empty()) + log_cmd_error("For AIGER witness file map parameter is mandatory.\n"); + std::ifstream mf(worker->map_filename); std::string type, symbol; int variable, index; + if (mf.fail()) + log_cmd_error("Not able to read AIGER witness map file.\n"); while (mf >> type >> variable >> index >> symbol) { RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); Wire *w = worker->top->module->wire(escaped_s); -- cgit v1.2.3 From ede348cdc285f4b4f1c53942d515a7082e53e37a Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 7 Mar 2022 16:32:32 +0100 Subject: cleanup --- 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 9771e83f3..d7f4de507 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1238,7 +1238,7 @@ struct SimWorker : SimShared curr_cycle = -1; // force detect change if (curr_cycle != prev_cycle) { - log("Simulating cycle %d %d.\n", cycle, cycle % 1); + log("Simulating cycle %d.\n", cycle); set_inports(clock, State::S1); set_inports(clockn, State::S0); update(); @@ -1282,6 +1282,7 @@ struct SimWorker : SimShared break; } } + register_output_step(10*cycle); write_output_files(); } }; -- cgit v1.2.3 From f37ac5d934e76c12d7412451d45ded7a7df04b82 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 9 Mar 2022 09:48:29 +0100 Subject: Fixes and error check --- passes/sat/sim.cc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index d7f4de507..79140e615 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1095,6 +1095,8 @@ struct SimWorker : SimShared void run_cosim_aiger_witness(Module *topmod) { log_assert(top == nullptr); + if ((clock.size()+clockn.size())==0) + log_error("Clock signal must be specified.\n"); std::ifstream mf(map_filename); std::string type, symbol; int variable, index; @@ -1213,6 +1215,8 @@ struct SimWorker : SimShared void run_cosim_btor2_witness(Module *topmod) { log_assert(top == nullptr); + if ((clock.size()+clockn.size())==0) + log_error("Clock signal must be specified.\n"); std::ifstream f; f.open(sim_filename.c_str()); if (f.fail() || GetSize(sim_filename) == 0) @@ -1278,7 +1282,7 @@ struct SimWorker : SimShared if ((int)parts[1].size() != w->width) log_error("Size of wire %s is different than provided data.\n", log_signal(w)); - top->set_state(w, Const(parts[1])); + top->set_state(w, Const::from_string(parts[1])); break; } } -- cgit v1.2.3 From 295b0d1899a6224405c28d81e52b62f32ea34b08 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 9 Mar 2022 18:34:02 +0100 Subject: Start work on memory init --- passes/sat/sim.cc | 43 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 34 insertions(+), 9 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 79140e615..823456e94 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1229,6 +1229,12 @@ struct SimWorker : SimShared int prev_cycle = 0; int curr_cycle = 0; std::vector parts; + size_t len = 0; + dict mem_dict; + for (auto &mem : top->memories) { + mem.narrow(); + mem_dict[mem.memid] = &mem; + } while (!f.eof()) { std::string line; @@ -1272,17 +1278,36 @@ struct SimWorker : SimShared break; default: // set state or inputs parts = split(line, " "); - if (parts.size()!=3) + len = parts.size(); + if (len<3 || len>4) log_error("Invalid set state line content.\n"); - RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[2])); - Wire *w = topmod->wire(escaped_s); - if (!w) - log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(topmod)); - if ((int)parts[1].size() != w->width) - log_error("Size of wire %s is different than provided data.\n", log_signal(w)); - - top->set_state(w, Const::from_string(parts[1])); + RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1])); + if (len==3) { + Wire *w = topmod->wire(escaped_s); + if (!w) + log_warning("Wire %s not present in module %s\n",log_id(escaped_s),log_id(topmod)); + if (w && (int)parts[1].size() != w->width) + log_error("Size of wire %s is different than provided data.\n", log_signal(w)); + if (w) + top->set_state(w, Const::from_string(parts[1])); + } else { + Cell *c = topmod->cell(escaped_s); + if (!c) + log_error("Cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod)); + if (!c->is_mem_cell()) + log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod)); + + Mem *mem = mem_dict[c->parameters.at(ID::MEMID).decode_string()]; + mem->clear_inits(); + MemInit minit; + minit.addr = Const::from_string(parts[1].substr(1,parts[1].size()-2)); + minit.data = Const::from_string(parts[2]); + log("[%s] = %s\n",log_signal(minit.addr), log_signal(minit.data)); + minit.en = Const(State::S1, mem->width); + mem->inits.push_back(minit); + mem->emit(); + } break; } } -- cgit v1.2.3 From 357336339a3d7f4100d44c508cd5fe5255b53218 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 11 Mar 2022 11:19:53 +0100 Subject: Proper write of memory data --- passes/sat/sim.cc | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 823456e94..e49f895f7 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -326,6 +326,16 @@ struct SimInstance return did_something; } + void set_memory_state(IdString memid, Const addr, Const data) + { + auto &state = mem_database[memid]; + + int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width; + for (int i = 0; i < GetSize(data); i++) + if (0 <= i+offset && i+offset < GetSize(data)) + state.data.bits[i+offset] = data.bits[i]; + } + void update_cell(Cell *cell) { if (ff_database.count(cell)) @@ -1230,11 +1240,6 @@ struct SimWorker : SimShared int curr_cycle = 0; std::vector parts; size_t len = 0; - dict mem_dict; - for (auto &mem : top->memories) { - mem.narrow(); - mem_dict[mem.memid] = &mem; - } while (!f.eof()) { std::string line; @@ -1298,15 +1303,9 @@ struct SimWorker : SimShared if (!c->is_mem_cell()) log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod)); - Mem *mem = mem_dict[c->parameters.at(ID::MEMID).decode_string()]; - mem->clear_inits(); - MemInit minit; - minit.addr = Const::from_string(parts[1].substr(1,parts[1].size()-2)); - minit.data = Const::from_string(parts[2]); - log("[%s] = %s\n",log_signal(minit.addr), log_signal(minit.data)); - minit.en = Const(State::S1, mem->width); - mem->inits.push_back(minit); - mem->emit(); + Const addr = Const::from_string(parts[1].substr(1,parts[1].size()-2)); + Const data = Const::from_string(parts[2]); + top->set_memory_state(c->parameters.at(ID::MEMID).decode_string(), addr, data); } break; } -- cgit v1.2.3 From ebe2ee431eb452e24f833f3bf52a13a8a330a2c3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 11 Mar 2022 14:04:02 +0100 Subject: handle state names of $anyconst and $anyseq --- backends/btor/btor.cc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index d62cc4c3d..e0283da8a 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -678,7 +678,11 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig_y)); int nid = next_nid++; - btorf("%d state %d\n", nid, sid); + btorf("%d state %d", nid, sid); + if (sig_y.is_wire() && sig_y.as_wire()->name.c_str()[0]!='$') + btorf(" %s\n", log_id(sig_y.as_wire())); + else + btorf("\n"); if (cell->type == ID($anyconst)) { int nid2 = next_nid++; -- cgit v1.2.3 From d340f302f6255b6aedcf8351a6374b34889edbbc Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Fri, 11 Mar 2022 14:21:12 +0100 Subject: Fix handling of some formal cells in btor back-end Signed-off-by: Claire Xenia Wolf --- backends/btor/btor.cc | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index e0283da8a..73e88c049 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -678,11 +678,7 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig_y)); int nid = next_nid++; - btorf("%d state %d", nid, sid); - if (sig_y.is_wire() && sig_y.as_wire()->name.c_str()[0]!='$') - btorf(" %s\n", log_id(sig_y.as_wire())); - else - btorf("\n"); + btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str()); if (cell->type == ID($anyconst)) { int nid2 = next_nid++; @@ -703,7 +699,7 @@ struct BtorWorker int one_nid = get_sig_nid(State::S1); int zero_nid = get_sig_nid(State::S0); initstate_nid = next_nid++; - btorf("%d state %d\n", initstate_nid, sid); + btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str()); btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid); btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid); } -- cgit v1.2.3 From b72c779204120d53895d895d3599b4c87fc2f687 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 11 Mar 2022 15:11:14 +0100 Subject: Support cell name in btor witness file --- passes/sat/sim.cc | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index e49f895f7..5d8e44830 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1290,12 +1290,21 @@ struct SimWorker : SimShared RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1])); if (len==3) { Wire *w = topmod->wire(escaped_s); - if (!w) - log_warning("Wire %s not present in module %s\n",log_id(escaped_s),log_id(topmod)); - if (w && (int)parts[1].size() != w->width) - log_error("Size of wire %s is different than provided data.\n", log_signal(w)); - if (w) + if (!w) { + Cell *c = topmod->cell(escaped_s); + if (!c) + log_warning("Wire/cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod)); + else if (c->type.in(ID($anyconst), ID($anyseq))) { + SigSpec sig_y= c->getPort(ID::Y); + if ((int)parts[1].size() != GetSize(sig_y)) + log_error("Size of wire %s is different than provided data.\n", log_signal(sig_y)); + top->set_state(sig_y, Const::from_string(parts[1])); + } + } else { + if ((int)parts[1].size() != w->width) + log_error("Size of wire %s is different than provided data.\n", log_signal(w)); top->set_state(w, Const::from_string(parts[1])); + } } else { Cell *c = topmod->cell(escaped_s); if (!c) -- cgit v1.2.3 From 5204694123e6ac10b931ac45dbe7f4cd0b11b93b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 11 Mar 2022 15:21:36 +0100 Subject: FstData already do conversion to VCD --- 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 5d8e44830..02b859bcc 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1785,7 +1785,8 @@ struct SimPass : public Pass { worker.run(top_mod, numcycles); else { std::string filename_trim = file_base_name(worker.sim_filename); - if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) { + if (filename_trim.size() > 4 && ((filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) || + filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0)) { worker.run_cosim_fst(top_mod, numcycles); } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) { if (worker.map_filename.empty()) -- cgit v1.2.3