passes/sat/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/register.h"
  21 #include "kernel/rtlil.h"
  22 #include "kernel/log.h"
  23
  24 USING_YOSYS_NAMESPACE
  25 PRIVATE_NAMESPACE_BEGIN
  26
  27 void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
  28 {
  29         bool flag_ignore_gold_x = false;
  30         bool flag_make_outputs = false;
  31         bool flag_make_outcmp = false;
  32         bool flag_make_assert = false;
  33         bool flag_flatten = false;
  34
  35         log_header(design, "Executing MITER pass (creating miter circuit).\n");
  36
  37         size_t argidx;
  38         for (argidx = 2; argidx < args.size(); argidx++)
  39         {
  40                 if (args[argidx] == "-ignore_gold_x") {
  41                         flag_ignore_gold_x = true;
  42                         continue;
  43                 }
  44                 if (args[argidx] == "-make_outputs") {
  45                         flag_make_outputs = true;
  46                         continue;
  47                 }
  48                 if (args[argidx] == "-make_outcmp") {
  49                         flag_make_outcmp = true;
  50                         continue;
  51                 }
  52                 if (args[argidx] == "-make_assert") {
  53                         flag_make_assert = true;
  54                         continue;
  55                 }
  56                 if (args[argidx] == "-flatten") {
  57                         flag_flatten = true;
  58                         continue;
  59                 }
  60                 break;
  61         }
  62         if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
  63                 that->cmd_error(args, argidx, "command argument error");
  64
  65         RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
  66         RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]);
  67         RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]);
  68
  69         if (design->modules_.count(gold_name) == 0)
  70                 log_cmd_error("Can't find gold module %s!\n", gold_name.c_str());
  71         if (design->modules_.count(gate_name) == 0)
  72                 log_cmd_error("Can't find gate module %s!\n", gate_name.c_str());
  73         if (design->modules_.count(miter_name) != 0)
  74                 log_cmd_error("There is already a module %s!\n", miter_name.c_str());
  75
  76         RTLIL::Module *gold_module = design->modules_.at(gold_name);
  77         RTLIL::Module *gate_module = design->modules_.at(gate_name);
  78
  79         for (auto &it : gold_module->wires_) {
  80                 RTLIL::Wire *w1 = it.second, *w2;
  81                 if (w1->port_id == 0)
  82                         continue;
  83                 if (gate_module->wires_.count(it.second->name) == 0)
  84                         goto match_gold_port_error;
  85                 w2 = gate_module->wires_.at(it.second->name);
  86                 if (w1->port_input != w2->port_input)
  87                         goto match_gold_port_error;
  88                 if (w1->port_output != w2->port_output)
  89                         goto match_gold_port_error;
  90                 if (w1->width != w2->width)
  91                         goto match_gold_port_error;
  92                 continue;
  93         match_gold_port_error:
  94                 log_cmd_error("No matching port in gate module was found for %s!\n", it.second->name.c_str());
  95         }
  96
  97         for (auto &it : gate_module->wires_) {
  98                 RTLIL::Wire *w1 = it.second, *w2;
  99                 if (w1->port_id == 0)
 100                         continue;
 101                 if (gold_module->wires_.count(it.second->name) == 0)
 102                         goto match_gate_port_error;
 103                 w2 = gold_module->wires_.at(it.second->name);
 104                 if (w1->port_input != w2->port_input)
 105                         goto match_gate_port_error;
 106                 if (w1->port_output != w2->port_output)
 107                         goto match_gate_port_error;
 108                 if (w1->width != w2->width)
 109                         goto match_gate_port_error;
 110                 continue;
 111         match_gate_port_error:
 112                 log_cmd_error("No matching port in gold module was found for %s!\n", it.second->name.c_str());
 113         }
 114
 115         log("Creating miter cell \"%s\" with gold cell \"%s\" and gate cell \"%s\".\n", RTLIL::id2cstr(miter_name), RTLIL::id2cstr(gold_name), RTLIL::id2cstr(gate_name));
 116
 117         RTLIL::Module *miter_module = new RTLIL::Module;
 118         miter_module->name = miter_name;
 119         design->add(miter_module);
 120
 121         RTLIL::Cell *gold_cell = miter_module->addCell("\\gold", gold_name);
 122         RTLIL::Cell *gate_cell = miter_module->addCell("\\gate", gate_name);
 123
 124         RTLIL::SigSpec all_conditions;
 125
 126         for (auto &it : gold_module->wires_)
 127         {
 128                 RTLIL::Wire *w1 = it.second;
 129
 130                 if (w1->port_input)
 131                 {
 132                         RTLIL::Wire *w2 = miter_module->addWire("\\in_" + RTLIL::unescape_id(w1->name), w1->width);
 133                         w2->port_input = true;
 134
 135                         gold_cell->setPort(w1->name, w2);
 136                         gate_cell->setPort(w1->name, w2);
 137                 }
 138
 139                 if (w1->port_output)
 140                 {
 141                         RTLIL::Wire *w2_gold = miter_module->addWire("\\gold_" + RTLIL::unescape_id(w1->name), w1->width);
 142                         w2_gold->port_output = flag_make_outputs;
 143
 144                         RTLIL::Wire *w2_gate = miter_module->addWire("\\gate_" + RTLIL::unescape_id(w1->name), w1->width);
 145                         w2_gate->port_output = flag_make_outputs;
 146
 147                         gold_cell->setPort(w1->name, w2_gold);
 148                         gate_cell->setPort(w1->name, w2_gate);
 149
 150                         RTLIL::SigSpec this_condition;
 151
 152                         if (flag_ignore_gold_x)
 153                         {
 154                                 RTLIL::SigSpec gold_x = miter_module->addWire(NEW_ID, w2_gold->width);
 155                                 for (int i = 0; i < w2_gold->width; i++) {
 156                                         RTLIL::Cell *eqx_cell = miter_module->addCell(NEW_ID, "$eqx");
 157                                         eqx_cell->parameters["\\A_WIDTH"] = 1;
 158                                         eqx_cell->parameters["\\B_WIDTH"] = 1;
 159                                         eqx_cell->parameters["\\Y_WIDTH"] = 1;
 160                                         eqx_cell->parameters["\\A_SIGNED"] = 0;
 161                                         eqx_cell->parameters["\\B_SIGNED"] = 0;
 162                                         eqx_cell->setPort("\\A", RTLIL::SigSpec(w2_gold, i));
 163                                         eqx_cell->setPort("\\B", RTLIL::State::Sx);
 164                                         eqx_cell->setPort("\\Y", gold_x.extract(i, 1));
 165                                 }
 166
 167                                 RTLIL::SigSpec gold_masked = miter_module->addWire(NEW_ID, w2_gold->width);
 168                                 RTLIL::SigSpec gate_masked = miter_module->addWire(NEW_ID, w2_gate->width);
 169
 170                                 RTLIL::Cell *or_gold_cell = miter_module->addCell(NEW_ID, "$or");
 171                                 or_gold_cell->parameters["\\A_WIDTH"] = w2_gold->width;
 172                                 or_gold_cell->parameters["\\B_WIDTH"] = w2_gold->width;
 173                                 or_gold_cell->parameters["\\Y_WIDTH"] = w2_gold->width;
 174                                 or_gold_cell->parameters["\\A_SIGNED"] = 0;
 175                                 or_gold_cell->parameters["\\B_SIGNED"] = 0;
 176                                 or_gold_cell->setPort("\\A", w2_gold);
 177                                 or_gold_cell->setPort("\\B", gold_x);
 178                                 or_gold_cell->setPort("\\Y", gold_masked);
 179
 180                                 RTLIL::Cell *or_gate_cell = miter_module->addCell(NEW_ID, "$or");
 181                                 or_gate_cell->parameters["\\A_WIDTH"] = w2_gate->width;
 182                                 or_gate_cell->parameters["\\B_WIDTH"] = w2_gate->width;
 183                                 or_gate_cell->parameters["\\Y_WIDTH"] = w2_gate->width;
 184                                 or_gate_cell->parameters["\\A_SIGNED"] = 0;
 185                                 or_gate_cell->parameters["\\B_SIGNED"] = 0;
 186                                 or_gate_cell->setPort("\\A", w2_gate);
 187                                 or_gate_cell->setPort("\\B", gold_x);
 188                                 or_gate_cell->setPort("\\Y", gate_masked);
 189
 190                                 RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, "$eqx");
 191                                 eq_cell->parameters["\\A_WIDTH"] = w2_gold->width;
 192                                 eq_cell->parameters["\\B_WIDTH"] = w2_gate->width;
 193                                 eq_cell->parameters["\\Y_WIDTH"] = 1;
 194                                 eq_cell->parameters["\\A_SIGNED"] = 0;
 195                                 eq_cell->parameters["\\B_SIGNED"] = 0;
 196                                 eq_cell->setPort("\\A", gold_masked);
 197                                 eq_cell->setPort("\\B", gate_masked);
 198                                 eq_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
 199                                 this_condition = eq_cell->getPort("\\Y");
 200                         }
 201                         else
 202                         {
 203                                 RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, "$eqx");
 204                                 eq_cell->parameters["\\A_WIDTH"] = w2_gold->width;
 205                                 eq_cell->parameters["\\B_WIDTH"] = w2_gate->width;
 206                                 eq_cell->parameters["\\Y_WIDTH"] = 1;
 207                                 eq_cell->parameters["\\A_SIGNED"] = 0;
 208                                 eq_cell->parameters["\\B_SIGNED"] = 0;
 209                                 eq_cell->setPort("\\A", w2_gold);
 210                                 eq_cell->setPort("\\B", w2_gate);
 211                                 eq_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
 212                                 this_condition = eq_cell->getPort("\\Y");
 213                         }
 214
 215                         if (flag_make_outcmp)
 216                         {
 217                                 RTLIL::Wire *w_cmp = miter_module->addWire("\\cmp_" + RTLIL::unescape_id(w1->name));
 218                                 w_cmp->port_output = true;
 219                                 miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
 220                         }
 221
 222                         all_conditions.append(this_condition);
 223                 }
 224         }
 225
 226         if (all_conditions.size() != 1) {
 227                 RTLIL::Cell *reduce_cell = miter_module->addCell(NEW_ID, "$reduce_and");
 228                 reduce_cell->parameters["\\A_WIDTH"] = all_conditions.size();
 229                 reduce_cell->parameters["\\Y_WIDTH"] = 1;
 230                 reduce_cell->parameters["\\A_SIGNED"] = 0;
 231                 reduce_cell->setPort("\\A", all_conditions);
 232                 reduce_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
 233                 all_conditions = reduce_cell->getPort("\\Y");
 234         }
 235
 236         if (flag_make_assert) {
 237                 RTLIL::Cell *assert_cell = miter_module->addCell(NEW_ID, "$assert");
 238                 assert_cell->setPort("\\A", all_conditions);
 239                 assert_cell->setPort("\\EN", State::S1);
 240         }
 241
 242         RTLIL::Wire *w_trigger = miter_module->addWire("\\trigger");
 243         w_trigger->port_output = true;
 244
 245         RTLIL::Cell *not_cell = miter_module->addCell(NEW_ID, "$not");
 246         not_cell->parameters["\\A_WIDTH"] = all_conditions.size();
 247         not_cell->parameters["\\A_WIDTH"] = all_conditions.size();
 248         not_cell->parameters["\\Y_WIDTH"] = w_trigger->width;
 249         not_cell->parameters["\\A_SIGNED"] = 0;
 250         not_cell->setPort("\\A", all_conditions);
 251         not_cell->setPort("\\Y", w_trigger);
 252
 253         miter_module->fixup_ports();
 254
 255         if (flag_flatten) {
 256                 log_push();
 257                 Pass::call_on_module(design, miter_module, "flatten -wb; opt_expr -keepdc -undriven;;");
 258                 log_pop();
 259         }
 260 }
 261
 262 void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
 263 {
 264         bool flag_make_outputs = false;
 265         bool flag_flatten = false;
 266
 267         log_header(design, "Executing MITER pass (creating miter circuit).\n");
 268
 269         size_t argidx;
 270         for (argidx = 2; argidx < args.size(); argidx++)
 271         {
 272                 if (args[argidx] == "-make_outputs") {
 273                         flag_make_outputs = true;
 274                         continue;
 275                 }
 276                 if (args[argidx] == "-flatten") {
 277                         flag_flatten = true;
 278                         continue;
 279                 }
 280                 break;
 281         }
 282         if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].compare(0, 1, "-") == 0)
 283                 that->cmd_error(args, argidx, "command argument error");
 284
 285         IdString module_name = RTLIL::escape_id(args[argidx++]);
 286         IdString miter_name = argidx < args.size() ? RTLIL::escape_id(args[argidx++]) : "";
 287
 288         if (design->modules_.count(module_name) == 0)
 289                 log_cmd_error("Can't find module %s!\n", module_name.c_str());
 290         if (!miter_name.empty() && design->modules_.count(miter_name) != 0)
 291                 log_cmd_error("There is already a module %s!\n", miter_name.c_str());
 292
 293         Module *module = design->module(module_name);
 294
 295         if (!miter_name.empty()) {
 296                 module = module->clone();
 297                 module->name = miter_name;
 298                 design->add(module);
 299         }
 300
 301         if (!flag_make_outputs)
 302                 for (auto wire : module->wires())
 303                         wire->port_output = false;
 304
 305         Wire *trigger = module->addWire("\\trigger");
 306         trigger->port_output = true;
 307         module->fixup_ports();
 308
 309         if (flag_flatten) {
 310                 log_push();
 311                 Pass::call_on_module(design, module, "flatten -wb;;");
 312                 log_pop();
 313         }
 314
 315         SigSpec assert_signals, assume_signals;
 316         vector<Cell*> cell_list = module->cells();
 317         for (auto cell : cell_list)
 318         {
 319                 if (!cell->type.in("$assert", "$assume"))
 320                         continue;
 321
 322                 SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
 323                 SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
 324
 325                 if (cell->type == "$assert") {
 326                         assert_signals.append(module->And(NEW_ID, is_active, is_enabled));
 327                 } else {
 328                         assume_signals.append(module->And(NEW_ID, is_active, is_enabled));
 329                 }
 330
 331                 module->remove(cell);
 332         }
 333
 334         if (assume_signals.empty())
 335         {
 336                 module->addReduceOr(NEW_ID, assert_signals, trigger);
 337         }
 338         else
 339         {
 340                 Wire *assume_q = module->addWire(NEW_ID);
 341                 assume_q->attributes["\\init"] = State::S0;
 342                 assume_signals.append(assume_q);
 343
 344                 SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
 345                 SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
 346                 module->addFf(NEW_ID, assume_nok, assume_q);
 347
 348                 SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
 349                 module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);
 350         }
 351
 352         if (flag_flatten) {
 353                 log_push();
 354                 Pass::call_on_module(design, module, "opt_expr -keepdc -undriven;;");
 355                 log_pop();
 356         }
 357 }
 358
 359 struct MiterPass : public Pass {
 360         MiterPass() : Pass("miter", "automatically create a miter circuit") { }
 361         void help() YS_OVERRIDE
 362         {
 363                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 364                 log("\n");
 365                 log("    miter -equiv [options] gold_name gate_name miter_name\n");
 366                 log("\n");
 367                 log("Creates a miter circuit for equivalence checking. The gold- and gate- modules\n");
 368                 log("must have the same interfaces. The miter circuit will have all inputs of the\n");
 369                 log("two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'\n");
 370                 log("output that goes high if an output mismatch between the two source modules is\n");
 371                 log("detected.\n");
 372                 log("\n");
 373                 log("    -ignore_gold_x\n");
 374                 log("        a undef (x) bit in the gold module output will match any value in\n");
 375                 log("        the gate module output.\n");
 376                 log("\n");
 377                 log("    -make_outputs\n");
 378                 log("        also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs\n");
 379                 log("        on the miter circuit.\n");
 380                 log("\n");
 381                 log("    -make_outcmp\n");
 382                 log("        also create a cmp_* output for each gold/gate output pair.\n");
 383                 log("\n");
 384                 log("    -make_assert\n");
 385                 log("        also create an 'assert' cell that checks if trigger is always low.\n");
 386                 log("\n");
 387                 log("    -flatten\n");
 388                 log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
 389                 log("\n");
 390                 log("\n");
 391                 log("    miter -assert [options] module [miter_name]\n");
 392                 log("\n");
 393                 log("Creates a miter circuit for property checking. All input ports are kept,\n");
 394                 log("output ports are discarded. An additional output 'trigger' is created that\n");
 395                 log("goes high when an assert is violated. Without a miter_name, the existing\n");
 396                 log("module is modified.\n");
 397                 log("\n");
 398                 log("    -make_outputs\n");
 399                 log("        keep module output ports.\n");
 400                 log("\n");
 401                 log("    -flatten\n");
 402                 log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
 403                 log("\n");
 404         }
 405         void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 406         {
 407                 if (args.size() > 1 && args[1] == "-equiv") {
 408                         create_miter_equiv(this, args, design);
 409                         return;
 410                 }
 411
 412                 if (args.size() > 1 && args[1] == "-assert") {
 413                         create_miter_assert(this, args, design);
 414                         return;
 415                 }
 416
 417                 log_cmd_error("Missing mode parameter!\n");
 418         }
 419 } MiterPass;
 420
 421 PRIVATE_NAMESPACE_END