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         int get_bv_sid(int width)
  57         {
  58                 if (sorts_bv.count(width) == 0) {
  59                         int nid = next_nid++;
  60                         f << stringf("%d sort bitvec %d\n", nid, width);
  61                         sorts_bv[width] = nid;
  62                 }
  63                 return sorts_bv.at(width);
  64         }
  65
  66         int get_sig_nid(SigSpec sig)
  67         {
  68                 sigmap.apply(sig);
  69
  70                 if (sig_nid.count(sig) == 0)
  71                 {
  72                         // <nid>, <bitidx>
  73                         vector<pair<int, int>> nidbits;
  74
  75                         // collect all bits
  76                         for (int i = 0; i < GetSize(sig); i++)
  77                         {
  78                                 SigBit bit = sig[i];
  79
  80                                 if (bit_nid.count(bit) == 0)
  81                                 {
  82                                         // FIXME
  83                                         log_abort();
  84                                 }
  85
  86                                 nidbits.push_back(bit_nid.at(bit));
  87                         }
  88
  89                         int width = 0;
  90                         int nid = -1;
  91
  92                         // group bits and emit slice-concat chain
  93                         for (int i = 0; i < GetSize(nidbits); i++)
  94                         {
  95                                 int nid2 = nidbits[i].first;
  96                                 int lower =  nidbits[i].second;
  97                                 int upper = lower;
  98
  99                                 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
 100                                                 nidbits[i+1].second == nidbits[i].second+1)
 101                                         upper++, i++;
 102
 103                                 int nid3 = nid2;
 104
 105                                 if (lower != 0 && upper+1 != nid_width.at(nid2)) {
 106                                         int sid = get_bv_sid(upper-lower+1);
 107                                         nid3 = next_nid++;
 108                                         f << stringf("%d slice %d %d %d %d\n", nid3, sid, nid, upper, lower);
 109                                 }
 110
 111                                 int nid4 = nid3;
 112
 113                                 if (nid >= 0) {
 114                                         int sid = get_bv_sid(width+upper-lower+1);
 115                                         int nid4 = next_nid++;
 116                                         f << stringf("%d concat %d %d %d\n", nid4, sid, nid, nid3);
 117                                 }
 118
 119                                 width += upper-lower+1;
 120                                 nid = nid4;
 121                         }
 122
 123                         sig_nid[sig] = nid;
 124                         nid_width[nid] = width;
 125                 }
 126
 127                 return sig_nid.at(sig);
 128         }
 129
 130         BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
 131                         f(f), sigmap(module), module(module), verbose(verbose), next_nid(1)
 132         {
 133                 for (auto wire : module->wires())
 134                 {
 135                         if (!wire->port_id || !wire->port_input)
 136                                 continue;
 137
 138                         SigSpec sig = sigmap(wire);
 139                         int sid = get_bv_sid(GetSize(sig));
 140                         int nid = next_nid++;
 141
 142                         f << stringf("%d input %d %s\n", nid, sid, log_id(wire));
 143
 144                         for (int i = 0; i < GetSize(sig); i++)
 145                                 bit_nid[sig[i]] = make_pair(nid, i);
 146                         sig_nid[sig] = nid;
 147                         nid_width[nid] = GetSize(sig);
 148                 }
 149
 150                 for (auto cell : module->cells())
 151                 for (auto &conn : cell->connections())
 152                 {
 153                         if (!cell->output(conn.first))
 154                                 continue;
 155
 156                         for (auto bit : sigmap(conn.second))
 157                                 bit_cell[bit] = cell;
 158                 }
 159
 160                 for (auto wire : module->wires())
 161                 {
 162                         if (!wire->port_id || !wire->port_output)
 163                                 continue;
 164
 165                         int nid = get_sig_nid(wire);
 166                         f << stringf("%d output %d %s\n", next_nid++, nid, log_id(wire));
 167                 }
 168         }
 169 };
 170
 171 struct BtorBackend : public Backend {
 172         BtorBackend() : Backend("btor", "write design to BTOR file") { }
 173         virtual void help()
 174         {
 175                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 176                 log("\n");
 177                 log("    write_btor [options] [filename]\n");
 178                 log("\n");
 179                 log("Write a BTOR description of the current design.\n");
 180                 log("\n");
 181         }
 182         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 183         {
 184                 bool verbose = false;
 185
 186                 log_header(design, "Executing BTOR backend.\n");
 187
 188                 size_t argidx;
 189                 for (argidx = 1; argidx < args.size(); argidx++)
 190                 {
 191                         if (args[argidx] == "-verbose") {
 192                                 verbose = true;
 193                                 continue;
 194                         }
 195                         break;
 196                 }
 197                 extra_args(f, filename, args, argidx);
 198
 199                 RTLIL::Module *topmod = design->top_module();
 200
 201                 if (topmod == nullptr)
 202                         log_cmd_error("No top module found.\n");
 203
 204                 *f << stringf("; BTOR description generated by %s for module %s.\n",
 205                                 yosys_version_str, log_id(topmod));
 206
 207                 BtorWorker(*f, topmod, verbose);
 208
 209                 *f << stringf("; end of yosys output\n");
 210         }
 211 } BtorBackend;
 212
 213 PRIVATE_NAMESPACE_END