passes/equiv/equiv_mark.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
  23 USING_YOSYS_NAMESPACE
  24 PRIVATE_NAMESPACE_BEGIN
  25
  26 struct EquivMarkWorker
  27 {
  28         Module *module;
  29         SigMap sigmap;
  30
  31         // cache for traversing signal flow graph
  32         dict<SigBit, pool<IdString>> up_bit2cells;
  33         dict<IdString, pool<SigBit>> up_cell2bits;
  34         pool<IdString> edge_cells, equiv_cells;
  35
  36         // graph traversal state
  37         pool<SigBit> queue, visited;
  38
  39         // assigned regions
  40         dict<IdString, int> cell_regions;
  41         dict<SigBit, int> bit_regions;
  42         int next_region;
  43
  44         // merge-find
  45         mfp<int> region_mf;
  46
  47         EquivMarkWorker(Module *module) : module(module), sigmap(module)
  48         {
  49                 for (auto cell : module->cells())
  50                 {
  51                         if (cell->type == "$equiv")
  52                                 equiv_cells.insert(cell->name);
  53
  54                         for (auto &port : cell->connections())
  55                         {
  56                                 if (cell->input(port.first))
  57                                         for (auto bit : sigmap(port.second))
  58                                                 up_cell2bits[cell->name].insert(bit);
  59
  60                                 if (cell->output(port.first))
  61                                         for (auto bit : sigmap(port.second))
  62                                                 up_bit2cells[bit].insert(cell->name);
  63                         }
  64                 }
  65
  66                 next_region = 0;
  67         }
  68
  69         void mark()
  70         {
  71                 while (!queue.empty())
  72                 {
  73                         pool<IdString> cells;
  74
  75                         for (auto &bit : queue)
  76                         {
  77                                 // log_assert(bit_regions.count(bit) == 0);
  78                                 bit_regions[bit] = next_region;
  79                                 visited.insert(bit);
  80
  81                                 for (auto cell : up_bit2cells[bit])
  82                                         if (edge_cells.count(cell) == 0)
  83                                                 cells.insert(cell);
  84                         }
  85
  86                         queue.clear();
  87
  88                         for (auto cell : cells)
  89                         {
  90                                 if (next_region == 0 && equiv_cells.count(cell))
  91                                         continue;
  92
  93                                 if (cell_regions.count(cell)) {
  94                                         if (cell_regions.at(cell) != 0)
  95                                                 region_mf.merge(cell_regions.at(cell), next_region);
  96                                         continue;
  97                                 }
  98
  99                                 cell_regions[cell] = next_region;
 100
 101                                 for (auto bit : up_cell2bits[cell])
 102                                         if (visited.count(bit) == 0)
 103                                                 queue.insert(bit);
 104                         }
 105                 }
 106
 107                 next_region++;
 108         }
 109
 110         void run()
 111         {
 112                 log("Running equiv_mark on module %s:\n", log_id(module));
 113
 114                 // marking region 0
 115
 116                 for (auto wire : module->wires())
 117                         if (wire->port_id > 0)
 118                                 for (auto bit : sigmap(wire))
 119                                         queue.insert(bit);
 120
 121                 for (auto cell_name : equiv_cells)
 122                 {
 123                         auto cell = module->cell(cell_name);
 124
 125                         SigSpec sig_a = sigmap(cell->getPort("\\A"));
 126                         SigSpec sig_b = sigmap(cell->getPort("\\B"));
 127
 128                         if (sig_a == sig_b) {
 129                                 for (auto bit : sig_a)
 130                                         queue.insert(bit);
 131                                 edge_cells.insert(cell_name);
 132                                 cell_regions[cell_name] = 0;
 133                         }
 134                 }
 135
 136                 mark();
 137
 138                 // marking unsolved regions
 139
 140                 for (auto cell : module->cells())
 141                 {
 142                         if (cell_regions.count(cell->name) || cell->type != "$equiv")
 143                                 continue;
 144
 145                         SigSpec sig_a = sigmap(cell->getPort("\\A"));
 146                         SigSpec sig_b = sigmap(cell->getPort("\\B"));
 147
 148                         log_assert(sig_a != sig_b);
 149
 150                         for (auto bit : sig_a)
 151                                 queue.insert(bit);
 152
 153                         for (auto bit : sig_b)
 154                                 queue.insert(bit);
 155
 156                         cell_regions[cell->name] = next_region;
 157                         mark();
 158                 }
 159
 160                 // setting attributes
 161
 162                 dict<int, int> final_region_map;
 163                 int next_final_region = 0;
 164
 165                 dict<int, int> region_cell_count;
 166                 dict<int, int> region_wire_count;
 167
 168                 for (int i = 0; i < next_region; i++) {
 169                         int r = region_mf.find(i);
 170                         if (final_region_map.count(r) == 0)
 171                                 final_region_map[r] = next_final_region++;
 172                         final_region_map[i] = final_region_map[r];
 173                 }
 174
 175                 for (auto cell : module->cells())
 176                 {
 177                         if (cell_regions.count(cell->name)) {
 178                                 int r = final_region_map.at(cell_regions.at(cell->name));
 179                                 cell->attributes["\\equiv_region"] = Const(r);
 180                                 region_cell_count[r]++;
 181                         } else
 182                                 cell->attributes.erase("\\equiv_region");
 183                 }
 184
 185                 for (auto wire : module->wires())
 186                 {
 187                         pool<int> regions;
 188                         for (auto bit : sigmap(wire))
 189                                 if (bit_regions.count(bit))
 190                                         regions.insert(region_mf.find(bit_regions.at(bit)));
 191
 192                         if (GetSize(regions) == 1) {
 193                                 int r = final_region_map.at(*regions.begin());
 194                                 wire->attributes["\\equiv_region"] = Const(r);
 195                                 region_wire_count[r]++;
 196                         } else
 197                                 wire->attributes.erase("\\equiv_region");
 198                 }
 199
 200                 for (int i = 0; i < next_final_region; i++)
 201                         log("  region %d: %d cells, %d wires\n", i, region_wire_count[i], region_cell_count[i]);
 202         }
 203 };
 204
 205 struct EquivMarkPass : public Pass {
 206         EquivMarkPass() : Pass("equiv_mark", "mark equivalence checking regions") { }
 207         void help() YS_OVERRIDE
 208         {
 209                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 210                 log("\n");
 211                 log("    equiv_mark [options] [selection]\n");
 212                 log("\n");
 213                 log("This command marks the regions in an equivalence checking module. Region 0 is\n");
 214                 log("the proven part of the circuit. Regions with higher numbers are connected\n");
 215                 log("unproven subcricuits. The integer attribute 'equiv_region' is set on all\n");
 216                 log("wires and cells.\n");
 217                 log("\n");
 218         }
 219         void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
 220         {
 221                 log_header(design, "Executing EQUIV_MARK pass.\n");
 222
 223                 size_t argidx;
 224                 for (argidx = 1; argidx < args.size(); argidx++) {
 225                         // if (args[argidx] == "-foobar") {
 226                         //      continue;
 227                         // }
 228                         break;
 229                 }
 230                 extra_args(args, argidx, design);
 231
 232                 for (auto module : design->selected_whole_modules_warn()) {
 233                         EquivMarkWorker worker(module);
 234                         worker.run();
 235                 }
 236         }
 237 } EquivMarkPass;
 238
 239 PRIVATE_NAMESPACE_END