Add "verific -autocover"
authorClifford Wolf <clifford@clifford.at>
Fri, 6 Apr 2018 12:10:57 +0000 (14:10 +0200)
committerClifford Wolf <clifford@clifford.at>
Fri, 6 Apr 2018 12:10:57 +0000 (14:10 +0200)
Signed-off-by: Clifford Wolf <clifford@clifford.at>
frontends/verific/verific.cc
frontends/verific/verific.h

index c72f513cbf22f2e5d52d7bed176dd916e1c23154..d68b81c8b1c705595c354abfcbb6e538733eb1c2 100644 (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);
index 9e3e39695b8bbebcddf3ea790d15f5c3e1d790c8..2dd688e0d20af582d63774e1e9e565ccc7256c22 100644 (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);