kernel/qcsat.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2021  Marcelina Kościelnicka <mwk@0x04.net>
   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/qcsat.h"
  21
  22 USING_YOSYS_NAMESPACE
  23
  24 std::vector<int> QuickConeSat::importSig(SigSpec sig)
  25 {
  26         sig = modwalker.sigmap(sig);
  27         for (auto bit : sig)
  28                 bits_queue.insert(bit);
  29         return satgen.importSigSpec(sig);
  30 }
  31
  32 int QuickConeSat::importSigBit(SigBit bit)
  33 {
  34         bit = modwalker.sigmap(bit);
  35         bits_queue.insert(bit);
  36         return satgen.importSigBit(bit);
  37 }
  38
  39 void QuickConeSat::prepare()
  40 {
  41         while (!bits_queue.empty())
  42         {
  43                 pool<ModWalker::PortBit> portbits;
  44                 modwalker.get_drivers(portbits, bits_queue);
  45
  46                 for (auto bit : bits_queue)
  47                         if (bit.wire && bit.wire->get_bool_attribute(ID::onehot) && !imported_onehot.count(bit.wire))
  48                         {
  49                                 std::vector<int> bits = satgen.importSigSpec(bit.wire);
  50                                 for (int i : bits)
  51                                 for (int j : bits)
  52                                         if (i != j)
  53                                                 ez->assume(ez->NOT(i), j);
  54                                 imported_onehot.insert(bit.wire);
  55                         }
  56
  57                 bits_queue.clear();
  58
  59                 for (auto &pbit : portbits)
  60                 {
  61                         if (imported_cells.count(pbit.cell))
  62                                 continue;
  63                         if (cell_complexity(pbit.cell) > max_cell_complexity)
  64                                 continue;
  65                         if (max_cell_outs && GetSize(modwalker.cell_outputs[pbit.cell]) > max_cell_outs)
  66                                 continue;
  67                         auto &inputs = modwalker.cell_inputs[pbit.cell];
  68                         bits_queue.insert(inputs.begin(), inputs.end());
  69                         satgen.importCell(pbit.cell);
  70                         imported_cells.insert(pbit.cell);
  71                 }
  72
  73                 if (max_cell_count && GetSize(imported_cells) > max_cell_count)
  74                         break;
  75         }
  76 }
  77
  78 int QuickConeSat::cell_complexity(RTLIL::Cell *cell)
  79 {
  80         if (cell->type.in(ID($concat), ID($slice), ID($pos), ID($_BUF_)))
  81                 return 0;
  82         if (cell->type.in(ID($not), ID($and), ID($or), ID($xor), ID($xnor),
  83                         ID($reduce_and), ID($reduce_or), ID($reduce_xor),
  84                         ID($reduce_xnor), ID($reduce_bool),
  85                         ID($logic_not), ID($logic_and), ID($logic_or),
  86                         ID($eq), ID($ne), ID($eqx), ID($nex), ID($fa),
  87                         ID($mux), ID($pmux), ID($lut), ID($sop),
  88                         ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_),
  89                         ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
  90                         ID($_MUX_), ID($_NMUX_), ID($_MUX4_), ID($_MUX8_), ID($_MUX16_),
  91                         ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
  92                 return 1;
  93         if (cell->type.in(ID($neg), ID($add), ID($sub), ID($alu), ID($lcu),
  94                         ID($lt), ID($le), ID($gt), ID($ge)))
  95                 return 2;
  96         if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
  97                 return 3;
  98         if (cell->type.in(ID($mul), ID($macc), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow)))
  99                 return 4;
 100         // Unknown cell.
 101         return 5;
 102 }