riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

assert feature

This commit is contained in:
Ahmed Irfan 2014-01-20 10:45:02 +01:00
parent b7adf4c7a0
commit c347f2825f
1 changed files with 40 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
backends/btor/btor.cc
View File

@ -96,13 +96,16 @@ struct BtorDumper
} }
curr_cell.clear(); curr_cell.clear();
cell_type_translation = { cell_type_translation = {
//assert
{"$assert","root"},
//unary //unary
{"$not","not"},{"$neg","neg"},{"$reduce_and","redand"}, {"$not","not"},{"$neg","neg"},{"$reduce_and","redand"},
{"$reduce_or","redor"},{"$reduce_xor","redxor"},{"$reduce_bool","redor"}, {"$reduce_or","redor"},{"$reduce_xor","redxor"},{"$reduce_bool","redor"},
//binary //binary
{"$and","and"},{"$or","or"},{"$xor","xor"},{"$xnor","xnor"}, {"$and","and"},{"$or","or"},{"$xor","xor"},{"$xnor","xnor"},
{"$shr","srl"},{"$shl","sll"},{"$sshr","sra"},{"$sshl","sll"}, {"$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"}, {"$add","add"},{"$sub","sub"},{"$mul","mul"},{"$mod","urem"},{"$div","udiv"},
//mux //mux
{"$mux","cond"}, {"$mux","cond"},
@ -365,6 +368,31 @@ struct BtorDumper
if(it==std::end(line_ref)) if(it==std::end(line_ref))
{ {
curr_cell = cell->name; 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 //unary cells
if(cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos" || cell->type == "$reduce_and" || 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") cell->type == "$reduce_or" || cell->type == "$reduce_xor" || cell->type == "$reduce_bool")
@ -417,12 +445,13 @@ struct BtorDumper
} }
//binary cells //binary cells
else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" || 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 == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt" ) cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" )
{ {
log("writing binary cell - %s\n", cstr(cell->type)); log("writing binary cell - %s\n", cstr(cell->type));
int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int(); 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 l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_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(); int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
@ -439,7 +468,8 @@ struct BtorDumper
++line_num; ++line_num;
std::string op = cell_type_translation.at(cell->type); std::string op = cell_type_translation.at(cell->type);
if(cell->type == "$lt" || cell->type == "$le" || 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) if(l1_signed)
op = s_cell_type_translation.at(cell->type); op = s_cell_type_translation.at(cell->type);
@ -717,7 +747,7 @@ struct BtorDumper
{ {
output_sig = &cell->connections.at(RTLIL::IdString("\\DATA")); output_sig = &cell->connections.at(RTLIL::IdString("\\DATA"));
} }
else if(cell->type == "$memwr") else if(cell->type == "$memwr" || cell->type == "$assert")
{ {
//no output //no output
} }
@ -884,9 +914,10 @@ struct BtorBackend : public Backend {
top_module_name = mod_it.first; top_module_name = mod_it.first;
fprintf(f, "; Generated by %s\n", yosys_version_str); fprintf(f, "; Generated by %s\n", yosys_version_str);
fprintf(f, "; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu>\n"); fprintf(f, "; %s developed and maintained by Clifford Wolf <clifford@clifford.at>\n", yosys_version_str);
fprintf(f, "; at Fondazione Bruno Kessler, Trento, Italy\n"); 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; std::vector<RTLIL::Module*> mod_list;
for (auto module_it : design->modules) for (auto module_it : design->modules)