From 1fdbb42fdd51aa940e4331cdf5b4d1ff56738658 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 21 Jun 2022 18:06:16 +0200 Subject: Revert "use new verific extensions library" This reverts commit 607e957657fc56625de5c28ea9cd43c859017d96. --- frontends/verific/verific.cc | 124 +++++++++++++++++++------------------------ 1 file changed, 54 insertions(+), 70 deletions(-) (limited to 'frontends/verific') 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 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 -- cgit v1.2.3