diff options
author | Clifford Wolf <clifford@clifford.at> | 2018-06-29 10:02:27 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2018-06-29 10:02:27 +0200 |
commit | ebf0f003d3e8d219b396d4c6a3943e1ce54d2879 (patch) | |
tree | 24eeb07e97c09921471bed42f79c4edae16e869a /frontends/verific/verific.cc | |
parent | afedb2d03ee07738025ae77d73d280044c29ec2f (diff) | |
download | yosys-ebf0f003d3e8d219b396d4c6a3943e1ce54d2879.tar.gz yosys-ebf0f003d3e8d219b396d4c6a3943e1ce54d2879.tar.bz2 yosys-ebf0f003d3e8d219b396d4c6a3943e1ce54d2879.zip |
Add "verific -formal" and "read -formal"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verific.cc')
-rw-r--r-- | frontends/verific/verific.cc | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index c9a071f70..62a8028b8 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1695,8 +1695,13 @@ 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 SYNTHESIS and VERIFIC are defined implicitly.\n"); log("\n"); log("\n"); + log(" verific -formal <verilog-file>..\n"); + log("\n"); + log("Like -sv, but define FORMAL instead of SYNTHESIS.\n"); + log("\n"); log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n"); log("\n"); log("Load the specified VHDL files into Verific.\n"); @@ -1715,7 +1720,7 @@ struct VerificPass : public Pass { log("\n"); log(" verific -vlog-define <macro>[=<value>]..\n"); log("\n"); - log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n"); + log("Add Verilog defines.\n"); log("\n"); log("\n"); log(" verific -vlog-undef <macro>..\n"); @@ -1790,8 +1795,6 @@ struct VerificPass : public Pass { RuntimeFlags::SetVar("veri_extract_dualport_rams", 0); RuntimeFlags::SetVar("veri_extract_multiport_rams", 1); RuntimeFlags::SetVar("db_infer_wide_operators", 1); - veri_file::DefineCmdLineMacro("VERIFIC"); - veri_file::DefineCmdLineMacro("SYNTHESIS"); verific_verbose = 0; @@ -1845,7 +1848,7 @@ struct VerificPass : public Pass { } if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" || - args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv")) + args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")) { Array file_names; unsigned verilog_mode; @@ -1858,11 +1861,14 @@ struct VerificPass : public Pass { verilog_mode = veri_file::SYSTEM_VERILOG_2005; else if (args[argidx] == "-sv2009") verilog_mode = veri_file::SYSTEM_VERILOG_2009; - else if (args[argidx] == "-sv2012" || args[argidx] == "-sv") + else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal") verilog_mode = veri_file::SYSTEM_VERILOG; else log_abort(); + veri_file::DefineMacro("VERIFIC"); + veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS"); + for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) { std::string name = args[argidx].substr(2); if (args[argidx] == "-D") { @@ -2157,7 +2163,7 @@ struct ReadPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n"); + log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n"); log("\n"); log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n"); log("is only available via Verific.)\n"); @@ -2206,11 +2212,13 @@ struct ReadPass : public Pass { return; } - if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv") { + if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") { if (use_verific) { args[0] = "verific"; } else { args[0] = "read_verilog"; + if (args[1] == "-formal") + args.insert(args.begin()+1, std::string()); args[1] = "-sv"; } Pass::call(design, args); |