mirror of https://github.com/YosysHQ/yosys.git
Revert "use new verific extensions library"
This reverts commit 607e957657
.
This commit is contained in:
parent
a30b38910c
commit
1fdbb42fdd
|
@ -58,9 +58,6 @@ USING_YOSYS_NAMESPACE
|
||||||
|
|
||||||
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
|
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
|
||||||
#include "InitialAssertions.h"
|
#include "InitialAssertions.h"
|
||||||
#include "VerificBasePass.h"
|
|
||||||
#include "TemplateGenerator.h"
|
|
||||||
#include "FormalApplication.h"
|
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
#ifndef YOSYSHQ_VERIFIC_API_VERSION
|
#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) :
|
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 false;
|
||||||
return true;
|
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
|
#endif
|
||||||
|
|
||||||
struct VerificPass : public Pass {
|
struct VerificPass : public Pass {
|
||||||
|
@ -2612,6 +2549,8 @@ struct VerificPass : public Pass {
|
||||||
#ifdef YOSYS_ENABLE_VERIFIC
|
#ifdef YOSYS_ENABLE_VERIFIC
|
||||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||||
{
|
{
|
||||||
|
static bool set_verific_global_flags = true;
|
||||||
|
|
||||||
if (check_noverific_env())
|
if (check_noverific_env())
|
||||||
log_cmd_error("This version of Yosys is built without Verific support.\n"
|
log_cmd_error("This version of Yosys is built without Verific support.\n"
|
||||||
"\n"
|
"\n"
|
||||||
|
@ -2623,7 +2562,56 @@ struct VerificPass : public Pass {
|
||||||
|
|
||||||
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
|
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_verbose = 0;
|
||||||
verific_sva_fsm_limit = 16;
|
verific_sva_fsm_limit = 16;
|
||||||
|
@ -2642,6 +2630,8 @@ struct VerificPass : public Pass {
|
||||||
|
|
||||||
int argidx = 1;
|
int argidx = 1;
|
||||||
std::string work = "work";
|
std::string work = "work";
|
||||||
|
YosysStreamCallBackHandler cb;
|
||||||
|
veri_file::RegisterCallBackVerificStream(&cb);
|
||||||
|
|
||||||
if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
|
if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
|
||||||
args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
|
args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
|
||||||
|
@ -3218,12 +3208,6 @@ struct VerificPass : public Pass {
|
||||||
#endif
|
#endif
|
||||||
} VerificPass;
|
} VerificPass;
|
||||||
|
|
||||||
|
|
||||||
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
|
|
||||||
VERIFIC_PASS(VerificTemplateGenerator, "template", "generate template")
|
|
||||||
VERIFIC_PASS(VerificFormalApplication, "formal_app", "running formal application")
|
|
||||||
#endif
|
|
||||||
|
|
||||||
struct ReadPass : public Pass {
|
struct ReadPass : public Pass {
|
||||||
ReadPass() : Pass("read", "load HDL designs") { }
|
ReadPass() : Pass("read", "load HDL designs") { }
|
||||||
void help() override
|
void help() override
|
||||||
|
|
Loading…
Reference in New Issue