backends/btor/btor.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #include "kernel/rtlil.h"
  21 #include "kernel/register.h"
  22 #include "kernel/sigtools.h"
  23 #include "kernel/celltypes.h"
  24 #include "kernel/log.h"
  25 #include <string>
  26
  27 USING_YOSYS_NAMESPACE
  28 PRIVATE_NAMESPACE_BEGIN
  29
  30 struct BtorWorker
  31 {
  32         std::ostream &f;
  33         SigMap sigmap;
  34         RTLIL::Module *module;
  35         bool verbose;
  36         int next_nid;
  37
  38         // <width> => <sid>
  39         dict<int, int> sorts_bv;
  40
  41         // (<address-width>, <data-width>) => <sid>
  42         dict<pair<int, int>, int> sorts_mem;
  43
  44         // SigBit => (<nid>, <bitidx>)
  45         dict<SigBit, pair<int, int>> bit_nid;
  46
  47         // <nid> => <bvwidth>
  48         dict<int, int> nid_width;
  49
  50         // SigSpec => <nid>
  51         dict<SigSpec, int> sig_nid;
  52
  53         // bit to driving cell
  54         dict<SigBit, Cell*> bit_cell;
  55
  56         // nids for constants
  57         dict<Const, int> consts;
  58
  59         // ff inputs that need to be evaluated (<nid>, <d>)
  60         vector<pair<int, SigSpec>> ff_todo;
  61
  62         pool<Cell*> cell_recursion_guard;
  63
  64         int get_bv_sid(int width)
  65         {
  66                 if (sorts_bv.count(width) == 0) {
  67                         int nid = next_nid++;
  68                         f << stringf("%d sort bitvec %d\n", nid, width);
  69                         sorts_bv[width] = nid;
  70                 }
  71                 return sorts_bv.at(width);
  72         }
  73
  74         void add_nid_sig(int nid, const SigSpec &sig)
  75         {
  76                 for (int i = 0; i < GetSize(sig); i++)
  77                         bit_nid[sig[i]] = make_pair(nid, i);
  78
  79                 sig_nid[sig] = nid;
  80                 nid_width[nid] = GetSize(sig);
  81         }
  82
  83         void export_cell(Cell *cell)
  84         {
  85                 log_assert(cell_recursion_guard.count(cell) == 0);
  86                 cell_recursion_guard.insert(cell);
  87
  88                 if (cell->type.in("$add", "$sub", "$xor"))
  89                 {
  90                         string btor_op;
  91                         if (cell->type == "$add") btor_op = "add";
  92                         if (cell->type == "$sub") btor_op = "sub";
  93                         if (cell->type == "$xor") btor_op = "xor";
  94                         log_assert(!btor_op.empty());
  95
  96                         int width = GetSize(cell->getPort("\\Y"));
  97                         width = std::max(width, GetSize(cell->getPort("\\A")));
  98                         width = std::max(width, GetSize(cell->getPort("\\B")));
  99
 100                         bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
 101                         bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
 102
 103                         int sid = get_bv_sid(width);
 104                         int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
 105                         int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
 106
 107                         int nid = next_nid++;
 108                         f << stringf("%d %s %d %d %d ; %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, log_id(cell));
 109
 110                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 111
 112                         if (GetSize(sig) < width) {
 113                                 int sid = get_bv_sid(GetSize(sig));
 114                                 int nid2 = next_nid++;
 115                                 f << stringf("%d slice %d %d %d 0 ; %s\n", nid2, sid, nid, GetSize(sig)-1, log_id(cell));
 116                                 nid = nid2;
 117                         }
 118
 119                         add_nid_sig(nid, sig);
 120                         goto okay;
 121                 }
 122
 123                 if (cell->type.in("$mux", "$_MUX_"))
 124                 {
 125                         SigSpec sig_a = sigmap(cell->getPort("\\A"));
 126                         SigSpec sig_b = sigmap(cell->getPort("\\B"));
 127                         SigSpec sig_s = sigmap(cell->getPort("\\S"));
 128                         SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 129
 130                         int nid_a = get_sig_nid(sig_a);
 131                         int nid_b = get_sig_nid(sig_b);
 132                         int nid_s = get_sig_nid(sig_s);
 133
 134                         int sid = get_bv_sid(GetSize(sig_y));
 135                         int nid = next_nid++;
 136                         f << stringf("%d ite %d %d %d %d ; %s\n", nid, sid, nid_s, nid_b, nid_a, log_id(cell));
 137
 138                         add_nid_sig(nid, sig_y);
 139                         goto okay;
 140                 }
 141
 142                 if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
 143                 {
 144                         SigSpec sig_d = sigmap(cell->getPort("\\D"));
 145                         SigSpec sig_q = sigmap(cell->getPort("\\Q"));
 146
 147                         string symbol = log_signal(sig_q);
 148                         if (symbol.find(' ') != string::npos)
 149                                 symbol = log_id(cell);
 150
 151                         if (symbol[0] == '\\')
 152                                 symbol = symbol.substr(1);
 153
 154                         int sid = get_bv_sid(GetSize(sig_q));
 155                         int nid = next_nid++;
 156                         f << stringf("%d state %d %s ; %s\n", nid, sid, symbol.c_str(), log_id(cell));
 157
 158                         ff_todo.push_back(make_pair(nid, sig_d));
 159                         add_nid_sig(nid, sig_q);
 160                         goto okay;
 161                 }
 162
 163                 log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 164
 165         okay:
 166                 cell_recursion_guard.erase(cell);
 167         }
 168
 169         int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
 170         {
 171                 sigmap.apply(sig);
 172
 173                 if (sig_nid.count(sig) == 0)
 174                 {
 175                         // <nid>, <bitidx>
 176                         vector<pair<int, int>> nidbits;
 177
 178                         // collect all bits
 179                         for (int i = 0; i < GetSize(sig); i++)
 180                         {
 181                                 SigBit bit = sig[i];
 182
 183                                 if (bit_nid.count(bit) == 0)
 184                                 {
 185                                         if (bit.wire == nullptr)
 186                                         {
 187                                                 Const c(bit.data);
 188
 189                                                 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
 190                                                         c.bits.push_back(sig[i+GetSize(c)].data);
 191
 192                                                 if (consts.count(c) == 0) {
 193                                                         int sid = get_bv_sid(GetSize(c));
 194                                                         int nid = next_nid++;
 195                                                         f << stringf("%d const %d %s\n", nid, sid, c.as_string().c_str());
 196                                                         consts[c] = nid;
 197                                                         nid_width[nid] = GetSize(c);
 198                                                 }
 199
 200                                                 int nid = consts.at(c);
 201
 202                                                 for (int j = 0; j < GetSize(c); j++)
 203                                                         nidbits.push_back(make_pair(nid, j));
 204
 205                                                 i += GetSize(c)-1;
 206                                                 continue;
 207                                         }
 208                                         else
 209                                         {
 210                                                 export_cell(bit_cell.at(bit));
 211                                                 log_assert(bit_nid.count(bit));
 212                                         }
 213                                 }
 214
 215                                 nidbits.push_back(bit_nid.at(bit));
 216                         }
 217
 218                         int width = 0;
 219                         int nid = -1;
 220
 221                         // group bits and emit slice-concat chain
 222                         for (int i = 0; i < GetSize(nidbits); i++)
 223                         {
 224                                 int nid2 = nidbits[i].first;
 225                                 int lower =  nidbits[i].second;
 226                                 int upper = lower;
 227
 228                                 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
 229                                                 nidbits[i+1].second == nidbits[i].second+1)
 230                                         upper++, i++;
 231
 232                                 int nid3 = nid2;
 233
 234                                 if (lower != 0 || upper+1 != nid_width.at(nid2)) {
 235                                         int sid = get_bv_sid(upper-lower+1);
 236                                         nid3 = next_nid++;
 237                                         f << stringf("%d slice %d %d %d %d\n", nid3, sid, nid, upper, lower);
 238                                 }
 239
 240                                 int nid4 = nid3;
 241
 242                                 if (nid >= 0) {
 243                                         int sid = get_bv_sid(width+upper-lower+1);
 244                                         int nid4 = next_nid++;
 245                                         f << stringf("%d concat %d %d %d\n", nid4, sid, nid, nid3);
 246                                 }
 247
 248                                 width += upper-lower+1;
 249                                 nid = nid4;
 250                         }
 251
 252                         sig_nid[sig] = nid;
 253                         nid_width[nid] = width;
 254                 }
 255
 256                 int nid = sig_nid.at(sig);
 257
 258                 if (to_width >= 0 && to_width != GetSize(sig))
 259                 {
 260                         if (to_width < GetSize(sig))
 261                         {
 262                                 int sid = get_bv_sid(to_width);
 263                                 int nid2 = next_nid++;
 264                                 f << stringf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1);
 265                                 nid = nid2;
 266                         }
 267                         else
 268                         {
 269                                 int sid = get_bv_sid(to_width);
 270                                 int nid2 = next_nid++;
 271                                 f << stringf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext",
 272                                                 sid, nid, to_width - GetSize(sig));
 273                                 nid = nid2;
 274                         }
 275                 }
 276
 277                 return nid;
 278         }
 279
 280         BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
 281                         f(f), sigmap(module), module(module), verbose(verbose), next_nid(1)
 282         {
 283                 for (auto wire : module->wires())
 284                 {
 285                         if (!wire->port_id || !wire->port_input)
 286                                 continue;
 287
 288                         SigSpec sig = sigmap(wire);
 289                         int sid = get_bv_sid(GetSize(sig));
 290                         int nid = next_nid++;
 291
 292                         f << stringf("%d input %d %s\n", nid, sid, log_id(wire));
 293                         add_nid_sig(nid, sig);
 294                 }
 295
 296                 for (auto cell : module->cells())
 297                 for (auto &conn : cell->connections())
 298                 {
 299                         if (!cell->output(conn.first))
 300                                 continue;
 301
 302                         for (auto bit : sigmap(conn.second))
 303                                 bit_cell[bit] = cell;
 304                 }
 305
 306                 for (auto wire : module->wires())
 307                 {
 308                         if (!wire->port_id || !wire->port_output)
 309                                 continue;
 310
 311                         int nid = get_sig_nid(wire);
 312                         f << stringf("%d output %d %s\n", next_nid++, nid, log_id(wire));
 313                 }
 314
 315                 while (!ff_todo.empty())
 316                 {
 317                         vector<pair<int, SigSpec>> todo;
 318                         todo.swap(ff_todo);
 319
 320                         for (auto &it : todo)
 321                         {
 322                                 int nid = get_sig_nid(it.second);
 323                                 int sid = get_bv_sid(GetSize(it.second));
 324                                 f << stringf("%d next %d %d %d\n", next_nid++, sid, it.first, nid);
 325                         }
 326                 }
 327         }
 328 };
 329
 330 struct BtorBackend : public Backend {
 331         BtorBackend() : Backend("btor", "write design to BTOR file") { }
 332         virtual void help()
 333         {
 334                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 335                 log("\n");
 336                 log("    write_btor [options] [filename]\n");
 337                 log("\n");
 338                 log("Write a BTOR description of the current design.\n");
 339                 log("\n");
 340         }
 341         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 342         {
 343                 bool verbose = false;
 344
 345                 log_header(design, "Executing BTOR backend.\n");
 346
 347                 size_t argidx;
 348                 for (argidx = 1; argidx < args.size(); argidx++)
 349                 {
 350                         // if (args[argidx] == "-verbose") {
 351                         //      verbose = true;
 352                         //      continue;
 353                         // }
 354                         break;
 355                 }
 356                 extra_args(f, filename, args, argidx);
 357
 358                 RTLIL::Module *topmod = design->top_module();
 359
 360                 if (topmod == nullptr)
 361                         log_cmd_error("No top module found.\n");
 362
 363                 *f << stringf("; BTOR description generated by %s for module %s.\n",
 364                                 yosys_version_str, log_id(topmod));
 365
 366                 BtorWorker(*f, topmod, verbose);
 367
 368                 *f << stringf("; end of yosys output\n");
 369         }
 370 } BtorBackend;
 371
 372 PRIVATE_NAMESPACE_END