aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
authorMiodrag Milanovic <mmicko@gmail.com>2022-06-21 18:06:16 +0200
committerMiodrag Milanovic <mmicko@gmail.com>2022-06-21 18:07:47 +0200
commit1fdbb42fdd51aa940e4331cdf5b4d1ff56738658 (patch)
treea288871facc3921989dfc71cb53b856c0fc359ce /frontends
parenta30b38910cc49303e4fa3d3c0d7f65647a751cfa (diff)
downloadyosys-1fdbb42fdd51aa940e4331cdf5b4d1ff56738658.tar.gz
yosys-1fdbb42fdd51aa940e4331cdf5b4d1ff56738658.tar.bz2
yosys-1fdbb42fdd51aa940e4331cdf5b4d1ff56738658.zip
Revert "use new verific extensions library"
This reverts commit 607e957657fc56625de5c28ea9cd43c859017d96.
Diffstat (limited to 'frontends')
-rw-r--r--frontends/verific/verific.cc124
1 files changed, 54 insertions, 70 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 5e610c0f3..bbf860c96 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -58,9 +58,6 @@ USING_YOSYS_NAMESPACE
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
#include "InitialAssertions.h"
-#include "VerificBasePass.h"
-#include "TemplateGenerator.h"
-#include "FormalApplication.h"
#endif
#ifndef YOSYSHQ_VERIFIC_API_VERSION
@@ -152,8 +149,6 @@ public:
}
};
-static YosysStreamCallBackHandler stream_cb;
-
// ==================================================================
VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
@@ -2350,64 +2345,6 @@ bool check_noverific_env()
return false;
return true;
}
-
-void set_verific_global_flags()
-{
- static bool g_set_verific_global_flags = true;
-
- if (g_set_verific_global_flags)
- {
- Message::SetConsoleOutput(0);
- Message::RegisterCallBackMsg(msg_func);
-
- RuntimeFlags::SetVar("db_preserve_user_instances", 1);
- RuntimeFlags::SetVar("db_preserve_user_nets", 1);
- RuntimeFlags::SetVar("db_preserve_x", 1);
-
- RuntimeFlags::SetVar("db_allow_external_nets", 1);
- RuntimeFlags::SetVar("db_infer_wide_operators", 1);
- RuntimeFlags::SetVar("db_infer_set_reset_registers", 0);
-
- RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
- RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
- RuntimeFlags::SetVar("veri_allow_any_ram_in_loop", 1);
-
-#ifdef VERIFIC_VHDL_SUPPORT
- RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
- RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
- RuntimeFlags::SetVar("vhdl_allow_any_ram_in_loop", 1);
-
- RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
- RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
-
- RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
- //RuntimeFlags::SetVar("vhdl_preserve_comments", 1);
- RuntimeFlags::SetVar("vhdl_preserve_drivers", 1);
-#endif
- RuntimeFlags::SetVar("veri_preserve_assignments", 1);
- RuntimeFlags::SetVar("veri_preserve_comments", 1);
- RuntimeFlags::SetVar("veri_preserve_drivers", 1);
-
- // Workaround for VIPER #13851
- RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
-
- // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
- Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
-
- // https://github.com/YosysHQ/yosys/issues/1055
- RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
-
- RuntimeFlags::SetVar("verific_produce_verbose_syntax_error_message", 1);
-
-#ifndef DB_PRESERVE_INITIAL_VALUE
-# warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
-#endif
-
- veri_file::RegisterCallBackVerificStream(&stream_cb);
-
- g_set_verific_global_flags = false;
- }
-}
#endif
struct VerificPass : public Pass {
@@ -2612,6 +2549,8 @@ struct VerificPass : public Pass {
#ifdef YOSYS_ENABLE_VERIFIC
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
+ static bool set_verific_global_flags = true;
+
if (check_noverific_env())
log_cmd_error("This version of Yosys is built without Verific support.\n"
"\n"
@@ -2623,7 +2562,56 @@ struct VerificPass : public Pass {
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
- set_verific_global_flags();
+ if (set_verific_global_flags)
+ {
+ Message::SetConsoleOutput(0);
+ Message::RegisterCallBackMsg(msg_func);
+
+ RuntimeFlags::SetVar("db_preserve_user_instances", 1);
+ RuntimeFlags::SetVar("db_preserve_user_nets", 1);
+ RuntimeFlags::SetVar("db_preserve_x", 1);
+
+ RuntimeFlags::SetVar("db_allow_external_nets", 1);
+ RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+ RuntimeFlags::SetVar("db_infer_set_reset_registers", 0);
+
+ RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
+ RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
+ RuntimeFlags::SetVar("veri_allow_any_ram_in_loop", 1);
+
+#ifdef VERIFIC_VHDL_SUPPORT
+ RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
+ RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
+ RuntimeFlags::SetVar("vhdl_allow_any_ram_in_loop", 1);
+
+ RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
+ RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
+
+ RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
+ //RuntimeFlags::SetVar("vhdl_preserve_comments", 1);
+ RuntimeFlags::SetVar("vhdl_preserve_drivers", 1);
+#endif
+ RuntimeFlags::SetVar("veri_preserve_assignments", 1);
+ RuntimeFlags::SetVar("veri_preserve_comments", 1);
+ RuntimeFlags::SetVar("veri_preserve_drivers", 1);
+
+ // Workaround for VIPER #13851
+ RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
+
+ // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
+ Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
+
+ // https://github.com/YosysHQ/yosys/issues/1055
+ RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
+
+ RuntimeFlags::SetVar("verific_produce_verbose_syntax_error_message", 1);
+
+#ifndef DB_PRESERVE_INITIAL_VALUE
+# warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
+#endif
+
+ set_verific_global_flags = false;
+ }
verific_verbose = 0;
verific_sva_fsm_limit = 16;
@@ -2642,6 +2630,8 @@ struct VerificPass : public Pass {
int argidx = 1;
std::string work = "work";
+ YosysStreamCallBackHandler cb;
+ veri_file::RegisterCallBackVerificStream(&cb);
if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
@@ -3218,12 +3208,6 @@ struct VerificPass : public Pass {
#endif
} VerificPass;
-
-#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
-VERIFIC_PASS(VerificTemplateGenerator, "template", "generate template")
-VERIFIC_PASS(VerificFormalApplication, "formal_app", "running formal application")
-#endif
-
struct ReadPass : public Pass {
ReadPass() : Pass("read", "load HDL designs") { }
void help() override