From 0b99f5e6d1e1aed150035421252b1ac1bf6e0cde Mon Sep 17 00:00:00 2001
From: Mohamed Gaber <me@donn.website>
Date: Thu, 11 Jun 2026 02:07:49 +0300
Subject: [PATCH] cmake/SilimateVerific: rework merged verific generation

---
 .github/actions/setup-build-env/action.yml |   2 +-
 cmake/SilimateConfig.cmake                 |   6 +-
 cmake/SilimateVerific-merge-archive.py     |  50 +++++++---
 cmake/SilimateVerific.cmake                | 102 ++++++++-------------
 4 files changed, 81 insertions(+), 79 deletions(-)

diff --git a/.github/actions/setup-build-env/action.yml b/.github/actions/setup-build-env/action.yml
index 7c1f7f60c..f9d06f719 100644
--- a/.github/actions/setup-build-env/action.yml
+++ b/.github/actions/setup-build-env/action.yml
@@ -70,7 +70,7 @@ runs:
       shell: bash
       run: |
         echo "${{ github.workspace }}/.local/bin" >> $GITHUB_PATH
-        echo "$(brew --prefix llvm@20)/bin" >> $GITHUB_PATH
+        echo "$(brew --prefix llvm)/bin" >> $GITHUB_PATH
         echo "$(brew --prefix bison)/bin" >> $GITHUB_PATH
         echo "$(brew --prefix flex)/bin" >> $GITHUB_PATH
         echo "procs=$(sysctl -n hw.ncpu)" >> $GITHUB_ENV
diff --git a/cmake/SilimateConfig.cmake b/cmake/SilimateConfig.cmake
index 968fa0383..b088b4124 100644
--- a/cmake/SilimateConfig.cmake
+++ b/cmake/SilimateConfig.cmake
@@ -1,6 +1,8 @@
 # Always force disable GNU Readline, GPL trap library
-set(YOSYS_ENABLE_READLINE OFF)
+set(YOSYS_ENABLE_READLINE OFF CACHE INTERNAL "")
+# Silimate fork has Verific in top-level directory
 set(YOSYS_VERIFIC_DIR ${PROJECT_SOURCE_DIR}/verific)
-set(YOSYS_WITH_PYTHON ON)
+# Pyosys is the primary interface for the Silimate fork
+set(YOSYS_WITH_PYTHON ON CACHE BOOL "" FORCE)
 
 add_library(verific INTERFACE)
diff --git a/cmake/SilimateVerific-merge-archive.py b/cmake/SilimateVerific-merge-archive.py
index dbcf7f8dd..d5f06cc7a 100644
--- a/cmake/SilimateVerific-merge-archive.py
+++ b/cmake/SilimateVerific-merge-archive.py
@@ -1,29 +1,51 @@
+# Copyright (c) 2026 Silimate, Inc.
+# SPDX-License-Identifier: MIT
+"""
+Usage: <script> <primary.a> [archive.a [archive.a [archive.a …]]]
+
+Merges a number of .a files such that the symbols of the first archive is
+prioritized by extracting and marking all symbols of subsequent archives as
+local.
+"""
+import os
 import sys
+import shutil
 import pathlib
 import subprocess
 
-out = sys.argv[1]
+if len(sys.argv) < 2:
+	print("Invalid argument count: must have at least one argument.", file=sys.stderr)
+	exit(1)
+
+primary = pathlib.Path(sys.argv[1])
 files = sys.argv[2:]
-
-final_archive_objects = []
-custom_silimate_symbols = set()
-for object in filter(lambda x: x.endswith(".o"), files):
-	final_archive_objects.append(object)
-	result = subprocess.check_output(["nm", "-gjU", object], encoding="utf8")
-	custom_silimate_symbols.update(filter(lambda x: len(x.strip()), result.splitlines()))
-
-symbol_localize_args = [f"-L{symbol}" for symbol in custom_silimate_symbols]
-
 cwd = pathlib.Path(".").resolve()
+
+objcopy_bin = shutil.which("objcopy") or shutil.which("llvm-objcopy")
+if objcopy_bin is None:
+	print("Could not find either objcopy or llvm-objcopy in PATH.", file=sys.stderr)
+	exit(1)
+
+prioritized_symbols = set()
+
+object_dir = cwd / "verific-merge" / primary.stem
+object_dir.mkdir(parents=True, exist_ok=True)
+subprocess.check_call(["ar", "x", primary], cwd=object_dir)
+for object in object_dir.glob("*.o"):
+	result = subprocess.check_output(["nm", "-gjU", object], encoding="utf8")
+	prioritized_symbols.update(filter(lambda x: len(x.strip()), result.splitlines()))
+
+symbol_localize_args = [f"-L{symbol}" for symbol in prioritized_symbols]
+final_archive_objects = []
 for archive in filter(lambda x: x.endswith(".a"), files):
 	file_path = pathlib.Path(archive)
 	name = file_path.stem
 	object_dir = cwd / "verific-merge" / name
 	object_dir.mkdir(parents=True, exist_ok=True)
 	subprocess.check_call(["ar", "x", archive], cwd=object_dir)
