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"))
+ {
+ SigSpec clk = sigmap(conn.second);
+ for (int i = 0; i < GetSize(clk); i++)
+ {
+ if (clk[i].wire == nullptr)
+ continue;
+
+ if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1)
+ continue;
+
+ if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\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"))
{
bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
if (type == 's' || type == 'd' || type == 'b') {
width = max(width, GetSize(cell->getPort("\\A")));
- width = max(width, GetSize(cell->getPort("\\B")));
+ if (cell->hasPort("\\B"))
+ width = max(width, GetSize(cell->getPort("\\B")));
}
if (cell->hasPort("\\A")) {
for (char ch : expr) {
if (ch == 'A') processed_expr += get_bv(sig_a);
else if (ch == 'B') processed_expr += get_bv(sig_b);
+ else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
else processed_expr += ch;
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->attributes.count("\\reg"))
infostr += " " + cell->attributes.at("\\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("\\Y")), infostr.c_str()));
+ if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){
+ decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
+ log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+ }
+ else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){
+ decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
+ log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
if (cell->type == "$anyseq")
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
if (cell->type.in("$shift", "$shiftx")) {
if (cell->getParam("\\B_SIGNED").as_bool()) {
- /* FIXME */
+ return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
+ "(bvlshr A B) (bvlshr A (bvneg B)))",
+ GetSize(cell->getPort("\\B")), 0), 's');
} else {
return export_bvop(cell, "(bvlshr A B)", 's');
}
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.in("$reduce_and", "$reduce_or", "$reduce_bool") &&
+ 2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) {
+ bool is_and = cell->type == "$reduce_and";
+ string bits(GetSize(cell->getPort("\\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 == "$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 == "$mux" || cell->type == "$pmux")
+ if (cell->type.in("$mux", "$pmux"))
{
int width = GetSize(cell->getPort("\\Y"));
std::string processed_expr = get_bv(cell->getPort("\\A"));
if (statebv)
makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
- if (statedt)
+ else if (statedt)
dtmembers.push_back(stringf(" (|%s_h %s| |%s_s|)\n",
get_id(module), get_id(cell->name), get_id(cell->type)));
else
string name_a = get_bool(cell->getPort("\\A"));
string name_en = get_bool(cell->getPort("\\EN"));
- decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
- cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+ string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\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")
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
break;
Const initword = init_data.extract(i*width, width, State::Sx);
+ Const initmask = initword;
bool gen_init_constr = false;
- for (auto bit : initword.bits)
- if (bit == State::S0 || bit == State::S1)
+ for (int k = 0; k < GetSize(initword); k++) {
+ if (initword[k] == State::S0 || initword[k] == State::S1) {
gen_init_constr = true;
+ initmask[k] = State::S1;
+ } else {
+ initmask[k] = State::S0;
+ initword[k] = State::S0;
+ }
+ }
if (gen_init_constr)
{
if (statebv)
/* FIXME */;
else
- init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+ init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
get_id(module), arrayid, Const(i, abits).as_string().c_str(),
- initword.as_string().c_str(), get_id(cell), i));
+ initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
}
}
}
struct Smt2Backend : public Backend {
Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
- virtual void help()
+ void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log("from non-zero to zero in the test design.\n");
log("\n");
}
- virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
std::ifstream template_f;
bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
int indent = 0;
while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
indent++;
- if (line.substr(indent, 2) == "%%")
+ if (line.compare(indent, 2, "%%") == 0)
break;
*f << line << std::endl;
}
for (auto module : sorted_modules)
{
- if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
+ if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn())
continue;
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
projects / yosys.git / blobdiff