From 29e9d3ea9213e4b7238ab25c6014c02893559500 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Tue, 9 Apr 2024 07:16:22 -0700 Subject: [PATCH] Updates for hiding verific --- frontends/verific/verific.cc | 88 +++++++++++++++---------------- tests/verific/case.ys | 8 +-- tests/verific/clocking.ys | 2 +- tests/verific/memory_semantics.ys | 2 +- tests/verific/range_case.ys | 8 +-- tests/verific/rom_case.ys.fail | 4 +- 6 files changed, 56 insertions(+), 56 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 96c2c3645..792e82e26 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -101,7 +101,7 @@ vector verific_incdirs, verific_libdirs, verific_libexts; void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) { - string message_prefix = stringf("ELAB-%s [%s] ", + string message_prefix = stringf("IMPORT-%s [%s] ", msg_type == VERIFIC_NONE ? "NONE" : msg_type == VERIFIC_ERROR ? "ERROR" : msg_type == VERIFIC_WARNING ? "WARNING" : @@ -207,9 +207,9 @@ bool is_blackbox(Netlist *nl) RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj) { - std::string s = stringf("$verific$%s", obj->Name()); + std::string s = stringf("$imp$%s", obj->Name()); if (obj->Linefile()) - s += stringf("$%s:%d", RTLIL::encode_filename(Verific::LineFile::GetFileName(obj->Linefile())).c_str(), Verific::LineFile::GetLineNo(obj->Linefile())); + s += stringf("$%s:%d.%d-%d.%d", RTLIL::encode_filename(LineFile::GetFileName(obj->Linefile())).c_str(), obj->Linefile()->GetLeftLine(), obj->Linefile()->GetLeftCol(), obj->Linefile()->GetRightLine(), obj->Linefile()->GetRightCol()); s += stringf("$%d", autoidx++); return s; } @@ -2678,14 +2678,14 @@ bool check_noverific_env() #endif struct VerificPass : public Pass { - VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } + VerificPass() : Pass("import", "load Verilog/SystemVerilog designs using IMPORT") { } void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} ..\n"); + log(" import {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} ..\n"); log("\n"); - log("Load the specified Verilog/SystemVerilog files into Verific.\n"); + log("Load the specified Verilog/SystemVerilog files into IMPORT.\n"); log("\n"); log("All files specified in one call to this command are one compilation unit.\n"); log("Files passed to different calls to this command are treated as belonging to\n"); @@ -2693,32 +2693,32 @@ struct VerificPass : public Pass { log("\n"); log("Additional -D[=] options may be added after the option indicating\n"); log("the language version (and before file names) to set additional verilog defines.\n"); - log("The macros YOSYS, SYNTHESIS, and VERIFIC are defined implicitly.\n"); + log("The macros YOSYS and SYNTHESIS are defined implicitly.\n"); log("\n"); log("\n"); - log(" verific -formal ..\n"); + log(" import -formal ..\n"); log("\n"); log("Like -sv, but define FORMAL instead of SYNTHESIS.\n"); log("\n"); log("\n"); #ifdef VERIFIC_VHDL_SUPPORT - log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} ..\n"); + log(" import {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} ..\n"); log("\n"); - log("Load the specified VHDL files into Verific.\n"); + log("Load the specified VHDL files into IMPORT.\n"); log("\n"); log("\n"); #endif #ifdef VERIFIC_EDIF_SUPPORT - log(" verific {-edif} ..\n"); + log(" import {-edif} ..\n"); log("\n"); - log("Load the specified EDIF files into Verific.\n"); + log("Load the specified EDIF files into IMPORT.\n"); log("\n"); log("\n"); #endif #ifdef VERIFIC_LIBERTY_SUPPORT - log(" verific {-liberty} ..\n"); + log(" import {-liberty} ..\n"); log("\n"); - log("Load the specified Liberty files into Verific.\n"); + log("Load the specified Liberty files into IMPORT.\n"); log("Default library when -work is not present is one specified in liberty file.\n"); log("To use from SystemVerilog or VHDL use -L to specify liberty library."); log("\n"); @@ -2727,12 +2727,12 @@ struct VerificPass : public Pass { log("\n"); log("\n"); #endif - log(" verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n"); + log(" import {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n"); log(" -sv2012|-sv|-formal] \n"); log("\n"); log("Load and execute the specified command file.\n"); log("Override verilog parsing mode can be set.\n"); - log("The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.\n"); + log("The macros YOSYS and SYNTHESIS/FORMAL are defined implicitly.\n"); log("\n"); log("Command file parser supports following commands in file:\n"); log(" +define+= - defines macro\n"); @@ -2760,48 +2760,48 @@ struct VerificPass : public Pass { log(" -sverilog\n"); log("\n"); log("\n"); - log(" verific [-work ] {-sv|-vhdl|...} \n"); + log(" import [-work ] {-sv|-vhdl|...} \n"); log("\n"); log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n"); log("(default library when -work is not present: \"work\")\n"); log("\n"); log("\n"); - log(" verific [-L ] {-sv|-vhdl|...} \n"); + log(" import [-L ] {-sv|-vhdl|...} \n"); log("\n"); log("Look up external definitions in the specified library.\n"); log("(-L may be used more than once)\n"); log("\n"); log("\n"); - log(" verific -vlog-incdir ..\n"); + log(" import -vlog-incdir ..\n"); log("\n"); log("Add Verilog include directories.\n"); log("\n"); log("\n"); - log(" verific -vlog-libdir ..\n"); + log(" import -vlog-libdir ..\n"); log("\n"); - log("Add Verilog library directories. Verific will search in this directories to\n"); + log("Add Verilog library directories. IMPORT will search in this directories to\n"); log("find undefined modules.\n"); log("\n"); log("\n"); - log(" verific -vlog-libext ..\n"); + log(" import -vlog-libext ..\n"); log("\n"); log("Add Verilog library extensions, used when searching in library directories.\n"); log("\n"); log("\n"); - log(" verific -vlog-define [=]..\n"); + log(" import -vlog-define [=]..\n"); log("\n"); log("Add Verilog defines.\n"); log("\n"); log("\n"); - log(" verific -vlog-undef ..\n"); + log(" import -vlog-undef ..\n"); log("\n"); log("Remove Verilog defines previously set with -vlog-define.\n"); log("\n"); log("\n"); - log(" verific -set-error ..\n"); - log(" verific -set-warning ..\n"); - log(" verific -set-info ..\n"); - log(" verific -set-ignore ..\n"); + log(" import -set-error ..\n"); + log(" import -set-warning ..\n"); + log(" import -set-info ..\n"); + log(" import -set-ignore ..\n"); log("\n"); log("Set message severity. is the string in square brackets when a message\n"); log("is printed, such as VERI-1209.\n"); @@ -2809,10 +2809,10 @@ struct VerificPass : public Pass { log("all messages of certain type.\n"); log("\n"); log("\n"); - log(" verific -import [options] ..\n"); + log(" import -import [options] ..\n"); log("\n"); log("Elaborate the design for the specified top modules or configurations, import to\n"); - log("Yosys and reset the internal state of Verific.\n"); + log("Yosys and reset the internal state of IMPORT.\n"); log("\n"); log("Import options:\n"); log("\n"); @@ -2824,7 +2824,7 @@ struct VerificPass : public Pass { log(" Create a gate-level netlist.\n"); log("\n"); log(" -flatten\n"); - log(" Flatten the design in Verific before importing.\n"); + log(" Flatten the design in IMPORT before importing.\n"); log("\n"); log(" -extnets\n"); log(" Resolve references to external nets by adding module ports as needed.\n"); @@ -2839,13 +2839,13 @@ struct VerificPass : public Pass { log(" Keep all register initializations, even those for non-FF registers.\n"); log("\n"); log(" -cells\n"); - log(" Import all cell definitions from Verific loaded libraries even if they are\n"); + log(" Import all cell definitions from IMPORT loaded libraries even if they are\n"); log(" unused in design. Useful with \"-edif\" and \"-liberty\" option.\n"); log("\n"); log(" -chparam name value \n"); log(" Elaborate the specified top modules (all modules when -all given) using\n"); log(" this parameter value. Modules on which this parameter does not exist will\n"); - log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n"); + log(" cause IMPORT to produce a VERI-1928 or VHDL-1676 message. This option\n"); log(" can be specified multiple times to override multiple parameters.\n"); log(" String values must be passed in double quotes (\").\n"); log("\n"); @@ -2855,17 +2855,17 @@ struct VerificPass : public Pass { log(" -pp \n"); log(" Pretty print design after elaboration to specified file.\n"); log("\n"); - log("The following additional import options are useful for debugging the Verific\n"); - log("bindings (for Yosys and/or Verific developers):\n"); + log("The following additional import options are useful for debugging the IMPORT\n"); + log("bindings (for Yosys and/or IMPORT developers):\n"); log("\n"); log(" -k\n"); - log(" Keep going after an unsupported verific primitive is found. The\n"); + log(" Keep going after an unsupported IMPORT primitive is found. The\n"); log(" unsupported primitive is added as blockbox module to the design.\n"); log(" This will also add all SVA related cells to the design parallel to\n"); log(" the checker logic inferred by it.\n"); log("\n"); log(" -V\n"); - log(" Import Verific netlist as-is without translating to Yosys cell types. \n"); + log(" Import IMPORT netlist as-is without translating to Yosys cell types. \n"); log("\n"); log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); @@ -2874,14 +2874,14 @@ struct VerificPass : public Pass { log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n"); log("\n"); log(" -n\n"); - log(" Keep all Verific names on instances and nets. By default only\n"); + log(" Keep all IMPORT names on instances and nets. By default only\n"); log(" user-declared names are preserved.\n"); log("\n"); log(" -d \n"); - log(" Dump the Verific netlist as a verilog file.\n"); + log(" Dump the IMPORT netlist as a verilog file.\n"); log("\n"); log("\n"); - log(" verific [-work ] -pp [options] []..\n"); + log(" import [-work ] -pp [options] []..\n"); log("\n"); log("Pretty print design (or just module) to the specified file from the\n"); log("specified library. (default library when -work is not present: \"work\")\n"); @@ -2895,9 +2895,9 @@ struct VerificPass : public Pass { log(" Save output for VHDL design units.\n"); log("\n"); log("\n"); - log(" verific -cfg [ []]\n"); + log(" import -cfg [ []]\n"); log("\n"); - log("Get/set Verific runtime flags.\n"); + log("Get/set IMPORT runtime flags.\n"); log("\n"); log("\n"); #if defined(YOSYS_ENABLE_VERIFIC) and defined(YOSYSHQ_VERIFIC_EXTENSIONS) @@ -3044,7 +3044,7 @@ struct VerificPass : public Pass { "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"); + log_header(design, "Executing IMPORT (loading SystemVerilog and VHDL designs using IMPORT).\n"); if (set_verific_global_flags) { @@ -3114,7 +3114,7 @@ struct VerificPass : public Pass { for (char *p = release_tmstr; *p; p++) if (*p == '\n') *p = 0; - log("Built with Verific %s, released at %s.\n", release_str, release_tmstr); + log("Built with IMPORT %s, released at %s.\n", release_str, release_tmstr); int argidx = 1; std::string work = "work"; diff --git a/tests/verific/case.ys b/tests/verific/case.ys index a181b39cf..df28476d6 100644 --- a/tests/verific/case.ys +++ b/tests/verific/case.ys @@ -1,12 +1,12 @@ -verific -cfg db_abstract_case_statement_synthesis 0 +import -cfg db_abstract_case_statement_synthesis 0 read -sv case.sv -verific -import top +import -import top prep rename top gold -verific -cfg db_abstract_case_statement_synthesis 1 +import -cfg db_abstract_case_statement_synthesis 1 read -sv case.sv -verific -import top +import -import top prep rename top gate diff --git a/tests/verific/clocking.ys b/tests/verific/clocking.ys index bfdbeb748..6bf7420a5 100644 --- a/tests/verific/clocking.ys +++ b/tests/verific/clocking.ys @@ -4,7 +4,7 @@ always @(*) assert(foo); endmodule EOT -verific -import test +import -import test prep select -assert-count 1 t:$assert diff --git a/tests/verific/memory_semantics.ys b/tests/verific/memory_semantics.ys index 7287f847f..9e61ba841 100644 --- a/tests/verific/memory_semantics.ys +++ b/tests/verific/memory_semantics.ys @@ -1,4 +1,4 @@ -verific -sv <