Merge branch 'YosysHQ:main' into master

Author: eder-matheus

Diff for: CHANGELOG

@@ -2,9 +2,26 @@
 List of major changes and improvements between releases
 =======================================================
 
-Yosys 0.50 .. Yosys 0.51-dev
+Yosys 0.51 .. Yosys 0.52-dev
 --------------------------
 
+Yosys 0.50 .. Yosys 0.51
+--------------------------
+ * New commands and options
+    - Added "abstract" pass to allow reducing and never increasing
+      the constraints on a circuit's behavior in a formal verification setting.
+
+ * Various
+    - "splitcells" pass now splits "aldff" cells.
+    - FunctionalIR documentation
+
+ * QuickLogic support
+    - Added IOFF inference for qlf_k6n10f
+
+ * Intel support
+    - Fixed RAM and DSP support.
+    - Overall performance improvement for "synth_intel".
+
 Yosys 0.49 .. Yosys 0.50
 --------------------------
  * Various

Diff for: CONTRIBUTING.md

@@ -0,0 +1,73 @@
+# Introduction
+
+Thanks for thinking about contributing to the Yosys project.  If this is your
+first time contributing to an open source project, please take a look at the
+following guide:
+https://opensource.guide/how-to-contribute/#orienting-yourself-to-a-new-project.
+
+Information about the Yosys coding style is available on our Read the Docs:
+https://yosys.readthedocs.io/en/latest/yosys_internals/extending_yosys/contributing.html.
+
+# Using the issue tracker
+
+The [issue tracker](https://github.com/YosysHQ/yosys/issues) is used for
+tracking bugs or other problems with Yosys or its documentation.  It is also the
+place to go for requesting new features.
+When [creating a new issue](https://github.com/YosysHQ/yosys/issues/new/choose),
+we have a few templates available.  Please make use of these!  It will make it
+much easier for someone to respond and help.
+
+### Bug reports
+
+Before you submit an issue, please have a search of the existing issues in case
+one already exists.  Making sure that you have a minimal, complete and
+verifiable example (MVCE) is a great way to quickly check an existing issue
+against a new one.  Stack overflow has a guide on [how to create an
+MVCE](https://stackoverflow.com/help/minimal-reproducible-example).  The
+[`bugpoint`
+command](https://yosyshq.readthedocs.io/projects/yosys/en/latest/cmd/bugpoint.html)
+in Yosys can be helpful for this process.
+
+
+# Using pull requests
+
+If you are working on something to add to Yosys, or fix something that isn't
+working quite right, make a [PR](https://github.com/YosysHQ/yosys/pulls)!  An
+open PR, even as a draft, tells everyone that you're working on it and they
+don't have to.  It can also be a useful way to solicit feedback on in-progress
+changes.  See below to find the best way to [ask us
+questions](#asking-questions).
+
+In general, all changes to the code are done as a PR, with [Continuous
+Integration (CI)](https://github.com/YosysHQ/yosys/actions) tools that
+automatically run the full suite of tests compiling and running Yosys.  Please
+make use of this!  If you're adding a feature: add a test!  Not only does it
+verify that your feature is working as expected, but it can also be a handy way
+for people to see how the feature is used.  If you're fixing a bug: add a test!
+If you can, do this first; it's okay if the test starts off failing - you
+already know there is a bug.  CI also helps to make sure that your changes still
+work under a range of compilers, settings, and targets.
+
+
+### Labels
+
+We use [labels](https://github.com/YosysHQ/yosys/labels) to help categorise
+issues and PRs.  If a label seems relevant to your work, please do add it; this
+also includes the labels beggining with 'status-'.  The 'merge-' labels are used
+by maintainers for tracking and communicating which PRs are ready and pending
+merge; please do not use these labels if you are not a maintainer.
+
+
+# Asking questions
+
+If you have a question about how to use Yosys, please ask on our [discussions
+page](https://github.com/YosysHQ/yosys/discussions) or in our [community
+slack](https://join.slack.com/t/yosyshq/shared_invite/zt-1aopkns2q-EiQ97BeQDt_pwvE41sGSuA).
+The slack is also a great place to ask questions about developing or
+contributing to Yosys.
+
+We have open dev 'jour fixe' (JF) meetings where developers from YosysHQ and the
+community come together to discuss open issues and PRs.  This is also a good
+place to talk to us about how to implement larger PRs.  Please join the
+community slack if you would like to join the next meeting, the link is
+available in the description of the #devel-discuss channel.

Diff for: Makefile

@@ -123,8 +123,8 @@ ifneq ($(shell :; command -v brew),)
 BREW_PREFIX := $(shell brew --prefix)/opt
 $(info $$BREW_PREFIX is [${BREW_PREFIX}])
 ifeq ($(ENABLE_PYOSYS),1)
-CXXFLAGS += -I$(BREW_PREFIX)/boost/include/boost
-LINKFLAGS += -L$(BREW_PREFIX)/boost/lib
+CXXFLAGS += -I$(BREW_PREFIX)/boost/include
+LINKFLAGS += -L$(BREW_PREFIX)/boost/lib -L$(BREW_PREFIX)/boost-python3/lib
 endif
 CXXFLAGS += -I$(BREW_PREFIX)/readline/include
 LINKFLAGS += -L$(BREW_PREFIX)/readline/lib
@@ -153,7 +153,14 @@ ifeq ($(OS), Haiku)
 CXXFLAGS += -D_DEFAULT_SOURCE
 endif
 
-YOSYS_VER := 0.50+0
+YOSYS_VER := 0.51+0
+YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
+YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1)
+YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2)
+CXXFLAGS += -DYOSYS_VER=\\"$(YOSYS_VER)\\" \
+			-DYOSYS_MAJOR=$(YOSYS_MAJOR) \
+			-DYOSYS_MINOR=$(YOSYS_MINOR) \
+			-DYOSYS_COMMIT=$(YOSYS_COMMIT)
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -169,7 +176,7 @@ endif
 OBJS = kernel/version_$(GIT_REV).o
 
 bumpversion:
-	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline b5170e1.. | wc -l`/;" Makefile
+	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline c4b5190.. | wc -l`/;" Makefile
 
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q)
 
@@ -330,8 +337,13 @@ TARGETS += libyosys.so
 endif
 
 ifeq ($(ENABLE_PYOSYS),1)
+# python-config --ldflags includes -l and -L, but LINKFLAGS is only -L
+LINKFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags))
+LIBS += $(shell $(PYTHON_CONFIG) --libs)
+CXXFLAGS += $(shell $(PYTHON_CONFIG) --includes) -DWITH_PYTHON
+
 # Detect name of boost_python library. Some distros use boost_python-py<version>, other boost_python<version>, some only use the major version number, some a concatenation of major and minor version numbers
-CHECK_BOOST_PYTHON = (echo "int main(int argc, char ** argv) {return 0;}" | $(CXX) -xc -o /dev/null $(shell $(PYTHON_CONFIG) --ldflags) -l$(1) - > /dev/null 2>&1 && echo "-l$(1)")
+CHECK_BOOST_PYTHON = (echo "int main(int argc, char ** argv) {return 0;}" | $(CXX) -xc -o /dev/null $(LINKFLAGS) $(LIBS) -l$(1) - > /dev/null 2>&1 && echo "-l$(1)")
 BOOST_PYTHON_LIB ?= $(shell \
 	$(call CHECK_BOOST_PYTHON,boost_python-py$(subst .,,$(PYTHON_VERSION))) || \
 	$(call CHECK_BOOST_PYTHON,boost_python-py$(PYTHON_MAJOR_VERSION)) || \
@@ -343,11 +355,7 @@ ifeq ($(BOOST_PYTHON_LIB),)
 $(error BOOST_PYTHON_LIB could not be detected. Please define manually)
 endif
 
-LIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem
-# python-config --ldflags includes LIBS for some reason
-LINKFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags))
-CXXFLAGS += $(shell $(PYTHON_CONFIG) --includes) -DWITH_PYTHON
-
+LIBS += $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem
 PY_WRAPPER_FILE = kernel/python_wrappers
 OBJS += $(PY_WRAPPER_FILE).o
 PY_GEN_SCRIPT= py_wrap_generator
@@ -651,6 +659,9 @@ OBJS += libs/fst/fastlz.o
 OBJS += libs/fst/lz4.o
 endif
 
+techlibs/%_pm.h: passes/pmgen/pmgen.py techlibs/%.pmg
+	$(P) mkdir -p $(dir $@) && $(PYTHON_EXECUTABLE) $< -o $@ -p $(notdir $*) $(filter-out $<,$^)
+
 ifneq ($(SMALL),1)
 
 OBJS += libs/subcircuit/subcircuit.o
@@ -775,6 +786,15 @@ check-git-abc:
 	elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && ! grep -q '\$$Format:%[hH]\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \
 		echo "'abc' comes from a tarball. Continuing."; \
 		exit 0; \
+	elif git -C "$(YOSYS_SRC)" submodule status abc 2>/dev/null | grep -q '^+'; then \
+		echo "'abc' submodule does not match expected commit."; \
+		echo "Run 'git submodule update' to check out the correct version."; \
+		echo "Note: If testing a different version of abc, call 'git commit abc' in the Yosys source directory to update the expected commit."; \
+		exit 1; \
+	elif git -C "$(YOSYS_SRC)" submodule status abc 2>/dev/null | grep -q '^U'; then \
+		echo "'abc' submodule has merge conflicts."; \
+		echo "Please resolve merge conflicts before continuing."; \
+		exit 1; \
 	elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && grep -q '\$$Format:%[hH]\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \
 		echo "Error: 'abc' is not configured as a git submodule."; \
 		echo "To resolve this:"; \
@@ -997,6 +1017,18 @@ docs/source/cell/word_add.rst: $(TARGETS) $(EXTRA_TARGETS)
 docs/source/generated/cells.json: docs/source/generated $(TARGETS) $(EXTRA_TARGETS)
 	$(Q) ./$(PROGRAM_PREFIX)yosys -p 'help -dump-cells-json $@'
 
+docs/source/generated/%.cc: backends/%.cc
+	$(Q) mkdir -p $(@D)
+	$(Q) cp $< $@
+
+# diff returns exit code 1 if the files are different, but it's not an error
+docs/source/generated/functional/rosette.diff: backends/functional/smtlib.cc backends/functional/smtlib_rosette.cc
+	$(Q) mkdir -p $(@D)
+	$(Q) diff -U 20 $^ > $@ || exit 0
+
+PHONY: docs/gen/functional_ir
+docs/gen/functional_ir: docs/source/generated/functional/smtlib.cc docs/source/generated/functional/rosette.diff
+
 PHONY: docs/gen docs/usage docs/reqs
 docs/gen: $(TARGETS)
 	$(Q) $(MAKE) -C docs gen
@@ -1032,7 +1064,7 @@ docs/reqs:
 	$(Q) $(MAKE) -C docs reqs
 
 .PHONY: docs/prep
-docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage
+docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage docs/gen/functional_ir
 
 DOC_TARGET ?= html
 docs: docs/prep
@@ -1053,6 +1085,7 @@ clean:
 	rm -rf vloghtb/Makefile vloghtb/refdat vloghtb/rtl vloghtb/scripts vloghtb/spec vloghtb/check_yosys vloghtb/vloghammer_tb.tar.bz2 vloghtb/temp vloghtb/log_test_*
 	rm -f tests/svinterfaces/*.log_stdout tests/svinterfaces/*.log_stderr tests/svinterfaces/dut_result.txt tests/svinterfaces/reference_result.txt tests/svinterfaces/a.out tests/svinterfaces/*_syn.v tests/svinterfaces/*.diff
 	rm -f  tests/tools/cmp_tbdata
+	rm -f $(addsuffix /run-test.mk,$(MK_TEST_DIRS))
 	-$(MAKE) -C docs clean
 	rm -rf docs/source/cmd docs/util/__pycache__
 

Diff for: abc

@@ -210,14 +210,8 @@ struct SmtrModule {
 			state_struct.insert(state->name, state->sort);
 	}
 
-	void write(std::ostream &out)
-	{    
-		SExprWriter w(out);
-
-		input_struct.write_definition(w);
-		output_struct.write_definition(w);
-		state_struct.write_definition(w);
-
+	void write_eval(SExprWriter &w)
+	{
 		w.push();
 		w.open(list("define", list(name, "inputs", "state")));
 		auto inlined = [&](Functional::Node n) {
@@ -240,7 +234,10 @@ struct SmtrModule {
 		output_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.output(name).value()); });
 		state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.state(name).next_value()); });
 		w.pop();
+	}
 
+	void write_initial(SExprWriter &w)
+	{
 		w.push();
 		auto initial = name + "_initial";
 		w.open(list("define", initial));
@@ -259,6 +256,18 @@ struct SmtrModule {
 		}
 		w.pop();
 	}
+
+	void write(std::ostream &out)
+	{    
+		SExprWriter w(out);
+
+		input_struct.write_definition(w);
+		output_struct.write_definition(w);
+		state_struct.write_definition(w);
+
+		write_eval(w);
+		write_initial(w);
+	}
 };
 
 struct FunctionalSmtrBackend : public Backend {
@@ -267,7 +276,7 @@ struct FunctionalSmtrBackend : public Backend {
     	void help() override {
         	//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    write_functional_rosette [options] [selection] [filename]\n");
+		log("    write_functional_rosette [options] [filename]\n");
 		log("\n");
 		log("Functional Rosette Backend.\n");
 		log("\n");

Diff for: backends/functional/smtlib_rosette.cc

@@ -0,0 +1,44 @@
+#include "kernel/functional.h"
+#include "kernel/yosys.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct FunctionalDummyBackend : public Backend {
+	FunctionalDummyBackend() : Backend("functional_dummy", "dump generated Functional IR") {}
+	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		// backend pass boiler plate
+		log_header(design, "Executing dummy functional backend.\n");
+
+		size_t argidx = 1;
+		extra_args(f, filename, args, argidx, design);
+
+		for (auto module : design->selected_modules())
+		{
+			log("Processing module `%s`.\n", module->name.c_str());
+
+			// convert module to FunctionalIR
+			auto ir = Functional::IR::from_module(module);
+			*f << "module " << module->name.c_str() << "\n";
+
+			// write node functions
+			for (auto node : ir)
+				*f << "  assign " << id2cstr(node.name())
+				   << " = " << node.to_string() << "\n";
+			*f << "\n";
+
+			// write outputs and next state
+			for (auto output : ir.outputs())
+				*f << " " << id2cstr(output->kind)
+				   << " " << id2cstr(output->name)
+				   << " = " << id2cstr(output->value().name()) << "\n";
+			for (auto state : ir.states())
+				*f << " " << id2cstr(state->kind)
+				   << " " << id2cstr(state->name)
+				   << " = " << id2cstr(state->next_value().name()) << "\n";
+		}
+	}
+} FunctionalDummyBackend;
+
+PRIVATE_NAMESPACE_END

Diff for: docs/source/code_examples/functional/dummy.cc

@@ -6,7 +6,7 @@
 project = 'YosysHQ Yosys'
 author = 'YosysHQ GmbH'
 copyright ='2025 YosysHQ GmbH'
-yosys_ver = "0.50"
+yosys_ver = "0.51"
 
 # select HTML theme
 html_theme = 'furo-ys'

Diff for: docs/source/conf.py

@@ -1,6 +1,14 @@
 Contributing to Yosys
 =====================
 
+.. note::
+
+   For information on making a pull request on github, refer to our
+   |CONTRIBUTING|_ file.
+
+.. |CONTRIBUTING| replace:: :file:`CONTRIBUTING.md`
+.. _CONTRIBUTING: https://github.com/YosysHQ/yosys/CONTRIBUTING.md
+
 Coding Style
 ------------