diff options
Diffstat (limited to 'backends/btor/btor.cc')
| -rw-r--r-- | backends/btor/btor.cc | 49 |
1 files changed, 40 insertions, 9 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 866bfe52..8377b259 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -96,13 +96,16 @@ struct BtorDumper } curr_cell.clear(); cell_type_translation = { + //assert + {"$assert","root"}, //unary {"$not","not"},{"$neg","neg"},{"$reduce_and","redand"}, {"$reduce_or","redor"},{"$reduce_xor","redxor"},{"$reduce_bool","redor"}, //binary {"$and","and"},{"$or","or"},{"$xor","xor"},{"$xnor","xnor"}, {"$shr","srl"},{"$shl","sll"},{"$sshr","sra"},{"$sshl","sll"}, - {"$lt","ult"},{"$le","ulte"},{"$eq","eq"},{"$ne","ne"},{"$gt","ugt"},{"$ge","ugte"}, + {"$lt","ult"},{"$le","ulte"},{"$gt","ugt"},{"$ge","ugte"}, + {"$eq","eq"},{"$eqx","eq"},{"$ne","ne"},{"$nex","ne"}, {"$add","add"},{"$sub","sub"},{"$mul","mul"},{"$mod","urem"},{"$div","udiv"}, //mux {"$mux","cond"}, @@ -365,6 +368,31 @@ struct BtorDumper if(it==std::end(line_ref)) { curr_cell = cell->name; + //assert cell + if(cell->type == "$assert") + { + log("writing assert cell - %s\n", cstr(cell->type)); + const RTLIL::SigSpec* expr = &cell->connections.at(RTLIL::IdString("\\A")); + const RTLIL::SigSpec* en = &cell->connections.at(RTLIL::IdString("\\EN")); + assert(expr->width == 1); + assert(en->width == 1); + int expr_line = dump_sigspec(expr, 1); + int en_line = dump_sigspec(en, 1); + int one_line = ++line_num; + str = stringf("%d one 1", line_num); + fprintf(f, "%s\n", str.c_str()); + ++line_num; + str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at("$eq").c_str(), 1, en_line, one_line); + fprintf(f, "%s\n", str.c_str()); + ++line_num; + str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), 1, line_num-1, + expr_line, one_line); + fprintf(f, "%s\n", str.c_str()); + int cell_line = ++line_num; + str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, line_num-1); + fprintf(f, "%s\n", str.c_str()); + line_ref[cell->name]=cell_line; + } //unary cells if(cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos" || cell->type == "$reduce_and" || cell->type == "$reduce_or" || cell->type == "$reduce_xor" || cell->type == "$reduce_bool") @@ -417,12 +445,13 @@ struct BtorDumper } //binary cells else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" || - cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || - cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt" ) + cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || + cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" ) { log("writing binary cell - %s\n", cstr(cell->type)); int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int(); - assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt") || output_width == 1); + assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" || + cell->type == "$ge" || cell->type == "$gt") || output_width == 1); bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool(); bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool(); int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int(); @@ -439,7 +468,8 @@ struct BtorDumper ++line_num; std::string op = cell_type_translation.at(cell->type); if(cell->type == "$lt" || cell->type == "$le" || - cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt") + cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" || + cell->type == "$ge" || cell->type == "$gt") { if(l1_signed) op = s_cell_type_translation.at(cell->type); @@ -717,7 +747,7 @@ struct BtorDumper { output_sig = &cell->connections.at(RTLIL::IdString("\\DATA")); } - else if(cell->type == "$memwr") + else if(cell->type == "$memwr" || cell->type == "$assert") { //no output } @@ -884,9 +914,10 @@ struct BtorBackend : public Backend { top_module_name = mod_it.first; fprintf(f, "; Generated by %s\n", yosys_version_str); - fprintf(f, "; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu>\n"); - fprintf(f, "; at Fondazione Bruno Kessler, Trento, Italy\n"); - + fprintf(f, "; %s developed and maintained by Clifford Wolf <clifford@clifford.at>\n", yosys_version_str); + fprintf(f, "; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy\n"); + fprintf(f, ";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n"); + std::vector<RTLIL::Module*> mod_list; for (auto module_it : design->modules) |