passes/equiv/equiv_induct.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/satgen.h"
  22 #include "kernel/sigtools.h"
  23
  24 USING_YOSYS_NAMESPACE
  25 PRIVATE_NAMESPACE_BEGIN
  26
  27 struct EquivInductWorker
  28 {
  29         Module *module;
  30         SigMap sigmap;
  31
  32         vector<Cell*> cells;
  33         pool<Cell*> workset;
  34
  35         ezSatPtr ez;
  36         SatGen satgen;
  37
  38         int max_seq;
  39         int success_counter;
  40
  41         dict<int, int> ez_step_is_consistent;
  42         pool<Cell*> cell_warn_cache;
  43         SigPool undriven_signals;
  44
  45         EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq) : module(module), sigmap(module),
  46                         cells(module->selected_cells()), workset(unproven_equiv_cells),
  47                         satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0)
  48         {
  49                 satgen.model_undef = model_undef;
  50         }
  51
  52         void create_timestep(int step)
  53         {
  54                 vector<int> ez_equal_terms;
  55
  56                 for (auto cell : cells) {
  57                         if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) {
  58                                 log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
  59                                 cell_warn_cache.insert(cell);
  60                         }
  61                         if (cell->type == ID($equiv)) {
  62                                 SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit();
  63                                 SigBit bit_b = sigmap(cell->getPort(ID::B)).as_bit();
  64                                 if (bit_a != bit_b) {
  65                                         int ez_a = satgen.importSigBit(bit_a, step);
  66                                         int ez_b = satgen.importSigBit(bit_b, step);
  67                                         int cond = ez->IFF(ez_a, ez_b);
  68                                         if (satgen.model_undef)
  69                                                 cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step));
  70                                         ez_equal_terms.push_back(cond);
  71                                 }
  72                         }
  73                 }
  74
  75                 if (satgen.model_undef) {
  76                         for (auto bit : undriven_signals.export_all())
  77                                 ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step)));
  78                 }
  79
  80                 log_assert(!ez_step_is_consistent.count(step));
  81                 ez_step_is_consistent[step] = ez->expression(ez->OpAnd, ez_equal_terms);
  82         }
  83
  84         void run()
  85         {
  86                 log("Found %d unproven $equiv cells in module %s:\n", GetSize(workset), log_id(module));
  87
  88                 if (satgen.model_undef) {
  89                         for (auto cell : cells)
  90                                 if (yosys_celltypes.cell_known(cell->type))
  91                                         for (auto &conn : cell->connections())
  92                                                 if (yosys_celltypes.cell_input(cell->type, conn.first))
  93                                                         undriven_signals.add(sigmap(conn.second));
  94                         for (auto cell : cells)
  95                                 if (yosys_celltypes.cell_known(cell->type))
  96                                         for (auto &conn : cell->connections())
  97                                                 if (yosys_celltypes.cell_output(cell->type, conn.first))
  98                                                         undriven_signals.del(sigmap(conn.second));
  99                 }
 100
 101                 create_timestep(1);
 102
 103                 if (satgen.model_undef) {
 104                         for (auto bit : satgen.initial_state.export_all())
 105                                 ez->assume(ez->NOT(satgen.importUndefSigBit(bit, 1)));
 106                         log("  Undef modelling: force def on %d initial reg values and %d inputs.\n",
 107                                 GetSize(satgen.initial_state), GetSize(undriven_signals));
 108                 }
 109
 110                 for (int step = 1; step <= max_seq; step++)
 111                 {
 112                         ez->assume(ez_step_is_consistent[step]);
 113
 114                         log("  Proving existence of base case for step %d. (%d clauses over %d variables)\n", step, ez->numCnfClauses(), ez->numCnfVariables());
 115                         if (!ez->solve()) {
 116                                 log("  Proof for base case failed. Circuit inherently diverges!\n");
 117                                 return;
 118                         }
 119
 120                         create_timestep(step+1);
 121                         int new_step_not_consistent = ez->NOT(ez_step_is_consistent[step+1]);
 122                         ez->bind(new_step_not_consistent);
 123
 124                         log("  Proving induction step %d. (%d clauses over %d variables)\n", step, ez->numCnfClauses(), ez->numCnfVariables());
 125                         if (!ez->solve(new_step_not_consistent)) {
 126                                 log("  Proof for induction step holds. Entire workset of %d cells proven!\n", GetSize(workset));
 127                                 for (auto cell : workset)
 128                                         cell->setPort(ID::B, cell->getPort(ID::A));
 129                                 success_counter += GetSize(workset);
 130                                 return;
 131                         }
 132
 133                         log("  Proof for induction step failed. %s\n", step != max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset.");
 134                 }
 135
 136                 workset.sort();
 137
 138                 for (auto cell : workset)
 139                 {
 140                         SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit();
 141                         SigBit bit_b = sigmap(cell->getPort(ID::B)).as_bit();
 142
 143                         log("  Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort(ID::Y))));
 144
 145                         int ez_a = satgen.importSigBit(bit_a, max_seq+1);
 146                         int ez_b = satgen.importSigBit(bit_b, max_seq+1);
 147                         int cond = ez->XOR(ez_a, ez_b);
 148
 149                         if (satgen.model_undef)
 150                                 cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1)));
 151
 152                         if (!ez->solve(cond)) {
 153                                 log(" success!\n");
 154                                 cell->setPort(ID::B, cell->getPort(ID::A));
 155                                 success_counter++;
 156                         } else {
 157                                 log(" failed.\n");
 158                         }
 159                 }
 160         }
 161 };
 162
 163 struct EquivInductPass : public Pass {
 164         EquivInductPass() : Pass("equiv_induct", "proving $equiv cells using temporal induction") { }
 165         void help() YS_OVERRIDE
 166         {
 167                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 168                 log("\n");
 169                 log("    equiv_induct [options] [selection]\n");
 170                 log("\n");
 171                 log("Uses a version of temporal induction to prove $equiv cells.\n");
 172                 log("\n");
 173                 log("Only selected $equiv cells are proven and only selected cells are used to\n");
 174                 log("perform the proof.\n");
 175                 log("\n");
 176                 log("    -undef\n");
 177                 log("        enable modelling of undef states\n");
 178                 log("\n");
 179                 log("    -seq <N>\n");
 180                 log("        the max. number of time steps to be considered (default = 4)\n");
 181                 log("\n");
 182                 log("This command is very effective in proving complex sequential circuits, when\n");
 183                 log("the internal state of the circuit quickly propagates to $equiv cells.\n");
 184                 log("\n");
 185                 log("However, this command uses a weak definition of 'equivalence': This command\n");
 186                 log("proves that the two circuits will not diverge after they produce equal\n");
 187                 log("outputs (observable points via $equiv) for at least <N> cycles (the <N>\n");
 188                 log("specified via -seq).\n");
 189                 log("\n");
 190                 log("Combined with simulation this is very powerful because simulation can give\n");
 191                 log("you confidence that the circuits start out synced for at least <N> cycles\n");
 192                 log("after reset.\n");
 193                 log("\n");
 194         }
 195         void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
 196         {
 197                 int success_counter = 0;
 198                 bool model_undef = false;
 199                 int max_seq = 4;
 200
 201                 log_header(design, "Executing EQUIV_INDUCT pass.\n");
 202
 203                 size_t argidx;
 204                 for (argidx = 1; argidx < args.size(); argidx++) {
 205                         if (args[argidx] == "-undef") {
 206                                 model_undef = true;
 207                                 continue;
 208                         }
 209                         if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 210                                 max_seq = atoi(args[++argidx].c_str());
 211                                 continue;
 212                         }
 213                         break;
 214                 }
 215                 extra_args(args, argidx, design);
 216
 217                 for (auto module : design->selected_modules())
 218                 {
 219                         pool<Cell*> unproven_equiv_cells;
 220
 221                         for (auto cell : module->selected_cells())
 222                                 if (cell->type == ID($equiv)) {
 223                                         if (cell->getPort(ID::A) != cell->getPort(ID::B))
 224                                                 unproven_equiv_cells.insert(cell);
 225                                 }
 226
 227                         if (unproven_equiv_cells.empty()) {
 228                                 log("No selected unproven $equiv cells found in %s.\n", log_id(module));
 229                                 continue;
 230                         }
 231
 232                         EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq);
 233                         worker.run();
 234                         success_counter += worker.success_counter;
 235                 }
 236
 237                 log("Proved %d previously unproven $equiv cells.\n", success_counter);
 238         }
 239 } EquivInductPass;
 240
 241 PRIVATE_NAMESPACE_END