Merge branch 'YosysHQ:main' into main

.github/workflows/extra-builds.yml

@@ -5,6 +5,7 @@ on:
   push:
     branches:
       - main
+  merge_group:
   # test PRs
   pull_request:
   # allow triggering tests, ignores skip check

.github/workflows/prepare-docs.yml

@@ -1,6 +1,6 @@
 name: Build docs artifact with Verific
 
-on: [push, pull_request]
+on: [push, pull_request, merge_group]
 
 jobs:
   check_docs_rebuild:

.github/workflows/test-build.yml

@@ -5,6 +5,7 @@ on:
   push:
     branches:
       - main
+  merge_group:
   # test PRs
   pull_request:
   # allow triggering tests, ignores skip check

.github/workflows/test-compile.yml

@@ -5,6 +5,7 @@ on:
   push:
     branches:
       - main
+  merge_group:
   # test PRs
   pull_request:
   # allow triggering tests, ignores skip check

.github/workflows/test-sanitizers.yml

@@ -5,6 +5,7 @@ on:
   push:
     branches:
       - main
+  merge_group:
   # ignore PRs due to time needed
   # allow triggering tests, ignores skip check
   workflow_dispatch:

.github/workflows/test-verific.yml

@@ -5,6 +5,7 @@ on:
   push:
     branches:
       - main
+  merge_group:
   # test PRs
   pull_request:
   # allow triggering tests, ignores skip check

CHANGELOG

@@ -2,9 +2,22 @@
 List of major changes and improvements between releases
 =======================================================
 
-Yosys 0.60 .. Yosys 0.61-dev
+Yosys 0.61 .. Yosys 0.62-dev
 --------------------------
 
+Yosys 0.60 .. Yosys 0.61
+--------------------------
+ * Various
+    - Removed "cover" pass for coverage tracking.
+    - Avoid merging formal properties with "opt_merge" pass.
+    - Parallelize "opt_merge" pass.
+
+ * New commands and options
+    - Added "design_equal" pass to support fuzz-test comparison.
+    - Added "lut2bmux" pass to convert $lut to $bmux.
+    - Added "-legalize" option to "read_rtlil" pass to prevent 
+      semantic errors.
+
 Yosys 0.59 .. Yosys 0.60
 --------------------------
  * Various

COPYING

@@ -1,6 +1,6 @@
 ISC License
 
-Copyright (C) 2012 - 2025  Claire Xenia Wolf <claire@yosyshq.com>
+Copyright (C) 2012 - 2026  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

Makefile

@@ -177,7 +177,7 @@ ifeq ($(OS), Haiku)
 CXXFLAGS += -D_DEFAULT_SOURCE
 endif
 
-YOSYS_VER := 0.60+102
+YOSYS_VER := 0.61+0
 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)
@@ -202,7 +202,7 @@ endif
 OBJS = kernel/version_$(GIT_REV).o
 
 bumpversion:
-	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 5bafeb7.. | wc -l`/;" Makefile
+	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 5ae48ee.. | wc -l`/;" Makefile
 
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) OPTFLAGS="-g -O3"
 
@@ -676,8 +676,6 @@ $(eval $(call add_include_file,libs/sha1/sha1.h))
 $(eval $(call add_include_file,libs/json11/json11.hpp))
 $(eval $(call add_include_file,passes/fsm/fsmdata.h))
 $(eval $(call add_include_file,passes/techmap/libparse.h))
-$(eval $(call add_include_file,frontends/ast/ast.h))
-$(eval $(call add_include_file,frontends/ast/ast_binding.h))
 $(eval $(call add_include_file,frontends/blif/blifparse.h))
 $(eval $(call add_include_file,backends/rtlil/rtlil_backend.h))
 

backends/smt2/smtbmc.py

@@ -735,6 +735,12 @@ def ywfile_signal(sig, step, mask=None):
 
     output = []
 
