From 0db45a6796fe45d9dc906f77a207b8e812b26dc7 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 04:03:31 -0700 Subject: [PATCH 01/10] Reenable VHDL --- Makefile | 90 +++++++++++++++++-- tests/verific/README.md | 4 +- tests/verific/import_warning_operator.ys | 5 ++ ...mixed_flist.ys.DISABLED => mixed_flist.ys} | 0 verific | 2 +- 5 files changed, 91 insertions(+), 10 deletions(-) create mode 100644 tests/verific/import_warning_operator.ys rename tests/verific/{mixed_flist.ys.DISABLED => mixed_flist.ys} (100%) diff --git a/Makefile b/Makefile index 33519a233..e73570f57 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,7 @@ ENABLE_GHDL := 0 ENABLE_SLANG := 0 ENABLE_VERIFIC := 1 ENABLE_VERIFIC_SYSTEMVERILOG := 1 -ENABLE_VERIFIC_VHDL := 0 +ENABLE_VERIFIC_VHDL := 1 ENABLE_VERIFIC_HIER_TREE := 1 ENABLE_VERIFIC_SILIMATE_EXTENSIONS := 1 ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0 @@ -515,7 +515,7 @@ endif LIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= ./verific -VERIFIC_COMPONENTS ?= database util containers +VERIFIC_COMPONENTS ?= database util containers pct ifeq ($(ENABLE_VERIFIC_HIER_TREE),1) VERIFIC_COMPONENTS += hier_tree CXXFLAGS += -DVERIFIC_HIER_TREE_SUPPORT @@ -553,8 +553,11 @@ VERIFIC_COMPONENTS += hdl_file_sort verilog_nl VERIFIC_COMPONENTS += commands upf CXXFLAGS += -DVERIFIC_UPF_SUPPORT endif +VERIFIC_SILIMATE_OBJS = ifeq ($(ENABLE_VERIFIC_SILIMATE_EXTENSIONS),1) CXXFLAGS += -DSILIMATE_VERIFIC_EXTENSIONS +VERIFIC_SILIMATE_OBJS += $(VERIFIC_DIR)/database/DBSilimate.o +VERIFIC_SILIMATE_OBJS += $(VERIFIC_DIR)/verilog/VeriSilimate.o endif ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1) VERIFIC_COMPONENTS += extensions @@ -574,6 +577,79 @@ LIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_C else LIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz endif + +# Silimate extension override objects: compile .cpp files and patch pre-compiled +# archives to localize overridden symbols, producing .a from .raw.a +ifeq ($(ENABLE_VERIFIC_SILIMATE_EXTENSIONS),1) + +$(VERIFIC_DIR)/database/DBSilimate.o: $(VERIFIC_DIR)/database/DBSilimate.cpp + $(P) $(CXX) -o $@ $(CPPFLAGS) $(CXXFLAGS) -c $< + +$(VERIFIC_DIR)/verilog/VeriSilimate.o: $(VERIFIC_DIR)/verilog/VeriSilimate.cpp + $(P) $(CXX) -o $@ $(CPPFLAGS) $(CXXFLAGS) -c $< + +ifeq ($(OS), Darwin) +VERIFIC_LIB_OS_SUFFIX = mac + +$(VERIFIC_DIR)/_override_syms.txt: $(VERIFIC_SILIMATE_OBJS) + $(Q) nm -gjU $^ | grep '^_' | sort -u > $@ + +$(VERIFIC_DIR)/database/database-mac.a: $(VERIFIC_DIR)/database/database-mac.raw.a $(VERIFIC_DIR)/_override_syms.txt + $(Q) cp $< $@ + $(Q) mkdir -p $@_patch_tmp + $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ + for o in *.o; do \ + nm -gjU "$$o" 2>/dev/null | grep -Fx -f $(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt > "$$o.syms" 2>/dev/null; \ + if [ -s "$$o.syms" ]; then nmedit -R "$$o.syms" "$$o"; fi; \ + rm -f "$$o.syms"; \ + done + $(Q) ar rcs $@ $@_patch_tmp/*.o + $(Q) rm -rf $@_patch_tmp + +$(VERIFIC_DIR)/verilog/verilog-mac.a: $(VERIFIC_DIR)/verilog/verilog-mac.raw.a $(VERIFIC_DIR)/_override_syms.txt + $(Q) cp $< $@ + $(Q) mkdir -p $@_patch_tmp + $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ + for o in *.o; do \ + nm -gjU "$$o" 2>/dev/null | grep -Fx -f $(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt > "$$o.syms" 2>/dev/null; \ + if [ -s "$$o.syms" ]; then nmedit -R "$$o.syms" "$$o"; fi; \ + rm -f "$$o.syms"; \ + done + $(Q) ar rcs $@ $@_patch_tmp/*.o + $(Q) rm -rf $@_patch_tmp + +else +VERIFIC_LIB_OS_SUFFIX = linux + +$(VERIFIC_DIR)/_override_syms.txt: $(VERIFIC_SILIMATE_OBJS) + $(Q) nm -g --defined-only $^ | awk '{print $$NF}' | sort -u > $@ + +$(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux.raw.a $(VERIFIC_DIR)/_override_syms.txt + $(Q) cp $< $@ + $(Q) mkdir -p $@_patch_tmp + $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ + for o in *.o; do \ + objcopy --localize-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ + done + $(Q) ar rcs $@ $@_patch_tmp/*.o + $(Q) rm -rf $@_patch_tmp + +$(VERIFIC_DIR)/verilog/verilog-linux.a: $(VERIFIC_DIR)/verilog/verilog-linux.raw.a $(VERIFIC_DIR)/_override_syms.txt + $(Q) cp $< $@ + $(Q) mkdir -p $@_patch_tmp + $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ + for o in *.o; do \ + objcopy --localize-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ + done + $(Q) ar rcs $@ $@_patch_tmp/*.o + $(Q) rm -rf $@_patch_tmp + +endif + +VERIFIC_PATCHED_ARCHIVES = $(VERIFIC_DIR)/database/database-$(VERIFIC_LIB_OS_SUFFIX).a $(VERIFIC_DIR)/verilog/verilog-$(VERIFIC_LIB_OS_SUFFIX).a + +endif # ENABLE_VERIFIC_SILIMATE_EXTENSIONS + endif ifeq ($(ENABLE_CCACHE),1) @@ -823,14 +899,14 @@ share: $(EXTRA_TARGETS) @echo " Share directory created." @echo "" -$(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) - $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(EXE_LIBS) $(LIBS) $(LIBS_VERIFIC) +$(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) $(VERIFIC_SILIMATE_OBJS) $(VERIFIC_PATCHED_ARCHIVES) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(VERIFIC_SILIMATE_OBJS) $(EXE_LIBS) $(LIBS) $(LIBS_VERIFIC) -libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) +libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) $(VERIFIC_SILIMATE_OBJS) $(VERIFIC_PATCHED_ARCHIVES) ifeq ($(OS), Darwin) - $(P) $(CXX) -o libyosys.so -shared -undefined dynamic_lookup -Wl,-install_name,libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -undefined dynamic_lookup -Wl,-install_name,libyosys.so $(LINKFLAGS) $(filter-out kernel/driver.o,$(OBJS)) $(VERIFIC_SILIMATE_OBJS) $(LIBS) $(LIBS_VERIFIC) else - $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,libyosys.so $(LINKFLAGS) $(filter-out kernel/driver.o,$(OBJS)) $(VERIFIC_SILIMATE_OBJS) $(LIBS) $(LIBS_VERIFIC) endif libyosys.a: $(filter-out kernel/driver.o,$(OBJS)) diff --git a/tests/verific/README.md b/tests/verific/README.md index a8d28f270..205d39eae 100644 --- a/tests/verific/README.md +++ b/tests/verific/README.md @@ -2,8 +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 diff --git a/tests/verific/import_warning_operator.ys b/tests/verific/import_warning_operator.ys new file mode 100644 index 000000000..1ecd6d296 --- /dev/null +++ b/tests/verific/import_warning_operator.ys @@ -0,0 +1,5 @@ +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 diff --git a/tests/verific/mixed_flist.ys.DISABLED b/tests/verific/mixed_flist.ys similarity index 100% rename from tests/verific/mixed_flist.ys.DISABLED rename to tests/verific/mixed_flist.ys diff --git a/verific b/verific index 1d26e0604..d62b81535 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 1d26e06044a35203790f3c9a9b0fbf069b512228 +Subproject commit d62b8153567305cbcb3d2e6b141b9cce422a4662 From 083eb8e5f193b4c6149375c01c65e1310fef7ae7 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 04:16:55 -0700 Subject: [PATCH 02/10] Try again --- tests/gen-tests-makefile.sh | 2 +- verific | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh index a0fb23ac3..66c86c440 100755 --- a/tests/gen-tests-makefile.sh +++ b/tests/gen-tests-makefile.sh @@ -92,7 +92,7 @@ generate_tests() { if [[ $do_sv = true ]]; then for x in *.sv; do if [ ! -f "${x%.sv}.ys" ]; then - generate_ys_test "$x" "-p \"prep -top top; async2sync; sat -enable_undef -verify -prove-asserts\" $yosys_args" + generate_ys_test "$x" "-p \"prep -top top; async2sync; select top; sat -enable_undef -verify -prove-asserts\" $yosys_args" fi; done fi; diff --git a/verific b/verific index d62b81535..0284e8560 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit d62b8153567305cbcb3d2e6b141b9cce422a4662 +Subproject commit 0284e8560e23dcf914213cb08e44041fbbbfd286 From 4b0d2bdd8de65aa67a652bf92e802ba5e9ee4448 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 10:39:54 -0700 Subject: [PATCH 03/10] Update Verific for Linux build --- verific | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verific b/verific index 0284e8560..052006b59 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 0284e8560e23dcf914213cb08e44041fbbbfd286 +Subproject commit 052006b591230179789359d75d702453e1832db7 From 0dc6bf07f3f332be4ea9995dc8f9fbe48311b5c8 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 10:47:05 -0700 Subject: [PATCH 04/10] Weaken symbols --- Makefile | 4 ++-- verific | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index e73570f57..4296017ce 100644 --- a/Makefile +++ b/Makefile @@ -629,7 +629,7 @@ $(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux $(Q) mkdir -p $@_patch_tmp $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ for o in *.o; do \ - objcopy --localize-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ + objcopy --weaken-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ done $(Q) ar rcs $@ $@_patch_tmp/*.o $(Q) rm -rf $@_patch_tmp @@ -639,7 +639,7 @@ $(VERIFIC_DIR)/verilog/verilog-linux.a: $(VERIFIC_DIR)/verilog/verilog-linux.raw $(Q) mkdir -p $@_patch_tmp $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ for o in *.o; do \ - objcopy --localize-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ + objcopy --weaken-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ done $(Q) ar rcs $@ $@_patch_tmp/*.o $(Q) rm -rf $@_patch_tmp diff --git a/verific b/verific index 052006b59..41e750a4a 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 052006b591230179789359d75d702453e1832db7 +Subproject commit 41e750a4a73c2f21083c921ded112221ea30a587 From 29024f215acebdfdf3e15cad6c5cd709fe8f69ae Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 11:05:14 -0700 Subject: [PATCH 05/10] Exclude weak symbols from overridden symbols --- Makefile | 2 +- verific | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 4296017ce..dbc71816e 100644 --- a/Makefile +++ b/Makefile @@ -622,7 +622,7 @@ else VERIFIC_LIB_OS_SUFFIX = linux $(VERIFIC_DIR)/_override_syms.txt: $(VERIFIC_SILIMATE_OBJS) - $(Q) nm -g --defined-only $^ | awk '{print $$NF}' | sort -u > $@ + $(Q) nm -g --defined-only $^ | awk '$$2 ~ /^[TDBR]$$/ {print $$NF}' | sort -u > $@ $(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux.raw.a $(VERIFIC_DIR)/_override_syms.txt $(Q) cp $< $@ diff --git a/verific b/verific index 41e750a4a..a38fbdb57 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 41e750a4a73c2f21083c921ded112221ea30a587 +Subproject commit a38fbdb575b50565f041f31909015c07e11020e5 From f1f38cd7658580a2e89d109cf0a58ef16c80a48f Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 11:20:26 -0700 Subject: [PATCH 06/10] Use multiple definition approach on Linux instead --- Makefile | 29 ++++++++--------------------- verific | 2 +- 2 files changed, 9 insertions(+), 22 deletions(-) diff --git a/Makefile b/Makefile index dbc71816e..b7925fe17 100644 --- a/Makefile +++ b/Makefile @@ -578,8 +578,11 @@ else LIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz endif -# Silimate extension override objects: compile .cpp files and patch pre-compiled -# archives to localize overridden symbols, producing .a from .raw.a +# Silimate extension override objects: compile .cpp files. On macOS we patch the +# pre-compiled archives (from .raw.a originals) to localize overridden symbols, +# since the macOS linker doesn't support --allow-multiple-definition. On Linux +# we just copy .raw.a to .a and rely on --allow-multiple-definition so override +# .o definitions (linked before the archives) take precedence. ifeq ($(ENABLE_VERIFIC_SILIMATE_EXTENSIONS),1) $(VERIFIC_DIR)/database/DBSilimate.o: $(VERIFIC_DIR)/database/DBSilimate.cpp @@ -620,29 +623,13 @@ $(VERIFIC_DIR)/verilog/verilog-mac.a: $(VERIFIC_DIR)/verilog/verilog-mac.raw.a $ else VERIFIC_LIB_OS_SUFFIX = linux +LINKFLAGS += -Wl,--allow-multiple-definition -$(VERIFIC_DIR)/_override_syms.txt: $(VERIFIC_SILIMATE_OBJS) - $(Q) nm -g --defined-only $^ | awk '$$2 ~ /^[TDBR]$$/ {print $$NF}' | sort -u > $@ - -$(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux.raw.a $(VERIFIC_DIR)/_override_syms.txt +$(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux.raw.a $(Q) cp $< $@ - $(Q) mkdir -p $@_patch_tmp - $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ - for o in *.o; do \ - objcopy --weaken-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ - done - $(Q) ar rcs $@ $@_patch_tmp/*.o - $(Q) rm -rf $@_patch_tmp -$(VERIFIC_DIR)/verilog/verilog-linux.a: $(VERIFIC_DIR)/verilog/verilog-linux.raw.a $(VERIFIC_DIR)/_override_syms.txt +$(VERIFIC_DIR)/verilog/verilog-linux.a: $(VERIFIC_DIR)/verilog/verilog-linux.raw.a $(Q) cp $< $@ - $(Q) mkdir -p $@_patch_tmp - $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ - for o in *.o; do \ - objcopy --weaken-symbols=$(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt "$$o" 2>/dev/null || true; \ - done - $(Q) ar rcs $@ $@_patch_tmp/*.o - $(Q) rm -rf $@_patch_tmp endif diff --git a/verific b/verific index a38fbdb57..f6114043e 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit a38fbdb575b50565f041f31909015c07e11020e5 +Subproject commit f6114043ecf341de28b3fca6f173a4aeee94ac24 From ae7caf4bf356e833846b18bcd8eeba35dfa06c22 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 11:37:20 -0700 Subject: [PATCH 07/10] Add back -no-pie --- verific | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verific b/verific index f6114043e..938cad4b0 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit f6114043ecf341de28b3fca6f173a4aeee94ac24 +Subproject commit 938cad4b0dbeac7dc97589ca0e48802fc1339118 From ed88ccd2fd2fb464df805d5fabbf85040459b50d Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 11:51:11 -0700 Subject: [PATCH 08/10] Add start/end group to fix linker issues --- verific | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verific b/verific index 938cad4b0..145e22d57 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 938cad4b0dbeac7dc97589ca0e48802fc1339118 +Subproject commit 145e22d578d6d854e89f4932a4683c154df2a5eb From 0ee2277d4f4551042a1e1659bb8d1892e753b009 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Thu, 16 Apr 2026 15:30:40 -0700 Subject: [PATCH 09/10] Use PIC Verific libraries --- verific | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verific b/verific index 145e22d57..fc343c990 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 145e22d578d6d854e89f4932a4683c154df2a5eb +Subproject commit fc343c9904855352fd8294bcd7209afcfca9bbbc From bf40364bd033ea178aae5191552051539aba04a9 Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Wed, 22 Apr 2026 03:12:26 -0700 Subject: [PATCH 10/10] No operator optimization, but it passes all tests --- Makefile | 24 +++++++++++++++++++++++- frontends/verific/verific.cc | 3 --- tests/gen-tests-makefile.sh | 2 +- tests/verific/README.md | 2 -- verific | 2 +- 5 files changed, 25 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index b7925fe17..dada0f7aa 100644 --- a/Makefile +++ b/Makefile @@ -558,6 +558,7 @@ ifeq ($(ENABLE_VERIFIC_SILIMATE_EXTENSIONS),1) CXXFLAGS += -DSILIMATE_VERIFIC_EXTENSIONS VERIFIC_SILIMATE_OBJS += $(VERIFIC_DIR)/database/DBSilimate.o VERIFIC_SILIMATE_OBJS += $(VERIFIC_DIR)/verilog/VeriSilimate.o +VERIFIC_SILIMATE_OBJS += $(VERIFIC_DIR)/util/UtilSilimate.o endif ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1) VERIFIC_COMPONENTS += extensions @@ -591,6 +592,9 @@ $(VERIFIC_DIR)/database/DBSilimate.o: $(VERIFIC_DIR)/database/DBSilimate.cpp $(VERIFIC_DIR)/verilog/VeriSilimate.o: $(VERIFIC_DIR)/verilog/VeriSilimate.cpp $(P) $(CXX) -o $@ $(CPPFLAGS) $(CXXFLAGS) -c $< +$(VERIFIC_DIR)/util/UtilSilimate.o: $(VERIFIC_DIR)/util/UtilSilimate.cpp + $(P) $(CXX) -o $@ $(CPPFLAGS) $(CXXFLAGS) -c $< + ifeq ($(OS), Darwin) VERIFIC_LIB_OS_SUFFIX = mac @@ -621,6 +625,18 @@ $(VERIFIC_DIR)/verilog/verilog-mac.a: $(VERIFIC_DIR)/verilog/verilog-mac.raw.a $ $(Q) ar rcs $@ $@_patch_tmp/*.o $(Q) rm -rf $@_patch_tmp +$(VERIFIC_DIR)/util/util-mac.a: $(VERIFIC_DIR)/util/util-mac.raw.a $(VERIFIC_DIR)/_override_syms.txt + $(Q) cp $< $@ + $(Q) mkdir -p $@_patch_tmp + $(Q) cd $@_patch_tmp && ar x $(CURDIR)/$@ && \ + for o in *.o; do \ + nm -gjU "$$o" 2>/dev/null | grep -Fx -f $(CURDIR)/$(VERIFIC_DIR)/_override_syms.txt > "$$o.syms" 2>/dev/null; \ + if [ -s "$$o.syms" ]; then nmedit -R "$$o.syms" "$$o"; fi; \ + rm -f "$$o.syms"; \ + done + $(Q) ar rcs $@ $@_patch_tmp/*.o + $(Q) rm -rf $@_patch_tmp + else VERIFIC_LIB_OS_SUFFIX = linux LINKFLAGS += -Wl,--allow-multiple-definition @@ -631,9 +647,15 @@ $(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux $(VERIFIC_DIR)/verilog/verilog-linux.a: $(VERIFIC_DIR)/verilog/verilog-linux.raw.a $(Q) cp $< $@ +$(VERIFIC_DIR)/util/util-linux.a: $(VERIFIC_DIR)/util/util-linux.raw.a + $(Q) cp $< $@ + endif -VERIFIC_PATCHED_ARCHIVES = $(VERIFIC_DIR)/database/database-$(VERIFIC_LIB_OS_SUFFIX).a $(VERIFIC_DIR)/verilog/verilog-$(VERIFIC_LIB_OS_SUFFIX).a +VERIFIC_PATCHED_ARCHIVES = \ + $(VERIFIC_DIR)/database/database-$(VERIFIC_LIB_OS_SUFFIX).a \ + $(VERIFIC_DIR)/verilog/verilog-$(VERIFIC_LIB_OS_SUFFIX).a \ + $(VERIFIC_DIR)/util/util-$(VERIFIC_LIB_OS_SUFFIX).a endif # ENABLE_VERIFIC_SILIMATE_EXTENSIONS diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 25f5928ff..a58842792 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -3223,9 +3223,6 @@ std::string verific_import(Design *design, const std::mapfirst.c_str()); nl->PostElaborationProcess(); - - log(" Running operator optimization for %s.\n", it->first.c_str()); - nl->OperatorOptimization(); } if (nl_done.count(it->first) == 0) { diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh index 66c86c440..a0fb23ac3 100755 --- a/tests/gen-tests-makefile.sh +++ b/tests/gen-tests-makefile.sh @@ -92,7 +92,7 @@ generate_tests() { if [[ $do_sv = true ]]; then for x in *.sv; do if [ ! -f "${x%.sv}.ys" ]; then - generate_ys_test "$x" "-p \"prep -top top; async2sync; select top; sat -enable_undef -verify -prove-asserts\" $yosys_args" + generate_ys_test "$x" "-p \"prep -top top; async2sync; sat -enable_undef -verify -prove-asserts\" $yosys_args" fi; done fi; diff --git a/tests/verific/README.md b/tests/verific/README.md index 205d39eae..aa4ce6ca1 100644 --- a/tests/verific/README.md +++ b/tests/verific/README.md @@ -2,8 +2,6 @@ ## Disabled - - - `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 diff --git a/verific b/verific index fc343c990..9280b3104 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit fc343c9904855352fd8294bcd7209afcfca9bbbc +Subproject commit 9280b31043881bbbc50bfedc74902b1f6debe81d