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

equiv_opt: new command, for verifying optimization passes.

This commit is contained in:
whitequark 2018-12-06 14:28:20 +00:00
parent 1bb728e24f
commit c38ea9ae65
4 changed files with 169 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
passes/equiv/Makefile.inc
View File

@ -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

165
passes/equiv/equiv_opt.cc Normal file
View File

@ -0,0 +1,165 @@
/*
* 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)"))
{
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;
PRIVATE_NAMESPACE_END

13
tests/lut/check_map.ys
View File

@ -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

13
tests/opt/opt_lut.ys
View File

@ -1,15 +1,4 @@
read_verilog opt_lut.v
synth_ice40
ice40_unlut
design -save preopt
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
equiv_opt -map ice40_carry.v -assert opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3