+    def ywfile_signal_error(reason, detail=None):
+        msg = f"Yosys witness signal mismatch for {sig.pretty()}: {reason}"
+        if detail:
+            msg += f" ({detail})"
+        raise ValueError(msg)
+
     if sig.path in smt_wires:
         for wire in smt_wires[sig.path]:
             width, offset = wire["width"], wire["offset"]
@@ -765,6 +771,12 @@ def ywfile_signal(sig, step, mask=None):
             for mem in smt_mems[sig.memory_path]:
                 width, size, bv = mem["width"], mem["size"], mem["statebv"]
 
+                if sig.memory_addr is not None and sig.memory_addr >= size:
+                    ywfile_signal_error(
+                        "memory address out of bounds",
+                        f"address={sig.memory_addr} size={size}",
+                    )
+
                 smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"])
 
                 if bv:
@@ -781,18 +793,34 @@ def ywfile_signal(sig, step, mask=None):
                     smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
 
                 output.append((0, sig.width, smt_expr))
+        else:
+            ywfile_signal_error("memory not found in design")
 
     output.sort()
 
     output = [chunk for chunk in output if chunk[0] != chunk[1]]
 
+    if not output:
+        if sig.memory_path:
+            ywfile_signal_error("memory signal has no matching bits in design")
+        else:
+            ywfile_signal_error("signal not found in design")
+
     pos = 0
 
     for start, end, smt_expr in output:
-        assert start == pos
+        if start != pos:
+            ywfile_signal_error(
+                "signal width/offset mismatch",
+                f"expected coverage at bit {pos}",
+            )
         pos = end
 
-    assert pos == sig.width
+    if pos != sig.width:
+        ywfile_signal_error(
+            "signal width/offset mismatch",
+            f"covered {pos} of {sig.width} bits",
+        )
 
     if len(output) == 1:
         return output[0][-1]

docs/source/conf.py

@@ -5,8 +5,8 @@ import os
 
 project = 'YosysHQ Yosys'
 author = 'YosysHQ GmbH'
-copyright ='2025 YosysHQ GmbH'
-yosys_ver = "0.60"
+copyright ='2026 YosysHQ GmbH'
+yosys_ver = "0.61"
 
 # select HTML theme
 html_theme = 'furo-ys'

frontends/ast/simplify.cc

@@ -4690,6 +4690,7 @@ void AstNode::expand_genblock(const std::string &prefix)
 
 		switch (child->type) {
 		case AST_WIRE:
+		case AST_AUTOWIRE:
 		case AST_MEMORY:
 		case AST_STRUCT:
 		case AST_UNION:
@@ -4718,6 +4719,93 @@ void AstNode::expand_genblock(const std::string &prefix)
 			}
 			break;
 
