diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml index 28c17a6c0..b3a6bd846 100644 --- a/.github/workflows/test-linux.yml +++ b/.github/workflows/test-linux.yml @@ -86,7 +86,6 @@ jobs: run: | git clone https://github.com/steveicarus/iverilog.git cd iverilog - git checkout 192b6aec96fde982e6ddcb28b346d5893aa8e874 echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV - name: Cache iverilog diff --git a/.github/workflows/test-macos.yml b/.github/workflows/test-macos.yml index 17e2ae331..8ca658c39 100644 --- a/.github/workflows/test-macos.yml +++ b/.github/workflows/test-macos.yml @@ -16,7 +16,7 @@ jobs: steps: - name: Install Dependencies run: | - brew install bison flex gawk libffi pkg-config bash + HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1 brew install bison flex gawk libffi pkg-config bash - name: Runtime environment shell: bash @@ -42,7 +42,6 @@ jobs: run: | git clone https://github.com/steveicarus/iverilog.git cd iverilog - git checkout 192b6aec96fde982e6ddcb28b346d5893aa8e874 echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV - name: Cache iverilog diff --git a/CHANGELOG b/CHANGELOG index ed91d5e7c..b172988d5 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,9 +2,30 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.38 .. Yosys 0.39-dev +Yosys 0.39 .. Yosys 0.40-dev -------------------------- +Yosys 0.38 .. Yosys 0.39 +-------------------------- + * New commands and options + - Added option "-extra-map" to "synth" pass. + - Added option "-dont_use" to "dfflibmap" pass. + - Added option "-href" to "show" command. + - Added option "-noscopeinfo" to "flatten" pass. + - Added option "-scopename" to "flatten" pass. + + * SystemVerilog + - Added support for packed multidimensional arrays. + + * Various + - Added "$scopeinfo" cells to preserve information about + the hierarchy during flattening. + - Added sequential area output to "stat -liberty". + - Added ability to record/replay diagnostics in cxxrtl backend. + + * Verific support + - Added attributes to module instantiation. + Yosys 0.37 .. Yosys 0.38 -------------------------- * New commands and options diff --git a/Makefile b/Makefile index 57e37351c..55941c8c3 100644 --- a/Makefile +++ b/Makefile @@ -92,14 +92,14 @@ VPATH := $(YOSYS_SRC) CXXSTD ?= c++11 CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include -LDLIBS := $(LDLIBS) -lstdc++ -lm -PLUGIN_LDFLAGS := -PLUGIN_LDLIBS := -EXE_LDFLAGS := +LIBS := $(LIBS) -lstdc++ -lm +PLUGIN_LINKFLAGS := +PLUGIN_LIBS := +EXE_LINKFLAGS := ifeq ($(OS), MINGW) -EXE_LDFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a -PLUGIN_LDFLAGS += -L"$(LIBDIR)" -PLUGIN_LDLIBS := -lyosys_exe +EXE_LINKFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a +PLUGIN_LINKFLAGS += -L"$(LIBDIR)" +PLUGIN_LIBS := -lyosys_exe endif PKG_CONFIG ?= pkg-config @@ -109,7 +109,7 @@ STRIP ?= strip AWK ?= awk ifeq ($(OS), Darwin) -PLUGIN_LDFLAGS += -undefined dynamic_lookup +PLUGIN_LINKFLAGS += -undefined dynamic_lookup # homebrew search paths ifneq ($(shell :; command -v brew),) @@ -117,10 +117,10 @@ BREW_PREFIX := $(shell brew --prefix)/opt $(info $$BREW_PREFIX is [${BREW_PREFIX}]) ifeq ($(ENABLE_PYOSYS),1) CXXFLAGS += -I$(BREW_PREFIX)/boost/include/boost -LDFLAGS += -L$(BREW_PREFIX)/boost/lib +LINKFLAGS += -L$(BREW_PREFIX)/boost/lib endif CXXFLAGS += -I$(BREW_PREFIX)/readline/include -LDFLAGS += -L$(BREW_PREFIX)/readline/lib +LINKFLAGS += -L$(BREW_PREFIX)/readline/lib PKG_CONFIG_PATH := $(BREW_PREFIX)/libffi/lib/pkgconfig:$(PKG_CONFIG_PATH) PKG_CONFIG_PATH := $(BREW_PREFIX)/tcl-tk/lib/pkgconfig:$(PKG_CONFIG_PATH) export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX)/flex/bin:$(PATH) @@ -129,19 +129,19 @@ export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX else ifneq ($(shell :; command -v port),) PORT_PREFIX := $(patsubst %/bin/port,%,$(shell :; command -v port)) CXXFLAGS += -I$(PORT_PREFIX)/include -LDFLAGS += -L$(PORT_PREFIX)/lib +LINKFLAGS += -L$(PORT_PREFIX)/lib PKG_CONFIG_PATH := $(PORT_PREFIX)/lib/pkgconfig:$(PKG_CONFIG_PATH) export PATH := $(PORT_PREFIX)/bin:$(PATH) endif else -LDFLAGS += -rdynamic +LINKFLAGS += -rdynamic ifneq ($(OS), OpenBSD) -LDLIBS += -lrt +LIBS += -lrt endif endif -YOSYS_VER := 0.38+46 +YOSYS_VER := 0.39+0 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -157,7 +157,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 543faed.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 0033808.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -165,7 +165,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 896e5e7 +ABCREV = 0cd90d0 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) @@ -215,41 +215,38 @@ ABC_ARCHFLAGS += "-DABC_NO_RLIMIT" endif ifeq ($(CONFIG),clang) -CXX = clang -LD = clang++ +CXX = clang++ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -Wno-c++11-narrowing $(ABC_ARCHFLAGS)" ifneq ($(SANITIZER),) $(info [Clang Sanitizer] $(SANITIZER)) CXXFLAGS += -g -O1 -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize=$(SANITIZER) -LDFLAGS += -g -fsanitize=$(SANITIZER) +LINKFLAGS += -g -fsanitize=$(SANITIZER) ifneq ($(findstring address,$(SANITIZER)),) ENABLE_COVER := 0 endif ifneq ($(findstring memory,$(SANITIZER)),) CXXFLAGS += -fPIE -fsanitize-memory-track-origins -LDFLAGS += -fPIE -fsanitize-memory-track-origins +LINKFLAGS += -fPIE -fsanitize-memory-track-origins endif ifneq ($(findstring cfi,$(SANITIZER)),) CXXFLAGS += -flto -LDFLAGS += -flto +LINKFLAGS += -flto endif endif else ifeq ($(CONFIG),gcc) -CXX = gcc -LD = gcc +CXX = g++ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" else ifeq ($(CONFIG),gcc-static) -LD = $(CXX) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -static -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -static +LIBS := $(filter-out -lrt,$(LIBS)) CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) CXXFLAGS += -std=$(CXXSTD) -Os -ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(LD)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ +ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(CXX)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ ARCHFLAGS="-DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING=1 -Wno-unused-but-set-variable $(ARCHFLAGS)" ABC_USE_NO_READLINE=1 ifeq ($(DISABLE_ABC_THREADS),1) ABCMKARGS += "ABC_USE_NO_PTHREADS=1" @@ -257,31 +254,28 @@ endif else ifeq ($(CONFIG),afl-gcc) CXX = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc -LD = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),cygwin) -CXX = gcc -LD = gcc +CXX = g++ CXXFLAGS += -std=gnu++11 -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),emcc) CXX = emcc -LD = emcc CXXFLAGS := -std=$(CXXSTD) $(filter-out -fPIC -ggdb,$(CXXFLAGS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8 -Wno-c++11-narrowing" EMCC_CXXFLAGS := -Os -Wno-warn-absolute-paths -EMCC_LDFLAGS := --memory-init-file 0 --embed-file share -EMCC_LDFLAGS += -s NO_EXIT_RUNTIME=1 -EMCC_LDFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" -EMCC_LDFLAGS += -s TOTAL_MEMORY=134217728 -EMCC_LDFLAGS += -s EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' +EMCC_LINKFLAGS := --embed-file share +EMCC_LINKFLAGS += -s NO_EXIT_RUNTIME=1 +EMCC_LINKFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" +EMCC_LINKFLAGS += -s TOTAL_MEMORY=134217728 +EMCC_LINKFLAGS += -s EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' # https://github.com/kripken/emscripten/blob/master/src/settings.js CXXFLAGS += $(EMCC_CXXFLAGS) -LDFLAGS += $(EMCC_LDFLAGS) -LDLIBS = +LINKFLAGS += $(EMCC_LINKFLAGS) +LIBS = EXE = .js DISABLE_SPAWN := 1 @@ -309,21 +303,19 @@ yosys.html: misc/yosys.html else ifeq ($(CONFIG),wasi) ifeq ($(WASI_SDK),) -CXX = clang -LD = clang++ +CXX = clang++ AR = llvm-ar RANLIB = llvm-ranlib WASIFLAGS := -target wasm32-wasi --sysroot $(WASI_SYSROOT) $(WASIFLAGS) else -CXX = $(WASI_SDK)/bin/clang -LD = $(WASI_SDK)/bin/clang++ +CXX = $(WASI_SDK)/bin/clang++ AR = $(WASI_SDK)/bin/ar RANLIB = $(WASI_SDK)/bin/ranlib WASIFLAGS := --sysroot $(WASI_SDK)/share/wasi-sysroot $(WASIFLAGS) endif CXXFLAGS := $(WASIFLAGS) -std=$(CXXSTD) -Os -D_WASI_EMULATED_PROCESS_CLOCKS $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LDFLAGS)) -LDLIBS := -lwasi-emulated-process-clocks $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LINKFLAGS)) +LIBS := -lwasi-emulated-process-clocks $(filter-out -lrt,$(LIBS)) ABCMKARGS += AR="$(AR)" RANLIB="$(RANLIB)" ABCMKARGS += ARCHFLAGS="$(WASIFLAGS) -D_WASI_EMULATED_PROCESS_CLOCKS -DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING -DABC_NO_RLIMIT -Wno-c++11-narrowing" ABCMKARGS += OPTFLAGS="-Os" @@ -339,34 +331,31 @@ endif else ifeq ($(CONFIG),mxe) PKG_CONFIG = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-pkg-config CXX = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ -LD = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s +LIBS := $(filter-out -lrt,$(LIBS)) ABCMKARGS += ARCHFLAGS="-DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" # TODO: Try to solve pthread linking issue in more appropriate way -ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" LDFLAGS="-Wl,--allow-multiple-definition" ABC_USE_NO_READLINE=1 CC="/usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-gcc" +ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" LINKFLAGS="-Wl,--allow-multiple-definition" ABC_USE_NO_READLINE=1 CC="/usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-gcc" EXE = .exe else ifeq ($(CONFIG),msys2-32) CXX = i686-w64-mingw32-g++ -LD = i686-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s +LIBS := $(filter-out -lrt,$(LIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe else ifeq ($(CONFIG),msys2-64) CXX = x86_64-w64-mingw32-g++ -LD = x86_64-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s -LDLIBS := $(filter-out -lrt,$(LDLIBS)) +LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s +LIBS := $(filter-out -lrt,$(LIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe @@ -393,9 +382,9 @@ ifeq ($(BOOST_PYTHON_LIB),) $(error BOOST_PYTHON_LIB could not be detected. Please define manually) endif -LDLIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem -# python-config --ldflags includes LDLIBS for some reason -LDFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags)) +LIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem +# python-config --ldflags includes LIBS for some reason +LINKFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags)) CXXFLAGS += $(shell $(PYTHON_CONFIG) --includes) -DWITH_PYTHON PY_WRAPPER_FILE = kernel/python_wrappers @@ -409,22 +398,22 @@ CXXFLAGS += -DYOSYS_ENABLE_READLINE ifeq ($(OS), $(filter $(OS),FreeBSD OpenBSD NetBSD)) CXXFLAGS += -I/usr/local/include endif -LDLIBS += -lreadline +LIBS += -lreadline ifeq ($(LINK_CURSES),1) -LDLIBS += -lcurses +LIBS += -lcurses ABCMKARGS += "ABC_READLINE_LIBRARIES=-lcurses -lreadline" endif ifeq ($(LINK_TERMCAP),1) -LDLIBS += -ltermcap +LIBS += -ltermcap ABCMKARGS += "ABC_READLINE_LIBRARIES=-lreadline -ltermcap" endif ifeq ($(CONFIG),mxe) -LDLIBS += -ltermcap +LIBS += -ltermcap endif else ifeq ($(ENABLE_EDITLINE),1) CXXFLAGS += -DYOSYS_ENABLE_EDITLINE -LDLIBS += -ledit -ltinfo -lbsd +LIBS += -ledit -ltinfo -lbsd else ABCMKARGS += "ABC_USE_NO_READLINE=1" endif @@ -443,9 +432,9 @@ CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-e ifeq ($(OS), MINGW) CXXFLAGS += -Ilibs/dlfcn-win32 endif -LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) +LIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) ifneq ($(OS), $(filter $(OS),FreeBSD OpenBSD NetBSD MINGW)) -LDLIBS += -ldl +LIBS += -ldl endif endif @@ -455,7 +444,7 @@ endif ifeq ($(ENABLE_ZLIB),1) CXXFLAGS += -DYOSYS_ENABLE_ZLIB -LDLIBS += -lz +LIBS += -lz endif @@ -472,21 +461,21 @@ endif ifeq ($(CONFIG),mxe) CXXFLAGS += -DYOSYS_ENABLE_TCL -LDLIBS += -ltcl86 -lwsock32 -lws2_32 -lnetapi32 -lz -luserenv +LIBS += -ltcl86 -lwsock32 -lws2_32 -lnetapi32 -lz -luserenv else CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags tcl || echo -I$(TCL_INCLUDE)) -DYOSYS_ENABLE_TCL -LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo $(TCL_LIBS)) +LIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo $(TCL_LIBS)) endif endif ifeq ($(ENABLE_GCOV),1) CXXFLAGS += --coverage -LDFLAGS += --coverage +LINKFLAGS += --coverage endif ifeq ($(ENABLE_GPROF),1) CXXFLAGS += -pg -LDFLAGS += -pg +LINKFLAGS += -pg endif ifeq ($(ENABLE_NDEBUG),1) @@ -506,7 +495,7 @@ CXXFLAGS += -DYOSYS_ENABLE_ABC ifeq ($(LINK_ABC),1) CXXFLAGS += -DYOSYS_LINK_ABC ifeq ($(DISABLE_ABC_THREADS),0) -LDLIBS += -lpthread +LIBS += -lpthread endif else ifeq ($(ABCEXTERNAL),) @@ -520,10 +509,10 @@ GHDL_PREFIX ?= $(PREFIX) GHDL_INCLUDE_DIR ?= $(GHDL_PREFIX)/include GHDL_LIB_DIR ?= $(GHDL_PREFIX)/lib CXXFLAGS += -I$(GHDL_INCLUDE_DIR) -DYOSYS_ENABLE_GHDL -LDLIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link) +LIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link) endif -LDLIBS_VERIFIC = +LIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= /usr/local/src/verific_lib VERIFIC_COMPONENTS ?= verilog database util containers hier_tree @@ -549,9 +538,9 @@ CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS endif CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC ifeq ($(OS), Darwin) -LDLIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz +LIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz else -LDLIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz +LIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz endif endif @@ -648,12 +637,6 @@ $(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)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h)) OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o OBJS += kernel/binding.o @@ -752,13 +735,13 @@ yosys.js: $(filter-out yosysjs-$(YOSYS_VER).zip,$(EXTRA_TARGETS)) endif $(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) - $(P) $(LD) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(LIBS) $(LIBS_VERIFIC) libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) ifeq ($(OS), Darwin) - $(P) $(LD) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) else - $(P) $(LD) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) + $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) endif %.o: %.cc @@ -767,7 +750,7 @@ endif %.pyh: %.h $(Q) mkdir -p $(dir $@) - $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) $(CXXFLAGS) -x c++ -o $@ -E -P - + $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(CXX) $(CXXFLAGS) -x c++ -o $@ -E -P - ifeq ($(ENABLE_PYOSYS),1) $(PY_WRAPPER_FILE).cc: misc/$(PY_GEN_SCRIPT).py $(PY_WRAP_INCLUDES) @@ -788,15 +771,15 @@ kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile ifeq ($(ENABLE_VERIFIC),1) CXXFLAGS_NOVERIFIC = $(foreach v,$(CXXFLAGS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) -LDLIBS_NOVERIFIC = $(foreach v,$(LDLIBS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) +LIBS_NOVERIFIC = $(foreach v,$(LIBS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) else CXXFLAGS_NOVERIFIC = $(CXXFLAGS) -LDLIBS_NOVERIFIC = $(LDLIBS) +LIBS_NOVERIFIC = $(LIBS) endif $(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in $(P) $(SED) -e 's#@CXXFLAGS@#$(subst -Ilibs/dlfcn-win32,,$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(strip $(CXXFLAGS_NOVERIFIC))))#;' \ - -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LDFLAGS@#$(strip $(LDFLAGS) $(PLUGIN_LDFLAGS))#;' -e 's#@LDLIBS@#$(strip $(LDLIBS_NOVERIFIC) $(PLUGIN_LDLIBS))#;' \ + -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LINKFLAGS@#$(strip $(LINKFLAGS) $(PLUGIN_LINKFLAGS))#;' -e 's#@LIBS@#$(strip $(LIBS_NOVERIFIC) $(PLUGIN_LIBS))#;' \ -e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > $(PROGRAM_PREFIX)yosys-config $(Q) chmod +x $(PROGRAM_PREFIX)yosys-config @@ -935,7 +918,7 @@ ystests: $(TARGETS) $(EXTRA_TARGETS) # Unit test unit-test: libyosys.so @$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CPPFLAGS="$(CPPFLAGS)" \ - CXXFLAGS="$(CXXFLAGS)" LDLIBS="$(LDLIBS)" ROOTPATH="$(CURDIR)" + CXXFLAGS="$(CXXFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)" clean-unit-test: @$(MAKE) -C $(UNITESTPATH) clean diff --git a/README.md b/README.md index 3be1b4c2e..660bd5c6d 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ ``` yosys -- Yosys Open SYnthesis Suite -Copyright (C) 2012 - 2020 Claire Xenia Wolf +Copyright (C) 2012 - 2024 Claire Xenia Wolf Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index fe4f7681d..f2cb5d9bc 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -67,6 +67,8 @@ struct AigerWriter int initstate_ff = 0; dict ywmap_clocks; + vector ywmap_asserts; + vector ywmap_assumes; int mkgate(int a0, int a1) { @@ -269,6 +271,7 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); asserts.push_back(make_pair(A, EN)); + ywmap_asserts.push_back(cell); continue; } @@ -279,6 +282,7 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); assumes.push_back(make_pair(A, EN)); + ywmap_assumes.push_back(cell); continue; } @@ -852,6 +856,19 @@ struct AigerWriter for (auto &it : init_lines) json.value(it.second); json.end_array(); + + json.name("asserts"); + json.begin_array(); + for (Cell *cell : ywmap_asserts) + json.value(witness_path(cell)); + json.end_array(); + + json.name("assumes"); + json.begin_array(); + for (Cell *cell : ywmap_assumes) + json.value(witness_path(cell)); + json.end_array(); + json.end_object(); } diff --git a/backends/cxxrtl/Makefile.inc b/backends/cxxrtl/Makefile.inc index aaa304502..dd77d2ad3 100644 --- a/backends/cxxrtl/Makefile.inc +++ b/backends/cxxrtl/Makefile.inc @@ -1,2 +1,11 @@ OBJS += backends/cxxrtl/cxxrtl_backend.o + +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_time.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc)) +$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h)) diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index c60b43d3f..877a829d3 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -25,6 +25,7 @@ #include "kernel/mem.h" #include "kernel/log.h" #include "kernel/fmt.h" +#include "kernel/scopeinfo.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -1518,8 +1519,9 @@ struct CxxrtlWorker { } else if (is_internal_cell(cell->type)) { log_cmd_error("Unsupported internal cell `%s'.\n", cell->type.c_str()); // User cells + } else if (for_debug) { + // Outlines are called on demand when computing the value of a debug item. Nothing to do here. } else { - log_assert(!for_debug); log_assert(cell->known()); bool buffered_inputs = false; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; @@ -2310,11 +2312,14 @@ struct CxxrtlWorker { dict attributes = object->attributes; // Inherently necessary to get access to the object, so a waste of space to emit. attributes.erase(ID::hdlname); + // Internal Yosys attribute that should be removed but isn't. + attributes.erase(ID::module_not_derived); dump_metadata_map(attributes); } void dump_debug_info_method(RTLIL::Module *module) { + size_t count_scopes = 0; size_t count_public_wires = 0; size_t count_member_wires = 0; size_t count_undriven = 0; @@ -2327,153 +2332,188 @@ struct CxxrtlWorker { size_t count_skipped_wires = 0; inc_indent(); f << indent << "assert(path.empty() || path[path.size() - 1] == ' ');\n"; - for (auto wire : module->wires()) { - const auto &debug_wire_type = debug_wire_types[wire]; - if (!wire->name.isPublic()) - continue; - count_public_wires++; - switch (debug_wire_type.type) { - case WireType::BUFFERED: - case WireType::MEMBER: { - // Member wire - std::vector flags; - - if (wire->port_input && wire->port_output) - flags.push_back("INOUT"); - else if (wire->port_output) - flags.push_back("OUTPUT"); - else if (wire->port_input) - flags.push_back("INPUT"); - - bool has_driven_sync = false; - bool has_driven_comb = false; - bool has_undriven = false; - if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { - for (auto bit : SigSpec(wire)) - if (!bit_has_state.count(bit)) - has_undriven = true; - else if (bit_has_state[bit]) - has_driven_sync = true; - else - has_driven_comb = true; - } else if (wire->port_output) { - switch (cxxrtl_port_type(module, wire->name)) { - case CxxrtlPortType::SYNC: - has_driven_sync = true; - break; - case CxxrtlPortType::COMB: - has_driven_comb = true; - break; - case CxxrtlPortType::UNKNOWN: - has_driven_sync = has_driven_comb = true; - break; - } - } else { - has_undriven = true; - } - if (has_undriven) - flags.push_back("UNDRIVEN"); - if (!has_driven_sync && !has_driven_comb && has_undriven) - count_undriven++; - if (has_driven_sync) - flags.push_back("DRIVEN_SYNC"); - if (has_driven_sync && !has_driven_comb && !has_undriven) - count_driven_sync++; - if (has_driven_comb) - flags.push_back("DRIVEN_COMB"); - if (!has_driven_sync && has_driven_comb && !has_undriven) - count_driven_comb++; - if (has_driven_sync + has_driven_comb + has_undriven > 1) - count_mixed_driver++; - - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset; - bool first = true; - for (auto flag : flags) { - if (first) { - first = false; - f << ", "; - } else { - f << "|"; - } - f << "debug_item::" << flag; - } - f << "), "; - dump_debug_attrs(wire); + f << indent << "if (scopes) {\n"; + inc_indent(); + // The module is responsible for adding its own scope. + f << indent << "scopes->add(path.empty() ? path : path.substr(0, path.size() - 1), "; + f << escape_cxx_string(get_hdl_name(module)) << ", "; + dump_debug_attrs(module); + f << ", std::move(cell_attrs));\n"; + count_scopes++; + // If there were any submodules that were flattened, the module is also responsible for adding them. + for (auto cell : module->cells()) { + if (cell->type != ID($scopeinfo)) continue; + if (cell->getParam(ID::TYPE).decode_string() == "module") { + auto module_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Module); + auto cell_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Cell); + cell_attrs.erase(ID::module_not_derived); + f << indent << "scopes->add(path + " << escape_cxx_string(get_hdl_name(cell)) << ", "; + f << escape_cxx_string(cell->get_string_attribute(ID(module))) << ", "; + dump_metadata_map(module_attrs); + f << ", "; + dump_metadata_map(cell_attrs); f << ");\n"; - count_member_wires++; - break; - } - case WireType::ALIAS: { - // Alias of a member wire - const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item("; - // If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream - // tooling has no way to find out about the outline. - if (debug_wire_types[aliasee].is_outline()) - f << "debug_eval_outline"; - else - f << "debug_alias()"; - f << ", " << mangle(aliasee) << ", " << wire->start_offset << "), "; - dump_debug_attrs(aliasee); - f << ");\n"; - count_alias_wires++; - break; - } - case WireType::CONST: { - // Wire tied to a constant - f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; - dump_const(debug_wire_type.sig_subst.as_const()); - f << ";\n"; - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "), "; - dump_debug_attrs(wire); - f << ");\n"; - count_const_wires++; - break; - } - case WireType::OUTLINE: { - // Localized or inlined, but rematerializable wire - f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(debug_eval_outline, " << mangle(wire) << ", " << wire->start_offset << "), "; - dump_debug_attrs(wire); - f << ");\n"; - count_inline_wires++; - break; - } - default: { - // Localized or inlined wire with no debug information - count_skipped_wires++; - break; - } + } else log_assert(false && "Unknown $scopeinfo type"); + count_scopes++; } - } - if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { - for (auto &mem : mod_memories[module]) { - if (!mem.memid.isPublic()) + dec_indent(); + f << indent << "}\n"; + f << indent << "if (items) {\n"; + inc_indent(); + for (auto wire : module->wires()) { + const auto &debug_wire_type = debug_wire_types[wire]; + if (!wire->name.isPublic()) continue; - f << indent << "items.add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)); - f << ", debug_item(" << mangle(&mem) << ", "; - f << mem.start_offset << "), "; - if (mem.packed) { - dump_debug_attrs(mem.cell); - } else { - dump_debug_attrs(mem.mem); + count_public_wires++; + switch (debug_wire_type.type) { + case WireType::BUFFERED: + case WireType::MEMBER: { + // Member wire + std::vector flags; + + if (wire->port_input && wire->port_output) + flags.push_back("INOUT"); + else if (wire->port_output) + flags.push_back("OUTPUT"); + else if (wire->port_input) + flags.push_back("INPUT"); + + bool has_driven_sync = false; + bool has_driven_comb = false; + bool has_undriven = false; + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { + for (auto bit : SigSpec(wire)) + if (!bit_has_state.count(bit)) + has_undriven = true; + else if (bit_has_state[bit]) + has_driven_sync = true; + else + has_driven_comb = true; + } else if (wire->port_output) { + switch (cxxrtl_port_type(module, wire->name)) { + case CxxrtlPortType::SYNC: + has_driven_sync = true; + break; + case CxxrtlPortType::COMB: + has_driven_comb = true; + break; + case CxxrtlPortType::UNKNOWN: + has_driven_sync = has_driven_comb = true; + break; + } + } else { + has_undriven = true; + } + if (has_undriven) + flags.push_back("UNDRIVEN"); + if (!has_driven_sync && !has_driven_comb && has_undriven) + count_undriven++; + if (has_driven_sync) + flags.push_back("DRIVEN_SYNC"); + if (has_driven_sync && !has_driven_comb && !has_undriven) + count_driven_sync++; + if (has_driven_comb) + flags.push_back("DRIVEN_COMB"); + if (!has_driven_sync && has_driven_comb && !has_undriven) + count_driven_comb++; + if (has_driven_sync + has_driven_comb + has_undriven > 1) + count_mixed_driver++; + + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset; + bool first = true; + for (auto flag : flags) { + if (first) { + first = false; + f << ", "; + } else { + f << "|"; + } + f << "debug_item::" << flag; + } + f << "), "; + dump_debug_attrs(wire); + f << ");\n"; + count_member_wires++; + break; + } + case WireType::ALIAS: { + // Alias of a member wire + const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item("; + // If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream + // tooling has no way to find out about the outline. + if (debug_wire_types[aliasee].is_outline()) + f << "debug_eval_outline"; + else + f << "debug_alias()"; + f << ", " << mangle(aliasee) << ", " << wire->start_offset << "), "; + dump_debug_attrs(aliasee); + f << ");\n"; + count_alias_wires++; + break; + } + case WireType::CONST: { + // Wire tied to a constant + f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; + dump_const(debug_wire_type.sig_subst.as_const()); + f << ";\n"; + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "), "; + dump_debug_attrs(wire); + f << ");\n"; + count_const_wires++; + break; + } + case WireType::OUTLINE: { + // Localized or inlined, but rematerializable wire + f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(debug_eval_outline, " << mangle(wire) << ", " << wire->start_offset << "), "; + dump_debug_attrs(wire); + f << ");\n"; + count_inline_wires++; + break; + } + default: { + // Localized or inlined wire with no debug information + count_skipped_wires++; + break; + } } - f << ");\n"; } + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { + for (auto &mem : mod_memories[module]) { + if (!mem.memid.isPublic()) + continue; + f << indent << "items->add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)); + f << ", debug_item(" << mangle(&mem) << ", "; + f << mem.start_offset << "), "; + if (mem.packed) { + dump_debug_attrs(mem.cell); + } else { + dump_debug_attrs(mem.mem); + } + f << ");\n"; + } + } + dec_indent(); + f << indent << "}\n"; + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { for (auto cell : module->cells()) { if (is_internal_cell(cell->type)) continue; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; - f << indent << mangle(cell) << access << "debug_info(items, "; - f << "path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ");\n"; + f << indent << mangle(cell) << access; + f << "debug_info(items, scopes, path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ", "; + dump_debug_attrs(cell); + f << ");\n"; } } dec_indent(); log_debug("Debug information statistics for module `%s':\n", log_id(module)); + log_debug(" Scopes: %zu", count_scopes); log_debug(" Public wires: %zu, of which:\n", count_public_wires); log_debug(" Member wires: %zu, of which:\n", count_member_wires); log_debug(" Undriven: %zu (incl. inputs)\n", count_undriven); @@ -2511,18 +2551,18 @@ struct CxxrtlWorker { dump_eval_method(module); f << indent << "}\n"; f << "\n"; - f << indent << "template\n"; - f << indent << "bool commit(ObserverT &observer) {\n"; + f << indent << "virtual bool commit(observer &observer) {\n"; dump_commit_method(module); f << indent << "}\n"; f << "\n"; f << indent << "bool commit() override {\n"; f << indent << indent << "observer observer;\n"; - f << indent << indent << "return commit<>(observer);\n"; + f << indent << indent << "return commit(observer);\n"; f << indent << "}\n"; if (debug_info) { f << "\n"; - f << indent << "void debug_info(debug_items &items, std::string path = \"\") override {\n"; + f << indent << "void debug_info(debug_items *items, debug_scopes *scopes, " + << "std::string path, metadata_map &&cell_attrs = {}) override {\n"; dump_debug_info_method(module); f << indent << "}\n"; } @@ -2631,7 +2671,8 @@ struct CxxrtlWorker { } } f << "\n"; - f << indent << "void debug_info(debug_items &items, std::string path = \"\") override;\n"; + f << indent << "void debug_info(debug_items *items, debug_scopes *scopes, " + << "std::string path, metadata_map &&cell_attrs = {}) override;\n"; } dec_indent(); f << indent << "}; // struct " << mangle(module) << "\n"; @@ -2659,7 +2700,8 @@ struct CxxrtlWorker { } f << "\n"; f << indent << "CXXRTL_EXTREMELY_COLD\n"; - f << indent << "void " << mangle(module) << "::debug_info(debug_items &items, std::string path) {\n"; + f << indent << "void " << mangle(module) << "::debug_info(debug_items *items, debug_scopes *scopes, " + << "std::string path, metadata_map &&cell_attrs) {\n"; dump_debug_info_method(module); f << indent << "}\n"; } @@ -3421,8 +3463,7 @@ struct CxxrtlBackend : public Backend { log(" wire<8> p_o_data;\n"); log("\n"); log(" bool eval(performer *performer) override;\n"); - log(" template\n"); - log(" bool commit(ObserverT &observer);\n"); + log(" virtual bool commit(observer &observer);\n"); log(" bool commit() override;\n"); log("\n"); log(" static std::unique_ptr\n"); diff --git a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc index 593e067a1..3c62401dd 100644 --- a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc +++ b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc @@ -35,19 +35,19 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design) { return cxxrtl_create_at(design, ""); } -cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *root) { - std::string path = root; - if (!path.empty()) { +cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path_) { + std::string top_path = top_path_; + if (!top_path.empty()) { // module::debug_info() accepts either an empty path, or a path ending in space to simplify // the logic in generated code. While this is sketchy at best to expose in the C++ API, this // would be a lot worse in the C API, so don't expose it here. - assert(path.back() != ' '); - path += ' '; + assert(top_path.back() != ' '); + top_path += ' '; } cxxrtl_handle handle = new _cxxrtl_handle; handle->module = std::move(design->module); - handle->module->debug_info(handle->objects, path); + handle->module->debug_info(handle->objects, top_path); delete design; return handle; } diff --git a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h index c2a9d37e1..ae42733ad 100644 --- a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h +++ b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h @@ -55,8 +55,8 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design); // Create a design handle at a given hierarchy position from a design toplevel. // // This operation is similar to `cxxrtl_create`, except the full hierarchical name of every object -// is prepended with `root`. -cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *root); +// is prepended with `top_path`. +cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path); // Release all resources used by a design and its handle. void cxxrtl_destroy(cxxrtl_handle handle); diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h index f9d22ff9b..b834cd120 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h @@ -1331,14 +1331,15 @@ struct debug_items { std::map> table; std::map> attrs_table; - void add(const std::string &name, debug_item &&item, metadata_map &&item_attrs = {}) { - std::unique_ptr &attrs = attrs_table[name]; + void add(const std::string &path, debug_item &&item, metadata_map &&item_attrs = {}) { + assert((path.empty() || path[path.size() - 1] != ' ') && path.find(" ") == std::string::npos); + std::unique_ptr &attrs = attrs_table[path]; if (attrs.get() == nullptr) attrs = std::unique_ptr(new debug_attrs); for (auto attr : item_attrs) attrs->map.insert(attr); item.attrs = attrs.get(); - std::vector &parts = table[name]; + std::vector &parts = table[path]; parts.emplace_back(item); std::sort(parts.begin(), parts.end(), [](const debug_item &a, const debug_item &b) { @@ -1346,25 +1347,58 @@ struct debug_items { }); } - size_t count(const std::string &name) const { - if (table.count(name) == 0) + size_t count(const std::string &path) const { + if (table.count(path) == 0) return 0; - return table.at(name).size(); + return table.at(path).size(); } - const std::vector &at(const std::string &name) const { - return table.at(name); + const std::vector &at(const std::string &path) const { + return table.at(path); } // Like `at()`, but operates only on single-part debug items. - const debug_item &operator [](const std::string &name) const { - const std::vector &parts = table.at(name); + const debug_item &operator [](const std::string &path) const { + const std::vector &parts = table.at(path); assert(parts.size() == 1); return parts.at(0); } - const metadata_map &attrs(const std::string &name) const { - return attrs_table.at(name)->map; + bool is_memory(const std::string &path) const { + return at(path).at(0).type == debug_item::MEMORY; + } + + const metadata_map &attrs(const std::string &path) const { + return attrs_table.at(path)->map; + } +}; + +// Only `module` scopes are defined. The type is implicit, since Yosys does not currently support +// any other scope types. +struct debug_scope { + std::string module_name; + std::unique_ptr module_attrs; + std::unique_ptr cell_attrs; +}; + +struct debug_scopes { + std::map table; + + void add(const std::string &path, const std::string &module_name, metadata_map &&module_attrs, metadata_map &&cell_attrs) { + assert((path.empty() || path[path.size() - 1] != ' ') && path.find(" ") == std::string::npos); + assert(table.count(path) == 0); + debug_scope &scope = table[path]; + scope.module_name = module_name; + scope.module_attrs = std::unique_ptr(new debug_attrs { module_attrs }); + scope.cell_attrs = std::unique_ptr(new debug_attrs { cell_attrs }); + } + + size_t contains(const std::string &path) const { + return table.count(path); + } + + const debug_scope &operator [](const std::string &path) const { + return table.at(path); } }; @@ -1412,8 +1446,16 @@ struct module { return deltas; } - virtual void debug_info(debug_items &items, std::string path = "") { - (void)items, (void)path; + virtual void debug_info(debug_items *items, debug_scopes *scopes, std::string path, metadata_map &&cell_attrs = {}) { + (void)items, (void)scopes, (void)path, (void)cell_attrs; + } + + // Compatibility method. +#if __has_attribute(deprecated) + __attribute__((deprecated("Use `debug_info(path, &items, /*scopes=*/nullptr);` instead. (`path` could be \"top \".)"))) +#endif + void debug_info(debug_items &items, std::string path) { + debug_info(&items, /*scopes=*/nullptr, path); } }; diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index b1cd9d9a1..b8233b007 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -49,11 +49,16 @@ // ::= + // ::= 0x52585843 0x00004c54 // ::= * -// ::= * +// ::= ( | )* // ::= 0xc0000000 ... // ::= 0xc0000001 ... // ::= 0x0??????? + | 0x1??????? + | 0x2??????? | 0x3??????? // , ::= 0x???????? +// ::= | | | +// ::= 0xc0000010 +// ::= 0xc0000011 +// ::= 0xc0000012 +// ::= 0xc0000013 // ::= 0xFFFFFFFF // // The replay log contains sample data, however, it does not cover the entire design. Rather, it only contains sample @@ -61,6 +66,10 @@ // a minimum, and recording speed to a maximum. The player samples any missing data by setting the design state items // to the same values they had during recording, and re-evaluating the design. // +// Packets for diagnostics (prints, breakpoints, assertions, and assumptions) are used solely for diagnostics emitted +// by the C++ testbench driving the simulation, and are not recorded while evaluating the design. (Diagnostics emitted +// by the RTL can be reconstructed at replay time, so recording them would be a waste of space.) +// // Limits // ------ // @@ -109,6 +118,33 @@ namespace cxxrtl { +// A single diagnostic that can be manipulated as an object (including being written to and read from a file). +// This differs from the base CXXRTL interface, where diagnostics can only be emitted via a procedure call, and are +// not materialized as objects. +struct diagnostic { + // The `BREAK` flavor corresponds to a breakpoint, which is a diagnostic type that can currently only be emitted + // by the C++ testbench code. + enum flavor { + BREAK = 0, + PRINT = 1, + ASSERT = 2, + ASSUME = 3, + }; + + flavor type; + std::string message; + std::string location; // same format as the `src` attribute of `$print` or `$check` cell + + diagnostic() + : type(BREAK) {} + + diagnostic(flavor type, const std::string &message, const std::string &location) + : type(type), message(message), location(location) {} + + diagnostic(flavor type, const std::string &message, const char *file, unsigned line) + : type(type), message(message), location(std::string(file) + ':' + std::to_string(line)) {} +}; + // A spool stores CXXRTL design state changes in a file. class spool { public: @@ -127,7 +163,7 @@ public: static constexpr uint32_t PACKET_SAMPLE = 0xc0000001; enum sample_flag : uint32_t { - EMPTY = 0, + EMPTY = 0, INCREMENTAL = 1, }; @@ -139,6 +175,9 @@ public: static constexpr uint32_t PACKET_CHANGEL = 0x20000000/* | ident */; static constexpr uint32_t PACKET_CHANGEH = 0x30000000/* | ident */; + static constexpr uint32_t PACKET_DIAGNOSTIC = 0xc0000010/* | diagnostic::flavor */; + static constexpr uint32_t DIAGNOSTIC_MASK = 0x0000000f; + static constexpr uint32_t PACKET_END = 0xffffffff; // Writing spools. @@ -281,6 +320,12 @@ public: emit_word(data[offset]); } + void write_diagnostic(const diagnostic &diagnostic) { + emit_word(PACKET_DIAGNOSTIC | diagnostic.type); + emit_string(diagnostic.message); + emit_string(diagnostic.location); + } + void write_end() { emit_word(PACKET_END); } @@ -397,11 +442,16 @@ public: return true; } - bool read_change_header(uint32_t &header, ident_t &ident) { + bool read_header(uint32_t &header) { header = absorb_word(); - if (header == PACKET_END) - return false; - assert((header & ~(CHANGE_MASK | MAXIMUM_IDENT)) == 0); + return header != PACKET_END; + } + + // This method must be separate from `read_change_data` because `chunks` and `depth` can only be looked up + // if `ident` is known. + bool read_change_ident(uint32_t header, ident_t &ident) { + if ((header & ~(CHANGE_MASK | MAXIMUM_IDENT)) != 0) + return false; // some other packet ident = header & MAXIMUM_IDENT; return true; } @@ -427,6 +477,18 @@ public: for (size_t offset = 0; offset < chunks; offset++) data[chunks * index + offset] = absorb_word(); } + + bool read_diagnostic(uint32_t header, diagnostic &diagnostic) { + if ((header & ~DIAGNOSTIC_MASK) != PACKET_DIAGNOSTIC) + return false; // some other packet + uint32_t type = header & DIAGNOSTIC_MASK; + assert(type == diagnostic::BREAK || type == diagnostic::PRINT || + type == diagnostic::ASSERT || type == diagnostic::ASSUME); + diagnostic.type = (diagnostic::flavor)type; + diagnostic.message = absorb_string(); + diagnostic.location = absorb_string(); + return true; + } }; // Opening spools. For certain uses of the record/replay mechanism, two distinct open files (two open files, i.e. @@ -491,9 +553,9 @@ public: template recorder(Args &&...args) : writer(std::forward(args)...) {} - void start(module &module) { + void start(module &module, std::string top_path = "") { debug_items items; - module.debug_info(items); + module.debug_info(&items, /*scopes=*/nullptr, top_path); start(items); } @@ -556,7 +618,7 @@ public: bool record_incremental(ModuleT &module) { assert(streaming); - struct { + struct : observer { std::unordered_map *ident_lookup; spool::writer *writer; @@ -569,7 +631,9 @@ public: void on_update(size_t chunks, const chunk_t *base, const chunk_t *value, size_t index) { writer->write_change(ident_lookup->at(base), chunks, value, index); } - } record_observer = { &ident_lookup, &writer }; + } record_observer; + record_observer.ident_lookup = &ident_lookup; + record_observer.writer = &writer; writer.write_sample(/*incremental=*/true, pointer++, timestamp); for (auto input_index : inputs) { @@ -582,6 +646,18 @@ public: return changed; } + void record_diagnostic(const diagnostic &diagnostic) { + assert(streaming); + + // Emit an incremental delta cycle per diagnostic to simplify the logic of the recorder. This is inefficient, but + // diagnostics should be rare enough that this inefficiency does not matter. If it turns out to be an issue, this + // code should be changed to accumulate diagnostics to a buffer that is flushed in `record_{complete,incremental}` + // and also in `advance_time` before the timestamp is changed. (Right now `advance_time` never writes to the spool.) + writer.write_sample(/*incremental=*/true, pointer++, timestamp); + writer.write_diagnostic(diagnostic); + writer.write_end(); + } + void flush() { writer.flush(); } @@ -619,9 +695,10 @@ public: template player(Args &&...args) : reader(std::forward(args)...) {} - void start(module &module) { + // The `top_path` must match the one given to the recorder. + void start(module &module, std::string top_path = "") { debug_items items; - module.debug_info(items); + module.debug_info(&items, /*scopes=*/nullptr, top_path); start(items); } @@ -654,8 +731,9 @@ public: streaming = true; // Establish the initial state of the design. - initialized = replay(); - assert(initialized); + std::vector diagnostics; + initialized = replay(&diagnostics); + assert(initialized && diagnostics.empty()); } // Returns the pointer of the current sample. @@ -687,8 +765,8 @@ public: // If this function returns `true`, then `current_pointer() == at_pointer`, and the module contains values that // correspond to this pointer in the replay log. To obtain a valid pointer, call `current_pointer()`; while pointers // are monotonically increasing for each consecutive sample, using arithmetic operations to create a new pointer is - // not allowed. - bool rewind_to(spool::pointer_t at_pointer) { + // not allowed. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in this sample. + bool rewind_to(spool::pointer_t at_pointer, std::vector *diagnostics) { assert(initialized); // The pointers in the replay log start from one that is greater than `at_pointer`. In this case the pointer will @@ -704,9 +782,12 @@ public: reader.rewind(position_it->second); // Replay samples until eventually arriving to `at_pointer` or encountering end of file. - while(replay()) { + while(replay(diagnostics)) { if (pointer == at_pointer) return true; + + if (diagnostics) + diagnostics->clear(); } return false; } @@ -714,8 +795,8 @@ public: // If this function returns `true`, then `current_time() <= at_or_before_timestamp`, and the module contains values // that correspond to `current_time()` in the replay log. If `current_time() == at_or_before_timestamp` and there // are several consecutive samples with the same time, the module contains values that correspond to the first of - // these samples. - bool rewind_to_or_before(const time &at_or_before_timestamp) { + // these samples. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in this sample. + bool rewind_to_or_before(const time &at_or_before_timestamp, std::vector *diagnostics) { assert(initialized); // The timestamps in the replay log start from one that is greater than `at_or_before_timestamp`. In this case @@ -731,7 +812,7 @@ public: reader.rewind(position_it->second); // Replay samples until eventually arriving to or past `at_or_before_timestamp` or encountering end of file. - while (replay()) { + while (replay(diagnostics)) { if (timestamp == at_or_before_timestamp) break; @@ -740,14 +821,17 @@ public: break; if (next_timestamp > at_or_before_timestamp) break; + + if (diagnostics) + diagnostics->clear(); } return true; } // If this function returns `true`, then `current_pointer()` and `current_time()` are updated for the next sample // and the module now contains values that correspond to that sample. If it returns `false`, there was no next sample - // to read. - bool replay() { + // to read. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in the next sample. + bool replay(std::vector *diagnostics) { assert(streaming); bool incremental; @@ -768,11 +852,16 @@ public: } uint32_t header; - spool::ident_t ident; - variable var; - while (reader.read_change_header(header, ident)) { - variable &var = variables.at(ident); - reader.read_change_data(header, var.chunks, var.depth, var.curr); + while (reader.read_header(header)) { + spool::ident_t ident; + diagnostic diag; + if (reader.read_change_ident(header, ident)) { + variable &var = variables.at(ident); + reader.read_change_data(header, var.chunks, var.depth, var.curr); + } else if (reader.read_diagnostic(header, diag)) { + if (diagnostics) + diagnostics->push_back(diag); + } else assert(false && "Unrecognized packet header"); } return true; } diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 5e63e6237..c702d5e7e 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1117,7 +1117,18 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - if (cell->name[0] == '$' && cell->attributes.count(ID::src)) + bool private_name = cell->name[0] == '$'; + + if (!private_name && cell->has_attribute(ID::hdlname)) { + for (auto const &part : cell->get_hdlname_attribute()) { + if (part == "_witness_") { + private_name = true; + break; + } + } + } + + if (private_name && cell->attributes.count(ID::src)) decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); else decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 34657be26..e6b4088db 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -57,6 +57,8 @@ keep_going = False check_witness = False detect_loops = False incremental = None +track_assumes = False +minimize_assumes = False so = SmtOpts() @@ -189,6 +191,15 @@ def help(): --incremental run in incremental mode (experimental) + --track-assumes + track individual assumptions and report a subset of used + assumptions that are sufficient for the reported outcome. This + can be used to debug PREUNSAT failures as well as to find a + smaller set of sufficient assumptions. + + --minimize-assumes + when using --track-assumes, solve for a minimal set of sufficient assumptions. + """ + so.helpmsg()) def usage(): @@ -200,7 +211,8 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:higcm:", so.longopts + ["help", "final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops", "incremental"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops", "incremental", + "track-assumes", "minimize-assumes"]) except: usage() @@ -289,6 +301,10 @@ for o, a in opts: elif o == "--incremental": from smtbmc_incremental import Incremental incremental = Incremental() + elif o == "--track-assumes": + track_assumes = True + elif o == "--minimize-assumes": + minimize_assumes = True elif so.handle(o, a): pass else: @@ -447,6 +463,9 @@ def get_constr_expr(db, state, final=False, getvalues=False, individual=False): smt = SmtIo(opts=so) +if track_assumes: + smt.smt2_options[':produce-unsat-assumptions'] = 'true' + if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None: smt.produce_models = False @@ -649,14 +668,20 @@ if aimfile is not None: num_steps = max(num_steps, step+2) step += 1 +ywfile_hierwitness_cache = None + def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache if map_steps is None: map_steps = {} with open(inywfile, "r") as f: inyw = ReadWitness(f) - inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) + + inits, seqs, clocks, mems = ywfile_hierwitness_cache smt_wires = defaultdict(list) smt_mems = defaultdict(list) @@ -1491,6 +1516,44 @@ def get_active_assert_map(step, active): return assert_map +assume_enables = {} + +def declare_assume_enables(): + def recurse(mod, path, key_base=()): + for expr, desc in smt.modinfo[mod].assumes.items(): + enable = f"|assume_enable {len(assume_enables)}|" + smt.smt2_assumptions[(expr, key_base)] = enable + smt.write(f"(declare-const {enable} Bool)") + assume_enables[(expr, key_base)] = (enable, path, desc) + + for cell, submod in smt.modinfo[mod].cells.items(): + recurse(submod, f"{path}.{cell}", (mod, cell, key_base)) + + recurse(topmod, topmod) + +if track_assumes: + declare_assume_enables() + +def smt_assert_design_assumes(step): + if not track_assumes: + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + return + + if not assume_enables: + return + + def expr_for_assume(assume_key, base=None): + expr, key_base = assume_key + expr_prefix = f"(|{expr}| " + expr_suffix = ")" + while key_base: + mod, cell, key_base = key_base + expr_prefix += f"(|{mod}_h {cell}| " + expr_suffix += ")" + return f"{expr_prefix} s{step}{expr_suffix}" + + for assume_key, (enable, path, desc) in assume_enables.items(): + smt_assert_consequent(f"(=> {enable} {expr_for_assume(assume_key)})") states = list() asserts_antecedent_cache = [list()] @@ -1645,6 +1708,13 @@ def smt_check_sat(expected=["sat", "unsat"]): smt_forall_assert() return smt.check_sat(expected=expected) +def report_tracked_assumptions(msg): + if track_assumes: + print_msg(msg) + for key in smt.get_unsat_assumptions(minimize=minimize_assumes): + enable, path, descr = assume_enables[key] + print_msg(f" In {path}: {descr}") + if incremental: incremental.mainloop() @@ -1658,7 +1728,7 @@ elif tempind: break smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1701,6 +1771,7 @@ elif tempind: else: print_msg("Temporal induction successful.") + report_tracked_assumptions("Used assumptions:") retstatus = "PASSED" break @@ -1726,7 +1797,7 @@ elif covermode: while step < num_steps: smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1747,6 +1818,7 @@ elif covermode: smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc))) if smt_check_sat() == "unsat": + report_tracked_assumptions("Used assumptions:") smt_pop() break @@ -1755,13 +1827,14 @@ elif covermode: print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + smt_assert_design_assumes(i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + report_tracked_assumptions("Conflicting assumptions:") found_failed_assert = True retstatus = "FAILED" break @@ -1817,7 +1890,7 @@ else: # not tempind, covermode retstatus = "PASSED" while step < num_steps: smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1847,7 +1920,7 @@ else: # not tempind, covermode if step+i < num_steps: smt_state(step+i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i)) + smt_assert_design_assumes(step + i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i)) smt_assert_consequent(get_constr_expr(constr_assumes, step+i)) @@ -1861,7 +1934,8 @@ else: # not tempind, covermode print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) if smt_check_sat() == "unsat": - print("%s Assumptions are unsatisfiable!" % smt.timestamp()) + print_msg("Assumptions are unsatisfiable!") + report_tracked_assumptions("Conficting assumptions:") retstatus = "PREUNSAT" break @@ -1914,13 +1988,14 @@ else: # not tempind, covermode print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + smt_assert_design_assumes(i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": - print("%s Cannot append steps without violating assumptions!" % smt.timestamp()) + print_msg("Cannot append steps without violating assumptions!") + report_tracked_assumptions("Conflicting assumptions:") retstatus = "FAILED" break print_anyconsts(step) diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index 1a2a45703..f43e878f3 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -15,6 +15,14 @@ class InteractiveError(Exception): pass +def mkkey(data): + if isinstance(data, list): + return tuple(map(mkkey, data)) + elif isinstance(data, dict): + raise InteractiveError(f"JSON objects found in assumption key: {data!r}") + return data + + class Incremental: def __init__(self): self.traceidx = 0 @@ -73,17 +81,17 @@ class Incremental: if min_len is not None and arg_len < min_len: if min_len == max_len: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression must have " f"{min_len} argument{'s' if min_len != 1 else ''}" ) else: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression must have at least " f"{min_len} argument{'s' if min_len != 1 else ''}" ) if max_len is not None and arg_len > max_len: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression can have at most " f"{min_len} argument{'s' if max_len != 1 else ''}" ) @@ -96,14 +104,31 @@ class Incremental: smt_out.append(f"s{step}") return "module", smtbmc.topmod - def expr_mod_constraint(self, expr, smt_out): - self.expr_arg_len(expr, 1) + def expr_cell(self, expr, smt_out): + self.expr_arg_len(expr, 2) position = len(smt_out) smt_out.append(None) - arg_sort = self.expr(expr[1], smt_out, required_sort=["module", None]) + arg_sort = self.expr(expr[2], smt_out, required_sort=["module", None]) + smt_out.append(")") module = arg_sort[1] + cell = expr[1] + submod = smtbmc.smt.modinfo[module].cells.get(cell) + if submod is None: + raise InteractiveError(f"module {module!r} has no cell {cell!r}") + smt_out[position] = f"(|{module}_h {cell}| " + return ("module", submod) + + def expr_mod_constraint(self, expr, smt_out): suffix = expr[0][3:] - smt_out[position] = f"(|{module}{suffix}| " + self.expr_arg_len(expr, 1, 2 if suffix in ["_a", "_u", "_c"] else 1) + position = len(smt_out) + smt_out.append(None) + arg_sort = self.expr(expr[-1], smt_out, required_sort=["module", None]) + module = arg_sort[1] + if len(expr) == 3: + smt_out[position] = f"(|{module}{suffix} {expr[1]}| " + else: + smt_out[position] = f"(|{module}{suffix}| " smt_out.append(")") return "Bool" @@ -223,20 +248,19 @@ class Incremental: subexpr = expr[2] if not isinstance(label, str): - raise InteractiveError(f"expression label has to be a string") + raise InteractiveError("expression label has to be a string") smt_out.append("(! ") - smt_out.appedd(label) - smt_out.append(" ") - sort = self.expr(subexpr, smt_out) - + smt_out.append(" :named ") + smt_out.append(label) smt_out.append(")") return sort expr_handlers = { "step": expr_step, + "cell": expr_cell, "mod_h": expr_mod_constraint, "mod_is": expr_mod_constraint, "mod_i": expr_mod_constraint, @@ -302,6 +326,30 @@ class Incremental: assert_fn(self.expr_smt(cmd.get("expr"), "Bool")) + def cmd_assert_design_assumes(self, cmd): + step = self.arg_step(cmd) + smtbmc.smt_assert_design_assumes(step) + + def cmd_get_design_assume(self, cmd): + key = mkkey(cmd.get("key")) + return smtbmc.assume_enables.get(key) + + def cmd_update_assumptions(self, cmd): + expr = cmd.get("expr") + key = cmd.get("key") + + + key = mkkey(key) + + result = smtbmc.smt.smt2_assumptions.pop(key, None) + if expr is not None: + expr = self.expr_smt(expr, "Bool") + smtbmc.smt.smt2_assumptions[key] = expr + return result + + def cmd_get_unsat_assumptions(self, cmd): + return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get('minimize'))) + def cmd_push(self, cmd): smtbmc.smt_push() @@ -313,11 +361,14 @@ class Incremental: def cmd_smtlib(self, cmd): command = cmd.get("command") + response = cmd.get("response", False) if not isinstance(command, str): raise InteractiveError( f"raw SMT-LIB command must be a string, found {json.dumps(command)}" ) smtbmc.smt.write(command) + if response: + return smtbmc.smt.read() def cmd_design_hierwitness(self, cmd=None): allregs = (cmd is None) or bool(cmd.get("allreges", False)) @@ -369,6 +420,21 @@ class Incremental: return dict(last_step=last_step) + def cmd_modinfo(self, cmd): + fields = cmd.get("fields", []) + + mod = cmd.get("mod") + if mod is None: + mod = smtbmc.topmod + modinfo = smtbmc.smt.modinfo.get(mod) + if modinfo is None: + return None + + result = dict(name=mod) + for field in fields: + result[field] = getattr(modinfo, field, None) + return result + def cmd_ping(self, cmd): return cmd @@ -377,6 +443,10 @@ class Incremental: "assert": cmd_assert, "assert_antecedent": cmd_assert, "assert_consequent": cmd_assert, + "assert_design_assumes": cmd_assert_design_assumes, + "get_design_assume": cmd_get_design_assume, + "update_assumptions": cmd_update_assumptions, + "get_unsat_assumptions": cmd_get_unsat_assumptions, "push": cmd_push, "pop": cmd_pop, "check": cmd_check, @@ -384,6 +454,7 @@ class Incremental: "design_hierwitness": cmd_design_hierwitness, "write_yw_trace": cmd_write_yw_trace, "read_yw_trace": cmd_read_yw_trace, + "modinfo": cmd_modinfo, "ping": cmd_ping, } diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 0ec7f08f4..e32f43c60 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -79,6 +79,20 @@ def except_hook(exctype, value, traceback): sys.excepthook = except_hook +def recursion_helper(iteration, *request): + stack = [iteration(*request)] + + while stack: + top = stack.pop() + try: + request = next(top) + except StopIteration: + continue + + stack.append(top) + stack.append(iteration(*request)) + + hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -100,6 +114,7 @@ class SmtModInfo: self.clocks = dict() self.cells = dict() self.asserts = dict() + self.assumes = dict() self.covers = dict() self.maximize = set() self.minimize = set() @@ -127,6 +142,7 @@ class SmtIo: self.recheck = False self.smt2cache = [list()] self.smt2_options = dict() + self.smt2_assumptions = dict() self.p = None self.p_index = solvers_index solvers_index += 1 @@ -298,10 +314,22 @@ class SmtIo: return stmt def unroll_stmt(self, stmt): - if not isinstance(stmt, list): - return stmt + result = [] + recursion_helper(self._unroll_stmt_into, stmt, result) + return result.pop() - stmt = [self.unroll_stmt(s) for s in stmt] + def _unroll_stmt_into(self, stmt, output, depth=128): + if not isinstance(stmt, list): + output.append(stmt) + return + + new_stmt = [] + for s in stmt: + if depth: + yield from self._unroll_stmt_into(s, new_stmt, depth - 1) + else: + yield s, new_stmt + stmt = new_stmt if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls: assert stmt[1] in self.unroll_objs @@ -330,12 +358,19 @@ class SmtIo: decl[2] = list() if len(decl) > 0: - decl = self.unroll_stmt(decl) + tmp = [] + if depth: + yield from self._unroll_stmt_into(decl, tmp, depth - 1) + else: + yield decl, tmp + + decl = tmp.pop() self.write(self.unparse(decl), unroll=False) - return self.unroll_cache[key] + output.append(self.unroll_cache[key]) + return - return stmt + output.append(stmt) def p_thread_main(self): while True: @@ -569,6 +604,12 @@ class SmtIo: else: self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-assume": + if len(fields) > 4: + self.modinfo[self.curmod].assumes["%s_u %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].assumes["%s_u %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-maximize": self.modinfo[self.curmod].maximize.add(fields[2]) @@ -752,8 +793,13 @@ class SmtIo: return stmt def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]): + if self.smt2_assumptions: + assume_exprs = " ".join(self.smt2_assumptions.values()) + check_stmt = f"(check-sat-assuming ({assume_exprs}))" + else: + check_stmt = "(check-sat)" if self.debug_print: - print("> (check-sat)") + print(f"> {check_stmt}") if self.debug_file and not self.nocomments: print("; running check-sat..", file=self.debug_file) self.debug_file.flush() @@ -767,7 +813,7 @@ class SmtIo: for cache_stmt in cache_ctx: self.p_write(cache_stmt + "\n", False) - self.p_write("(check-sat)\n", True) + self.p_write(f"{check_stmt}\n", True) if self.timeinfo: i = 0 @@ -835,7 +881,7 @@ class SmtIo: if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) - print("(check-sat)", file=self.debug_file) + print(check_stmt, file=self.debug_file) self.debug_file.flush() if result not in expected: @@ -912,6 +958,48 @@ class SmtIo: def bv2int(self, v): return int(self.bv2bin(v), 2) + def get_raw_unsat_assumptions(self): + self.write("(get-unsat-assumptions)") + exprs = set(self.unparse(part) for part in self.parse(self.read())) + unsat_assumptions = [] + for key, value in self.smt2_assumptions.items(): + # normalize expression + value = self.unparse(self.parse(value)) + if value in exprs: + exprs.remove(value) + unsat_assumptions.append(key) + return unsat_assumptions + + def get_unsat_assumptions(self, minimize=False): + if not minimize: + return self.get_raw_unsat_assumptions() + required_assumptions = {} + + while True: + candidate_assumptions = {} + for key in self.get_raw_unsat_assumptions(): + if key not in required_assumptions: + candidate_assumptions[key] = self.smt2_assumptions[key] + + while candidate_assumptions: + + candidate_key, candidate_assume = candidate_assumptions.popitem() + + self.smt2_assumptions = {} + for key, assume in candidate_assumptions.items(): + self.smt2_assumptions[key] = assume + for key, assume in required_assumptions.items(): + self.smt2_assumptions[key] = assume + result = self.check_sat() + + if result == 'unsat': + candidate_assumptions = None + else: + required_assumptions[candidate_key] = candidate_assume + + if candidate_assumptions is not None: + return list(required_assumptions) + def get(self, expr): self.write("(get-value (%s))" % (expr)) return self.parse(self.read())[0][1] @@ -920,7 +1008,7 @@ class SmtIo: if len(expr_list) == 0: return [] self.write("(get-value (%s))" % " ".join(expr_list)) - return [n[1] for n in self.parse(self.read())] + return [n[1] for n in self.parse(self.read()) if n] def get_path(self, mod, path): assert mod in self.modinfo diff --git a/docs/source/CHAPTER_CellLib.rst b/docs/source/CHAPTER_CellLib.rst index 3b6f1b4d3..70a0e2150 100644 --- a/docs/source/CHAPTER_CellLib.rst +++ b/docs/source/CHAPTER_CellLib.rst @@ -195,7 +195,7 @@ from ``\S`` is set the output is undefined. Cells of this type are used to model by an optimization). The ``$tribuf`` cell is used to implement tristate logic. Cells of this type -have a ``\B`` parameter and inputs ``\A`` and ``\EN`` and an output ``\Y``. The +have a ``\WIDTH`` parameter and inputs ``\A`` and ``\EN`` and an output ``\Y``. The ``\A`` input and ``\Y`` output are ``\WIDTH`` bits wide, and the ``\EN`` input is one bit wide. When ``\EN`` is 0, the output is not driven. When ``\EN`` is 1, the value from ``\A`` input is sent to the ``\Y`` output. Therefore, the diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index ead79fd95..996f6715d 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -1820,7 +1820,7 @@ std::string AstModule::derive_common(RTLIL::Design *design, const dictclone(); if (!new_ast->attributes.count(ID::hdlname)) - new_ast->set_attribute(ID::hdlname, AstNode::mkconst_str(stripped_name)); + new_ast->set_attribute(ID::hdlname, AstNode::mkconst_str(stripped_name.substr(1))); para_counter = 0; for (auto child : new_ast->children) { diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 96296aeb8..43a4e03a2 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -5662,7 +5662,7 @@ std::string AstNode::try_pop_module_prefix() const if (current_scope.count(new_str)) { std::string prefix = str.substr(0, pos); auto it = current_scope_ast->attributes.find(ID::hdlname); - if ((it != current_scope_ast->attributes.end() && it->second->str == prefix) + if ((it != current_scope_ast->attributes.end() && it->second->str == prefix.substr(1)) || prefix == current_scope_ast->str) return new_str; } diff --git a/kernel/celledges.cc b/kernel/celledges.cc index c43ba8db3..2ed0d5036 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -172,6 +172,141 @@ void demux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) } } +void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); + bool is_b_signed = cell->getParam(ID::B_SIGNED).as_bool(); + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + int y_width = GetSize(cell->getPort(ID::Y)); + + // Behavior of the different shift cells: + // + // $shl, $sshl -- shifts left by the amount on B port, B always unsigned + // $shr, $sshr -- ditto right + // $shift, $shiftx -- shifts right by the amount on B port, B optionally signed + // + // Sign extension (if A signed): + // + // $shl, $shr, $shift -- only sign-extends up to size of Y, then shifts in zeroes + // $sshl, $sshr -- fully sign-extends + // $shiftx -- no sign extension + // + // Because $shl, $sshl only shift left, and $shl sign-extens up to size of Y, they + // are effectively the same. + + // the cap below makes sure we don't overflow in the arithmetic further down, though + // it makes the edge data invalid once a_width approaches the order of 2**30 + // (that ever happening is considered improbable) + int b_width_capped = min(b_width, 30); + + int b_high, b_low; + if (!is_b_signed) { + b_high = (1 << b_width_capped) - 1; + b_low = 0; + } else { + b_high = (1 << (b_width_capped - 1)) - 1; + b_low = -(1 << (b_width_capped - 1)); + } + + for (int i = 0; i < y_width; i++){ + // highest position of Y that can change with the value of B + int b_range_upper = 0; + // 1 + highest position of A that can be moved to Y[i] + int a_range_upper; + // lowest position of A that can be moved to Y[i] + int a_range_lower; + + if (cell->type.in(ID($shl), ID($sshl))) { + b_range_upper = a_width + b_high; + if (is_signed) b_range_upper -= 1; + a_range_lower = max(0, i - b_high); + a_range_upper = min(i+1, a_width); + } else if (cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)) { + b_range_upper = a_width; + a_range_lower = min(i, a_width - 1); + a_range_upper = min(i+1 + b_high, a_width); + } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed) { + // can go both ways depending on sign of B + // 2's complement range is different depending on direction + b_range_upper = a_width - b_low; + a_range_lower = max(0, i + b_low); + if (is_signed) + a_range_lower = min(a_range_lower, a_width - 1); + a_range_upper = min(i+1 + b_high, a_width); + } else { + log_assert(false && "unreachable"); + } + + if (i < b_range_upper) { + for (int k = a_range_lower; k < a_range_upper; k++) + db->add_edge(cell, ID::A, k, ID::Y, i, -1); + } else { + // only influence is through sign extension + if (is_signed) + db->add_edge(cell, ID::A, a_width - 1, ID::Y, i, -1); + } + + for (int k = 0; k < b_width; k++) { + // left shifts + if (cell->type.in(ID($shl), ID($sshl))) { + 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) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else if (is_signed) { + if (i - a_width + 2 < 1 << b_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + if (i - a_width + 1 < 1 << b_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + // right shifts + } else if (cell->type.in(ID($shr), ID($sshr)) || (cell->type.in(ID($shift), ID($shiftx)) && !is_b_signed)) { + if (is_signed) { + bool shift_in_bulk = i < a_width - 1; + // can we jump into the zero-padding by toggling B[k]? + bool zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) < (1 << b_width))); + + if (shift_in_bulk || (cell->type.in(ID($shr), ID($shift), ID($shiftx)) && zpad_jump)) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + if (i < a_width) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + // bidirectional shifts (positive B shifts right, negative left) + } else if (cell->type.in(ID($shift), ID($shiftx)) && is_b_signed) { + if (is_signed) { + if (k != b_width - 1) { + bool r_shift_in_bulk = i < a_width - 1; + // assuming B is positive, can we jump into the upper zero-padding by toggling B[k]? + bool r_zpad_jump = (((y_width - i) & ((1 << (k + 1)) - 1)) != 0 \ + && (((y_width - i) & ~(1 << k)) <= b_high)); + // assuming B is negative, can we influence Y[i] by toggling B[k]? + bool l = a_width - 2 - i >= b_low; + if (a_width == 1) { + // in case of a_width==1 we go into more detailed reasoning + l = l && (~(i - a_width) & ((1 << (k + 1)) - 1)) != 0; + } + if (r_shift_in_bulk || r_zpad_jump || l) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } else { + if (y_width - i <= b_high || a_width - 2 - i >= b_low) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + } else { + if (a_width - 1 - i >= b_low) + db->add_edge(cell, ID::B, k, ID::Y, i, -1); + } + } else { + log_assert(false && "unreachable"); + } + } + } +} + PRIVATE_NAMESPACE_END bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL::Cell *cell) @@ -201,11 +336,10 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } - // FIXME: - // if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) { - // shift_op(this, cell); - // return true; - // } + if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) { + shift_op(this, cell); + return true; + } if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt))) { compare_op(this, cell); @@ -227,8 +361,17 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } - // FIXME: $mul $div $mod $divfloor $modfloor $slice $concat - // FIXME: $lut $sop $alu $lcu $macc $fa + // FIXME: $mul $div $mod $divfloor $modfloor $pow $slice $concat $bweqx + // FIXME: $lut $sop $alu $lcu $macc $fa $logic_and $logic_or $bwmux + + // FIXME: $_BUF_ $_NOT_ $_AND_ $_NAND_ $_OR_ $_NOR_ $_XOR_ $_XNOR_ $_ANDNOT_ $_ORNOT_ + // FIXME: $_MUX_ $_NMUX_ $_MUX4_ $_MUX8_ $_MUX16_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_ + + // FIXME: $specify2 $specify3 $specrule ??? + // FIXME: $equiv $set_tag $get_tag $overwrite_tag $original_tag + + if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover), ID($initstate), ID($anyconst), ID($anyseq), ID($allconst), ID($allseq))) + return true; // no-op: these have either no inputs or no outputs return false; } diff --git a/kernel/register.cc b/kernel/register.cc index 1853e94d5..3ccb5ee78 100644 --- a/kernel/register.cc +++ b/kernel/register.cc @@ -992,4 +992,44 @@ struct MinisatSatSolver : public SatSolver { } } MinisatSatSolver; +struct LicensePass : public Pass { + LicensePass() : Pass("license", "print license terms") { } + void help() override + { + log("\n"); + log(" license\n"); + log("\n"); + log("This command produces the following notice.\n"); + notice(); + } + void execute(std::vector, RTLIL::Design*) override + { + notice(); + } + void notice() + { + log("\n"); + log(" /----------------------------------------------------------------------------\\\n"); + log(" | |\n"); + log(" | yosys -- Yosys Open SYnthesis Suite |\n"); + log(" | |\n"); + log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\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"); + log(" | copyright notice and this permission notice appear in all copies. |\n"); + log(" | |\n"); + log(" | THE SOFTWARE IS PROVIDED \"AS IS\" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |\n"); + log(" | WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |\n"); + log(" | MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |\n"); + log(" | ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |\n"); + log(" | WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |\n"); + log(" | ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |\n"); + log(" | OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |\n"); + log(" | |\n"); + log(" \\----------------------------------------------------------------------------/\n"); + log("\n"); + } +} LicensePass; + YOSYS_NAMESPACE_END diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 928bc0440..40422dce5 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -712,7 +712,7 @@ struct RTLIL::Const inline unsigned int hash() const { unsigned int h = mkhash_init; for (auto b : bits) - mkhash(h, b); + h = mkhash(h, b); return h; } }; diff --git a/kernel/yosys.cc b/kernel/yosys.cc index c7f5bebda..57433d0d9 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -55,7 +55,7 @@ # include #endif -#ifdef __FreeBSD__ +#if defined(__FreeBSD__) || defined(__NetBSD__) # include #endif @@ -138,27 +138,11 @@ void yosys_banner() { log("\n"); log(" /----------------------------------------------------------------------------\\\n"); - log(" | |\n"); log(" | yosys -- Yosys Open SYnthesis Suite |\n"); - log(" | |\n"); - log(" | Copyright (C) 2012 - 2020 Claire Xenia Wolf |\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"); - log(" | copyright notice and this permission notice appear in all copies. |\n"); - log(" | |\n"); - log(" | THE SOFTWARE IS PROVIDED \"AS IS\" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |\n"); - log(" | WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |\n"); - log(" | MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |\n"); - log(" | ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |\n"); - log(" | WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |\n"); - log(" | ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |\n"); - log(" | OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |\n"); - log(" | |\n"); + log(" | Copyright (C) 2012 - 2024 Claire Xenia Wolf |\n"); + log(" | Distributed under an ISC-like license, type \"license\" to see terms |\n"); log(" \\----------------------------------------------------------------------------/\n"); - log("\n"); log(" %s\n", yosys_version_str); - log("\n"); } int ceil_log2(int x) @@ -917,10 +901,14 @@ std::string proc_self_dirname() buflen--; return std::string(path, buflen); } -#elif defined(__FreeBSD__) +#elif defined(__FreeBSD__) || defined(__NetBSD__) std::string proc_self_dirname() { +#ifdef __NetBSD__ + int mib[4] = {CTL_KERN, KERN_PROC_ARGS, getpid(), KERN_PROC_PATHNAME}; +#else int mib[4] = {CTL_KERN, KERN_PROC, KERN_PROC_PATHNAME, -1}; +#endif size_t buflen; char *buffer; std::string path; diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile index b1f864160..c41038dc9 100644 --- a/libs/ezsat/Makefile +++ b/libs/ezsat/Makefile @@ -1,9 +1,9 @@ CC = clang -CXX = clang +CXX = clang++ CXXFLAGS = -MD -Wall -Wextra -ggdb CXXFLAGS += -std=c++11 -O0 -LDLIBS = ../minisat/Options.cc ../minisat/SimpSolver.cc ../minisat/Solver.cc ../minisat/System.cc -lm -lstdc++ +LIBS = ../minisat/Options.cc ../minisat/SimpSolver.cc ../minisat/Solver.cc ../minisat/System.cc -lm -lstdc++ all: demo_vec demo_bit demo_cmp testbench puzzle3d @@ -27,4 +27,3 @@ clean: .PHONY: all test clean -include *.d - diff --git a/libs/subcircuit/Makefile b/libs/subcircuit/Makefile index f81085b5b..3d93ad0a2 100644 --- a/libs/subcircuit/Makefile +++ b/libs/subcircuit/Makefile @@ -5,9 +5,9 @@ CONFIG := clang-debug # CONFIG := release CC = clang -CXX = clang +CXX = clang++ CXXFLAGS = -MD -Wall -Wextra -ggdb -LDLIBS = -lstdc++ +LIBS = -lstdc++ ifeq ($(CONFIG),clang-debug) CXXFLAGS += -std=c++11 -O0 @@ -15,19 +15,19 @@ endif ifeq ($(CONFIG),gcc-debug) CC = gcc -CXX = gcc +CXX = g++ CXXFLAGS += -std=gnu++0x -O0 endif ifeq ($(CONFIG),profile) CC = gcc -CXX = gcc +CXX = g++ CXXFLAGS += -std=gnu++0x -Os -DNDEBUG endif ifeq ($(CONFIG),release) CC = gcc -CXX = gcc +CXX = g++ CXXFLAGS += -std=gnu++0x -march=native -O3 -DNDEBUG endif @@ -50,4 +50,3 @@ clean: .PHONY: all test clean -include *.d - diff --git a/misc/yosys-config.in b/misc/yosys-config.in old mode 100644 new mode 100755 index f0f0f7552..dd42b7c87 --- a/misc/yosys-config.in +++ b/misc/yosys-config.in @@ -9,8 +9,10 @@ help() { echo "Replacement args:" echo " --cxx @CXX@" echo " --cxxflags $( echo '@CXXFLAGS@' | fmt -w60 | sed ':a;N;$!ba;s/\n/ \\\n /g' )" - echo " --ldflags @LDFLAGS@" - echo " --ldlibs @LDLIBS@" + echo " --linkflags @LINKFLAGS@" + echo " --ldflags (alias of --linkflags)" + echo " --libs @LIBS@" + echo " --ldlibs (alias of --libs)" echo " --bindir @BINDIR@" echo " --datdir @DATDIR@" echo "" @@ -18,7 +20,7 @@ help() { echo "" echo "Use --exec to call a command instead of generating output. Example usage:" echo "" - echo " $0 --exec --cxx --cxxflags --ldflags -o plugin.so -shared plugin.cc --ldlibs" + echo " $0 --exec --cxx --cxxflags --ldflags -o plugin.so -shared plugin.cc --libs" echo "" echo "The above command can be abbreviated as:" echo "" @@ -44,7 +46,7 @@ fi if [ "$1" == "--build" ]; then modname="$2"; shift 2 - set -- --exec --cxx --cxxflags --ldflags -o "$modname" -shared "$@" --ldlibs + set -- --exec --cxx --cxxflags --ldflags -o "$modname" -shared "$@" --libs fi prefix="--" @@ -63,10 +65,14 @@ for opt; do tokens=( "${tokens[@]}" @CXX@ ) ;; "$prefix"cxxflags) tokens=( "${tokens[@]}" @CXXFLAGS@ ) ;; + "$prefix"linkflags) + tokens=( "${tokens[@]}" @LINKFLAGS@ ) ;; + "$prefix"libs) + tokens=( "${tokens[@]}" @LIBS@ ) ;; "$prefix"ldflags) - tokens=( "${tokens[@]}" @LDFLAGS@ ) ;; + tokens=( "${tokens[@]}" @LINKFLAGS@ ) ;; "$prefix"ldlibs) - tokens=( "${tokens[@]}" @LDLIBS@ ) ;; + tokens=( "${tokens[@]}" @LIBS@ ) ;; "$prefix"bindir) tokens=( "${tokens[@]}" '@BINDIR@' ) ;; "$prefix"datdir) @@ -104,4 +110,3 @@ fi echo "${tokens[@]}" exit 0 - diff --git a/passes/cmds/connect.cc b/passes/cmds/connect.cc index 1bd52aab2..65292ef92 100644 --- a/passes/cmds/connect.cc +++ b/passes/cmds/connect.cc @@ -47,7 +47,7 @@ struct ConnectPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" connect [-nomap] [-nounset] -set \n"); + log(" connect [-nomap] [-nounset] -set [selection]\n"); log("\n"); log("Create a connection. This is equivalent to adding the statement 'assign\n"); log(" = ;' to the Verilog input. Per default, all existing\n"); @@ -55,12 +55,12 @@ struct ConnectPass : public Pass { log("the -nounset option.\n"); log("\n"); log("\n"); - log(" connect [-nomap] -unset \n"); + log(" connect [-nomap] -unset [selection]\n"); log("\n"); log("Unconnect all existing drivers for the specified expression.\n"); log("\n"); log("\n"); - log(" connect [-nomap] [-assert] -port \n"); + log(" connect [-nomap] [-assert] -port [selection]\n"); log("\n"); log("Connect the specified cell port to the specified cell port.\n"); log("\n"); @@ -80,17 +80,6 @@ struct ConnectPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { - RTLIL::Module *module = nullptr; - for (auto mod : design->selected_modules()) { - if (module != nullptr) - log_cmd_error("Multiple modules selected: %s, %s\n", log_id(module->name), log_id(mod->name)); - module = mod; - } - if (module == nullptr) - log_cmd_error("No modules selected.\n"); - if (!module->processes.empty()) - log_cmd_error("Found processes in selected module.\n"); - bool flag_nounset = false, flag_nomap = false, flag_assert = false; std::string set_lhs, set_rhs, unset_expr; std::string port_cell, port_port, port_expr; @@ -128,6 +117,18 @@ struct ConnectPass : public Pass { } break; } + extra_args(args, argidx, design); + + RTLIL::Module *module = nullptr; + for (auto mod : design->selected_modules()) { + if (module != nullptr) + log_cmd_error("Multiple modules selected: %s, %s\n", log_id(module->name), log_id(mod->name)); + module = mod; + } + if (module == nullptr) + log_cmd_error("No modules selected.\n"); + if (!module->processes.empty()) + log_cmd_error("Found processes in selected module.\n"); SigMap sigmap; if (!flag_nomap) diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index da4ba2f17..3f8d807b3 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict &ca cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); renames.emplace_back(cell, new_id); } - break; } if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { @@ -165,6 +164,20 @@ static bool rename_witness(RTLIL::Design *design, dict &ca } } } + + + if (cell->type.in(ID($assert), ID($assume), ID($cover), ID($live), ID($fair), ID($check))) { + has_witness_signals = true; + if (cell->name.isPublic()) + continue; + std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1); + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + renames.emplace_back(cell, new_id); + cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + } } for (auto rename : renames) { module->rename(rename.first, rename.second); diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 8c2695dbe..82b5c6bcf 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -65,6 +65,7 @@ struct ShowWorker bool enumerateIds; bool abbreviateIds; bool notitle; + bool href; int page_counter; const std::vector> &color_selections; @@ -432,9 +433,13 @@ struct ShowWorker if (wire->port_input || wire->port_output) shape = "octagon"; if (wire->name.isPublic()) { - fprintf(f, "n%d [ shape=%s, label=\"%s\", %s ];\n", + std::string src_href; + if (href && wire->attributes.count(ID::src) > 0) + src_href = stringf(", href=\"%s\" ", escape(wire->attributes.at(ID::src).decode_string())); + fprintf(f, "n%d [ shape=%s, label=\"%s\", %s%s];\n", id2num(wire->name), shape, findLabel(wire->name.str()), - nextColor(RTLIL::SigSpec(wire), "color=\"black\", fontcolor=\"black\"").c_str()); + nextColor(RTLIL::SigSpec(wire), "color=\"black\", fontcolor=\"black\"").c_str(), + src_href.c_str()); if (wire->port_input) all_sources.insert(stringf("n%d", id2num(wire->name))); else if (wire->port_output) @@ -496,14 +501,18 @@ struct ShowWorker conn.second, ct.cell_output(cell->type, conn.first)); } + std::string src_href; + if (href && cell->attributes.count(ID::src) > 0) { + src_href = stringf("%shref=\"%s\" ", (findColor(cell->name).empty() ? "" :" , "), escape(cell->attributes.at(ID::src).decode_string())); + } #ifdef CLUSTER_CELLS_AND_PORTBOXES if (!code.empty()) - fprintf(f, "subgraph cluster_c%d {\nc%d [ shape=record, label=\"%s\"%s ];\n%s}\n", - id2num(cell->name), id2num(cell->name), label_string.c_str(), color.c_str(), code.c_str()); + fprintf(f, "subgraph cluster_c%d {\nc%d [ shape=record, label=\"%s\"%s%s ];\n%s}\n", + id2num(cell->name), id2num(cell->name), label_string.c_str(), color.c_str(), src_href.c_str(), code.c_str()); else #endif - fprintf(f, "c%d [ shape=record, label=\"%s\", %s ];\n%s", - id2num(cell->name), label_string.c_str(), findColor(cell->name).c_str(), code.c_str()); + fprintf(f, "c%d [ shape=record, label=\"%s\", %s%s ];\n%s", + id2num(cell->name), label_string.c_str(), findColor(cell->name).c_str(), src_href.c_str(), code.c_str()); } for (auto &it : module->processes) @@ -608,12 +617,12 @@ struct ShowWorker } ShowWorker(FILE *f, RTLIL::Design *design, std::vector &libs, uint32_t colorSeed, bool genWidthLabels, - bool genSignedLabels, bool stretchIO, bool enumerateIds, bool abbreviateIds, bool notitle, + bool genSignedLabels, bool stretchIO, bool enumerateIds, bool abbreviateIds, bool notitle, bool href, const std::vector> &color_selections, const std::vector> &label_selections, RTLIL::IdString colorattr) : f(f), design(design), currentColor(colorSeed), genWidthLabels(genWidthLabels), genSignedLabels(genSignedLabels), stretchIO(stretchIO), enumerateIds(enumerateIds), abbreviateIds(abbreviateIds), - notitle(notitle), color_selections(color_selections), label_selections(label_selections), colorattr(colorattr) + notitle(notitle), href(href), color_selections(color_selections), label_selections(label_selections), colorattr(colorattr) { ct.setup_internals(); ct.setup_internals_mem(); @@ -726,6 +735,10 @@ struct ShowPass : public Pass { log(" don't run viewer in the background, IE wait for the viewer tool to\n"); log(" exit before returning\n"); log("\n"); + log(" -href\n"); + log(" adds href attribute to all items representing cells and wires, using\n"); + log(" src attribute of origin\n"); + log("\n"); log("When no is specified, 'dot' is used. When no and is\n"); log("specified, 'xdot' is used to display the schematic (POSIX systems only).\n"); log("\n"); @@ -763,6 +776,7 @@ struct ShowPass : public Pass { bool flag_enum = false; bool flag_abbreviate = true; bool flag_notitle = false; + bool flag_href = false; bool custom_prefix = false; std::string background = "&"; RTLIL::IdString colorattr; @@ -850,6 +864,10 @@ struct ShowPass : public Pass { background= ""; continue; } + if (arg == "-href") { + flag_href = true; + continue; + } break; } extra_args(args, argidx, design); @@ -894,7 +912,7 @@ struct ShowPass : public Pass { delete lib; log_cmd_error("Can't open dot file `%s' for writing.\n", dot_file.c_str()); } - ShowWorker worker(f, design, libs, colorSeed, flag_width, flag_signed, flag_stretch, flag_enum, flag_abbreviate, flag_notitle, color_selections, label_selections, colorattr); + ShowWorker worker(f, design, libs, colorSeed, flag_width, flag_signed, flag_stretch, flag_enum, flag_abbreviate, flag_notitle, flag_href, color_selections, label_selections, colorattr); fclose(f); for (auto lib : libs) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index d34373c1c..85107b68f 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -28,6 +28,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct cell_area_t { + double area; + bool is_sequential; +}; + struct statdata_t { #define STAT_INT_MEMBERS X(num_wires) X(num_wire_bits) X(num_pub_wires) X(num_pub_wire_bits) \ @@ -39,6 +44,7 @@ struct statdata_t STAT_INT_MEMBERS #undef X double area; + double sequential_area; string tech; std::map techinfo; @@ -74,7 +80,7 @@ struct statdata_t #undef X } - statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_area, string techname) + statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict &cell_area, string techname) { tech = techname; @@ -132,10 +138,16 @@ struct statdata_t } if (!cell_area.empty()) { - if (cell_area.count(cell_type)) - area += cell_area.at(cell_type); - else + if (cell_area.count(cell_type)) { + cell_area_t cell_data = cell_area.at(cell_type); + if (cell_data.is_sequential) { + sequential_area += cell_data.area; + } + area += cell_data.area; + } + else { unknown_cell_area.insert(cell_type); + } } num_cells++; @@ -244,6 +256,7 @@ struct statdata_t if (area != 0) { log("\n"); log(" Chip area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), area); + log(" of which used for sequential elements: %f (%.2f%%)\n", sequential_area, 100.0*sequential_area/area); } if (tech == "xilinx") @@ -325,7 +338,7 @@ statdata_t hierarchy_worker(std::map &mod_stat, RTL return mod_data; } -void read_liberty_cellarea(dict &cell_area, string liberty_file) +void read_liberty_cellarea(dict &cell_area, string liberty_file) { std::ifstream f; f.open(liberty_file.c_str()); @@ -341,8 +354,9 @@ void read_liberty_cellarea(dict &cell_area, string liberty_fil continue; LibertyAst *ar = cell->find("area"); + bool is_flip_flop = cell->find("ff") != nullptr; if (ar != nullptr && !ar->value.empty()) - cell_area["\\" + cell->args[0]] = atof(ar->value.c_str()); + cell_area["\\" + cell->args[0]] = {/*area=*/atof(ar->value.c_str()), is_flip_flop}; } } @@ -383,7 +397,7 @@ struct StatPass : public Pass { bool width_mode = false, json_mode = false; RTLIL::Module *top_mod = nullptr; std::map mod_stat; - dict cell_area; + dict cell_area; string techname; size_t argidx; diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 2c9d82914..59974a1e6 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -339,6 +339,8 @@ struct EquivSimplePass : public Pass { CellTypes ct; ct.setup_internals(); ct.setup_stdcells(); + ct.setup_internals_ff(); + ct.setup_stdcells_mem(); for (auto module : design->selected_modules()) { diff --git a/passes/memory/memory_collect.cc b/passes/memory/memory_collect.cc index bf3bb34f8..157042c9c 100644 --- a/passes/memory/memory_collect.cc +++ b/passes/memory/memory_collect.cc @@ -39,6 +39,9 @@ struct MemoryCollectPass : public Pass { log_header(design, "Executing MEMORY_COLLECT pass (generating $mem cells).\n"); extra_args(args, 1, design); for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + for (auto &mem : Mem::get_selected_memories(module)) { if (!mem.packed) { mem.packed = true; diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc index 2e683b8eb..77a4eb81b 100644 --- a/passes/memory/memory_libmap.cc +++ b/passes/memory/memory_libmap.cc @@ -2229,6 +2229,9 @@ struct MemoryLibMapPass : public Pass { Library lib = parse_library(lib_files, defines); for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + MapWorker worker(module); auto mems = Mem::get_selected_memories(module); for (auto &mem : mems) diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index e2f74c2e1..cafc0aaf3 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -493,6 +493,9 @@ struct MemoryMapPass : public Pass { extra_args(args, argidx, design); for (auto mod : design->selected_modules()) { + if (mod->has_processes_warn()) + continue; + MemoryMapWorker worker(design, mod); worker.attr_icase = attr_icase; worker.attributes = attributes; diff --git a/passes/memory/memory_memx.cc b/passes/memory/memory_memx.cc index 7edc26caa..22aebb43f 100644 --- a/passes/memory/memory_memx.cc +++ b/passes/memory/memory_memx.cc @@ -50,7 +50,7 @@ struct MemoryMemxPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { - log_header(design, "Executing MEMORY_MEMX pass (converting $mem cells to logic and flip-flops).\n"); + log_header(design, "Executing MEMORY_MEMX pass (emit soft logic for out-of-bounds handling).\n"); extra_args(args, 1, design); for (auto module : design->selected_modules()) diff --git a/passes/memory/memory_narrow.cc b/passes/memory/memory_narrow.cc index cf5e43465..46c538bab 100644 --- a/passes/memory/memory_narrow.cc +++ b/passes/memory/memory_narrow.cc @@ -46,6 +46,9 @@ struct MemoryNarrowPass : public Pass { extra_args(args, argidx, design); for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + for (auto &mem : Mem::get_selected_memories(module)) { bool wide = false; diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc index 8b2354ef8..e06989f4a 100644 --- a/passes/memory/memory_share.cc +++ b/passes/memory/memory_share.cc @@ -558,8 +558,12 @@ struct MemorySharePass : public Pass { extra_args(args, argidx, design); MemoryShareWorker msw(design, flag_widen, flag_sat); - for (auto module : design->selected_modules()) + for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + msw(module); + } } } MemorySharePass; diff --git a/passes/opt/opt_mem.cc b/passes/opt/opt_mem.cc index 885b6f97d..9a2d8e6a5 100644 --- a/passes/opt/opt_mem.cc +++ b/passes/opt/opt_mem.cc @@ -52,6 +52,9 @@ struct OptMemPass : public Pass { int total_count = 0; for (auto module : design->selected_modules()) { + if (module->has_processes_warn()) + continue; + SigMap sigmap(module); FfInitVals initvals(&sigmap, module); for (auto &mem : Mem::get_selected_memories(module)) { diff --git a/passes/proc/proc_dlatch.cc b/passes/proc/proc_dlatch.cc index 8340e1431..5b392ce51 100644 --- a/passes/proc/proc_dlatch.cc +++ b/passes/proc/proc_dlatch.cc @@ -46,7 +46,7 @@ struct proc_dlatch_db_t for (auto cell : module->cells()) { - if (cell->type.in(ID($mux), ID($pmux))) + if (cell->type.in(ID($mux), ID($pmux), ID($bwmux))) { auto sig_y = sigmap(cell->getPort(ID::Y)); for (int i = 0; i < GetSize(sig_y); i++) @@ -186,6 +186,8 @@ struct proc_dlatch_db_t Cell *cell = it->second.first; int index = it->second.second; + log_assert(cell->type.in(ID($mux), ID($pmux), ID($bwmux))); + bool is_bwmux = (cell->type == ID($bwmux)); SigSpec sig_a = sigmap(cell->getPort(ID::A)); SigSpec sig_b = sigmap(cell->getPort(ID::B)); SigSpec sig_s = sigmap(cell->getPort(ID::S)); @@ -200,12 +202,16 @@ struct proc_dlatch_db_t sig[index] = State::Sx; cell->setPort(ID::A, sig); } - for (int i = 0; i < GetSize(sig_s); i++) - n = make_inner(sig_s[i], State::S0, n); + if (!is_bwmux) { + for (int i = 0; i < GetSize(sig_s); i++) + n = make_inner(sig_s[i], State::S0, n); + } else { + n = make_inner(sig_s[index], State::S0, n); + } children.insert(n); } - for (int i = 0; i < GetSize(sig_s); i++) { + for (int i = 0; i < (is_bwmux ? 1 : GetSize(sig_s)); i++) { n = find_mux_feedback(sig_b[i*width + index], needle, set_undef); if (n != false_node) { if (set_undef && sig_b[i*width + index] == needle) { @@ -213,7 +219,7 @@ struct proc_dlatch_db_t sig[i*width + index] = State::Sx; cell->setPort(ID::B, sig); } - children.insert(make_inner(sig_s[i], State::S1, n)); + children.insert(make_inner(sig_s[is_bwmux ? index : i], State::S1, n)); } } diff --git a/passes/proc/proc_rom.cc b/passes/proc/proc_rom.cc index b83466ce7..ebc2377aa 100644 --- a/passes/proc/proc_rom.cc +++ b/passes/proc/proc_rom.cc @@ -66,6 +66,11 @@ struct RomWorker } } + if (lhs.empty()) { + log_debug("rejecting switch: lhs empty\n"); + return; + } + int swsigbits = 0; for (int i = 0; i < GetSize(sw->signal); i++) if (sw->signal[i] != State::S0) diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 05879426e..acebea6c5 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -543,13 +543,13 @@ struct EvalPass : public Pass { int pos = 0; for (auto &c : tabsigs.chunks()) { - tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width))); + tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width), false)); pos += c.width; } pos = 0; for (auto &c : signal.chunks()) { - tab_line.push_back(log_signal(value.extract(pos, c.width))); + tab_line.push_back(log_signal(value.extract(pos, c.width), false)); pos += c.width; } diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index 97d8b76f3..9d57e3d71 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -56,5 +56,5 @@ EXTRA_OBJS += passes/techmap/filterlib.o $(PROGRAM_PREFIX)yosys-filterlib$(EXE): passes/techmap/filterlib.o $(Q) mkdir -p $(dir $@) - $(P) $(LD) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS) + $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LINKFLAGS) $^ $(LIBS) endif diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 12c3a95de..78bfe1586 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -115,7 +115,7 @@ static bool parse_pin(LibertyAst *cell, LibertyAst *attr, std::string &pin_name, return false; } -static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval) +static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, std::vector &dont_use_cells) { LibertyAst *best_cell = nullptr; std::map best_cell_ports; @@ -135,6 +135,18 @@ static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has if (dn != nullptr && dn->value == "true") continue; + bool dont_use = false; + for (std::string &dont_use_cell : dont_use_cells) + { + if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str())) + { + dont_use = true; + break; + } + } + if (dont_use) + continue; + LibertyAst *ff = cell->find("ff"); if (ff == nullptr) continue; @@ -227,7 +239,7 @@ static void find_cell(LibertyAst *ast, IdString cell_type, bool clkpol, bool has } } -static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool setpol, bool clrpol) +static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool setpol, bool clrpol, std::vector &dont_use_cells) { LibertyAst *best_cell = nullptr; std::map best_cell_ports; @@ -247,6 +259,18 @@ static void find_cell_sr(LibertyAst *ast, IdString cell_type, bool clkpol, bool if (dn != nullptr && dn->value == "true") continue; + bool dont_use = false; + for (std::string &dont_use_cell : dont_use_cells) + { + if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str())) + { + dont_use = true; + break; + } + } + if (dont_use) + continue; + LibertyAst *ff = cell->find("ff"); if (ff == nullptr) continue; @@ -414,7 +438,7 @@ struct DfflibmapPass : public Pass { void help() override { log("\n"); - log(" dfflibmap [-prepare] [-map-only] [-info] -liberty [selection]\n"); + log(" dfflibmap [-prepare] [-map-only] [-info] [-dont_use ] -liberty [selection]\n"); log("\n"); log("Map internal flip-flop cells to the flip-flop cells in the technology\n"); log("library specified in the given liberty file.\n"); @@ -435,6 +459,11 @@ struct DfflibmapPass : public Pass { log("that would be passed to the dfflegalize pass. The design will not be\n"); log("changed.\n"); log("\n"); + log("When called with -dont_use, this command will not map to the specified cell\n"); + log("name as an alternative to setting the dont_use property in the Liberty file.\n"); + log("This argument can be called multiple times with different cell names. This\n"); + log("argument also supports simple glob patterns in the cell name.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -446,6 +475,8 @@ struct DfflibmapPass : public Pass { bool map_only_mode = false; bool info_mode = false; + std::vector dont_use_cells; + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -467,6 +498,10 @@ struct DfflibmapPass : public Pass { info_mode = true; continue; } + if (arg == "-dont_use" && argidx+1 < args.size()) { + dont_use_cells.push_back(args[++argidx]); + continue; + } break; } extra_args(args, argidx, design); @@ -491,26 +526,26 @@ struct DfflibmapPass : public Pass { LibertyParser libparser(f); f.close(); - find_cell(libparser.ast, ID($_DFF_N_), false, false, false, false); - find_cell(libparser.ast, ID($_DFF_P_), true, false, false, false); + find_cell(libparser.ast, ID($_DFF_N_), false, false, false, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_P_), true, false, false, false, dont_use_cells); - find_cell(libparser.ast, ID($_DFF_NN0_), false, true, false, false); - find_cell(libparser.ast, ID($_DFF_NN1_), false, true, false, true); - find_cell(libparser.ast, ID($_DFF_NP0_), false, true, true, false); - find_cell(libparser.ast, ID($_DFF_NP1_), false, true, true, true); - find_cell(libparser.ast, ID($_DFF_PN0_), true, true, false, false); - find_cell(libparser.ast, ID($_DFF_PN1_), true, true, false, true); - find_cell(libparser.ast, ID($_DFF_PP0_), true, true, true, false); - find_cell(libparser.ast, ID($_DFF_PP1_), true, true, true, true); + find_cell(libparser.ast, ID($_DFF_NN0_), false, true, false, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_NN1_), false, true, false, true, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_NP0_), false, true, true, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_NP1_), false, true, true, true, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PN0_), true, true, false, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PN1_), true, true, false, true, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PP0_), true, true, true, false, dont_use_cells); + find_cell(libparser.ast, ID($_DFF_PP1_), true, true, true, true, dont_use_cells); - find_cell_sr(libparser.ast, ID($_DFFSR_NNN_), false, false, false); - find_cell_sr(libparser.ast, ID($_DFFSR_NNP_), false, false, true); - find_cell_sr(libparser.ast, ID($_DFFSR_NPN_), false, true, false); - find_cell_sr(libparser.ast, ID($_DFFSR_NPP_), false, true, true); - find_cell_sr(libparser.ast, ID($_DFFSR_PNN_), true, false, false); - find_cell_sr(libparser.ast, ID($_DFFSR_PNP_), true, false, true); - find_cell_sr(libparser.ast, ID($_DFFSR_PPN_), true, true, false); - find_cell_sr(libparser.ast, ID($_DFFSR_PPP_), true, true, true); + find_cell_sr(libparser.ast, ID($_DFFSR_NNN_), false, false, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_NNP_), false, false, true, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_NPN_), false, true, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_NPP_), false, true, true, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PNN_), true, false, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PNP_), true, false, true, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PPN_), true, true, false, dont_use_cells); + find_cell_sr(libparser.ast, ID($_DFFSR_PPP_), true, true, true, dont_use_cells); log(" final dff cell mappings:\n"); logmap_all(); diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index 144f596c8..db395315c 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -1041,8 +1041,8 @@ struct TechmapPass : public Pass { log("\n"); log("When a port on a module in the map file has the 'techmap_autopurge' attribute\n"); log("set, and that port is not connected in the instantiation that is mapped, then\n"); - log("then a cell port connected only to such wires will be omitted in the mapped\n"); - log("version of the circuit.\n"); + log("a cell port connected only to such wires will be omitted in the mapped version\n"); + log("of the circuit.\n"); log("\n"); log("All wires in the modules from the map file matching the pattern _TECHMAP_*\n"); log("or *._TECHMAP_* are special wires that are used to pass instructions from\n"); diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc index e5013678a..74a484d59 100644 --- a/techlibs/common/synth.cc +++ b/techlibs/common/synth.cc @@ -88,6 +88,10 @@ struct SynthPass : public ScriptPass { log(" read/write collision\" (same result as setting the no_rw_check\n"); log(" attribute on all memories).\n"); log("\n"); + log(" -extra-map filename\n"); + log(" source extra rules from the given file to complement the default\n"); + log(" mapping library in the `techmap` step. this option can be\n"); + log(" repeated.\n"); log("\n"); log("The following commands are executed by this synthesis command:\n"); help_script(); @@ -96,8 +100,8 @@ struct SynthPass : public ScriptPass { string top_module, fsm_opts, memory_opts, abc; bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth; - int lut; + std::vector techmap_maps; void clear_flags() override { @@ -115,6 +119,7 @@ struct SynthPass : public ScriptPass { flowmap = false; booth = false; abc = "abc"; + techmap_maps.clear(); } void execute(std::vector args, RTLIL::Design *design) override @@ -151,7 +156,7 @@ struct SynthPass : public ScriptPass { flatten = true; continue; } - if (args[argidx] == "-lut") { + if (args[argidx] == "-lut" && argidx + 1 < args.size()) { lut = atoi(args[++argidx].c_str()); continue; } @@ -192,6 +197,10 @@ struct SynthPass : public ScriptPass { memory_opts += " -no-rw-check"; continue; } + if (args[argidx] == "-extra-map" && argidx + 1 < args.size()) { + techmap_maps.push_back(args[++argidx]); + continue; + } break; } extra_args(args, argidx, design); @@ -261,7 +270,17 @@ struct SynthPass : public ScriptPass { run("opt -fast -full"); run("memory_map"); run("opt -full"); - run("techmap"); + if (help_mode) { + run("techmap", " (unless -extra-map)"); + run("techmap -map +/techmap.v -map ", " (if -extra-map)"); + } else { + std::string techmap_opts; + if (!techmap_maps.empty()) + techmap_opts += " -map +/techmap.v"; + for (auto fn : techmap_maps) + techmap_opts += stringf(" -map %s", fn.c_str()); + run("techmap" + techmap_opts); + } if (help_mode) { run("techmap -map +/gate2lut.v", "(if -noabc and -lut)"); run("clean; opt_lut", " (if -noabc and -lut)"); diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh index 6bf91b4dc..2b26d8c98 100755 --- a/tests/gen-tests-makefile.sh +++ b/tests/gen-tests-makefile.sh @@ -16,8 +16,8 @@ generate_target() { # $ generate_ys_test ys_file [yosys_args] generate_ys_test() { ys_file=$1 - yosys_args=${2:-} - generate_target "$ys_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${ys_file%.*}.log $yosys_args $ys_file" + yosys_args_=${2:-} + generate_target "$ys_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${ys_file%.*}.log $yosys_args_ $ys_file" } # $ generate_bash_test bash_file diff --git a/tests/proc/proc_rom.ys b/tests/proc/proc_rom.ys index 0ef2e2c61..93fd5002b 100644 --- a/tests/proc/proc_rom.ys +++ b/tests/proc/proc_rom.ys @@ -186,4 +186,27 @@ design -stash preopt equiv_opt -assert -run prepare: dummy +design -reset +read_ilang < ${prefix}_pass.sby generate_sby fail > ${prefix}_fail.sby - sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby - sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby + + # Check that SBY is up to date enough for this yosys version + if sby --help | grep -q -e '--status'; then + set -x + sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby + sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby + else + echo "sva test '${prefix}' requires an up to date SBY, skipping" + fi else generate_sby pass > ${prefix}.sby - sby --yosys $PWD/../../yosys -f ${prefix}.sby + + # Check that SBY is up to date enough for this yosys version + if sby --help | grep -q -e '--status'; then + set -x + sby --yosys $PWD/../../yosys -f ${prefix}.sby + else + echo "sva test '${prefix}' requires an up to date SBY, skipping" + fi fi +{ set +x; } &>/dev/null + touch $prefix.ok diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index b0a7d6b7e..e8b125456 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -58,3 +58,10 @@ select -assert-count 4 t:$_NOT_ select -assert-count 1 t:dffn select -assert-count 4 t:dffsr select -assert-none t:dffn t:dffsr t:$_NOT_ %% %n t:* %i + +design -load orig +dfflibmap -liberty dfflibmap.lib -dont_use *ffn +clean + +select -assert-count 0 t:dffn +select -assert-count 5 t:dffsr diff --git a/tests/unit/Makefile b/tests/unit/Makefile index 9f1e5c99e..b4a752f8f 100644 --- a/tests/unit/Makefile +++ b/tests/unit/Makefile @@ -15,7 +15,7 @@ TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o))) all: prepare $(TESTS) run-tests $(BINTEST)/%: $(OBJTEST)/%.o - $(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LDLIBS) \ + $(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LIBS) \ $(GTESTFLAG) $(EXTRAFLAGS) $(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc diff --git a/tests/various/celledges_shift.ys b/tests/various/celledges_shift.ys new file mode 100644 index 000000000..753c8641e --- /dev/null +++ b/tests/various/celledges_shift.ys @@ -0,0 +1 @@ +test_cell -s 1705659041 -n 100 -edges $shift $shiftx $shl $shr $sshl $sshr diff --git a/tests/xprop/test.py b/tests/xprop/test.py index a275b0d93..e2cddf679 100644 --- a/tests/xprop/test.py +++ b/tests/xprop/test.py @@ -270,8 +270,9 @@ if "prepare" in steps: print("initial begin", file=tb_file) for pattern in patterns: + # A[0] might be the clock which requires special sequencing print( - f' gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5', + f' #0; gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5', file=tb_file, )