assert feature

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 866bfe52ab87377d3a98b380bb344ac212b6a6da..8377b25917e1840eabaed4af09299bd4a71c1102 100644 (file)
--- 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)