Merge branch 'main' into sat_clkgate

.github/actions/setup-build-env/action.yml

@@ -42,7 +42,7 @@ runs:
       if: runner.os == 'Linux' && inputs.get-build-deps == 'true'
       uses: awalsh128/cache-apt-pkgs-action@v1.6.0
       with:
-        packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev
+        packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev libgtest-dev
         version: ${{ inputs.runs-on }}-buildys
 
     - name: Linux docs dependencies
@@ -52,15 +52,6 @@ runs:
         packages: graphviz xdot
         version: ${{ inputs.runs-on }}-docsys
 
-    # if updating test dependencies, make sure to update
-    # docs/source/yosys_internals/extending_yosys/test_suites.rst to match.
-    - name: Linux test dependencies
-      if: runner.os == 'Linux' && inputs.get-test-deps == 'true'
-      uses: awalsh128/cache-apt-pkgs-action@v1.6.0
-      with:
-        packages: libgtest-dev
-        version: ${{ inputs.runs-on }}-testys
-
     - name: Install macOS Dependencies
       if: runner.os == 'macOS'
       shell: bash

.github/workflows/test-build.yml

@@ -73,8 +73,9 @@ jobs:
         run: |
           mkdir build
           cd build
-          make -f ../Makefile config-$CC SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0 VERIFIC_DIR=../verific
+          make -f ../Makefile config-$CC ENABLE_LTO=1 SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0 VERIFIC_DIR=../verific
           make -f ../Makefile -j$procs ENABLE_LTO=1 SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0 VERIFIC_DIR=../verific
+          make -f ../Makefile unit-test -j$procs ENABLE_LTO=1 SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0 VERIFIC_DIR=../verific
 
       - name: Log yosys-config output
         run: |
@@ -84,7 +85,7 @@ jobs:
         shell: bash
         run: |
           cd build
-          tar -cvf ../build.tar share/ yosys yosys-*
+          tar -cvf ../build.tar share/ yosys yosys-* libyosys.so
 
       - name: Store build artifact
         uses: actions/upload-artifact@v4
@@ -138,7 +139,7 @@ jobs:
       - name: Run tests
         shell: bash
         run: |
-          make -j$procs test TARGETS= EXTRA_TARGETS= CONFIG=$CC SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0
+          make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= CONFIG=$CC SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0
 
       - name: Report errors
         if: ${{ failure() }}

.github/workflows/test-sanitizers.yml

@@ -66,7 +66,7 @@ jobs:
       - name: Run tests
         shell: bash
         run: |
-          make -j$procs test TARGETS= EXTRA_TARGETS= SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0 ENABLE_VERIFIC=0
+          make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= SMALL=0 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0 ENABLE_VERIFIC=0
 
       - name: Report errors
         if: ${{ failure() }}
@@ -74,7 +74,3 @@ jobs:
         run: |
           find tests/**/*.err -print -exec cat {} \;
 
-      - name: Run unit tests
-        shell: bash
-        run: |
-          make -j$procs unit-test ENABLE_LIBYOSYS=1

.github/workflows/test-verific.yml

@@ -68,7 +68,7 @@ jobs:
 
       - name: Run Yosys tests
         run: |
-          make -j$procs test
+          make -j$procs vanilla-test
 
       - name: Run Verific specific Yosys tests
         run: |
@@ -80,11 +80,6 @@ jobs:
         run: |
           make -C sby run_ci
 
-      - name: Run unit tests
-        shell: bash
-        run: |
-          make -j$procs unit-test ENABLE_LTO=1 ENABLE_LIBYOSYS=1
-
   test-pyosys:
     needs: pre-job
     if: ${{ needs.pre-job.outputs.should_skip != 'true' && github.repository == 'YosysHQ/Yosys' }}

Dockerfile

@@ -1,58 +0,0 @@
-ARG IMAGE="python:3-slim-buster"
-
-#---
-
-FROM $IMAGE AS base
-
-RUN apt-get update -qq \
- && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
-    ca-certificates \
-    clang \
-    lld \
-    curl \
-    libffi-dev \
-    libreadline-dev \
-    tcl-dev \
-    graphviz \
-    xdot \
- && apt-get autoclean && apt-get clean && apt-get -y autoremove \
- && update-ca-certificates \
- && rm -rf /var/lib/apt/lists
-
-#---
-
-FROM base AS build
-
-RUN apt-get update -qq \
- && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
-    bison \
-    flex \
-    gawk \
-    gcc \
-    git \
-    iverilog \
-    pkg-config \
- && apt-get autoclean && apt-get clean && apt-get -y autoremove \
- && rm -rf /var/lib/apt/lists
-
-COPY . /yosys
-
-ENV PREFIX /opt/yosys
-
-RUN cd /yosys \
- && make \
- && make install \
- && make test
-
-#---
-
-FROM base
-
-COPY --from=build /opt/yosys /opt/yosys
-
-ENV PATH /opt/yosys/bin:$PATH
-
-RUN useradd -m yosys
-USER yosys
-
-CMD ["yosys"]

Makefile

@@ -17,7 +17,7 @@ ENABLE_GHDL := 0
 ENABLE_SLANG := 0
 ENABLE_VERIFIC := 1
 ENABLE_VERIFIC_SYSTEMVERILOG := 1
-ENABLE_VERIFIC_VHDL := 1
+ENABLE_VERIFIC_VHDL := 0
 ENABLE_VERIFIC_HIER_TREE := 1
 ENABLE_VERIFIC_SILIMATE_EXTENSIONS := 1
 ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0
@@ -177,7 +177,7 @@ ifeq ($(OS), Haiku)
 CXXFLAGS += -D_DEFAULT_SOURCE
 endif
 
-YOSYS_VER := 0.62+9
+YOSYS_VER := 0.62+55
 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
 YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2)
 YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'.' -f3)
@@ -669,6 +669,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h))
 $(eval $(call add_include_file,kernel/yw.h))
 $(eval $(call add_include_file,libs/ezsat/ezsat.h))
 $(eval $(call add_include_file,libs/ezsat/ezminisat.h))
+$(eval $(call add_include_file,libs/ezsat/ezcmdline.h))
 ifeq ($(ENABLE_ZLIB),1)
 $(eval $(call add_include_file,libs/fst/fstapi.h))
 endif
@@ -714,6 +715,7 @@ OBJS += libs/json11/json11.o
 
 OBJS += libs/ezsat/ezsat.o
 OBJS += libs/ezsat/ezminisat.o
+OBJS += libs/ezsat/ezcmdline.o
 
 OBJS += libs/minisat/Options.o
 OBJS += libs/minisat/SimpSolver.o
@@ -1032,9 +1034,11 @@ makefile-tests/%: %/run-test.mk $(TARGETS) $(EXTRA_TARGETS)
 	$(MAKE) -C $* -f run-test.mk
 	+@echo "...passed tests in $*"
 
-test: makefile-tests abcopt-tests seed-tests
+test: vanilla-test unit-test
+
+vanilla-test: makefile-tests abcopt-tests seed-tests
 	@echo ""
-	@echo "  Passed \"make test\"."
+	@echo "  Passed \"make vanilla-test\"."
 ifeq ($(ENABLE_VERIFIC),1)
 ifeq ($(YOSYS_NOVERIFIC),1)
 	@echo "  Ran tests without verific support due to YOSYS_NOVERIFIC=1."
@@ -1066,11 +1070,11 @@ ystests: $(TARGETS) $(EXTRA_TARGETS)
 
 # Unit test
 unit-test: libyosys.so
-	@$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \
+	@$(MAKE) -f $(UNITESTPATH)/Makefile CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \
 		CXXFLAGS="$(CXXFLAGS)" LINKFLAGS="$(LINKFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)"
 
 clean-unit-test:
-	@$(MAKE) -C $(UNITESTPATH) clean
+	@$(MAKE) -f $(UNITESTPATH)/Makefile clean
 
 install-dev: $(PROGRAM_PREFIX)yosys-config share
 	$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR)

README.md

@@ -114,8 +114,8 @@ To build Yosys simply type 'make' in this directory.
 	$ sudo make install
 
 Tests are located in the tests subdirectory and can be executed using the test
-target. Note that you need gawk as well as a recent version of iverilog (i.e.
-build from git). Then, execute tests via:
+target. Note that you need gawk, a recent version of iverilog, and gtest.
+Execute tests via:
 
 	$ make test
 

abc

@@ -1 +1 @@
-Subproject commit f37e4e1361d8ed14d2cadf1494143bb1a4d10cf2
+Subproject commit bb9bc209ff23e6690865935a70bcc9294101c5ce

backends/verilog/verilog_backend.cc

@@ -95,7 +95,8 @@ bool VERILOG_BACKEND::id_is_verilog_escaped(const std::string &str) {
 
 PRIVATE_NAMESPACE_BEGIN
 
-bool verbose, norename, noattr, srcattronly, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase;
+bool verbose, norename, noattr, srcattronly, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs,
+  noparallelcase, default_params;
 int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
 dict<RTLIL::IdString, int> auto_name_map;
 std::set<RTLIL::IdString> reg_wires;
@@ -439,6 +440,13 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
 	}
 }
 
+void dump_parameter(std::ostream &f, std::string indent, RTLIL::IdString id_string, RTLIL::Const parameter)
+{
+	f << stringf("%sparameter %s = ", indent.c_str(), id(id_string).c_str());
+	dump_const(f, parameter);
+	f << ";\n";
+}
+
 void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 {
 	dump_attributes(f, indent, wire->attributes, "\n", /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name));
@@ -2456,6 +2464,10 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		f << indent + "  " << "reg " << id(initial_id) << " = 0;\n";
 	}
 
