diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index e027103bb..572ed2153 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -115,6 +115,7 @@ struct ChformalPass : public Pass { log("\n"); #endif log(" -assert2assume\n"); + log(" -assert2cover\n"); log(" -assume2assert\n"); log(" -live2fair\n"); log(" -fair2live\n"); @@ -129,6 +130,7 @@ struct ChformalPass : public Pass { void execute(std::vector args, RTLIL::Design *design) override { bool assert2assume = false; + bool assert2cover = false; bool assume2assert = false; bool live2fair = false; bool fair2live = false; @@ -187,6 +189,11 @@ struct ChformalPass : public Pass { mode = 'c'; continue; } + if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2cover") { + assert2cover = true; + mode = 'c'; + continue; + } if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") { assume2assert = true; mode = 'c'; @@ -218,6 +225,10 @@ struct ChformalPass : public Pass { constr_types.insert(ID($cover)); } + if (assert2assume && assert2cover) { + log_cmd_error("Cannot use both -assert2assume and -assert2cover.\n"); + } + if (mode == 0) log_cmd_error("Mode option is missing.\n"); @@ -381,6 +392,8 @@ struct ChformalPass : public Pass { IdString flavor = formal_flavor(cell); if (assert2assume && flavor == ID($assert)) set_formal_flavor(cell, ID($assume)); + if (assert2cover && flavor == ID($assert)) + set_formal_flavor(cell, ID($cover)); else if (assume2assert && flavor == ID($assume)) set_formal_flavor(cell, ID($assert)); else if (live2fair && flavor == ID($live)) diff --git a/tests/various/chformal_check.ys b/tests/various/chformal_check.ys index 951543fa5..2b2d292e4 100644 --- a/tests/various/chformal_check.ys +++ b/tests/various/chformal_check.ys @@ -36,6 +36,12 @@ select -assert-count 1 t:$assert design -load prep +chformal -assert2cover + +select -assert-count 1 t:$check r:FLAVOR=cover %i + +design -load prep + chformal -assert2assume async2sync chformal -lower @@ -66,3 +72,8 @@ design -copy-from gate -as gate top miter -equiv -flatten -make_assert gold gate miter sat -verify -prove-asserts -tempinduct miter + +design -load prep + +logger -expect error "Cannot use both" 1 +chformal -assert2assume -assert2cover diff --git a/tests/verific/chformal.ys b/tests/verific/chformal.ys new file mode 100644 index 000000000..0734f7bb7 --- /dev/null +++ b/tests/verific/chformal.ys @@ -0,0 +1,74 @@ +verific -formal <