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