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

Add "chformal -assert2assume" and friends

This commit is contained in:
Clifford Wolf 2017-02-27 23:59:59 +01:00
parent db7fc0e32d
commit 1a6c02a532
1 changed files with 44 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
passes/cmds/chformal.cc
View File

@ -55,9 +55,20 @@ struct ChformalPass : public Pass {
log(" -skip <N>\n");
log(" ignore activation of the constraint in the first <N> clock cycles\n");
log("\n");
log(" -assert2assume\n");
log(" -assume2assert\n");
log(" -live2fair\n");
log(" -fair2live\n");
log(" change the roles of cells as indicated. this options can be combined\n");
log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
bool assert2assume = false;
bool assume2assert = false;
bool live2fair = false;
bool fair2live = false;
pool<IdString> constr_types;
char mode = 0;
int mode_arg;
@ -103,6 +114,26 @@ struct ChformalPass : public Pass {
mode_arg = atoi(args[++argidx].c_str());
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
assert2assume = true;
mode = 'c';
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") {
assume2assert = true;
mode = 'c';
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-live2fair") {
live2fair = true;
mode = 'c';
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-fair2live") {
fair2live = true;
mode = 'c';
continue;
}
break;
}
extra_args(args, argidx, design);
@ -231,6 +262,19 @@ struct ChformalPass : public Pass {
for (auto cell : constr_cells)
cell->setPort("\\EN", module->LogicAnd(NEW_ID, en, cell->getPort("\\EN")));
}
else
if (mode == 'c')
{
for (auto cell : constr_cells)
if (assert2assume && cell->type == "$assert")
cell->type = "$assume";
else if (assume2assert && cell->type == "$assume")
cell->type = "$assert";
else if (live2fair && cell->type == "$live")
cell->type = "$fair";
else if (fair2live && cell->type == "$fair")
cell->type = "$live";
}
}
}
} ChformalPass;