summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAhmed Irfan <irfan@ubuntu.(none)>2014-02-11 13:06:01 +0100
committerAhmed Irfan <irfan@ubuntu.(none)>2014-02-11 13:06:01 +0100
commite8f6b8f201c0ead8c17f9c9ae4de3e859e9e13ef (patch)
tree5ba60416a07c5c0a273440d0a49beaa1b307ef1b
parentfb186e6299f9e26f0011c9623f10adcf8eadb304 (diff)
added concat and slice cell translation
-rw-r--r--backends/btor/btor.cc87
-rw-r--r--backends/btor/btor.ys4
-rwxr-xr-xbackends/btor/verilog2btor.sh4
3 files changed, 59 insertions, 36 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 80a2da1f..2c8546f0 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; 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 20bce87e..e58db8a3 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 06a32c81..6485b6db 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;