X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=backends%2Fbtor%2Fbtor.cc;h=eabd870ab715540072db1e35c87fe887663b2c09;hb=dde3dfd72e25bc1f166a8448fed2742c46b4aa71;hp=4472993d4fadbcd3678b1fd8b1e49afddaeae675;hpb=cb0dc6e68b9432edc9c30c153954be53c8576911;p=yosys.git diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4472993d4..eabd870ab 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -39,6 +39,7 @@ struct BtorWorker RTLIL::Module *module; bool verbose; bool single_bad; + bool cover_mode; int next_nid = 1; int initstate_nid = -1; @@ -71,7 +72,11 @@ struct BtorWorker vector bad_properties; dict initbits; pool statewires; - string indent; + pool srcsymbols; + + string indent, info_filename; + vector info_lines; + dict info_clocks; void btorf(const char *fmt, ...) { @@ -81,6 +86,40 @@ struct BtorWorker va_end(ap); } + void infof(const char *fmt, ...) + { + va_list ap; + va_start(ap, fmt); + info_lines.push_back(vstringf(fmt, ap)); + va_end(ap); + } + + template + string getinfo(T *obj, bool srcsym = false) + { + string infostr = log_id(obj); + if (obj->attributes.count("\\src")) { + string src = obj->attributes.at("\\src").decode_string().c_str(); + if (srcsym && infostr[0] == '$') { + std::replace(src.begin(), src.end(), ' ', '_'); + if (srcsymbols.count(src) || module->count_id("\\" + src)) { + for (int i = 1;; i++) { + string s = stringf("%s-%d", src.c_str(), i); + if (!srcsymbols.count(s) && !module->count_id("\\" + s)) { + src = s; + break; + } + } + } + srcsymbols.insert(src); + infostr = src; + } else { + infostr += " ; " + src; + } + } + return infostr; + } + void btorf_push(const string &id) { if (verbose) { @@ -164,9 +203,9 @@ struct BtorWorker if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor"; log_assert(!btor_op.empty()); - int width = GetSize(cell->getPort("\\Y")); - width = std::max(width, GetSize(cell->getPort("\\A"))); - width = std::max(width, GetSize(cell->getPort("\\B"))); + int width = GetSize(cell->getPort(ID::Y)); + width = std::max(width, GetSize(cell->getPort(ID::A))); + width = std::max(width, GetSize(cell->getPort(ID::B))); bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false; @@ -185,8 +224,8 @@ struct BtorWorker if (btor_op == "shift") { - int nid_a = get_sig_nid(cell->getPort("\\A"), width, false); - int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + int nid_a = get_sig_nid(cell->getPort(ID::A), width, false); + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); int nid_r = next_nid++; btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); @@ -203,18 +242,18 @@ struct BtorWorker btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero); nid = next_nid++; - btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r); + btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str()); } else { - int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); - int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); nid = next_nid++; - btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); + btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); } - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); if (GetSize(sig) < width) { int sid = get_bv_sid(GetSize(sig)); @@ -234,21 +273,21 @@ struct BtorWorker if (cell->type == "$mod") btor_op = "rem"; log_assert(!btor_op.empty()); - int width = GetSize(cell->getPort("\\Y")); - width = std::max(width, GetSize(cell->getPort("\\A"))); - width = std::max(width, GetSize(cell->getPort("\\B"))); + int width = GetSize(cell->getPort(ID::Y)); + width = std::max(width, GetSize(cell->getPort(ID::A))); + width = std::max(width, GetSize(cell->getPort(ID::B))); bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false; - int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); - int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); int sid = get_bv_sid(width); int nid = next_nid++; - btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b); + btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); if (GetSize(sig) < width) { int sid = get_bv_sid(GetSize(sig)); @@ -264,23 +303,23 @@ struct BtorWorker if (cell->type.in("$_ANDNOT_", "$_ORNOT_")) { int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); - int nid_b = get_sig_nid(cell->getPort("\\B")); + int nid_a = get_sig_nid(cell->getPort(ID::A)); + int nid_b = get_sig_nid(cell->getPort(ID::B)); int nid1 = next_nid++; int nid2 = next_nid++; if (cell->type == "$_ANDNOT_") { btorf("%d not %d %d\n", nid1, sid, nid_b); - btorf("%d and %d %d %d\n", nid2, sid, nid_a, nid1); + btorf("%d and %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str()); } if (cell->type == "$_ORNOT_") { btorf("%d not %d %d\n", nid1, sid, nid_b); - btorf("%d or %d %d %d\n", nid2, sid, nid_a, nid1); + btorf("%d or %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str()); } - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); add_nid_sig(nid2, sig); goto okay; } @@ -288,8 +327,8 @@ struct BtorWorker if (cell->type.in("$_OAI3_", "$_AOI3_")) { int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); - int nid_b = get_sig_nid(cell->getPort("\\B")); + int nid_a = get_sig_nid(cell->getPort(ID::A)); + int nid_b = get_sig_nid(cell->getPort(ID::B)); int nid_c = get_sig_nid(cell->getPort("\\C")); int nid1 = next_nid++; @@ -299,16 +338,16 @@ struct BtorWorker if (cell->type == "$_OAI3_") { btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b); btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c); - btorf("%d not %d %d\n", nid3, sid, nid2); + btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str()); } if (cell->type == "$_AOI3_") { btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b); btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c); - btorf("%d not %d %d\n", nid3, sid, nid2); + btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str()); } - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); add_nid_sig(nid3, sig); goto okay; } @@ -316,8 +355,8 @@ struct BtorWorker if (cell->type.in("$_OAI4_", "$_AOI4_")) { int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); - int nid_b = get_sig_nid(cell->getPort("\\B")); + int nid_a = get_sig_nid(cell->getPort(ID::A)); + int nid_b = get_sig_nid(cell->getPort(ID::B)); int nid_c = get_sig_nid(cell->getPort("\\C")); int nid_d = get_sig_nid(cell->getPort("\\D")); @@ -330,17 +369,17 @@ struct BtorWorker btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b); btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d); btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2); - btorf("%d not %d %d\n", nid4, sid, nid3); + btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str()); } if (cell->type == "$_AOI4_") { btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b); btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d); btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2); - btorf("%d not %d %d\n", nid4, sid, nid3); + btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str()); } - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); add_nid_sig(nid4, sig); goto okay; } @@ -357,24 +396,24 @@ struct BtorWorker log_assert(!btor_op.empty()); int width = 1; - width = std::max(width, GetSize(cell->getPort("\\A"))); - width = std::max(width, GetSize(cell->getPort("\\B"))); + width = std::max(width, GetSize(cell->getPort(ID::A))); + width = std::max(width, GetSize(cell->getPort(ID::B))); bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false; int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); - int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); int nid = next_nid++; if (cell->type.in("$lt", "$le", "$ge", "$gt")) { - btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b); + btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); } else { - btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); + btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); } - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); if (GetSize(sig) > 1) { int sid = get_bv_sid(GetSize(sig)); @@ -394,18 +433,17 @@ struct BtorWorker if (cell->type == "$neg") btor_op = "neg"; log_assert(!btor_op.empty()); - int width = GetSize(cell->getPort("\\Y")); - width = std::max(width, GetSize(cell->getPort("\\A"))); + int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; int sid = get_bv_sid(width); - int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); + int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); int nid = next_nid++; - btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a); + btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); if (GetSize(sig) < width) { int sid = get_bv_sid(GetSize(sig)); @@ -427,16 +465,16 @@ struct BtorWorker log_assert(!btor_op.empty()); int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); - int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort("\\B")) : 0; + int nid_a = get_sig_nid(cell->getPort(ID::A)); + int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort(ID::B)) : 0; - if (GetSize(cell->getPort("\\A")) > 1) { + if (GetSize(cell->getPort(ID::A)) > 1) { int nid_red_a = next_nid++; btorf("%d redor %d %d\n", nid_red_a, sid, nid_a); nid_a = nid_red_a; } - if (btor_op != "not" && GetSize(cell->getPort("\\B")) > 1) { + if (btor_op != "not" && GetSize(cell->getPort(ID::B)) > 1) { int nid_red_b = next_nid++; btorf("%d redor %d %d\n", nid_red_b, sid, nid_b); nid_b = nid_red_b; @@ -444,11 +482,11 @@ struct BtorWorker int nid = next_nid++; if (btor_op != "not") - btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); + btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); else - btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a); + btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); if (GetSize(sig) > 1) { int sid = get_bv_sid(GetSize(sig)); @@ -471,18 +509,20 @@ struct BtorWorker log_assert(!btor_op.empty()); int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); + int nid_a = get_sig_nid(cell->getPort(ID::A)); int nid = next_nid++; - btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a); if (cell->type == "$reduce_xnor") { int nid2 = next_nid++; + btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); btorf("%d not %d %d %d\n", nid2, sid, nid); nid = nid2; + } else { + btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); } - SigSpec sig = sigmap(cell->getPort("\\Y")); + SigSpec sig = sigmap(cell->getPort(ID::Y)); if (GetSize(sig) > 1) { int sid = get_bv_sid(GetSize(sig)); @@ -498,10 +538,10 @@ struct BtorWorker if (cell->type.in("$mux", "$_MUX_", "$_NMUX_")) { - SigSpec sig_a = sigmap(cell->getPort("\\A")); - SigSpec sig_b = sigmap(cell->getPort("\\B")); - SigSpec sig_s = sigmap(cell->getPort("\\S")); - SigSpec sig_y = sigmap(cell->getPort("\\Y")); + SigSpec sig_a = sigmap(cell->getPort(ID::A)); + SigSpec sig_b = sigmap(cell->getPort(ID::B)); + SigSpec sig_s = sigmap(cell->getPort(ID::S)); + SigSpec sig_y = sigmap(cell->getPort(ID::Y)); int nid_a = get_sig_nid(sig_a); int nid_b = get_sig_nid(sig_b); @@ -509,12 +549,14 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig_y)); int nid = next_nid++; - btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a); if (cell->type == "$_NMUX_") { int tmp = nid; nid = next_nid++; - btorf("%d not %d %d\n", nid, sid, tmp); + btorf("%d ite %d %d %d %d\n", tmp, sid, nid_s, nid_b, nid_a); + btorf("%d not %d %d %s\n", nid, sid, tmp, getinfo(cell).c_str()); + } else { + btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str()); } add_nid_sig(nid, sig_y); @@ -523,10 +565,10 @@ struct BtorWorker if (cell->type == "$pmux") { - SigSpec sig_a = sigmap(cell->getPort("\\A")); - SigSpec sig_b = sigmap(cell->getPort("\\B")); - SigSpec sig_s = sigmap(cell->getPort("\\S")); - SigSpec sig_y = sigmap(cell->getPort("\\Y")); + SigSpec sig_a = sigmap(cell->getPort(ID::A)); + SigSpec sig_b = sigmap(cell->getPort(ID::B)); + SigSpec sig_s = sigmap(cell->getPort(ID::S)); + SigSpec sig_y = sigmap(cell->getPort(ID::Y)); int width = GetSize(sig_a); int sid = get_bv_sid(width); @@ -536,7 +578,10 @@ struct BtorWorker int nid_b = get_sig_nid(sig_b.extract(i*width, width)); int nid_s = get_sig_nid(sig_s.extract(i)); int nid2 = next_nid++; - btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid); + if (i == GetSize(sig_s)-1) + btorf("%d ite %d %d %d %d %s\n", nid2, sid, nid_s, nid_b, nid, getinfo(cell).c_str()); + else + btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid); nid = nid2; } @@ -544,11 +589,26 @@ struct BtorWorker goto okay; } - if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_")) + if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N_", "$_FF_")) { SigSpec sig_d = sigmap(cell->getPort("\\D")); SigSpec sig_q = sigmap(cell->getPort("\\Q")); + if (!info_filename.empty() && cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) + { + SigSpec sig_c = sigmap(cell->getPort(cell->type == "$dff" ? "\\CLK" : "\\C")); + int nid = get_sig_nid(sig_c); + bool negedge = false; + + if (cell->type == "$_DFF_N_") + negedge = true; + + if (cell->type == "$dff" && !cell->getParam("\\CLK_POLARITY").as_bool()) + negedge = true; + + info_clocks[nid] |= negedge ? 2 : 1; + } + IdString symbol; if (sig_q.is_wire()) { @@ -569,7 +629,7 @@ struct BtorWorker int nid_init_val = -1; if (!initval.is_fully_undef()) - nid_init_val = get_sig_nid(initval); + nid_init_val = get_sig_nid(initval, -1, false, true); int sid = get_bv_sid(GetSize(sig_q)); int nid = next_nid++; @@ -593,7 +653,7 @@ struct BtorWorker if (cell->type.in("$anyconst", "$anyseq")) { - SigSpec sig_y = sigmap(cell->getPort("\\Y")); + SigSpec sig_y = sigmap(cell->getPort(ID::Y)); int sid = get_bv_sid(GetSize(sig_y)); int nid = next_nid++; @@ -611,7 +671,7 @@ struct BtorWorker if (cell->type == "$initstate") { - SigSpec sig_y = sigmap(cell->getPort("\\Y")); + SigSpec sig_y = sigmap(cell->getPort(ID::Y)); if (initstate_nid < 0) { @@ -681,7 +741,7 @@ struct BtorWorker { if (verbose) btorf("; initval = %s\n", log_signal(firstword)); - nid_init_val = get_sig_nid(firstword); + nid_init_val = get_sig_nid(firstword, -1, false, true); } else { @@ -693,8 +753,8 @@ struct BtorWorker if (thisword.is_fully_undef()) continue; Const thisaddr(i, abits); - int nid_thisword = get_sig_nid(thisword); - int nid_thisaddr = get_sig_nid(thisaddr); + int nid_thisword = get_sig_nid(thisword, -1, false, true); + int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true); int last_nid_init_val = nid_init_val; nid_init_val = next_nid++; if (verbose) @@ -792,7 +852,7 @@ struct BtorWorker cell_recursion_guard.erase(cell); } - int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false) + int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false) { int nid = -1; sigmap.apply(sig); @@ -823,7 +883,10 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig)); int nid_input = next_nid++; - btorf("%d input %d\n", nid_input, sid); + if (is_init) + btorf("%d state %d\n", nid_input, sid); + else + btorf("%d input %d\n", nid_input, sid); int nid_masked_input; if (sig_mask_undef.is_fully_ones()) { @@ -897,9 +960,12 @@ struct BtorWorker int sid = get_bv_sid(GetSize(s)); int nid = next_nid++; - btorf("%d input %d %s\n", nid, sid); + btorf("%d input %d\n", nid, sid); nid_width[nid] = GetSize(s); + for (int j = 0; j < GetSize(s); j++) + nidbits.push_back(make_pair(nid, j)); + i += GetSize(s)-1; continue; } @@ -977,9 +1043,12 @@ struct BtorWorker return nid; } - BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad) : - f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad) + BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, string info_filename) : + f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), info_filename(info_filename) { + if (!info_filename.empty()) + infof("name %s\n", log_id(module)); + btorf_push("inputs"); for (auto wire : module->wires()) @@ -998,7 +1067,7 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig)); int nid = next_nid++; - btorf("%d input %d %s\n", nid, sid, log_id(wire)); + btorf("%d input %d %s\n", nid, sid, getinfo(wire).c_str()); add_nid_sig(nid, sig); } @@ -1022,7 +1091,7 @@ struct BtorWorker btorf_push(stringf("output %s", log_id(wire))); int nid = get_sig_nid(wire); - btorf("%d output %d %s\n", next_nid++, nid, log_id(wire)); + btorf("%d output %d %s\n", next_nid++, nid, getinfo(wire).c_str()); btorf_pop(stringf("output %s", log_id(wire))); } @@ -1034,7 +1103,7 @@ struct BtorWorker btorf_push(log_id(cell)); int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); + int nid_a = get_sig_nid(cell->getPort(ID::A)); int nid_en = get_sig_nid(cell->getPort("\\EN")); int nid_not_en = next_nid++; int nid_a_or_not_en = next_nid++; @@ -1052,7 +1121,7 @@ struct BtorWorker btorf_push(log_id(cell)); int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort("\\A")); + int nid_a = get_sig_nid(cell->getPort(ID::A)); int nid_en = get_sig_nid(cell->getPort("\\EN")); int nid_not_a = next_nid++; int nid_en_and_not_a = next_nid++; @@ -1060,11 +1129,36 @@ struct BtorWorker 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); - if (single_bad) { + if (single_bad && !cover_mode) { bad_properties.push_back(nid_en_and_not_a); + } else { + if (cover_mode) { + infof("bad %d %s\n", nid_en_and_not_a, getinfo(cell, true).c_str()); + } else { + int nid = next_nid++; + btorf("%d bad %d %s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str()); + } + } + + btorf_pop(log_id(cell)); + } + + if (cell->type == "$cover" && cover_mode) + { + 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")); + int nid_en_and_a = next_nid++; + + btorf("%d and %d %d %d\n", nid_en_and_a, sid, nid_en, nid_a); + + if (single_bad) { + bad_properties.push_back(nid_en_and_a); } else { int nid = next_nid++; - btorf("%d bad %d\n", nid, nid_en_and_not_a); + btorf("%d bad %d %s\n", nid, nid_en_and_a, getinfo(cell, true).c_str()); } btorf_pop(log_id(cell)); @@ -1085,7 +1179,7 @@ struct BtorWorker continue; int this_nid = next_nid++; - btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, log_id(wire)); + btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, getinfo(wire).c_str()); btorf_pop(stringf("wire %s", log_id(wire))); continue; @@ -1156,14 +1250,14 @@ struct BtorWorker } int nid2 = next_nid++; - btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head); + btorf("%d next %d %d %d %s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str()); } else { SigSpec sig = sigmap(cell->getPort("\\D")); int nid_q = get_sig_nid(sig); int sid = get_bv_sid(GetSize(sig)); - btorf("%d next %d %d %d\n", next_nid++, sid, nid, nid_q); + btorf("%d next %d %d %d %s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); } btorf_pop(stringf("next %s", log_id(cell))); @@ -1199,6 +1293,35 @@ struct BtorWorker btorf("%d bad %d\n", nid, todo[cursor]); } } + + if (!info_filename.empty()) + { + for (auto &it : info_clocks) + { + switch (it.second) + { + case 1: + infof("posedge %d\n", it.first); + break; + case 2: + infof("negedge %d\n", it.first); + break; + case 3: + infof("event %d\n", it.first); + break; + default: + log_abort(); + } + } + + std::ofstream f; + f.open(info_filename.c_str(), std::ofstream::trunc); + if (f.fail()) + log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno)); + for (auto &it : info_lines) + f << it; + f.close(); + } } }; @@ -1218,10 +1341,17 @@ struct BtorBackend : public Backend { log(" -s\n"); log(" Output only a single bad property for all asserts\n"); log("\n"); + log(" -c\n"); + log(" Output cover properties using 'bad' statements instead of asserts\n"); + log("\n"); + log(" -i \n"); + log(" Create additional info file with auxiliary information\n"); + log("\n"); } void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) YS_OVERRIDE { - bool verbose = false, single_bad = false; + bool verbose = false, single_bad = false, cover_mode = false; + string info_filename; log_header(design, "Executing BTOR backend.\n"); @@ -1236,6 +1366,14 @@ struct BtorBackend : public Backend { single_bad = true; continue; } + if (args[argidx] == "-c") { + cover_mode = true; + continue; + } + if (args[argidx] == "-i" && argidx+1 < args.size()) { + info_filename = args[++argidx]; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -1248,7 +1386,7 @@ struct BtorBackend : public Backend { *f << stringf("; BTOR description generated by %s for module %s.\n", yosys_version_str, log_id(topmod)); - BtorWorker(*f, topmod, verbose, single_bad); + BtorWorker(*f, topmod, verbose, single_bad, cover_mode, info_filename); *f << stringf("; end of yosys output\n"); }