text: /*
   *  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("    -multiclock\n");
  		log("        run clk2fflogic before equivalence checking.\n");
  		log("\n");
  		log("    -undef\n");
  		log("        enable modelling of undef states during equiv_induct.\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, undef, multiclock;
  
  	void clear_flags() YS_OVERRIDE
  	{
  		command = "";
  		techmap_opts = "";
  		assert = false;
  		undef = false;
  		multiclock = 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;
  			}
  			if (args[argidx] == "-undef") {
  				undef = true;
  				continue;
  			}
  			if (args[argidx] == "-multiclock") {
  				multiclock = true;
  				continue;
  			}
  			break;
  		}
  
  		for (; argidx < args.size(); argidx++) {
  			if (command.empty()) {
  				if (args[argidx].compare(0, 1, "-") == 0)
  					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 -wb -D EQUIV -autoproc" + opts);
  		}
  
  		if (check_label("prove")) {
  			if (multiclock || help_mode)
  				run("clk2fflogic", "(only with -multiclock)");
  			run("equiv_make gold gate equiv");
  			if (help_mode)
  				run("equiv_induct [-undef] equiv");
  			else if (undef)
  				run("equiv_induct -undef equiv");
  			else
  				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
  