diff options
author | Kaj Tuomi <kaj.tuomi@siru.fi> | 2017-10-17 09:53:11 +0300 |
---|---|---|
committer | Kaj Tuomi <kaj.tuomi@siru.fi> | 2017-10-17 09:53:11 +0300 |
commit | 778df553eda678c31eed91f16728fab84a8c8c1d (patch) | |
tree | c4779751b645d6a28881a9bb50653a54518708f8 | |
parent | 3efce9dea99d8b18e6e4694160b5348373afc175 (diff) | |
parent | 716dbc92745aa8b41d85a60d50263433d5a79393 (diff) | |
download | yosys-778df553eda678c31eed91f16728fab84a8c8c1d.tar.gz yosys-778df553eda678c31eed91f16728fab84a8c8c1d.tar.bz2 yosys-778df553eda678c31eed91f16728fab84a8c8c1d.zip |
Merge branch 'master' of https://github.com/cliffordwolf/yosys into vector_fix
-rw-r--r-- | frontends/verific/README | 7 | ||||
-rw-r--r-- | frontends/verific/verific.cc | 47 | ||||
-rw-r--r-- | passes/opt/opt_reduce.cc | 1 |
3 files changed, 54 insertions, 1 deletions
diff --git a/frontends/verific/README b/frontends/verific/README index e747255db..b4c436a3a 100644 --- a/frontends/verific/README +++ b/frontends/verific/README @@ -33,6 +33,13 @@ make -j8 ./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top' +Verific Features that should be enabled in your Verific library +=============================================================== + +database/DBCompileFlags.h: + DB_PRESERVE_INITIAL_VALUE + + Testing Verific+Yosys+SymbiYosys for formal verification ======================================================== diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index e77931528..77594b8cf 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1851,6 +1851,22 @@ struct VerificPass : public Pass { log("Load the specified VHDL files into Verific.\n"); log("\n"); log("\n"); + log(" verific -vlog-incdir <directory>..\n"); + log("\n"); + log("Add Verilog include directories.\n"); + log("\n"); + log("\n"); + log(" verific -vlog-libdir <directory>..\n"); + log("\n"); + log("Add Verilog library directories. Verific will search in this directories to\n"); + log("find undefined modules.\n"); + log("\n"); + 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("\n"); + log("\n"); log(" verific -import [options] <top-module>..\n"); log("\n"); log("Elaborate the design for the specified top modules, import to Yosys and\n"); @@ -1909,6 +1925,8 @@ struct VerificPass : public Pass { Message::RegisterCallBackMsg(msg_func); RuntimeFlags::SetVar("db_allow_external_nets", 1); RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0); + veri_file::DefineCmdLineMacro("VERIFIC"); + veri_file::DefineCmdLineMacro("SYNTHESIS"); const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); @@ -1924,6 +1942,33 @@ struct VerificPass : public Pass { int argidx = 1; + if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") { + for (argidx++; argidx < GetSize(args); argidx++) + veri_file::AddIncludeDir(args[argidx].c_str()); + goto check_error; + } + + if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") { + for (argidx++; argidx < GetSize(args); argidx++) + veri_file::AddYDir(args[argidx].c_str()); + goto check_error; + } + + if (GetSize(args) > argidx && args[argidx] == "-vlog-define") { + for (argidx++; argidx < GetSize(args); argidx++) { + string name = args[argidx]; + size_t equal = name.find('='); + if (equal != std::string::npos) { + string value = name.substr(equal+1); + name = name.substr(0, equal); + veri_file::DefineCmdLineMacro(name.c_str(), value.c_str()); + } else { + veri_file::DefineCmdLineMacro(name.c_str()); + } + } + goto check_error; + } + if (GetSize(args) > argidx && args[argidx] == "-vlog95") { for (argidx++; argidx < GetSize(args); argidx++) if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95)) @@ -2139,6 +2184,8 @@ struct VerificPass : public Pass { nl_done.insert(nl); } + veri_file::Reset(); + vhdl_file::Reset(); Libset::Reset(); goto check_error; } diff --git a/passes/opt/opt_reduce.cc b/passes/opt/opt_reduce.cc index 10bdf7221..eb9d02ad5 100644 --- a/passes/opt/opt_reduce.cc +++ b/passes/opt/opt_reduce.cc @@ -88,7 +88,6 @@ struct OptReduceWorker RTLIL::SigSpec new_sig_a(new_sig_a_bits); if (new_sig_a != sig_a || sig_a.size() != cell->getPort("\\A").size()) { - new_sig_a.sort_and_unify(); log(" New input vector for %s cell %s: %s\n", cell->type.c_str(), cell->name.c_str(), log_signal(new_sig_a)); did_something = true; total_count++; |