From e8f6b8f201c0ead8c17f9c9ae4de3e859e9e13ef Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Tue, 11 Feb 2014 13:06:01 +0100 Subject: [PATCH] added concat and slice cell translation --- backends/btor/btor.cc | 87 ++++++++++++++++++++++------------- backends/btor/btor.ys | 4 +- backends/btor/verilog2btor.sh | 4 +- 3 files changed, 59 insertions(+), 36 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 80a2da1fb..2c8546f05 100644 --- 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; ichunks.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 20bce87e1..e58db8a38 100644 --- 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 06a32c81d..6485b6db8 100755 --- 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; -- 2.30.2