Add "verific -autocover"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-04-06 14:10:57 +02:00
parent f10e0e15c5
commit ab8db2c168
2 changed files with 17 additions and 5 deletions

View File

@ -99,9 +99,9 @@ string get_full_netlist_name(Netlist *nl)
// ==================================================================
VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific) :
VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover) :
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
mode_names(mode_names), mode_verific(mode_verific)
mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover)
{
}
@ -1279,8 +1279,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (!mode_nosva)
{
for (auto inst : sva_asserts)
for (auto inst : sva_asserts) {
if (mode_autocover)
verific_import_sva_cover(this, inst);
verific_import_sva_assert(this, inst);
}
for (auto inst : sva_assumes)
verific_import_sva_assume(this, inst);
@ -1594,6 +1597,9 @@ struct VerificPass : public Pass {
log(" -extnets\n");
log(" Resolve references to external nets by adding module ports as needed.\n");
log("\n");
log(" -autocover\n");
log(" Generate automatic cover statements for all asserts\n");
log("\n");
log(" -v, -vv\n");
log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
log("\n");
@ -1746,6 +1752,7 @@ struct VerificPass : public Pass {
std::set<Netlist*> nl_todo, nl_done;
bool mode_all = false, mode_gates = false, mode_keep = false;
bool mode_nosva = false, mode_names = false, mode_verific = false;
bool mode_autocover = false;
bool flatten = false, extnets = false;
string dumpfile;
@ -1778,6 +1785,10 @@ struct VerificPass : public Pass {
mode_names = true;
continue;
}
if (args[argidx] == "-autocover") {
mode_autocover = true;
continue;
}
if (args[argidx] == "-V") {
mode_verific = true;
continue;
@ -1930,7 +1941,7 @@ struct VerificPass : public Pass {
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
VerificImporter importer(mode_gates, mode_keep, mode_nosva,
mode_names, mode_verific);
mode_names, mode_verific, mode_autocover);
importer.import_netlist(design, nl, nl_todo);
}
nl_todo.erase(nl);

View File

@ -67,8 +67,9 @@ struct VerificImporter
std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
bool mode_autocover;
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific);
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover);
RTLIL::SigBit net_map_at(Verific::Net *net);