passes/sat/fmcombine.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 opts_t
  28 {
  29         bool initeq = false;
  30         bool anyeq = false;
  31         bool fwd = false;
  32         bool bwd = false;
  33         bool nop = false;
  34 };
  35
  36 struct FmcombineWorker
  37 {
  38         const opts_t &opts;
  39         Design *design;
  40         Module *original = nullptr;
  41         Module *module = nullptr;
  42         IdString orig_type, combined_type;
  43
  44         FmcombineWorker(Design *design, IdString orig_type, const opts_t &opts) :
  45                         opts(opts), design(design), original(design->module(orig_type)),
  46                         orig_type(orig_type), combined_type("$fmcombine" + orig_type.str())
  47         {
  48         }
  49
  50         SigSpec import_sig(SigSpec sig, const string &suffix)
  51         {
  52                 SigSpec newsig;
  53                 for (auto chunk : sig.chunks()) {
  54                         if (chunk.wire != nullptr)
  55                                 chunk.wire = module->wire(chunk.wire->name.str() + suffix);
  56                         newsig.append(chunk);
  57                 }
  58                 return newsig;
  59         }
  60
  61         Cell *import_prim_cell(Cell *cell, const string &suffix)
  62         {
  63                 Cell *c = module->addCell(cell->name.str() + suffix, cell->type);
  64                 c->parameters = cell->parameters;
  65                 c->attributes = cell->attributes;
  66
  67                 for (auto &conn : cell->connections())
  68                         c->setPort(conn.first, import_sig(conn.second, suffix));
  69
  70                 return c;
  71         }
  72
  73         void import_hier_cell(Cell *cell)
  74         {
  75                 if (!cell->parameters.empty())
  76                         log_cmd_error("Cell %s.%s has unresolved instance parameters.\n", log_id(original), log_id(cell));
  77
  78                 FmcombineWorker sub_worker(design, cell->type, opts);
  79                 sub_worker.generate();
  80
  81                 Cell *c = module->addCell(cell->name.str() + "_combined", sub_worker.combined_type);
  82                 // c->parameters = cell->parameters;
  83                 c->attributes = cell->attributes;
  84
  85                 for (auto &conn : cell->connections()) {
  86                         c->setPort(conn.first.str() + "_gold", import_sig(conn.second, "_gold"));
  87                         c->setPort(conn.first.str() + "_gate", import_sig(conn.second, "_gate"));
  88                 }
  89         }
  90
  91         void generate()
  92         {
  93                 if (design->module(combined_type)) {
  94                         // log("Combined module %s already exists.\n", log_id(combined_type));
  95                         return;
  96                 }
  97
  98                 log("Generating combined module %s from module %s.\n", log_id(combined_type), log_id(orig_type));
  99                 module = design->addModule(combined_type);
 100
 101                 for (auto wire : original->wires()) {
 102                         module->addWire(wire->name.str() + "_gold", wire);
 103                         module->addWire(wire->name.str() + "_gate", wire);
 104                 }
 105                 module->fixup_ports();
 106
 107                 for (auto cell : original->cells()) {
 108                         if (design->module(cell->type) == nullptr) {
 109                                 if (opts.anyeq && cell->type.in("$anyseq", "$anyconst")) {
 110                                         Cell *gold = import_prim_cell(cell, "_gold");
 111                                         for (auto &conn : cell->connections())
 112                                                 module->connect(import_sig(conn.second, "_gate"), gold->getPort(conn.first));
 113                                 } else {
 114                                         Cell *gold = import_prim_cell(cell, "_gold");
 115                                         Cell *gate = import_prim_cell(cell, "_gate");
 116                                         if (opts.initeq) {
 117                                                 if (cell->type.in("$ff", "$dff", "$dffe",
 118                                                                 "$dffsr", "$adff", "$dlatch", "$dlatchsr")) {
 119                                                         SigSpec gold_q = gold->getPort("\\Q");
 120                                                         SigSpec gate_q = gate->getPort("\\Q");
 121                                                         SigSpec en = module->Initstate(NEW_ID);
 122                                                         SigSpec eq = module->Eq(NEW_ID, gold_q, gate_q);
 123                                                         module->addAssume(NEW_ID, eq, en);
 124                                                 }
 125                                         }
 126                                 }
 127                         } else {
 128                                 import_hier_cell(cell);
 129                         }
 130                 }
 131
 132                 for (auto &conn : original->connections()) {
 133                         module->connect(import_sig(conn.first, "_gold"), import_sig(conn.second, "_gold"));
 134                         module->connect(import_sig(conn.first, "_gate"), import_sig(conn.second, "_gate"));
 135                 }
 136
 137                 if (opts.nop)
 138                         return;
 139
 140                 CellTypes ct;
 141                 ct.setup_internals_eval();
 142                 ct.setup_stdcells_eval();
 143
 144                 SigMap sigmap(module);
 145
 146                 dict<SigBit, SigBit> data_bit_to_eq_net;
 147                 dict<Cell*, SigSpec> cell_to_eq_nets;
 148                 dict<SigSpec, SigSpec> reduce_db;
 149                 dict<SigSpec, SigSpec> invert_db;
 150
 151                 for (auto cell : original->cells())
 152                 {
 153                         if (!ct.cell_known(cell->type))
 154                                 continue;
 155
 156                         for (auto &conn : cell->connections())
 157                         {
 158                                 if (!cell->output(conn.first))
 159                                         continue;
 160
 161                                 SigSpec A = import_sig(conn.second, "_gold");
 162                                 SigSpec B = import_sig(conn.second, "_gate");
 163                                 SigBit EQ = module->Eq(NEW_ID, A, B);
 164
 165                                 for (auto bit : sigmap({A, B}))
 166                                         data_bit_to_eq_net[bit] = EQ;
 167
 168                                 cell_to_eq_nets[cell].append(EQ);
 169                         }
 170                 }
 171
 172                 for (auto cell : original->cells())
 173                 {
 174                         if (!ct.cell_known(cell->type))
 175                                 continue;
 176
 177                         bool skip_cell = !cell_to_eq_nets.count(cell);
 178                         pool<SigBit> src_eq_bits;
 179
 180                         for (auto &conn : cell->connections())
 181                         {
 182                                 if (skip_cell)
 183                                         break;
 184
 185                                 if (cell->output(conn.first))
 186                                         continue;
 187
 188                                 SigSpec A = import_sig(conn.second, "_gold");
 189                                 SigSpec B = import_sig(conn.second, "_gate");
 190
 191                                 for (auto bit : sigmap({A, B})) {
 192                                         if (data_bit_to_eq_net.count(bit))
 193                                                 src_eq_bits.insert(data_bit_to_eq_net.at(bit));
 194                                         else
 195                                                 skip_cell = true;
 196                                 }
 197                         }
 198
 199                         if (!skip_cell) {
 200                                 SigSpec antecedent = SigSpec(src_eq_bits);
 201                                 antecedent.sort_and_unify();
 202
 203                                 if (GetSize(antecedent) > 1) {
 204                                         if (reduce_db.count(antecedent) == 0)
 205                                                 reduce_db[antecedent] = module->ReduceAnd(NEW_ID, antecedent);
 206                                         antecedent = reduce_db.at(antecedent);
 207                                 }
 208
 209                                 SigSpec consequent = cell_to_eq_nets.at(cell);
 210                                 consequent.sort_and_unify();
 211
 212                                 if (GetSize(consequent) > 1) {
 213                                         if (reduce_db.count(consequent) == 0)
 214                                                 reduce_db[consequent] = module->ReduceAnd(NEW_ID, consequent);
 215                                         consequent = reduce_db.at(consequent);
 216                                 }
 217
 218                                 if (opts.fwd)
 219                                         module->addAssume(NEW_ID, consequent, antecedent);
 220
 221                                 if (opts.bwd)
 222                                 {
 223                                         if (invert_db.count(antecedent) == 0)
 224                                                 invert_db[antecedent] = module->Not(NEW_ID, antecedent);
 225
 226                                         if (invert_db.count(consequent) == 0)
 227                                                 invert_db[consequent] = module->Not(NEW_ID, consequent);
 228
 229                                         module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent));
 230                                 }
 231                         }
 232                 }
 233         }
 234 };
 235
 236 struct FmcombinePass : public Pass {
 237         FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { }
 238         void help() YS_OVERRIDE
 239         {
 240                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 241                 log("\n");
 242                 log("    fmcombine [options] module_name gold_cell gate_cell\n");
 243                 // log("    fmcombine [options] @gold_cell @gate_cell\n");
 244                 log("\n");
 245                 log("This pass takes two cells, which are instances of the same module, and replaces\n");
 246                 log("them with one instance of a special 'combined' module, that effectively\n");
 247                 log("contains two copies of the original module, plus some formal properties.\n");
 248                 log("\n");
 249                 log("This is useful for formal test benches that check what differences in behavior\n");
 250                 log("a slight difference in input causes in a module.\n");
 251                 log("\n");
 252                 log("    -initeq\n");
 253                 log("        Insert assumptions that initially all FFs in both circuits have the\n");
 254                 log("        same initial values.\n");
 255                 log("\n");
 256                 log("    -anyeq\n");
 257                 log("        Do not duplicate $anyseq/$anyconst cells.\n");
 258                 log("\n");
 259                 log("    -fwd\n");
 260                 log("        Insert forward hint assumptions into the combined module.\n");
 261                 log("\n");
 262                 log("    -bwd\n");
 263                 log("        Insert backward hint assumptions into the combined module.\n");
 264                 log("        (Backward hints are logically equivalend to fordward hits, but\n");
 265                 log("        some solvers are faster with bwd hints, or even both -bwd and -fwd.)\n");
 266                 log("\n");
 267                 log("    -nop\n");
 268                 log("        Don't insert hint assumptions into the combined module.\n");
 269                 log("        (This should not provide any speedup over the original design, but\n");
 270                 log("        strangely sometimes it does.)\n");
 271                 log("\n");
 272                 log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n");
 273                 log("\n");
 274         }
 275         void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 276         {
 277                 opts_t opts;
 278                 Module *module = nullptr;
 279                 Cell *gold_cell = nullptr;
 280                 Cell *gate_cell = nullptr;
 281
 282                 log_header(design, "Executing FMCOMBINE pass.\n");
 283
 284                 size_t argidx;
 285                 for (argidx = 1; argidx < args.size(); argidx++)
 286                 {
 287                         // if (args[argidx] == "-o" && argidx+1 < args.size()) {
 288                         //      filename = args[++argidx];
 289                         //      continue;
 290                         // }
 291                         if (args[argidx] == "-initeq") {
 292                                 opts.initeq = true;
 293                                 continue;
 294                         }
 295                         if (args[argidx] == "-anyeq") {
 296                                 opts.anyeq = true;
 297                                 continue;
 298                         }
 299                         if (args[argidx] == "-fwd") {
 300                                 opts.fwd = true;
 301                                 continue;
 302                         }
 303                         if (args[argidx] == "-bwd") {
 304                                 opts.bwd = true;
 305                                 continue;
 306                         }
 307                         if (args[argidx] == "-nop") {
 308                                 opts.nop = true;
 309                                 continue;
 310                         }
 311                         break;
 312                 }
 313                 if (argidx+2 == args.size())
 314                 {
 315                         string gold_name = args[argidx++];
 316                         string gate_name = args[argidx++];
 317                         log_cmd_error("fmcombine @gold_cell @gate_cell call style is not implemented yet.");
 318                 }
 319                 else if (argidx+3 == args.size())
 320                 {
 321                         IdString module_name = RTLIL::escape_id(args[argidx++]);
 322                         IdString gold_name = RTLIL::escape_id(args[argidx++]);
 323                         IdString gate_name = RTLIL::escape_id(args[argidx++]);
 324
 325                         module = design->module(module_name);
 326                         if (module == nullptr)
 327                                 log_cmd_error("Module %s not found.\n", log_id(module_name));
 328
 329                         gold_cell = module->cell(gold_name);
 330                         if (gold_cell == nullptr)
 331                                 log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gold_name), log_id(module));
 332
 333                         gate_cell = module->cell(gate_name);
 334                         if (gate_cell == nullptr)
 335                                 log_cmd_error("Gate cell %s not found in module %s.\n", log_id(gate_name), log_id(module));
 336                 }
 337                 else
 338                 {
 339                         log_cmd_error("Invalid number of arguments.\n");
 340                 }
 341                 // extra_args(args, argidx, design);
 342
 343                 if (opts.nop && (opts.fwd || opts.bwd))
 344                         log_cmd_error("Option -nop can not be combined with -fwd and/or -bwd.\n");
 345
 346                 if (!opts.nop && !opts.fwd && !opts.bwd)
 347                         opts.fwd = true;
 348
 349                 if (gold_cell->type != gate_cell->type)
 350                         log_cmd_error("Types of gold and gate cells do not match.\n");
 351                 if (!gold_cell->parameters.empty())
 352                         log_cmd_error("Gold cell has unresolved instance parameters.\n");
 353                 if (!gate_cell->parameters.empty())
 354                         log_cmd_error("Gate cell has unresolved instance parameters.\n");
 355
 356                 FmcombineWorker worker(design, gold_cell->type, opts);
 357                 worker.generate();
 358                 IdString combined_cell_name = module->uniquify(stringf("\\%s_%s", log_id(gold_cell), log_id(gate_cell)));
 359
 360                 Cell *cell = module->addCell(combined_cell_name, worker.combined_type);
 361                 cell->attributes = gold_cell->attributes;
 362                 cell->add_strpool_attribute("\\src", gate_cell->get_strpool_attribute("\\src"));
 363
 364                 log("Combining cells %s and %s in module %s into new cell %s.\n", log_id(gold_cell), log_id(gate_cell), log_id(module), log_id(cell));
 365
 366                 for (auto &conn : gold_cell->connections())
 367                         cell->setPort(conn.first.str() + "_gold", conn.second);
 368                 module->remove(gold_cell);
 369
 370                 for (auto &conn : gate_cell->connections())
 371                         cell->setPort(conn.first.str() + "_gate", conn.second);
 372                 module->remove(gate_cell);
 373         }
 374 } FmcombinePass;
 375
 376 PRIVATE_NAMESPACE_END