Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor

added case for memwr cell that is used in muxes (same cell is used more than one time)
corrected bug for xnor and logic_not
added pmux cell translation

Conflicts:
	backends/btor/btor.cc

diff --cc backends/btor/btor.cc
index abe09943a0e88acad9499aab34c2cffb6273f3f7,3482faa70a0073f65e342f696ed826d6f2b849e8..8ce5bb5ed36d2a18c4a3d77b941deda06590675a
--- 1/backends/btor/btor.cc
--- 2/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@@ -75,10 -74,9 +74,10 @@@ struct BtorDumpe
        std::string str;//temp string for writing file
        std::map<RTLIL::IdString, bool> basic_wires;//input wires and registers 
        RTLIL::IdString curr_cell; //current cell being dumped
-         std::set<int> mem_next; //if memory (line_number) already has next
-         std::map<std::string, std::string> cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation
-       BtorDumper(FILE *f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
-                       f(f), module(module), design(design), config(config), ct(design), sigmap(module)
+       std::map<std::string, std::string> cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation
 -      BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
 -                      f(f), module(module), design(design), config(config), ct(design), sigmap(module)
++      std::set<int> mem_next; //if memory (line_number) already has next
++      BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
++              f(f), module(module), design(design), config(config), ct(design), sigmap(module)
        {
                line_num=0;
                str.clear();
@@@ -458,12 -458,11 +459,11 @@@
                                {
                                        ++line_num;
                                        str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_xor").c_str(), output_width, l);
-                                       fprintf(f, "%s\n", str.c_str());
-                                         l = line_num;
+                                       f << stringf("%s\n", str.c_str());
                                }               
                                ++line_num;
 -                              str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$not").c_str(), output_width, line_num-1);
 +                              str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$not").c_str(), output_width, l);
-                               fprintf(f, "%s\n", str.c_str());
+                               f << stringf("%s\n", str.c_str());
                                line_ref[cell->name]=line_num;
                        }
                        //binary cells
@@@ -632,51 -631,16 +632,52 @@@
                        {
                                log("writing mux cell\n");
                                int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
-                               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 s = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\S")), 1);
+                               int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
+                               int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
+                               int s = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), 1);
                                ++line_num;
                                str = stringf ("%d %s %d %d %d %d", 
-                                       line_num, cell_type_translation.at(cell->type).c_str(), output_width, s, l2, l1);//if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
-                               fprintf(f, "%s\n", str.c_str());
 -                                      line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, s, l2, l1);//if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
++                                      line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, s, l2, l1);
++                              //if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
+                               f << stringf("%s\n", str.c_str());
                                line_ref[cell->name]=line_num;
                        }
 -                      //registers
 +                      else if(cell->type == "$pmux")
 +                        {
 +                          log("writing pmux cell\n");
 +                          int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
 +                          int select_width = cell->parameters.at(RTLIL::IdString("\\S_WIDTH")).as_int();
-                           int default_case = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\A")), output_width);
-                           int cases = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\B")), output_width*select_width);
-                           int select = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\S")), select_width);
++                          int default_case = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
++                          int cases = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width*select_width);
++                          int select = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), select_width);
 +                          int *c = new int[select_width];
 +                          
 +                          for (int i=0; i<select_width; ++i)
 +                          {
 +                            ++line_num;
 +                            str = stringf ("%d slice 1 %d %d %d", line_num, select, i, i);
-                             fprintf(f, "%s\n", str.c_str());
++                            f << stringf("%s\n", str.c_str());
 +                            c[i] = line_num;
 +                            ++line_num;
 +                            str = stringf ("%d slice %d %d %d %d", line_num, output_width, cases, i*output_width+output_width-1, 
 +                                           i*output_width);
-                             fprintf(f, "%s\n", str.c_str());
++                            f << stringf("%s\n", str.c_str());
 +                          }
 +                          
 +                          ++line_num;
 +                          str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[select_width-1], c[select_width-1]+1, default_case);
-                           fprintf(f, "%s\n", str.c_str());
++                          f << stringf("%s\n", str.c_str());
 +                          
 +                          for (int i=select_width-2; i>=0; --i)
 +                          {
 +                            ++line_num;
 +                            str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[i], c[i]+1, line_num-1);
-                             fprintf(f, "%s\n", str.c_str());
++                            f << stringf("%s\n", str.c_str());
 +                          }
 +
 +                          line_ref[cell->name]=line_num;
 +                        }
