verilog default options pull

shift operator width issues

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 6ef9c3fc1a2cc6ddb3bdbca6611d9f994ebdd4bd..866bfe52ab87377d3a98b380bb344ac212b6a6da 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -2,7 +2,7 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  Copyright (C) 2014  Ahmed Irfan <ahmedirfan1983@gmail.com>
+ *  Copyright (C) 2014  Ahmed Irfan <irfan@fbk.eu>
  *  
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
@@ -372,7 +372,7 @@ struct BtorDumper
                                log("writing unary cell - %s\n", cstr(cell->type));
                                int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
                                int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
-                               w = w>output_width ? w:output_width;
+                               w = w>output_width ? w:output_width; //padding of w
                                int l = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), w);                         
                                int cell_line = l;
                                if(cell->type != "$pos")
@@ -396,6 +396,7 @@ struct BtorDumper
                                log("writing unary cell - %s\n", cstr(cell->type));
                                int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
                                int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
+                               assert(output_width == 1);
                                int l = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), w);
                                if(cell->type == "$logic_not" && w > 1)
                                {
@@ -416,54 +417,72 @@ struct BtorDumper
                        }
                        //binary cells
                        else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
-                                cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || 
-                                cell->type == "$mod" || cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || 
-                                cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt" || 
-                                cell->type == "$shr" || cell->type == "$shl" || cell->type == "$sshr" || cell->type == "$sshl")
+                                cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || 
+                                cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt" )
                        {
-                               //TODO: division by zero case
                                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);
                                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();
                                int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
-                               if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
-                                cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || 
-                                cell->type == "$mod" || cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || 
-                                cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt")
-                               {
-                                       l1_width = l1_width > output_width ? l1_width : output_width;                                   
-                                       l1_width = l1_width > l2_width ? l1_width : l2_width;
-                                       l2_width = l2_width > l1_width ? l2_width : l1_width;
-                               }
-                               else if(cell->type == "$shr" || cell->type == "$shl" || cell->type == "$sshr" || cell->type == "$sshl")
-                               {
-                                       //TODO: second operand width greater than the log_2(width of the first operand)
-                                       assert(l2_width <= ceil(log(l1_width)/log(2)) );
-                                       l2_width = ceil(log(l1_width)/log(2));                          
-                               }
+                               
+                               assert(l1_signed == l2_signed);
+                               l1_width = l1_width > output_width ? l1_width : output_width;                                   
+                               l1_width = l1_width > l2_width ? l1_width : l2_width;
+                               l2_width = l2_width > l1_width ? l2_width : l1_width;
+
                                int l1 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), l1_width);
                                int l2 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\B")), l2_width);
+                               
                                ++line_num;
                                std::string op = cell_type_translation.at(cell->type);
-                               if(cell->type == "$div" || 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")
                                {
-                                       assert(l1_signed == l2_signed);
                                        if(l1_signed)
                                                op = s_cell_type_translation.at(cell->type);
                                }
-                               if(cell->type == "$mod")
+                               
+                               str = stringf ("%d %s %d %d %d", line_num, op.c_str(), output_width, l1, l2);
+                               fprintf(f, "%s\n", str.c_str());
+
+                               line_ref[cell->name]=line_num;
+                       }
+                       else if(cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || 
+                                cell->type == "$mod" )
+                       {
+                               //TODO: division by zero case
+                               log("writing binary cell - %s\n", cstr(cell->type));
+                               int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
+                               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();
+                               int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+                               
+                               assert(l1_signed == l2_signed);
+                               l1_width = l1_width > output_width ? l1_width : output_width;                                   
+                               l1_width = l1_width > l2_width ? l1_width : l2_width;
+                               l2_width = l2_width > l1_width ? l2_width : l1_width;
+
+                               int l1 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), l1_width);
+                               int l2 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\B")), l2_width);
+                               
+                               ++line_num;
+                               std::string op = cell_type_translation.at(cell->type);
+                               if(cell->type == "$div" && l1_signed)
+                                       op = s_cell_type_translation.at(cell->type);
+                               else if(cell->type == "$mod")
                                {
                                        if(l1_signed)
                                                op = s_cell_type_translation.at("$modx");
                                        else if(l2_signed)
                                                op = s_cell_type_translation.at("$mody");
                                }
-                               str = stringf ("%d %s %d %d %d", 
-                                       line_num, op.c_str(), output_width, l1, l2);
+                               str = stringf ("%d %s %d %d %d", line_num, op.c_str(), l1_width, l1, l2);
                                fprintf(f, "%s\n", str.c_str());