+	if (default_params)
+		for (auto p : module->parameter_default_values)
+			dump_parameter(f, indent + "  ", p.first, p.second);
+
 	// first dump input / output according to their order in module->ports
 	for (auto port : module->ports)
 		dump_wire(f, indent + "  ", module->wire(port));
@@ -2566,6 +2578,10 @@ struct VerilogBackend : public Backend {
 		log("        use 'defparam' statements instead of the Verilog-2001 syntax for\n");
 		log("        cell parameters.\n");
 		log("\n");
+		log("    -default_params\n");
+		log("        emit module parameter declarations from\n");
+		log("        parameter_default_values.\n");
+		log("\n");
 		log("    -blackboxes\n");
 		log("        usually modules with the 'blackbox' attribute are ignored. with\n");
 		log("        this option set only the modules with the 'blackbox' attribute\n");
@@ -2604,6 +2620,7 @@ struct VerilogBackend : public Backend {
 		siminit = false;
 		simple_lhs = false;
 		noparallelcase = false;
+		default_params = false;
 		auto_prefix = "";
 
 		bool blackboxes = false;
@@ -2668,6 +2685,10 @@ struct VerilogBackend : public Backend {
 				defparam = true;
 				continue;
 			}
+			if (arg == "-defaultparams") {
+				default_params = true;
+				continue;
+			}
 			if (arg == "-decimal") {
 				decimal = true;
 				continue;

docs/source/yosys_internals/extending_yosys/test_suites.rst

@@ -8,7 +8,44 @@ Running the included test suite
 
 The Yosys source comes with a test suite to avoid regressions and keep
 everything working as expected.  Tests can be run by calling ``make test`` from
-the root Yosys directory.
+the root Yosys directory. By default, this runs vanilla and unit tests.
+
+Vanilla tests
+~~~~~~~~~~~~~
+
+These make up the majority of our testing coverage.
+They can be run with ``make vanilla-test`` and are based on calls to
+make subcommands (``make makefile-tests``) and shell scripts
+(``make seed-tests`` and ``make abcopt-tests``). Both use ``run-test.sh``
+files, but make-based tests only call ``tests/gen-tests-makefile.sh``
+to generate a makefile appropriate for the given directory, so only
+afterwards when make is invoked do the tests actually run.
+
+Usually their structure looks something like this:
+you write a .ys file that gets automatically run,
+which runs a frontend like ``read_verilog`` or ``read_rtlil`` with
+a relative path or a heredoc, then runs some commands including the command
+under test, and then uses :doc:`/using_yosys/more_scripting/selections`
+with ``-assert-count``. Usually it's unnecessary to "register" the test anywhere
+as if it's being added to an existing directory, depending
+on how the ``run-test.sh`` in that directory works.
+
+Unit tests
+~~~~~~~~~~
+
+Running the unit tests requires the following additional packages:
+
+.. tab:: Ubuntu
+
+   .. code:: console
+
+      sudo apt-get install libgtest-dev
+
+.. tab:: macOS
+
+   No additional requirements.
+
+Unit tests can be run with ``make unit-test``.
 
 Functional tests
 ~~~~~~~~~~~~~~~~
@@ -41,23 +78,6 @@ instructions <https://github.com/Z3Prover/z3>`_.
 Then, set the :makevar:`ENABLE_FUNCTIONAL_TESTS` make variable when calling
 ``make test`` and the functional tests will be run as well.
 
-Unit tests
-~~~~~~~~~~
-
-Running the unit tests requires the following additional packages:
-
-.. tab:: Ubuntu
-
-   .. code:: console
-
-      sudo apt-get install libgtest-dev
-
-.. tab:: macOS
-
-   No additional requirements.
-
-Unit tests can be run with ``make unit-test``. 
-
 Docs tests
 ~~~~~~~~~~
 

frontends/blif/blifparse.cc

@@ -678,6 +678,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
 							goto try_next_value;
 					}
 				}
+				log_assert(i < lutptr->size());
 				lutptr->set(i, !strcmp(output, "0") ? RTLIL::State::S0 : RTLIL::State::S1);
 			try_next_value:;
 			}

frontends/json/jsonparse.cc

@@ -302,6 +302,9 @@ void json_import(Design *design, string &modname, JsonNode *node)
 	if (node->data_dict.count("attributes"))
 		json_parse_attr_param(module->attributes, node->data_dict.at("attributes"));
 
+	if (node->data_dict.count("parameter_default_values"))
+		json_parse_attr_param(module->parameter_default_values, node->data_dict.at("parameter_default_values"));
+
 	dict<int, SigBit> signal_bits;
 
 	if (node->data_dict.count("ports"))

frontends/verific/verific.cc

@@ -257,12 +257,16 @@ bool is_blackbox(Netlist *nl)
 
 RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
 {
-	return module->uniquify(RTLIL::escape_id(obj->Name()));
+	RTLIL::IdString base = RTLIL::escape_id(obj->Name());
+	int &idx = uniquify_cache[base];
+	return module->uniquify(base, idx);
 }
 
 RTLIL::IdString VerificImporter::new_verific_id_suffix(RTLIL::IdString id, const char *suffix)
 {
-	return module->uniquify(stringf("%s_%s", id, suffix));
+	RTLIL::IdString base = stringf("%s_%s", id, suffix);
+	int &idx = uniquify_cache[base];
+	return module->uniquify(base, idx);
 }
 
 static const RTLIL::Const extract_vhdl_boolean(std::string &val)
@@ -1549,6 +1553,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 	module->name = module_name;
 	design->add(module);
 
+	uniquify_cache.clear();
+
 	if (is_blackbox(nl)) {
 		log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
 		log_flush();

frontends/verific/verific.h

@@ -80,6 +80,8 @@ struct VerificImporter
 	bool mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific;
 	bool mode_autocover, mode_fullinit;
 
+	dict<RTLIL::IdString, int> uniquify_cache;
+
 	int num_sva_continue = 0;
 
 	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);

kernel/celledges.cc

@@ -112,6 +112,41 @@ void reduce_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
 		db->add_edge(cell, ID::A, i, ID::Y, 0, -1);
 }
 
+void logic_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
+{
+	int a_width = GetSize(cell->getPort(ID::A));
+	int b_width = GetSize(cell->getPort(ID::B));
+
+	for (int i = 0; i < a_width; i++)
+		db->add_edge(cell, ID::A, i, ID::Y, 0, -1);
+	for (int i = 0; i < b_width; i++)
+		db->add_edge(cell, ID::B, i, ID::Y, 0, -1);
+}
+
+void concat_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
+{
+	int a_width = GetSize(cell->getPort(ID::A));
+	int b_width = GetSize(cell->getPort(ID::B));
+
+	for (int i = 0; i < a_width; i++)
+		db->add_edge(cell, ID::A, i, ID::Y, i, -1);
+	for (int i = 0; i < b_width; i++)
+		db->add_edge(cell, ID::B, i, ID::Y, a_width + i, -1);
+}
+
+void slice_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
+{
+	int offset = cell->getParam(ID::OFFSET).as_int();
+	int a_width = GetSize(cell->getPort(ID::A));
+	int y_width = GetSize(cell->getPort(ID::Y));
+
+	for (int i = 0; i < y_width; i++) {
+		int a_bit = offset + i;
+		if (a_bit >= 0 && a_bit < a_width)
+			db->add_edge(cell, ID::A, a_bit, ID::Y, i, -1);
+	}
+}
+
 void compare_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
 {
 	int a_width = GetSize(cell->getPort(ID::A));
@@ -254,7 +289,7 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
 					int skip = 1 << (k + 1);
 					int base = skip -1;
 					if (i % skip != base && i - a_width + 2 < 1 << b_width_capped)
-						db->add_edge(cell, ID::B, k, ID::Y, i, -1);	
+						db->add_edge(cell, ID::B, k, ID::Y, i, -1);
 				} else if (is_signed) {
 					if (i - a_width + 2 < 1 << b_width_capped)
 						db->add_edge(cell, ID::B, k, ID::Y, i, -1);
@@ -388,6 +423,64 @@ void ff_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
 			db->add_edge(cell, ID::ARST, 0, ID::Q, k, -1);
 }
 
+void full_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
+{
+	std::vector<RTLIL::IdString> input_ports;
+	std::vector<RTLIL::IdString> output_ports;
+
+	for (auto &conn : cell->connections())
+	{
+		RTLIL::IdString port = conn.first;
+		RTLIL::PortDir dir = cell->port_dir(port);
+		if (cell->input(port) || dir == RTLIL::PortDir::PD_INOUT)
+			input_ports.push_back(port);
+		if (cell->output(port) || dir == RTLIL::PortDir::PD_INOUT)
+			output_ports.push_back(port);
+	}
+
+	for (auto out_port : output_ports)
+	{
+		int out_width = GetSize(cell->getPort(out_port));
+		for (int out_bit = 0; out_bit < out_width; out_bit++)
+		{
+			for (auto in_port : input_ports)
+			{
+				int in_width = GetSize(cell->getPort(in_port));
+				for (int in_bit = 0; in_bit < in_width; in_bit++)
+					db->add_edge(cell, in_port, in_bit, out_port, out_bit, -1);
+			}
+		}
+	}
+}
+
+void bweqx_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
+{
+	int width = GetSize(cell->getPort(ID::Y));
+	int a_width = GetSize(cell->getPort(ID::A));
+	int b_width = GetSize(cell->getPort(ID::B));
+	int max_width = std::min(width, std::min(a_width, b_width));
+
+	for (int i = 0; i < max_width; i++) {
+		db->add_edge(cell, ID::A, i, ID::Y, i, -1);
+		db->add_edge(cell, ID::B, i, ID::Y, i, -1);
+	}
+}
+
+void bwmux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
+{
+	int width = GetSize(cell->getPort(ID::Y));
+	int a_width = GetSize(cell->getPort(ID::A));
+	int b_width = GetSize(cell->getPort(ID::B));
+	int s_width = GetSize(cell->getPort(ID::S));
+	int max_width = std::min(width, std::min(a_width, std::min(b_width, s_width)));
+
+	for (int i = 0; i < max_width; i++) {
+		db->add_edge(cell, ID::A, i, ID::Y, i, -1);
+		db->add_edge(cell, ID::B, i, ID::Y, i, -1);
+		db->add_edge(cell, ID::S, i, ID::Y, i, -1);
+	}
+}
+
 PRIVATE_NAMESPACE_END
 
 bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL::Cell *cell)
