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 uses temporal induction to check circuit equivalence before and\n");
  36                 log("after an optimization pass.\n");
  37                 log("\n");
  38                 log("    -run <from_label>:<to_label>\n");
  39                 log("        only run the commands between the labels (see below). an empty\n");
  40                 log("        from label is synonymous to the start of the command list, and empty to\n");
  41                 log("        label is synonymous to the end of the command list.\n");
  42                 log("\n");
  43                 log("    -map <filename>\n");
  44                 log("        expand the modules in this file before proving equivalence. this is\n");
  45                 log("        useful for handling architecture-specific primitives.\n");
  46                 log("\n");
  47                 log("    -blacklist <file>\n");
  48                 log("        Do not match cells or signals that match the names in the file\n");
  49                 log("        (passed to equiv_make).\n");
  50                 log("\n");
  51                 log("    -assert\n");
  52                 log("        produce an error if the circuits are not equivalent.\n");
  53                 log("\n");
  54                 log("    -multiclock\n");
  55                 log("        run clk2fflogic before equivalence checking.\n");
  56                 log("\n");
  57                 log("    -async2sync\n");
  58                 log("        run async2sync before equivalence checking.\n");
  59                 log("\n");
  60                 log("    -undef\n");
  61                 log("        enable modelling of undef states during equiv_induct.\n");
  62                 log("\n");
  63                 log("The following commands are executed by this verification command:\n");
  64                 help_script();
  65                 log("\n");
  66         }
  67
  68         std::string command, techmap_opts, make_opts;
  69         bool assert, undef, multiclock, async2sync;
  70
  71         void clear_flags() YS_OVERRIDE
  72         {
  73                 command = "";
  74                 techmap_opts = "";
  75                 make_opts = "";
  76                 assert = false;
  77                 undef = false;
  78                 multiclock = false;
  79                 async2sync = false;
  80         }
  81
  82         void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
  83         {
  84                 string run_from, run_to;
  85                 clear_flags();
  86
  87                 size_t argidx;
  88                 for (argidx = 1; argidx < args.size(); argidx++) {
  89                         if (args[argidx] == "-run" && argidx + 1 < args.size()) {
  90                                 size_t pos = args[argidx + 1].find(':');
  91                                 if (pos == std::string::npos)
  92                                         break;
  93                                 run_from = args[++argidx].substr(0, pos);
  94                                 run_to = args[argidx].substr(pos + 1);
  95                                 continue;
  96                         }
  97                         if (args[argidx] == "-map" && argidx + 1 < args.size()) {
  98                                 techmap_opts += " -map " + args[++argidx];
  99                                 continue;
 100                         }
 101                         if (args[argidx] == "-blacklist" && argidx + 1 < args.size()) {
 102                                 make_opts += " -blacklist " + args[++argidx];
 103                                 continue;
 104                         }
 105                         if (args[argidx] == "-assert") {
 106                                 assert = true;
 107                                 continue;
 108                         }
 109                         if (args[argidx] == "-undef") {
 110                                 undef = true;
 111                                 continue;
 112                         }
 113                         if (args[argidx] == "-multiclock") {
 114                                 multiclock = true;
 115                                 continue;
 116                         }
 117                         if (args[argidx] == "-async2sync") {
 118                                 async2sync = true;
 119                                 continue;
 120                         }
 121                         break;
 122                 }
 123
 124                 for (; argidx < args.size(); argidx++) {
 125                         if (command.empty()) {
 126                                 if (args[argidx].compare(0, 1, "-") == 0)
 127                                         cmd_error(args, argidx, "Unknown option.");
 128                         } else {
 129                                 command += " ";
 130                         }
 131                         command += args[argidx];
 132                 }
 133
 134                 if (command.empty())
 135                         log_cmd_error("No optimization pass specified!\n");
 136
 137                 if (!design->full_selection())
 138                         log_cmd_error("This command only operates on fully selected designs!\n");
 139
 140                 if (async2sync && multiclock)
 141                         log_cmd_error("The '-async2sync' and '-multiclock' options are mutually exclusive!\n");
 142
 143                 log_header(design, "Executing EQUIV_OPT pass.\n");
 144                 log_push();
 145
 146                 run_script(design, run_from, run_to);
 147
 148                 log_pop();
 149         }
 150
 151         void script() YS_OVERRIDE
 152         {
 153                 if (check_label("run_pass")) {
 154                         run("hierarchy -auto-top");
 155                         run("design -save preopt");
 156                         if (help_mode)
 157                                 run("[command]");
 158                         else
 159                                 run(command);
 160                         run("design -stash postopt");
 161                 }
 162
 163                 if (check_label("prepare")) {
 164                         run("design -copy-from preopt  -as gold A:top");
 165                         run("design -copy-from postopt -as gate A:top");
 166                 }
 167
 168                 if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)")) {
 169                         string opts;
 170                         if (help_mode)
 171                                 opts = " -map <filename> ...";
 172                         else
 173                                 opts = techmap_opts;
 174                         run("techmap -wb -D EQUIV -autoproc" + opts);
 175                 }
 176
 177                 if (check_label("prove")) {
 178                         if (multiclock || help_mode)
 179                                 run("clk2fflogic", "(only with -multiclock)");
 180                         if (async2sync || help_mode)
 181                                 run("async2sync", " (only with -async2sync)");
 182                         string opts;
 183                         if (help_mode)
 184                                 opts = " -blacklist <filename> ...";
 185                         else
 186                                 opts = make_opts;
 187                         run("equiv_make" + opts + " gold gate equiv");
 188                         if (help_mode)
 189                                 run("equiv_induct [-undef] equiv");
 190                         else if (undef)
 191                                 run("equiv_induct -undef equiv");
 192                         else
 193                                 run("equiv_induct equiv");
 194                         if (help_mode)
 195                                 run("equiv_status [-assert] equiv");
 196                         else if (assert)
 197                                 run("equiv_status -assert equiv");
 198                         else
 199                                 run("equiv_status equiv");
 200                 }
 201
 202                 if (check_label("restore")) {
 203                         run("design -load preopt");
 204                 }
 205         }
 206 } EquivOptPass;
 207
 208 PRIVATE_NAMESPACE_END