mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-22 16:45:32 +00:00
Code Activity

Updates for hiding verific

Browse source
This commit is contained in:
Akash Levy 2024-04-09 07:16:22 -07:00
parent 0fa8098ff4
commit 29e9d3ea92
6 changed files with 56 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

88
frontends/verific/verific.cc
View file

@ -101,7 +101,7 @@ vector<string> 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} <verilog-file>..\n");
log(" import {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\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<macro>[=<value>] 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 <verilog-file>..\n");
log(" import -formal <verilog-file>..\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} <vhdl-file>..\n");
log(" import {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\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} <edif-file>..\n");
log(" import {-edif} <edif-file>..\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} <liberty-file>..\n");
log(" import {-liberty} <liberty-file>..\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] <command-file>\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+<MACRO>=<VALUE> - defines macro\n");
@ -2760,48 +2760,48 @@ struct VerificPass : public Pass {
log(" -sverilog\n");
log("\n");
log("\n");
log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n");
log(" import [-work <libname>] {-sv|-vhdl|...} <hdl-file>\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 <libname>] {-sv|-vhdl|...} <hdl-file>\n");
log(" import [-L <libname>] {-sv|-vhdl|...} <hdl-file>\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 <directory>..\n");
log(" import -vlog-incdir <directory>..\n");
log("\n");
log("Add Verilog include directories.\n");
log("\n");
log("\n");
log(" verific -vlog-libdir <directory>..\n");
log(" import -vlog-libdir <directory>..\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 <extension>..\n");
log(" import -vlog-libext <extension>..\n");
log("\n");
log("Add Verilog library extensions, used when searching in library directories.\n");
log("\n");
log("\n");
log(" verific -vlog-define <macro>[=<value>]..\n");
log(" import -vlog-define <macro>[=<value>]..\n");
log("\n");
log("Add Verilog defines.\n");
log("\n");
log("\n");
log(" verific -vlog-undef <macro>..\n");
log(" import -vlog-undef <macro>..\n");
log("\n");
log("Remove Verilog defines previously set with -vlog-define.\n");
log("\n");
log("\n");
log(" verific -set-error <msg_id>..\n");
log(" verific -set-warning <msg_id>..\n");
log(" verific -set-info <msg_id>..\n");
log(" verific -set-ignore <msg_id>..\n");
log(" import -set-error <msg_id>..\n");
log(" import -set-warning <msg_id>..\n");
log(" import -set-info <msg_id>..\n");
log(" import -set-ignore <msg_id>..\n");
log("\n");
log("Set message severity. <msg_id> 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] <top>..\n");
log(" import -import [options] <top>..\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 <filename>\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 <dump_file>\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 <libname>] -pp [options] <filename> [<module>]..\n");
log(" import [-work <libname>] -pp [options] <filename> [<module>]..\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 [<name> [<value>]]\n");
log(" import -cfg [<name> [<value>]]\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";

8
tests/verific/case.ys
View file

@ -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

2
tests/verific/clocking.ys
View file

@ -4,7 +4,7 @@ always @(*) assert(foo);
endmodule
EOT
verific -import test
import -import test
prep
select -assert-count 1 t:$assert

2
tests/verific/memory_semantics.ys
View file

@ -1,4 +1,4 @@
verific -sv <<EOF
import -sv <<EOF
module top(clk);
input wire clk;

8
tests/verific/range_case.ys
View file

@ -1,12 +1,12 @@
verific -cfg db_abstract_case_statement_synthesis 0
import -cfg db_abstract_case_statement_synthesis 0
read -sv range_case.sv
verific -import top
import -import top
proc
rename top gold
verific -cfg db_abstract_case_statement_synthesis 1
import -cfg db_abstract_case_statement_synthesis 1
read -sv range_case.sv
verific -import top
import -import top
proc
rename top gate

4
tests/verific/rom_case.ys.fail
View file

@ -1,4 +1,4 @@
verific -sv <<EOF
import -sv <<EOF
module rom(input clk, input [2:0] addr, (* ram_style = "block" *) output reg [7:0] data);
always @(posedge clk) begin
@ -30,7 +30,7 @@ select -assert-count 1 t:RAM_BLOCK_SDP
design -reset
verific -vhdl <<EOF
import -vhdl <<EOF
library IEEE;
use IEEE.std_logic_1164.all;
use ieee.std_logic_unsigned.all;