+		case AST_IDENTIFIER:
+			if (!child->str.empty() && prefix.size() > 0) {
+				bool is_resolved = false;
+				std::string identifier_str = child->str;
+				if (current_ast_mod != nullptr && identifier_str.compare(0, current_ast_mod->str.size(), current_ast_mod->str) == 0) {
+					if (identifier_str.at(current_ast_mod->str.size()) == '.') {
+						identifier_str = '\\' + identifier_str.substr(current_ast_mod->str.size()+1, identifier_str.size());
+					}
+				}
+				// search starting in the innermost scope and then stepping outward
+				for (size_t ppos = prefix.size() - 1; ppos; --ppos) {
+					if (prefix.at(ppos) != '.') continue;
+
+					std::string new_prefix = prefix.substr(0, ppos + 1);
+					auto attempt_resolve = [&new_prefix](const std::string &ident) -> std::string {
+						std::string new_name = prefix_id(new_prefix, ident);
+						if (current_scope.count(new_name))
+							return new_name;
+						return {};
+					};
+
+					// attempt to resolve the full identifier
+					std::string resolved = attempt_resolve(identifier_str);
+					if (!resolved.empty()) {
+						is_resolved = true;
+						break;
+					}
+					// attempt to resolve hierarchical prefixes within the identifier,
+					// as the prefix could refer to a local scope which exists but
+					// hasn't yet been elaborated
+					for (size_t spos = identifier_str.size() - 1; spos; --spos) {
+						if (identifier_str.at(spos) != '.') continue;
+						resolved = attempt_resolve(identifier_str.substr(0, spos));
+						if (!resolved.empty()) {
+							is_resolved = true;
+							identifier_str = resolved + identifier_str.substr(spos);
+							ppos = 1; // break outer loop
+							break;
+						}
+					}
+					if (current_scope.count(identifier_str) == 0) {
+						AstNode *current_scope_ast = (current_ast_mod == nullptr) ? current_ast : current_ast_mod;
+						for (auto& node : current_scope_ast->children) {
+							switch (node->type) {
+							case AST_PARAMETER:
+							case AST_LOCALPARAM:
+							case AST_WIRE:
+							case AST_AUTOWIRE:
+							case AST_GENVAR:
+							case AST_MEMORY:
+							case AST_FUNCTION:
+							case AST_TASK:
+							case AST_DPI_FUNCTION:
+								if (prefix_id(new_prefix, identifier_str) == node->str) {
+									is_resolved = true;
+									current_scope[node->str] = node.get();
+								}
+								break;
+							case AST_ENUM:
+								current_scope[node->str] = node.get();
+								for (auto& enum_node : node->children) {
+									log_assert(enum_node->type==AST_ENUM_ITEM);
+									if (prefix_id(new_prefix, identifier_str) == enum_node->str) {
+										is_resolved = true;
+										current_scope[enum_node->str] = enum_node.get();
+									}
+								}
+								break;
+							default:
+								break;
+							}
+						}
+					}
+				}
+				if ((current_scope.count(identifier_str) == 0) && is_resolved == false) {
+					if (current_ast_mod == nullptr) {
+						input_error("Identifier `%s' is implicitly declared outside of a module.\n", child->str.c_str());
+					} else if (flag_autowire || identifier_str == "\\$global_clock") {
+						auto auto_wire = std::make_unique<AstNode>(child->location, AST_AUTOWIRE);
+						auto_wire->str = identifier_str;
+						children.push_back(std::move(auto_wire));
+					} else {
+						input_error("Identifier `%s' is implicitly declared and `default_nettype is set to none.\n", identifier_str.c_str());
+					}
+				}
+			}
+			break;
 		default:
 			break;
 		}

frontends/verilog/verilog_frontend.cc

