blif: Use library cells' start_offset and upto for wideports.

[yosys.git] / frontends / verific / verific.cc

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index e236aaaf2f34faba3f21e3c3160b55571f69d9f5..7aa3ebcbb8113063b15aa75089a3550b62fbbe78 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -49,14 +49,17 @@ USING_YOSYS_NAMESPACE
 #include "VeriWrite.h"
 #include "VhdlUnits.h"
 #include "VeriLibrary.h"
+
+#if defined(YOSYSHQ_VERIFIC_INITSTATE) || defined(YOSYSHQ_VERIFIC_TEMPLATES) || defined(YOSYSHQ_VERIFIC_FORMALAPPS)
 #include "VeriExtensions.h"
+#endif
 
-#ifndef SYMBIOTIC_VERIFIC_API_VERSION
-#  error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
+#ifndef YOSYSHQ_VERIFIC_API_VERSION
+#  error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
 #endif
 
-#if SYMBIOTIC_VERIFIC_API_VERSION < 20200902
-#  error "Please update your version of Symbiotic EDA flavored Verific."
+#if YOSYSHQ_VERIFIC_API_VERSION < 20210103
+#  error "Please update your version of YosysHQ flavored Verific."
 #endif
 
 #ifdef __clang__
@@ -1471,7 +1474,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
                                continue;
                }
 
-               if (inst->Type() == PRIM_SEDA_INITSTATE)
+#ifdef YOSYSHQ_VERIFIC_INITSTATE
+               if (inst->Type() == PRIM_YOSYSHQ_INITSTATE)
                {
                        SigBit initstate = module->Initstate(new_verific_id(inst));
                        SigBit sig_o = net_map_at(inst->GetOutput());
@@ -1480,7 +1484,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
                        if (!mode_keep)
                                continue;
                }
-
+#endif
                if (!mode_keep && verific_sva_prims.count(inst->Type())) {
                        if (verific_verbose)
                                log("    skipping SVA cell in non k-mode\n");
@@ -1958,9 +1962,10 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
        for (const auto &i : parameters)
                verific_params.Insert(i.first.c_str(), i.second.c_str());
 
+#ifdef YOSYSHQ_VERIFIC_INITSTATE
        InitialAssertionRewriter rw;
        rw.RegisterCallBack();
-
+#endif
        if (top.empty()) {
                netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
        }
@@ -2199,7 +2204,7 @@ struct VerificPass : public Pass {
                log("\n");
                log("    verific -app <application>..\n");
                log("\n");
-               log("Execute SEDA formal application on loaded Verilog files.\n");
+               log("Execute YosysHQ formal application on loaded Verilog files.\n");
                log("\n");
                log("Application options:\n");
                log("\n");
@@ -2217,7 +2222,7 @@ struct VerificPass : public Pass {
                log("\n");
                log("Applications:\n");
                log("\n");
-#ifdef YOSYS_ENABLE_VERIFIC
+#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS)
                VerificFormalApplications vfa;
                log("%s\n",vfa.GetHelp().c_str());
 #else
@@ -2243,18 +2248,18 @@ struct VerificPass : public Pass {
                log("\n");
                log("Templates:\n");
                log("\n");
-#ifdef YOSYS_ENABLE_VERIFIC
+#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES)
                VerificTemplateGenerator vfg;
                log("%s\n",vfg.GetHelp().c_str());
 #else
                log("  WARNING: Templates only available in commercial build.\n");
                log("\n");
 #endif
-               log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
-               log("https://www.symbioticeda.com/seda-suite\n");
+               log("Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n");
+               log("https://www.yosyshq.com/\n");
                log("\n");
-               log("Contact office@symbioticeda.com for free evaluation\n");
-               log("binaries of Symbiotic EDA Suite.\n");
+               log("Contact office@yosyshq.com for free evaluation\n");
+               log("binaries of YosysHQ Tabby CAD Suite.\n");
                log("\n");
        }
 #ifdef YOSYS_ENABLE_VERIFIC
@@ -2265,11 +2270,11 @@ struct VerificPass : public Pass {
                if (check_noverific_env())
                        log_cmd_error("This version of Yosys is built without Verific support.\n"
                                        "\n"
-                                       "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
-                                       "https://www.symbioticeda.com/seda-suite\n"
+                                       "Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"
+                                       "https://www.yosyshq.com/\n"
                                        "\n"
-                                       "Contact office@symbioticeda.com for free evaluation\n"
-                                       "binaries of Symbiotic EDA Suite.\n");
+                                       "Contact office@yosyshq.com for free evaluation\n"
+                                       "binaries of YosysHQ Tabby CAD Suite.\n");
 
                log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
 
@@ -2494,6 +2499,7 @@ struct VerificPass : public Pass {
                        goto check_error;
                }
 
+#ifdef YOSYSHQ_VERIFIC_FORMALAPPS
                if (argidx < GetSize(args) && args[argidx] == "-app")
                {
                        if (!(argidx+1 < GetSize(args)))
@@ -2587,7 +2593,7 @@ struct VerificPass : public Pass {
                        }
                        goto check_error;
                }
-
+#endif
                if (argidx < GetSize(args) && args[argidx] == "-pp")
                {
                        const char* filename = nullptr;
@@ -2630,6 +2636,7 @@ struct VerificPass : public Pass {
                        goto check_error;
                }
 
+#ifdef YOSYSHQ_VERIFIC_TEMPLATES
                if (argidx < GetSize(args) && args[argidx] == "-template")
                {
                        if (!(argidx+1 < GetSize(args)))
@@ -2713,7 +2720,7 @@ struct VerificPass : public Pass {
                                fclose(of);
                        goto check_error;
                }
-
+#endif
                if (GetSize(args) > argidx && args[argidx] == "-import")
                {
                        std::set<Netlist*> nl_todo, nl_done;
@@ -2798,9 +2805,10 @@ struct VerificPass : public Pass {
 
                        std::set<std::string> top_mod_names;
 
+#ifdef YOSYSHQ_VERIFIC_INITSTATE
                        InitialAssertionRewriter rw;
                        rw.RegisterCallBack();
-
+#endif
                        if (mode_all)
                        {
                                log("Running hier_tree::ElaborateAll().\n");
@@ -2926,11 +2934,11 @@ struct VerificPass : public Pass {
        void execute(std::vector<std::string>, RTLIL::Design *) override {
                log_cmd_error("This version of Yosys is built without Verific support.\n"
                                "\n"
-                               "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
-                               "https://www.symbioticeda.com/seda-suite\n"
+                               "Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"
+                               "https://www.yosyshq.com/\n"
                                "\n"
-                               "Contact office@symbioticeda.com for free evaluation\n"
-                               "binaries of Symbiotic EDA Suite.\n");
+                               "Contact office@yosyshq.com for free evaluation\n"
+                               "binaries of YosysHQ Tabby CAD Suite.\n");
        }
 #endif
 } VerificPass;