Merge pull request #724 from whitequark/equiv_opt

equiv_opt: new command, for verifying optimization passes

passes/equiv/Makefile.inc

@@ -9,4 +9,4 @@ OBJS += passes/equiv/equiv_induct.o
 OBJS += passes/equiv/equiv_struct.o
 OBJS += passes/equiv/equiv_purge.o
 OBJS += passes/equiv/equiv_mark.o
-
+OBJS += passes/equiv/equiv_opt.o

passes/equiv/equiv_opt.cc

@@ -0,0 +1,167 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2018  whitequark <whitequark@whitequark.org>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/register.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EquivOptPass : public ScriptPass
+{
+  EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { }
+
+  void help() YS_OVERRIDE
+  {
+    //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+    log("\n");
+    log("    equiv_opt [options] [command]\n");
+    log("\n");
+    log("This command checks circuit equivalence before and after an optimization pass.\n");
+    log("\n");
+    log("    -run <from_label>:<to_label>\n");
+    log("        only run the commands between the labels (see below). an empty\n");
+    log("        from label is synonymous to the start of the command list, and empty to\n");
+    log("        label is synonymous to the end of the command list.\n");
+    log("\n");
+    log("    -map <filename>\n");
+    log("        expand the modules in this file before proving equivalence. this is\n");
+    log("        useful for handling architecture-specific primitives.\n");
+    log("\n");
+    log("    -assert\n");
+    log("        produce an error if the circuits are not equivalent\n");
+    log("\n");
+    log("The following commands are executed by this verification command:\n");
+    help_script();
+    log("\n");
+  }
+
+  std::string command, techmap_opts;
+  bool assert;
+
+  void clear_flags() YS_OVERRIDE
+  {
+    command = "";
+    techmap_opts = "";
+    assert = false;
+  }
+
+  void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+  {
+    string run_from, run_to;
+    clear_flags();
+
+    size_t argidx;
+    for (argidx = 1; argidx < args.size(); argidx++)
+    {
+      if (args[argidx] == "-run" && argidx+1 < args.size()) {
+        size_t pos = args[argidx+1].find(':');
+        if (pos == std::string::npos)
+          break;
+        run_from = args[++argidx].substr(0, pos);
+        run_to = args[argidx].substr(pos+1);
+        continue;
+      }
+      if (args[argidx] == "-map" && argidx+1 < args.size()) {
+        techmap_opts += " -map " + args[++argidx];
+        continue;
+      }
+      if (args[argidx] == "-assert") {
+        assert = true;
+        continue;
+      }
+      break;
+    }
+
+    for (; argidx < args.size(); argidx++)
+    {
+      if (command.empty())
+      {
+        if (args[argidx].substr(0, 1) == "-")
+          cmd_error(args, argidx, "Unknown option.");
+      }
+      else
+      {
+        command += " ";
+      }
+      command += args[argidx];
+    }
+
+    if (command.empty())
+      log_cmd_error("No optimization pass specified!\n");
+
+    if (!design->full_selection())
+      log_cmd_error("This command only operates on fully selected designs!\n");
+
+    log_header(design, "Executing EQUIV_OPT pass.\n");
+    log_push();
+
+    run_script(design, run_from, run_to);
+
+    log_pop();
+  }
+
+  void script() YS_OVERRIDE
+  {
+    if (check_label("run_pass"))
+    {
+      run("hierarchy -auto-top");
+      run("design -save preopt");
+      if (help_mode)
+        run("[command]");
+      else
+        run(command);
+      run("design -stash postopt");
+    }
+
+    if (check_label("prepare"))
+    {
+      run("design -copy-from preopt  -as gold A:top");
+      run("design -copy-from postopt -as gate A:top");
+    }
+
+    if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)"))
+    {
+      string opts;
+      if (help_mode)
+        opts = " -map <filename> ...";
+      else
+        opts = techmap_opts;
+      run("techmap -D EQUIV -autoproc" + opts);
+    }
+
+    if (check_label("prove"))
+    {
+      run("equiv_make gold gate equiv");
+      run("equiv_induct equiv");
+      if (help_mode)
+        run("equiv_status [-assert] equiv");
+      else if(assert)
+        run("equiv_status -assert equiv");
+      else
+        run("equiv_status equiv");
+    }
+
+    if (check_label("restore"))
+    {
+      run("design -load preopt");
+    }
+  }
+} EquivOptPass;
+
+PRIVATE_NAMESPACE_END

techlibs/ice40/cells_sim.v

@@ -947,6 +947,7 @@ module SB_SPRAM256KA (
 	output reg [15:0] DATAOUT
 );
 `ifndef BLACKBOX
+`ifndef EQUIV
 	reg [15:0] mem [0:16383];
 	wire off = SLEEP || !POWEROFF;
 	integer i;
@@ -973,6 +974,7 @@ module SB_SPRAM256KA (
 		end
 	end
 `endif
+`endif
 endmodule
 
 (* blackbox *)

tests/lut/check_map.ys

@@ -1,13 +1,4 @@
-design -save preopt
-
 simplemap
-techmap -map +/gate2lut.v -D LUT_WIDTH=4
+equiv_opt -assert techmap -map +/gate2lut.v -D LUT_WIDTH=4
+design -load postopt
 select -assert-count 1 t:$lut
-design -stash postopt
-
-design -copy-from preopt -as preopt top
-design -copy-from postopt -as postopt top
-equiv_make preopt postopt equiv
-prep -flatten -top equiv
-equiv_induct
-equiv_status -assert

tests/opt/ice40_carry.v

@@ -1,3 +0,0 @@
-module SB_CARRY (output CO, input I0, I1, CI);
-    assign CO = (I0 && I1) || ((I0 || I1) && CI);
-endmodule

tests/opt/opt_lut.ys

@@ -1,15 +1,4 @@
 read_verilog opt_lut.v
 synth_ice40
 ice40_unlut
-design -save preopt
+equiv_opt -map +/ice40/cells_sim.v -assert opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3
-
-opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3
-design -stash postopt
-
-design -copy-from preopt -as preopt top
-design -copy-from postopt -as postopt top
-equiv_make preopt postopt equiv
-techmap -map ice40_carry.v
-prep -flatten -top equiv
-equiv_induct
-equiv_status -assert