+
                                if(output_width < l1_width)
                                {
                                        ++line_num;
@@ -472,10 +491,58 @@ struct BtorDumper
                                }
                                line_ref[cell->name]=line_num;
                        }
+                       else if(cell->type == "$shr" || cell->type == "$shl" || cell->type == "$sshr" || cell->type == "$sshl")
+                       {
+                               log("writing binary cell - %s\n", cstr(cell->type));
+                               int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
+                               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();
+                               l1_width = pow(2, ceil(log(l1_width)/log(2)));
+                               int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+                               //assert(l2_width <= ceil(log(l1_width)/log(2)) );
+                               int l1 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), l1_width);
+                               int l2 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\B")), ceil(log(l1_width)/log(2)));
+                               int cell_output = ++line_num;
+                               str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type).c_str(), l1_width, l1, l2);
+                               fprintf(f, "%s\n", str.c_str());
+
+                               if(l2_width > ceil(log(l1_width)/log(2)))
+                               {
+                                       int extra_width = l2_width - ceil(log(l1_width)/log(2));
+                                       l2 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\B")), l2_width);
+                                       ++line_num;
+                                       str = stringf ("%d slice %d %d %d %d;6", line_num, extra_width, l2, l2_width-1, l2_width-extra_width);
+                                       fprintf(f, "%s\n", str.c_str());
+                                       ++line_num;
+                                       str = stringf ("%d one %d", line_num, extra_width);
+                                       fprintf(f, "%s\n", str.c_str());
+                                       int mux = ++line_num;
+                                       str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$gt").c_str(), 1, line_num-2, line_num-1);
+                                       fprintf(f, "%s\n", str.c_str());
+                                       ++line_num;
+                                       str = stringf("%d %s %d", line_num, l1_signed && cell->type == "$sshr" ? "ones":"zero", l1_width);
+                                       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(), l1_width, mux, line_num-1, cell_output);
+                                       fprintf(f, "%s\n", str.c_str());
+                                       cell_output = line_num;
+                               }
+
+                               if(output_width < l1_width)
+                               {
+                                       ++line_num;
+                                       str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, cell_output, output_width-1, 0);
+                                       fprintf(f, "%s\n", str.c_str());
+                                       cell_output = line_num;
+                               }
+                               line_ref[cell->name] = cell_output;     
+                       }
                        else if(cell->type == "$logic_and" || cell->type == "$logic_or")//no direct translation in btor
                        {
                                log("writing binary cell - %s\n", cstr(cell->type));
                                int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
+                               assert(output_width == 1);
                                int l1 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), output_width);
                                int l2 = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\B")), output_width);
                                int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
@@ -524,6 +591,7 @@ struct BtorDumper
                        //registers
                        else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
                        {
+                               //TODO: remodelling fo adff cells
                                log("writing cell - %s\n", cstr(cell->type));
                                int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
                                log(" - width is %d\n", output_width);
@@ -816,7 +884,8 @@ struct BtorBackend : public Backend {
                                        top_module_name = mod_it.first;
 
                fprintf(f, "; Generated by %s\n", yosys_version_str);
-               fprintf(f, "; BTOR Backend developed at FBK\n");
+               fprintf(f, "; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu>\n");
+               fprintf(f, ";  at Fondazione Bruno Kessler, Trento, Italy\n");
 
                std::vector<RTLIL::Module*> mod_list;
 

diff --git a/btor.ys b/btor.ys
index 5293ed63b28b2b5fa1a06f26f54fa48ac0f1c91d..65accc95c80b2e24dae838b1be184e2ab46f92f9 100644 (file)
--- a/btor.ys
+++ b/btor.ys
@@ -1,4 +1,6 @@
 #design should be loaded before executing 
+#set the: hierarchy -top <module_top>
+#set the: hierarchy -libdir <dir>
 
 #high level synthesis
 #################
@@ -7,13 +9,12 @@ proc;
 opt; opt_const -mux_undef; opt;
 rename -hide;;;
 #converting pmux to mux
-techmap -map techlibs/common/pmux2mux.v;
-opt;
-#converting asyn memory write to syn memory
-memory_dff; 
-opt;
+techmap -map techlibs/common/pmux2mux.v;;
+memory -nomap;;
 #flatten design
-flatten;;;
+flatten;;
+#converting asyn memory write to syn memory
+memory_unpack; 
 #cell output to be a single wire
 splitnets -driver;
 opt;;;