Merge branch 'YosysHQ:main' into master

.github/workflows/test-build.yml

@@ -56,6 +56,7 @@ jobs:
           mkdir build
           cd build
           make -f ../Makefile config-$CC
+          echo 'SANITIZER = undefined' >> Makefile.conf
           make -f ../Makefile -j$procs ENABLE_LTO=1
 
       - name: Log yosys-config output
@@ -82,6 +83,7 @@ jobs:
     if: needs.pre_job.outputs.should_skip != 'true'
     env:
       CC: clang
+      UBSAN_OPTIONS: halt_on_error=1
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]

.mailmap

@@ -1,6 +1,6 @@
-Marcelina Kościelnicka <mwk@0x04.net>
+Wanda Phinode <wanda@phinode.net> <mwk@0x04.net>
-Marcelina Kościelnicka <mwk@0x04.net> <koriakin@0x04.net>
+Wanda Phinode <wanda@phinode.net> <koriakin@0x04.net>
-Marcelina Kościelnicka <mwk@0x04.net> <marcin@symbioticeda.com>
+Wanda Phinode <wanda@phinode.net> <marcin@symbioticeda.com>
 Claire Xenia Wolf <claire@yosyshq.com> <claire@clairexen.net>
 Claire Xenia Wolf <claire@yosyshq.com> <claire@symbioticeda.com>
 Claire Xenia Wolf <claire@yosyshq.com> <clifford@symbioticeda.com>

CHANGELOG

@@ -2,9 +2,14 @@
 List of major changes and improvements between releases
 =======================================================
 
-Yosys 0.49 .. Yosys 0.50-dev
+Yosys 0.50 .. Yosys 0.51-dev
 --------------------------
 
+Yosys 0.49 .. Yosys 0.50
+--------------------------
+ * Various
+    - "write_verilog" emits "$check" cell names as labels.
+
 Yosys 0.48 .. Yosys 0.49
 --------------------------
  * Various

Makefile

@@ -153,7 +153,7 @@ ifeq ($(OS), Haiku)
 CXXFLAGS += -D_DEFAULT_SOURCE
 endif
 
-YOSYS_VER := 0.49+1
+YOSYS_VER := 0.50+0
 
 # 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 +169,7 @@ endif
 OBJS = kernel/version_$(GIT_REV).o
 
 bumpversion:
-	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 427b5a2.. | wc -l`/;" Makefile
+	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline b5170e1.. | wc -l`/;" Makefile
 
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q)
 
@@ -1054,7 +1054,6 @@ clean:
 	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
 	-$(MAKE) -C docs clean
-	-$(MAKE) -C docs/images clean
 	rm -rf docs/source/cmd docs/util/__pycache__
 
 clean-abc:

backends/json/json.cc

