aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGELOG15
-rw-r--r--Makefile2
-rw-r--r--backends/smt2/smt2.cc77
-rw-r--r--backends/smt2/smtio.py21
-rw-r--r--frontends/verific/verific.cc50
-rw-r--r--kernel/constids.inc2
-rw-r--r--kernel/rtlil.cc10
-rw-r--r--kernel/rtlil.h4
-rw-r--r--manual/command-reference-manual.tex251
-rw-r--r--passes/cmds/sta.cc5
-rw-r--r--passes/fsm/fsmdata.h4
-rw-r--r--passes/opt/opt_ffinv.cc4
-rw-r--r--passes/opt/wreduce.cc10
-rw-r--r--passes/techmap/iopadmap.cc28
-rw-r--r--tests/various/.gitignore2
-rw-r--r--tests/various/smtlib2_module-expected.smt288
-rwxr-xr-xtests/various/smtlib2_module.sh5
-rw-r--r--tests/various/smtlib2_module.v33
18 files changed, 481 insertions, 130 deletions
diff --git a/CHANGELOG b/CHANGELOG
index 60e53aa6c..bb96fb3c6 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -4,6 +4,17 @@ List of major changes and improvements between releases
Yosys 0.17 .. Yosys 0.17-dev
--------------------------
+ * New commands and options
+ - Added "memory_libmap" pass
+ - Added "memory_bmux2rom" pass - converts muxes to ROMs
+ - Added "memory_dff -no-rw-check"
+ - Added "opt_ffinv" pass - push inverters through FFs
+ - Added "proc_rom" pass - convert switches to ROMs
+ - Added "proc -norom" option - will omit the proc_rom pass
+ - Added option "-no-rw-check" to synth passes
+ - Added "synth_ice40 -spram" option for automatic inference of SB_SPRAM256KA
+ - Added options "-nobram" and "-nolutram" to synth_machxo2 pass
+
* Formal Verification
- Fixed the signedness of $past's return value to be the same as the
argument's instead of always unsigned.
@@ -17,6 +28,10 @@ Yosys 0.17 .. Yosys 0.17-dev
- Fixed size and signedness computation of functions used in ternary
expressions or case item expressions
+ * Verific support
+ - Proper file location for readmem commands
+ - Added "-vlog-libext" option to specify search extension for libraries
+
Yosys 0.16 .. Yosys 0.17
--------------------------
* New commands and options
diff --git a/Makefile b/Makefile
index d9b149073..3cd3a7425 100644
--- a/Makefile
+++ b/Makefile
@@ -129,7 +129,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.17+72
+YOSYS_VER := 0.17+94
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index ed6f3aff9..7481e0510 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -53,6 +53,8 @@ struct Smt2Worker
std::map<int, int> bvsizes;
dict<IdString, char*> ids;
+ bool is_smtlib2_module;
+
const char *get_id(IdString n)
{
if (ids.count(n) == 0) {
@@ -112,9 +114,10 @@ struct Smt2Worker
}
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
- dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
- ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
- verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
+ dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache)
+ : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose),
+ statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width),
+ is_smtlib2_module(module->has_attribute(ID::smtlib2_module))
{
pool<SigBit> noclock;
@@ -124,6 +127,9 @@ struct Smt2Worker
memories = Mem::get_all_memories(module);
for (auto &mem : memories)
{
+ if (is_smtlib2_module)
+ log_error("Memory %s.%s not allowed in module with smtlib2_module attribute", get_id(module), mem.memid.c_str());
+
mem.narrow();
mem_dict[mem.memid] = &mem;
for (auto &port : mem.wr_ports)
@@ -893,10 +899,25 @@ struct Smt2Worker
log_id(cell->type), log_id(module), log_id(cell));
}
+ void verify_smtlib2_module()
+ {
+ if (!module->get_blackbox_attribute())
+ log_error("Module %s with smtlib2_module attribute must also have blackbox attribute.\n", log_id(module));
+ if (module->cells().size() > 0)
+ log_error("Module %s with smtlib2_module attribute must not have any cells inside it.\n", log_id(module));
+ for (auto wire : module->wires())
+ if (!wire->port_id)
+ log_error("Wire %s.%s must be input or output since module has smtlib2_module attribute.\n", log_id(module),
+ log_id(wire));
+ }
+
void run()
{
if (verbose) log("=> export logic driving outputs\n");
+ if (is_smtlib2_module)
+ verify_smtlib2_module();
+
pool<SigBit> reg_bits;
for (auto cell : module->cells())
if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
@@ -905,11 +926,25 @@ struct Smt2Worker
reg_bits.insert(bit);
}
+ std::string smtlib2_inputs;
+ std::vector<std::string> smtlib2_decls;
+ if (is_smtlib2_module) {
+ for (auto wire : module->wires()) {
+ if (!wire->port_input)
+ continue;
+ smtlib2_inputs += stringf("(|%s| (|%s_n %s| state))\n", get_id(wire), get_id(module), get_id(wire));
+ }
+ }
+
for (auto wire : module->wires()) {
bool is_register = false;
for (auto bit : SigSpec(wire))
if (reg_bits.count(bit))
is_register = true;
+ bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
+ if (is_smtlib2_comb_expr && !is_smtlib2_module)
+ log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
+ log_id(wire));
if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
RTLIL::SigSpec sig = sigmap(wire);
std::vector<std::string> comments;
@@ -924,11 +959,22 @@ struct Smt2Worker
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
+ std::string smtlib2_comb_expr;
+ if (is_smtlib2_comb_expr) {
+ smtlib2_comb_expr =
+ "(let (\n" + smtlib2_inputs + ")\n" + wire->get_string_attribute(ID::smtlib2_comb_expr) + "\n)";
+ if (wire->port_input || !wire->port_output)
+ log_error("smtlib2_comb_expr is only valid on output: wire %s.%s", log_id(module), log_id(wire));
+ if (!bvmode && GetSize(sig) > 1)
+ log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
+ log_id(module), log_id(wire));
+ }
+ auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
if (bvmode && GetSize(sig) > 1) {
- std::string sig_bv = get_bv(sig);
+ std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig);
if (!comments.empty())
- decls.insert(decls.end(), comments.begin(), comments.end());
- decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
+ out_decls.insert(out_decls.end(), comments.begin(), comments.end());
+ out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -936,19 +982,19 @@ struct Smt2Worker
} else {
std::vector<std::string> sig_bool;
for (int i = 0; i < GetSize(sig); i++) {
- sig_bool.push_back(get_bool(sig[i]));
+ sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
}
if (!comments.empty())
- decls.insert(decls.end(), comments.begin(), comments.end());
+ out_decls.insert(out_decls.end(), comments.begin(), comments.end());
for (int i = 0; i < GetSize(sig); i++) {
if (GetSize(sig) > 1) {
- decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
+ out_decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
} else {
- decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
+ out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -959,11 +1005,17 @@ struct Smt2Worker
}
}
+ decls.insert(decls.end(), smtlib2_decls.begin(), smtlib2_decls.end());
+
if (verbose) log("=> export logic associated with the initial state\n");
vector<string> init_list;
for (auto wire : module->wires())
if (wire->attributes.count(ID::init)) {
+ if (is_smtlib2_module)
+ log_error("init attribute not allowed on wires in module with smtlib2_module attribute: wire %s.%s",
+ log_id(module), log_id(wire));
+
RTLIL::SigSpec sig = sigmap(wire);
Const val = wire->attributes.at(ID::init);
val.bits.resize(GetSize(sig), State::Sx);
@@ -1687,7 +1739,10 @@ struct Smt2Backend : public Backend {
for (auto module : sorted_modules)
{
- if (module->get_blackbox_attribute() || module->has_processes_warn())
+ if (module->get_blackbox_attribute() && !module->has_attribute(ID::smtlib2_module))
+ continue;
+
+ if (module->has_processes_warn())
continue;
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 14feec30d..64e4cd79a 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -123,6 +123,7 @@ class SmtIo:
self.forall = False
self.timeout = 0
self.produce_models = True
+ self.recheck = False
self.smt2cache = [list()]
self.smt2_options = dict()
self.p = None
@@ -176,7 +177,10 @@ class SmtIo:
self.unroll = False
if self.solver == "yices":
- if self.noincr or self.forall:
+ if self.forall:
+ self.noincr = True
+
+ if self.noincr:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
@@ -189,11 +193,12 @@ class SmtIo:
if self.timeout != 0:
self.popen_vargs.append('-T:%d' % self.timeout);
- if self.solver == "cvc4":
+ if self.solver in ["cvc4", "cvc5"]:
+ self.recheck = True
if self.noincr:
- self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+ self.popen_vargs = [self.solver, '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
else:
- self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+ self.popen_vargs = [self.solver, '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
if self.timeout != 0:
self.popen_vargs.append('--tlimit=%d000' % self.timeout);
@@ -404,6 +409,8 @@ class SmtIo:
stmt = re.sub(r" *;.*", "", stmt)
if stmt == "": return
+ recheck = None
+
if unroll and self.unroll:
stmt = self.unroll_buffer + stmt
self.unroll_buffer = ""
@@ -415,6 +422,9 @@ class SmtIo:
s = self.parse(stmt)
+ if self.recheck and s and s[0].startswith("get-"):
+ recheck = self.unroll_idcnt
+
if self.debug_print:
print("-> %s" % s)
@@ -440,6 +450,9 @@ class SmtIo:
stmt = self.unparse(self.unroll_stmt(s))
+ if recheck is not None and recheck != self.unroll_idcnt:
+ self.check_sat(["sat"])
+
if stmt == "(push 1)":
self.unroll_stack.append((
copy(self.unroll_sorts),
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 328593099..6351483db 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -53,6 +53,9 @@ USING_YOSYS_NAMESPACE
#include "VhdlUnits.h"
#endif
+#include "VerificStream.h"
+#include "FileSystem.h"
+
#ifdef YOSYSHQ_VERIFIC_EXTENSIONS
#include "InitialAssertions.h"
#endif
@@ -83,7 +86,7 @@ bool verific_import_pending;
string verific_error_msg;
int verific_sva_fsm_limit;
-vector<string> verific_incdirs, verific_libdirs;
+vector<string> verific_incdirs, verific_libdirs, verific_libexts;
void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
{
@@ -118,6 +121,34 @@ string get_full_netlist_name(Netlist *nl)
return nl->CellBaseName();
}
+class YosysStreamCallBackHandler : public VerificStreamCallBackHandler
+{
+public:
+ YosysStreamCallBackHandler() : VerificStreamCallBackHandler() { }
+ virtual ~YosysStreamCallBackHandler() { }
+
+ virtual verific_stream *GetSysCallStream(const char *file_path)
+ {
+ if (!file_path) return nullptr;
+
+ linefile_type src_loc = GetFromLocation();
+
+ char *this_file_name = nullptr;
+ if (src_loc && !FileSystem::IsAbsolutePath(file_path)) {
+ const char *src_file_name = LineFile::GetFileName(src_loc);
+ char *dir_name = FileSystem::DirectoryPath(src_file_name);
+ if (dir_name) {
+ this_file_name = Strings::save(dir_name, "/", file_path);
+ Strings::free(dir_name);
+ file_path = this_file_name;
+ }
+ }
+ verific_stream *strm = new verific_ifstream(file_path);
+ Strings::free(this_file_name);
+ return strm;
+ }
+};
+
// ==================================================================
VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
@@ -2292,6 +2323,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
LineFile::DeleteAllLineFiles();
verific_incdirs.clear();
verific_libdirs.clear();
+ verific_libexts.clear();
verific_import_pending = false;
if (!verific_error_msg.empty())
@@ -2402,6 +2434,11 @@ struct VerificPass : public Pass {
log("find undefined modules.\n");
log("\n");
log("\n");
+ log(" verific -vlog-libext <extension>..\n");
+ log("\n");
+ log("Add Verilog library extensions, used when searching in library directories.\n");
+ log("\n");
+ log("\n");
log(" verific -vlog-define <macro>[=<value>]..\n");
log("\n");
log("Add Verilog defines.\n");
@@ -2648,6 +2685,8 @@ struct VerificPass : public Pass {
int argidx = 1;
std::string work = "work";
+ YosysStreamCallBackHandler cb;
+ veri_file::RegisterCallBackVerificStream(&cb);
if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
@@ -2683,6 +2722,12 @@ struct VerificPass : public Pass {
goto check_error;
}
+ if (GetSize(args) > argidx && args[argidx] == "-vlog-libext") {
+ for (argidx++; argidx < GetSize(args); argidx++)
+ verific_libexts.push_back(args[argidx]);
+ goto check_error;
+ }
+
if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
for (argidx++; argidx < GetSize(args); argidx++) {
string name = args[argidx];
@@ -2823,6 +2868,8 @@ struct VerificPass : public Pass {
veri_file::AddIncludeDir(dir.c_str());
for (auto &dir : verific_libdirs)
veri_file::AddYDir(dir.c_str());
+ for (auto &ext : verific_libexts)
+ veri_file::AddLibExt(ext.c_str());
while (argidx < GetSize(args))
file_names.Insert(args[argidx++].c_str());
@@ -3312,6 +3359,7 @@ struct VerificPass : public Pass {
LineFile::DeleteAllLineFiles();
verific_incdirs.clear();
verific_libdirs.clear();
+ verific_libexts.clear();
verific_import_pending = false;
goto check_error;
}
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 443ac3bcb..0f6dfc29b 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -196,6 +196,8 @@ X(STATE_NUM)
X(STATE_NUM_LOG2)
X(STATE_RST)
X(STATE_TABLE)
+X(smtlib2_module)
+X(smtlib2_comb_expr)
X(submod)
X(syn_ramstyle)
X(syn_romstyle)
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 72dcb89af..8346b56e0 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -204,7 +204,7 @@ RTLIL::Const::Const()
flags = RTLIL::CONST_FLAG_NONE;
}
-RTLIL::Const::Const(std::string str)
+RTLIL::Const::Const(const std::string &str)
{
flags = RTLIL::CONST_FLAG_STRING;
bits.reserve(str.size() * 8);
@@ -243,14 +243,6 @@ RTLIL::Const::Const(const std::vector<bool> &bits)
this->bits.emplace_back(b ? State::S1 : State::S0);
}
-RTLIL::Const::Const(const RTLIL::Const &c)
-{
- flags = c.flags;
- this->bits.reserve(c.size());
- for (const auto &b : c.bits)
- this->bits.push_back(b);
-}
-
bool RTLIL::Const::operator <(const RTLIL::Const &other) const
{
if (bits.size() != other.bits.size())
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index d8300f159..7a0b6b9c7 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -636,12 +636,12 @@ struct RTLIL::Const
std::vector<RTLIL::State> bits;
Const();
- Const(std::string str);
+ Const(const std::string &str);
Const(int val, int width = 32);
Const(RTLIL::State bit, int width = 1);
Const(const std::vector<RTLIL::State> &bits) : bits(bits) { flags = CONST_FLAG_NONE; }
Const(const std::vector<bool> &bits);
- Const(const RTLIL::Const &c);
+ Const(const RTLIL::Const &c) = default;
RTLIL::Const &operator =(const RTLIL::Const &other) = default;
bool operator <(const RTLIL::Const &other) const;
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index bafce6de6..4108527d8 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -2744,14 +2744,15 @@ is used then the $macc cell is mapped to $add, $sub, etc. cells instead.
\section{memory -- translate memories to basic cells}
\label{cmd:memory}
\begin{lstlisting}[numbers=left,frame=single]
- memory [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-bram <bram_rules>] [selection]
+ memory [-norom] [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-no-rw-check] [-bram <bram_rules>] [selection]
This pass calls all the other memory_* passes in a useful order:
opt_mem
opt_mem_priority
opt_mem_feedback
- memory_dff (skipped if called with -nordff or -memx)
+ memory_bmux2rom (skipped if called with -norom)
+ memory_dff [-no-rw-check] (skipped if called with -nordff or -memx)
opt_clean
memory_share [-nowiden] [-nosat]
opt_mem_widen
@@ -2765,6 +2766,14 @@ This converts memories to word-wide DFFs and address decoders
or multiport memory blocks if called with the -nomap option.
\end{lstlisting}
+\section{memory\_bmux2rom -- convert muxes to ROMs}
+\label{cmd:memory_bmux2rom}
+\begin{lstlisting}[numbers=left,frame=single]
+ memory_bmux2rom [options] [selection]
+
+This pass converts $bmux cells with constant A input to ROMs.
+\end{lstlisting}
+
\section{memory\_bram -- map memories to block rams}
\label{cmd:memory_bram}
\begin{lstlisting}[numbers=left,frame=single]
@@ -2878,11 +2887,45 @@ memory cells.
\section{memory\_dff -- merge input/output DFFs into memory read ports}
\label{cmd:memory_dff}
\begin{lstlisting}[numbers=left,frame=single]
- memory_dff [options] [selection]
+ memory_dff [-no-rw-check] [selection]
This pass detects DFFs at memory read ports and merges them into the memory port.
I.e. it consumes an asynchronous memory port and the flip-flops at its
interface and yields a synchronous memory port.
+
+ -no-rw-check
+ marks all recognized read ports as "return don't-care value on
+ read/write collision" (same result as setting the no_rw_check
+ attribute on all memories).
+\end{lstlisting}
+
+\section{memory\_libmap -- map memories to cells}
+\label{cmd:memory_libmap}
+\begin{lstlisting}[numbers=left,frame=single]
+ memory_libmap -lib <library_file> [-D <condition>] [selection]
+
+This pass takes a description of available RAM cell types and maps
+all selected memories to one of them, or leaves them to be mapped to FFs.
+
+ -lib <library_file>
+ Selects a library file containing RAM cell definitions. This option
+ can be passed more than once to select multiple libraries.
+ See passes/memory/memlib.md for description of the library format.
+
+ -D <condition>
+ Enables a condition that can be checked within the library file
+ to eg. select between slightly different hardware variants.
+ This option can be passed any number of times.
+
+ -logic-cost-rom <num>
+ -logic-cost-ram <num>
+ Sets the cost of a single bit for memory lowered to soft logic.
+
+ -no-auto-distributed
+ -no-auto-block
+ -no-auto-huge
+ Disables automatic mapping of given kind of RAMs. Manual mapping
+ (using ram_style or other attributes) is still supported.
\end{lstlisting}
\section{memory\_map -- translate multiport memories to basic cells}
@@ -3270,6 +3313,15 @@ It also performs some simple expression rewriting.
replaced by 'a'. the -keepdc option disables all such optimizations.
\end{lstlisting}
+\section{opt\_ffinv -- push inverters through FFs}
+\label{cmd:opt_ffinv}
+\begin{lstlisting}[numbers=left,frame=single]
+ opt_ffinv [selection]
+
+This pass pushes inverters to the other side of a FF when they can be merged
+into LUTs on the other side.
+\end{lstlisting}
+
\section{opt\_lut -- optimize LUT cells}
\label{cmd:opt_lut}
\begin{lstlisting}[numbers=left,frame=single]
@@ -3595,6 +3647,7 @@ This pass calls all the other proc_* passes in the most common order.
proc_prune
proc_init
proc_arst
+ proc_rom
proc_mux
proc_dlatch
proc_dff
@@ -3610,6 +3663,9 @@ The following options are supported:
-nomux
Will omit the proc_mux pass.
+ -norom
+ Will omit the proc_rom pass.
+
-global_arst [!]<netname>
This option is passed through to proc_arst.
@@ -3716,6 +3772,14 @@ a later assignment to the same signal and removes them.
This pass identifies unreachable branches in decision trees and removes them.
\end{lstlisting}
+\section{proc\_rom -- convert switches to ROMs}
+\label{cmd:proc_rom}
+\begin{lstlisting}[numbers=left,frame=single]
+ proc_rom [selection]
+
+This pass converts switches into read-only memories when appropriate.
+\end{lstlisting}
+
\section{qbfsat -- solve a 2QBF-SAT problem in the circuit}
\label{cmd:qbfsat}
\begin{lstlisting}[numbers=left,frame=single]
@@ -4498,15 +4562,16 @@ described here.
-unset <name>
do not modify the current selection. instead remove a previously saved
selection under the given name (see @<name> below).
+
-assert-none
do not modify the current selection. instead assert that the given
- selection is empty. i.e. produce an error if any object matching the
- selection is found.
+ selection is empty. i.e. produce an error if any object or module
+ matching the selection is found.
-assert-any
do not modify the current selection. instead assert that the given
- selection is non-empty. i.e. produce an error if no object matching
- the selection is found.
+ selection is non-empty. i.e. produce an error if no object or module
+ matching the selection is found.
-assert-count N
do not modify the current selection. instead assert that the given
@@ -5257,6 +5322,11 @@ on partly selected designs.
-flowmap
use FlowMap LUT techmapping instead of ABC
+ -no-rw-check
+ marks all recognized read ports as "return don't-care value on
+ read/write collision" (same result as setting the no_rw_check
+ attribute on all memories).
+
The following commands are executed by this synthesis command:
@@ -5424,16 +5494,9 @@ The following commands are executed by this synthesis command:
coarse:
synth -run coarse
- map_bram: (skip if -nobram)
- memory_bram -rules +/anlogic/brams.txt
- techmap -map +/anlogic/brams_map.v
- setundef -zero -params t:EG_PHY_BRAM
- setundef -zero -params t:EG_PHY_BRAM32K
-
- map_lutram: (skip if -nolutram)
- memory_bram -rules +/anlogic/lutrams.txt
- techmap -map +/anlogic/lutrams_map.v
- setundef -zero -params t:EG_LOGIC_DRAM16X4
+ map_ram:
+ memory_libmap -lib +/anlogic/lutrams.txt -lib +/anlogic/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+ techmap -map +/anlogic/lutrams_map.v -map +/anlogic/brams_map.v
map_ffram:
opt -fast -mux_undef -undriven -fine
@@ -5697,6 +5760,11 @@ This command runs synthesis for ECP5 FPGAs.
-nodsp
do not map multipliers to MULT18X18D
+ -no-rw-check
+ marks all recognized read ports as "return don't-care value on
+ read/write collision" (same result as setting the no_rw_check
+ attribute on all memories).
+
The following commands are executed by this synthesis command:
@@ -5726,20 +5794,16 @@ The following commands are executed by this synthesis command:
chtype -set $mul t:$__soft_mul (unless -nodsp)
alumacc
opt
- memory -nomap
+ memory -nomap [-no-rw-check]
opt_clean
- map_bram: (skip if -nobram)
- memory_bram -rules +/ecp5/brams.txt
- techmap -map +/ecp5/brams_map.v
-
- map_lutram: (skip if -nolutram)
- memory_bram -rules +/ecp5/lutrams.txt
- techmap -map +/ecp5/lutrams_map.v
+ map_ram:
+ memory_libmap -lib +/ecp5/lutrams.txt -lib +/ecp5/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+ techmap -map +/ecp5/lutrams_map.v -map +/ecp5/brams_map.v
map_ffram:
opt -fast -mux_undef -undriven -fine
- memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
+ memory_map
opt -undriven -fine
map_gates:
@@ -5835,9 +5899,10 @@ The following commands are executed by this synthesis command:
coarse:
synth -run coarse
- memory_bram -rules +/efinix/brams.txt
+
+ map_ram:
+ memory_libmap -lib +/efinix/brams.txt
techmap -map +/efinix/brams_map.v
- setundef -zero -params t:EFX_RAM_5K
map_ffram:
opt -fast -mux_undef -undriven -fine
@@ -5969,8 +6034,7 @@ The following commands are executed by this synthesis command:
opt_clean
map_bram: (skip if '-nobram')
- memory_bram -rules +/gatemate/brams.txt
- setundef -zero -params t:$__CC_BRAM_CASCADE t:$__CC_BRAM_40K_SDP t:$__CC_BRAM_20K_SDP t:$__CC_BRAM_20K_TDP t:$__CC_BRAM_40K_TDP
+ memory_libmap -lib +/gatemate/brams.txt
techmap -map +/gatemate/brams_map.v
map_ffram:
@@ -6076,6 +6140,11 @@ This command runs synthesis for Gowin FPGAs. This work is experimental.
-abc9
use new ABC9 flow (EXPERIMENTAL)
+ -no-rw-check
+ marks all recognized read ports as "return don't-care value on
+ read/write collision" (same result as setting the no_rw_check
+ attribute on all memories).
+
The following commands are executed by this synthesis command:
@@ -6090,16 +6159,11 @@ The following commands are executed by this synthesis command:
deminout
coarse:
- synth -run coarse
-
- map_bram: (skip if -nobram)
- memory_bram -rules +/gowin/brams.txt
- techmap -map +/gowin/brams_map.v
+ synth -run coarse [-no-rw-check]
- map_lutram: (skip if -nolutram)
- memory_bram -rules +/gowin/lutrams.txt
- techmap -map +/gowin/lutrams_map.v
- setundef -params -zero t:RAM16S4
+ map_ram:
+ memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+ techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map.v
map_ffram:
opt -fast -mux_undef -undriven -fine
@@ -6283,6 +6347,9 @@ This command runs synthesis for iCE40 FPGAs.
-nobram
do not use SB_RAM40_4K* cells in output netlist
+ -spram
+ enable automatic inference of SB_SPRAM256KA
+
-dsp
use iCE40 UltraPlus DSP cells for large arithmetic
@@ -6302,6 +6369,11 @@ This command runs synthesis for iCE40 FPGAs.
-flowmap
use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)
+ -no-rw-check
+ marks all recognized read ports as "return don't-care value on
+ read/write collision" (same result as setting the no_rw_check
+ attribute on all memories).
+
The following commands are executed by this synthesis command:
@@ -6329,7 +6401,7 @@ The following commands are executed by this synthesis command:
techmap -map +/cmp2lut.v -D LUT_WIDTH=4
opt_expr
opt_clean
- memory_dff
+ memory_dff [-no-rw-check]
wreduce t:$mul
techmap -map +/mul2dsp.v -map +/ice40/dsp_map.v -D DSP_A_MAXWIDTH=16 -D DSP_B_MAXWIDTH=16 -D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_Y_MINWIDTH=11 -D DSP_NAME=$__MUL16X16 (if -dsp)
select a:mul2dsp (if -dsp)
@@ -6341,17 +6413,17 @@ The following commands are executed by this synthesis command:
chtype -set $mul t:$__soft_mul (if -dsp)
alumacc
opt
- memory -nomap
+ memory -nomap [-no-rw-check]
opt_clean
- map_bram: (skip if -nobram)
- memory_bram -rules +/ice40/brams.txt
- techmap -map +/ice40/brams_map.v
+ map_ram:
+ memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt -no-auto-huge [-no-auto-huge] [-no-auto-block] (-no-auto-huge unless -spram, -no-auto-block if -nobram)
+ techmap -map +/ice40/brams_map.v -map +/ice40/spram_map.v
ice40_braminit
map_ffram:
opt -fast -mux_undef -undriven -fine
- memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
+ memory_map
opt -undriven -fine
map_gates:
@@ -6669,6 +6741,12 @@ This command runs synthesis for MachXO2 FPGAs.
from label is synonymous to 'begin', and empty to label is
synonymous to the end of the command list.
+ -nobram
+ do not use block RAM cells in output netlist
+
+ -nolutram
+ do not use LUT RAM cells in output netlist
+
-noflatten
do not flatten design before synthesis
@@ -6695,6 +6773,10 @@ The following commands are executed by this synthesis command:
coarse:
synth -run coarse
+ map_ram:
+ memory_libmap -lib +/machxo2/lutrams.txt -lib +/machxo2/brams.txt [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+ techmap -map +/machxo2/lutrams_map.v -map +/machxo2/brams_map.v
+
fine:
memory_map
opt -full
@@ -6830,24 +6912,13 @@ The following commands are executed by this synthesis command:
memory -nomap
opt_clean
- map_lram: (skip if -nolram)
- memory_bram -rules +/nexus/lrams.txt
- setundef -zero -params t:$__NX_PDPSC512K
- techmap -map +/nexus/lrams_map.v
-
- map_bram: (skip if -nobram)
- memory_bram -rules +/nexus/brams.txt
- setundef -zero -params t:$__NX_PDP16K
- techmap -map +/nexus/brams_map.v
-
- map_lutram: (skip if -nolutram)
- memory_bram -rules +/nexus/lutrams.txt
- setundef -zero -params t:$__NEXUS_DPR16X4
- techmap -map +/nexus/lutrams_map.v
+ map_ram:
+ memory_libmap -lib +/nexus/lutrams.txt -lib +/nexus/brams.txt -lib +/nexus/lrams.txt -no-auto-huge [-no-auto-block] [-no-auto-distributed] (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+ techmap -map +/nexus/lutrams_map.v -map +/nexus/brams_map.v -map +/nexus/lrams_map.v
map_ffram:
opt -fast -mux_undef -undriven -fine
- memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
+ memory_map
opt -undriven -fine
map_gates:
@@ -7238,17 +7309,10 @@ The following commands are executed by this synthesis command:
memory -nomap
opt_clean
- map_uram: (only if '-uram')
- memory_bram -rules +/xilinx/{family}_urams.txt
- techmap -map +/xilinx/{family}_urams_map.v
-
- map_bram: (skip if '-nobram')
- memory_bram -rules +/xilinx/{family}_brams.txt
- techmap -map +/xilinx/{family}_brams_map.v
-
- map_lutram: (skip if '-nolutram')
- memory_bram -rules +/xilinx/lut[46]_lutrams.txt
- techmap -map +/xilinx/lutrams_map.v
+ map_memory:
+ memory_libmap [...]
+ techmap -map +/xilinx/lutrams_<family>_map.v
+ techmap -map +/xilinx/brams_<family>_map.v
map_ffram:
opt -fast -full
@@ -7718,31 +7782,36 @@ Like -sv, but define FORMAL instead of SYNTHESIS.
Load the specified VHDL files into Verific.
- verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal] <command-file>
+ verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|
+ -sv2012|-sv|-formal] <command-file>
Load and execute the specified command file.
Override verilog parsing mode can be set.
The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.
-Command file parser supports following commands:
- +define - defines macro
- -u - upper case all identifier (makes Verilog parser case insensitive)
- -v - register library name (file)
- -y - register library name (directory)
- +incdir - specify include dir
- +libext - specify library extension
- +liborder - add library in ordered list
- +librescan - unresolved modules will be always searched starting with the first
- library specified by -y/-v options.
- -f/-file - nested -f option
- -F - nested -F option
-
- parse mode:
+Command file parser supports following commands in file:
+ +define+<MACRO>=<VALUE> - defines macro
+ -u - upper case all identifier (makes Verilog parser
+ case insensitive)
+ -v <filepath> - register library name (file)
+ -y <filepath> - register library name (directory)
+ +incdir+<filepath> - specify include dir
+ +libext+<filepath> - specify library extension
+ +liborder+<id> - add library in ordered list
+ +librescan - unresolved modules will be always searched
+ starting with the first library specified
+ by -y/-v options.
+ -f/-file <filepath> - nested -f option
+ -F <filepath> - nested -F option (relative path)
+ parse files:
+ <filepath>
+ +systemverilogext+<filepath>
+ +verilog1995ext+<filepath>
+ +verilog2001ext+<filepath>
+
+ analysis mode:
-ams
- +systemverilogext
+v2k
- +verilog1995ext
- +verilog2001ext
-sverilog
@@ -7879,8 +7948,8 @@ Application options:
Parameter can also contain comma separated list of file locations.
-blfile <file>
- Do not run application on locations specified in file, they can represent filename
- or filename and location in file.
+ Do not run application on locations specified in file, they can
+ represent filename or filename and location in file.
Applications:
diff --git a/passes/cmds/sta.cc b/passes/cmds/sta.cc
index 13e1ee13c..4ad0e96be 100644
--- a/passes/cmds/sta.cc
+++ b/passes/cmds/sta.cc
@@ -58,11 +58,14 @@ struct StaWorker
{
TimingInfo timing;
+ pool<IdString> unrecognised_cells;
+
for (auto cell : module->cells())
{
Module *inst_module = design->module(cell->type);
if (!inst_module) {
- log_warning("Cell type '%s' not recognised! Ignoring.\n", log_id(cell->type));
+ if (unrecognised_cells.insert(cell->type).second)
+ log_warning("Cell type '%s' not recognised! Ignoring.\n", log_id(cell->type));
continue;
}
diff --git a/passes/fsm/fsmdata.h b/passes/fsm/fsmdata.h
index 4ba3b4e4f..97371efab 100644
--- a/passes/fsm/fsmdata.h
+++ b/passes/fsm/fsmdata.h
@@ -91,8 +91,8 @@ struct FsmData
if (reset_state < 0 || reset_state >= state_num)
reset_state = -1;
- RTLIL::Const state_table = cell->parameters[ID::STATE_TABLE];
- RTLIL::Const trans_table = cell->parameters[ID::TRANS_TABLE];
+ const RTLIL::Const &state_table = cell->parameters[ID::STATE_TABLE];
+ const RTLIL::Const &trans_table = cell->parameters[ID::TRANS_TABLE];
for (int i = 0; i < state_num; i++) {
RTLIL::Const state_code;
diff --git a/passes/opt/opt_ffinv.cc b/passes/opt/opt_ffinv.cc
index fd76dd2be..fe5b59fa5 100644
--- a/passes/opt/opt_ffinv.cc
+++ b/passes/opt/opt_ffinv.cc
@@ -72,6 +72,8 @@ struct OptFfInvWorker
for (auto &port: q_ports) {
if (port.cell == ff.cell && port.port == ID::Q)
continue;
+ if (port.cell == d_inv)
+ return false;
if (port.port != ID::A)
return false;
if (!port.cell->type.in(ID($not), ID($_NOT_), ID($lut)))
@@ -148,6 +150,8 @@ struct OptFfInvWorker
for (auto &port: q_ports) {
if (port.cell == ff.cell && port.port == ID::Q)
continue;
+ if (port.cell == d_lut)
+ return false;
if (port.port != ID::A)
return false;
if (port.cell->type.in(ID($not), ID($_NOT_))) {
diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc
index aaad28ef0..08ab6de6f 100644
--- a/passes/opt/wreduce.cc
+++ b/passes/opt/wreduce.cc
@@ -30,6 +30,7 @@ struct WreduceConfig
{
pool<IdString> supported_cell_types;
bool keepdc = false;
+ bool mux_undef = false;
WreduceConfig()
{
@@ -83,7 +84,7 @@ struct WreduceWorker
SigBit ref = sig_a[i];
for (int k = 0; k < GetSize(sig_s); k++) {
- if ((config->keepdc || (ref != State::Sx && sig_b[k*GetSize(sig_a) + i] != State::Sx)) && ref != sig_b[k*GetSize(sig_a) + i])
+ if ((config->keepdc || !config->mux_undef || (ref != State::Sx && sig_b[k*GetSize(sig_a) + i] != State::Sx)) && ref != sig_b[k*GetSize(sig_a) + i])
goto no_match_ab;
if (sig_b[k*GetSize(sig_a) + i] != State::Sx)
ref = sig_b[k*GetSize(sig_a) + i];
@@ -479,6 +480,9 @@ struct WreducePass : public Pass {
log(" Do not change the width of memory address ports. Use this options in\n");
log(" flows that use the 'memory_memx' pass.\n");
log("\n");
+ log(" -mux_undef\n");
+ log(" remove 'undef' inputs from $mux, $pmux and $_MUX_ cells\n");
+ log("\n");
log(" -keepdc\n");
log(" Do not optimize explicit don't-care values.\n");
log("\n");
@@ -500,6 +504,10 @@ struct WreducePass : public Pass {
config.keepdc = true;
continue;
}
+ if (args[argidx] == "-mux_undef") {
+ config.mux_undef = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
diff --git a/passes/techmap/iopadmap.cc b/passes/techmap/iopadmap.cc
index 437ad5156..322eb7779 100644
--- a/passes/techmap/iopadmap.cc
+++ b/passes/techmap/iopadmap.cc
@@ -240,13 +240,13 @@ struct IopadmapPass : public Pass {
for (auto module : design->selected_modules())
{
dict<Wire *, dict<int, pair<Cell *, IdString>>> rewrite_bits;
- pool<SigSig> remove_conns;
+ dict<SigSig, pool<int>> remove_conns;
if (!toutpad_celltype.empty() || !tinoutpad_celltype.empty())
{
dict<SigBit, Cell *> tbuf_bits;
pool<SigBit> driven_bits;
- dict<SigBit, SigSig> z_conns;
+ dict<SigBit, std::pair<SigSig, int>> z_conns;
// Gather tristate buffers and always-on drivers.
for (auto cell : module->cells())
@@ -266,7 +266,7 @@ struct IopadmapPass : public Pass {
SigBit dstbit = conn.first[i];
SigBit srcbit = conn.second[i];
if (!srcbit.wire && srcbit.data == State::Sz) {
- z_conns[dstbit] = conn;
+ z_conns[dstbit] = {conn, i};
continue;
}
driven_bits.insert(dstbit);
@@ -317,8 +317,9 @@ struct IopadmapPass : public Pass {
// enable.
en_sig = SigBit(State::S0);
data_sig = SigBit(State::Sx);
- if (z_conns.count(wire_bit))
- remove_conns.insert(z_conns[wire_bit]);
+ auto it = z_conns.find(wire_bit);
+ if (it != z_conns.end())
+ remove_conns[it->second.first].insert(it->second.second);
}
if (wire->port_input)
@@ -477,9 +478,22 @@ struct IopadmapPass : public Pass {
if (!remove_conns.empty()) {
std::vector<SigSig> new_conns;
- for (auto &conn : module->connections())
- if (!remove_conns.count(conn))
+ for (auto &conn : module->connections()) {
+ auto it = remove_conns.find(conn);
+ if (it == remove_conns.end()) {
new_conns.push_back(conn);
+ } else {
+ SigSpec lhs, rhs;
+ for (int i = 0; i < GetSize(conn.first); i++) {
+ if (!it->second.count(i)) {
+ lhs.append(conn.first[i]);
+ rhs.append(conn.second[i]);
+ }
+ }
+ new_conns.push_back(SigSig(lhs, rhs));
+
+ }
+ }
module->new_connections(new_conns);
}
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index c6373468a..83e634820 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -6,3 +6,5 @@
/plugin.so
/plugin.so.dSYM
/temp
+/smtlib2_module.smt2
+/smtlib2_module-filtered.smt2
diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
new file mode 100644
index 000000000..ace858ca8
--- /dev/null
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -0,0 +1,88 @@
+; SMT-LIBv2 description generated by Yosys $VERSION
+; yosys-smt2-module smtlib2
+(declare-sort |smtlib2_s| 0)
+(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
+(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-input a 8
+(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
+(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
+; yosys-smt2-input b 8
+(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
+; yosys-smt2-output add 8
+(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a b)
+))
+; yosys-smt2-output eq 1
+(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(= a b)
+))
+; yosys-smt2-output sub 8
+(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a (bvneg b))
+))
+(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2
+; yosys-smt2-module uut
+(declare-sort |uut_s| 0)
+(declare-fun |uut_is| (|uut_s|) Bool)
+; yosys-smt2-cell smtlib2 s
+(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
+(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
+(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
+(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
+; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
+(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
+(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
+(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
+(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
+; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22
+(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19
+(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2
+(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11
+; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22
+(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20
+(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y
+(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13
+; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25
+(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21
+(define-fun |uut_a| ((state |uut_s|)) Bool (and
+ (|uut_a 0| state)
+ (|uut_a 1| state)
+ (|uut_a 2| state)
+ (|smtlib2_a| (|uut_h s| state))
+))
+(define-fun |uut_u| ((state |uut_s|)) Bool
+ (|smtlib2_u| (|uut_h s| state))
+)
+(define-fun |uut_i| ((state |uut_s|)) Bool
+ (|smtlib2_i| (|uut_h s| state))
+)
+(define-fun |uut_h| ((state |uut_s|)) Bool (and
+ (= (|uut_is| state) (|smtlib2_is| (|uut_h s| state)))
+ (= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a
+ (= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add
+ (= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b
+ (= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq
+ (= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub
+ (|smtlib2_h| (|uut_h s| state))
+))
+(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and
+ (= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b
+ (= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a
+ (|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state))
+)) ; end of module uut
+; yosys-smt2-topmod uut
+; end of yosys output
diff --git a/tests/various/smtlib2_module.sh b/tests/various/smtlib2_module.sh
new file mode 100755
index 000000000..491f65148
--- /dev/null
+++ b/tests/various/smtlib2_module.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+set -ex
+../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2'
+sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/ *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2
+diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2
diff --git a/tests/various/smtlib2_module.v b/tests/various/smtlib2_module.v
new file mode 100644
index 000000000..4aad86905
--- /dev/null
+++ b/tests/various/smtlib2_module.v
@@ -0,0 +1,33 @@
+(* smtlib2_module *)
+module smtlib2(a, b, add, sub, eq);
+ input [7:0] a, b;
+ (* smtlib2_comb_expr = "(bvadd a b)" *)
+ output [7:0] add;
+ (* smtlib2_comb_expr = "(bvadd a (bvneg b))" *)
+ output [7:0] sub;
+ (* smtlib2_comb_expr = "(= a b)" *)
+ output eq;
+endmodule
+
+(* top *)
+module uut;
+ wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2;
+ wire eq;
+
+ assign add2 = a + b;
+ assign sub2 = a - b;
+
+ smtlib2 s (
+ .a(a),
+ .b(b),
+ .add(add),
+ .sub(sub),
+ .eq(eq)
+ );
+
+ always @* begin
+ assert(add == add2);
+ assert(sub == sub2);
+ assert(eq == (a == b));
+ end
+endmodule
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-12 01:43:16 +0000