aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile4
-rw-r--r--backends/btor/btor.cc1
-rw-r--r--backends/smt2/smt2.cc1
-rw-r--r--frontends/verific/verific.cc32
-rw-r--r--manual/command-reference-manual.tex3
-rw-r--r--passes/hierarchy/hierarchy.cc23
-rw-r--r--passes/memory/memory_map.cc20
-rw-r--r--passes/sat/async2sync.cc3
8 files changed, 70 insertions, 17 deletions
diff --git a/Makefile b/Makefile
index a8254e7fa..f6dc4332b 100644
--- a/Makefile
+++ b/Makefile
@@ -129,7 +129,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.18+33
+YOSYS_VER := 0.18+40
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -153,7 +153,7 @@ bumpversion:
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
-ABCREV = 09a7e6d
+ABCREV = 1863430
ABCPULL = 1
ABCURL ?= https://github.com/YosysHQ/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 VERBOSE=$(Q)
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 7dec70545..831a3ada2 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1405,7 +1405,6 @@ struct BtorBackend : public Backend {
log_header(design, "Executing BTOR backend.\n");
log_push();
- Pass::call(design, "memory_map -rom-only");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
log_pop();
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 6e70f9043..7481e0510 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1609,7 +1609,6 @@ struct Smt2Backend : public Backend {
log_header(design, "Executing SMT2 backend.\n");
log_push();
- Pass::call(design, "memory_map -rom-only");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
log_pop();
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index bbf860c96..8ecf54472 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -57,7 +57,7 @@ USING_YOSYS_NAMESPACE
#include "FileSystem.h"
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
-#include "InitialAssertions.h"
+#include "VerificExtensions.h"
#endif
#ifndef YOSYSHQ_VERIFIC_API_VERSION
@@ -2246,7 +2246,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
verific_params.Insert(i.first.c_str(), i.second.c_str());
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
- InitialAssertions::Rewrite("work", &verific_params);
+ VerificExtensions::ElaborateAndRewrite("work", &verific_params);
#endif
if (top.empty()) {
@@ -2312,6 +2312,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
nl_todo.erase(it);
}
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ VerificExtensions::Reset();
+#endif
hier_tree::DeleteHierarchicalTree();
veri_file::Reset();
#ifdef VERIFIC_VHDL_SUPPORT
@@ -2493,6 +2496,8 @@ struct VerificPass : public Pass {
log("\n");
log(" -v, -vv\n");
log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
+ log(" -pp <filename>\n");
+ log(" Pretty print design after elaboration to specified file.\n");
log("\n");
log("The following additional import options are useful for debugging the Verific\n");
log("bindings (for Yosys and/or Verific developers):\n");
@@ -2539,6 +2544,9 @@ struct VerificPass : public Pass {
log("Get/set Verific runtime flags.\n");
log("\n");
log("\n");
+#if defined(YOSYS_ENABLE_VERIFIC) and defined(YOSYSHQ_VERIFIC_EXTENSIONS)
+ VerificExtensions::Help();
+#endif
log("Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n");
log("https://www.yosyshq.com/\n");
log("\n");
@@ -2922,6 +2930,7 @@ struct VerificPass : public Pass {
bool mode_autocover = false, mode_fullinit = false;
bool flatten = false, extnets = false;
string dumpfile;
+ string ppfile;
Map parameters(STRING_HASH);
for (argidx++; argidx < GetSize(args); argidx++) {
@@ -2990,6 +2999,10 @@ struct VerificPass : public Pass {
dumpfile = args[++argidx];
continue;
}
+ if (args[argidx] == "-pp" && argidx+1 < GetSize(args)) {
+ ppfile = args[++argidx];
+ continue;
+ }
break;
}
@@ -2999,8 +3012,11 @@ struct VerificPass : public Pass {
std::set<std::string> top_mod_names;
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
- InitialAssertions::Rewrite(work, &parameters);
+ VerificExtensions::ElaborateAndRewrite(work, &parameters);
#endif
+ if (!ppfile.empty())
+ veri_file::PrettyPrint(ppfile.c_str(), nullptr, work.c_str());
+
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");
@@ -3113,6 +3129,9 @@ struct VerificPass : public Pass {
nl_todo.erase(it);
}
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ VerificExtensions::Reset();
+#endif
hier_tree::DeleteHierarchicalTree();
veri_file::Reset();
#ifdef VERIFIC_VHDL_SUPPORT
@@ -3187,6 +3206,13 @@ struct VerificPass : public Pass {
}
}
}
+#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
+ if (VerificExtensions::Execute(args, argidx, work,
+ [this](const std::vector<std::string> &args, size_t argidx, std::string msg)
+ { cmd_error(args, argidx, msg); } )) {
+ goto check_error;
+ }
+#endif
cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index edc8af6e6..3a9259867 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -2379,6 +2379,9 @@ resolves positional module parameters, unrolls array instances, and more.
like -check, but also throw an error if blackbox modules are
instantiated, and throw an error if the design has no top module.
+ -smtcheck
+ like -simcheck, but allow smtlib2_module modules.
+
-purge_lib
by default the hierarchy command will not remove library (blackbox)
modules. use this option to also remove unused blackbox modules.
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index d40d6e59f..d27fddf1c 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -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;
}
diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc
index ccfb8c94f..fd5b1f1ad 100644
--- a/passes/memory/memory_map.cc
+++ b/passes/memory/memory_map.cc
@@ -31,6 +31,7 @@ struct MemoryMapWorker
{
bool attr_icase = false;
bool rom_only = false;
+ bool keepdc = false;
dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
RTLIL::Design *design;
@@ -190,14 +191,15 @@ struct MemoryMapWorker
{
int addr = i + mem.start_offset;
int idx = addr & ((1 << abits) - 1);
+ SigSpec w_init = init_data.extract(i*mem.width, mem.width);
if (static_cells_map.count(addr) > 0)
{
data_reg_out[idx] = static_cells_map[addr];
count_static++;
}
- else if (mem.wr_ports.empty())
+ else if (mem.wr_ports.empty() && (!keepdc || w_init.is_fully_def()))
{
- data_reg_out[idx] = init_data.extract(i*mem.width, mem.width);
+ data_reg_out[idx] = w_init;
}
else
{
@@ -220,13 +222,15 @@ struct MemoryMapWorker
w_out_name = genid(mem.memid, "", addr, "$q");
RTLIL::Wire *w_out = module->addWire(w_out_name, mem.width);
- SigSpec w_init = init_data.extract(i*mem.width, mem.width);
if (!w_init.is_fully_undef())
w_out->attributes[ID::init] = w_init.as_const();
data_reg_out[idx] = w_out;
c->setPort(ID::Q, w_out);
+
+ if (mem.wr_ports.empty())
+ module->connect(RTLIL::SigSig(w_in, w_out));
}
}
@@ -380,11 +384,15 @@ struct MemoryMapPass : public Pass {
log(" -rom-only\n");
log(" only perform conversion for ROMs (memories with no write ports).\n");
log("\n");
+ log(" -keepdc\n");
+ log(" when mapping ROMs, keep x-bits shared across read ports.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool attr_icase = false;
bool rom_only = false;
+ bool keepdc = false;
dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n");
@@ -426,6 +434,11 @@ struct MemoryMapPass : public Pass {
rom_only = true;
continue;
}
+ if (args[argidx] == "-keepdc")
+ {
+ keepdc = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -435,6 +448,7 @@ struct MemoryMapPass : public Pass {
worker.attr_icase = attr_icase;
worker.attributes = attributes;
worker.rom_only = rom_only;
+ worker.keepdc = keepdc;
worker.run();
}
}
diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc
index 46c76eba9..6fdf470b1 100644
--- a/passes/sat/async2sync.cc
+++ b/passes/sat/async2sync.cc
@@ -75,6 +75,9 @@ struct Async2syncPass : public Pass {
if (ff.has_gclk)
continue;
+ if (ff.has_clk && ff.sig_clk.is_fully_const())
+ ff.has_ce = ff.has_clk = ff.has_srst = false;
+
if (ff.has_clk)
{
if (ff.has_sr) {
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-07 21:02:05 +0000