@@ -408,7 +408,7 @@ struct JsonBackend : public Backend {
 		log("\n");
 		log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.\n");
 		log("They don't affect connection semantics, and are only used to preserve original\n");
-		log("HDL bit indexing.");
+		log("HDL bit indexing.\n");
 		log("And <cell_details> is:\n");
 		log("\n");
 		log("    {\n");

backends/verilog/verilog_backend.cc

@@ -1044,16 +1044,23 @@ void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell
 void dump_cell_expr_check(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
 {
 	std::string flavor = cell->getParam(ID(FLAVOR)).decode_string();
+	std::string label = "";
+	if (cell->name.isPublic()) {
+		label = stringf("%s: ", id(cell->name).c_str());
+	}
+
 	if (flavor == "assert")
-		f << stringf("%s" "assert (", indent.c_str());
+		f << stringf("%s" "%s" "assert (", indent.c_str(), label.c_str());
 	else if (flavor == "assume")
-		f << stringf("%s" "assume (", indent.c_str());
+		f << stringf("%s" "%s" "assume (", indent.c_str(), label.c_str());
 	else if (flavor == "live")
-		f << stringf("%s" "assert (eventually ", indent.c_str());
+		f << stringf("%s" "%s" "assert (eventually ", indent.c_str(), label.c_str());
 	else if (flavor == "fair")
-		f << stringf("%s" "assume (eventually ", indent.c_str());
+		f << stringf("%s" "%s" "assume (eventually ", indent.c_str(), label.c_str());
 	else if (flavor == "cover")
-		f << stringf("%s" "cover (", indent.c_str());
+		f << stringf("%s" "%s" "cover (", indent.c_str(), label.c_str());
+	else
+		log_abort();
 	dump_sigspec(f, cell->getPort(ID::A));
 	f << stringf(");\n");
 }

docs/source/conf.py

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

frontends/ast/simplify.cc

@@ -2936,7 +2936,10 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
 					lsb_expr->children[stride_ix]->detectSignWidth(stride_width, stride_sign);
 					max_width = std::max(i_width, stride_width);
 					// Stride width calculated from actual stride value.
-					stride_width = std::ceil(std::log2(std::abs(stride)));
+					if (stride == 0)
+						stride_width = 0;
+					else
+						stride_width = std::ceil(std::log2(std::abs(stride)));
 
 					if (i_width + stride_width > max_width) {
 						// For (truncated) i*stride to be within the range of dst, the following must hold:

kernel/celledges.cc

@@ -253,13 +253,13 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
 				if (a_width == 1 && is_signed) {
 					int skip = 1 << (k + 1);
 					int base = skip -1;
-					if (i % skip != base && i - a_width + 2 < 1 << b_width)
+					if (i % skip != base && i - a_width + 2 < 1 << b_width_capped)
 						db->add_edge(cell, ID::B, k, ID::Y, i, -1);	
 				} else if (is_signed) {
-					if (i - a_width + 2 < 1 << b_width)
+					if (i - a_width + 2 < 1 << b_width_capped)
 						db->add_edge(cell, ID::B, k, ID::Y, i, -1);
 				} else {
-					if (i - a_width + 1 < 1 << b_width)
+					if (i - a_width + 1 < 1 << b_width_capped)
 						db->add_edge(cell, ID::B, k, ID::Y, i, -1);
 				}
 			// right shifts

libs/fst/00_PATCH_strict_alignment.patch

@@ -0,0 +1,42 @@
+diff --git a/fastlz.cc b/fastlz.cc
+index 3272ca7a8..41ea27a16 100644
+--- a/fastlz.cc
++++ b/fastlz.cc
+@@ -60,24 +60,9 @@
+ #endif
+ 
+ /*
+- * Prevent accessing more than 8-bit at once, except on x86 architectures.
++ * Yosys patch: do not do unaligned accesses on any platform
+  */
+-#if !defined(FASTLZ_STRICT_ALIGN)
+ #define FASTLZ_STRICT_ALIGN
+-#if defined(__i386__) || defined(__386)  /* GNU C, Sun Studio */
+-#undef FASTLZ_STRICT_ALIGN
+-#elif defined(__i486__) || defined(__i586__) || defined(__i686__) || defined(__amd64) /* GNU C */
+-#undef FASTLZ_STRICT_ALIGN
+-#elif defined(_M_IX86) /* Intel, MSVC */
+-#undef FASTLZ_STRICT_ALIGN
+-#elif defined(__386)
+-#undef FASTLZ_STRICT_ALIGN
+-#elif defined(_X86_) /* MinGW */
+-#undef FASTLZ_STRICT_ALIGN
+-#elif defined(__I86__) /* Digital Mars */
+-#undef FASTLZ_STRICT_ALIGN
+-#endif
+-#endif
+ 
+ /* prototypes */
+ int fastlz_compress(const void* input, int length, void* output);
+@@ -88,11 +73,7 @@ int fastlz_decompress(const void* input, int length, void* output, int maxout);
+ #define MAX_LEN       264  /* 256 + 8 */
+ #define MAX_DISTANCE 8192
+ 
+-#if !defined(FASTLZ_STRICT_ALIGN)
+-#define FASTLZ_READU16(p) *((const flzuint16*)(p))
+-#else
+ #define FASTLZ_READU16(p) ((p)[0] | (p)[1]<<8)
+-#endif
+ 
+ #define HASH_LOG  13
+ #define HASH_SIZE (1<< HASH_LOG)

libs/fst/00_UPDATE.sh

@@ -17,3 +17,4 @@ sed -i -e 's,"fastlz.c","fastlz.cc",' *.cc *.h
 
 patch -p0 < 00_PATCH_win_zlib.patch
 patch -p0 < 00_PATCH_win_io.patch
+patch -p1 < 00_PATCH_strict_alignment.patch

libs/fst/fastlz.cc

@@ -60,24 +60,9 @@
 #endif
 
 /*
- * Prevent accessing more than 8-bit at once, except on x86 architectures.
+ * Yosys patch: do not do unaligned accesses on any platform
  */
-#if !defined(FASTLZ_STRICT_ALIGN)
 #define FASTLZ_STRICT_ALIGN
-#if defined(__i386__) || defined(__386)  /* GNU C, Sun Studio */
-#undef FASTLZ_STRICT_ALIGN
-#elif defined(__i486__) || defined(__i586__) || defined(__i686__) || defined(__amd64) /* GNU C */
-#undef FASTLZ_STRICT_ALIGN
-#elif defined(_M_IX86) /* Intel, MSVC */
-#undef FASTLZ_STRICT_ALIGN
-#elif defined(__386)
-#undef FASTLZ_STRICT_ALIGN
-#elif defined(_X86_) /* MinGW */
-#undef FASTLZ_STRICT_ALIGN
-#elif defined(__I86__) /* Digital Mars */
-#undef FASTLZ_STRICT_ALIGN
-#endif
-#endif
 
 /* prototypes */
 int fastlz_compress(const void* input, int length, void* output);
@@ -88,11 +73,7 @@ int fastlz_decompress(const void* input, int length, void* output, int maxout);
 #define MAX_LEN       264  /* 256 + 8 */
 #define MAX_DISTANCE 8192
 
-#if !defined(FASTLZ_STRICT_ALIGN)
-#define FASTLZ_READU16(p) *((const flzuint16*)(p))
-#else
 #define FASTLZ_READU16(p) ((p)[0] | (p)[1]<<8)
-#endif
 
 #define HASH_LOG  13
 #define HASH_SIZE (1<< HASH_LOG)

passes/opt/wreduce.cc

@@ -280,7 +280,7 @@ struct WreduceWorker
 	{
 		bool did_something = false;
 
-		if (!cell->type.in(config->supported_cell_types))
+		if (!config->supported_cell_types.count(cell->type))
 			return;
 
 		if (cell->type.in(ID($mux), ID($pmux)))

passes/techmap/alumacc.cc

@@ -405,11 +405,6 @@ struct AlumaccWorker
 			RTLIL::SigSpec B = sigmap(cell->getPort(ID::B));
 			RTLIL::SigSpec Y = sigmap(cell->getPort(ID::Y));
 
-			if (B < A && GetSize(B)) {
-				cmp_less = !cmp_less;
-				std::swap(A, B);
-			}
-
 			alunode_t *n = nullptr;
 
 			for (auto node : sig_alu[RTLIL::SigSig(A, B)])
@@ -418,6 +413,16 @@ struct AlumaccWorker
 					break;
 				}
 
+			if (n == nullptr) {
+				for (auto node : sig_alu[RTLIL::SigSig(B, A)])
+					if (node->is_signed == is_signed && node->invert_b && node->c == State::S1) {
+						n = node;
+						cmp_less = !cmp_less;
+						std::swap(A, B);
+						break;
+					}
+			}
+
 			if (n == nullptr) {
 				n = new alunode_t;
 				n->a = A;
@@ -445,9 +450,6 @@ struct AlumaccWorker
 			RTLIL::SigSpec B = sigmap(cell->getPort(ID::B));
 			RTLIL::SigSpec Y = sigmap(cell->getPort(ID::Y));
 
-			if (B < A && GetSize(B))
-				std::swap(A, B);
-
 			alunode_t *n = nullptr;
 
 			for (auto node : sig_alu[RTLIL::SigSig(A, B)])
@@ -456,6 +458,14 @@ struct AlumaccWorker
 					break;
 				}
 
+			if (n == nullptr) {
+				for (auto node : sig_alu[RTLIL::SigSig(B, A)])
+					if (node->is_signed == is_signed && node->invert_b && node->c == State::S1) {
+						n = node;
+						break;
+					}
+			}
+
 			if (n != nullptr) {
 				log("  creating $alu model for %s (%s): merged with %s.\n", log_id(cell), log_id(cell->type), log_id(n->cells.front()));
 				n->cells.push_back(cell);

passes/techmap/extract_fa.cc

@@ -412,14 +412,15 @@ struct ExtractFaWorker
 					facache[fakey] = make_tuple(X, Y, cell);
 				}
 
+				bool invert_y = f3i.inv_a ^ f3i.inv_b ^ f3i.inv_c;
 				if (func3.at(key).count(xor3_func)) {
-					SigBit YY = invert_xy ? module->NotGate(NEW_ID, Y) : Y;
+					SigBit YY = invert_xy ^ invert_y ? module->NotGate(NEW_ID, Y) : Y;
 					for (auto bit : func3.at(key).at(xor3_func))
 						assign_new_driver(bit, YY);
 				}
 
 				if (func3.at(key).count(xnor3_func)) {
-					SigBit YY = invert_xy ? Y : module->NotGate(NEW_ID, Y);
+					SigBit YY = invert_xy ^ invert_y ? Y : module->NotGate(NEW_ID, Y);
 					for (auto bit : func3.at(key).at(xnor3_func))
 						assign_new_driver(bit, YY);
 				}

passes/techmap/libparse.h

@@ -59,6 +59,10 @@ namespace Yosys
 
 			std::string pin() {
 				auto length = s.find_first_of("\t()'!^*& +|");
+				if (length == std::string::npos) {
+					// nothing found so use size of s
+					length = s.size();
+				}
 				auto pin = s.substr(0, length);
 				s = s.substr(length, s.size());
 				return pin;

tests/various/bug3879.ys

@@ -0,0 +1,29 @@
+read_verilog <<EOF
+module gcd(I, D);
+
+  output [2:0] I;
+  input [3:0] D;
+
+  assign I = D[0]+D[1]+D[2]+D[3];
+endmodule
+EOF
+design -save input
+
+prep
+
+design -stash gold
+
+design -load input
+
+synth  -top gcd -flatten
+
+extract_fa -v
+
+design -stash gate
+
+design -copy-from gold -as gold gcd
+design -copy-from gate -as gate gcd
+
+miter -equiv -make_assert -flatten gold gate miter
+
+sat -verify -prove-asserts -show-all miter