summaryrefslogtreecommitdiff
path: root/backends/btor/btor.cc
diff options
context:
space:
mode:
authorAhmed Irfan <irfan@ubuntu.(none)>2014-01-20 10:45:02 +0100
committerAhmed Irfan <irfan@ubuntu.(none)>2014-01-20 10:45:02 +0100
commitc347f2825f150451e6fb82d3c1d65015cd5405d8 (patch)
tree7d50bd960b5d4dc1ddc0344e06aa3f40daa69374 /backends/btor/btor.cc
parentb7adf4c7a0d0f561d08d7e4dcf66b4e651596318 (diff)
assert feature
Diffstat (limited to 'backends/btor/btor.cc')
-rw-r--r--backends/btor/btor.cc49
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)