mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-28 15:07:58 +00:00
kernel: big fat patch to use more ID::*, otherwise ID(*)
This commit is contained in:
parent
2d86563bb2
commit
956ecd48f7
152 changed files with 4503 additions and 4391 deletions
|
@ -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:
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue