mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-27 19:18:49 +00:00
Code Activity

Merge pull request #18 from YosysHQ/master

Browse source 
bump fork for version 0.39
This commit is contained in:
Eder Monteiro 2024-03-12 14:03:27 -03:00 • committed by GitHub
commit 216a82a8da
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
52 changed files with 1239 additions and 439 deletions
Download patch file Download diff file Expand all files Collapse all files

1
.github/workflows/test-linux.yml vendored
View file

@ -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

3
.github/workflows/test-macos.yml vendored
View file

@ -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

23
CHANGELOG
View file

@ -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

159
Makefile
View file

@ -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

2
README.md
View file

@ -1,7 +1,7 @@
```
yosys -- Yosys Open SYnthesis Suite
Copyright (C) 2012 - 2020 Claire Xenia Wolf <claire@yosyshq.com>
Copyright (C) 2012 - 2024 Claire Xenia Wolf <claire@yosyshq.com>
Permission to use, copy, modify, and/or distribute this software for any
purpose with or without fee is hereby granted, provided that the above

17
backends/aiger/aiger.cc
View file

@ -67,6 +67,8 @@ struct AigerWriter
int initstate_ff = 0;
dict<SigBit, int> ywmap_clocks;
vector<Cell *> ywmap_asserts;
vector<Cell *> 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();
}

9
backends/cxxrtl/Makefile.inc
View file

@ -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))

325
backends/cxxrtl/cxxrtl_backend.cc
View file

@ -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<RTLIL::IdString, RTLIL::Const> 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<std::string> 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<std::string> 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<class ObserverT>\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<class ObserverT>\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<bb_p_debug>\n");

12
backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc
View file

@ -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;
}

4
backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h
View file

@ -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);

70
backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
View file

@ -1331,14 +1331,15 @@ struct debug_items {
std::map<std::string, std::vector<debug_item>> table;
std::map<std::string, std::unique_ptr<debug_attrs>> attrs_table;
void add(const std::string &name, debug_item &&item, metadata_map &&item_attrs = {}) {
std::unique_ptr<debug_attrs> &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<debug_attrs> &attrs = attrs_table[path];
if (attrs.get() == nullptr)
attrs = std::unique_ptr<debug_attrs>(new debug_attrs);
for (auto attr : item_attrs)
attrs->map.insert(attr);
item.attrs = attrs.get();
std::vector<debug_item> &parts = table[name];
std::vector<debug_item> &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<debug_item> &at(const std::string &name) const {
return table.at(name);
const std::vector<debug_item> &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<debug_item> &parts = table.at(name);
const debug_item &operator [](const std::string &path) const {
const std::vector<debug_item> &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<debug_attrs> module_attrs;
std::unique_ptr<debug_attrs> cell_attrs;
};
struct debug_scopes {
std::map<std::string, debug_scope> 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<debug_attrs>(new debug_attrs { module_attrs });
scope.cell_attrs = std::unique_ptr<debug_attrs>(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);
}
};

143
backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h
View file

@ -49,11 +49,16 @@
// <file> ::= <file-header> <definitions> <sample>+
// <file-header> ::= 0x52585843 0x00004c54
// <definitions> ::= <packet-define>* <packet-end>
// <sample> ::= <packet-sample> <packet-change>* <packet-end>
// <sample> ::= <packet-sample> (<packet-change> | <packet-diag>)* <packet-end>
// <packet-define> ::= 0xc0000000 ...
// <packet-sample> ::= 0xc0000001 ...
// <packet-change> ::= 0x0??????? <chunk>+ | 0x1??????? <index> <chunk>+ | 0x2??????? | 0x3???????
// <chunk>, <index> ::= 0x????????
// <packet-diag> ::= <packet-break> | <packet-print> | <packet-assert> | <packet-assume>
// <packet-break> ::= 0xc0000010 <message> <source-location>
// <packet-print> ::= 0xc0000011 <message> <source-location>
// <packet-assert> ::= 0xc0000012 <message> <source-location>
// <packet-assume> ::= 0xc0000013 <message> <source-location>
// <packet-end> ::= 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<typename ...Args>
recorder(Args &&...args) : writer(std::forward<Args>(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<const chunk_t*, spool::ident_t> *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<typename ...Args>
player(Args &&...args) : reader(std::forward<Args>(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<diagnostic> 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<diagnostic> *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<diagnostic> *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<diagnostic> *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;
}

13
backends/smt2/smt2.cc
View file

@ -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)));

95
backends/smt2/smtbmc.py
View file

@ -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)

95
backends/smt2/smtbmc_incremental.py
View file

@ -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,
}

108
backends/smt2/smtio.py
View file

@ -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

2
docs/source/CHAPTER_CellLib.rst
View file

@ -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

2
frontends/ast/ast.cc
View file

@ -1820,7 +1820,7 @@ std::string AstModule::derive_common(RTLIL::Design *design, const dict<RTLIL::Id
AstNode *new_ast = ast->clone();
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) {

2
frontends/ast/simplify.cc
View file

@ -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;
}

157
kernel/celledges.cc
View file

@ -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;
}

40
kernel/register.cc
View file

@ -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<std::string>, 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 <claire@yosyshq.com> |\n");
log(" | |\n");
log(" | Permission to use, copy, modify, and/or distribute this software for any |\n");
log(" | purpose with or without fee is hereby granted, provided that the above |\n");
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

2
kernel/rtlil.h
View file

@ -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;
}
};

28
kernel/yosys.cc
View file

@ -55,7 +55,7 @@
# include <glob.h>
#endif
#ifdef __FreeBSD__
#if defined(__FreeBSD__) || defined(__NetBSD__)
# include <sys/sysctl.h>
#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 <claire@yosyshq.com> |\n");
log(" | |\n");
log(" | Permission to use, copy, modify, and/or distribute this software for any |\n");
log(" | purpose with or without fee is hereby granted, provided that the above |\n");
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 <claire@yosyshq.com> |\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;

5
libs/ezsat/Makefile
View file

@ -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

11
libs/subcircuit/Makefile
View file

@ -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

19
misc/yosys-config.in Normal file → Executable file
View file

@ -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

29
passes/cmds/connect.cc
View file

@ -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 <lhs-expr> <rhs-expr>\n");
log(" connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr> [selection]\n");
log("\n");
log("Create a connection. This is equivalent to adding the statement 'assign\n");
log("<lhs-expr> = <rhs-expr>;' 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 <expr>\n");
log(" connect [-nomap] -unset <expr> [selection]\n");
log("\n");
log("Unconnect all existing drivers for the specified expression.\n");
log("\n");
log("\n");
log(" connect [-nomap] [-assert] -port <cell> <port> <expr>\n");
log(" connect [-nomap] [-assert] -port <cell> <port> <expr> [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<std::string> 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)

15
passes/cmds/rename.cc
View file

@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &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<RTLIL::Module *, int> &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);

36
passes/cmds/show.cc
View file

@ -65,6 +65,7 @@ struct ShowWorker
bool enumerateIds;
bool abbreviateIds;
bool notitle;
bool href;
int page_counter;
const std::vector<std::pair<std::string, RTLIL::Selection>> &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<RTLIL::Design*> &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<std::pair<std::string, RTLIL::Selection>> &color_selections,
const std::vector<std::pair<std::string, RTLIL::Selection>> &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 <format> is specified, 'dot' is used. When no <format> and <viewer> 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)

28
passes/cmds/stat.cc
View file

@ -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<RTLIL::IdString, int> techinfo;
@ -74,7 +80,7 @@ struct statdata_t
#undef X
}
statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict<IdString, double> &cell_area, string techname)
statdata_t(RTLIL::Design *design, RTLIL::Module *mod, bool width_mode, const dict<IdString, cell_area_t> &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<RTLIL::IdString, statdata_t> &mod_stat, RTL
return mod_data;
}
void read_liberty_cellarea(dict<IdString, double> &cell_area, string liberty_file)
void read_liberty_cellarea(dict<IdString, cell_area_t> &cell_area, string liberty_file)
{
std::ifstream f;
f.open(liberty_file.c_str());
@ -341,8 +354,9 @@ void read_liberty_cellarea(dict<IdString, double> &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<RTLIL::IdString, statdata_t> mod_stat;
dict<IdString, double> cell_area;
dict<IdString, cell_area_t> cell_area;
string techname;
size_t argidx;

2
passes/equiv/equiv_simple.cc
View file

@ -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())
{

3
passes/memory/memory_collect.cc
View file

@ -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;

3
passes/memory/memory_libmap.cc
View file

@ -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)

3
passes/memory/memory_map.cc
View file

@ -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;

2
passes/memory/memory_memx.cc
View file

@ -50,7 +50,7 @@ struct MemoryMemxPass : public Pass {
}
void execute(std::vector<std::string> 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())

3
passes/memory/memory_narrow.cc
View file

@ -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;

6
passes/memory/memory_share.cc
View file

@ -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;

3
passes/opt/opt_mem.cc
View file

@ -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)) {

16
passes/proc/proc_dlatch.cc
View file

@ -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));
}
}

5
passes/proc/proc_rom.cc
View file

@ -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)

4
passes/sat/eval.cc
View file

@ -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;
}

2
passes/techmap/Makefile.inc
View file

@ -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

77
passes/techmap/dfflibmap.cc
View file

@ -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<std::string> &dont_use_cells)
{
LibertyAst *best_cell = nullptr;
std::map<std::string, char> 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<std::string> &dont_use_cells)
{
LibertyAst *best_cell = nullptr;
std::map<std::string, char> 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 <file> [selection]\n");
log(" dfflibmap [-prepare] [-map-only] [-info] [-dont_use <cell_name>] -liberty <file> [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<std::string> args, RTLIL::Design *design) override
{
@ -446,6 +475,8 @@ struct DfflibmapPass : public Pass {
bool map_only_mode = false;
bool info_mode = false;
std::vector<std::string> 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();

4
passes/techmap/techmap.cc
View file

@ -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");

25
techlibs/common/synth.cc
View file

@ -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<std::string> 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<std::string> 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 <inject>", " (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)");

4
tests/gen-tests-makefile.sh
View file

@ -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

23
tests/proc/proc_rom.ys
View file

@ -186,4 +186,27 @@ design -stash preopt
equiv_opt -assert -run prepare: dummy
design -reset
read_ilang <<EOT
module \m
wire width 3 input 1 \a
process \p
switch \a
case 3'000
case 3'001
case 3'010
case 3'011
case 3'100
case 3'101
case 3'110
case 3'111
end
end
end
EOT
proc_rom

25
tests/sva/runtest.sh
View file

@ -1,6 +1,6 @@
#!/usr/bin/env bash
set -ex
set -e
prefix=${1%.ok}
prefix=${prefix%.sv}
@ -58,16 +58,33 @@ generate_sby() {
}
if [ -f $prefix.ys ]; then
set -x
$PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys
elif [ -f $prefix.sv ]; then
generate_sby pass > ${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

7
tests/techmap/dfflibmap.ys
View file

@ -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

2
tests/unit/Makefile
View file

@ -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

1
tests/various/celledges_shift.ys Normal file
View file

@ -0,0 +1 @@
test_cell -s 1705659041 -n 100 -edges $shift $shiftx $shl $shr $sshl $sshr

3
tests/xprop/test.py
View file

@ -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,
)