mirror of https://github.com/YosysHQ/yosys.git
Merge branch 'master' of https://github.com/cliffordwolf/yosys into vector_fix
This commit is contained in:
commit
778df553ed
|
@ -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
|
||||
========================================================
|
||||
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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++;
|
||||
|
|
Loading…
Reference in New Issue