mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-09-22 01:11:28 +00:00
Code Activity

Remove .c_str() from stringf parameters

Browse source
This commit is contained in:
Robert O'Callahan 2025-08-19 22:45:26 +00:00
parent c41ba912d8
commit c7df6954b9
90 changed files with 773 additions and 773 deletions
Download patch file Download diff file Expand all files Collapse all files

64
backends/smt2/smt2.cc
View file

@ -82,27 +82,27 @@ struct Smt2Worker
if (statebv)
{
if (width == 0) {
decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name.c_str(), get_id(module), statebv_width, statebv_width);
decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name, get_id(module), statebv_width, statebv_width);
statebv_width += 1;
} else {
decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name.c_str(), get_id(module), width, statebv_width+width-1, statebv_width);
decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name, get_id(module), width, statebv_width+width-1, statebv_width);
statebv_width += width;
}
}
else if (statedt)
{
if (width == 0) {
decl_str = stringf(" (|%s| Bool)", name.c_str());
decl_str = stringf(" (|%s| Bool)", name);
} else {
decl_str = stringf(" (|%s| (_ BitVec %d))", name.c_str(), width);
decl_str = stringf(" (|%s| (_ BitVec %d))", name, width);
}
}
else
{
if (width == 0) {
decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module));
decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name, get_id(module));
} else {
decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width);
decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name, get_id(module), width);
}
}
@ -383,7 +383,7 @@ struct Smt2Worker
}
if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) {
subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str()));
subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name)));
continue;
}
@ -495,7 +495,7 @@ struct Smt2Worker
}
if (width != GetSize(sig_y) && type != 'b')
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr);
if (verbose)
log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
@ -617,7 +617,7 @@ struct Smt2Worker
string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
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(QY)), infostr.c_str()));
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(QY)), infostr));
if (cell->getPort(QY).is_wire() && cell->getPort(QY).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(QY).as_wire()->name.str().c_str());
@ -722,7 +722,7 @@ struct Smt2Worker
2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
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');
return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits), 'b');
}
if (cell->type == ID($reduce_and)) return export_reduce(cell, "(and A)", true);
@ -746,7 +746,7 @@ struct Smt2Worker
get_bv(sig_s);
for (int i = 0; i < GetSize(sig_s); i++)
processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]),
get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
if (verbose)
@ -1090,13 +1090,13 @@ struct Smt2Worker
use_mask = true;
}
if (use_mask)
init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire)));
init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig), mask.as_string(), val.as_string(), get_id(wire)));
else
init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig), val.as_string(), get_id(wire)));
} else {
for (int i = 0; i < GetSize(sig); i++)
if (val[i] == State::S0 || val[i] == State::S1)
init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]), val[i] == State::S1 ? "true" : "false", get_id(wire)));
}
}
@ -1131,7 +1131,7 @@ struct Smt2Worker
}
if (private_name && cell->attributes.count(ID::src))
decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str()));
decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string()));
else
decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell)));
@ -1180,11 +1180,11 @@ struct Smt2Worker
SigSpec sig = sigmap(conn.second);
if (bvmode || GetSize(w) == 1) {
hier.push_back(stringf(" (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
hier.push_back(stringf(" (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)),
get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
} else {
for (int i = 0; i < GetSize(w); i++)
hier.push_back(stringf(" (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
hier.push_back(stringf(" (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]),
get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
}
}
@ -1204,25 +1204,25 @@ struct Smt2Worker
{
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()));
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d, expr_q, get_id(cell), log_signal(cell->getPort(ID::Q))));
ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)), get_bool(cell->getPort(ID::Q), "other_state")));
}
if (cell->type.in(ID($ff), ID($dff), ID($anyinit)))
{
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()));
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d, expr_q, get_id(cell), log_signal(cell->getPort(ID::Q))));
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Q)), get_bv(cell->getPort(ID::Q), "other_state")));
}
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))));
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d, expr_q, get_id(cell), log_signal(cell->getPort(ID::Y))));
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()));
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)), get_bv(cell->getPort(ID::Y), "other_state")));
}
}
@ -1341,11 +1341,11 @@ struct Smt2Worker
std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports));
std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid)));
trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d, expr_q, get_id(mem->memid)));
ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
if (has_async_wr)
hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid)));
hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d, final_memstate, get_id(mem->memid)));
Const init_data = mem->get_init_data();
@ -1402,7 +1402,7 @@ struct Smt2Worker
expr = "\n " + ex_state_eq.front() + "\n";
} else {
for (auto &str : ex_state_eq)
expr += stringf("\n %s", str.c_str());
expr += stringf("\n %s", str);
expr += "\n)";
}
}
@ -1415,7 +1415,7 @@ struct Smt2Worker
expr = "\n " + ex_input_eq.front() + "\n";
} else {
for (auto &str : ex_input_eq)
expr += stringf("\n %s", str.c_str());
expr += stringf("\n %s", str);
expr += "\n)";
}
}
@ -1429,7 +1429,7 @@ struct Smt2Worker
assert_expr = "\n " + assert_list.front() + "\n";
} else {
for (auto &str : assert_list)
assert_expr += stringf("\n %s", str.c_str());
assert_expr += stringf("\n %s", str);
assert_expr += "\n)";
}
}
@ -1442,7 +1442,7 @@ struct Smt2Worker
assume_expr = "\n " + assume_list.front() + "\n";
} else {
for (auto &str : assume_list)
assume_expr += stringf("\n %s", str.c_str());
assume_expr += stringf("\n %s", str);
assume_expr += "\n)";
}
}
@ -1455,7 +1455,7 @@ struct Smt2Worker
init_expr = "\n " + init_list.front() + "\n";
} else {
for (auto &str : init_list)
init_expr += stringf("\n %s", str.c_str());
init_expr += stringf("\n %s", str);
init_expr += "\n)";
}
}
@ -1846,7 +1846,7 @@ struct Smt2Backend : public Backend {
*f << stringf("; yosys-smt2-stdt\n");
for (auto &it : solver_options)
*f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str());
*f << stringf("; yosys-smt2-solver-option %s %s\n", it.first, it.second);
std::vector<RTLIL::Module*> sorted_modules;
@ -1913,7 +1913,7 @@ struct Smt2Backend : public Backend {
}
if (topmod)
*f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str());
*f << stringf("; yosys-smt2-topmod %s\n", topmod_id);
*f << stringf("; end of yosys output\n");