diff --git a/Makefile b/Makefile index 33519a233..dada0f7aa 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,12 @@ 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 +VERIFIC_SILIMATE_OBJS += $(VERIFIC_DIR)/util/UtilSilimate.o endif ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1) VERIFIC_COMPONENTS += extensions @@ -574,6 +578,87 @@ 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. 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 + $(P) $(CXX) -o $@ $(CPPFLAGS) $(CXXFLAGS) -c $< + +$(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 + +$(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 + +$(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 + +$(VERIFIC_DIR)/database/database-linux.a: $(VERIFIC_DIR)/database/database-linux.raw.a + $(Q) cp $< $@ + +$(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_DIR)/util/util-$(VERIFIC_LIB_OS_SUFFIX).a + +endif # ENABLE_VERIFIC_SILIMATE_EXTENSIONS + endif ifeq ($(ENABLE_CCACHE),1) @@ -823,14 +908,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/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/verific/README.md b/tests/verific/README.md index a8d28f270..aa4ce6ca1 100644 --- a/tests/verific/README.md +++ b/tests/verific/README.md @@ -2,8 +2,6 @@ ## 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..9280b3104 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 1d26e06044a35203790f3c9a9b0fbf069b512228 +Subproject commit 9280b31043881bbbc50bfedc74902b1f6debe81d