-	for object in object_dir.glob("*"):
+	for object in object_dir.glob("*.o"):
 		if len(symbol_localize_args):
-			subprocess.check_call(["objcopy", *symbol_localize_args, object])
+			subprocess.check_call([objcopy_bin, *symbol_localize_args, object])
 		final_archive_objects.append(object)
 
-subprocess.check_call(["ar", "rcs", out, *final_archive_objects])
+subprocess.check_call(["ar", "rs", primary, *final_archive_objects])
diff --git a/cmake/SilimateVerific.cmake b/cmake/SilimateVerific.cmake
index e59b4e387..a4fca0156 100644
--- a/cmake/SilimateVerific.cmake
+++ b/cmake/SilimateVerific.cmake
@@ -1,14 +1,13 @@
 if (YOSYS_ENABLE_VERIFIC)
 	# user-facing options
-	option(WITH_VERIFIC_SYSTEMVERILOG "" ON)
-	option(WITH_VERIFIC_VHDL "" ON)
-	option(WITH_VERIFIC_HIER_TREE "" ON)
-	option(WITH_VERIFIC_SILIMATE_EXTENSIONS "" ON)
-	option(WITH_VERIFIC_YOSYSHQ_EXTENSIONS "" OFF)
-	option(WITH_VERIFIC_EDIF "" OFF)
-	option(WITH_VERIFIC_LIBERTY "" OFF)
-	option(WITH_VERIFIC_UPF "" OFF)
-	option(WITH_VERIFIC_SILIMATE_EXTENSIONS "Enable Silimate-specific options for Verific" ON)
+	option(WITH_VERIFIC_SYSTEMVERILOG "Enable Verific SystemVerilog support" ON)
+	option(WITH_VERIFIC_VHDL "Enable Verific VHDL support" ON)
+	option(WITH_VERIFIC_HIER_TREE "Enable Verific hier_tree component" ON)
+	option(WITH_VERIFIC_SILIMATE_EXTENSIONS "Enable Silimate-specific Verific modifications" ON)
+	option(WITH_VERIFIC_YOSYSHQ_EXTENSIONS "Enable YosysHQ-specific Verific modifications" OFF)
+	option(WITH_VERIFIC_EDIF "Enable Verific EDIF support" OFF)
+	option(WITH_VERIFIC_LIBERTY "Enable Verific Liberty file support" OFF)
+	option(WITH_VERIFIC_UPF "Enable Verific UPF support (requires Tcl support)" OFF)
 
 	# further checks and conditions
 	condition(ENABLE_VERIFIC_SYSTEMVERILOG WITH_VERIFIC_SYSTEMVERILOG)
@@ -44,7 +43,7 @@ if (YOSYS_ENABLE_VERIFIC)
 		list(APPEND YOSYS_VERIFIC_COMPONENTS extensions)
 	endif()
 
-	# Prepare Silimate-specific objects
+	# Prepare Silimate-specific objects overriding existing Verific symbols
 	flex_target(veri_flex
 		${YOSYS_VERIFIC_DIR}/verilog/verilog.l
 		veri_lex.cpp
@@ -57,14 +56,35 @@ if (YOSYS_ENABLE_VERIFIC)
 		COMPILE_FLAGS "--name-prefix=veri --no-lines"
 	)
 
-	add_library(verific_database_modified OBJECT
-		${YOSYS_VERIFIC_DIR}/database/DBSilimate.cpp
+	string(REPLACE ".a" ".raw.a" VERIFIC_RAW_LIB_SUFFIX "${VERIFIC_LIB_SUFFIX}")
+
+	# prepare archive list
+	foreach(component ${YOSYS_VERIFIC_COMPONENTS})
+		if (component STREQUAL "util")
+			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/util${VERIFIC_RAW_LIB_SUFFIX})
+		elseif (component STREQUAL "database")
+			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/database${VERIFIC_RAW_LIB_SUFFIX})
+		elseif (component STREQUAL "verilog")
+			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/verilog${VERIFIC_RAW_LIB_SUFFIX})
+		else()
+			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/${component}${VERIFIC_LIB_SUFFIX})
+		endif()
+	endforeach()
+
+	# Compile "verific_merged", which prioritizes the custom, listed Silimate
+	# files but also merges in .a files from upstream with a lower priority.
+	add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/empty.cpp
+		COMMAND touch ${CMAKE_CURRENT_BINARY_DIR}/empty.cpp
 	)
