added concat and slice cell translation

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 80a2da1fb957f31a06dbcc437e93b883ae22420d..2c8546f05e0dafeb78c8b21eb8379b84563106ee 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -133,6 +133,10 @@ struct BtorDumper
                cell_type_translation["$dffsr"] = "next";
                //memories
                //nothing here
+               //slice
+               cell_type_translation["$slice"] = "slice";
+               //concat
+               cell_type_translation["$concat"] = "concat";
 
                //signed cell type translation 
                //binary
@@ -350,39 +354,25 @@ struct BtorDumper
                if (expected_width != s.width)
                {
                        log(" - changing width of sigspec\n");
-                       //TODO: save the new signal in map
-                       /*if(expected_width > s.width)
-                               s.extend_u0(expected_width);
-                       else if (expected_width < s.width)
-                               s = s.extract(0, expected_width);
-                       
-                       it = sig_ref.find(s);
-                       if(it == std::end(sig_ref))
-                       {*/
-                               if(expected_width > s.width)
-                               {
-                                       //TODO: case the signal is signed
-                                       ++line_num;
-                                       str = stringf ("%d zero %d", line_num, expected_width - s.width);
-                                       fprintf(f, "%s\n", str.c_str());
-                                       ++line_num;
-                                       str = stringf ("%d concat %d %d %d", line_num, expected_width, line_num-1, l);
-                                       fprintf(f, "%s\n", str.c_str());
-                                       l = line_num;
-                               }
-                               else if(expected_width < s.width)
-                               {
-                                       ++line_num;
-                                       str = stringf ("%d slice %d %d %d %d;3", line_num, expected_width, l, expected_width-1, 0);
-                                       fprintf(f, "%s\n", str.c_str());
-                                       l = line_num;
-                               }
-                               /*sig_ref[s] = l;
+                       //TODO: this block may not be needed anymore, due to explicit type conversion by "splice" command
+                       if(expected_width > s.width)
+                       {
+                               //TODO: case the signal is signed
+                               ++line_num;
+                               str = stringf ("%d zero %d", line_num, expected_width - s.width);
+                               fprintf(f, "%s\n", str.c_str());
+                               ++line_num;
+                               str = stringf ("%d concat %d %d %d", line_num, expected_width, line_num-1, l);
+                               fprintf(f, "%s\n", str.c_str());
+                               l = line_num;
                        }
-                       else
+                       else if(expected_width < s.width)
                        {
-                               l = it->second;
-                       }*/
+                               ++line_num;
+                               str = stringf ("%d slice %d %d %d %d;3", line_num, expected_width, l, expected_width-1, 0);
+                               fprintf(f, "%s\n", str.c_str());
+                               l = line_num;
+                       }
                }
                assert(l>0);
                return l;
@@ -657,7 +647,7 @@ struct BtorDumper
                                log(" - width is %d\n", output_width);
                                int cond = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\CLK")), 1);
                                bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
-                               const RTLIL::SigSpec* cell_output = &cell->connections.at(RTLIL::IdString("\\Q"));
+                               const RTLIL::SigSpec* cell_output = &cell->connections.at(RTLIL::IdString("\\D"));
                                int value = dump_sigspec(&cell->connections.at(RTLIL::IdString("\\D")), output_width);
                                unsigned start_bit = 0;
                                for(unsigned i=0; i<cell_output->chunks.size(); ++i)
@@ -765,6 +755,39 @@ struct BtorDumper
                                fprintf(f, "%s\n", str.c_str());                                
                                line_ref[cell->name]=line_num;
                        }
+                       else if(cell->type == "$slice")
+                       {
+                               log("writing slice cell\n");
+                               const RTLIL::SigSpec* input = &cell->connections.at(RTLIL::IdString("\\A"));
+                               int input_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
+                               assert(input->width == input_width);
+                               int input_line = dump_sigspec(input, input_width);
+                               const RTLIL::SigSpec* output = &cell->connections.at(RTLIL::IdString("\\Y"));
+                               int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
+                               assert(output->width == output_width);
+                               int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int(); 
+                               ++line_num;
+                               str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at(cell->type).c_str(), output_width, input_line, output_width+offset-1, offset);    
+                               fprintf(f, "%s\n", str.c_str());                                
+                               line_ref[cell->name]=line_num;  
+                       }
+                       else if(cell->type == "$concat")
+                       {
+                               log("writing concat cell\n");
+                               const RTLIL::SigSpec* input_a = &cell->connections.at(RTLIL::IdString("\\A"));
+                               int input_a_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
+                               assert(input_a->width == input_a_width);
+                               int input_a_line = dump_sigspec(input_a, input_a_width);
+                               const RTLIL::SigSpec* input_b = &cell->connections.at(RTLIL::IdString("\\B"));
+                               int input_b_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
+                               assert(input_b->width == input_b_width);
+                               int input_b_line = dump_sigspec(input_b, input_b_width);
+                               ++line_num;
+                               str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type).c_str(), input_a_width+input_b_width, 
+                                       input_a_line, input_b_line);    
+                               fprintf(f, "%s\n", str.c_str());                                
+                               line_ref[cell->name]=line_num;                          
+                       }
                        curr_cell.clear();
                        return line_num;
                }

diff --git a/backends/btor/btor.ys b/backends/btor/btor.ys
index 20bce87e101c561783e56f82af659fbd6cd6de79..e58db8a385f3822dd2bf0f2443d881424fcf324b 100644 (file)
--- a/backends/btor/btor.ys
+++ b/backends/btor/btor.ys
@@ -1,9 +1,9 @@
 proc; 
-opt; opt_const -mux_undef; opt;
+opt; opt_const -mux_undef; splice; opt;
 rename -hide;;;
 #converting pmux to mux
 techmap -share_map pmux2mux.v;;
-memory -nomap;;
+memory_dff -wr_only; memory_collect;;
 #flatten design
 flatten;;
 #converting asyn memory write to syn memory

diff --git a/backends/btor/verilog2btor.sh b/backends/btor/verilog2btor.sh
index 06a32c81dad0550ea51d110b6859e116521b74d8..6485b6db8c6288a3a2045f87bc68d6c878d0ca0b 100755 (executable)
--- a/backends/btor/verilog2btor.sh
+++ b/backends/btor/verilog2btor.sh
@@ -22,10 +22,10 @@ hierarchy -top $3;
 hierarchy -libdir $DIR; 
 hierarchy -check; 
 proc; 
-opt; opt_const -mux_undef; opt;
+opt; opt_const -mux_undef; splice; opt;
 rename -hide;;;
 techmap -share_map pmux2mux.v;;
-memory_dff -wr_only
+memory_dff -wr_only;
 memory_collect;;
 flatten;;
 memory_unpack;