@@ -417,6 +510,21 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
 		return true;
 	}
 
+	if (cell->type.in(ID($logic_and), ID($logic_or))) {
+		logic_op(this, cell);
+		return true;
+	}
+
+	if (cell->type == ID($slice)) {
+		slice_op(this, cell);
+		return true;
+	}
+
+	if (cell->type == ID($concat)) {
+		concat_op(this, cell);
+		return true;
+	}
+
 	if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) {
 		shift_op(this, cell);
 		return true;
@@ -442,6 +550,16 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
 		return true;
 	}
 
+	if (cell->type == ID($bweqx)) {
+		bweqx_op(this, cell);
+		return true;
+	}
+
+	if (cell->type == ID($bwmux)) {
+		bwmux_op(this, cell);
+		return true;
+	}
+
 	if (cell->type.in(ID($mem_v2), ID($memrd), ID($memrd_v2), ID($memwr), ID($memwr_v2), ID($meminit))) {
 		mem_op(this, cell);
 		return true;
@@ -452,13 +570,24 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
 		return true;
 	}
 
-	// FIXME: $mul $div $mod $divfloor $modfloor $slice $concat
-	// FIXME: $lut $sop $alu $lcu $macc $macc_v2 $fa
-	// FIXME: $mul $div $mod $divfloor $modfloor $pow $slice $concat $bweqx
-	// FIXME: $lut $sop $alu $lcu $macc $fa $logic_and $logic_or $bwmux
+	if (cell->type.in(ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow))) {
+		full_op(this, cell);
+		return true;
+	}
 
-	// FIXME: $_BUF_ $_NOT_ $_AND_ $_NAND_ $_OR_ $_NOR_ $_XOR_ $_XNOR_ $_ANDNOT_ $_ORNOT_
-	// FIXME: $_MUX_ $_NMUX_ $_MUX4_ $_MUX8_ $_MUX16_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_
+	if (cell->type.in(ID($lut), ID($sop), ID($alu), ID($lcu), ID($macc), ID($macc_v2))) {
+		full_op(this, cell);
+		return true;
+	}
+
+	if (cell->type.in(
+			ID($_BUF_), ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_),
+			ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_), ID($_MUX_), ID($_NMUX_),
+			ID($_MUX4_), ID($_MUX8_), ID($_MUX16_), ID($_AOI3_), ID($_OAI3_), ID($_AOI4_),
+			ID($_OAI4_), ID($_TBUF_))) {
+		full_op(this, cell);
+		return true;
+	}
 
 	// FIXME: $specify2 $specify3 $specrule ???
 	// FIXME: $equiv $set_tag $get_tag $overwrite_tag $original_tag
@@ -468,4 +597,3 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
 
 	return false;
 }
-

kernel/ffmerge.cc

@@ -156,8 +156,8 @@ bool FfMergeHelper::find_output_ff(RTLIL::SigSpec sig, FfData &ff, pool<std::pai
 	return found;
 }
 
