backends/btor/btor.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *  Copyright (C) 2014  Ahmed Irfan <irfan@fbk.eu>
   6  *
   7  *  Permission to use, copy, modify, and/or distribute this software for any
   8  *  purpose with or without fee is hereby granted, provided that the above
   9  *  copyright notice and this permission notice appear in all copies.
  10  *
  11  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  12  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  13  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  14  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  15  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  16  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  17  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  18  *
  19  */
  20
  21 // [[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
  22 // Johannes Kepler University, Linz, Austria
  23 // http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
  24
  25 #include "kernel/rtlil.h"
  26 #include "kernel/register.h"
  27 #include "kernel/sigtools.h"
  28 #include "kernel/celltypes.h"
  29 #include "kernel/log.h"
  30 #include <string>
  31 #include <math.h>
  32
  33 USING_YOSYS_NAMESPACE
  34 PRIVATE_NAMESPACE_BEGIN
  35
  36 struct BtorDumperConfig
  37 {
  38         bool subckt_mode;
  39         bool conn_mode;
  40         bool impltf_mode;
  41
  42         std::string buf_type, buf_in, buf_out;
  43         std::string true_type, true_out, false_type, false_out;
  44
  45         BtorDumperConfig() : subckt_mode(false), conn_mode(false), impltf_mode(false) { }
  46 };
  47
  48 struct WireInfo
  49 {
  50         RTLIL::IdString cell_name;
  51         const RTLIL::SigChunk *chunk;
  52
  53         WireInfo(RTLIL::IdString c, const RTLIL::SigChunk* ch) : cell_name(c), chunk(ch) { }
  54 };
  55
  56 struct WireInfoOrder
  57 {
  58         bool operator() (const WireInfo& x, const WireInfo& y)
  59         {
  60                 return x.chunk < y.chunk;
  61         }
  62 };
  63
  64 struct BtorDumper
  65 {
  66         std::ostream &f;
  67         RTLIL::Module *module;
  68         RTLIL::Design *design;
  69         BtorDumperConfig *config;
  70         CellTypes ct;
  71
  72         SigMap sigmap;
  73         std::map<RTLIL::IdString, std::set<WireInfo,WireInfoOrder>> inter_wire_map;//<wire, dependency list> for maping the intermediate wires that are output of some cell
  74         std::map<RTLIL::IdString, int> line_ref;//mapping of ids to line_num of the btor file
  75         std::map<RTLIL::SigSpec, int> sig_ref;//mapping of sigspec to the line_num of the btor file
  76         int line_num;//last line number of btor file
  77         std::string str;//temp string for writing file
  78         std::map<RTLIL::IdString, bool> basic_wires;//input wires and registers
  79         RTLIL::IdString curr_cell; //current cell being dumped
  80         std::map<std::string, std::string> cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation
  81         std::set<int> mem_next; //if memory (line_number) already has next
  82         BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) :
  83                 f(f), module(module), design(design), config(config), ct(design), sigmap(module)
  84         {
  85                 line_num=0;
  86                 str.clear();
  87                 for(auto it=module->wires_.begin(); it!=module->wires_.end(); ++it)
  88                 {
  89                         if(it->second->port_input)
  90                         {
  91                                 basic_wires[it->first]=true;
  92                         }
  93                         else
  94                         {
  95                                 basic_wires[it->first]=false;
  96                         }
  97                         inter_wire_map[it->first].clear();
  98                 }
  99                 curr_cell.clear();
 100                 //assert
 101                 cell_type_translation["$assert"] = "root";
 102                 //unary
 103                 cell_type_translation["$not"] = "not";
 104                 cell_type_translation["$neg"] = "neg";
 105                 cell_type_translation["$reduce_and"] = "redand";
 106                 cell_type_translation["$reduce_or"] = "redor";
 107                 cell_type_translation["$reduce_xor"] = "redxor";
 108                 cell_type_translation["$reduce_bool"] = "redor";
 109                 //binary
 110                 cell_type_translation["$and"] = "and";
 111                 cell_type_translation["$or"] = "or";
 112                 cell_type_translation["$xor"] = "xor";
 113                 cell_type_translation["$xnor"] = "xnor";
 114                 cell_type_translation["$shr"] = "srl";
 115                 cell_type_translation["$shl"] = "sll";
 116                 cell_type_translation["$sshr"] = "sra";
 117                 cell_type_translation["$sshl"] = "sll";
 118                 cell_type_translation["$shift"] = "srl";
 119                 cell_type_translation["$shiftx"] = "srl";
 120                 cell_type_translation["$lt"] = "ult";
 121                 cell_type_translation["$le"] = "ulte";
 122                 cell_type_translation["$gt"] = "ugt";
 123                 cell_type_translation["$ge"] = "ugte";
 124                 cell_type_translation["$eq"] = "eq";
 125                 cell_type_translation["$eqx"] = "eq";
 126                 cell_type_translation["$ne"] = "ne";
 127                 cell_type_translation["$nex"] = "ne";
 128                 cell_type_translation["$add"] = "add";
 129                 cell_type_translation["$sub"] = "sub";
 130                 cell_type_translation["$mul"] = "mul";
 131                 cell_type_translation["$mod"] = "urem";
 132                 cell_type_translation["$div"] = "udiv";
 133                 //mux
 134                 cell_type_translation["$mux"] = "cond";
 135                 //reg
 136                 cell_type_translation["$dff"] = "next";
 137                 cell_type_translation["$adff"] = "next";
 138                 cell_type_translation["$dffsr"] = "next";
 139                 //memories
 140                 //nothing here
 141                 //slice
 142                 cell_type_translation["$slice"] = "slice";
 143                 //concat
 144                 cell_type_translation["$concat"] = "concat";
 145
 146                 //signed cell type translation
 147                 //binary
 148                 s_cell_type_translation["$modx"] = "srem";
 149                 s_cell_type_translation["$mody"] = "smod";
 150                 s_cell_type_translation["$div"] = "sdiv";
 151                 s_cell_type_translation["$lt"] = "slt";
 152                 s_cell_type_translation["$le"] = "slte";
 153                 s_cell_type_translation["$gt"] = "sgt";
 154                 s_cell_type_translation["$ge"] = "sgte";
 155
 156         }
 157
 158         std::vector<std::string> cstr_buf;
 159
 160         const char *cstr(const RTLIL::IdString id)
 161         {
 162                 str = RTLIL::unescape_id(id);
 163                 for (size_t i = 0; i < str.size(); ++i)
 164                         if (str[i] == '#' || str[i] == '=')
 165                                 str[i] = '?';
 166                 cstr_buf.push_back(str);
 167                 return cstr_buf.back().c_str();
 168         }
 169
 170         int dump_wire(RTLIL::Wire* wire)
 171         {
 172                 if(basic_wires[wire->name])
 173                 {
 174                         log("writing wire %s\n", cstr(wire->name));
 175                         auto it = line_ref.find(wire->name);
 176                         if(it==std::end(line_ref))
 177                         {
 178                                 ++line_num;
 179                                 line_ref[wire->name]=line_num;
 180                                 str = stringf("%d var %d %s", line_num, wire->width, cstr(wire->name));
 181                                 f << stringf("%s\n", str.c_str());
 182                                 return line_num;
 183                         }
 184                         else return it->second;
 185                 }
 186                 else // case when the wire is not basic wire
 187                 {
 188                         log("case of non-basic wire - %s\n", cstr(wire->name));
 189                         auto it = line_ref.find(wire->name);
 190                         if(it==std::end(line_ref))
 191                         {
 192                                 std::set<WireInfo, WireInfoOrder>& dep_set = inter_wire_map.at(wire->name);
 193                                 int wire_line = 0;
 194                                 int wire_width = 0;
 195                                 for(auto dep_set_it=dep_set.begin(); dep_set_it!=dep_set.end(); ++dep_set_it)
 196                                 {
 197                                         RTLIL::IdString cell_id = dep_set_it->cell_name;
 198                                         if(cell_id == curr_cell)
 199                                                 break;
 200                                         log(" -- found cell %s\n", cstr(cell_id));
 201                                         RTLIL::Cell* cell = module->cells_.at(cell_id);
 202                                         const RTLIL::SigSpec* cell_output = get_cell_output(cell);
 203                                         int cell_line = dump_cell(cell);
 204
 205                                         if(dep_set.size()==1 && wire->width == cell_output->size())
 206                                         {
 207                                                 wire_line = cell_line;
 208                                                 break;
 209                                         }
 210                                         else
 211                                         {
 212                                                 int prev_wire_line=0; //previously dumped wire line
 213                                                 int start_bit=0;
 214                                                 for(unsigned j=0; j<cell_output->chunks().size(); ++j)
 215                                                 {
 216                                                         start_bit+=cell_output->chunks().at(j).width;
 217                                                         if(cell_output->chunks().at(j).wire->name == wire->name)
 218                                                         {
 219                                                                 prev_wire_line = wire_line;
 220                                                                 wire_line = ++line_num;
 221                                                                 str = stringf("%d slice %d %d %d %d;1", line_num, cell_output->chunks().at(j).width,
 222                                                                         cell_line, start_bit-1, start_bit-cell_output->chunks().at(j).width);
 223                                                                 f << stringf("%s\n", str.c_str());
 224                                                                 wire_width += cell_output->chunks().at(j).width;
 225                                                                 if(prev_wire_line!=0)
 226                                                                 {
 227                                                                         ++line_num;
 228                                                                         str = stringf("%d concat %d %d %d", line_num, wire_width, wire_line, prev_wire_line);
 229                                                                         f << stringf("%s\n", str.c_str());
 230                                                                         wire_line = line_num;
 231                                                                 }
 232                                                         }
 233                                                 }
 234                                         }
 235                                 }
 236                                 if(dep_set.size()==0)
 237                                 {
 238                                         log(" - checking sigmap\n");
 239                                         RTLIL::SigSpec s = RTLIL::SigSpec(wire);
 240                                         wire_line = dump_sigspec(&s, s.size());
 241                                         line_ref[wire->name]=wire_line;
 242                                 }
 243                                 line_ref[wire->name]=wire_line;
 244                                 return wire_line;
 245                         }
 246                         else
 247                         {
 248                                 log(" -- already processed wire\n");
 249                                 return it->second;
 250                         }
 251                 }
 252                 log_abort();
 253                 return -1;
 254         }
 255
 256         int dump_memory(const RTLIL::Memory* memory)
 257         {
 258                 log("writing memory %s\n", cstr(memory->name));
 259                 auto it = line_ref.find(memory->name);
 260                 if(it==std::end(line_ref))
 261                 {
 262                         ++line_num;
 263                         int address_bits = ceil(log(memory->size)/log(2));
 264                         str = stringf("%d array %d %d", line_num, memory->width, address_bits);
 265                         line_ref[memory->name]=line_num;
 266                         f << stringf("%s\n", str.c_str());
 267                         return line_num;
 268                 }
 269                 else return it->second;
 270         }
 271
 272         int dump_const(const RTLIL::Const* data, int width, int offset)
 273         {
 274                 log("writing const \n");
 275                 if((data->flags & RTLIL::CONST_FLAG_STRING) == 0)
 276                 {
 277                         if(width<0)
 278                                 width = data->bits.size() - offset;
 279
 280                         std::string data_str = data->as_string();
 281                         //if(offset > 0)
 282                                 data_str = data_str.substr(offset, width);
 283
 284                         ++line_num;
 285                         str = stringf("%d const %d %s", line_num, width, data_str.c_str());
 286                         f << stringf("%s\n", str.c_str());
 287                         return line_num;
 288                 }
 289                 else
 290                         log("writing const error\n");
 291                 log_abort();
 292                 return -1;
 293         }
 294
 295         int dump_sigchunk(const RTLIL::SigChunk* chunk)
 296         {
 297                 log("writing sigchunk\n");
 298                 int l=-1;
 299                 if(chunk->wire == NULL)
 300                 {
 301                         RTLIL::Const data_const(chunk->data);
 302                         l=dump_const(&data_const, chunk->width, chunk->offset);
 303                 }
 304                 else
 305                 {
 306                         if (chunk->width == chunk->wire->width && chunk->offset == 0)
 307                                 l = dump_wire(chunk->wire);
 308                         else
 309                         {
 310                                 int wire_line_num = dump_wire(chunk->wire);
 311                                 log_assert(wire_line_num>0);
 312                                 ++line_num;
 313                                 str = stringf("%d slice %d %d %d %d;2", line_num, chunk->width, wire_line_num,
 314                                         chunk->width + chunk->offset - 1, chunk->offset);
 315                                 f << stringf("%s\n", str.c_str());
 316                                 l = line_num;
 317                         }
 318                 }
 319                 return l;
 320         }
 321
 322         int dump_sigspec(const RTLIL::SigSpec* sig, int expected_width)
 323         {
 324                 log("writing sigspec\n");
 325                 RTLIL::SigSpec s = sigmap(*sig);
 326                 int l = -1;
 327                 auto it = sig_ref.find(s);
 328                 if(it == std::end(sig_ref))
 329                 {
 330                         if (s.is_chunk())
 331                         {
 332                                 l = dump_sigchunk(&s.chunks().front());
 333                         }
 334                         else
 335                         {
 336                                 int l1, l2, w1, w2;
 337                                 l1 = dump_sigchunk(&s.chunks().front());
 338                                 log_assert(l1>0);
 339                                 w1 = s.chunks().front().width;
 340                                 for (unsigned i=1; i < s.chunks().size(); ++i)
 341                                 {
 342                                         l2 = dump_sigchunk(&s.chunks().at(i));
 343                                         log_assert(l2>0);
 344                                         w2 = s.chunks().at(i).width;
 345                                         ++line_num;
 346                                         str = stringf("%d concat %d %d %d", line_num, w1+w2, l2, l1);
 347                                         f << stringf("%s\n", str.c_str());
 348                                         l1=line_num;
 349                                         w1+=w2;
 350                                 }
 351                                 l = line_num;
 352                         }
 353                         sig_ref[s] = l;
 354                 }
 355                 else
 356                 {
 357                         l = it->second;
 358                 }
 359
 360                 if (expected_width != s.size())
 361                 {
 362                         log(" - changing width of sigspec\n");
 363                         //TODO: this block may not be needed anymore, due to explicit type conversion by "splice" command
 364                         if(expected_width > s.size())
 365                         {
 366                                 //TODO: case the signal is signed
 367                                 ++line_num;
 368                                 str = stringf ("%d zero %d", line_num, expected_width - s.size());
 369                                 f << stringf("%s\n", str.c_str());
 370                                 ++line_num;
 371                                 str = stringf ("%d concat %d %d %d", line_num, expected_width, line_num-1, l);
 372                                 f << stringf("%s\n", str.c_str());
 373                                 l = line_num;
 374                         }
 375                         else if(expected_width < s.size())
 376                         {
 377                                 ++line_num;
 378                                 str = stringf ("%d slice %d %d %d %d;3", line_num, expected_width, l, expected_width-1, 0);
 379                                 f << stringf("%s\n", str.c_str());
 380                                 l = line_num;
 381                         }
 382                 }
 383                 log_assert(l>0);
 384                 return l;
 385         }
 386
 387         int dump_cell(const RTLIL::Cell* cell)
 388         {
 389                 auto it = line_ref.find(cell->name);
 390                 if(it==std::end(line_ref))
 391                 {
 392                         curr_cell = cell->name;
 393                         //assert cell
 394                         if(cell->type == "$assert")
 395                         {
 396                                 log("writing assert cell - %s\n", cstr(cell->type));
 397                                 const RTLIL::SigSpec* expr = &cell->getPort(RTLIL::IdString("\\A"));
 398                                 const RTLIL::SigSpec* en = &cell->getPort(RTLIL::IdString("\\EN"));
 399                                 log_assert(expr->size() == 1);
 400                                 log_assert(en->size() == 1);
 401                                 int expr_line = dump_sigspec(expr, 1);
 402                                 int en_line = dump_sigspec(en, 1);
 403                                 int one_line = ++line_num;
 404                                 str = stringf("%d one 1", line_num);
 405                                 f << stringf("%s\n", str.c_str());
 406                                 ++line_num;
 407                                 str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at("$eq").c_str(), 1, en_line, one_line);
 408                                 f << stringf("%s\n", str.c_str());
 409                                 ++line_num;
 410                                 str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at("$mux").c_str(), 1, line_num-1,
 411                                         expr_line, one_line);
 412                                 f << stringf("%s\n", str.c_str());
 413                                 int cell_line = ++line_num;
 414                                 str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, -1*(line_num-1));
 415                                 //multiplying the line number with -1, which means logical negation
 416                                 //the reason for negative sign is that the properties in btor are given as "negation of the original property"
 417                                 //bug identified by bobosoft
 418                                 //http://www.reddit.com/r/yosys/comments/1w3xig/btor_backend_bug/
 419                                 f << stringf("%s\n", str.c_str());
 420                                 line_ref[cell->name]=cell_line;
 421                         }
 422                         //unary cells
 423                         else if(cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos" || cell->type == "$reduce_and" ||
 424                                 cell->type == "$reduce_or" || cell->type == "$reduce_xor" || cell->type == "$reduce_bool")
 425                         {
 426                                 log("writing unary cell - %s\n", cstr(cell->type));
 427                                 int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 428                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 429                                 w = w>output_width ? w:output_width; //padding of w
 430                                 int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
 431                                 int cell_line = l;
 432                                 if(cell->type != "$pos")
 433                                 {
 434                                         cell_line = ++line_num;
 435                                         bool reduced = (cell->type == "$not" || cell->type == "$neg") ? false : true;
 436                                         str = stringf ("%d %s %d %d", cell_line, cell_type_translation.at(cell->type.str()).c_str(), reduced?output_width:w, l);
 437                                         f << stringf("%s\n", str.c_str());
 438                                 }
 439                                 if(output_width < w && (cell->type == "$not" || cell->type == "$neg" || cell->type == "$pos"))
 440                                 {
 441                                         ++line_num;
 442                                         str = stringf ("%d slice %d %d %d %d;4", line_num, output_width, cell_line, output_width-1, 0);
 443                                         f << stringf("%s\n", str.c_str());
 444                                         cell_line = line_num;
 445                                 }
 446                                 line_ref[cell->name]=cell_line;
 447                         }
 448                         else if(cell->type == "$reduce_xnor" || cell->type == "$logic_not")//no direct translation in btor
 449                         {
 450                                 log("writing unary cell - %s\n", cstr(cell->type));
 451                                 int w = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 452                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 453                                 log_assert(output_width == 1);
 454                                 int l = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), w);
 455                                 if(cell->type == "$logic_not" && w > 1)
 456                                 {
 457                                         ++line_num;
 458                                         str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l);
 459                                         f << stringf("%s\n", str.c_str());
 460                                 }
 461                                 else if(cell->type == "$reduce_xnor")
 462                                 {
 463                                         ++line_num;
 464                                         str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_xor").c_str(), output_width, l);
 465                                         f << stringf("%s\n", str.c_str());
 466                                 }
 467                                 ++line_num;
 468                                 str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$not").c_str(), output_width, l);
 469                                 f << stringf("%s\n", str.c_str());
 470                                 line_ref[cell->name]=line_num;
 471                         }
 472                         //binary cells
 473                         else if(cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
 474                                  cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" ||
 475                                  cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt" )
 476                         {
 477                                 log("writing binary cell - %s\n", cstr(cell->type));
 478                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 479                                 log_assert(!(cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
 480                                         cell->type == "$ge" || cell->type == "$gt") || output_width == 1);
 481                                 bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
 482                                 bool l2_signed YS_ATTRIBUTE(unused) = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
 483                                 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 484                                 int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
 485
 486                                 log_assert(l1_signed == l2_signed);
 487                                 l1_width = l1_width > output_width ? l1_width : output_width;
 488                                 l1_width = l1_width > l2_width ? l1_width : l2_width;
 489                                 l2_width = l2_width > l1_width ? l2_width : l1_width;
 490
 491                                 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
 492                                 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
 493
 494                                 ++line_num;
 495                                 std::string op = cell_type_translation.at(cell->type.str());
 496                                 if(cell->type == "$lt" || cell->type == "$le" ||
 497                                  cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" ||
 498                                  cell->type == "$ge" || cell->type == "$gt")
 499                                 {
 500                                         if(l1_signed)
 501                                                 op = s_cell_type_translation.at(cell->type.str());
 502                                 }
 503
 504                                 str = stringf ("%d %s %d %d %d", line_num, op.c_str(), output_width, l1, l2);
 505                                 f << stringf("%s\n", str.c_str());
 506
 507                                 line_ref[cell->name]=line_num;
 508                         }
 509                         else if(cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" ||
 510                                  cell->type == "$mod" )
 511                         {
 512                                 //TODO: division by zero case
 513                                 log("writing binary cell - %s\n", cstr(cell->type));
 514                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 515                                 bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
 516                                 bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
 517                                 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 518                                 int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
 519
 520                                 log_assert(l1_signed == l2_signed);
 521                                 l1_width = l1_width > output_width ? l1_width : output_width;
 522                                 l1_width = l1_width > l2_width ? l1_width : l2_width;
 523                                 l2_width = l2_width > l1_width ? l2_width : l1_width;
 524
 525                                 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
 526                                 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
 527
 528                                 ++line_num;
 529                                 std::string op = cell_type_translation.at(cell->type.str());
 530                                 if(cell->type == "$div" && l1_signed)
 531                                         op = s_cell_type_translation.at(cell->type.str());
 532                                 else if(cell->type == "$mod")
 533                                 {
 534                                         if(l1_signed)
 535                                                 op = s_cell_type_translation.at("$modx");
 536                                         else if(l2_signed)
 537                                                 op = s_cell_type_translation.at("$mody");
 538                                 }
 539                                 str = stringf ("%d %s %d %d %d", line_num, op.c_str(), l1_width, l1, l2);
 540                                 f << stringf("%s\n", str.c_str());
 541
 542                                 if(output_width < l1_width)
 543                                 {
 544                                         ++line_num;
 545                                         str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, line_num-1, output_width-1, 0);
 546                                         f << stringf("%s\n", str.c_str());
 547                                 }
 548                                 line_ref[cell->name]=line_num;
 549                         }
 550                         else if(cell->type == "$shr" || cell->type == "$shl" || cell->type == "$sshr" || cell->type == "$sshl" || cell->type == "$shift" || cell->type == "$shiftx")
 551                         {
 552                                 log("writing binary cell - %s\n", cstr(cell->type));
 553                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 554                                 bool l1_signed = cell->parameters.at(RTLIL::IdString("\\A_SIGNED")).as_bool();
 555                                 //bool l2_signed = cell->parameters.at(RTLIL::IdString("\\B_SIGNED")).as_bool();
 556                                 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 557                                 l1_width = pow(2, ceil(log(l1_width)/log(2)));
 558                                 int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
 559                                 //log_assert(l2_width <= ceil(log(l1_width)/log(2)) );
 560                                 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), l1_width);
 561                                 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), ceil(log(l1_width)/log(2)));
 562                                 int cell_output = ++line_num;
 563                                 str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), l1_width, l1, l2);
 564                                 f << stringf("%s\n", str.c_str());
 565
 566                                 if(l2_width > ceil(log(l1_width)/log(2)))
 567                                 {
 568                                         int extra_width = l2_width - ceil(log(l1_width)/log(2));
 569                                         l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), l2_width);
 570                                         ++line_num;
 571                                         str = stringf ("%d slice %d %d %d %d;6", line_num, extra_width, l2, l2_width-1, l2_width-extra_width);
 572                                         f << stringf("%s\n", str.c_str());
 573                                         ++line_num;
 574                                         str = stringf ("%d one %d", line_num, extra_width);
 575                                         f << stringf("%s\n", str.c_str());
 576                                         int mux = ++line_num;
 577                                         str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$gt").c_str(), 1, line_num-2, line_num-1);
 578                                         f << stringf("%s\n", str.c_str());
 579                                         ++line_num;
 580                                         str = stringf("%d %s %d", line_num, l1_signed && cell->type == "$sshr" ? "ones":"zero", l1_width);
 581                                         f << stringf("%s\n", str.c_str());
 582                                         ++line_num;
 583                                         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);
 584                                         f << stringf("%s\n", str.c_str());
 585                                         cell_output = line_num;
 586                                 }
 587
 588                                 if(output_width < l1_width)
 589                                 {
 590                                         ++line_num;
 591                                         str = stringf ("%d slice %d %d %d %d;5", line_num, output_width, cell_output, output_width-1, 0);
 592                                         f << stringf("%s\n", str.c_str());
 593                                         cell_output = line_num;
 594                                 }
 595                                 line_ref[cell->name] = cell_output;
 596                         }
 597                         else if(cell->type == "$logic_and" || cell->type == "$logic_or")//no direct translation in btor
 598                         {
 599                                 log("writing binary cell - %s\n", cstr(cell->type));
 600                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 601                                 log_assert(output_width == 1);
 602                                 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
 603                                 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
 604                                 int l1_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 605                                 int l2_width =  cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
 606                                 if(l1_width >1)
 607                                 {
 608                                         ++line_num;
 609                                         str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l1);
 610                                         f << stringf("%s\n", str.c_str());
 611                                         l1 = line_num;
 612                                 }
 613                                 if(l2_width > 1)
 614                                 {
 615                                         ++line_num;
 616                                         str = stringf ("%d %s %d %d", line_num, cell_type_translation.at("$reduce_or").c_str(), output_width, l2);
 617                                         f << stringf("%s\n", str.c_str());
 618                                         l2 = line_num;
 619                                 }
 620                                 if(cell->type == "$logic_and")
 621                                 {
 622                                         ++line_num;
 623                                         str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$and").c_str(), output_width, l1, l2);
 624                                 }
 625                                 else if(cell->type == "$logic_or")
 626                                 {
 627                                         ++line_num;
 628                                         str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at("$or").c_str(), output_width, l1, l2);
 629                                 }
 630                                 f << stringf("%s\n", str.c_str());
 631                                 line_ref[cell->name]=line_num;
 632                         }
 633                         //multiplexers
 634                         else if(cell->type == "$mux")
 635                         {
 636                                 log("writing mux cell\n");
 637                                 int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
 638                                 int l1 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
 639                                 int l2 = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width);
 640                                 int s = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), 1);
 641                                 ++line_num;
 642                                 str = stringf ("%d %s %d %d %d %d",
 643                                         line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, s, l2, l1);
 644                                 //if s is 0 then l1, if s is 1 then l2 //according to the implementation of mux cell
 645                                 f << stringf("%s\n", str.c_str());
 646                                 line_ref[cell->name]=line_num;
 647                         }
 648                         else if(cell->type == "$pmux")
 649                         {
 650                           log("writing pmux cell\n");
 651                           int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
 652                           int select_width = cell->parameters.at(RTLIL::IdString("\\S_WIDTH")).as_int();
 653                           int default_case = dump_sigspec(&cell->getPort(RTLIL::IdString("\\A")), output_width);
 654                           int cases = dump_sigspec(&cell->getPort(RTLIL::IdString("\\B")), output_width*select_width);
 655                           int select = dump_sigspec(&cell->getPort(RTLIL::IdString("\\S")), select_width);
 656                           int *c = new int[select_width];
 657
 658                           for (int i=0; i<select_width; ++i)
 659                           {
 660                             ++line_num;
 661                             str = stringf ("%d slice 1 %d %d %d", line_num, select, i, i);
 662                             f << stringf("%s\n", str.c_str());
 663                             c[i] = line_num;
 664                             ++line_num;
 665                             str = stringf ("%d slice %d %d %d %d", line_num, output_width, cases, i*output_width+output_width-1,
 666                                            i*output_width);
 667                             f << stringf("%s\n", str.c_str());
 668                           }
 669
 670                           ++line_num;
 671                           str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[select_width-1], c[select_width-1]+1, default_case);
 672                           f << stringf("%s\n", str.c_str());
 673
 674                           for (int i=select_width-2; i>=0; --i)
 675                           {
 676                             ++line_num;
 677                             str = stringf ("%d cond %d %d %d %d", line_num, output_width, c[i], c[i]+1, line_num-1);
 678                             f << stringf("%s\n", str.c_str());
 679                           }
 680
 681                           line_ref[cell->name]=line_num;
 682                         }
 683             //registers
 684                         else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
 685                         {
 686                                 //TODO: remodelling fo adff cells
 687                                 log("writing cell - %s\n", cstr(cell->type));
 688                                 int output_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
 689                                 log(" - width is %d\n", output_width);
 690                                 int cond = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
 691                                 bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
 692                                 const RTLIL::SigSpec* cell_output = &cell->getPort(RTLIL::IdString("\\Q"));
 693                                 int value = dump_sigspec(&cell->getPort(RTLIL::IdString("\\D")), output_width);
 694                                 unsigned start_bit = 0;
 695                                 for(unsigned i=0; i<cell_output->chunks().size(); ++i)
 696                                 {
 697                                         output_width = cell_output->chunks().at(i).width;
 698                                         log_assert( output_width == cell_output->chunks().at(i).wire->width);//full reg is given the next value
 699                                         int reg = dump_wire(cell_output->chunks().at(i).wire);//register
 700                                         int slice = value;
 701                                         if(cell_output->chunks().size()>1)
 702                                         {
 703                                                 start_bit+=output_width;
 704                                                 slice = ++line_num;
 705                                                 str = stringf ("%d slice %d %d %d %d;", line_num, output_width, value, start_bit-1,
 706                                                         start_bit-output_width);
 707                                                 f << stringf("%s\n", str.c_str());
 708                                         }
 709                                         if(cell->type == "$dffsr")
 710                                         {
 711                                                 int sync_reset = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLR")), 1);
 712                                                 bool sync_reset_pol = cell->parameters.at(RTLIL::IdString("\\CLR_POLARITY")).as_bool();
 713                                                 int sync_reset_value = dump_sigspec(&cell->getPort(RTLIL::IdString("\\SET")),
 714                                                         output_width);
 715                                                 bool sync_reset_value_pol = cell->parameters.at(RTLIL::IdString("\\SET_POLARITY")).as_bool();
 716                                                 ++line_num;
 717                                                 str = stringf ("%d %s %d %s%d %s%d %d", line_num, cell_type_translation.at("$mux").c_str(),
 718                                                         output_width, sync_reset_pol ? "":"-", sync_reset, sync_reset_value_pol? "":"-",
 719                                                         sync_reset_value, slice);
 720                                                 f << stringf("%s\n", str.c_str());
 721                                                 slice = line_num;
 722                                         }
 723                                         ++line_num;
 724                                         str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
 725                                                 output_width, polarity?"":"-", cond, slice, reg);
 726
 727                                         f << stringf("%s\n", str.c_str());
 728                                         int next = line_num;
 729                                         if(cell->type == "$adff")
 730                                         {
 731                                                 int async_reset = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ARST")), 1);
 732                                                 bool async_reset_pol = cell->parameters.at(RTLIL::IdString("\\ARST_POLARITY")).as_bool();
 733                                                 int async_reset_value = dump_const(&cell->parameters.at(RTLIL::IdString("\\ARST_VALUE")),
 734                                                         output_width, 0);
 735                                                 ++line_num;
 736                                                 str = stringf ("%d %s %d %s%d %d %d", line_num, cell_type_translation.at("$mux").c_str(),
 737                                                         output_width, async_reset_pol ? "":"-", async_reset, async_reset_value, next);
 738                                                 f << stringf("%s\n", str.c_str());
 739                                         }
 740                                         ++line_num;
 741                                         str = stringf ("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(),
 742                                                 output_width, reg, next);
 743                                         f << stringf("%s\n", str.c_str());
 744                                 }
 745                                 line_ref[cell->name]=line_num;
 746                         }
 747                         //memories
 748                         else if(cell->type == "$memrd")
 749                         {
 750                                 log("writing memrd cell\n");
 751                                 if (cell->parameters.at("\\CLK_ENABLE").as_bool() == true)
 752                                         log_error("The btor backen does not support $memrd cells with built-in registers. Run memory_dff with -wr_only.\n");
 753                                 str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
 754                                 int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
 755                                 int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
 756                                 int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
 757                                 int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
 758                                 ++line_num;
 759                                 str = stringf("%d read %d %d %d", line_num, data_width, mem, address);
 760                                 f << stringf("%s\n", str.c_str());
 761                                 line_ref[cell->name]=line_num;
 762                         }
 763                         else if(cell->type == "$memwr")
 764                         {
 765                                 log("writing memwr cell\n");
 766                                 if (cell->parameters.at("\\CLK_ENABLE").as_bool() == false)
 767                                         log_error("The btor backen does not support $memwr cells without built-in registers. Run memory_dff (but with -wr_only).\n");
 768                                 int clk = dump_sigspec(&cell->getPort(RTLIL::IdString("\\CLK")), 1);
 769                                 bool polarity = cell->parameters.at(RTLIL::IdString("\\CLK_POLARITY")).as_bool();
 770                                 int enable = dump_sigspec(&cell->getPort(RTLIL::IdString("\\EN")), 1);
 771                                 int address_width = cell->parameters.at(RTLIL::IdString("\\ABITS")).as_int();
 772                                 int address = dump_sigspec(&cell->getPort(RTLIL::IdString("\\ADDR")), address_width);
 773                                 int data_width = cell->parameters.at(RTLIL::IdString("\\WIDTH")).as_int();
 774                                 int data = dump_sigspec(&cell->getPort(RTLIL::IdString("\\DATA")), data_width);
 775                                 str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
 776                                 int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str())));
 777                                 //check if the memory has already next
 778                                 auto it = mem_next.find(mem);
 779                                 if(it != std::end(mem_next))
 780                                 {
 781                                         ++line_num;
 782                                         str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string();
 783                                         RTLIL::Memory *memory = module->memories.at(RTLIL::IdString(str.c_str()));
 784                                         int address_bits = ceil(log(memory->size)/log(2));
 785                                         str = stringf("%d array %d %d", line_num, memory->width, address_bits);
 786                                         f << stringf("%s\n", str.c_str());
 787                                         ++line_num;
 788                                         str = stringf("%d eq 1 %d %d", line_num, mem, line_num - 1);
 789                                         f << stringf("%s\n", str.c_str());
 790                                         mem = line_num - 1;
 791                                 }
 792                                 ++line_num;
 793                                 if(polarity)
 794                                         str = stringf("%d one 1", line_num);
 795                                 else
 796                                         str = stringf("%d zero 1", line_num);
 797                                 f << stringf("%s\n", str.c_str());
 798                                 ++line_num;
 799                                 str = stringf("%d eq 1 %d %d", line_num, clk, line_num-1);
 800                                 f << stringf("%s\n", str.c_str());
 801                                 ++line_num;
 802                                 str = stringf("%d and 1 %d %d", line_num, line_num-1, enable);
 803                                 f << stringf("%s\n", str.c_str());
 804                                 ++line_num;
 805                                 str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data);
 806                                 f << stringf("%s\n", str.c_str());
 807                                 ++line_num;
 808                                 str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2/*enable*/, line_num-1, mem);
 809                                 f << stringf("%s\n", str.c_str());
 810                                 ++line_num;
 811                                 str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1);
 812                                 f << stringf("%s\n", str.c_str());
 813                                 mem_next.insert(mem);
 814                                 line_ref[cell->name]=line_num;
 815                         }
 816                         else if(cell->type == "$slice")
 817                         {
 818                                 log("writing slice cell\n");
 819                                 const RTLIL::SigSpec* input = &cell->getPort(RTLIL::IdString("\\A"));
 820                                 int input_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 821                                 log_assert(input->size() == input_width);
 822                                 int input_line = dump_sigspec(input, input_width);
 823                                 const RTLIL::SigSpec* output YS_ATTRIBUTE(unused) = &cell->getPort(RTLIL::IdString("\\Y"));
 824                                 int output_width = cell->parameters.at(RTLIL::IdString("\\Y_WIDTH")).as_int();
 825                                 log_assert(output->size() == output_width);
 826                                 int offset = cell->parameters.at(RTLIL::IdString("\\OFFSET")).as_int();
 827                                 ++line_num;
 828                                 str = stringf("%d %s %d %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), output_width, input_line, output_width+offset-1, offset);
 829                                 f << stringf("%s\n", str.c_str());
 830                                 line_ref[cell->name]=line_num;
 831                         }
 832                         else if(cell->type == "$concat")
 833                         {
 834                                 log("writing concat cell\n");
 835                                 const RTLIL::SigSpec* input_a = &cell->getPort(RTLIL::IdString("\\A"));
 836                                 int input_a_width = cell->parameters.at(RTLIL::IdString("\\A_WIDTH")).as_int();
 837                                 log_assert(input_a->size() == input_a_width);
 838                                 int input_a_line = dump_sigspec(input_a, input_a_width);
 839                                 const RTLIL::SigSpec* input_b = &cell->getPort(RTLIL::IdString("\\B"));
 840                                 int input_b_width = cell->parameters.at(RTLIL::IdString("\\B_WIDTH")).as_int();
 841                                 log_assert(input_b->size() == input_b_width);
 842                                 int input_b_line = dump_sigspec(input_b, input_b_width);
 843                                 ++line_num;
 844                                 str = stringf("%d %s %d %d %d", line_num, cell_type_translation.at(cell->type.str()).c_str(), input_a_width+input_b_width,
 845                                         input_a_line, input_b_line);
 846                                 f << stringf("%s\n", str.c_str());
 847                                 line_ref[cell->name]=line_num;
 848                         }
 849                         curr_cell.clear();
 850                         return line_num;
 851                 }
 852                 else
 853                 {
 854                         return it->second;
 855                 }
 856         }
 857
 858         const RTLIL::SigSpec* get_cell_output(RTLIL::Cell* cell)
 859         {
 860                 const RTLIL::SigSpec *output_sig = nullptr;
 861                 if (cell->type == "$memrd")
 862                 {
 863                         output_sig = &cell->getPort(RTLIL::IdString("\\DATA"));
 864                 }
 865                 else if(cell->type == "$memwr" || cell->type == "$assert")
 866                 {
 867                         //no output
 868                 }
 869                 else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
 870                 {
 871                         output_sig = &cell->getPort(RTLIL::IdString("\\Q"));
 872                 }
 873                 else
 874                 {
 875                         output_sig = &cell->getPort(RTLIL::IdString("\\Y"));
 876                 }
 877                 return output_sig;
 878         }
 879
 880         void dump_property(RTLIL::Wire *wire)
 881         {
 882                 int l = dump_wire(wire);
 883                 ++line_num;
 884                 str = stringf("%d root 1 %d", line_num, l);
 885                 f << stringf("%s\n", str.c_str());
 886         }
 887
 888         void dump()
 889         {
 890                 f << stringf(";module %s\n", cstr(module->name));
 891
 892                 log("creating intermediate wires map\n");
 893                 //creating map of intermediate wires as output of some cell
 894                 for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it)
 895                 {
 896                         RTLIL::Cell *cell = it->second;
 897                         const RTLIL::SigSpec* output_sig = get_cell_output(cell);
 898                         if(output_sig==nullptr)
 899                                 continue;
 900                         RTLIL::SigSpec s = sigmap(*output_sig);
 901                         output_sig = &s;
 902                         log(" - %s\n", cstr(it->second->type));
 903                         if (cell->type == "$memrd")
 904                         {
 905                                 for(unsigned i=0; i<output_sig->chunks().size(); ++i)
 906                                 {
 907                                         RTLIL::Wire *w = output_sig->chunks().at(i).wire;
 908                                         RTLIL::IdString wire_id = w->name;
 909                                         inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
 910                                 }
 911                         }
 912                         else if(cell->type == "$memwr")
 913                         {
 914                                 continue;//nothing to do
 915                         }
 916                         else if(cell->type == "$dff" || cell->type == "$adff" || cell->type == "$dffsr")
 917                         {
 918                                 RTLIL::IdString wire_id = output_sig->chunks().front().wire->name;
 919                                 for(unsigned i=0; i<output_sig->chunks().size(); ++i)
 920                                 {
 921                                         RTLIL::Wire *w = output_sig->chunks().at(i).wire;
 922                                         RTLIL::IdString wire_id = w->name;
 923                                         inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
 924                                         basic_wires[wire_id] = true;
 925                                 }
 926                         }
 927                         else
 928                         {
 929                                 for(unsigned i=0; i<output_sig->chunks().size(); ++i)
 930                                 {
 931                                         RTLIL::Wire *w = output_sig->chunks().at(i).wire;
 932                                         RTLIL::IdString wire_id = w->name;
 933                                         inter_wire_map[wire_id].insert(WireInfo(cell->name,&output_sig->chunks().at(i)));
 934                                 }
 935                         }
 936                 }
 937
 938                 log("writing input\n");
 939                 std::map<int, RTLIL::Wire*> inputs, outputs;
 940                 std::vector<RTLIL::Wire*> safety;
 941
 942                 for (auto &wire_it : module->wires_) {
 943                         RTLIL::Wire *wire = wire_it.second;
 944                         if (wire->port_input)
 945                                 inputs[wire->port_id] = wire;
 946                         if (wire->port_output) {
 947                                 outputs[wire->port_id] = wire;
 948                                 if (wire->name.str().find("safety") != std::string::npos )
 949                                         safety.push_back(wire);
 950                         }
 951                 }
 952
 953                 f << stringf(";inputs\n");
 954                 for (auto &it : inputs) {
 955                         RTLIL::Wire *wire = it.second;
 956                         dump_wire(wire);
 957                 }
 958                 f << stringf("\n");
 959
 960                 log("writing memories\n");
 961                 for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it)
 962                 {
 963                         dump_memory(mem_it->second);
 964                 }
 965
 966                 log("writing output wires\n");
 967                 for (auto &it : outputs) {
 968                         RTLIL::Wire *wire = it.second;
 969                         dump_wire(wire);
 970                 }
 971
 972                 log("writing cells\n");
 973                 for(auto cell_it = module->cells_.begin(); cell_it != module->cells_.end(); ++cell_it)
 974                 {
 975                         dump_cell(cell_it->second);
 976                 }
 977
 978                 for(auto it: safety)
 979                         dump_property(it);
 980
 981                 f << stringf("\n");
 982
 983                 log("writing outputs info\n");
 984                 f << stringf(";outputs\n");
 985                 for (auto &it : outputs) {
 986                         RTLIL::Wire *wire = it.second;
 987                         int l = dump_wire(wire);
 988                         f << stringf(";%d %s", l, cstr(wire->name));
 989                 }
 990                 f << stringf("\n");
 991         }
 992
 993         static void dump(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig &config)
 994         {
 995                 BtorDumper dumper(f, module, design, &config);
 996                 dumper.dump();
 997         }
 998 };
 999
