aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--frontends/verific/verific.cc98
-rw-r--r--passes/opt/opt_clean.cc53
-rw-r--r--tests/opt/opt_clean_mem.ys49
4 files changed, 178 insertions, 24 deletions
diff --git a/Makefile b/Makefile
index 79b0061ea..f7d90c4b1 100644
--- a/Makefile
+++ b/Makefile
@@ -123,7 +123,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.9+3617
+YOSYS_VER := 0.9+3621
GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
OBJS = kernel/version_$(GIT_REV).o
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 05c4ec344..e236aaaf2 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -55,7 +55,7 @@ USING_YOSYS_NAMESPACE
# error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
#endif
-#if SYMBIOTIC_VERIFIC_API_VERSION < 20200901
+#if SYMBIOTIC_VERIFIC_API_VERSION < 20200902
# error "Please update your version of Symbiotic EDA flavored Verific."
#endif
@@ -2203,6 +2203,9 @@ struct VerificPass : public Pass {
log("\n");
log("Application options:\n");
log("\n");
+ log(" -module <module>\n");
+ log(" Run formal application only on specified module.\n");
+ log("\n");
log(" -blacklist <filename[:lineno]>\n");
log(" Do not run application on modules from files that match the filename\n");
log(" or filename and line number if provided in such format.\n");
@@ -2491,8 +2494,11 @@ struct VerificPass : public Pass {
goto check_error;
}
- if (argidx+1 < GetSize(args) && args[argidx] == "-app")
+ if (argidx < GetSize(args) && args[argidx] == "-app")
{
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx, "No formal application specified.\n");
+
VerificFormalApplications vfa;
auto apps = vfa.GetApps();
std::string app = args[++argidx];
@@ -2500,15 +2506,42 @@ struct VerificPass : public Pass {
if (apps.find(app) == apps.end())
log_cmd_error("Application '%s' does not exist.\n", app.c_str());
+ FormalApplication *application = apps[app];
+ application->setLogger([](std::string msg) { log("%s",msg.c_str()); } );
+ VeriModule *selected_module = nullptr;
+
for (argidx++; argidx < GetSize(args); argidx++) {
- if (args[argidx] == "-blacklist" && argidx+1 < GetSize(args)) {
+ std::string error;
+ if (application->checkParams(args, argidx, error)) {
+ if (!error.empty())
+ cmd_error(args, argidx, error);
+ continue;
+ }
+
+ if (args[argidx] == "-module" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No module name specified.\n");
+ std::string module = args[++argidx];
+ VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+ selected_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr;
+ if (!selected_module) {
+ log_error("Can't find module '%s'.\n", module.c_str());
+ }
+ continue;
+ }
+ if (args[argidx] == "-blacklist" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No blacklist specified.\n");
+
std::string line = args[++argidx];
std::string p;
while (!(p = next_token(line, ",\t\r\n ")).empty())
blacklists.push_back(p);
continue;
}
- if (args[argidx] == "-blfile" && argidx+1 < GetSize(args)) {
+ if (args[argidx] == "-blfile" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No blacklist file specified.\n");
std::string fn = args[++argidx];
std::ifstream f(fn);
if (f.fail())
@@ -2525,12 +2558,32 @@ struct VerificPass : public Pass {
}
if (argidx < GetSize(args))
cmd_error(args, argidx, "unknown option/parameter");
+
+ application->setBlacklists(&blacklists);
+ application->setSingleModuleMode(selected_module!=nullptr);
+
+ const char *err = application->validate();
+ if (err)
+ cmd_error(args, argidx, err);
+
MapIter mi;
- VeriModule *module ;
VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
log("Running formal application '%s'.\n", app.c_str());
- FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) {
- vfa.Run(module,apps[app],blacklists);
+
+ if (selected_module) {
+ std::string out;
+ if (!application->execute(selected_module, out))
+ log_error("%s", out.c_str());
+ }
+ else {
+ VeriModule *module ;
+ FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) {
+ std::string out;
+ if (!application->execute(module, out)) {
+ log_error("%s", out.c_str());
+ break;
+ }
+ }
}
goto check_error;
}
@@ -2579,8 +2632,8 @@ struct VerificPass : public Pass {
if (argidx < GetSize(args) && args[argidx] == "-template")
{
- if (!(argidx < GetSize(args)))
- cmd_error(args, argidx, "No template type specified.\n");
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No template type specified.\n");
VerificTemplateGenerator vfg;
auto gens = vfg.GetGenerators();
@@ -2588,8 +2641,9 @@ struct VerificPass : public Pass {
if (gens.find(app) == gens.end())
log_cmd_error("Template generator '%s' does not exist.\n", app.c_str());
TemplateGenerator *generator = gens[app];
- if (!(argidx < GetSize(args)))
- cmd_error(args, argidx, "No top module specified.\n");
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No top module specified.\n");
+ generator->setLogger([](std::string msg) { log("%s",msg.c_str()); } );
std::string module = args[++argidx];
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
@@ -2604,9 +2658,19 @@ struct VerificPass : public Pass {
const char *out_filename = nullptr;
for (argidx++; argidx < GetSize(args); argidx++) {
- if (generator->checkParams(args, argidx))
+ std::string error;
+ if (generator->checkParams(args, argidx, error)) {
+ if (!error.empty())
+ cmd_error(args, argidx, error);
continue;
- if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
+ }
+
+ if (args[argidx] == "-chparam" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No param name specified.\n");
+ if (!(argidx+2 < GetSize(args)))
+ cmd_error(args, argidx+2, "No param value specified.\n");
+
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
@@ -2616,7 +2680,9 @@ struct VerificPass : public Pass {
continue;
}
- if (args[argidx] == "-out" && argidx+1 < GetSize(args)) {
+ if (args[argidx] == "-out" && argidx < GetSize(args)) {
+ if (!(argidx+1 < GetSize(args)))
+ cmd_error(args, argidx+1, "No output file specified.\n");
out_filename = args[++argidx].c_str();
continue;
}
@@ -2630,7 +2696,9 @@ struct VerificPass : public Pass {
if (err)
cmd_error(args, argidx, err);
- std::string val = generator->generate(veri_module, &parameters);
+ std::string val;
+ if (!generator->generate(veri_module, val, &parameters))
+ log_error("%s", val.c_str());
FILE *of = stdout;
if (out_filename) {
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index bd9856e81..883374cf6 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -55,7 +55,7 @@ struct keep_cache_t
if (!module->get_bool_attribute(ID::keep)) {
bool found_keep = false;
for (auto cell : module->cells())
- if (query(cell, true /* ignore_specify_mem */)) {
+ if (query(cell, true /* ignore_specify */)) {
found_keep = true;
break;
}
@@ -70,12 +70,12 @@ struct keep_cache_t
return cache[module];
}
- bool query(Cell *cell, bool ignore_specify_mem = false)
+ bool query(Cell *cell, bool ignore_specify = false)
{
if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
return true;
- if (!ignore_specify_mem && cell->type.in(ID($memwr), ID($meminit), ID($specify2), ID($specify3), ID($specrule)))
+ if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
return true;
if (cell->has_keep_attr())
@@ -95,6 +95,8 @@ int count_rm_cells, count_rm_wires;
void rmunused_module_cells(Module *module, bool verbose)
{
SigMap sigmap(module);
+ dict<IdString, pool<Cell*>> mem2cells;
+ pool<IdString> mem_unused;
pool<Cell*> queue, unused;
pool<SigBit> used_raw_bits;
dict<SigBit, pool<Cell*>> wire2driver;
@@ -108,6 +110,17 @@ void rmunused_module_cells(Module *module, bool verbose)
}
}
+ for (auto &it : module->memories) {
+ mem_unused.insert(it.first);
+ }
+
+ for (Cell *cell : module->cells()) {
+ if (cell->type.in(ID($memwr), ID($meminit))) {
+ IdString mem_id = cell->getParam(ID::MEMID).decode_string();
+ mem2cells[mem_id].insert(cell);
+ }
+ }
+
for (auto &it : module->cells_) {
Cell *cell = it.second;
for (auto &it2 : cell->connections()) {
@@ -145,17 +158,33 @@ void rmunused_module_cells(Module *module, bool verbose)
while (!queue.empty())
{
pool<SigBit> bits;
- for (auto cell : queue)
- for (auto &it : cell->connections())
- if (!ct_all.cell_known(cell->type) || ct_all.cell_input(cell->type, it.first))
- for (auto bit : sigmap(it.second))
- bits.insert(bit);
+ pool<IdString> mems;
+ for (auto cell : queue) {
+ for (auto &it : cell->connections())
+ if (!ct_all.cell_known(cell->type) || ct_all.cell_input(cell->type, it.first))
+ for (auto bit : sigmap(it.second))
+ bits.insert(bit);
+
+ if (cell->type == ID($memrd)) {
+ IdString mem_id = cell->getParam(ID::MEMID).decode_string();
+ if (mem_unused.count(mem_id)) {
+ mem_unused.erase(mem_id);
+ mems.insert(mem_id);
+ }
+ }
+ }
queue.clear();
+
for (auto bit : bits)
for (auto c : wire2driver[bit])
if (unused.count(c))
queue.insert(c), unused.erase(c);
+
+ for (auto mem : mems)
+ for (auto c : mem2cells[mem])
+ if (unused.count(c))
+ queue.insert(c), unused.erase(c);
}
unused.sort(RTLIL::sort_by_name_id<RTLIL::Cell>());
@@ -168,6 +197,14 @@ void rmunused_module_cells(Module *module, bool verbose)
count_rm_cells++;
}
+ for (auto it : mem_unused)
+ {
+ if (verbose)
+ log_debug(" removing unused memory `%s'.\n", it.c_str());
+ delete module->memories.at(it);
+ module->memories.erase(it);
+ }
+
for (auto &it : module->cells_) {
Cell *cell = it.second;
for (auto &it2 : cell->connections()) {
diff --git a/tests/opt/opt_clean_mem.ys b/tests/opt/opt_clean_mem.ys
new file mode 100644
index 000000000..b35b15871
--- /dev/null
+++ b/tests/opt/opt_clean_mem.ys
@@ -0,0 +1,49 @@
+read_verilog <<EOT
+module top(...);
+
+input [7:0] wa;
+input [7:0] ra1;
+input [7:0] ra2;
+input [7:0] wd;
+input clk;
+wire [7:0] rd1;
+wire [7:0] rd2;
+
+reg [7:0] mem[0:7];
+
+always @(posedge clk)
+ mem[wa] <= wd;
+assign rd1 = mem[ra1];
+assign rd2 = mem[ra2];
+
+initial mem[8'h12] = 8'h34;
+
+endmodule
+EOT
+
+proc
+memory_dff
+
+select -assert-count 2 t:$memrd
+select -assert-count 1 t:$memwr
+select -assert-count 1 t:$meminit
+design -save orig
+
+opt_clean
+select -assert-none t:$memrd
+select -assert-none t:$memwr
+select -assert-none t:$meminit
+
+design -load orig
+expose top/rd1
+opt_clean
+select -assert-count 1 t:$memrd
+select -assert-count 1 t:$memwr
+select -assert-count 1 t:$meminit
+
+design -load orig
+expose top/rd1 top/rd2
+opt_clean
+select -assert-count 2 t:$memrd
+select -assert-count 1 t:$memwr
+select -assert-count 1 t:$meminit
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-23 12:30:00 +0000