-	target_include_directories(verific_database_modified PRIVATE ${YOSYS_VERIFIC_DIR}/containers ${YOSYS_VERIFIC_DIR}/containers ${YOSYS_VERIFIC_DIR}/util)
-	add_library(verific_verilog_modified OBJECT
-		${YOSYS_VERIFIC_DIR}/verilog/VeriSilimate.cpp
+	add_library(verific_merged STATIC
+		${CMAKE_CURRENT_BINARY_DIR}/empty.cpp # empty file so the source list isn't empty if silimate extensions are off
+		$<${ENABLE_VERIFIC_SILIMATE_EXTENSIONS}:veri_yacc.cpp>
+		$<${ENABLE_VERIFIC_SILIMATE_EXTENSIONS}:veri_lex.cpp>
+		$<${ENABLE_VERIFIC_SILIMATE_EXTENSIONS}:${YOSYS_VERIFIC_DIR}/util/UtilSilimate.cpp>
+		$<${ENABLE_VERIFIC_SILIMATE_EXTENSIONS}:${YOSYS_VERIFIC_DIR}/database/DBSilimate.cpp>
+		$<${ENABLE_VERIFIC_SILIMATE_EXTENSIONS}:${YOSYS_VERIFIC_DIR}/verilog/VeriSilimate.cpp>
 	)
-	target_include_directories(verific_verilog_modified PRIVATE
+	target_include_directories(verific_merged PRIVATE
 		${YOSYS_VERIFIC_DIR}/containers
 		${YOSYS_VERIFIC_DIR}/database
 		${YOSYS_VERIFIC_DIR}/util
@@ -72,62 +92,20 @@ if (YOSYS_ENABLE_VERIFIC)
 		${YOSYS_VERIFIC_DIR}/vhdl
 		${YOSYS_VERIFIC_DIR}/verilog
 	)
-	add_library(verific_vparser_modified OBJECT
-		veri_yacc.cpp
-	)
-	target_include_directories(verific_vparser_modified PRIVATE
-		${YOSYS_VERIFIC_DIR}/containers
-		${YOSYS_VERIFIC_DIR}/verilog
-		${YOSYS_VERIFIC_DIR}/util
-	)
-	add_library(verific_util_modified OBJECT
-		${YOSYS_VERIFIC_DIR}/util/UtilSilimate.cpp
-	)
-	target_include_directories(verific_util_modified PRIVATE ${YOSYS_VERIFIC_DIR}/containers ${YOSYS_VERIFIC_DIR}/util)
-
-	string(REPLACE ".a" ".raw.a" VERIFIC_RAW_LIB_SUFFIX "${VERIFIC_LIB_SUFFIX}")
-
-	# prepare object list based on component list + whether to load silimate
-	# customizations
-	list(APPEND VERIFIC_OBJECTS $<TARGET_OBJECTS:verific_vparser_modified>)
-	foreach(component ${YOSYS_VERIFIC_COMPONENTS})
-		if (component STREQUAL "util")
-			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/util${VERIFIC_RAW_LIB_SUFFIX})
-			if (ENABLE_VERIFIC_SILIMATE_EXTENSIONS)
-				list(APPEND VERIFIC_OBJECTS $<TARGET_OBJECTS:verific_util_modified>)
-			endif()
-		elseif (component STREQUAL "database")
-			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/database${VERIFIC_RAW_LIB_SUFFIX})
-			if (ENABLE_VERIFIC_SILIMATE_EXTENSIONS)
-				list(APPEND VERIFIC_OBJECTS $<TARGET_OBJECTS:verific_database_modified>)
-			endif()
-		elseif (component STREQUAL "verilog")
-			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/verilog${VERIFIC_RAW_LIB_SUFFIX})
-			if (ENABLE_VERIFIC_SILIMATE_EXTENSIONS)
-				list(APPEND VERIFIC_OBJECTS $<TARGET_OBJECTS:verific_verilog_modified>)
-			endif()
-		else()
-			list(APPEND VERIFIC_OBJECTS ${YOSYS_VERIFIC_DIR}/${component}/${component}${VERIFIC_LIB_SUFFIX})
-		endif()
-	endforeach()
-
-	# prepare merged .a object using custom Python script
-	add_custom_command(
-		OUTPUT ${PROJECT_BINARY_DIR}/verific_merged.a
+	add_custom_command(TARGET verific_merged POST_BUILD
 		DEPENDS
 			${VERIFIC_OBJECTS}
 		COMMAND
-			${Python3_EXECUTABLE} ${CMAKE_CURRENT_LIST_DIR}/SilimateVerific-merge-archive.py ${CMAKE_CURRENT_BINARY_DIR}/verific_merged.a ${VERIFIC_OBJECTS}
+			env CMAKE_OBJCOPY=${CMAKE_OBJCOPY} ${Python3_EXECUTABLE} ${CMAKE_CURRENT_LIST_DIR}/SilimateVerific-merge-archive.py $<TARGET_FILE:verific_merged> ${VERIFIC_OBJECTS}
 	)
-	add_custom_target(verific_merged DEPENDS ${PROJECT_BINARY_DIR}/verific_merged.a)
 
-	# prepare interface as in YosysVerific.cmake
+	# Prepare verific interface library as in YosysVerific.cmake
 	get_verific_options(verific_include_dirs verific_libraries ${YOSYS_VERIFIC_COMPONENTS})
 	target_include_directories(verific INTERFACE
 		${verific_include_dirs}
 	)
 	target_link_libraries(verific INTERFACE
-		$<LINK_LIBRARY:WHOLE_ARCHIVE,${PROJECT_BINARY_DIR}/verific_merged.a>
+		$<LINK_LIBRARY:WHOLE_ARCHIVE,$<TARGET_FILE:verific_merged>>
 		PkgConfig::zlib
 	)