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         pool<Cell*> cell_recursion_guard;
  60
  61         int get_bv_sid(int width)
  62         {
  63                 if (sorts_bv.count(width) == 0) {
  64                         int nid = next_nid++;
  65                         f << stringf("%d sort bitvec %d\n", nid, width);
  66                         sorts_bv[width] = nid;
  67                 }
  68                 return sorts_bv.at(width);
  69         }
  70
  71         void export_cell(Cell *cell)
  72         {
  73                 log_assert(cell_recursion_guard.count(cell) == 0);
  74                 cell_recursion_guard.insert(cell);
  75
  76                 if (cell->type.in("$add", "$sub"))
  77                 {
  78                         string btor_op;
  79                         if (cell->type == "$add") btor_op = "add";
  80                         if (cell->type == "$sub") btor_op = "sub";
  81                         log_assert(!btor_op.empty());
  82
  83                         int width = GetSize(cell->getPort("\\Y"));
  84                         width = std::max(width, GetSize(cell->getPort("\\A")));
  85                         width = std::max(width, GetSize(cell->getPort("\\B")));
  86
  87                         bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
  88                         bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
  89
  90                         int sid = get_bv_sid(width);
  91                         int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
  92                         int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
  93
  94                         int nid = next_nid++;
  95                         f << stringf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
  96
  97                         SigSpec sig = sigmap(cell->getPort("\\Y"));
  98
  99                         if (GetSize(sig) < width) {
 100                                 int sid = get_bv_sid(GetSize(sig));
 101                                 int nid2 = next_nid++;
 102                                 f << stringf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
 103                                 nid = nid2;
 104                         }
 105
 106                         for (int i = 0; i < GetSize(sig); i++)
 107                                 bit_nid[sig[i]] = make_pair(nid, i);
 108
 109                         sig_nid[sig] = nid;
 110                         nid_width[nid] = GetSize(sig);
 111
 112                         goto okay;
 113                 }
 114
 115                 log_error("Unsupported cell type: %s\n", log_id(cell));
 116
 117         okay:
 118                 cell_recursion_guard.erase(cell);
 119         }
 120
 121         int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
 122         {
 123                 sigmap.apply(sig);
 124
 125                 if (sig_nid.count(sig) == 0)
 126                 {
 127                         // <nid>, <bitidx>
 128                         vector<pair<int, int>> nidbits;
 129
 130                         // collect all bits
 131                         for (int i = 0; i < GetSize(sig); i++)
 132                         {
 133                                 SigBit bit = sig[i];
 134
 135                                 if (bit_nid.count(bit) == 0)
 136                                 {
 137                                         if (bit.wire == nullptr)
 138                                         {
 139                                                 Const c(bit.data);
 140
 141                                                 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
 142                                                         c.bits.push_back(sig[i+GetSize(c)].data);
 143
 144                                                 if (consts.count(c) == 0) {
 145                                                         int sid = get_bv_sid(GetSize(c));
 146                                                         int nid = next_nid++;
 147                                                         f << stringf("%d const %d %s\n", nid, sid, c.as_string().c_str());
 148                                                         consts[c] = nid;
 149                                                 }
 150
 151                                                 int nid = consts.at(c);
 152
 153                                                 for (int j = 0; j < GetSize(c); j++)
 154                                                         nidbits.push_back(make_pair(nid, j));
 155
 156                                                 i += GetSize(c)-1;
 157                                                 continue;
 158                                         }
 159                                         else
 160                                         {
 161                                                 export_cell(bit_cell.at(bit));
 162                                                 log_assert(bit_nid.count(bit));
 163                                         }
 164                                 }
 165
 166                                 nidbits.push_back(bit_nid.at(bit));
 167                         }
 168
 169                         int width = 0;
 170                         int nid = -1;
 171
 172                         // group bits and emit slice-concat chain
 173                         for (int i = 0; i < GetSize(nidbits); i++)
 174                         {
 175                                 int nid2 = nidbits[i].first;
 176                                 int lower =  nidbits[i].second;
 177                                 int upper = lower;
 178
 179                                 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
 180                                                 nidbits[i+1].second == nidbits[i].second+1)
 181                                         upper++, i++;
 182
 183                                 int nid3 = nid2;
 184
 185                                 if (lower != 0 && upper+1 != nid_width.at(nid2)) {
 186                                         int sid = get_bv_sid(upper-lower+1);
 187                                         nid3 = next_nid++;
 188                                         f << stringf("%d slice %d %d %d %d\n", nid3, sid, nid, upper, lower);
 189                                 }
 190
 191                                 int nid4 = nid3;
 192
 193                                 if (nid >= 0) {
 194                                         int sid = get_bv_sid(width+upper-lower+1);
 195                                         int nid4 = next_nid++;
 196                                         f << stringf("%d concat %d %d %d\n", nid4, sid, nid, nid3);
 197                                 }
 198
 199                                 width += upper-lower+1;
 200                                 nid = nid4;
 201                         }
 202
 203                         sig_nid[sig] = nid;
 204                         nid_width[nid] = width;
 205                 }
 206
 207                 int nid = sig_nid.at(sig);
 208
 209                 if (to_width >= 0 && to_width != GetSize(sig))
 210                 {
 211                         if (to_width < GetSize(sig))
 212                         {
 213                                 int sid = get_bv_sid(to_width);
 214                                 int nid2 = next_nid++;
 215                                 f << stringf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1);
 216                                 nid = nid2;
 217                         }
 218                         else
 219                         {
 220                                 int sid = get_bv_sid(to_width);
 221                                 int nid2 = next_nid++;
 222                                 f << stringf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext",
 223                                                 sid, nid, to_width - GetSize(sig));
 224                                 nid = nid2;
 225                         }
 226                 }
 227
 228                 return nid;
 229         }
 230
 231         BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
 232                         f(f), sigmap(module), module(module), verbose(verbose), next_nid(1)
 233         {
 234                 for (auto wire : module->wires())
 235                 {
 236                         if (!wire->port_id || !wire->port_input)
 237                                 continue;
 238
 239                         SigSpec sig = sigmap(wire);
 240                         int sid = get_bv_sid(GetSize(sig));
 241                         int nid = next_nid++;
 242
 243                         f << stringf("%d input %d %s\n", nid, sid, log_id(wire));
 244
 245                         for (int i = 0; i < GetSize(sig); i++)
 246                                 bit_nid[sig[i]] = make_pair(nid, i);
 247                         sig_nid[sig] = nid;
 248                         nid_width[nid] = GetSize(sig);
 249                 }
 250
 251                 for (auto cell : module->cells())
 252                 for (auto &conn : cell->connections())
 253                 {
 254                         if (!cell->output(conn.first))
 255                                 continue;
 256
 257                         for (auto bit : sigmap(conn.second))
 258                                 bit_cell[bit] = cell;
 259                 }
 260
 261                 for (auto wire : module->wires())
 262                 {
 263                         if (!wire->port_id || !wire->port_output)
 264                                 continue;
 265
 266                         int nid = get_sig_nid(wire);
 267                         f << stringf("%d output %d %s\n", next_nid++, nid, log_id(wire));
 268                 }
 269         }
 270 };
 271
 272 struct BtorBackend : public Backend {
 273         BtorBackend() : Backend("btor", "write design to BTOR file") { }
 274         virtual void help()
 275         {
 276                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 277                 log("\n");
 278                 log("    write_btor [options] [filename]\n");
 279                 log("\n");
 280                 log("Write a BTOR description of the current design.\n");
 281                 log("\n");
 282         }
 283         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 284         {
 285                 bool verbose = false;
 286
 287                 log_header(design, "Executing BTOR backend.\n");
 288
 289                 size_t argidx;
 290                 for (argidx = 1; argidx < args.size(); argidx++)
 291                 {
 292                         // if (args[argidx] == "-verbose") {
 293                         //      verbose = true;
 294                         //      continue;
 295                         // }
 296                         break;
 297                 }
 298                 extra_args(f, filename, args, argidx);
 299
 300                 RTLIL::Module *topmod = design->top_module();
 301
 302                 if (topmod == nullptr)
 303                         log_cmd_error("No top module found.\n");
 304
 305                 *f << stringf("; BTOR description generated by %s for module %s.\n",
 306                                 yosys_version_str, log_id(topmod));
 307
 308                 BtorWorker(*f, topmod, verbose);
 309
 310                 *f << stringf("; end of yosys output\n");
 311         }
 312 } BtorBackend;
 313
 314 PRIVATE_NAMESPACE_END