diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 270 |
1 files changed, 135 insertions, 135 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e1d6f5535..3e67e55f2 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -135,7 +135,7 @@ struct Smt2Worker log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); - if (cell->type.in("$mem") && conn.first.in("\\RD_CLK", "\\WR_CLK")) + if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK)) { SigSpec clk = sigmap(conn.second); for (int i = 0; i < GetSize(clk); i++) @@ -143,19 +143,19 @@ struct Smt2Worker if (clk[i].wire == nullptr) continue; - if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1) + if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1) continue; - if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\WR_CLK_POLARITY")[i] == State::S1) + if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1) clock_posedge.insert(clk[i]); else clock_negedge.insert(clk[i]); } } else - if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C")) + if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C)) { - bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool()); + bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool()); for (auto bit : sigmap(conn.second)) { if (posedge) clock_posedge.insert(bit); @@ -373,8 +373,8 @@ struct Smt2Worker for (char ch : expr) { if (ch == 'A') processed_expr += get_bool(cell->getPort(ID::A)); else if (ch == 'B') processed_expr += get_bool(cell->getPort(ID::B)); - else if (ch == 'C') processed_expr += get_bool(cell->getPort("\\C")); - else if (ch == 'D') processed_expr += get_bool(cell->getPort("\\D")); + else if (ch == 'C') processed_expr += get_bool(cell->getPort(ID::C)); + else if (ch == 'D') processed_expr += get_bool(cell->getPort(ID::D)); else if (ch == 'S') processed_expr += get_bool(cell->getPort(ID::S)); else processed_expr += ch; } @@ -392,7 +392,7 @@ struct Smt2Worker { RTLIL::SigSpec sig_a, sig_b; RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - bool is_signed = cell->getParam("\\A_SIGNED").as_bool(); + bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); int width = GetSize(sig_y); if (type == 's' || type == 'd' || type == 'b') { @@ -480,7 +480,7 @@ struct Smt2Worker exported_cells.insert(cell); recursive_cells.insert(cell); - if (cell->type == "$initstate") + if (cell->type == ID($initstate)) { SigBit bit = sigmap(cell->getPort(ID::Y).as_bit()); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n", @@ -490,80 +490,80 @@ struct Smt2Worker return; } - if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_")) + if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { registers.insert(cell); - makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q"))); - register_bool(cell->getPort("\\Q"), idcounter++); + makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q))); + register_bool(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); return; } - if (cell->type == "$_BUF_") return export_gate(cell, "A"); - if (cell->type == "$_NOT_") return export_gate(cell, "(not A)"); - if (cell->type == "$_AND_") return export_gate(cell, "(and A B)"); - if (cell->type == "$_NAND_") return export_gate(cell, "(not (and A B))"); - if (cell->type == "$_OR_") return export_gate(cell, "(or A B)"); - if (cell->type == "$_NOR_") return export_gate(cell, "(not (or A B))"); - if (cell->type == "$_XOR_") return export_gate(cell, "(xor A B)"); - if (cell->type == "$_XNOR_") return export_gate(cell, "(not (xor A B))"); - if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))"); - if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))"); - if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)"); - if (cell->type == "$_NMUX_") return export_gate(cell, "(not (ite S B A))"); - if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))"); - if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))"); - if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))"); - if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))"); + if (cell->type == ID($_BUF_)) return export_gate(cell, "A"); + if (cell->type == ID($_NOT_)) return export_gate(cell, "(not A)"); + if (cell->type == ID($_AND_)) return export_gate(cell, "(and A B)"); + if (cell->type == ID($_NAND_)) return export_gate(cell, "(not (and A B))"); + if (cell->type == ID($_OR_)) return export_gate(cell, "(or A B)"); + if (cell->type == ID($_NOR_)) return export_gate(cell, "(not (or A B))"); + if (cell->type == ID($_XOR_)) return export_gate(cell, "(xor A B)"); + if (cell->type == ID($_XNOR_)) return export_gate(cell, "(not (xor A B))"); + if (cell->type == ID($_ANDNOT_)) return export_gate(cell, "(and A (not B))"); + if (cell->type == ID($_ORNOT_)) return export_gate(cell, "(or A (not B))"); + if (cell->type == ID($_MUX_)) return export_gate(cell, "(ite S B A)"); + if (cell->type == ID($_NMUX_)) return export_gate(cell, "(not (ite S B A))"); + if (cell->type == ID($_AOI3_)) return export_gate(cell, "(not (or (and A B) C))"); + if (cell->type == ID($_OAI3_)) return export_gate(cell, "(not (and (or A B) C))"); + if (cell->type == ID($_AOI4_)) return export_gate(cell, "(not (or (and A B) (and C D)))"); + if (cell->type == ID($_OAI4_)) return export_gate(cell, "(not (and (or A B) (or C D)))"); // FIXME: $lut if (bvmode) { - if (cell->type.in("$ff", "$dff")) + if (cell->type.in(ID($ff), ID($dff))) { registers.insert(cell); - makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))); - register_bv(cell->getPort("\\Q"), idcounter++); + makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))); + register_bv(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); return; } - if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq")) + if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq))) { registers.insert(cell); string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell); - if (cell->attributes.count("\\reg")) - infostr += " " + cell->attributes.at("\\reg").decode_string(); + if (cell->attributes.count(ID::reg)) + infostr += " " + cell->attributes.at(ID::reg).decode_string(); decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str())); - if (cell->getPort("\\Y").is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute("\\maximize")){ + if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){ decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter)); log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str()); } - else if (cell->getPort("\\Y").is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute("\\minimize")){ + else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){ decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter)); log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str()); } makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y))); - if (cell->type == "$anyseq") + if (cell->type == ID($anyseq)) ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter)); register_bv(cell->getPort(ID::Y), idcounter++); recursive_cells.erase(cell); return; } - if (cell->type == "$and") return export_bvop(cell, "(bvand A B)"); - if (cell->type == "$or") return export_bvop(cell, "(bvor A B)"); - if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)"); - if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)"); + if (cell->type == ID($and)) return export_bvop(cell, "(bvand A B)"); + if (cell->type == ID($or)) return export_bvop(cell, "(bvor A B)"); + if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)"); + if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)"); - if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's'); - if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's'); - if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's'); - if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's'); + if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's'); + if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's'); + if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's'); + if (cell->type == ID($sshr)) return export_bvop(cell, "(bvLshr A B)", 's'); - if (cell->type.in("$shift", "$shiftx")) { - if (cell->getParam("\\B_SIGNED").as_bool()) { + if (cell->type.in(ID($shift), ID($shiftx))) { + if (cell->getParam(ID::B_SIGNED).as_bool()) { return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) " "(bvlshr A B) (bvlshr A (bvneg B)))", GetSize(cell->getPort(ID::B)), 0), 's'); @@ -572,44 +572,44 @@ struct Smt2Worker } } - if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b'); - if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b'); - if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b'); - if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b'); + if (cell->type == ID($lt)) return export_bvop(cell, "(bvUlt A B)", 'b'); + if (cell->type == ID($le)) return export_bvop(cell, "(bvUle A B)", 'b'); + if (cell->type == ID($ge)) return export_bvop(cell, "(bvUge A B)", 'b'); + if (cell->type == ID($gt)) return export_bvop(cell, "(bvUgt A B)", 'b'); - if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b'); - if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b'); - if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b'); - if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b'); + if (cell->type == ID($ne)) return export_bvop(cell, "(distinct A B)", 'b'); + if (cell->type == ID($nex)) return export_bvop(cell, "(distinct A B)", 'b'); + if (cell->type == ID($eq)) return export_bvop(cell, "(= A B)", 'b'); + if (cell->type == ID($eqx)) return export_bvop(cell, "(= A B)", 'b'); - if (cell->type == "$not") return export_bvop(cell, "(bvnot A)"); - if (cell->type == "$pos") return export_bvop(cell, "A"); - if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)"); + if (cell->type == ID($not)) return export_bvop(cell, "(bvnot A)"); + if (cell->type == ID($pos)) return export_bvop(cell, "A"); + if (cell->type == ID($neg)) return export_bvop(cell, "(bvneg A)"); - if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)"); - if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)"); - if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)"); - if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd'); - if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd'); + if (cell->type == ID($add)) return export_bvop(cell, "(bvadd A B)"); + if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)"); + if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)"); + if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd'); + if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd'); - if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool") && + if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) && 2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) { - bool is_and = cell->type == "$reduce_and"; + bool is_and = cell->type == ID($reduce_and); string bits(GetSize(cell->getPort(ID::A)), is_and ? '1' : '0'); return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b'); } - if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true); - if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false); - if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false); - if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false); - if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false); + if (cell->type == ID($reduce_and)) return export_reduce(cell, "(and A)", true); + if (cell->type == ID($reduce_or)) return export_reduce(cell, "(or A)", false); + if (cell->type == ID($reduce_xor)) return export_reduce(cell, "(xor A)", false); + if (cell->type == ID($reduce_xnor)) return export_reduce(cell, "(not (xor A))", false); + if (cell->type == ID($reduce_bool)) return export_reduce(cell, "(or A)", false); - if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false); - if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false); - if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false); + if (cell->type == ID($logic_not)) return export_reduce(cell, "(not (or A))", false); + if (cell->type == ID($logic_and)) return export_reduce(cell, "(and (or A) (or B))", false); + if (cell->type == ID($logic_or)) return export_reduce(cell, "(or A B)", false); - if (cell->type.in("$mux", "$pmux")) + if (cell->type.in(ID($mux), ID($pmux))) { int width = GetSize(cell->getPort(ID::Y)); std::string processed_expr = get_bv(cell->getPort(ID::A)); @@ -637,19 +637,19 @@ struct Smt2Worker // FIXME: $slice $concat } - if (memmode && cell->type == "$mem") + if (memmode && cell->type == ID($mem)) { int arrayid = idcounter++; memarrays[cell] = arrayid; - int abits = cell->getParam("\\ABITS").as_int(); - int width = cell->getParam("\\WIDTH").as_int(); - int rd_ports = cell->getParam("\\RD_PORTS").as_int(); - int wr_ports = cell->getParam("\\WR_PORTS").as_int(); + int abits = cell->getParam(ID::ABITS).as_int(); + int width = cell->getParam(ID::WIDTH).as_int(); + int rd_ports = cell->getParam(ID::RD_PORTS).as_int(); + int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); bool async_read = false; - if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) { - if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero()) + if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { + if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()) log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); async_read = true; } @@ -665,8 +665,8 @@ struct Smt2Worker if (statebv) { - int mem_size = cell->getParam("\\SIZE").as_int(); - int mem_offset = cell->getParam("\\OFFSET").as_int(); + int mem_size = cell->getParam(ID::SIZE).as_int(); + int mem_offset = cell->getParam(ID::OFFSET).as_int(); makebits(memstate, width*mem_size, get_id(cell)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n", @@ -674,11 +674,11 @@ struct Smt2Worker for (int i = 0; i < rd_ports; i++) { - SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits); - SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width); + SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); + SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); std::string addr = get_bv(addr_sig); - if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool()) + if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module)); @@ -717,11 +717,11 @@ struct Smt2Worker for (int i = 0; i < rd_ports; i++) { - SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits); - SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width); + SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); + SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); std::string addr = get_bv(addr_sig); - if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool()) + if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module)); @@ -801,9 +801,9 @@ struct Smt2Worker pool<SigBit> reg_bits; for (auto cell : module->cells()) - if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) { + if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { // not using sigmap -- we want the net directly at the dff output - for (auto bit : cell->getPort("\\Q")) + for (auto bit : cell->getPort(ID::Q)) reg_bits.insert(bit); } @@ -812,7 +812,7 @@ struct Smt2Worker for (auto bit : SigSpec(wire)) if (reg_bits.count(bit)) is_register = true; - if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) { + if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) { RTLIL::SigSpec sig = sigmap(wire); if (wire->port_input) decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); @@ -820,7 +820,7 @@ struct Smt2Worker decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); if (is_register) decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); - if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) + if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), @@ -854,9 +854,9 @@ struct Smt2Worker vector<string> init_list; for (auto wire : module->wires()) - if (wire->attributes.count("\\init")) { + if (wire->attributes.count(ID::init)) { RTLIL::SigSpec sig = sigmap(wire); - Const val = wire->attributes.at("\\init"); + Const val = wire->attributes.at(ID::init); val.bits.resize(GetSize(sig), State::Sx); if (bvmode && GetSize(sig) > 1) { Const mask(State::S1, GetSize(sig)); @@ -885,31 +885,31 @@ struct Smt2Worker for (auto cell : module->cells()) { - if (cell->type.in("$assert", "$assume", "$cover")) + if (cell->type.in(ID($assert), ID($assume), ID($cover))) { - int &id = cell->type == "$assert" ? assert_id : - cell->type == "$assume" ? assume_id : - cell->type == "$cover" ? cover_id : *(int*)nullptr; + int &id = cell->type == ID($assert) ? assert_id : + cell->type == ID($assume) ? assume_id : + cell->type == ID($cover) ? cover_id : *(int*)nullptr; - char postfix = cell->type == "$assert" ? 'a' : - cell->type == "$assume" ? 'u' : - cell->type == "$cover" ? 'c' : 0; + char postfix = cell->type == ID($assert) ? 'a' : + cell->type == ID($assume) ? 'u' : + cell->type == ID($cover) ? 'c' : 0; string name_a = get_bool(cell->getPort(ID::A)); - string name_en = get_bool(cell->getPort("\\EN")); + string name_en = get_bool(cell->getPort(ID::EN)); string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell); decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); - if (cell->type == "$cover") + if (cell->type == ID($cover)) decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); else decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); - if (cell->type == "$assert") + if (cell->type == ID($assert)) assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id)); - else if (cell->type == "$assume") + else if (cell->type == ID($assume)) assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id)); id++; @@ -965,44 +965,44 @@ struct Smt2Worker for (auto cell : this_regs) { - if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_")) + if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { - std::string expr_d = get_bool(cell->getPort("\\D")); - std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state"); - trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); - ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str())); + std::string expr_d = get_bool(cell->getPort(ID::D)); + std::string expr_q = get_bool(cell->getPort(ID::Q), "next_state"); + trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q)))); + ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str())); } - if (cell->type.in("$ff", "$dff")) + if (cell->type.in(ID($ff), ID($dff))) { - std::string expr_d = get_bv(cell->getPort("\\D")); - std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state"); - trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); - ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str())); + std::string expr_d = get_bv(cell->getPort(ID::D)); + std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state"); + trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q)))); + ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Q)).c_str(), get_bv(cell->getPort(ID::Q), "other_state").c_str())); } - if (cell->type.in("$anyconst", "$allconst")) + if (cell->type.in(ID($anyconst), ID($allconst))) { std::string expr_d = get_bv(cell->getPort(ID::Y)); std::string expr_q = get_bv(cell->getPort(ID::Y), "next_state"); trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Y)))); - if (cell->type == "$anyconst") + if (cell->type == ID($anyconst)) ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str())); } - if (cell->type == "$mem") + if (cell->type == ID($mem)) { int arrayid = memarrays.at(cell); - int abits = cell->getParam("\\ABITS").as_int(); - int width = cell->getParam("\\WIDTH").as_int(); - int wr_ports = cell->getParam("\\WR_PORTS").as_int(); + int abits = cell->getParam(ID::ABITS).as_int(); + int width = cell->getParam(ID::WIDTH).as_int(); + int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); bool async_read = false; string initial_memstate, final_memstate; - if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) { - log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero()); + if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { + log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()); async_read = true; initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); final_memstate = stringf("%s#%d#final", get_id(module), arrayid); @@ -1010,8 +1010,8 @@ struct Smt2Worker if (statebv) { - int mem_size = cell->getParam("\\SIZE").as_int(); - int mem_offset = cell->getParam("\\OFFSET").as_int(); + int mem_size = cell->getParam(ID::SIZE).as_int(); + int mem_offset = cell->getParam(ID::OFFSET).as_int(); if (async_read) { makebits(final_memstate, width*mem_size, get_id(cell)); @@ -1019,9 +1019,9 @@ struct Smt2Worker for (int i = 0; i < wr_ports; i++) { - SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits); - SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width); - SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width); + SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); + SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); + SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); std::string addr = get_bv(addr_sig); std::string data = get_bv(data_sig); @@ -1066,9 +1066,9 @@ struct Smt2Worker for (int i = 0; i < wr_ports; i++) { - SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits); - SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width); - SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width); + SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); + SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); + SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); std::string addr = get_bv(addr_sig); std::string data = get_bv(data_sig); @@ -1104,8 +1104,8 @@ struct Smt2Worker if (async_read) hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell))); - Const init_data = cell->getParam("\\INIT"); - int memsize = cell->getParam("\\SIZE").as_int(); + Const init_data = cell->getParam(ID::INIT); + int memsize = cell->getParam(ID::SIZE).as_int(); for (int i = 0; i < memsize; i++) { @@ -1540,7 +1540,7 @@ struct Smt2Backend : public Backend { for (auto module : sorted_modules) for (auto cell : module->cells()) - if (cell->type.in("$allconst", "$allseq")) + if (cell->type.in(ID($allconst), ID($allseq))) goto found_forall; if (0) { found_forall: |