passes/equiv/equiv_opt.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2018  whitequark <whitequark@whitequark.org>
   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
  22 USING_YOSYS_NAMESPACE
  23 PRIVATE_NAMESPACE_BEGIN
  24
  25 struct EquivOptPass : public ScriptPass
  26 {
  27   EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { }
  28
  29   void help() YS_OVERRIDE
  30   {
  31     //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
  32     log("\n");
  33     log("    equiv_opt [options] [command]\n");
  34     log("\n");
  35     log("This command checks circuit equivalence before and after an optimization pass.\n");
  36     log("\n");
  37     log("    -run <from_label>:<to_label>\n");
  38     log("        only run the commands between the labels (see below). an empty\n");
  39     log("        from label is synonymous to the start of the command list, and empty to\n");
  40     log("        label is synonymous to the end of the command list.\n");
  41     log("\n");
  42     log("    -map <filename>\n");
  43     log("        expand the modules in this file before proving equivalence. this is\n");
  44     log("        useful for handling architecture-specific primitives.\n");
  45     log("\n");
  46     log("    -assert\n");
  47     log("        produce an error if the circuits are not equivalent\n");
  48     log("\n");
  49     log("The following commands are executed by this verification command:\n");
  50     help_script();
  51     log("\n");
  52   }
  53
  54   std::string command, techmap_opts;
  55   bool assert;
  56
  57   void clear_flags() YS_OVERRIDE
  58   {
  59     command = "";
  60     techmap_opts = "";
  61     assert = false;
  62   }
  63
  64   void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
  65   {
  66     string run_from, run_to;
  67     clear_flags();
  68
  69     size_t argidx;
  70     for (argidx = 1; argidx < args.size(); argidx++)
  71     {
  72       if (args[argidx] == "-run" && argidx+1 < args.size()) {
  73         size_t pos = args[argidx+1].find(':');
  74         if (pos == std::string::npos)
  75           break;
  76         run_from = args[++argidx].substr(0, pos);
  77         run_to = args[argidx].substr(pos+1);
  78         continue;
  79       }
  80       if (args[argidx] == "-map" && argidx+1 < args.size()) {
  81         techmap_opts += " -map " + args[++argidx];
  82         continue;
  83       }
  84       if (args[argidx] == "-assert") {
  85         assert = true;
  86         continue;
  87       }
  88       break;
  89     }
  90
  91     for (; argidx < args.size(); argidx++)
  92     {
  93       if (command.empty())
  94       {
  95         if (args[argidx].substr(0, 1) == "-")
  96           cmd_error(args, argidx, "Unknown option.");
  97       }
  98       else
  99       {
 100         command += " ";
 101       }
 102       command += args[argidx];
 103     }
 104
 105     if (command.empty())
 106       log_cmd_error("No optimization pass specified!\n");
 107
 108     if (!design->full_selection())
 109       log_cmd_error("This command only operates on fully selected designs!\n");
 110
 111     log_header(design, "Executing EQUIV_OPT pass.\n");
 112     log_push();
 113
 114     run_script(design, run_from, run_to);
 115
 116     log_pop();
 117   }
 118
 119   void script() YS_OVERRIDE
 120   {
 121     if (check_label("run_pass"))
 122     {
 123       run("hierarchy -auto-top");
 124       run("design -save preopt");
 125       if (help_mode)
 126         run("[command]");
 127       else
 128         run(command);
 129       run("design -stash postopt");
 130     }
 131
 132     if (check_label("prepare"))
 133     {
 134       run("design -copy-from preopt  -as gold A:top");
 135       run("design -copy-from postopt -as gate A:top");
 136     }
 137
 138     if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)"))
 139     {
 140       string opts;
 141       if (help_mode)
 142         opts = " -map <filename> ...";
 143       else
 144         opts = techmap_opts;
 145       run("techmap -D EQUIV -autoproc" + opts);
 146     }
 147
 148     if (check_label("prove"))
 149     {
 150       run("equiv_make gold gate equiv");
 151       run("equiv_induct equiv");
 152       if (help_mode)
 153         run("equiv_status [-assert] equiv");
 154       else if(assert)
 155         run("equiv_status -assert equiv");
 156       else
 157         run("equiv_status equiv");
 158     }
 159
 160     if (check_label("restore"))
 161     {
 162       run("design -load preopt");
 163     }
 164   }
 165 } EquivOptPass;
 166
 167 PRIVATE_NAMESPACE_END