-                         //registers
++            //registers
                        else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
                        {
                                //TODO: remodelling fo adff cells
@@@ -761,53 -725,37 +762,53 @@@
                                log("writing memwr cell\n");
                                if (cell->parameters.at("\\CLK_ENABLE").as_bool() == false)
                                        log_error("The btor backen does not support $memwr cells without built-in registers. Run memory_dff (but with -wr_only).\n");
-                               int clk = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\CLK")), 1);
+                               int clk = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
                                bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
-                               int enable = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\EN")), 1);
+                               int enable = dump_sigspec(&cell->getPort(RTLIL::IdString("\\EN")), 1);
                                int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
-                               int address = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\ADDR")), address_width);
-                                 int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
-                               int data = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\DATA")), data_width);
+                               int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
+                               int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
+                               int data = dump_sigspec(&cell->getPort(RTLIL::IdString("\\DATA")), data_width);
                                str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
                                int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
 -                              ++line_num;
 +                              //check if the memory has already next
 +                                auto it = mem_next.find(mem);
 +                                if(it != std::end(mem_next))
 +                                {
 +                                        ++line_num;
 +                                        str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
 +                                        RTLIL::Memory *memory = module->memories.at(RTLIL::IdString(str.c_str()));
 +                                        int address_bits = ceil(log(memory->size)/log(2));
 +                                        str = stringf("%d array %d %d", line_num, memory->width, address_bits);
-                                         fprintf(f, "%s\n", str.c_str());
++                                        f << stringf("%s\n", str.c_str());
 +                                        ++line_num;
 +                                        str = stringf("%d eq 1 %d %d", line_num, mem, line_num - 1);
-                                         fprintf(f, "%s\n", str.c_str());
++                                        f << stringf("%s\n", str.c_str());
 +                                        mem = line_num - 1;
 +                                }
-                                 ++line_num;
++                              ++line_num;
                                if(polarity)
                                        str = stringf("%d one 1", line_num);
                                else
                                        str = stringf("%d zero 1", line_num);
-                               fprintf(f, "%s\n", str.c_str());
+                               f << stringf("%s\n", str.c_str());
                                ++line_num;
                                str = stringf("%d eq 1 %d %d", line_num, clk, line_num-1);      
-                               fprintf(f, "%s\n", str.c_str());
+                               f << stringf("%s\n", str.c_str());
                                ++line_num;
                                str = stringf("%d and 1 %d %d", line_num, line_num-1, enable);  
-                               fprintf(f, "%s\n", str.c_str());
+                               f << stringf("%s\n", str.c_str());
                                ++line_num;
                                str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data);      
-                               fprintf(f, "%s\n", str.c_str());
+                               f << stringf("%s\n", str.c_str());
                                ++line_num;
                                str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2/*enable*/, line_num-1, mem);   
-                               fprintf(f, "%s\n", str.c_str());                                
+                               f << stringf("%s\n", str.c_str());                              
                                ++line_num;
                                str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1);    
-                               fprintf(f, "%s\n", str.c_str());                                
+                               f << stringf("%s\n", str.c_str());                              
 +                              mem_next.insert(mem);
-                                 line_ref[cell->name]=line_num;
+                               line_ref[cell->name]=line_num;
                        }
                        else if(cell->type == "$slice")
                        {

diff --cc backends/btor/verilog2btor.sh
index 870f0a28d15ba478d6c7e6556bf7465358bfe452,870f0a28d15ba478d6c7e6556bf7465358bfe452..ab45b4901bbdea2b71e4377daa1c7a869cb88540
--- 1/backends/btor/verilog2btor.sh
--- 2/backends/btor/verilog2btor.sh
+++ b/backends/btor/verilog2btor.sh
@@@ -17,14 -17,14 +17,14 @@@ FULL_PATH=$(readlink -f $1
  DIR=$(dirname $FULL_PATH)
  
  ./yosys -q -p "
--read_verilog $1; 
++read_verilog -sv $1; 
  hierarchy -top $3; 
  hierarchy -libdir $DIR; 
  hierarchy -check; 
  proc; 
  opt; opt_const -mux_undef; opt;
  rename -hide;;;
--techmap -share_map pmux2mux.v;;
++#techmap -share_map pmux2mux.v;;
  splice; opt;
  memory_dff -wr_only;
  memory_collect;;