diff options
author | Claire Xenia Wolf <claire@clairexen.net> | 2022-02-28 10:50:08 +0100 |
---|---|---|
committer | Claire Xenia Wolf <claire@clairexen.net> | 2022-02-28 10:50:08 +0100 |
commit | 56b968f61c01600fde97f1b9b8e857b0f6ecd16d (patch) | |
tree | e49987a4534bd85fcb085a577ed621c8e47332d4 | |
parent | 1fd3a642c94b642624f05efecff282c195f984d1 (diff) | |
download | yosys-56b968f61c01600fde97f1b9b8e857b0f6ecd16d.tar.gz yosys-56b968f61c01600fde97f1b9b8e857b0f6ecd16d.tar.bz2 yosys-56b968f61c01600fde97f1b9b8e857b0f6ecd16d.zip |
Add writing of aiw files to "sim" command
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
-rw-r--r-- | passes/sat/sim.cc | 88 |
1 files changed, 87 insertions, 1 deletions
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 57d6182c0..304dfef13 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -857,9 +857,11 @@ struct SimInstance struct SimWorker : SimShared { SimInstance *top = nullptr; - std::ofstream vcdfile; + std::ofstream vcdfile, aiwfile; struct fstContext *fstfile = nullptr; pool<IdString> clock, clockn, reset, resetn; + dict<int, std::pair<SigBit, bool>> aiw_latches; + dict<int, SigBit> aiw_inputs, aiw_inits; std::string timescale; std::string sim_filename; std::string map_filename; @@ -916,12 +918,82 @@ struct SimWorker : SimShared top->write_fst_step(fstfile); } + void write_aiw_header() + { + std::ifstream mf(map_filename); + std::string type, symbol; + int variable, index; + while (mf >> type >> variable >> index >> symbol) { + RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); + Wire *w = top->module->wire(escaped_s); + if (!w) + log_error("Wire %s not present in module %s\n",log_signal(w),log_id(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") { + aiw_inputs[variable] = SigBit(w,index); + } else if (type == "init") { + aiw_inits[variable] = SigBit(w,index); + } else if (type == "latch") { + aiw_latches[variable] = {SigBit(w,index), false}; + } else if (type == "invlatch") { + aiw_latches[variable] = {SigBit(w,index), true}; + } + } + + for (int i = 0;; i++) + { + if (aiw_latches.count(i)) { + auto v = top->get_state(aiw_latches.at(i).first); + if (v == State::S1) + aiwfile << (aiw_latches.at(i).second ? '0' : '1'); + else + aiwfile << (aiw_latches.at(i).second ? '1' : '0'); + continue; + } + aiwfile << '\n'; + break; + } + } + + void write_aiw_step() + { + for (int i = 0;; i++) + { + if (aiw_inputs.count(i)) { + auto v = top->get_state(aiw_inputs.at(i)); + if (v == State::S1) + aiwfile << '1'; + else + aiwfile << '0'; + continue; + } + if (aiw_inits.count(i)) { + auto v = top->get_state(aiw_inits.at(i)); + if (v == State::S1) + aiwfile << '1'; + else + aiwfile << '0'; + continue; + } + aiwfile << '\n'; + break; + } + } + + void write_aiw_end() + { + aiwfile << '.' << '\n'; + } + void write_output_header() { if (vcdfile.is_open()) write_vcd_header(); if (fstfile) write_fst_header(); + if (aiwfile.is_open()) + write_aiw_header(); } void write_output_step(int t) @@ -930,12 +1002,16 @@ struct SimWorker : SimShared write_vcd_step(t); if (fstfile) write_fst_step(t); + if (aiwfile.is_open()) + write_aiw_step(); } void write_output_end() { if (fstfile) fstWriterClose(fstfile); + if (aiwfile.is_open()) + write_aiw_end(); } void update() @@ -1269,6 +1345,10 @@ struct SimPass : public Pass { log(" -fst <filename>\n"); log(" write the simulation results to the given FST file\n"); log("\n"); + log(" -aiw <filename>\n"); + log(" write the simulation results to an AIGER witness file\n"); + log(" (requires a *.aim file via -map)\n"); + log("\n"); log(" -clock <portname>\n"); log(" name of top-level clock input\n"); log("\n"); @@ -1355,6 +1435,12 @@ struct SimPass : public Pass { worker.fstfile = (struct fstContext *)fstWriterCreate(fst_filename.c_str(),1); continue; } + if (args[argidx] == "-aiw" && argidx+1 < args.size()) { + std::string aiw_filename = args[++argidx]; + rewrite_filename(aiw_filename); + worker.aiwfile.open(aiw_filename.c_str()); + continue; + } if (args[argidx] == "-n" && argidx+1 < args.size()) { numcycles = atoi(args[++argidx].c_str()); worker.cycles_set = true; |