mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

chformal: Add -assert2cover option

Browse source 
Also add to chformal tests.
This commit is contained in:
Krystine Sherwin 2025-06-14 10:54:06 +12:00
parent 67f8de54dc
commit 45131f4425
No known key found for this signature in database
2 changed files with 24 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
passes/cmds/chformal.cc
View file

@ -115,6 +115,7 @@ struct ChformalPass : public Pass {
log("\n"); log("\n");
#endif #endif
log(" -assert2assume\n"); log(" -assert2assume\n");
log(" -assert2cover\n");
log(" -assume2assert\n"); log(" -assume2assert\n");
log(" -live2fair\n"); log(" -live2fair\n");
log(" -fair2live\n"); log(" -fair2live\n");
@ -129,6 +130,7 @@ struct ChformalPass : public Pass {
void execute(std::vector<std::string> args, RTLIL::Design *design) override void execute(std::vector<std::string> args, RTLIL::Design *design) override
{ {
bool assert2assume = false; bool assert2assume = false;
bool assert2cover = false;
bool assume2assert = false; bool assume2assert = false;
bool live2fair = false; bool live2fair = false;
bool fair2live = false; bool fair2live = false;
@ -187,6 +189,11 @@ struct ChformalPass : public Pass {
mode = 'c'; mode = 'c';
continue; continue;
} }
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2cover") {
assert2cover = true;
mode = 'c';
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") { if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") {
assume2assert = true; assume2assert = true;
mode = 'c'; mode = 'c';
@ -218,6 +225,10 @@ struct ChformalPass : public Pass {
constr_types.insert(ID($cover)); constr_types.insert(ID($cover));
} }
if (assert2assume && assert2cover) {
log_cmd_error("Cannot use both -assert2assume and -assert2cover.\n");
}
if (mode == 0) if (mode == 0)
log_cmd_error("Mode option is missing.\n"); log_cmd_error("Mode option is missing.\n");
@ -381,6 +392,8 @@ struct ChformalPass : public Pass {
IdString flavor = formal_flavor(cell); IdString flavor = formal_flavor(cell);
if (assert2assume && flavor == ID($assert)) if (assert2assume && flavor == ID($assert))
set_formal_flavor(cell, ID($assume)); set_formal_flavor(cell, ID($assume));
if (assert2cover && flavor == ID($assert))
set_formal_flavor(cell, ID($cover));
else if (assume2assert && flavor == ID($assume)) else if (assume2assert && flavor == ID($assume))
set_formal_flavor(cell, ID($assert)); set_formal_flavor(cell, ID($assert));
else if (live2fair && flavor == ID($live)) else if (live2fair && flavor == ID($live))

11
tests/various/chformal_check.ys
View file

@ -36,6 +36,12 @@ select -assert-count 1 t:$assert
design -load prep design -load prep
chformal -assert2cover
select -assert-count 1 t:$check r:FLAVOR=cover %i
design -load prep
chformal -assert2assume chformal -assert2assume
async2sync async2sync
chformal -lower chformal -lower
@ -66,3 +72,8 @@ design -copy-from gate -as gate top
miter -equiv -flatten -make_assert gold gate miter miter -equiv -flatten -make_assert gold gate miter
sat -verify -prove-asserts -tempinduct miter sat -verify -prove-asserts -tempinduct miter
design -load prep
logger -expect error "Cannot use both" 1
chformal -assert2assume -assert2cover