mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

Merge pull request #3391 from programmerjake/simcheck-allow-smtlib2-blackboxes

Browse source 
add hierarchy -smtcheck
This commit is contained in:
Jannis Harder 2022-07-01 14:38:45 +02:00 • committed by GitHub
commit 0182b26aba
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 19 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

23
passes/hierarchy/hierarchy.cc
View file

@ -439,7 +439,8 @@ void check_cell_connections(const RTLIL::Module &module, RTLIL::Cell &cell, RTLI
}
}
bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, std::vector<std::string> &libdirs)
bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, bool flag_smtcheck,
std::vector<std::string> &libdirs)
{
bool did_something = false;
std::map<RTLIL::Cell*, std::pair<int, int>> array_cells;
@ -477,7 +478,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
RTLIL::Module *mod = design->module(cell->type);
if (!mod)
{
mod = get_module(*design, *cell, *module, flag_check || flag_simcheck, libdirs);
mod = get_module(*design, *cell, *module, flag_check || flag_simcheck || flag_smtcheck, libdirs);
// If we still don't have a module, treat the cell as a black box and skip
// it. Otherwise, we either loaded or derived something so should set the
@ -495,11 +496,11 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
// interfaces.
if_expander.visit_connections(*cell, *mod);
if (flag_check || flag_simcheck)
if (flag_check || flag_simcheck || flag_smtcheck)
check_cell_connections(*module, *cell, *mod);
if (mod->get_blackbox_attribute()) {
if (flag_simcheck)
if (flag_simcheck || (flag_smtcheck && !mod->get_bool_attribute(ID::smtlib2_module)))
log_error("Module `%s' referenced in module `%s' in cell `%s' is a blackbox/whitebox module.\n",
cell->type.c_str(), module->name.c_str(), cell->name.c_str());
continue;
@ -737,6 +738,9 @@ struct HierarchyPass : public Pass {
log(" like -check, but also throw an error if blackbox modules are\n");
log(" instantiated, and throw an error if the design has no top module.\n");
log("\n");
log(" -smtcheck\n");
log(" like -simcheck, but allow smtlib2_module modules.\n");
log("\n");
log(" -purge_lib\n");
log(" by default the hierarchy command will not remove library (blackbox)\n");
log(" modules. use this option to also remove unused blackbox modules.\n");
@ -803,6 +807,7 @@ struct HierarchyPass : public Pass {
bool flag_check = false;
bool flag_simcheck = false;
bool flag_smtcheck = false;
bool purge_lib = false;
RTLIL::Module *top_mod = NULL;
std::string load_top_mod;
@ -821,7 +826,7 @@ struct HierarchyPass : public Pass {
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !top_mod) {
if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !flag_smtcheck && !top_mod) {
generate_mode = true;
log("Entering generate mode.\n");
while (++argidx < args.size()) {
@ -868,6 +873,10 @@ struct HierarchyPass : public Pass {
flag_simcheck = true;
continue;
}
if (args[argidx] == "-smtcheck") {
flag_smtcheck = true;
continue;
}
if (args[argidx] == "-purge_lib") {
purge_lib = true;
continue;
@ -1013,7 +1022,7 @@ struct HierarchyPass : public Pass {
}
}
if (flag_simcheck && top_mod == nullptr)
if ((flag_simcheck || flag_smtcheck) && top_mod == nullptr)
log_error("Design has no top module.\n");
if (top_mod != NULL) {
@ -1039,7 +1048,7 @@ struct HierarchyPass : public Pass {
}
for (auto module : used_modules) {
if (expand_module(design, module, flag_check, flag_simcheck, libdirs))
if (expand_module(design, module, flag_check, flag_simcheck, flag_smtcheck, libdirs))
did_something = true;
}