From 60d11295061956c56af5517272d0b58035c30ee6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 23 Nov 2017 23:44:39 +0100 Subject: [PATCH] Progress in new BTOR back-end --- backends/btor/btor.cc | 133 ++++++++++++++++++++++++++++++------------ 1 file changed, 97 insertions(+), 36 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 61caf57e4..2a98d1aba 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -58,16 +58,42 @@ struct BtorWorker // nids for constants dict consts; - // ff inputs that need to be evaluated (, ) - vector> ff_todo; + // ff inputs that need to be evaluated (, ) + vector> ff_todo; pool cell_recursion_guard; + pool output_symbols; + string indent; + + void btorf(const char *fmt, ...) + { + va_list ap; + va_start(ap, fmt); + f << indent << vstringf(fmt, ap); + va_end(ap); + } + + void btorf_push(const string &id) + { + if (verbose) { + f << indent << stringf(" ; begin %s\n", id.c_str()); + indent += " "; + } + } + + void btorf_pop(const string &id) + { + if (verbose) { + indent = indent.substr(4); + f << indent << stringf(" ; end %s\n", id.c_str()); + } + } int get_bv_sid(int width) { if (sorts_bv.count(width) == 0) { int nid = next_nid++; - f << stringf("%d sort bitvec %d\n", nid, width); + btorf("%d sort bitvec %d\n", nid, width); sorts_bv[width] = nid; } return sorts_bv.at(width); @@ -86,6 +112,7 @@ struct BtorWorker { log_assert(cell_recursion_guard.count(cell) == 0); cell_recursion_guard.insert(cell); + btorf_push(log_id(cell)); if (cell->type.in("$add", "$sub", "$xor")) { @@ -107,14 +134,14 @@ struct BtorWorker int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); int nid = next_nid++; - f << stringf("%d %s %d %d %d ; %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, log_id(cell)); + btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); SigSpec sig = sigmap(cell->getPort("\\Y")); if (GetSize(sig) < width) { int sid = get_bv_sid(GetSize(sig)); int nid2 = next_nid++; - f << stringf("%d slice %d %d %d 0 ; %s\n", nid2, sid, nid, GetSize(sig)-1, log_id(cell)); + btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1); nid = nid2; } @@ -135,18 +162,18 @@ struct BtorWorker if (GetSize(cell->getPort("\\A")) > 1) { int nid_red_a = next_nid++; - f << stringf("%d redor %d %d\n", nid_red_a, sid, nid_a); + btorf("%d redor %d %d\n", nid_red_a, sid, nid_a); nid_a = nid_red_a; } if (GetSize(cell->getPort("\\B")) > 1) { int nid_red_b = next_nid++; - f << stringf("%d redor %d %d\n", nid_red_b, sid, nid_b); + btorf("%d redor %d %d\n", nid_red_b, sid, nid_b); nid_b = nid_red_b; } int nid = next_nid++; - f << stringf("%d %s %d %d %d ; %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, log_id(cell)); + btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); SigSpec sig = sigmap(cell->getPort("\\Y")); @@ -154,7 +181,7 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig)); int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1)); int nid2 = next_nid++; - f << stringf("%d concat %d %d %d ; %s\n", nid2, sid, zeros_nid, nid, log_id(cell)); + btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid); nid = nid2; } @@ -175,7 +202,7 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig_y)); int nid = next_nid++; - f << stringf("%d ite %d %d %d %d ; %s\n", nid, sid, nid_s, nid_b, nid_a, log_id(cell)); + btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a); add_nid_sig(nid, sig_y); goto okay; @@ -195,9 +222,13 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig_q)); int nid = next_nid++; - f << stringf("%d state %d %s ; %s\n", nid, sid, symbol.c_str(), log_id(cell)); - ff_todo.push_back(make_pair(nid, sig_d)); + if (output_symbols.count(symbol)) + btorf("%d state %d\n", nid, sid); + else + btorf("%d state %d %s\n", nid, sid, symbol.c_str()); + + ff_todo.push_back(make_pair(nid, cell)); add_nid_sig(nid, sig_q); goto okay; } @@ -212,9 +243,9 @@ struct BtorWorker int one_nid = get_sig_nid(Const(1, 1)); int zero_nid = get_sig_nid(Const(0, 1)); initstate_nid = next_nid++; - f << stringf("%d state %d ; initstate\n", initstate_nid, sid); - f << stringf("%d init %d %d %d ; initstate\n", next_nid++, sid, initstate_nid, one_nid); - f << stringf("%d next %d %d %d ; initstate\n", next_nid++, sid, initstate_nid, zero_nid); + btorf("%d state %d\n", initstate_nid, sid); + 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); } add_nid_sig(initstate_nid, sig_y); @@ -224,6 +255,7 @@ struct BtorWorker log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); okay: + btorf_pop(log_id(cell)); cell_recursion_guard.erase(cell); } @@ -253,7 +285,7 @@ struct BtorWorker if (consts.count(c) == 0) { int sid = get_bv_sid(GetSize(c)); int nid = next_nid++; - f << stringf("%d const %d %s\n", nid, sid, c.as_string().c_str()); + btorf("%d const %d %s\n", nid, sid, c.as_string().c_str()); consts[c] = nid; nid_width[nid] = GetSize(c); } @@ -295,7 +327,7 @@ struct BtorWorker if (lower != 0 || upper+1 != nid_width.at(nid2)) { int sid = get_bv_sid(upper-lower+1); nid3 = next_nid++; - f << stringf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower); + btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower); } int nid4 = nid3; @@ -303,7 +335,7 @@ struct BtorWorker if (nid >= 0) { int sid = get_bv_sid(width+upper-lower+1); int nid4 = next_nid++; - f << stringf("%d concat %d %d %d\n", nid4, sid, nid, nid3); + btorf("%d concat %d %d %d\n", nid4, sid, nid, nid3); } width += upper-lower+1; @@ -322,14 +354,14 @@ struct BtorWorker { int sid = get_bv_sid(to_width); int nid2 = next_nid++; - f << stringf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1); + btorf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1); nid = nid2; } else { int sid = get_bv_sid(to_width); int nid2 = next_nid++; - f << stringf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext", + btorf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext", sid, nid, to_width - GetSize(sig)); nid = nid2; } @@ -341,6 +373,8 @@ struct BtorWorker BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) : f(f), sigmap(module), module(module), verbose(verbose) { + btorf_push("inputs"); + for (auto wire : module->wires()) { if (!wire->port_id || !wire->port_input) @@ -350,10 +384,12 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig)); int nid = next_nid++; - f << stringf("%d input %d %s\n", nid, sid, log_id(wire)); + btorf("%d input %d %s\n", nid, sid, log_id(wire)); add_nid_sig(nid, sig); } + btorf_pop("inputs"); + for (auto cell : module->cells()) for (auto &conn : cell->connections()) { @@ -364,19 +400,29 @@ struct BtorWorker bit_cell[bit] = cell; } + for (auto wire : module->wires()) + if (wire->port_output) + output_symbols.insert(log_id(wire)); + for (auto wire : module->wires()) { if (!wire->port_id || !wire->port_output) continue; + btorf_push(stringf("output %s", log_id(wire))); + int nid = get_sig_nid(wire); - f << stringf("%d output %d %s\n", next_nid++, nid, log_id(wire)); + btorf("%d output %d %s\n", next_nid++, nid, log_id(wire)); + + btorf_pop(stringf("output %s", log_id(wire))); } for (auto cell : module->cells()) { if (cell->type == "$assume") { + btorf_push(log_id(cell)); + int sid = get_bv_sid(1); int nid_a = get_sig_nid(cell->getPort("\\A")); int nid_en = get_sig_nid(cell->getPort("\\EN")); @@ -384,13 +430,17 @@ struct BtorWorker int nid_a_or_not_en = next_nid++; int nid = next_nid++; - f << stringf("%d not %d %d\n", nid_not_en, sid, nid_en); - f << stringf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en); - f << stringf("%d constraint %d ; %s\n", nid, nid_a_or_not_en, log_id(cell)); + btorf("%d not %d %d\n", nid_not_en, sid, nid_en); + btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en); + btorf("%d constraint %d\n", nid, nid_a_or_not_en); + + btorf_pop(log_id(cell)); } if (cell->type == "$assert") { + btorf_push(log_id(cell)); + int sid = get_bv_sid(1); int nid_a = get_sig_nid(cell->getPort("\\A")); int nid_en = get_sig_nid(cell->getPort("\\EN")); @@ -398,22 +448,30 @@ struct BtorWorker int nid_en_and_not_a = next_nid++; int nid = next_nid++; - f << stringf("%d not %d %d\n", nid_not_a, sid, nid_a); - f << stringf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a); - f << stringf("%d bad %d ; %s\n", nid, nid_en_and_not_a, log_id(cell)); + btorf("%d not %d %d\n", nid_not_a, sid, nid_a); + btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a); + btorf("%d bad %d\n", nid, nid_en_and_not_a); + + btorf_pop(log_id(cell)); } } while (!ff_todo.empty()) { - vector> todo; + vector> todo; todo.swap(ff_todo); for (auto &it : todo) { - int nid = get_sig_nid(it.second); - int sid = get_bv_sid(GetSize(it.second)); - f << stringf("%d next %d %d %d\n", next_nid++, sid, it.first, nid); + btorf_push(stringf("next %s", log_id(it.second))); + + SigSpec sig = sigmap(it.second->getPort("\\D")); + + int nid = get_sig_nid(sig); + int sid = get_bv_sid(GetSize(sig)); + btorf("%d next %d %d %d\n", next_nid++, sid, it.first, nid); + + btorf_pop(stringf("next %s", log_id(it.second))); } } } @@ -429,6 +487,9 @@ struct BtorBackend : public Backend { log("\n"); log("Write a BTOR description of the current design.\n"); log("\n"); + log(" -v\n"); + log(" Add comments and indentation to BTOR output file\n"); + log("\n"); } virtual void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) { @@ -439,10 +500,10 @@ struct BtorBackend : public Backend { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - // if (args[argidx] == "-verbose") { - // verbose = true; - // continue; - // } + if (args[argidx] == "-v") { + verbose = true; + continue; + } break; } extra_args(f, filename, args, argidx); -- 2.30.2