USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-struct EquivOptPass : public ScriptPass
+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)"))
- {
- if (help_mode)
- run("techmap -autoproc -map <filename> ...");
- else
- run("techmap -autoproc" + techmap_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() : 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 uses temporal induction to check circuit equivalence before and\n");
+ log("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(" -async2sync\n");
+ log(" run async2sync 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, async2sync;
+
+ void clear_flags() YS_OVERRIDE
+ {
+ command = "";
+ techmap_opts = "";
+ assert = false;
+ undef = false;
+ multiclock = false;
+ async2sync = 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;
+ }
+ if (args[argidx] == "-async2sync") {
+ async2sync = 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");
+
+ if (async2sync && multiclock)
+ log_cmd_error("The '-async2sync' and '-multiclock' options are mutually exclusive!\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)");
+ if (async2sync || help_mode)
+ run("async2sync", " (only with -async2sync)");
+ 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
projects / yosys.git / blobdiff