passes/equiv/equiv_miter.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/yosys.h"
  21 #include "kernel/sigtools.h"
  22 #include "kernel/celltypes.h"
  23
  24 USING_YOSYS_NAMESPACE
  25 PRIVATE_NAMESPACE_BEGIN
  26
  27 struct EquivMiterWorker
  28 {
  29         CellTypes ct;
  30         SigMap sigmap;
  31
  32         bool mode_trigger;
  33         bool mode_cmp;
  34         bool mode_assert;
  35         bool mode_undef;
  36
  37         IdString miter_name;
  38         Module *miter_module;
  39         Module *source_module;
  40
  41         dict<SigBit, Cell*> bit_to_driver;
  42         pool<Cell*> seed_cells, miter_cells;
  43         pool<Wire*> miter_wires;
  44
  45         void follow_cone(pool<Cell*> &cone, pool<Cell*> &leaves, Cell *c, bool gold_mode)
  46         {
  47                 if (cone.count(c))
  48                         return;
  49
  50                 if (c->type == ID($equiv) && !seed_cells.count(c)) {
  51                         leaves.insert(c);
  52                         return;
  53                 }
  54
  55                 cone.insert(c);
  56
  57                 for (auto &conn : c->connections()) {
  58                         if (!ct.cell_input(c->type, conn.first))
  59                                 continue;
  60                         if (c->type == ID($equiv) && (conn.first == ID::A) != gold_mode)
  61                                 continue;
  62                         for (auto bit : sigmap(conn.second))
  63                                 if (bit_to_driver.count(bit))
  64                                         follow_cone(cone, leaves, bit_to_driver.at(bit), gold_mode);
  65                 }
  66         }
  67
  68         void find_miter_cells_wires()
  69         {
  70                 sigmap.set(source_module);
  71
  72                 // initialize bit_to_driver
  73
  74                 for (auto c : source_module->cells())
  75                         for (auto &conn : c->connections())
  76                                 if (ct.cell_output(c->type, conn.first))
  77                                         for (auto bit : sigmap(conn.second))
  78                                                 if (bit.wire)
  79                                                         bit_to_driver[bit] = c;
  80
  81                 // find seed cells
  82
  83                 for (auto c : source_module->selected_cells())
  84                         if (c->type == ID($equiv)) {
  85                                 log("Seed $equiv cell: %s\n", log_id(c));
  86                                 seed_cells.insert(c);
  87                         }
  88
  89                 // follow cone from seed cells to next $equiv
  90
  91                 while (1)
  92                 {
  93                         pool<Cell*> gold_cone, gold_leaves;
  94                         pool<Cell*> gate_cone, gate_leaves;
  95
  96                         for (auto c : seed_cells) {
  97                                 follow_cone(gold_cone, gold_leaves, c, true);
  98                                 follow_cone(gate_cone, gate_leaves, c, false);
  99                         }
 100
 101                         log("Gold cone: %d cells (%d leaves).\n", GetSize(gold_cone), GetSize(gold_leaves));
 102                         log("Gate cone: %d cells (%d leaves).\n", GetSize(gate_cone), GetSize(gate_leaves));
 103
 104                         // done if all leaves are shared leaves
 105
 106                         if (gold_leaves == gate_leaves) {
 107                                 miter_cells = gold_cone;
 108                                 miter_cells.insert(gate_cone.begin(), gate_cone.end());
 109                                 log("Selected %d miter cells.\n", GetSize(miter_cells));
 110                                 break;
 111                         }
 112
 113                         // remove shared leaves
 114
 115                         for (auto it = gold_leaves.begin(); it != gold_leaves.end(); ) {
 116                                 auto it2 = gate_leaves.find(*it);
 117                                 if (it2 != gate_leaves.end()) {
 118                                         it = gold_leaves.erase(it);
 119                                         gate_leaves.erase(it2);
 120                                 } else
 121                                         ++it;
 122                         }
 123
 124                         // add remaining leaves to seeds and re-run
 125
 126                         log("Adding %d gold and %d gate seed cells.\n", GetSize(gold_leaves), GetSize(gate_leaves));
 127                         seed_cells.insert(gold_leaves.begin(), gold_leaves.end());
 128                         seed_cells.insert(gate_leaves.begin(), gate_leaves.end());
 129                 }
 130
 131                 for (auto c : miter_cells)
 132                         for (auto &conn : c->connections())
 133                                 for (auto bit : sigmap(conn.second))
 134                                         if (bit.wire)
 135                                                 miter_wires.insert(bit.wire);
 136                 log("Selected %d miter wires.\n", GetSize(miter_wires));
 137         }
 138
 139         void copy_to_miter()
 140         {
 141                 // copy wires and cells
 142
 143                 for (auto w :  miter_wires)
 144                         miter_module->addWire(w->name, w->width);
 145                 for (auto c :  miter_cells) {
 146                         miter_module->addCell(c->name, c);
 147                         auto mc = miter_module->cell(c->name);
 148                         for (auto &conn : mc->connections())
 149                                 mc->setPort(conn.first, sigmap(conn.second));
 150                 }
 151
 152                 // fixup wire references in cells
 153
 154                 sigmap.clear();
 155
 156                 struct RewriteSigSpecWorker {
 157                         RTLIL::Module * mod;
 158                         void operator()(SigSpec &sig) {
 159                                 vector<SigChunk> chunks = sig.chunks();
 160                                 for (auto &c : chunks)
 161                                         if (c.wire != NULL)
 162                                                 c.wire = mod->wires_.at(c.wire->name);
 163                                 sig = chunks;
 164                         }
 165                 };
 166
 167                 RewriteSigSpecWorker rewriteSigSpecWorker;
 168                 rewriteSigSpecWorker.mod = miter_module;
 169                 miter_module->rewrite_sigspecs(rewriteSigSpecWorker);
 170
 171                 // find undriven or unused wires
 172
 173                 pool<SigBit> driven_bits, used_bits;
 174
 175                 for (auto c : miter_module->cells())
 176                 for (auto &conn : c->connections()) {
 177                         if (ct.cell_input(c->type, conn.first))
 178                                 for (auto bit : conn.second)
 179                                         if (bit.wire)
 180                                                 used_bits.insert(bit);
 181                         if (ct.cell_output(c->type, conn.first))
 182                                 for (auto bit : conn.second)
 183                                         if (bit.wire)
 184                                                 driven_bits.insert(bit);
 185                 }
 186
 187                 // create ports
 188
 189                 for (auto w : miter_module->wires()) {
 190                         for (auto bit : SigSpec(w)) {
 191                                 if (driven_bits.count(bit) && !used_bits.count(bit))
 192                                         w->port_output = true;
 193                                 if (!driven_bits.count(bit) && used_bits.count(bit))
 194                                         w->port_input = true;
 195                         }
 196                         if (w->port_output && w->port_input)
 197                                 log("Created miter inout port %s.\n", log_id(w));
 198                         else if (w->port_output)
 199                                 log("Created miter output port %s.\n", log_id(w));
 200                         else if (w->port_input)
 201                                 log("Created miter input port %s.\n", log_id(w));
 202                 }
 203
 204                 miter_module->fixup_ports();
 205         }
 206
 207         void make_stuff()
 208         {
 209                 if (!mode_trigger && !mode_cmp && !mode_assert)
 210                         return;
 211
 212                 SigSpec trigger_signals;
 213                 vector<Cell*> equiv_cells;
 214
 215                 for (auto c : miter_module->cells())
 216                         if (c->type == ID($equiv) && c->getPort(ID::A) != c->getPort(ID::B))
 217                                 equiv_cells.push_back(c);
 218
 219                 for (auto c : equiv_cells)
 220                 {
 221                         SigSpec cmp = mode_undef ?
 222                                         miter_module->LogicOr(NEW_ID, miter_module->Eqx(NEW_ID, c->getPort(ID::A), State::Sx),
 223                                                         miter_module->Eqx(NEW_ID, c->getPort(ID::A), c->getPort(ID::B))) :
 224                                         miter_module->Eq(NEW_ID, c->getPort(ID::A), c->getPort(ID::B));
 225
 226                         if (mode_cmp) {
 227                                 string cmp_name = stringf("\\cmp%s", log_signal(c->getPort(ID::Y)));
 228                                 for (int i = 1; i < GetSize(cmp_name); i++)
 229                                         if (cmp_name[i] == '\\')
 230                                                 cmp_name[i] = '_';
 231                                         else if (cmp_name[i] == ' ')
 232                                                 cmp_name = cmp_name.substr(0, i) + cmp_name.substr(i+1);
 233                                 auto w = miter_module->addWire(cmp_name);
 234                                 w->port_output = true;
 235                                 miter_module->connect(w, cmp);
 236                         }
 237
 238                         if (mode_assert)
 239                                 miter_module->addAssert(NEW_ID, cmp, State::S1);
 240
 241                         trigger_signals.append(miter_module->Not(NEW_ID, cmp));
 242                 }
 243
 244                 if (mode_trigger) {
 245                         auto w = miter_module->addWire(ID(trigger));
 246                         w->port_output = true;
 247                         miter_module->addReduceOr(NEW_ID, trigger_signals, w);
 248                 }
 249
 250                 miter_module->fixup_ports();
 251         }
 252
 253         void run()
 254         {
 255                 log("Creating miter %s from module %s.\n", log_id(miter_module), log_id(source_module));
 256                 find_miter_cells_wires();
 257                 copy_to_miter();
 258                 make_stuff();
 259         }
 260 };
 261
 262 struct EquivMiterPass : public Pass {
 263         EquivMiterPass() : Pass("equiv_miter", "extract miter from equiv circuit") { }
 264         void help() YS_OVERRIDE
 265         {
 266                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 267                 log("\n");
 268                 log("    equiv_miter [options] miter_module [selection]\n");
 269                 log("\n");
 270                 log("This creates a miter module for further analysis of the selected $equiv cells.\n");
 271                 log("\n");
 272                 log("    -trigger\n");
 273                 log("        Create a trigger output\n");
 274                 log("\n");
 275                 log("    -cmp\n");
 276                 log("        Create cmp_* outputs for individual unproven $equiv cells\n");
 277                 log("\n");
 278                 log("    -assert\n");
 279                 log("        Create a $assert cell for each unproven $equiv cell\n");
 280                 log("\n");
 281                 log("    -undef\n");
 282                 log("        Create compare logic that handles undefs correctly\n");
 283                 log("\n");
 284         }
 285         void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 286         {
 287                 EquivMiterWorker worker;
 288                 worker.ct.setup(design);
 289                 worker.mode_trigger = false;
 290                 worker.mode_cmp = false;
 291                 worker.mode_assert = false;
 292                 worker.mode_undef = false;
 293
 294                 size_t argidx;
 295                 for (argidx = 1; argidx < args.size(); argidx++)
 296                 {
 297                         if (args[argidx] == "-trigger") {
 298                                 worker.mode_trigger = true;
 299                                 continue;
 300                         }
 301                         if (args[argidx] == "-cmp") {
 302                                 worker.mode_cmp = true;
 303                                 continue;
 304                         }
 305                         if (args[argidx] == "-assert") {
 306                                 worker.mode_assert = true;
 307                                 continue;
 308                         }
 309                         if (args[argidx] == "-undef") {
 310                                 worker.mode_undef = true;
 311                                 continue;
 312                         }
 313                         break;
 314                 }
 315
 316                 if (argidx >= args.size())
 317                         log_cmd_error("Invalid number of arguments.\n");
 318
 319                 worker.miter_name = RTLIL::escape_id(args[argidx++]);
 320                 extra_args(args, argidx, design);
 321
 322                 if (design->module(worker.miter_name))
 323                         log_cmd_error("Miter module %s already exists.\n", log_id(worker.miter_name));
 324
 325                 worker.source_module = nullptr;
 326                 for (auto m : design->selected_modules()) {
 327                         if (worker.source_module != nullptr)
 328                                 goto found_two_modules;
 329                         worker.source_module = m;
 330                 }
 331
 332                 if (worker.source_module == nullptr)
 333         found_two_modules:
 334                         log_cmd_error("Exactly one module must be selected for 'equiv_miter'!\n");
 335
 336                 log_header(design, "Executing EQUIV_MITER pass.\n");
 337
 338                 worker.miter_module = design->addModule(worker.miter_name);
 339                 worker.run();
 340         }
 341 } EquivMiterPass;
 342
 343 PRIVATE_NAMESPACE_END