aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2018-04-06 14:10:57 +0200
committerClifford Wolf <clifford@clifford.at>2018-04-06 14:10:57 +0200
commitab8db2c168ed2177146ec744f6397a3a9951d7cc (patch)
tree62d33c6be6e803e217baf5e88b8b3cdab0d90191 /frontends
parentf10e0e15c5c2c01c1b5ff3c244679e4842415b79 (diff)
downloadyosys-ab8db2c168ed2177146ec744f6397a3a9951d7cc.tar.gz
yosys-ab8db2c168ed2177146ec744f6397a3a9951d7cc.tar.bz2
yosys-ab8db2c168ed2177146ec744f6397a3a9951d7cc.zip
Add "verific -autocover"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends')
-rw-r--r--frontends/verific/verific.cc19
-rw-r--r--frontends/verific/verific.h3
2 files changed, 17 insertions, 5 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index c72f513cb..d68b81c8b 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -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);
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 9e3e39695..2dd688e0d 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -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);