riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Fix equiv_opt indenting 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-12-16 15:57:28 +01:00
parent 2a681909df
commit f53e19cc71
1 changed files with 113 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

236
passes/equiv/equiv_opt.cc
View File

@ -22,146 +22,136 @@
USING_YOSYS_NAMESPACE USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN PRIVATE_NAMESPACE_BEGIN
struct EquivOptPass : public ScriptPass struct EquivOptPass:public ScriptPass
{ {
EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { } EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { }
void help() YS_OVERRIDE void help() YS_OVERRIDE
{ {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n"); log("\n");
log(" equiv_opt [options] [command]\n"); log(" equiv_opt [options] [command]\n");
log("\n"); log("\n");
log("This command checks circuit equivalence before and after an optimization pass.\n"); log("This command checks circuit equivalence before and after an optimization pass.\n");
log("\n"); log("\n");
log(" -run <from_label>:<to_label>\n"); log(" -run <from_label>:<to_label>\n");
log(" only run the commands between the labels (see below). an empty\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(" 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(" label is synonymous to the end of the command list.\n");
log("\n"); log("\n");
log(" -map <filename>\n"); log(" -map <filename>\n");
log(" expand the modules in this file before proving equivalence. this is\n"); log(" expand the modules in this file before proving equivalence. this is\n");
log(" useful for handling architecture-specific primitives.\n"); log(" useful for handling architecture-specific primitives.\n");
log("\n"); log("\n");
log(" -assert\n"); log(" -assert\n");
log(" produce an error if the circuits are not equivalent\n"); log(" produce an error if the circuits are not equivalent\n");
log("\n"); log("\n");
log("The following commands are executed by this verification command:\n"); log("The following commands are executed by this verification command:\n");
help_script(); help_script();
log("\n"); log("\n");
} }
std::string command, techmap_opts; std::string command, techmap_opts;
bool assert; bool assert;
void clear_flags() YS_OVERRIDE void clear_flags() YS_OVERRIDE
{ {
command = ""; command = "";
techmap_opts = ""; techmap_opts = "";
assert = false; assert = false;
} }
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
{ {
string run_from, run_to; string run_from, run_to;
clear_flags(); clear_flags();
size_t argidx; size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) for (argidx = 1; argidx < args.size(); argidx++) {
{ if (args[argidx] == "-run" && argidx + 1 < args.size()) {
if (args[argidx] == "-run" && argidx+1 < args.size()) { size_t pos = args[argidx + 1].find(':');
size_t pos = args[argidx+1].find(':'); if (pos == std::string::npos)
if (pos == std::string::npos) break;
break; run_from = args[++argidx].substr(0, pos);
run_from = args[++argidx].substr(0, pos); run_to = args[argidx].substr(pos + 1);
run_to = args[argidx].substr(pos+1); continue;
continue; }
} if (args[argidx] == "-map" && argidx + 1 < args.size()) {
if (args[argidx] == "-map" && argidx+1 < args.size()) { techmap_opts += " -map " + args[++argidx];
techmap_opts += " -map " + args[++argidx]; continue;
continue; }
} if (args[argidx] == "-assert") {
if (args[argidx] == "-assert") { assert = true;
assert = true; continue;
continue; }
} break;
break; }
}
for (; argidx < args.size(); argidx++) for (; argidx < args.size(); argidx++) {
{ if (command.empty()) {
if (command.empty()) if (args[argidx].substr(0, 1) == "-")
{ cmd_error(args, argidx, "Unknown option.");
if (args[argidx].substr(0, 1) == "-") } else {
cmd_error(args, argidx, "Unknown option."); command += " ";
} }
else command += args[argidx];
{ }
command += " ";
}
command += args[argidx];
}
if (command.empty()) if (command.empty())
log_cmd_error("No optimization pass specified!\n"); log_cmd_error("No optimization pass specified!\n");
if (!design->full_selection()) if (!design->full_selection())
log_cmd_error("This command only operates on fully selected designs!\n"); log_cmd_error("This command only operates on fully selected designs!\n");
log_header(design, "Executing EQUIV_OPT pass.\n"); log_header(design, "Executing EQUIV_OPT pass.\n");
log_push(); log_push();
run_script(design, run_from, run_to); run_script(design, run_from, run_to);
log_pop(); log_pop();
} }
void script() YS_OVERRIDE void script() YS_OVERRIDE
{ {
if (check_label("run_pass")) if (check_label("run_pass")) {
{ run("hierarchy -auto-top");
run("hierarchy -auto-top"); run("design -save preopt");
run("design -save preopt"); if (help_mode)
if (help_mode) run("[command]");
run("[command]"); else
else run(command);
run(command); run("design -stash postopt");
run("design -stash postopt"); }
}
if (check_label("prepare")) if (check_label("prepare")) {
{ run("design -copy-from preopt -as gold A:top");
run("design -copy-from preopt -as gold A:top"); run("design -copy-from postopt -as gate A:top");
run("design -copy-from postopt -as gate A:top"); }
}
if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)")) if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)")) {
{ string opts;
string opts; if (help_mode)
if (help_mode) opts = " -map <filename> ...";
opts = " -map <filename> ..."; else
else opts = techmap_opts;
opts = techmap_opts; run("techmap -D EQUIV -autoproc" + opts);
run("techmap -D EQUIV -autoproc" + opts); }
}
if (check_label("prove")) if (check_label("prove")) {
{ run("equiv_make gold gate equiv");
run("equiv_make gold gate equiv"); run("equiv_induct equiv");
run("equiv_induct equiv"); if (help_mode)
if (help_mode) run("equiv_status [-assert] equiv");
run("equiv_status [-assert] equiv"); else if (assert)
else if(assert) run("equiv_status -assert equiv");
run("equiv_status -assert equiv"); else
else run("equiv_status equiv");
run("equiv_status equiv"); }
}
if (check_label("restore")) if (check_label("restore")) {
{ run("design -load preopt");
run("design -load preopt"); }
} }
}
} EquivOptPass; } EquivOptPass;
PRIVATE_NAMESPACE_END PRIVATE_NAMESPACE_END