@@ -500,7 +500,6 @@ struct VerilogFrontend : public Frontend {
 		log("Parsing %s%s input from `%s' to AST representation.\n",
 				parse_mode.formal ? "formal " : "", parse_mode.sv ? "SystemVerilog" : "Verilog", filename.c_str());
 
-		log("verilog frontend filename %s\n", filename.c_str());
 		if (flag_relative_share) {
 			auto share_path = proc_share_dirname();
 			if (filename.substr(0, share_path.length()) == share_path)

kernel/log.cc

@@ -90,11 +90,11 @@ int gettimeofday(struct timeval *tv, struct timezone *tz)
 	QueryPerformanceFrequency(&freq);
 	QueryPerformanceCounter(&counter);
 
-	counter.QuadPart *= 1000000;
+	counter.QuadPart *= 1'000'000;
 	counter.QuadPart /= freq.QuadPart;
 
 	tv->tv_sec = long(counter.QuadPart / 1000000);
-	tv->tv_usec = counter.QuadPart % 1000000;
+	tv->tv_usec = counter.QuadPart % 1'000'000;
 
 	return 0;
 }
@@ -135,7 +135,7 @@ static void logv_string(std::string_view format, std::string str) {
 				initial_tv = tv;
 			if (tv.tv_usec < initial_tv.tv_usec) {
 				tv.tv_sec--;
-				tv.tv_usec += 1000000;
+				tv.tv_usec += 1'000'000;
 			}
 			tv.tv_sec -= initial_tv.tv_sec;
 			tv.tv_usec -= initial_tv.tv_usec;

kernel/register.cc

@@ -1204,7 +1204,7 @@ struct LicensePass : public Pass {
 		log(" |                                                                            |\n");
 		log(" |  yosys -- Yosys Open SYnthesis Suite                                       |\n");
 		log(" |                                                                            |\n");
-		log(" |  Copyright (C) 2012 - 2025  Claire Xenia Wolf <claire@yosyshq.com>         |\n");
+		log(" |  Copyright (C) 2012 - 2026  Claire Xenia Wolf <claire@yosyshq.com>         |\n");
 		log(" |                                                                            |\n");
 		log(" |  Permission to use, copy, modify, and/or distribute this software for any  |\n");
 		log(" |  purpose with or without fee is hereby granted, provided that the above    |\n");

kernel/yosys.cc

@@ -175,7 +175,7 @@ void yosys_banner()
 	log("\n");
 	log(" /----------------------------------------------------------------------------\\\n");
 	log(" |  yosys -- Yosys Open SYnthesis Suite                                       |\n");
-	log(" |  Copyright (C) 2012 - 2025  Claire Xenia Wolf <claire@yosyshq.com>         |\n");
+	log(" |  Copyright (C) 2012 - 2026  Claire Xenia Wolf <claire@yosyshq.com>         |\n");
 	log(" |  Distributed under an ISC-like license, type \"license\" to see terms        |\n");
 	log(" \\----------------------------------------------------------------------------/\n");
 	log(" %s\n", yosys_maybe_version());

passes/cmds/select.cc

@@ -570,7 +570,7 @@ static void select_op_expand(RTLIL::Design *design, const std::string &arg, char
 		ct.setup(design);
 
 	if (pos < int(arg.size()) && arg[pos] == '*') {
-		levels = 1000000;
+		levels = 1'000'000;
 		pos++;
 	} else
 	if (pos < int(arg.size()) && '0' <= arg[pos] && arg[pos] <= '9') {

passes/opt/opt_muxtree.cc

@@ -64,7 +64,7 @@ struct OptMuxtreeWorker
 	RTLIL::Module *module;
 	SigMap assign_map;
 	int removed_count;
-	int glob_evals_left = 10000000;
+	int glob_evals_left = 10'000'000;
 
 	struct bitinfo_t {
 		// Is bit directly used by non-mux cells or ports?

passes/techmap/extract_fa.cc

@@ -40,10 +40,10 @@ int bindec(unsigned char v)
 	r += (~((v & 2) - 1)) & 10;
 	r += (~((v & 4) - 1)) & 100;
 	r += (~((v & 8) - 1)) & 1000;
-	r += (~((v & 16) - 1)) & 10000;
-	r += (~((v & 32) - 1)) & 100000;
-	r += (~((v & 64) - 1)) & 1000000;
-	r += (~((v & 128) - 1)) & 10000000;
+	r += (~((v & 16) - 1)) & 10'000;
+	r += (~((v & 32) - 1)) & 100'000;
+	r += (~((v & 64) - 1)) & 1'000'000;
+	r += (~((v & 128) - 1)) & 10'000'000;
 	return r;
 }
 

tests/functional/test_smtbmc_witness_mismatch.py

@@ -0,0 +1,190 @@
+import json
+import shutil
+import subprocess
+from pathlib import Path
+
+import pytest
+
+base_path = Path(__file__).resolve().parent.parent.parent
+
+pytestmark = pytest.mark.skipif(shutil.which("z3") is None, reason="z3 not available")
+
+def run(cmd, **kwargs):
+    """Run a command and assert it succeeds."""
+    status = subprocess.run(cmd, **kwargs)
+    assert status.returncode == 0, f"{cmd[0]} failed"
+    return status
+
+
+def write_smt2(tmp_path, verilog_text):
+    """Write Verilog to temp and emit SMT2 via yosys."""
+    vfile = tmp_path / "design.v"
+    smt2 = tmp_path / "design.smt2"
+    vfile.write_text(verilog_text)
+    run([base_path / "yosys", "-Q", "-p",
+         f"read_verilog {vfile}; prep -top top; write_smt2 {smt2}"])
+    return smt2
+
+
+def witness_entries(smt2_path):
+    """Parse yosys-smt2-witness JSON records from an SMT2 file."""
+    entries = []
+    marker = "yosys-smt2-witness"
+    with open(smt2_path, "r") as f:
+        for line in f:
+            if marker not in line:
+                continue
+            payload = line.split(marker, 1)[1].strip()
+            entries.append(json.loads(payload))
+    return entries
+
+
+def find_entry(entries, entry_type):
+    """Return the first witness entry of the given type."""
+    for entry in entries:
+        if entry.get("type") == entry_type:
+            return entry
+    return None
+
+
+def write_yw(yw_path, signals, bits):
+    """Write a minimal Yosys witness file with one step of bits."""
+    data = {
+        "format": "Yosys Witness Trace",
+        "clocks": [],
+        "signals": signals,
+        "steps": [{"bits": bits}],
+    }
+    yw_path.write_text(json.dumps(data))
+
+
+def run_smtbmc(smt2_path, yw_path):
+    """Run yosys-smtbmc on the SMT2 file with a witness trace."""
+    cmd = [
+        base_path / "yosys-smtbmc",
+        "-s", "z3",
+        "-m", "top",
+        "--check-witness",
+        "--yw", yw_path,
+        "-t", "1",
+        smt2_path,
+    ]
+    return subprocess.run(cmd, capture_output=True, text=True)
+
+
+def assert_no_mismatch_message(result):
+    """Assert the mismatch error prefix is absent from outputs."""
+    combined = (result.stderr or "") + (result.stdout or "")
+    assert "Yosys witness signal mismatch" not in combined
+
+
+def assert_has_mismatch_message(result, msg):
+    """Assert the mismatch error prefix and substring are present."""
+    combined = (result.stderr or "") + (result.stdout or "")
+    assert "Yosys witness signal mismatch" in combined
+    assert msg in combined
+
+
+def test_missing_signal_path(tmp_path):
+    smt2 = write_smt2(tmp_path, "module top(input ok, output out); assign out = ok; endmodule")
+    yw_path = tmp_path / "trace.yw"
+    signals = [{"path": ["\\missing"], "offset": 0, "width": 1, "init_only": False}]
+    write_yw(yw_path, signals, "1")
+    result = run_smtbmc(smt2, yw_path)
+    assert result.returncode != 0
+    assert_has_mismatch_message(result, "signal not found in design")
+
+
+def test_width_mismatch(tmp_path):
+    smt2 = write_smt2(tmp_path, "module top(input ok, output out); assign out = ok; endmodule")
+    entries = witness_entries(smt2)
+    input_entry = find_entry(entries, "input")
+    assert input_entry is not None
+    yw_path = tmp_path / "trace.yw"
+    signals = [{
+        "path": input_entry["path"],
+        "offset": 0,
+        "width": 2,
+        "init_only": False,
+    }]
+    write_yw(yw_path, signals, "10")
+    result = run_smtbmc(smt2, yw_path)
+    assert result.returncode != 0
+    assert_has_mismatch_message(result, "signal width/offset mismatch")
+
+
+def test_memory_address_oob(tmp_path):
+    verilog = """
+module top(input ok, output [7:0] mem_out);
+  reg [7:0] mem [0:1];
+  assign mem_out = mem[0] ^ {8{ok}};
+endmodule
+"""
+    smt2 = write_smt2(tmp_path, verilog)
+    entries = witness_entries(smt2)
+    mem_entry = find_entry(entries, "mem")
+    assert mem_entry is not None
+    addr = mem_entry["size"]
+    yw_path = tmp_path / "trace.yw"
+    signals = [{
+        "path": mem_entry["path"] + [f"\\[{addr}]"],
+        "offset": 0,
+        "width": mem_entry["width"],
+        "init_only": False,
+    }]
+    bits = "0" * mem_entry["width"]
+    write_yw(yw_path, signals, bits)
+    result = run_smtbmc(smt2, yw_path)
+    assert result.returncode != 0
+    assert_has_mismatch_message(result, "memory address out of bounds")
+
+
+def test_allowed_extra_signal_in_design(tmp_path):
+    verilog = """
+module top(input ok, input extra, output [1:0] out);
+  assign out = {ok, extra};
+endmodule
+"""
+    smt2 = write_smt2(tmp_path, verilog)
+    entries = witness_entries(smt2)
+    input_entry = find_entry(entries, "input")
+    assert input_entry is not None
+    yw_path = tmp_path / "trace.yw"
+    signals = [{
+        "path": input_entry["path"],
+        "offset": 0,
+        "width": input_entry["width"],
+        "init_only": False,
+    }]
+    bits = "0" * input_entry["width"]
+    write_yw(yw_path, signals, bits)
+    result = run_smtbmc(smt2, yw_path)
+    # With --check-witness and no assertions, smtbmc can still exit non-zero.
+    # Thus we don't check the result.returncode here and in the other success
+    # cases.
+    assert_no_mismatch_message(result)
+
+
+def test_allowed_extra_memory_in_design(tmp_path):
+    verilog = """
+module top(input ok, output [7:0] out);
+  reg [7:0] mem0 [0:1];
+  reg [7:0] mem1 [0:3];
+  assign out = mem0[0] ^ mem1[0];
+endmodule
+"""
+    smt2 = write_smt2(tmp_path, verilog)
+    entries = witness_entries(smt2)
+    input_entry = find_entry(entries, "input")
+    assert input_entry is not None
+    yw_path = tmp_path / "trace.yw"
+    signals = [{
+        "path": input_entry["path"],
+        "offset": 0,
+        "width": input_entry["width"],
+        "init_only": False,
+    }]
+    bits = "1" * input_entry["width"]
+    write_yw(yw_path, signals, bits)
+    result = run_smtbmc(smt2, yw_path)
+    assert_no_mismatch_message(result)

tests/verilog/genblk_wire.sv

@@ -0,0 +1,20 @@
+module gold(a, b);
+	output wire [1:0] a;
+	input wire [1:0] b;
+	genvar i;
+	for (i = 0; i < 2; i++) begin
+		wire x;
+		assign x = b[i];
+		assign a[i] = x;
+	end
+endmodule
+
+module gate(a, b);
+	output wire [1:0] a;
+	input wire [1:0] b;
+	genvar i;
+	for (i = 0; i < 2; i++) begin
+		assign x = b[i];
+		assign a[i] = x;
+	end
+endmodule

tests/verilog/genblk_wire.ys

@@ -0,0 +1,17 @@
+logger -expect warning "Identifier `\\genblk1[[]0[]]\.x' is implicitly declared." 1
+logger -expect warning "Identifier `\\genblk1[[]1[]]\.x' is implicitly declared." 1
+read_verilog -sv genblk_wire.sv
+logger -check-expected
+
+select -assert-count 1 gate/genblk1[0].x
+select -assert-count 1 gate/genblk1[1].x
+select -assert-count 0 gate/genblk1[2].x
+
+select -assert-count 1 gold/genblk1[0].x
+select -assert-count 1 gold/genblk1[1].x
+select -assert-count 0 gold/genblk1[2].x
+
+proc
+equiv_make gold gate equiv
+equiv_simple
+equiv_status -assert