-bool FfMergeHelper::find_input_ff(RTLIL::SigSpec sig, FfData &ff, pool<std::pair<Cell *, int>> &bits) {
-	ff = FfData(module, initvals, NEW_ID);
+bool FfMergeHelper::find_input_ff(RTLIL::SigSpec sig, FfData &ff, pool<std::pair<Cell *, int>> &bits, RTLIL::IdString name) {
+	ff = FfData(module, initvals, name);
 	sigmap->apply(sig);
 
 	bool found = false;

kernel/ffmerge.h

@@ -110,7 +110,7 @@ struct FfMergeHelper
 	// a constant-input FF bit (with matching initial value and reset value).
 	// However, this will not work if the input is all-constant — if the caller
 	// cares about this case, it needs to check for it explicitely.
-	bool find_input_ff(RTLIL::SigSpec sig, FfData &ff, pool<std::pair<Cell *, int>> &bits);
+	bool find_input_ff(RTLIL::SigSpec sig, FfData &ff, pool<std::pair<Cell *, int>> &bits, RTLIL::IdString name);
 
 	// To be called on find_output_ff result that will be merged.  This
 	// marks the given FF bits as used up (and not to be considered for

kernel/rtlil.cc

@@ -1346,8 +1346,10 @@ void RTLIL::Design::add(RTLIL::Binding *binding)
 
 RTLIL::Module *RTLIL::Design::addModule(RTLIL::IdString name)
 {
-	if (modules_.count(name) != 0)
-		log_error("Attempted to add new module named '%s', but a module by that name already exists\n", name);
+	if (modules_.count(name) != 0) {
+		log_warning("Attempted to add new module named '%s', but a module by that name already exists\n", name);
+		return modules_.at(name);
+	}
 	log_assert(refcount_modules_ == 0);
 
 	RTLIL::Module *module = new RTLIL::Module;

kernel/satgen.h

@@ -59,6 +59,7 @@ struct SatSolver
 
 struct ezSatPtr : public std::unique_ptr<ezSAT> {
 	ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
+	explicit ezSatPtr(SatSolver *solver) : unique_ptr<ezSAT>((solver ? solver : yosys_satsolver)->create()) { }
 };
 
 struct SatGen

libs/ezsat/ezcmdline.cc

@@ -0,0 +1,92 @@
+
+#include "ezcmdline.h"
+
+#include "../../kernel/yosys.h"
+
+ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {}
+
+ezCmdlineSAT::~ezCmdlineSAT() {}
+
+bool ezCmdlineSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
+{
+#if !defined(YOSYS_DISABLE_SPAWN)
+	const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX");
+	const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str());
+	const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str());
+	FILE *dimacs = fopen(cnf_filename.c_str(), "w");
+	if (dimacs == nullptr) {
+		Yosys::log_cmd_error("Failed to create CNF file `%s`.\n", cnf_filename.c_str());
+	}
+
+	std::vector<int> modelIdx;
+	for (auto id : modelExpressions)
+		modelIdx.push_back(bind(id));
+	std::vector<std::vector<int>> extraClauses;
+	for (auto id : assumptions)
+		extraClauses.push_back({bind(id)});
+
+	printDIMACS(dimacs, false, extraClauses);
+	fclose(dimacs);
+
+	bool status_sat = false;
+	bool status_unsat = false;
+	std::vector<bool> values;
+
+	auto line_callback = [&](const std::string &line) {
+		if (line.empty()) {
+			return;
+		}
+		if (line[0] == 's') {
+			if (line.substr(0, 5) == "s SAT") {
+				status_sat = true;
+			}
+			if (line.substr(0, 7) == "s UNSAT") {
+				status_unsat = true;
+			}
+			return;
+		}
+		if (line[0] == 'v') {
+			std::stringstream ss(line.substr(1));
+			int lit;
+			while (ss >> lit) {
+				if (lit == 0) {
+					return;
+				}
+				bool val = lit >= 0;
+				int ind = lit >= 0 ? lit - 1 : -lit - 1;
+				if (Yosys::GetSize(values) <= ind) {
+					values.resize(ind + 1);
+				}
+				values[ind] = val;
+			}
+		}
+	};
+	int return_code = Yosys::run_command(sat_command, line_callback);
+	if (return_code != 0 && return_code != 10 && return_code != 20) {
+		Yosys::log_cmd_error("Shell command failed!\n");
+	}
+
+	modelValues.clear();
+	modelValues.resize(modelIdx.size());
+
+	if (!status_sat && !status_unsat) {
+		solverTimeoutStatus = true;
+	}
+	if (!status_sat) {
+		return false;
+	}
+
+	for (size_t i = 0; i < modelIdx.size(); i++) {
+		int idx = modelIdx[i];
+		bool refvalue = true;
+
+		if (idx < 0)
+			idx = -idx, refvalue = false;
+
+		modelValues[i] = (values.at(idx - 1) == refvalue);
+	}
+	return true;
+#else
+	Yosys::log_error("SAT solver command not available in this build!\n");
+#endif
+}

libs/ezsat/ezcmdline.h

@@ -0,0 +1,36 @@
+/*
+ *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.com>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#ifndef EZSATCOMMAND_H
+#define EZSATCOMMAND_H
+
+#include "ezsat.h"
+
+class ezCmdlineSAT : public ezSAT
+{
+private:
+	std::string command;
+
+public:
+	ezCmdlineSAT(const std::string &cmd);
+	virtual ~ezCmdlineSAT();
+	bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) override;
+};
+
+#endif

libs/ezsat/ezminisat.cc

@@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
 {
 	preSolverCallback();
 
-	solverTimoutStatus = false;
+	solverTimeoutStatus = false;
 
 	if (0) {
 contradiction:
@@ -206,7 +206,7 @@ contradiction:
 #if defined(HAS_ALARM)
 	if (solverTimeout > 0) {
 		if (alarmHandlerTimeout == 0)
-			solverTimoutStatus = true;
+			solverTimeoutStatus = true;
 		alarm(0);
 		sigaction(SIGALRM, &old_sig_action, NULL);
 		alarm(old_alarm_timeout);

libs/ezsat/ezsat.cc

@@ -54,7 +54,7 @@ ezSAT::ezSAT()
 	cnfClausesCount = 0;
 
 	solverTimeout = 0;
-	solverTimoutStatus = false;
+	solverTimeoutStatus = false;
 
 	literal("CONST_TRUE");
 	literal("CONST_FALSE");
@@ -1222,10 +1222,15 @@ ezSATvec ezSAT::vec(const std::vector<int> &vec)
 	return ezSATvec(*this, vec);
 }
 
-void ezSAT::printDIMACS(FILE *f, bool verbose) const
+void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector<std::vector<int>> &extraClauses) const
 {
+	if (f == nullptr) {
+		fprintf(stderr, "Usage error: printDIMACS() must not be called with a null FILE pointer\n");
+		abort();
+	}
+
 	if (cnfConsumed) {
-		fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
+		fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n");
 		abort();
 	}
 
@@ -1259,8 +1264,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
 	std::vector<std::vector<int>> all_clauses;
 	getFullCnf(all_clauses);
 	assert(cnfClausesCount == int(all_clauses.size()));
+	for (auto c : extraClauses)
+		all_clauses.push_back(c);
 
-	fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
+	fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size());
 	int maxClauseLen = 0;
 	for (auto &clause : all_clauses)
 		maxClauseLen = std::max(int(clause.size()), maxClauseLen);

libs/ezsat/ezsat.h

@@ -78,7 +78,7 @@ protected:
 
 public:
 	int solverTimeout;
-	bool solverTimoutStatus;
+	bool solverTimeoutStatus;
 
 	ezSAT();
 	virtual ~ezSAT();
@@ -153,8 +153,8 @@ public:
 		solverTimeout = newTimeoutSeconds;
 	}
 
-	bool getSolverTimoutStatus() {
-		return solverTimoutStatus;
+	bool getSolverTimeoutStatus() {
+		return solverTimeoutStatus;
 	}
 
 	// manage CNF (usually only accessed by SAT solvers)
@@ -295,7 +295,7 @@ public:
 
 	// printing CNF and internal state
 
-	void printDIMACS(FILE *f, bool verbose = false) const;
+	void printDIMACS(FILE *f, bool verbose = false, const std::vector<std::vector<int>> &extraClauses = std::vector<std::vector<int>>()) const;
 	void printInternalState(FILE *f) const;
 
 	// more sophisticated constraints (designed to be used directly with assume(..))

passes/cmds/scratchpad.cc

@@ -37,7 +37,7 @@ struct ScratchpadPass : public Pass {
 		log("\n");
 		log("    scratchpad [options]\n");
 		log("\n");
-		log("This pass allows to read and modify values from the scratchpad of the current\n");
+		log("This pass allows reading and modifying values from the scratchpad of the current\n");
 		log("design. Options:\n");
 		log("\n");
 		log("    -get <identifier>\n");

passes/memory/memory_dff.cc

@@ -558,7 +558,7 @@ struct MemoryDffWorker
 
 		FfData ff;
 		pool<std::pair<Cell *, int>> bits;
-		if (!merger.find_input_ff(port.addr, ff, bits)) {
+		if (!merger.find_input_ff(port.addr, ff, bits, mem.memid)) {
 			log("no address FF found.\n");
 			return;
 		}

passes/opt/opt_expr.cc

@@ -1484,26 +1484,6 @@ skip_identity:
 			goto next_cell;
 		}
 
-		if (consume_x && mux_bool && (cell->type == ID($_MUX_) || (cell->type == ID($mux) && cell->parameters[ID::WIDTH] == 1)) && cell->getPort(ID::A) == State::S1) {
-			log_debug("Replacing %s cell `%s' in module `%s' with or-gate and not-gate.\n", log_id(cell->type), log_id(cell), log_id(module));
-			cell->setPort(ID::A, module->Not(NEW_ID2_SUFFIX("not"), cell->getPort(ID::S), false, cell->get_src_attribute()));
-			cell->unsetPort(ID::S);
-			if (cell->type == ID($mux)) {
-				Const width = cell->parameters[ID::WIDTH];
-				cell->parameters[ID::A_WIDTH] = width;
-				cell->parameters[ID::B_WIDTH] = width;
-				cell->parameters[ID::Y_WIDTH] = width;
-				cell->parameters[ID::A_SIGNED] = 0;
-				cell->parameters[ID::B_SIGNED] = 0;
-				cell->parameters.erase(ID::WIDTH);
-				cell->type = ID($or);
-			} else
-				cell->type = ID($_OR_);
-			module->rename(cell, NEW_ID2_SUFFIX("ornot"));
-			did_something = true;
-			goto next_cell;
-		}
-
 		if (consume_x && mux_bool && cell->type.in(ID($mux), ID($_MUX_)) && cell->getPort(ID::B) == State::S1) {
 			log_debug("Replacing %s cell `%s' in module `%s' with or-gate.\n", log_id(cell->type), log_id(cell), log_id(module));
 			cell->setPort(ID::B, cell->getPort(ID::S));
@@ -1523,26 +1503,6 @@ skip_identity:
 			goto next_cell;
 		}
 
-		if (consume_x && mux_bool && cell->type.in(ID($mux), ID($_MUX_)) && cell->getPort(ID::B) == State::S0) {
-			log_debug("Replacing %s cell `%s' in module `%s' with and-gate and not-gate.\n", log_id(cell->type), log_id(cell), log_id(module));
-			cell->setPort(ID::B, module->Not(NEW_ID2_SUFFIX("not"), cell->getPort(ID::S), false, cell->get_src_attribute()));
-			cell->unsetPort(ID::S);
-			if (cell->type == ID($mux)) {
-				Const width = cell->parameters[ID::WIDTH];
-				cell->parameters[ID::A_WIDTH] = width;
-				cell->parameters[ID::B_WIDTH] = width;
-				cell->parameters[ID::Y_WIDTH] = width;
-				cell->parameters[ID::A_SIGNED] = 0;
-				cell->parameters[ID::B_SIGNED] = 0;
-				cell->parameters.erase(ID::WIDTH);
-				cell->type = ID($and);
-			} else
-				cell->type = ID($_AND_);
-			module->rename(cell, NEW_ID2_SUFFIX("andnot"));
-			did_something = true;
-			goto next_cell;
-		}
-
 		if (mux_undef && cell->type.in(ID($mux), ID($pmux))) {
 			RTLIL::SigSpec new_a, new_b, new_s;
 			int width = GetSize(cell->getPort(ID::A));

passes/opt/wreduce.cc

@@ -462,7 +462,7 @@ struct WreduceWorker
 		return count;
 	}
 
-	void run_wire(Wire *w, pool<SigSpec> complete_wires)
+	void run_wire(Wire *w, const pool<SigSpec> &complete_wires)
 	{
 		int unused_top_bits = 0;
 
@@ -482,7 +482,7 @@ struct WreduceWorker
 		if (unused_top_bits == 0 || unused_top_bits == GetSize(w))
 			return;
 
-		if (complete_wires[mi.sigmap(w).extract(0, GetSize(w) - unused_top_bits)])
+		if (complete_wires.count(mi.sigmap(w).extract(0, GetSize(w) - unused_top_bits)))
 			return;
 
 		log_debug("Removed top %d bits (of %d) from wire %s.%s.\n", unused_top_bits, GetSize(w), log_id(module), log_id(w));
@@ -512,21 +512,25 @@ struct WreduceWorker
 					keep_bits.insert(bit);
 		}
 
-		while (!work_queue_cells.empty() && !work_queue_wires.empty())
+		while (!work_queue_cells.empty() || !work_queue_wires.empty())
 		{
-			// Initialize complete wires
-			pool<SigSpec> complete_wires;
-			for (auto w : module->wires())
-				complete_wires.insert(mi.sigmap(w));
-
 			// Run cells
 			work_queue_bits.clear();
 			for (auto c : work_queue_cells)
 				run_cell(c);
 
 			// Run wires
-			for (auto w : work_queue_wires)
-				run_wire(w, complete_wires);
+			if (!work_queue_wires.empty()) {
+				pool<SigSpec> complete_wires;
+				for (auto w : module->wires())
+					complete_wires.insert(mi.sigmap(w));
+				for (auto w : work_queue_wires)
+					run_wire(w, complete_wires);
+			}
+
+			// Skip reload if nothing changed
+			if (work_queue_bits.empty())
+				break;
 
 			// Get next batch of cells to process
 			work_queue_cells.clear();
@@ -541,8 +545,9 @@ struct WreduceWorker
 				if (bit.wire != NULL && module->selected(bit.wire))
 					work_queue_wires.insert(bit.wire);
 
-			// Reload module
-			mi.reload_module();
+			// Reload module only if there is more work to do
+			if (!work_queue_cells.empty() || !work_queue_wires.empty())
+				mi.reload_module();
 		}
 	}
 };

passes/sat/sat.cc

@@ -31,6 +31,22 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static SatSolver *find_satsolver(const std::string &name)
+{
+	for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
+		if (solver->name == name)
+			return solver;
+	return nullptr;
+}
+
+static std::string list_satsolvers()
+{
+	std::string result;
+	for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
+		result += result.empty() ? solver->name : ", " + solver->name;
+	return result;
+}
+
 struct SatHelper
 {
 	RTLIL::Design *design;
@@ -60,8 +76,8 @@ struct SatHelper
 	int max_timestep, timeout;
 	bool gotTimeout;
 
-	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
-		design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
+	SatHelper(RTLIL::Design *design, RTLIL::Module *module, SatSolver *solver, bool enable_undef, bool set_def_formal) :
+		design(design), module(module), sigmap(module), ct(design), ez(solver), satgen(ez.get(), &sigmap)
 	{
 		this->enable_undef = enable_undef;
 		satgen.model_undef = enable_undef;
@@ -441,7 +457,7 @@ struct SatHelper
 		log_assert(gotTimeout == false);
 		ez->setSolverTimeout(timeout);
 		bool success = ez->solve(modelExpressions, modelValues, assumptions);
-		if (ez->getSolverTimoutStatus())
+		if (ez->getSolverTimeoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -451,7 +467,7 @@ struct SatHelper
 		log_assert(gotTimeout == false);
 		ez->setSolverTimeout(timeout);
 		bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
-		if (ez->getSolverTimoutStatus())
+		if (ez->getSolverTimeoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -1066,6 +1082,10 @@ struct SatPass : public Pass {
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
 		log("\n");
+		log("    -select-solver <name>\n");
+		log("        Select SAT solver implementation for this invocation.\n");
+		log("        If not given, uses scratchpad key 'sat.solver' if set, otherwise default.\n");
+		log("\n");
 		log("    -verify\n");
 		log("        Return an error and stop the synthesis script if the proof fails.\n");
 		log("\n");
@@ -1097,8 +1117,14 @@ struct SatPass : public Pass {
 
 		log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
 
+		std::string solver_name = design->scratchpad_get_string("sat.solver", "");
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-select-solver" && argidx+1 < args.size()) {
+				solver_name = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-all") {
 				loopcount = -1;
 				continue;
@@ -1336,6 +1362,14 @@ struct SatPass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
+		SatSolver *solver = yosys_satsolver;
+		if (!solver_name.empty()) {
+			solver = find_satsolver(solver_name);
+			if (solver == nullptr)
+				log_cmd_error("Unknown SAT solver '%s'. Available solvers: %s\n",
+						solver_name, list_satsolvers());
+		}
+
 		RTLIL::Module *module = NULL;
 		for (auto mod : design->selected_modules()) {
 			if (module)
@@ -1398,13 +1432,15 @@ struct SatPass : public Pass {
 				shows.push_back(wire->name.str());
 		}
 
+		log("Using SAT solver `%s`.\n", solver->name.c_str());
+
 		if (tempinduct)
 		{
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
 
-			SatHelper basecase(design, module, enable_undef, set_def_formal);
-			SatHelper inductstep(design, module, enable_undef, set_def_formal);
+			SatHelper basecase(design, module, solver, enable_undef, set_def_formal);
+			SatHelper inductstep(design, module, solver, enable_undef, set_def_formal);
 
 			basecase.sets = sets;
 			basecase.set_assumes = set_assumes;
@@ -1593,7 +1629,7 @@ struct SatPass : public Pass {
 			if (maxsteps > 0)
 				log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
 
-			SatHelper sathelper(design, module, enable_undef, set_def_formal);
+			SatHelper sathelper(design, module, solver, enable_undef, set_def_formal);
 
 			sathelper.sets = sets;
 			sathelper.set_assumes = set_assumes;

passes/techmap/abc.cc

@@ -277,7 +277,7 @@ using AbcSigMap = SigValMap<AbcSigVal>;
 struct RunAbcState {
 	const AbcConfig &config;
 
-	std::string tempdir_name;
+	std::string per_run_tempdir_name;
 	std::vector<gate_t> signal_list;
 	bool did_run = false;
 	bool err = false;
@@ -822,16 +822,23 @@ std::string fold_abc_cmd(std::string str)
 	return new_str;
 }
 
-std::string replace_tempdir(std::string text, std::string tempdir_name, bool show_tempdir)
+std::string replace_tempdir(std::string text, std::string_view global_tempdir_name, std::string_view per_run_tempdir_name, bool show_tempdir)
 {
 	if (show_tempdir)
 		return text;
 
 	while (1) {
-		size_t pos = text.find(tempdir_name);
+		size_t pos = text.find(global_tempdir_name);
 		if (pos == std::string::npos)
 			break;
-		text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(tempdir_name));
+		text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(global_tempdir_name));
+	}
+
+	while (1) {
+		size_t pos = text.find(per_run_tempdir_name);
+		if (pos == std::string::npos)
+			break;
+		text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(per_run_tempdir_name));
 	}
 
 	std::string  selfdir_name = proc_self_dirname();
@@ -853,11 +860,12 @@ struct abc_output_filter
 	bool got_cr;
 	int escape_seq_state;
 	std::string linebuf;
-	std::string tempdir_name;
+	std::string global_tempdir_name;
+	std::string per_run_tempdir_name;
 	bool show_tempdir;
 
-	abc_output_filter(RunAbcState& state, std::string tempdir_name, bool show_tempdir)
-		: state(state), tempdir_name(tempdir_name), show_tempdir(show_tempdir)
+	abc_output_filter(RunAbcState& state, std::string global_tempdir_name, std::string per_run_tempdir_name, bool show_tempdir)
+		: state(state), global_tempdir_name(global_tempdir_name), per_run_tempdir_name(per_run_tempdir_name), show_tempdir(show_tempdir)
 	{
 		got_cr = false;
 		escape_seq_state = 0;
@@ -884,7 +892,7 @@ struct abc_output_filter
 			return;
 		}
 		if (ch == '\n') {
-			state.logs.log("ABC: %s\n", replace_tempdir(linebuf, tempdir_name, show_tempdir));
+			state.logs.log("ABC: %s\n", replace_tempdir(linebuf, global_tempdir_name, per_run_tempdir_name, show_tempdir));
 			got_cr = false, linebuf.clear();
 			return;
 		}
@@ -985,15 +993,19 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
 
 	const AbcConfig &config = run_abc.config;
 	if (config.cleanup)
-		run_abc.tempdir_name = get_base_tmpdir() + "/";
+		run_abc.per_run_tempdir_name = get_base_tmpdir() + "/";
 	else
-		run_abc.tempdir_name = "_tmp_";
-	run_abc.tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX";
-	run_abc.tempdir_name = make_temp_dir(run_abc.tempdir_name);
+		run_abc.per_run_tempdir_name = "_tmp_";
+	run_abc.per_run_tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX";
+	run_abc.per_run_tempdir_name = make_temp_dir(run_abc.per_run_tempdir_name);
 	log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n",
-			module->name.c_str(), replace_tempdir(run_abc.tempdir_name, run_abc.tempdir_name, config.show_tempdir).c_str());
+			module->name.c_str(), replace_tempdir(run_abc.per_run_tempdir_name, config.global_tempdir_name, run_abc.per_run_tempdir_name, config.show_tempdir).c_str());
 
-	std::string abc_script = stringf((std::string("read_blif") + (config.abc_node_retention ? stringf(" -M %d -r", config.abc_max_node_retention_origins) : "") + " \"%s/input.blif\"; ").c_str(), run_abc.tempdir_name);
+	std::string abc_script;
+	if (config.abc_node_retention)
+		abc_script = stringf("read_blif -M %d -r \"%s/input.blif\"; ", config.abc_max_node_retention_origins, run_abc.per_run_tempdir_name);
+	else
+		abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.per_run_tempdir_name);
 
 	if (!config.liberty_files.empty() || !config.genlib_files.empty()) {
 		std::string dont_use_args;
@@ -1059,8 +1071,8 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
 	for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
 		abc_script = abc_script.substr(0, pos) + config.lutin_shared + abc_script.substr(pos+3);
 	if (config.abc_dress)
-		abc_script += stringf("; dress \"%s/input.blif\"", run_abc.tempdir_name);
-	abc_script += stringf("; write_blif %s/output.blif", run_abc.tempdir_name);
+		abc_script += stringf("; dress \"%s/input.blif\"", run_abc.per_run_tempdir_name);
+	abc_script += stringf("; write_blif %s/output.blif", run_abc.per_run_tempdir_name);
 	abc_script = add_echos_to_abc_cmd(abc_script);
 #if defined(__linux__) && !defined(YOSYS_DISABLE_SPAWN)
 	abc_script += "; echo; echo \"YOSYS_ABC_DONE\"\n";
@@ -1070,7 +1082,7 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
 		if (abc_script[i] == ';' && abc_script[i+1] == ' ')
 			abc_script[i+1] = '\n';
 
-	std::string buffer = stringf("%s/abc.script", run_abc.tempdir_name);
+	std::string buffer = stringf("%s/abc.script", run_abc.per_run_tempdir_name);
 	FILE *f = fopen(buffer.c_str(), "wt");
 	if (f == nullptr)
 		log_error("Opening %s for writing failed: %s\n", buffer, strerror(errno));
@@ -1167,7 +1179,7 @@ bool read_until_abc_done(abc_output_filter &filt, int fd, DeferredLogs &logs) {
 
 void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
 {
-	std::string buffer = stringf("%s/input.blif", tempdir_name);
+	std::string buffer = stringf("%s/input.blif", per_run_tempdir_name);
 	FILE *f = fopen(buffer.c_str(), "wt");
 	if (f == nullptr) {
 		logs.log("Opening %s for writing failed: %s\n", buffer, strerror(errno));
@@ -1292,13 +1304,13 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
 			count_gates, GetSize(signal_list), count_input, count_output);
 	if (count_output > 0)
 	{
-		std::string tmp_script_name = stringf("%s/abc.script", tempdir_name);
-		logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, tempdir_name, config.show_tempdir));
+		std::string tmp_script_name = stringf("%s/abc.script", per_run_tempdir_name);
+		logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir));
 
 		errno = 0;
-		abc_output_filter filt(*this, tempdir_name, config.show_tempdir);
+		abc_output_filter filt(*this, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir);
 #ifdef YOSYS_LINK_ABC
-		string temp_stdouterr_name = stringf("%s/stdouterr.txt", tempdir_name);
+		string temp_stdouterr_name = stringf("%s/stdouterr.txt", per_run_tempdir_name);
 		FILE *temp_stdouterr_w = fopen(temp_stdouterr_name.c_str(), "w");
 		if (temp_stdouterr_w == NULL)
 			log_error("ABC: cannot open a temporary file for output redirection");
@@ -1360,7 +1372,7 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
 			process_pool.push_back(std::move(process));
 		}
 #else
-		std::string cmd = stringf("\"%s\" -s -f %s/abc.script 2>&1", config.exe_file.c_str(), tempdir_name.c_str());
+		std::string cmd = stringf("\"%s\" -s -f %s/abc.script 2>&1", config.exe_file.c_str(), per_run_tempdir_name.c_str());
 		int ret = run_command(cmd, std::bind(&abc_output_filter::next_line, filt, std::placeholders::_1));
 #endif
 		if (ret != 0) {
@@ -1442,7 +1454,7 @@ void AbcModuleState::extract(AbcSigMap &assign_map, dict<SigSpec, std::string> &
 		return;
 	}
 
-	std::string buffer = stringf("%s/%s", run_abc.tempdir_name, "output.blif");
+	std::string buffer = stringf("%s/%s", run_abc.per_run_tempdir_name, "output.blif");
 	std::ifstream ifs;
 	ifs.open(buffer);
 	if (ifs.fail())
@@ -1485,7 +1497,7 @@ void AbcModuleState::extract(AbcSigMap &assign_map, dict<SigSpec, std::string> &
 			}
 			wire->add_strpool_attribute(ID::src, src_pool);
 		} else if (run_abc.config.abc_node_retention) {
-			log_error("No node retention sources found for wire %s\n", w->name.c_str());
+			log_warning("No node retention sources found for wire %s\n", w->name.c_str());
 		}
 
 		if (markgroups) wire->attributes[ID::abcgroup] = map_autoidx;
@@ -1797,7 +1809,7 @@ void AbcModuleState::finish()
 	if (run_abc.config.cleanup)
 	{
 		log("Removing temp directory.\n");
-		remove_directory(run_abc.tempdir_name);
+		remove_directory(run_abc.per_run_tempdir_name);
 	}
 	log_pop();
 }

passes/techmap/abc9.cc

@@ -219,9 +219,7 @@ struct Abc9Pass : public ScriptPass
 		for (argidx = 1; argidx < args.size(); argidx++) {
 			std::string arg = args[argidx];
 			if ((arg == "-exe" || arg == "-script" || arg == "-D" ||
-						/*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" ||
-						/*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" ||
-						arg == "-constr" || arg == "-dont_use" || arg == "-liberty") &&
+						arg == "-lut" || arg == "-luts" || arg == "-W") &&
 					argidx+1 < args.size()) {
 				if (arg == "-lut" || arg == "-luts")
 					lut_mode = true;

passes/techmap/clockgate.cc

@@ -421,6 +421,14 @@ struct ClockgatePass : public Pass {
 				log("Found new_net for %s\n", cell->name);
 				if (!it->second.new_net)
 					continue;
+				
+				// Accumulate src attributes from all FFs sharing this ICG
+				if (max_src < 0 || it->second.src_count < max_src) {
+					it->second.icg_cell->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+					if (it->second.ce_not_cell)
+						it->second.ce_not_cell->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+					it->second.src_count++;
+				}
 
 				// Accumulate src attributes from all FFs sharing this ICG
 				if (max_src < 0 || it->second.src_count < max_src) {

techlibs/gowin/Makefile.inc

@@ -12,3 +12,4 @@ $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams_map_gw5a.v))
 $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams.txt))
 $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams_map.v))
 $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams.txt))
+$(eval $(call add_share_file,share/gowin,techlibs/gowin/dsp_map.v))

techlibs/gowin/dsp_map.v

@@ -0,0 +1,70 @@
+module \$__MUL9X9 (input [8:0] A, input [8:0] B, output [17:0] Y);
+
+    parameter A_WIDTH = 9;
+    parameter B_WIDTH = 9;
+    parameter Y_WIDTH = 18;
+    parameter A_SIGNED = 0;
+    parameter B_SIGNED = 0;
+
+	MULT9X9 __TECHMAP_REPLACE__ (
+		.CLK(1'b0),
+		.CE(1'b0),
+		.RESET(1'b0),
+		.A(A),
+		.SIA({A_WIDTH{1'b0}}),
+		.ASEL(1'b0),
+		.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
+		.B(B),
+		.SIB({B_WIDTH{1'b0}}),
+		.BSEL(1'b0),
+		.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
+		.DOUT(Y)
+	);
+
+endmodule
+
+module \$__MUL18X18 (input [17:0] A, input [17:0] B, output [35:0] Y);
+
+    parameter A_WIDTH = 18;
+    parameter B_WIDTH = 18;
+    parameter Y_WIDTH = 36;
+    parameter A_SIGNED = 0;
+    parameter B_SIGNED = 0;
+
+	MULT18X18 __TECHMAP_REPLACE__ (
+		.CLK(1'b0),
+		.CE(1'b0),
+		.RESET(1'b0),
+		.A(A),
+		.SIA({A_WIDTH{1'b0}}),
+		.ASEL(1'b0),
+		.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
+		.B(B),
+		.SIB({B_WIDTH{1'b0}}),
+		.BSEL(1'b0),
+		.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
+		.DOUT(Y)
+	);
+
+endmodule
+
+module \$__MUL36X36 (input [35:0] A, input [35:0] B, output [71:0] Y);
+
+    parameter A_WIDTH = 36;
+    parameter B_WIDTH = 36;
+    parameter Y_WIDTH = 72;
+    parameter A_SIGNED = 0;
+    parameter B_SIGNED = 0;
+
+	MULT36X36 __TECHMAP_REPLACE__ (
+		.CLK(1'b0),
+		.RESET(1'b0),
+		.CE(1'b0),
+		.A(A),
+		.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
+		.B(B),
+		.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
+		.DOUT(Y)
+	);
+
+endmodule

techlibs/gowin/synth_gowin.cc

@@ -29,6 +29,21 @@ struct SynthGowinPass : public ScriptPass
 {
 	SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { }
 
+	struct DSPRule {
+		int a_maxwidth;
+		int b_maxwidth;
+		int a_minwidth;
+		int b_minwidth;
+		std::string prim;
+	};
+
+	const std::vector<DSPRule> dsp_rules = {
+		{36, 36, 22, 22, "$__MUL36X36"},
+		{18, 18, 10, 4, "$__MUL18X18"},
+		{18, 18, 4, 10, "$__MUL18X18"},
+		{9, 9, 4, 4, "$__MUL9X9"},
+	};
+
 	void help() override
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -97,13 +112,16 @@ struct SynthGowinPass : public ScriptPass
 		log("    -setundef\n");
 		log("        set undriven wires and parameters to zero\n");
 		log("\n");
+		log("    -nodsp\n");
+		log("        do not infer DSP multipliers\n");
+		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
 		help_script();
 		log("\n");
 	}
 
 	string top_opt, vout_file, json_file, family;
-	bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef;
+	bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef, nodsp;
 
 	void clear_flags() override
 	{
@@ -123,6 +141,7 @@ struct SynthGowinPass : public ScriptPass
 		noalu = false;
 		no_rw_check = false;
 		setundef = false;
+		nodsp = false;
 	}
 
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
@@ -209,6 +228,10 @@ struct SynthGowinPass : public ScriptPass
 				setundef = true;
 				continue;
 			}
+			if (args[argidx] == "-nodsp") {
+				nodsp = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -239,17 +262,40 @@ struct SynthGowinPass : public ScriptPass
 			run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt));
 		}
 
-		if (flatten && check_label("flatten", "(unless -noflatten)"))
-		{
-			run("proc");
-			run("flatten");
-			run("tribuf -logic");
-			run("deminout");
-		}
-
 		if (check_label("coarse"))
 		{
-			run("synth -run coarse" + no_rw_check_opt);
+			run("proc");
+			if (flatten || help_mode)
+				run("flatten", "(unless -noflatten)");
+			run("tribuf -logic");
+			run("deminout");
+			run("opt_expr");
+			run("opt_clean");
+			run("check");
+			run("opt -nodffe -nosdff");
+			run("fsm");
+			run("opt");
+			run("wreduce");
+			run("peepopt");
+			run("opt_clean");
+			run("share");
+
+			if (help_mode) {
+				run("techmap -map +/mul2dsp.v [...]", "(unless -nodsp and if -family gw1n or gw2a)");
+				run("techmap -map +/gowin/dsp_map.v", "(unless -nodsp and if -family gw1n or gw2a)");
+			} else if (!nodsp && (family == "gw1n" || family == "gw2a")) {
+				for (const auto &rule : dsp_rules) {
+					run(stringf("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=%d -D DSP_B_MAXWIDTH=%d -D DSP_A_MINWIDTH=%d -D DSP_B_MINWIDTH=%d -D DSP_NAME=%s",
+						rule.a_maxwidth, rule.b_maxwidth, rule.a_minwidth, rule.b_minwidth, rule.prim));
+					run("chtype -set $mul t:$__soft_mul");
+				}
+				run("techmap -map +/gowin/dsp_map.v");
+			}
+
+			run("alumacc");
+			run("opt");
+			run("memory -nomap" + no_rw_check_opt);
+			run("opt_clean");
 		}
 
 		if (check_label("map_ram"))

techlibs/xilinx/xilinx_dsp.cc

@@ -263,6 +263,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
 	log("Analysing %s.%s for Xilinx DSP packing.\n", log_id(pm.module), log_id(st.dsp));
 
 	log_debug("preAdd:     %s\n", log_id(st.preAdd, "--"));
+	log_debug("preSub:     %s\n", log_id(st.preSub, "--"));
 	log_debug("ffAD:       %s\n", log_id(st.ffAD, "--"));
 	log_debug("ffA2:       %s\n", log_id(st.ffA2, "--"));
 	log_debug("ffA1:       %s\n", log_id(st.ffA1, "--"));
@@ -278,17 +279,22 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
 
 	Cell *cell = st.dsp;
 
-	if (st.preAdd) {
-		log("  preadder %s (%s)\n", log_id(st.preAdd), log_id(st.preAdd->type));
-		bool A_SIGNED = st.preAdd->getParam(ID::A_SIGNED).as_bool();
-		bool D_SIGNED = st.preAdd->getParam(ID::B_SIGNED).as_bool();
-		if (st.sigA == st.preAdd->getPort(ID::B))
+	if (st.preAdd || st.preSub) {
+		Cell* preAdder = st.preAdd ? st.preAdd : st.preSub;
+
+		log("  preadder %s (%s)\n", log_id(preAdder), log_id(preAdder->type));
+		bool A_SIGNED = preAdder->getParam(ID::A_SIGNED).as_bool();
+		bool D_SIGNED = preAdder->getParam(ID::B_SIGNED).as_bool();
+		if (st.sigA == preAdder->getPort(ID::B))
 			std::swap(A_SIGNED, D_SIGNED);
 		st.sigA.extend_u0(30, A_SIGNED);
 		st.sigD.extend_u0(25, D_SIGNED);
 		cell->setPort(ID::A, st.sigA);
 		cell->setPort(ID::D, st.sigD);
-		cell->setPort(ID(INMODE), Const::from_string("00100"));
+		if (preAdder->type == ID($add))
+			cell->setPort(ID(INMODE), Const::from_string("00100"));
+		else
+			cell->setPort(ID(INMODE), Const::from_string("01100"));
 
 		if (st.ffAD) {
 			if (st.ffAD->type.in(ID($dffe), ID($sdffe))) {
@@ -303,7 +309,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
 
 		cell->setParam(ID(USE_DPORT), Const("TRUE"));
 
-		pm.autoremove(st.preAdd);
+		pm.autoremove(preAdder);
 	}
 	if (st.postAdd) {
 		log("  postadder %s (%s)\n", log_id(st.postAdd), log_id(st.postAdd->type));

techlibs/xilinx/xilinx_dsp.pmg

@@ -6,6 +6,8 @@
 //        If ADREG matched, treat 'A' input as input of ADREG
 //   ( 3) Match the driver of the 'A' and 'D' inputs for a possible $add cell
 //       (pre-adder)
+// 	 (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell
+//         (pre-adder)
 //   ( 4) If pre-adder was present, find match 'A' input for A2REG
 //        If pre-adder was not present, move ADREG to A2REG
 //        If A2REG, then match 'A' input for A1REG
@@ -152,13 +154,41 @@ code sigA sigD
 	}
 endcode
 
+// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell
+//     (pre-adder)
+match preSub
+	if sigD.empty() || sigD.is_fully_zero()
+	// Ensure that preAdder not already used
+	if param(dsp, \USE_DPORT).decode_string() == "FALSE"
+	if port(dsp, \INMODE, Const(0, 5)).is_fully_zero()
+
+	select preSub->type.in($sub)
+	// Output has to be 25 bits or less
+	select GetSize(port(preSub, \Y)) <= 25
+	select nusers(port(preSub, \Y)) == 2
+	// D port has to be 25 bits or less
+	select GetSize(port(preSub, \A)) <= 25
+	// A port has to be 30 bits or less
+	select GetSize(port(preSub, \B)) <= 30
+	index <SigSpec> port(preSub, \Y) === sigA
+
+	optional
+endmatch
+
+code sigA sigD
+	if (preSub) {
+		sigD = port(preSub, \A);
+		sigA = port(preSub, \B);
+	}
+endcode
+
 // (4) If pre-adder was present, find match 'A' input for A2REG
 //     If pre-adder was not present, move ADREG to A2REG
 //     Then match 'A' input for A1REG
 code argQ ffAD sigA clock ffA2 ffA1
 	// Only search for ffA2 if there was a pre-adder
 	//   (otherwise ffA2 would have been matched as ffAD)
-	if (preAdd) {
+	if (preAdd || preSub) {
 		if (param(dsp, \AREG).as_int() == 0) {
 			argQ = sigA;
 			subpattern(in_dffe);

tests/arch/gowin/mul_gw1n.ys

@@ -0,0 +1,53 @@
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+# equivalence checking is somewhat slow (and missing simulation models)
+synth_gowin -family gw1n
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT9X9
+
+
+# Make sure that DSPs are not inferred with -nodsp option
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+synth_gowin -family gw1n -nodsp
+cd top # Constrain all select calls below inside the top module
+select -assert-none t:MULT9X9
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
+hierarchy -top top
+proc
+synth_gowin -family gw1n
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT18X18
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT36X36
+
+
+# We end up with two 18x18 multipliers
+# 36x36 min width is 22
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin
+cd top # Constrain all select calls below inside the top module
+select -assert-count 2 t:MULT18X18

tests/arch/gowin/mul_gw2a.ys

@@ -0,0 +1,53 @@
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+# equivalence checking is somewhat slow (and missing simulation models)
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT9X9
+
+
+# Make sure that DSPs are not inferred with -nodsp option
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+synth_gowin -family gw2a -nodsp
+cd top # Constrain all select calls below inside the top module
+select -assert-none t:MULT9X9
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
+hierarchy -top top
+proc
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT18X18
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT36X36
+
+
+# We end up with two 18x18 multipliers
+# 36x36 min width is 22
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 2 t:MULT18X18

tests/arch/xilinx/dsp_preadder_sub.ys

@@ -0,0 +1,29 @@
+read_verilog <<EOT
+module top(
+	input  signed [7:0] A,
+	input  signed [7:0] D,
+	input  signed [7:0] B,
+	output signed [16:0] P
+);
+	assign P = (A - D) * B;
+endmodule
+EOT
+
+proc
+design -save gold
+synth_xilinx -noiopad
+design -save gate
+cd top
+select -assert-count 1 t:DSP48E1
+select -assert-count 1 t:DSP48E1 r:USE_DPORT=TRUE %i
+select -assert-none t:DSP48E1 %% t:* %D
+
+# Now prove functional equivalence of the mapped netlist against the original
+# (saved as `gold` above).
+design -reset
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+techmap -wb -D EQUIV -autoproc -map +/xilinx/cells_sim.v
+equiv_make gold gate equiv
+equiv_induct equiv
+equiv_status -assert equiv

tests/memlib/generate.py

@@ -1428,7 +1428,7 @@ endmodule
 for (testname, 		reset_gate, 	rdwr,  clk_en, add_logic) in [
 	("no_reset", 	"", 		"old", False, 	0),
 	("gclken", 	"rst", 		"old", False, 	0),
-	("ungated", 	"ungated", 	"old", False, 	2), # muxes wren with rst
+	("ungated", 	"ungated", 	"old", False, 	1), # muxes wren with rst
 	("gclken_ce", 	"rst", 		"old", True, 	3), # AND to simulate CLK_EN
 	("grden", 	"rden && rst", 	"old", False, 	1), # selects _clken, simulates _rden
 	("grden_ce", 	"rden && rst", 	"old", True, 	4), # both of the above
@@ -1473,9 +1473,9 @@ end"""
 for (testname, 			reset_gate, 	defs, 		rdwr,  add_logic) in [
 	("wr_byte",		"", 	["USE_SRST_BLOCKING"],	"old", 0),
 	("trans_byte",		"", 	["USE_SRST_BLOCKING"],	"new", 0),
-	("wr_rst_byte",		"rst", 	["USE_SRST"],		"old", 3), # expected mux to emulate blocking
-	("rst_wr_byte",		"rst", 	["USE_SRST_BLOCKING"],	"old", 3), # should use hardware blocking, doesn't
-	("rdenrst_wr_byte", 	"rden && rst", ["USE_SRST"],	"old", 4),
+	("wr_rst_byte",		"rst", 	["USE_SRST"],		"old", 2), # expected mux to emulate blocking
+	("rst_wr_byte",		"rst", 	["USE_SRST_BLOCKING"],	"old", 2), # should use hardware blocking, doesn't
+	("rdenrst_wr_byte", 	"rden && rst", ["USE_SRST"],	"old", 3),
 ]:
 	wordsloop = "for (i=0; i<WORDS; i=i+1)"
 	if rdwr == "old":

tests/silimate/mux_andnot.ys

@@ -1,222 +0,0 @@
-log -header "Simple positive case"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? 1'b0 : a;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$and
-select -assert-count 1 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "Case with inverted a"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? 1'b0 : ~a;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$and
-select -assert-count 2 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "Case with inverted s"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = ~s ? a : 1'b0;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-# Did not include check for not count since we have an unassigned ~s wire
-design -load postopt
-select -assert-count 1 t:$and
-
-design -reset
-log -pop
-
-
-
-log -header "Nested AND gates"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire b,
-  input wire s,
-  output wire x
-);
-  assign x = s ? 1'b0 : a & b;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 2 t:$and
-select -assert-count 1 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "Nested OR gates"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire b,
-  input wire s,
-  output wire x
-);
-  assign x = s ? 1'b0 : a | b;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$and
-select -assert-count 1 t:$not
-select -assert-count 1 t:$or
-
-design -reset
-log -pop
-
-
-
-log -header "Nested muxes"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s1,
-  input wire s2,
-  output wire x
-);
-  assign x = s1 ? 1'b0 : (s2 ? 1'b0 : a);
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 2 t:$and
-select -assert-count 2 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "With constant propagation"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? 1'b0 : a & 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$and
-select -assert-count 1 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "With multibit constant"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? 32'b0 : a;
-endmodule
-EOF
-check -assert
-
-# Runs wreduce to reduce width of the constant before applying opt_expr
-# Without this line, this test case will not pass
-# Believe it is intended behavior to not optimize constant with more than one bit
-wreduce
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$and
-select -assert-count 1 t:$not
-
-design -reset
-log -pop

tests/silimate/mux_ornot.ys

@@ -1,222 +0,0 @@
-log -header "Simple positive case"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? a : 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$or
-select -assert-count 1 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "Case with inverted a"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? ~a : 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$or
-select -assert-count 2 t:$not
-
-design -reset
-log -pop
-
-
-
-log -header "Case with inverted s"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = ~s ? 1'b1 : a;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-# Did not include check for not count since we have an unassigned ~s wire
-design -load postopt
-select -assert-count 1 t:$or
-
-design -reset
-log -pop
-
-
-
-log -header "Nested AND gates"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire b,
-  input wire s,
-  output wire x
-);
-  assign x = s ? a & b : 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$and
-select -assert-count 1 t:$not
-select -assert-count 1 t:$or
-
-design -reset
-log -pop
-
-
-
-log -header "Nested OR gates"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire b,
-  input wire s,
-  output wire x
-);
-  assign x = s ? a | b : 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$not
-select -assert-count 2 t:$or
-
-design -reset
-log -pop
-
-
-
-log -header "Nested muxes"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s1,
-  input wire s2,
-  output wire x
-);
-  assign x = s1 ? (s2 ? a : 1'b1) : 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 2 t:$not
-select -assert-count 2 t:$or
-
-design -reset
-log -pop
-
-
-
-log -header "With constant propagation"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? a & 1'b1 : 1'b1;
-endmodule
-EOF
-check -assert
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$not
-select -assert-count 1 t:$or
-
-design -reset
-log -pop
-
-
-
-log -header "With multibit constant"
-log -push
-design -reset
-read_verilog <<EOF
-module top (
-  input wire a,
-  input wire s,
-  output wire x
-);
-  assign x = s ? a : 32'b1;
-endmodule
-EOF
-check -assert
-
-# Runs wreduce to reduce width of the constant before applying opt_expr
-# Without this line, this test case will not pass
-# Believe it is intended behavior to not optimize constant with more than one bit
-wreduce
-
-# Check equivalence after opt_expr
-equiv_opt -assert opt_expr -mux_bool
-
-# Check final design has correct number of gates
-design -load postopt
-select -assert-count 1 t:$not
-select -assert-count 1 t:$or
-
-design -reset
-log -pop

tests/techmap/abc_temp_dir_sanitization.ys

@@ -0,0 +1,13 @@
+read_verilog <<EOT
+module simple(I1, I2, O);
+	input wire I1;
+	input wire I2;
+	output wire O;
+
+	assign O = I1 | I2;
+endmodule
+EOT
+techmap
+
+logger -warn " /tmp/" -werror " /tmp/"
+abc -g all

tests/unit/Makefile

@@ -16,12 +16,14 @@ else
   RPATH = -Wl,-rpath=$(ROOTPATH)
 endif
 
-EXTRAFLAGS := -lyosys -pthread
+PYTHON_CONFIG := $(shell if python3-config --embed --libs > /dev/null 2>&1; then echo "python3-config --embed"; else echo "python3-config"; fi)
+EXTRAFLAGS := -lyosys -pthread $(shell $(PYTHON_CONFIG) --ldflags --libs)
 
-OBJTEST := objtest
-BINTEST := bintest
+MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
+OBJTEST := $(MAKEFILE_DIR)objtest
+BINTEST := $(MAKEFILE_DIR)bintest
 
-ALLTESTFILE := $(shell find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ')
+ALLTESTFILE := $(shell cd $(MAKEFILE_DIR) && find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ')
 TESTDIRS := $(sort $(dir $(ALLTESTFILE)))
 TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o)))
 
@@ -34,7 +36,7 @@ $(BINTEST)/%: $(OBJTEST)/%.o | prepare
 	$(CXX) -L$(ROOTPATH) $(RPATH) $(LINKFLAGS) -o $@ $^ $(LIBS) \
 		$(GTEST_LDFLAGS) $(EXTRAFLAGS)
 
-$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc | prepare
+$(OBJTEST)/%.o: $(MAKEFILE_DIR)/%.cc | prepare
 	$(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $(GTEST_CXXFLAGS) $^
 
 .PHONY: prepare run-tests clean

tests/various/.gitignore

@@ -7,6 +7,8 @@
 /plugin.so
 /plugin_search
 /plugin.so.dSYM
+/ezcmdline_plugin.so
+/ezcmdline_plugin.so.dSYM
 /temp
 /smtlib2_module.smt2
 /smtlib2_module-filtered.smt2

tests/various/ezcmdline_dummy_solver

@@ -0,0 +1,61 @@
+#!/bin/sh
+# Dummy SAT solver for ezCmdlineSAT tests.
+# Accepts exactly two CNF shapes:
+#  - SAT:   p cnf 1 1; clause: "1 0"  -> exits 10 with v 1
+#  - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20
+set -e
+
+if [ "$#" -ne 1 ]; then
+	echo "usage: $0 <cnf>" >&2
+	exit 1
+fi
+
+awk '
+BEGIN {
+	vars = 0;
+	clauses = 0;
+	clause_count = 0;
+	clause_data = "";
+	current = "";
+}
+$1 == "c" {
+	next;
+}
+$1 == "p" && $2 == "cnf" {
+	vars = $3;
+	clauses = $4;
+	next;
+}
+{
+	for (i = 1; i <= NF; i++) {
+		lit = $i;
+		if (lit == 0) {
+			clause_count++;
+			if (clause_data != "")
+				clause_data = clause_data ";" current;
+			else
+				clause_data = current;
+			current = "";
+		} else {
+			if (current == "")
+				current = lit;
+			else
+				current = current "," lit;
+		}
+	}
+}
+END {
+	if (vars == 1 && clause_count == 1 && clause_data == "1") {
+		print "s SATISFIABLE";
+		print "v 1 0";
+		exit 10;
+	}
+	if (vars == 1 && clause_count == 2 && clause_data == "1;-1") {
+		print "s UNSATISFIABLE";
+		exit 20;
+	}
+	print "c unexpected CNF for dummy solver";
+	print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data;
+	exit 1;
+}
+' "$1"

tests/various/ezcmdline_plugin.cc

@@ -0,0 +1,53 @@
+#include "kernel/yosys.h"
+#include "libs/ezsat/ezcmdline.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EzCmdlineTestPass : public Pass {
+	EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { }
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		std::string cmd;
+		size_t argidx = 1;
+
+		while (argidx < args.size()) {
+			if (args[argidx] == "-cmd" && argidx + 1 < args.size()) {
+				cmd = args[argidx + 1];
+				argidx += 2;
+				continue;
+			}
+			break;
+		}
+
+		extra_args(args, argidx, design);
+
+		if (cmd.empty())
+			log_error("Missing -cmd <solver> argument.\n");
+
+		ezCmdlineSAT sat(cmd);
+		sat.non_incremental();
+
+		// assume("A") adds a permanent CNF clause "A".
+		sat.assume(sat.VAR("A"));
+
+		std::vector<int> model_expressions;
+		std::vector<bool> model_values;
+		model_expressions.push_back(sat.VAR("A"));
+
+		// Expect SAT with A=true.
+		if (!sat.solve(model_expressions, model_values))
+			log_error("ezCmdlineSAT SAT case failed.\n");
+		if (model_values.size() != 1 || !model_values[0])
+			log_error("ezCmdlineSAT SAT model mismatch.\n");
+
+		// Passing NOT("A") here adds a temporary unit clause for this solve call,
+		// so the solver sees A && !A and must return UNSAT.
+		if (sat.solve(model_expressions, model_values, sat.NOT("A")))
+			log_error("ezCmdlineSAT UNSAT case failed.\n");
+
+		log("ezcmdline_test passed!\n");
+	}
+} EzCmdlineTestPass;
+
+PRIVATE_NAMESPACE_END

tests/various/ezcmdline_plugin.sh

@@ -0,0 +1,12 @@
+set -e
+
+DIR=$(cd "$(dirname "$0")" && pwd)
+BASEDIR=$(cd "$DIR/../.." && pwd)
+rm -f "$DIR/ezcmdline_plugin.so"
+chmod +x "$DIR/ezcmdline_dummy_solver"
+CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags)
+DATDIR=$("$BASEDIR/yosys-config" --datdir)
+DATDIR=${DATDIR//\//\\\/}
+CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share}
+"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc"
+"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!"

tests/various/json_param_defaults.v

@@ -0,0 +1,10 @@
+module json_param_defaults #(
+	parameter WIDTH = 8,
+	parameter SIGNED = 1
+) (
+	input  [WIDTH-1:0] a,
+	output [WIDTH-1:0] y
+);
+	wire [WIDTH-1:0] y_int = a << SIGNED;
+	assign y = y_int;
+endmodule

tests/various/json_param_defaults.ys

@@ -0,0 +1,8 @@
+! mkdir -p temp
+read_verilog -sv json_param_defaults.v
+write_json temp/json_param_defaults.json
+design -reset
+read_json temp/json_param_defaults.json
+write_verilog -noattr -defaultparams temp/json_param_defaults.v
+! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v
+! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v

tests/verific/README.md

@@ -2,6 +2,8 @@
 
 ## Disabled
 
+- `import_warning_operator`: no VHDL
+- `mixed_flist`: no VHDL
 - `memory_semantics`: relies on initial values being retained, which we do not want
 - `rom_case`: we need different behavior for multi-port memories
 - `blackbox*`: we need different behavior for parametrized blackboxes

tests/verific/import_warning_operator.ys

@@ -1,5 +0,0 @@
-logger -expect warning "import_warning_operator.vhd:[0-9]+.[0-9]+-[0-9]+.[0-9]+: Unsupported Verific operator: nor_4 \(fallback to gate level implementation provided by verific\)" 1
-verific -vhdl import_warning_operator.vhd
-verific -import top
-logger -check-expected
-design -reset

verific

@@ -1 +1 @@
-Subproject commit 01ad443c3fff2a92c9473b69291ac32ef788683a
+Subproject commit 4feaf1f923157af0ed064eab8e302647bd5fa1b7