aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorKaj Tuomi <kaj.tuomi@siru.fi>2017-10-17 09:53:11 +0300
committerKaj Tuomi <kaj.tuomi@siru.fi>2017-10-17 09:53:11 +0300
commit778df553eda678c31eed91f16728fab84a8c8c1d (patch)
treec4779751b645d6a28881a9bb50653a54518708f8
parent3efce9dea99d8b18e6e4694160b5348373afc175 (diff)
parent716dbc92745aa8b41d85a60d50263433d5a79393 (diff)
downloadyosys-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/README7
-rw-r--r--frontends/verific/verific.cc47
-rw-r--r--passes/opt/opt_reduce.cc1
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++;