1000 struct BtorBackend : public Backend {
1001         BtorBackend() : Backend("btor", "write design to BTOR file") { }
1002
1003         virtual void help()
1004         {
1005                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1006                 log("\n");
1007                 log("    write_btor [filename]\n");
1008                 log("\n");
1009                 log("Write the current design to an BTOR file.\n");
1010         }
1011
1012         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
1013         {
1014                 std::string top_module_name;
1015                 std::string buf_type, buf_in, buf_out;
1016                 std::string true_type, true_out;
1017                 std::string false_type, false_out;
1018                 BtorDumperConfig config;
1019
1020                 log_header("Executing BTOR backend.\n");
1021
1022                 size_t argidx=1;
1023                 extra_args(f, filename, args, argidx);
1024
1025                 if (top_module_name.empty())
1026                         for (auto & mod_it:design->modules_)
1027                                 if (mod_it.second->get_bool_attribute("\\top"))
1028                                         top_module_name = mod_it.first.str();
1029
1030                 *f << stringf("; Generated by %s\n", yosys_version_str);
1031                 *f << stringf(";  %s developed and maintained by Clifford Wolf <clifford@clifford.at>\n", yosys_version_str);
1032                 *f << stringf("; BTOR Backend developed by Ahmed Irfan <irfan@fbk.eu> - Fondazione Bruno Kessler, Trento, Italy\n");
1033                 *f << stringf(";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n");
1034
1035                 std::vector<RTLIL::Module*> mod_list;
1036
1037                 for (auto module_it : design->modules_)
1038                 {
1039                         RTLIL::Module *module = module_it.second;
1040                         if (module->get_bool_attribute("\\blackbox"))
1041                                 continue;
1042
1043                         if (module->processes.size() != 0)
1044                                 log_error("Found unmapped processes in module %s: unmapped processes are not supported in BTOR backend!\n", RTLIL::id2cstr(module->name));
1045
1046                         if (module->name == RTLIL::escape_id(top_module_name)) {
1047                                 BtorDumper::dump(*f, module, design, config);
1048                                 top_module_name.clear();
1049                                 continue;
1050                         }
1051
1052                         mod_list.push_back(module);
1053                 }
1054
1055                 if (!top_module_name.empty())
1056                         log_error("Can't find top module `%s'!\n", top_module_name.c_str());
1057
1058                 for (auto module : mod_list)
1059                         BtorDumper::dump(*f, module, design, config);
1060         }
1061 } BtorBackend;
1062
1063 PRIVATE_NAMESPACE_END