diff --git a/.github/actions/setup-build-env/action.yml b/.github/actions/setup-build-env/action.yml index 60fe481e7..c9dc5fc22 100644 --- a/.github/actions/setup-build-env/action.yml +++ b/.github/actions/setup-build-env/action.yml @@ -42,7 +42,7 @@ runs: if: runner.os == 'Linux' && inputs.get-build-deps == 'true' uses: awalsh128/cache-apt-pkgs-action@v1.6.0 with: - packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev + packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev libgtest-dev version: ${{ inputs.runs-on }}-buildys - name: Linux docs dependencies @@ -52,15 +52,6 @@ runs: packages: graphviz xdot version: ${{ inputs.runs-on }}-docsys - # if updating test dependencies, make sure to update - # docs/source/yosys_internals/extending_yosys/test_suites.rst to match. - - name: Linux test dependencies - if: runner.os == 'Linux' && inputs.get-test-deps == 'true' - uses: awalsh128/cache-apt-pkgs-action@v1.6.0 - with: - packages: libgtest-dev - version: ${{ inputs.runs-on }}-testys - - name: Install macOS Dependencies if: runner.os == 'macOS' shell: bash diff --git a/.github/workflows/extra-builds.yml b/.github/workflows/extra-builds.yml index 5d0ac72d4..8af99def8 100644 --- a/.github/workflows/extra-builds.yml +++ b/.github/workflows/extra-builds.yml @@ -103,6 +103,7 @@ jobs: ENABLE_ZLIB := 0 CXXFLAGS += -I$(pwd)/flex-prefix/include + LINKFLAGS += -Wl,-z,stack-size=8388608 -Wl,--stack-first -Wl,--strip-all END make -C build -f ../Makefile CXX=clang -j$(nproc) diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index ab6eb3148..ebdeb15d8 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -72,6 +72,7 @@ jobs: cd build make -f ../Makefile config-$CC make -f ../Makefile -j$procs + make -f ../Makefile unit-test -j$procs - name: Log yosys-config output run: | @@ -81,7 +82,7 @@ jobs: shell: bash run: | cd build - tar -cvf ../build.tar share/ yosys yosys-* + tar -cvf ../build.tar share/ yosys yosys-* libyosys.so - name: Store build artifact uses: actions/upload-artifact@v4 @@ -131,7 +132,7 @@ jobs: - name: Run tests shell: bash run: | - make -j$procs test TARGETS= EXTRA_TARGETS= CONFIG=$CC + make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= CONFIG=$CC - name: Report errors if: ${{ failure() }} diff --git a/.github/workflows/test-sanitizers.yml b/.github/workflows/test-sanitizers.yml index 11a339cd3..7650470c3 100644 --- a/.github/workflows/test-sanitizers.yml +++ b/.github/workflows/test-sanitizers.yml @@ -65,7 +65,7 @@ jobs: - name: Run tests shell: bash run: | - make -j$procs test TARGETS= EXTRA_TARGETS= + make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= - name: Report errors if: ${{ failure() }} @@ -73,7 +73,3 @@ jobs: run: | find tests/**/*.err -print -exec cat {} \; - - name: Run unit tests - shell: bash - run: | - make -j$procs unit-test ENABLE_LIBYOSYS=1 diff --git a/.github/workflows/test-verific-cfg.yml b/.github/workflows/test-verific-cfg.yml new file mode 100644 index 000000000..232ca6bd7 --- /dev/null +++ b/.github/workflows/test-verific-cfg.yml @@ -0,0 +1,109 @@ +name: Build various Verific configurations + +on: + workflow_dispatch: + +jobs: + test-verific-cfg: + if: github.repository_owner == 'YosysHQ' + runs-on: [self-hosted, linux, x64, fast] + steps: + - name: Checkout Yosys + uses: actions/checkout@v4 + with: + persist-credentials: false + submodules: true + - name: Runtime environment + run: | + echo "procs=$(nproc)" >> $GITHUB_ENV + + - name: verific [SV] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [VHDL] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + VHDL] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + HIER] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [VHDL + HIER] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + VHDL + HIER] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + VHDL + HIER + EDIF + LIBERTY] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml index adc6f59d8..cd2545cc8 100644 --- a/.github/workflows/test-verific.yml +++ b/.github/workflows/test-verific.yml @@ -68,7 +68,7 @@ jobs: - name: Run Yosys tests run: | - make -j$procs test + make -j$procs vanilla-test - name: Run Verific specific Yosys tests run: | @@ -80,11 +80,6 @@ jobs: run: | make -C sby run_ci - - name: Run unit tests - shell: bash - run: | - make -j$procs unit-test ENABLE_LTO=1 ENABLE_LIBYOSYS=1 - test-pyosys: needs: pre-job if: ${{ needs.pre-job.outputs.should_skip != 'true' && github.repository == 'YosysHQ/Yosys' }} diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml deleted file mode 100644 index b32498baf..000000000 --- a/.github/workflows/update-flake-lock.yml +++ /dev/null @@ -1,25 +0,0 @@ -name: update-flake-lock -on: - workflow_dispatch: # allows manual triggering - schedule: - - cron: '0 0 * * 0' # runs weekly on Sunday at 00:00 - -jobs: - lockfile: - if: github.repository == 'YosysHQ/Yosys' - runs-on: ubuntu-latest - steps: - - name: Checkout repository - uses: actions/checkout@v4 - with: - persist-credentials: false - - name: Install Nix - uses: DeterminateSystems/nix-installer-action@main - - name: Update flake.lock - uses: DeterminateSystems/update-flake-lock@main - with: - token: ${{CI_CREATE_PR_TOKEN}} - pr-title: "Update flake.lock" # Title of PR to be created - pr-labels: | # Labels to be set on the PR - dependencies - automated diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml deleted file mode 100644 index 78d34db46..000000000 --- a/.github/workflows/version.yml +++ /dev/null @@ -1,34 +0,0 @@ -name: Bump version - -on: - workflow_dispatch: - schedule: - - cron: '0 0 * * *' - -jobs: - bump-version: - if: github.repository == 'YosysHQ/Yosys' - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: true - persist-credentials: false - - name: Take last commit - id: log - run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT - - name: Bump version - if: ${{ !contains(steps.log.outputs.message, 'Bump version') }} - run: | - make bumpversion - git config --local user.email "41898282+github-actions[bot]@users.noreply.github.com" - git config --local user.name "github-actions[bot]" - git add Makefile - git commit -m "Bump version" - - name: Push changes # push the output folder to your repo - if: ${{ !contains(steps.log.outputs.message, 'Bump version') }} - uses: ad-m/github-push-action@master - with: - github_token: ${{ secrets.GITHUB_TOKEN }} diff --git a/CHANGELOG b/CHANGELOG index e345a8514..372a59d58 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,9 +2,24 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.62 .. Yosys 0.63-dev +Yosys 0.63 .. Yosys 0.64-dev -------------------------- +Yosys 0.62 .. Yosys 0.63 +-------------------------- + * Various + - Added DSP inference for Gowin GW1N and GW2A. + - Added support for subtract in preadder for Xilinx arch. + - Added infrastructure to run a sat solver as a command. + + * New commands and options + - Added "-ignore-unknown-cells" option to "equiv_induct" + and "equiv_simple" pass. + - Added "-force-params" option to "memory_libmap" pass. + - Added "-select-solver" option to "sat" pass. + - Added "-default_params" option to "write_verilog" pass. + - Added "-nodsp" option to "synth_gowin" pass. + Yosys 0.61 .. Yosys 0.62 -------------------------- * Various diff --git a/Dockerfile b/Dockerfile deleted file mode 100644 index 9806696e0..000000000 --- a/Dockerfile +++ /dev/null @@ -1,58 +0,0 @@ -ARG IMAGE="python:3-slim-buster" - -#--- - -FROM $IMAGE AS base - -RUN apt-get update -qq \ - && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ - ca-certificates \ - clang \ - lld \ - curl \ - libffi-dev \ - libreadline-dev \ - tcl-dev \ - graphviz \ - xdot \ - && apt-get autoclean && apt-get clean && apt-get -y autoremove \ - && update-ca-certificates \ - && rm -rf /var/lib/apt/lists - -#--- - -FROM base AS build - -RUN apt-get update -qq \ - && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ - bison \ - flex \ - gawk \ - gcc \ - git \ - iverilog \ - pkg-config \ - && apt-get autoclean && apt-get clean && apt-get -y autoremove \ - && rm -rf /var/lib/apt/lists - -COPY . /yosys - -ENV PREFIX /opt/yosys - -RUN cd /yosys \ - && make \ - && make install \ - && make test - -#--- - -FROM base - -COPY --from=build /opt/yosys /opt/yosys - -ENV PATH /opt/yosys/bin:$PATH - -RUN useradd -m yosys -USER yosys - -CMD ["yosys"] diff --git a/Makefile b/Makefile index 81f9e0652..507c74a63 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,19 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.62+9 +YOSYS_VER := 0.63 + +ifneq (, $(shell command -v git 2>/dev/null)) +ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) + GIT_COMMIT_COUNT := $(or $(shell git rev-list --count v$(YOSYS_VER)..HEAD 2>/dev/null),0) + ifneq ($(GIT_COMMIT_COUNT),0) + YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT) + endif +else + YOSYS_VER := $(YOSYS_VER)+post +endif +endif + YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2) @@ -185,9 +197,6 @@ endif OBJS = kernel/version_$(GIT_REV).o -bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7326bb7.. | wc -l`/;" Makefile - ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) # set ABCEXTERNAL = to use an external ABC instance @@ -638,6 +647,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h)) $(eval $(call add_include_file,kernel/yw.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) +$(eval $(call add_include_file,libs/ezsat/ezcmdline.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,libs/fst/fstapi.h)) endif @@ -683,6 +693,7 @@ OBJS += libs/json11/json11.o OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o +OBJS += libs/ezsat/ezcmdline.o OBJS += libs/minisat/Options.o OBJS += libs/minisat/SimpSolver.o @@ -791,9 +802,30 @@ endif $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $< +YOSYS_REPO := +ifneq (, $(shell command -v git 2>/dev/null)) +ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) + GIT_REMOTE := $(strip $(shell git config --get remote.origin.url 2>/dev/null | $(AWK) '{print tolower($$0)}')) + ifneq ($(strip $(GIT_REMOTE)),) + YOSYS_REPO := $(strip $(shell echo $(GIT_REMOTE) | $(AWK) -F '[:/]' '{gsub(/\.git$$/, "", $$NF); printf "%s/%s", $$(NF-1), $$NF}')) + endif + ifeq ($(strip $(YOSYS_REPO)),yosyshq/yosys) + YOSYS_REPO := + endif + GIT_BRANCH := $(shell git rev-parse --abbrev-ref HEAD 2>/dev/null) + ifeq ($(filter main HEAD release/v%,$(GIT_BRANCH)),) + YOSYS_REPO := $(YOSYS_REPO) at $(GIT_BRANCH) + endif + YOSYS_REPO := $(strip $(YOSYS_REPO)) +endif +endif + YOSYS_GIT_STR := $(GIT_REV)$(GIT_DIRTY) YOSYS_COMPILER := $(notdir $(CXX)) $(shell $(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1) $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)) YOSYS_VER_STR := Yosys $(YOSYS_VER) (git sha1 $(YOSYS_GIT_STR), $(YOSYS_COMPILER)) +ifneq ($(strip $(YOSYS_REPO)),) + YOSYS_VER_STR := $(YOSYS_VER_STR) [$(YOSYS_REPO)] +endif kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile $(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc @@ -977,9 +1009,11 @@ makefile-tests/%: %/run-test.mk $(TARGETS) $(EXTRA_TARGETS) $(MAKE) -C $* -f run-test.mk +@echo "...passed tests in $*" -test: makefile-tests abcopt-tests seed-tests +test: vanilla-test unit-test + +vanilla-test: makefile-tests abcopt-tests seed-tests @echo "" - @echo " Passed \"make test\"." + @echo " Passed \"make vanilla-test\"." ifeq ($(ENABLE_VERIFIC),1) ifeq ($(YOSYS_NOVERIFIC),1) @echo " Ran tests without verific support due to YOSYS_NOVERIFIC=1." @@ -1011,11 +1045,11 @@ ystests: $(TARGETS) $(EXTRA_TARGETS) # Unit test unit-test: libyosys.so - @$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \ + @$(MAKE) -f $(UNITESTPATH)/Makefile CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \ CXXFLAGS="$(CXXFLAGS)" LINKFLAGS="$(LINKFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)" clean-unit-test: - @$(MAKE) -C $(UNITESTPATH) clean + @$(MAKE) -f $(UNITESTPATH)/Makefile clean install-dev: $(PROGRAM_PREFIX)yosys-config share $(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR) diff --git a/README.md b/README.md index 3b2f41768..df65a6a10 100644 --- a/README.md +++ b/README.md @@ -114,8 +114,8 @@ To build Yosys simply type 'make' in this directory. $ sudo make install Tests are located in the tests subdirectory and can be executed using the test -target. Note that you need gawk as well as a recent version of iverilog (i.e. -build from git). Then, execute tests via: +target. Note that you need gawk, a recent version of iverilog, and gtest. +Execute tests via: $ make test diff --git a/abc b/abc index 734f64d5b..8e401543d 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit 734f64d5b907158dc4337ee82b3b74566d74ba08 +Subproject commit 8e401543d3ecf65e3a3631c7a271793a4d356cb0 diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 95f4c19e2..0c49e84b8 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -930,7 +930,9 @@ struct AigerBackend : public Backend { log(" make indexes zero based, enable using map files with smt solvers.\n"); log("\n"); log(" -ywmap \n"); - log(" write a map file for conversion to and from yosys witness traces.\n"); + log(" write a map file for conversion to and from yosys witness traces,\n"); + log(" also allows for mapping AIGER bad-state properties and invariant\n"); + log(" constraints back to individual formal properties by name.\n"); log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 3d451117c..73ffcbf3e 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -95,7 +95,8 @@ bool VERILOG_BACKEND::id_is_verilog_escaped(const std::string &str) { PRIVATE_NAMESPACE_BEGIN -bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase; +bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, + noparallelcase, default_params; int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter; dict auto_name_map; std::set reg_wires; @@ -421,6 +422,13 @@ void dump_attributes(std::ostream &f, std::string indent, dictattributes, "\n", /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name)); @@ -2438,6 +2446,10 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) f << indent + " " << "reg " << id(initial_id) << " = 0;\n"; } + if (default_params) + for (auto p : module->parameter_default_values) + dump_parameter(f, indent + " ", p.first, p.second); + // first dump input / output according to their order in module->ports for (auto port : module->ports) dump_wire(f, indent + " ", module->wire(port)); @@ -2545,6 +2557,10 @@ struct VerilogBackend : public Backend { log(" use 'defparam' statements instead of the Verilog-2001 syntax for\n"); log(" cell parameters.\n"); log("\n"); + log(" -default_params\n"); + log(" emit module parameter declarations from\n"); + log(" parameter_default_values.\n"); + log("\n"); log(" -blackboxes\n"); log(" usually modules with the 'blackbox' attribute are ignored. with\n"); log(" this option set only the modules with the 'blackbox' attribute\n"); @@ -2582,6 +2598,7 @@ struct VerilogBackend : public Backend { siminit = false; simple_lhs = false; noparallelcase = false; + default_params = false; auto_prefix = ""; bool blackboxes = false; @@ -2642,6 +2659,10 @@ struct VerilogBackend : public Backend { defparam = true; continue; } + if (arg == "-defaultparams") { + default_params = true; + continue; + } if (arg == "-decimal") { decimal = true; continue; diff --git a/docs/source/conf.py b/docs/source/conf.py index a7da22d97..458040db0 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -6,7 +6,7 @@ import os project = 'YosysHQ Yosys' author = 'YosysHQ GmbH' copyright ='2026 YosysHQ GmbH' -yosys_ver = "0.62" +yosys_ver = "0.63" # select HTML theme html_theme = 'furo-ys' diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index 799c99b6f..cbf5dc7b0 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -3,9 +3,9 @@ Symbolic model checking .. todo:: check text context -.. note:: - - While it is possible to perform model checking directly in Yosys, it +.. note:: + + While it is possible to perform model checking directly in Yosys, it is highly recommended to use SBY or EQY for formal hardware verification. Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or @@ -117,3 +117,32 @@ Result with fixed :file:`axis_master.v`: Solving problem with 159144 variables and 441626 clauses.. SAT proof finished - no model found: SUCCESS! + +Witness framework and per-property tracking +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When using AIGER-based formal verification flows (such as the ``abc`` engine in +SBY), Yosys provides infrastructure for tracking individual formal +properties through the verification pipeline. + +The `rename -witness` pass assigns public names to all cells that participate in +the witness framework: + +- Witness signal cells: `$anyconst`, `$anyseq`, `$anyinit`, + `$allconst`, `$allseq` +- Formal property cells: `$assert`, `$assume`, `$cover`, `$live`, + `$fair`, `$check` + +These public names allow downstream tools to refer to individual properties by +their hierarchical path rather than by anonymous internal identifiers. + +The `write_aiger -ywmap` option generates a map file for conversion to and from +Yosys witness traces, and also allows for mapping AIGER bad-state properties and +invariant constraints back to individual formal properties by name. This enables +features like per-property pass/fail reporting (e.g. ``abc pdr`` with +``--keep-going`` mode). + +The `write_smt2` backend similarly uses the public witness names when emitting +SMT2 comments. Cells whose ``hdlname`` attribute contains the ``_witness_`` +marker are treated as having private names for comment purposes, keeping solver +output clean. diff --git a/docs/source/yosys_internals/extending_yosys/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst index 81a79e77f..d3422b23a 100644 --- a/docs/source/yosys_internals/extending_yosys/test_suites.rst +++ b/docs/source/yosys_internals/extending_yosys/test_suites.rst @@ -8,7 +8,44 @@ Running the included test suite The Yosys source comes with a test suite to avoid regressions and keep everything working as expected. Tests can be run by calling ``make test`` from -the root Yosys directory. +the root Yosys directory. By default, this runs vanilla and unit tests. + +Vanilla tests +~~~~~~~~~~~~~ + +These make up the majority of our testing coverage. +They can be run with ``make vanilla-test`` and are based on calls to +make subcommands (``make makefile-tests``) and shell scripts +(``make seed-tests`` and ``make abcopt-tests``). Both use ``run-test.sh`` +files, but make-based tests only call ``tests/gen-tests-makefile.sh`` +to generate a makefile appropriate for the given directory, so only +afterwards when make is invoked do the tests actually run. + +Usually their structure looks something like this: +you write a .ys file that gets automatically run, +which runs a frontend like ``read_verilog`` or ``read_rtlil`` with +a relative path or a heredoc, then runs some commands including the command +under test, and then uses :doc:`/using_yosys/more_scripting/selections` +with ``-assert-count``. Usually it's unnecessary to "register" the test anywhere +as if it's being added to an existing directory, depending +on how the ``run-test.sh`` in that directory works. + +Unit tests +~~~~~~~~~~ + +Running the unit tests requires the following additional packages: + +.. tab:: Ubuntu + + .. code:: console + + sudo apt-get install libgtest-dev + +.. tab:: macOS + + No additional requirements. + +Unit tests can be run with ``make unit-test``. Functional tests ~~~~~~~~~~~~~~~~ @@ -41,23 +78,6 @@ instructions `_. Then, set the :makevar:`ENABLE_FUNCTIONAL_TESTS` make variable when calling ``make test`` and the functional tests will be run as well. -Unit tests -~~~~~~~~~~ - -Running the unit tests requires the following additional packages: - -.. tab:: Ubuntu - - .. code:: console - - sudo apt-get install libgtest-dev - -.. tab:: macOS - - No additional requirements. - -Unit tests can be run with ``make unit-test``. - Docs tests ~~~~~~~~~~ diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 4df37c0cd..e55349aa7 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -286,10 +286,15 @@ end_of_header: RTLIL::IdString escaped_s = stringf("\\%s", s); RTLIL::Wire* wire; - if (c == 'i') wire = inputs[l1]; - else if (c == 'l') wire = latches[l1]; - else if (c == 'o') { + if (c == 'i') { + log_assert(l1 < inputs.size()); + wire = inputs[l1]; + } else if (c == 'l') { + log_assert(l1 < latches.size()); + wire = latches[l1]; + } else if (c == 'o') { wire = module->wire(escaped_s); + log_assert(l1 < outputs.size()); if (wire) { // Could have been renamed by a latch module->swap_names(wire, outputs[l1]); @@ -297,9 +302,9 @@ end_of_header: goto next; } wire = outputs[l1]; - } - else if (c == 'b') wire = bad_properties[l1]; - else log_abort(); + } else if (c == 'b') { + wire = bad_properties[l1]; + } else log_abort(); module->rename(wire, escaped_s); } @@ -652,6 +657,9 @@ void AigerReader::parse_aiger_binary() unsigned l1, l2, l3; std::string line; + if (M != I + L + A) + log_error("Binary AIGER input is malformed: maximum variable index M is %u, but number of inputs, latches and AND gates adds up to %u.\n", M, I + L + A); + // Parse inputs int digits = decimal_digits(I); for (unsigned i = 1; i <= I; ++i) { diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index d9eb51a9c..65af26132 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -403,6 +403,18 @@ struct AST_INTERNAL::ProcessGenerator if (GetSize(syncrule->signal) != 1) always->input_error("Found posedge/negedge event on a signal that is not 1 bit wide!\n"); addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true); + // Automatic (nosync) variables must not become flip-flops: remove + // them from clocked sync rules so that proc_dff does not infer + // an unnecessary register for a purely combinational temporary. + syncrule->actions.erase( + std::remove_if(syncrule->actions.begin(), syncrule->actions.end(), + [](const RTLIL::SigSig &ss) { + for (auto &chunk : ss.first.chunks()) + if (chunk.wire && chunk.wire->get_bool_attribute(ID::nosync)) + return true; + return false; + }), + syncrule->actions.end()); proc->syncs.push_back(syncrule); } if (proc->syncs.empty()) { diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 30512d324..350d7cafe 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -629,6 +629,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool goto try_next_value; } } + log_assert(i < lutptr->size()); lutptr->set(i, !strcmp(output, "0") ? RTLIL::State::S0 : RTLIL::State::S1); try_next_value:; } diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc index 743ac5d9e..803931f32 100644 --- a/frontends/json/jsonparse.cc +++ b/frontends/json/jsonparse.cc @@ -302,6 +302,9 @@ void json_import(Design *design, string &modname, JsonNode *node) if (node->data_dict.count("attributes")) json_parse_attr_param(module->attributes, node->data_dict.at("attributes")); + if (node->data_dict.count("parameter_default_values")) + json_parse_attr_param(module->parameter_default_values, node->data_dict.at("parameter_default_values")); + dict signal_bits; if (node->data_dict.count("ports")) diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 684727d5b..148a6cc63 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -84,7 +84,7 @@ int current_function_or_task_port_id; std::vector case_type_stack; bool do_not_require_port_stubs; - bool current_wire_rand, current_wire_const; + bool current_wire_rand, current_wire_const, current_wire_automatic; bool current_modport_input, current_modport_output; bool default_nettype_wire = true; std::istream* lexin; @@ -958,14 +958,18 @@ delay: non_opt_delay | %empty; io_wire_type: - { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; } + { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; } wire_type_token_io wire_type_const_rand opt_wire_type_token wire_type_signedness { $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); }; non_io_wire_type: - { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; } - wire_type_const_rand wire_type_token wire_type_signedness - { $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); }; + { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; } + opt_lifetime wire_type_const_rand wire_type_token wire_type_signedness + { + if (extra->current_wire_automatic) + extra->astbuf3->set_attribute(ID::nosync, AstNode::mkconst_int(extra->astbuf3->location, 1, false)); + $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); + }; wire_type: io_wire_type { $$ = std::move($1); } | @@ -1253,6 +1257,10 @@ opt_automatic: TOK_AUTOMATIC | %empty; +opt_lifetime: + TOK_AUTOMATIC { extra->current_wire_automatic = true; } | + %empty; + task_func_args_opt: TOK_LPAREN TOK_RPAREN | %empty | TOK_LPAREN { extra->albuf = nullptr; diff --git a/kernel/calc.cc b/kernel/calc.cc index 9b0885db9..84ac100ab 100644 --- a/kernel/calc.cc +++ b/kernel/calc.cc @@ -291,7 +291,7 @@ static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Co if (pos < 0) result.set(i, vacant_bits); else if (pos >= BigInteger(GetSize(arg1))) - result.set(i, sign_ext ? arg1.back() : vacant_bits); + result.set(i, sign_ext && !arg1.empty() ? arg1.back() : vacant_bits); else result.set(i, arg1[pos.toInt()]); } diff --git a/kernel/celledges.cc b/kernel/celledges.cc index c39ced95a..195d4b15b 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -112,6 +112,41 @@ void reduce_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) db->add_edge(cell, ID::A, i, ID::Y, 0, -1); } +void logic_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + + for (int i = 0; i < a_width; i++) + db->add_edge(cell, ID::A, i, ID::Y, 0, -1); + for (int i = 0; i < b_width; i++) + db->add_edge(cell, ID::B, i, ID::Y, 0, -1); +} + +void concat_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + + for (int i = 0; i < a_width; i++) + db->add_edge(cell, ID::A, i, ID::Y, i, -1); + for (int i = 0; i < b_width; i++) + db->add_edge(cell, ID::B, i, ID::Y, a_width + i, -1); +} + +void slice_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int offset = cell->getParam(ID::OFFSET).as_int(); + int a_width = GetSize(cell->getPort(ID::A)); + int y_width = GetSize(cell->getPort(ID::Y)); + + for (int i = 0; i < y_width; i++) { + int a_bit = offset + i; + if (a_bit >= 0 && a_bit < a_width) + db->add_edge(cell, ID::A, a_bit, ID::Y, i, -1); + } +} + void compare_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) { int a_width = GetSize(cell->getPort(ID::A)); @@ -254,7 +289,7 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) int skip = 1 << (k + 1); int base = skip -1; if (i % skip != base && i - a_width + 2 < 1 << b_width_capped) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); + db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else if (is_signed) { if (i - a_width + 2 < 1 << b_width_capped) db->add_edge(cell, ID::B, k, ID::Y, i, -1); @@ -388,6 +423,64 @@ void ff_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) db->add_edge(cell, ID::ARST, 0, ID::Q, k, -1); } +void full_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + std::vector input_ports; + std::vector output_ports; + + for (auto &conn : cell->connections()) + { + RTLIL::IdString port = conn.first; + RTLIL::PortDir dir = cell->port_dir(port); + if (cell->input(port) || dir == RTLIL::PortDir::PD_INOUT) + input_ports.push_back(port); + if (cell->output(port) || dir == RTLIL::PortDir::PD_INOUT) + output_ports.push_back(port); + } + + for (auto out_port : output_ports) + { + int out_width = GetSize(cell->getPort(out_port)); + for (int out_bit = 0; out_bit < out_width; out_bit++) + { + for (auto in_port : input_ports) + { + int in_width = GetSize(cell->getPort(in_port)); + for (int in_bit = 0; in_bit < in_width; in_bit++) + db->add_edge(cell, in_port, in_bit, out_port, out_bit, -1); + } + } + } +} + +void bweqx_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int width = GetSize(cell->getPort(ID::Y)); + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + int max_width = std::min(width, std::min(a_width, b_width)); + + for (int i = 0; i < max_width; i++) { + db->add_edge(cell, ID::A, i, ID::Y, i, -1); + db->add_edge(cell, ID::B, i, ID::Y, i, -1); + } +} + +void bwmux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int width = GetSize(cell->getPort(ID::Y)); + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + int s_width = GetSize(cell->getPort(ID::S)); + int max_width = std::min(width, std::min(a_width, std::min(b_width, s_width))); + + for (int i = 0; i < max_width; i++) { + db->add_edge(cell, ID::A, i, ID::Y, i, -1); + db->add_edge(cell, ID::B, i, ID::Y, i, -1); + db->add_edge(cell, ID::S, i, ID::Y, i, -1); + } +} + PRIVATE_NAMESPACE_END bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL::Cell *cell) @@ -417,6 +510,21 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } + if (cell->type.in(ID($logic_and), ID($logic_or))) { + logic_op(this, cell); + return true; + } + + if (cell->type == ID($slice)) { + slice_op(this, cell); + return true; + } + + if (cell->type == ID($concat)) { + concat_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; @@ -442,6 +550,16 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } + if (cell->type == ID($bweqx)) { + bweqx_op(this, cell); + return true; + } + + if (cell->type == ID($bwmux)) { + bwmux_op(this, cell); + return true; + } + if (cell->type.in(ID($mem_v2), ID($memrd), ID($memrd_v2), ID($memwr), ID($memwr_v2), ID($meminit))) { mem_op(this, cell); return true; @@ -452,13 +570,24 @@ 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 $macc_v2 $fa - // FIXME: $mul $div $mod $divfloor $modfloor $pow $slice $concat $bweqx - // FIXME: $lut $sop $alu $lcu $macc $fa $logic_and $logic_or $bwmux + if (cell->type.in(ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow))) { + full_op(this, cell); + return true; + } - // FIXME: $_BUF_ $_NOT_ $_AND_ $_NAND_ $_OR_ $_NOR_ $_XOR_ $_XNOR_ $_ANDNOT_ $_ORNOT_ - // FIXME: $_MUX_ $_NMUX_ $_MUX4_ $_MUX8_ $_MUX16_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_ + if (cell->type.in(ID($lut), ID($sop), ID($alu), ID($lcu), ID($macc), ID($macc_v2))) { + full_op(this, cell); + return true; + } + + if (cell->type.in( + ID($_BUF_), ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), + ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_), ID($_MUX_), ID($_NMUX_), + ID($_MUX4_), ID($_MUX8_), ID($_MUX16_), ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), + ID($_OAI4_), ID($_TBUF_))) { + full_op(this, cell); + return true; + } // FIXME: $specify2 $specify3 $specrule ??? // FIXME: $equiv $set_tag $get_tag $overwrite_tag $original_tag @@ -468,4 +597,3 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return false; } - diff --git a/kernel/modtools.h b/kernel/modtools.h index a081c7556..5cd8e3cb2 100644 --- a/kernel/modtools.h +++ b/kernel/modtools.h @@ -28,6 +28,22 @@ YOSYS_NAMESPACE_BEGIN struct ModIndex : public RTLIL::Monitor { + struct PointerOrderedSigBit : public RTLIL::SigBit { + PointerOrderedSigBit(SigBit s) { + wire = s.wire; + if (wire) + offset = s.offset; + else + data = s.data; + } + inline bool operator<(const RTLIL::SigBit &other) const { + if (wire == other.wire) + return wire ? (offset < other.offset) : (data < other.data); + if (wire != nullptr && other.wire != nullptr) + return wire < other.wire; // look here + return (wire != nullptr) < (other.wire != nullptr); + } + }; struct PortInfo { RTLIL::Cell* cell; RTLIL::IdString port; @@ -77,7 +93,7 @@ struct ModIndex : public RTLIL::Monitor SigMap sigmap; RTLIL::Module *module; - std::map database; + std::map database; int auto_reload_counter; bool auto_reload_module; @@ -94,8 +110,11 @@ struct ModIndex : public RTLIL::Monitor { for (int i = 0; i < GetSize(sig); i++) { RTLIL::SigBit bit = sigmap(sig[i]); - if (bit.wire) + if (bit.wire) { database[bit].ports.erase(PortInfo(cell, port, i)); + if (!database[bit].is_input && !database[bit].is_output && database[bit].ports.empty()) + database.erase(bit); + } } } @@ -132,11 +151,11 @@ struct ModIndex : public RTLIL::Monitor } } - void check() + bool ok() { #ifndef NDEBUG if (auto_reload_module) - return; + return true; for (auto it : database) log_assert(it.first == sigmap(it.first)); @@ -156,11 +175,17 @@ struct ModIndex : public RTLIL::Monitor else if (!(it.second == database_bak.at(it.first))) log("ModuleIndex::check(): Different content for database[%s].\n", log_signal(it.first)); - log_assert(database == database_bak); + return false; } + return true; #endif } + void check() + { + log_assert(ok()); + } + void notify_connect(RTLIL::Cell *cell, RTLIL::IdString port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) override { log_assert(module == cell->module); diff --git a/kernel/satgen.cc b/kernel/satgen.cc index f2c1e00c2..7fbcba1b2 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -19,6 +19,7 @@ #include "kernel/satgen.h" #include "kernel/ff.h" +#include "kernel/yosys_common.h" USING_YOSYS_NAMESPACE @@ -1378,7 +1379,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } - if (cell->type == ID($scopeinfo)) + if (cell->type == ID($scopeinfo) || cell->type == ID($input_port)) { return true; } @@ -1387,3 +1388,22 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) // .. and all sequential cells with asynchronous inputs return false; } + +namespace Yosys { + +void report_missing_model(bool warn_only, RTLIL::Cell* cell) +{ + std::string s; + if (cell->is_builtin_ff()) + s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); + else + s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); + + if (warn_only) { + log_formatted_warning_noprefix(s); + } else { + log_formatted_error(s); + } +} + +} diff --git a/kernel/satgen.h b/kernel/satgen.h index 7815847b3..c11d480a4 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -59,6 +59,7 @@ struct SatSolver struct ezSatPtr : public std::unique_ptr { ezSatPtr() : unique_ptr(yosys_satsolver->create()) { } + explicit ezSatPtr(SatSolver *solver) : unique_ptr((solver ? solver : yosys_satsolver)->create()) { } }; struct SatGen @@ -292,6 +293,8 @@ struct SatGen bool importCell(RTLIL::Cell *cell, int timestep = -1); }; +void report_missing_model(bool warn_only, RTLIL::Cell* cell); + YOSYS_NAMESPACE_END #endif diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc new file mode 100644 index 000000000..57800591c --- /dev/null +++ b/libs/ezsat/ezcmdline.cc @@ -0,0 +1,92 @@ + +#include "ezcmdline.h" + +#include "../../kernel/yosys.h" + +ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {} + +ezCmdlineSAT::~ezCmdlineSAT() {} + +bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +{ +#if !defined(YOSYS_DISABLE_SPAWN) + const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX"); + const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str()); + const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str()); + FILE *dimacs = fopen(cnf_filename.c_str(), "w"); + if (dimacs == nullptr) { + Yosys::log_cmd_error("Failed to create CNF file `%s`.\n", cnf_filename.c_str()); + } + + std::vector modelIdx; + for (auto id : modelExpressions) + modelIdx.push_back(bind(id)); + std::vector> extraClauses; + for (auto id : assumptions) + extraClauses.push_back({bind(id)}); + + printDIMACS(dimacs, false, extraClauses); + fclose(dimacs); + + bool status_sat = false; + bool status_unsat = false; + std::vector values; + + auto line_callback = [&](const std::string &line) { + if (line.empty()) { + return; + } + if (line[0] == 's') { + if (line.substr(0, 5) == "s SAT") { + status_sat = true; + } + if (line.substr(0, 7) == "s UNSAT") { + status_unsat = true; + } + return; + } + if (line[0] == 'v') { + std::stringstream ss(line.substr(1)); + int lit; + while (ss >> lit) { + if (lit == 0) { + return; + } + bool val = lit >= 0; + int ind = lit >= 0 ? lit - 1 : -lit - 1; + if (Yosys::GetSize(values) <= ind) { + values.resize(ind + 1); + } + values[ind] = val; + } + } + }; + int return_code = Yosys::run_command(sat_command, line_callback); + if (return_code != 0 && return_code != 10 && return_code != 20) { + Yosys::log_cmd_error("Shell command failed!\n"); + } + + modelValues.clear(); + modelValues.resize(modelIdx.size()); + + if (!status_sat && !status_unsat) { + solverTimeoutStatus = true; + } + if (!status_sat) { + return false; + } + + for (size_t i = 0; i < modelIdx.size(); i++) { + int idx = modelIdx[i]; + bool refvalue = true; + + if (idx < 0) + idx = -idx, refvalue = false; + + modelValues[i] = (values.at(idx - 1) == refvalue); + } + return true; +#else + Yosys::log_error("SAT solver command not available in this build!\n"); +#endif +} diff --git a/libs/ezsat/ezcmdline.h b/libs/ezsat/ezcmdline.h new file mode 100644 index 000000000..8ec8c7043 --- /dev/null +++ b/libs/ezsat/ezcmdline.h @@ -0,0 +1,36 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Claire Xenia Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#ifndef EZSATCOMMAND_H +#define EZSATCOMMAND_H + +#include "ezsat.h" + +class ezCmdlineSAT : public ezSAT +{ +private: + std::string command; + +public: + ezCmdlineSAT(const std::string &cmd); + virtual ~ezCmdlineSAT(); + bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) override; +}; + +#endif diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index 30df625cb..1f4b8855f 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector &modelExpressions, std::vector 0) { if (alarmHandlerTimeout == 0) - solverTimoutStatus = true; + solverTimeoutStatus = true; alarm(0); sigaction(SIGALRM, &old_sig_action, NULL); alarm(old_alarm_timeout); diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 20a210abe..8e3114705 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -54,7 +54,7 @@ ezSAT::ezSAT() cnfClausesCount = 0; solverTimeout = 0; - solverTimoutStatus = false; + solverTimeoutStatus = false; literal("CONST_TRUE"); literal("CONST_FALSE"); @@ -1222,10 +1222,15 @@ ezSATvec ezSAT::vec(const std::vector &vec) return ezSATvec(*this, vec); } -void ezSAT::printDIMACS(FILE *f, bool verbose) const +void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector> &extraClauses) const { + if (f == nullptr) { + fprintf(stderr, "Usage error: printDIMACS() must not be called with a null FILE pointer\n"); + abort(); + } + if (cnfConsumed) { - fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!"); + fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n"); abort(); } @@ -1259,8 +1264,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const std::vector> all_clauses; getFullCnf(all_clauses); assert(cnfClausesCount == int(all_clauses.size())); + for (auto c : extraClauses) + all_clauses.push_back(c); - fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount); + fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size()); int maxClauseLen = 0; for (auto &clause : all_clauses) maxClauseLen = std::max(int(clause.size()), maxClauseLen); diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 7f3bdf68d..445c8edba 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -78,7 +78,7 @@ protected: public: int solverTimeout; - bool solverTimoutStatus; + bool solverTimeoutStatus; ezSAT(); virtual ~ezSAT(); @@ -153,8 +153,8 @@ public: solverTimeout = newTimeoutSeconds; } - bool getSolverTimoutStatus() { - return solverTimoutStatus; + bool getSolverTimeoutStatus() { + return solverTimeoutStatus; } // manage CNF (usually only accessed by SAT solvers) @@ -295,7 +295,7 @@ public: // printing CNF and internal state - void printDIMACS(FILE *f, bool verbose = false) const; + void printDIMACS(FILE *f, bool verbose = false, const std::vector> &extraClauses = std::vector>()) const; void printInternalState(FILE *f) const; // more sophisticated constraints (designed to be used directly with assume(..)) diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 078ffb769..a07d588c4 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -254,18 +254,17 @@ struct RenamePass : public Pass { log("\n"); log(" rename -enumerate [-pattern ] [selection]\n"); log("\n"); - log("Assign short auto-generated names to all selected wires and cells with private\n"); - log("names. The -pattern option can be used to set the pattern for the new names.\n"); - log("The character %% in the pattern is replaced with a integer number. The default\n"); - log("pattern is '_%%_'.\n"); + log("Assigns auto-generated names to objects used in formal verification\n"); + log("that do not have a public name. This applies to all formal property\n"); + log("cells, $any*/$all* output wires, and their containing cells.\n"); log("\n"); log("\n"); log(" rename -witness\n"); log("\n"); - log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); - log("cells that do not have a public name. This ensures that, during formal\n"); - log("verification, a solver-found trace can be fully specified using a public\n"); - log("hierarchical names.\n"); + log("Assigns auto-generated names to objects used in formal verification\n"); + log("that do not have a public name. This applies to all formal property\n"); + log("cells ($assert, $assume, $cover, $live, $fair, $check), $any*/$all*\n"); + log("output wires, and their containing cells.\n"); log("\n"); log("\n"); log(" rename -hide [selection]\n"); diff --git a/passes/cmds/scratchpad.cc b/passes/cmds/scratchpad.cc index f64ce943c..24ab5cfd8 100644 --- a/passes/cmds/scratchpad.cc +++ b/passes/cmds/scratchpad.cc @@ -37,7 +37,7 @@ struct ScratchpadPass : public Pass { log("\n"); log(" scratchpad [options]\n"); log("\n"); - log("This pass allows to read and modify values from the scratchpad of the current\n"); + log("This pass allows reading and modifying values from the scratchpad of the current\n"); log("design. Options:\n"); log("\n"); log(" -get \n"); diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h new file mode 100644 index 000000000..95d4b25e9 --- /dev/null +++ b/passes/equiv/equiv.h @@ -0,0 +1,67 @@ +#ifndef EQUIV_H +#define EQUIV_H + +#include "kernel/log.h" +#include "kernel/yosys_common.h" +#include "kernel/sigtools.h" +#include "kernel/satgen.h" + +YOSYS_NAMESPACE_BEGIN + +struct EquivBasicConfig { + bool model_undef = false; + int max_seq = 1; + bool set_assumes = false; + bool ignore_unknown_cells = false; + + bool parse(const std::vector& args, size_t& idx) { + if (args[idx] == "-undef") { + model_undef = true; + return true; + } + if (args[idx] == "-seq" && idx+1 < args.size()) { + max_seq = atoi(args[++idx].c_str()); + return true; + } + if (args[idx] == "-set-assumes") { + set_assumes = true; + return true; + } + if (args[idx] == "-ignore-unknown-cells") { + ignore_unknown_cells = true; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return stringf( + " -undef\n" + " enable modelling of undef states\n" + "\n" + " -seq \n" + " the max. number of time steps to be considered (default = %s)\n" + "\n" + " -set-assumes\n" + " set all assumptions provided via $assume cells\n" + "\n" + " -ignore-unknown-cells\n" + " ignore all cells that can not be matched to a SAT model\n" + , default_seq); + } +}; + +template +struct EquivWorker { + RTLIL::Module *module; + + ezSatPtr ez; + SatGen satgen; + Config cfg; + + EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) { + satgen.model_undef = cfg.model_undef; + } +}; + +YOSYS_NAMESPACE_END +#endif // EQUIV_H diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index e1a3a7990..e4480c893 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -18,49 +18,34 @@ */ #include "kernel/yosys.h" -#include "kernel/satgen.h" -#include "kernel/sigtools.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivInductWorker +struct EquivInductWorker : public EquivWorker<> { - Module *module; SigMap sigmap; vector cells; pool workset; - ezSatPtr ez; - SatGen satgen; - - int max_seq; int success_counter; - bool set_assumes; dict ez_step_is_consistent; - pool cell_warn_cache; SigPool undriven_signals; - EquivInductWorker(Module *module, const pool &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, EquivBasicConfig cfg) : EquivWorker<>(module, &sigmap, cfg), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), - satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes) - { - satgen.model_undef = model_undef; - } + success_counter(0) {} void create_timestep(int step) { vector ez_equal_terms; for (auto cell : cells) { - if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) { - if (cell->is_builtin_ff()) - log_warning("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - cell_warn_cache.insert(cell); + if (!satgen.importCell(cell, step)) { + report_missing_model(cfg.ignore_unknown_cells, cell); } if (cell->type == ID($equiv)) { SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit(); @@ -78,7 +63,7 @@ struct EquivInductWorker } } - if (set_assumes) { + if (cfg.set_assumes) { if (step == 1) { RTLIL::SigSpec assumes_a, assumes_en; satgen.getAssumes(assumes_a, assumes_en, step); @@ -123,7 +108,7 @@ struct EquivInductWorker GetSize(satgen.initial_state), GetSize(undriven_signals)); } - for (int step = 1; step <= max_seq; step++) + for (int step = 1; step <= cfg.max_seq; step++) { ez->assume(ez_step_is_consistent[step]); @@ -146,7 +131,7 @@ struct EquivInductWorker return; } - log(" Proof for induction step failed. %s\n", step != max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset."); + log(" Proof for induction step failed. %s\n", step != cfg.max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset."); } workset.sort(); @@ -158,12 +143,12 @@ struct EquivInductWorker log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort(ID::Y)))); - int ez_a = satgen.importSigBit(bit_a, max_seq+1); - int ez_b = satgen.importSigBit(bit_b, max_seq+1); + int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1); + int ez_b = satgen.importSigBit(bit_b, cfg.max_seq+1); int cond = ez->XOR(ez_a, ez_b); if (satgen.model_undef) - cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1))); + cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, cfg.max_seq+1))); if (!ez->solve(cond)) { log(" success!\n"); @@ -189,14 +174,7 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); - log(" -undef\n"); - log(" enable modelling of undef states\n"); - log("\n"); - log(" -seq \n"); - log(" the max. number of time steps to be considered (default = 4)\n"); - log("\n"); - log(" -set-assumes\n"); - log(" set all assumptions provided via $assume cells\n"); + log("%s", EquivBasicConfig::help("4")); log("\n"); log("This command is very effective in proving complex sequential circuits, when\n"); log("the internal state of the circuit quickly propagates to $equiv cells.\n"); @@ -214,25 +192,15 @@ struct EquivInductPass : public Pass { void execute(std::vector args, Design *design) override { int success_counter = 0; - bool model_undef = false, set_assumes = false; - int max_seq = 4; + EquivBasicConfig cfg {}; + cfg.max_seq = 4; log_header(design, "Executing EQUIV_INDUCT pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-undef") { - model_undef = true; + if (cfg.parse(args, argidx)) continue; - } - if (args[argidx] == "-seq" && argidx+1 < args.size()) { - max_seq = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-set-assumes") { - set_assumes = true; - continue; - } break; } extra_args(args, argidx, design); @@ -253,7 +221,7 @@ struct EquivInductPass : public Pass { continue; } - EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes); + EquivInductWorker worker(module, unproven_equiv_cells, cfg); worker.run(); success_counter += worker.success_counter; } diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 97f95ac63..e498928c3 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -17,15 +17,51 @@ * */ +#include "kernel/log.h" #include "kernel/yosys.h" -#include "kernel/satgen.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivSimpleWorker +struct EquivSimpleConfig : EquivBasicConfig { + bool verbose = false; + bool short_cones = false; + bool group = true; + bool parse(const std::vector& args, size_t& idx) { + if (EquivBasicConfig::parse(args, idx)) + return true; + if (args[idx] == "-v") { + verbose = true; + return true; + } + if (args[idx] == "-short") { + short_cones = true; + return true; + } + if (args[idx] == "-nogroup") { + group = false; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return EquivBasicConfig::help(default_seq) + + " -v\n" + " verbose output\n" + "\n" + " -short\n" + " create shorter input cones that stop at shared nodes. This yields\n" + " simpler SAT problems but sometimes fails to prove equivalence.\n" + "\n" + " -nogroup\n" + " disabling grouping of $equiv cells by output wire\n" + "\n"; + } +}; + +struct EquivSimpleWorker : public EquivWorker { - Module *module; const vector &equiv_cells; const vector &assume_cells; struct Cone { @@ -43,27 +79,11 @@ struct EquivSimpleWorker }; DesignModel model; - ezSatPtr ez; - SatGen satgen; - - struct Config { - bool verbose = false; - bool short_cones = false; - bool model_undef = false; - bool nogroup = false; - bool set_assumes = false; - int max_seq = 1; - }; - Config cfg; - pool> imported_cells_cache; - EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, Config cfg) : - module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells), - model(model), satgen(ez.get(), &model.sigmap), cfg(cfg) - { - satgen.model_undef = cfg.model_undef; - } + EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, EquivSimpleConfig cfg) : + EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), + model(model) {} struct ConeFinder { DesignModel model; @@ -229,14 +249,6 @@ struct EquivSimpleWorker return extra_problem_cells; } - static void report_missing_model(Cell* cell) - { - if (cell->is_builtin_ff()) - log_cmd_error("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - } - void prepare_ezsat(int ez_context, SigBit bit_a, SigBit bit_b) { if (satgen.model_undef) @@ -257,7 +269,9 @@ struct EquivSimpleWorker } void construct_ezsat(const pool& input_bits, int step) { + log("ezsat\n"); if (cfg.set_assumes) { + log("yep assume\n"); if (cfg.verbose && step == cfg.max_seq) { RTLIL::SigSpec assumes_a, assumes_en; satgen.getAssumes(assumes_a, assumes_en, step+1); @@ -323,7 +337,7 @@ struct EquivSimpleWorker for (auto cell : problem_cells) { auto key = pair(cell, step+1); if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) { - report_missing_model(cell); + report_missing_model(cfg.ignore_unknown_cells, cell); } imported_cells_cache.insert(key); } @@ -414,59 +428,20 @@ struct EquivSimplePass : public Pass { log("\n"); log("This command tries to prove $equiv cells using a simple direct SAT approach.\n"); log("\n"); - log(" -v\n"); - log(" verbose output\n"); - log("\n"); - log(" -undef\n"); - log(" enable modelling of undef states\n"); - log("\n"); - log(" -short\n"); - log(" create shorter input cones that stop at shared nodes. This yields\n"); - log(" simpler SAT problems but sometimes fails to prove equivalence.\n"); - log("\n"); - log(" -nogroup\n"); - log(" disabling grouping of $equiv cells by output wire\n"); - log("\n"); - log(" -seq \n"); - log(" the max. number of time steps to be considered (default = 1)\n"); - log("\n"); - log(" -set-assumes\n"); - log(" set all assumptions provided via $assume cells\n"); + log("%s", EquivSimpleConfig::help("1")); log("\n"); } void execute(std::vector args, Design *design) override { - EquivSimpleWorker::Config cfg = {}; + EquivSimpleConfig cfg {}; int success_counter = 0; log_header(design, "Executing EQUIV_SIMPLE pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-v") { - cfg.verbose = true; + if (cfg.parse(args, argidx)) continue; - } - if (args[argidx] == "-short") { - cfg.short_cones = true; - continue; - } - if (args[argidx] == "-undef") { - cfg.model_undef = true; - continue; - } - if (args[argidx] == "-nogroup") { - cfg.nogroup = true; - continue; - } - if (args[argidx] == "-seq" && argidx+1 < args.size()) { - cfg.max_seq = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-set-assumes") { - cfg.set_assumes = true; - continue; - } break; } extra_args(args, argidx, design); @@ -489,7 +464,7 @@ struct EquivSimplePass : public Pass { if (cell->type == ID($equiv) && cell->getPort(ID::A) != cell->getPort(ID::B)) { auto bit = sigmap(cell->getPort(ID::Y).as_bit()); auto bit_group = bit; - if (!cfg.nogroup && bit_group.wire) + if (cfg.group && bit_group.wire) bit_group.offset = 0; unproven_equiv_cells[bit_group][bit] = cell; unproven_cells_counter++; diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc index c3c10363b..87adaa26d 100644 --- a/passes/memory/memory_libmap.cc +++ b/passes/memory/memory_libmap.cc @@ -39,6 +39,7 @@ struct PassOptions { bool no_auto_distributed; bool no_auto_block; bool no_auto_huge; + bool force_params; double logic_cost_rom; double logic_cost_ram; }; @@ -1859,7 +1860,7 @@ void MemMapping::emit_port(const MemConfig &cfg, std::vector &cells, cons cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren)); } else { cell->setPort(stringf("\\PORT_%s_WR_EN", name), hw_wren); - if (cfg.def->byte != 0 && cfg.def->width_mode != WidthMode::Single) + if (cfg.def->byte != 0 && (cfg.def->width_mode != WidthMode::Single || opts.force_params)) cell->setParam(stringf("\\PORT_%s_WR_EN_WIDTH", name), GetSize(hw_wren)); } } @@ -2068,8 +2069,10 @@ void MemMapping::emit(const MemConfig &cfg) { std::vector cells; for (int rd = 0; rd < cfg.repl_d; rd++) { Cell *cell = mem.module->addCell(stringf("%s.%d.%d", mem.memid, rp, rd), cfg.def->id); - if (cfg.def->width_mode == WidthMode::Global) + if (cfg.def->width_mode == WidthMode::Global || opts.force_params) cell->setParam(ID::WIDTH, cfg.def->dbits[cfg.base_width_log2]); + if (opts.force_params) + cell->setParam(ID::ABITS, cfg.def->abits); if (cfg.def->widthscale) { std::vector val; for (auto &bit: init_swz.bits[rd]) @@ -2179,6 +2182,9 @@ struct MemoryLibMapPass : public Pass { log(" Disables automatic mapping of given kind of RAMs. Manual mapping\n"); log(" (using ram_style or other attributes) is still supported.\n"); log("\n"); + log(" -force-params\n"); + log(" Always generate memories with WIDTH and ABITS parameters.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -2188,6 +2194,7 @@ struct MemoryLibMapPass : public Pass { opts.no_auto_distributed = false; opts.no_auto_block = false; opts.no_auto_huge = false; + opts.force_params = false; opts.logic_cost_ram = 1.0; opts.logic_cost_rom = 1.0/16.0; log_header(design, "Executing MEMORY_LIBMAP pass (mapping memories to cells).\n"); @@ -2214,6 +2221,10 @@ struct MemoryLibMapPass : public Pass { opts.no_auto_huge = true; continue; } + if (args[argidx] == "-force-params") { + opts.force_params = true; + continue; + } if (args[argidx] == "-logic-cost-rom" && argidx+1 < args.size()) { opts.logic_cost_rom = strtod(args[++argidx].c_str(), nullptr); continue; diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 90b85d709..9988eef62 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -31,6 +31,22 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +static SatSolver *find_satsolver(const std::string &name) +{ + for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next) + if (solver->name == name) + return solver; + return nullptr; +} + +static std::string list_satsolvers() +{ + std::string result; + for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next) + result += result.empty() ? solver->name : ", " + solver->name; + return result; +} + struct SatHelper { RTLIL::Design *design; @@ -60,8 +76,8 @@ struct SatHelper int max_timestep, timeout; bool gotTimeout; - SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) : - design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap) + SatHelper(RTLIL::Design *design, RTLIL::Module *module, SatSolver *solver, bool enable_undef, bool set_def_formal) : + design(design), module(module), sigmap(module), ct(design), ez(solver), satgen(ez.get(), &sigmap) { this->enable_undef = enable_undef; satgen.model_undef = enable_undef; @@ -227,16 +243,12 @@ struct SatHelper int import_cell_counter = 0; for (auto cell : module->cells()) if (design->selected(module, cell)) { - // log("Import cell: %s\n", RTLIL::id2cstr(cell->name)); if (satgen.importCell(cell, timestep)) { for (auto &p : cell->connections()) if (ct.cell_output(cell->type, p.first)) show_drivers.insert(sigmap(p.second), cell); import_cell_counter++; - } else if (ignore_unknown_cells) - log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); - else - log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); + } else report_missing_model(ignore_unknown_cells, cell); } log("Imported %d cells to SAT database.\n", import_cell_counter); @@ -441,7 +453,7 @@ struct SatHelper log_assert(gotTimeout == false); ez->setSolverTimeout(timeout); bool success = ez->solve(modelExpressions, modelValues, assumptions); - if (ez->getSolverTimoutStatus()) + if (ez->getSolverTimeoutStatus()) gotTimeout = true; return success; } @@ -451,7 +463,7 @@ struct SatHelper log_assert(gotTimeout == false); ez->setSolverTimeout(timeout); bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f); - if (ez->getSolverTimoutStatus()) + if (ez->getSolverTimeoutStatus()) gotTimeout = true; return success; } @@ -961,10 +973,10 @@ struct SatPass : public Pass { log(" -show-regs, -show-public, -show-all\n"); log(" show all registers, show signals with 'public' names, show all signals\n"); log("\n"); - log(" -ignore_div_by_zero\n"); + log(" -ignore-div-by-zero\n"); log(" ignore all solutions that involve a division by zero\n"); log("\n"); - log(" -ignore_unknown_cells\n"); + log(" -ignore-unknown-cells\n"); log(" ignore all cells that can not be matched to a SAT model\n"); log("\n"); log("The following options can be used to set up a sequential problem:\n"); @@ -1066,6 +1078,10 @@ struct SatPass : public Pass { log(" -timeout \n"); log(" Maximum number of seconds a single SAT instance may take.\n"); log("\n"); + log(" -select-solver \n"); + log(" Select SAT solver implementation for this invocation.\n"); + log(" If not given, uses scratchpad key 'sat.solver' if set, otherwise default.\n"); + log("\n"); log(" -verify\n"); log(" Return an error and stop the synthesis script if the proof fails.\n"); log("\n"); @@ -1097,8 +1113,14 @@ struct SatPass : public Pass { log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n"); + std::string solver_name = design->scratchpad_get_string("sat.solver", ""); + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-select-solver" && argidx+1 < args.size()) { + solver_name = args[++argidx]; + continue; + } if (args[argidx] == "-all") { loopcount = -1; continue; @@ -1141,7 +1163,7 @@ struct SatPass : public Pass { stepsize = max(1, atoi(args[++argidx].c_str())); continue; } - if (args[argidx] == "-ignore_div_by_zero") { + if (args[argidx] == "-ignore-div-by-zero" || args[argidx] == "-ignore_div_by_zero") { ignore_div_by_zero = true; continue; } @@ -1316,7 +1338,7 @@ struct SatPass : public Pass { show_all = true; continue; } - if (args[argidx] == "-ignore_unknown_cells") { + if (args[argidx] == "-ignore-unknown-cells" || args[argidx] == "-ignore_unknown_cells") { ignore_unknown_cells = true; continue; } @@ -1336,6 +1358,14 @@ struct SatPass : public Pass { } extra_args(args, argidx, design); + SatSolver *solver = yosys_satsolver; + if (!solver_name.empty()) { + solver = find_satsolver(solver_name); + if (solver == nullptr) + log_cmd_error("Unknown SAT solver '%s'. Available solvers: %s\n", + solver_name, list_satsolvers()); + } + RTLIL::Module *module = NULL; for (auto mod : design->selected_modules()) { if (module) @@ -1398,13 +1428,15 @@ struct SatPass : public Pass { shows.push_back(wire->name.str()); } + log("Using SAT solver `%s`.\n", solver->name.c_str()); + if (tempinduct) { if (loopcount > 0 || max_undef) log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n"); - SatHelper basecase(design, module, enable_undef, set_def_formal); - SatHelper inductstep(design, module, enable_undef, set_def_formal); + SatHelper basecase(design, module, solver, enable_undef, set_def_formal); + SatHelper inductstep(design, module, solver, enable_undef, set_def_formal); basecase.sets = sets; basecase.set_assumes = set_assumes; @@ -1593,7 +1625,7 @@ struct SatPass : public Pass { if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); - SatHelper sathelper(design, module, enable_undef, set_def_formal); + SatHelper sathelper(design, module, solver, enable_undef, set_def_formal); sathelper.sets = sets; sathelper.set_assumes = set_assumes; diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index f7fa095a0..6e5b1fba8 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -285,7 +285,7 @@ using AbcSigMap = SigValMap; struct RunAbcState { const AbcConfig &config; - std::string tempdir_name; + std::string per_run_tempdir_name; std::vector signal_list; bool did_run = false; bool err = false; @@ -836,16 +836,23 @@ std::string fold_abc_cmd(std::string str) return new_str; } -std::string replace_tempdir(std::string text, std::string tempdir_name, bool show_tempdir) +std::string replace_tempdir(std::string text, std::string_view global_tempdir_name, std::string_view per_run_tempdir_name, bool show_tempdir) { if (show_tempdir) return text; while (1) { - size_t pos = text.find(tempdir_name); + size_t pos = text.find(global_tempdir_name); if (pos == std::string::npos) break; - text = text.substr(0, pos) + "" + text.substr(pos + GetSize(tempdir_name)); + text = text.substr(0, pos) + "" + text.substr(pos + GetSize(global_tempdir_name)); + } + + while (1) { + size_t pos = text.find(per_run_tempdir_name); + if (pos == std::string::npos) + break; + text = text.substr(0, pos) + "" + text.substr(pos + GetSize(per_run_tempdir_name)); } std::string selfdir_name = proc_self_dirname(); @@ -867,11 +874,12 @@ struct abc_output_filter bool got_cr; int escape_seq_state; std::string linebuf; - std::string tempdir_name; + std::string global_tempdir_name; + std::string per_run_tempdir_name; bool show_tempdir; - abc_output_filter(RunAbcState& state, std::string tempdir_name, bool show_tempdir) - : state(state), tempdir_name(tempdir_name), show_tempdir(show_tempdir) + abc_output_filter(RunAbcState& state, std::string global_tempdir_name, std::string per_run_tempdir_name, bool show_tempdir) + : state(state), global_tempdir_name(global_tempdir_name), per_run_tempdir_name(per_run_tempdir_name), show_tempdir(show_tempdir) { got_cr = false; escape_seq_state = 0; @@ -898,7 +906,7 @@ struct abc_output_filter return; } if (ch == '\n') { - state.logs.log("ABC: %s\n", replace_tempdir(linebuf, tempdir_name, show_tempdir)); + state.logs.log("ABC: %s\n", replace_tempdir(linebuf, global_tempdir_name, per_run_tempdir_name, show_tempdir)); got_cr = false, linebuf.clear(); return; } @@ -999,15 +1007,15 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module const AbcConfig &config = run_abc.config; if (config.cleanup) - run_abc.tempdir_name = get_base_tmpdir() + "/"; + run_abc.per_run_tempdir_name = get_base_tmpdir() + "/"; else - run_abc.tempdir_name = "_tmp_"; - run_abc.tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX"; - run_abc.tempdir_name = make_temp_dir(run_abc.tempdir_name); + run_abc.per_run_tempdir_name = "_tmp_"; + run_abc.per_run_tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX"; + run_abc.per_run_tempdir_name = make_temp_dir(run_abc.per_run_tempdir_name); log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n", - module->name.c_str(), replace_tempdir(run_abc.tempdir_name, run_abc.tempdir_name, config.show_tempdir).c_str()); + module->name.c_str(), replace_tempdir(run_abc.per_run_tempdir_name, config.global_tempdir_name, run_abc.per_run_tempdir_name, config.show_tempdir).c_str()); - std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.tempdir_name); + std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.per_run_tempdir_name); if (!config.liberty_files.empty() || !config.genlib_files.empty()) { std::string dont_use_args; @@ -1073,8 +1081,8 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos)) abc_script = abc_script.substr(0, pos) + config.lutin_shared + abc_script.substr(pos+3); if (config.abc_dress) - abc_script += stringf("; dress \"%s/input.blif\"", run_abc.tempdir_name); - abc_script += stringf("; write_blif %s/output.blif", run_abc.tempdir_name); + abc_script += stringf("; dress \"%s/input.blif\"", run_abc.per_run_tempdir_name); + abc_script += stringf("; write_blif %s/output.blif", run_abc.per_run_tempdir_name); abc_script = add_echos_to_abc_cmd(abc_script); #if defined(REUSE_YOSYS_ABC_PROCESSES) if (config.is_yosys_abc()) @@ -1085,7 +1093,7 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module if (abc_script[i] == ';' && abc_script[i+1] == ' ') abc_script[i+1] = '\n'; - std::string buffer = stringf("%s/abc.script", run_abc.tempdir_name); + std::string buffer = stringf("%s/abc.script", run_abc.per_run_tempdir_name); FILE *f = fopen(buffer.c_str(), "wt"); if (f == nullptr) log_error("Opening %s for writing failed: %s\n", buffer, strerror(errno)); @@ -1220,7 +1228,7 @@ void RunAbcState::run(ConcurrentStack &process_pool) void RunAbcState::run(ConcurrentStack &) #endif { - std::string buffer = stringf("%s/input.blif", tempdir_name); + std::string buffer = stringf("%s/input.blif", per_run_tempdir_name); FILE *f = fopen(buffer.c_str(), "wt"); if (f == nullptr) { logs.log("Opening %s for writing failed: %s\n", buffer, strerror(errno)); @@ -1348,14 +1356,14 @@ void RunAbcState::run(ConcurrentStack &) return; } int ret; - std::string tmp_script_name = stringf("%s/abc.script", tempdir_name); + std::string tmp_script_name = stringf("%s/abc.script", per_run_tempdir_name); do { - logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, tempdir_name, config.show_tempdir)); + logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir)); errno = 0; - abc_output_filter filt(*this, tempdir_name, config.show_tempdir); + abc_output_filter filt(*this, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir); #ifdef YOSYS_LINK_ABC - string temp_stdouterr_name = stringf("%s/stdouterr.txt", tempdir_name); + string temp_stdouterr_name = stringf("%s/stdouterr.txt", per_run_tempdir_name); FILE *temp_stdouterr_w = fopen(temp_stdouterr_name.c_str(), "w"); if (temp_stdouterr_w == NULL) log_error("ABC: cannot open a temporary file for output redirection"); @@ -1502,7 +1510,7 @@ void AbcModuleState::extract(AbcSigMap &assign_map, RTLIL::Design *design, RTLIL return; } - std::string buffer = stringf("%s/%s", run_abc.tempdir_name, "output.blif"); + std::string buffer = stringf("%s/%s", run_abc.per_run_tempdir_name, "output.blif"); std::ifstream ifs; ifs.open(buffer); if (ifs.fail()) @@ -1789,7 +1797,7 @@ void AbcModuleState::finish() if (run_abc.config.cleanup) { log("Removing temp directory.\n"); - remove_directory(run_abc.tempdir_name); + remove_directory(run_abc.per_run_tempdir_name); } log_pop(); } diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 8b61a9299..16df82bb6 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -219,9 +219,7 @@ struct Abc9Pass : public ScriptPass for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; if ((arg == "-exe" || arg == "-script" || arg == "-D" || - /*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" || - /*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" || - arg == "-constr" || arg == "-dont_use" || arg == "-liberty") && + arg == "-lut" || arg == "-luts" || arg == "-W") && argidx+1 < args.size()) { if (arg == "-lut" || arg == "-luts") lut_mode = true; diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index 4449065f8..2baf53a02 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -248,7 +248,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe } abc9_script += stringf("; &ps -l; &write -n %s/output.aig", tempdir_name); - if (design->scratchpad_get_bool("abc9.verify")) { + if (design->scratchpad_get_bool("abc9.verify", true)) { if (dff_mode) abc9_script += "; &verify -s"; else diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc index 8d3869ece..7471ec700 100644 --- a/passes/techmap/abc9_ops.cc +++ b/passes/techmap/abc9_ops.cc @@ -23,6 +23,7 @@ #include "kernel/utils.h" #include "kernel/celltypes.h" #include "kernel/timinginfo.h" +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -587,6 +588,7 @@ void break_scc(RTLIL::Module *module) auto id = it->second; auto r = ids_seen.insert(id); cell->attributes.erase(it); + // Cut exactly one representative cell per SCC id. if (!r.second) continue; for (auto &c : cell->connections_) { @@ -710,8 +712,6 @@ void prep_xaiger(RTLIL::Module *module, bool dff) SigMap sigmap(module); - dict> bit_drivers, bit_users; - TopoSort toposort; dict> box_ports; for (auto cell : module->cells()) { @@ -750,39 +750,100 @@ void prep_xaiger(RTLIL::Module *module, bool dff) } } } - else if (!yosys_celltypes.cell_known(cell->type)) - continue; - - // TODO: Speed up toposort -- we care about box ordering only - for (auto conn : cell->connections()) { - if (cell->input(conn.first)) - for (auto bit : sigmap(conn.second)) - bit_users[bit].insert(cell->name); - - if (cell->output(conn.first) && !abc9_flop) - for (auto bit : sigmap(conn.second)) - bit_drivers[bit].insert(cell->name); - } - toposort.node(cell->name); } if (box_ports.empty()) return; - for (auto &it : bit_users) - if (bit_drivers.count(it.first)) - for (auto driver_cell : bit_drivers.at(it.first)) - for (auto user_cell : it.second) - toposort.edge(driver_cell, user_cell); + // Build the same topo graph for the initial pass and the optional retry. + auto build_toposort = [&](TopoSort &toposort) { + dict> bit_drivers, bit_users; - if (ys_debug(1)) - toposort.analyze_loops = true; + for (auto cell : module->cells()) { + if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_))) + continue; + if (cell->has_keep_attr()) + continue; - bool no_loops = toposort.sort(); + auto inst_module = design->module(cell->type); + bool abc9_flop = inst_module && inst_module->get_bool_attribute(ID::abc9_flop); + if (abc9_flop && !dff) + continue; + if (!(inst_module && inst_module->get_bool_attribute(ID::abc9_box)) && !yosys_celltypes.cell_known(cell->type)) + continue; + + // TODO: Speed up toposort -- we care about box ordering only + for (auto conn : cell->connections()) { + if (cell->input(conn.first)) + for (auto bit : sigmap(conn.second)) + bit_users[bit].insert(cell->name); + + if (cell->output(conn.first) && !abc9_flop) + for (auto bit : sigmap(conn.second)) + bit_drivers[bit].insert(cell->name); + } + toposort.node(cell->name); + } + + // Build producer -> consumer edges on sigmapped nets. + for (auto &it : bit_users) + if (bit_drivers.count(it.first)) + for (auto driver_cell : bit_drivers.at(it.first)) + for (auto user_cell : it.second) + toposort.edge(driver_cell, user_cell); + if (ys_debug(1)) + toposort.analyze_loops = true; + return toposort.sort(); + }; + + // Build TopoSort in a container, as we may need to conditionally rebuild it on retry. + std::optional> toposort; + toposort.emplace(); + bool no_loops = build_toposort(toposort.value()); + + // Fallback for residual loops after SCC cutting: insert additional + // breakers on non-box loop cells, then re-run toposort checks. + if (!no_loops) { + SigSpec I, O; + pool broken_cells; + + for (auto &loop : toposort.value().loops) + for (auto cell_name : loop) { + // Loop reports can overlap; cut each cell at most once. + if (!broken_cells.insert(cell_name).second) + continue; + auto cell = module->cell(cell_name); + log_assert(cell); + auto inst_module = design->module(cell->type); + if (inst_module && inst_module->get_bool_attribute(ID::abc9_box)) + continue; + for (auto &c : cell->connections_) { + if (c.second.is_fully_const()) continue; + if (cell->output(c.first)) { + Wire *w = module->addWire(NEW_ID, GetSize(c.second)); + I.append(w); + O.append(c.second); + c.second = w; + } + } + } + + if (!I.empty()) { + auto cell = module->addCell(NEW_ID, ID($__ABC9_SCC_BREAKER)); + log_assert(GetSize(I) == GetSize(O)); + cell->setParam(ID::WIDTH, GetSize(I)); + cell->setPort(ID::I, std::move(I)); + cell->setPort(ID::O, std::move(O)); + + // Rebuild topo ordering after inserting the additional breakers. + toposort.emplace(); + no_loops = build_toposort(toposort.value()); + } + } if (ys_debug(1)) { unsigned i = 0; - for (auto &it : toposort.loops) { + for (auto &it : toposort.value().loops) { log(" loop %d\n", i++); for (auto cell_name : it) { auto cell = module->cell(cell_name); @@ -806,7 +867,7 @@ void prep_xaiger(RTLIL::Module *module, bool dff) TimingInfo timing; int port_id = 1, box_count = 0; - for (auto cell_name : toposort.sorted) { + for (auto cell_name : toposort.value().sorted) { RTLIL::Cell *cell = module->cell(cell_name); log_assert(cell); diff --git a/techlibs/gowin/Makefile.inc b/techlibs/gowin/Makefile.inc index df1b79317..0744b1389 100644 --- a/techlibs/gowin/Makefile.inc +++ b/techlibs/gowin/Makefile.inc @@ -12,3 +12,4 @@ $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams_map_gw5a.v)) $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams.txt)) $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams_map.v)) $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams.txt)) +$(eval $(call add_share_file,share/gowin,techlibs/gowin/dsp_map.v)) diff --git a/techlibs/gowin/brams_map.v b/techlibs/gowin/brams_map.v index 774896e79..6187eadac 100644 --- a/techlibs/gowin/brams_map.v +++ b/techlibs/gowin/brams_map.v @@ -205,7 +205,7 @@ output [PORT_A_WIDTH-1:0] PORT_B_RD_DATA; wire RSTA = OPTION_RESET_MODE == "SYNC" ? PORT_A_RD_SRST : PORT_A_RD_ARST; wire RSTB = OPTION_RESET_MODE == "SYNC" ? PORT_B_RD_SRST : PORT_B_RD_ARST; -wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_B_WR_BE); +wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_A_WR_BE); wire [13:0] ADB = `addrbe(PORT_B_WIDTH, PORT_B_ADDR, PORT_B_WR_BE); generate diff --git a/techlibs/gowin/brams_map_gw5a.v b/techlibs/gowin/brams_map_gw5a.v index 547b0d1d1..8bc77bf4f 100644 --- a/techlibs/gowin/brams_map_gw5a.v +++ b/techlibs/gowin/brams_map_gw5a.v @@ -205,7 +205,7 @@ output [PORT_A_WIDTH-1:0] PORT_B_RD_DATA; wire RSTA = OPTION_RESET_MODE == "SYNC" ? PORT_A_RD_SRST : PORT_A_RD_ARST; wire RSTB = OPTION_RESET_MODE == "SYNC" ? PORT_B_RD_SRST : PORT_B_RD_ARST; -wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_B_WR_BE); +wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_A_WR_BE); wire [13:0] ADB = `addrbe(PORT_B_WIDTH, PORT_B_ADDR, PORT_B_WR_BE); generate diff --git a/techlibs/gowin/dsp_map.v b/techlibs/gowin/dsp_map.v new file mode 100644 index 000000000..f03bcdff0 --- /dev/null +++ b/techlibs/gowin/dsp_map.v @@ -0,0 +1,70 @@ +module \$__MUL9X9 (input [8:0] A, input [8:0] B, output [17:0] Y); + + parameter A_WIDTH = 9; + parameter B_WIDTH = 9; + parameter Y_WIDTH = 18; + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + + MULT9X9 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .CE(1'b0), + .RESET(1'b0), + .A(A), + .SIA({A_WIDTH{1'b0}}), + .ASEL(1'b0), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .SIB({B_WIDTH{1'b0}}), + .BSEL(1'b0), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); + +endmodule + +module \$__MUL18X18 (input [17:0] A, input [17:0] B, output [35:0] Y); + + parameter A_WIDTH = 18; + parameter B_WIDTH = 18; + parameter Y_WIDTH = 36; + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + + MULT18X18 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .CE(1'b0), + .RESET(1'b0), + .A(A), + .SIA({A_WIDTH{1'b0}}), + .ASEL(1'b0), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .SIB({B_WIDTH{1'b0}}), + .BSEL(1'b0), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); + +endmodule + +module \$__MUL36X36 (input [35:0] A, input [35:0] B, output [71:0] Y); + + parameter A_WIDTH = 36; + parameter B_WIDTH = 36; + parameter Y_WIDTH = 72; + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + + MULT36X36 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .RESET(1'b0), + .CE(1'b0), + .A(A), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); + +endmodule diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc index 36d827b7c..9fd4dca86 100644 --- a/techlibs/gowin/synth_gowin.cc +++ b/techlibs/gowin/synth_gowin.cc @@ -29,6 +29,21 @@ struct SynthGowinPass : public ScriptPass { SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { } + struct DSPRule { + int a_maxwidth; + int b_maxwidth; + int a_minwidth; + int b_minwidth; + std::string prim; + }; + + const std::vector dsp_rules = { + {36, 36, 22, 22, "$__MUL36X36"}, + {18, 18, 10, 4, "$__MUL18X18"}, + {18, 18, 4, 10, "$__MUL18X18"}, + {9, 9, 4, 4, "$__MUL9X9"}, + }; + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| @@ -97,13 +112,16 @@ struct SynthGowinPass : public ScriptPass log(" -setundef\n"); log(" set undriven wires and parameters to zero\n"); log("\n"); + log(" -nodsp\n"); + log(" do not infer DSP multipliers\n"); + log("\n"); log("The following commands are executed by this synthesis command:\n"); help_script(); log("\n"); } string top_opt, vout_file, json_file, family; - bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef; + bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef, nodsp; void clear_flags() override { @@ -123,6 +141,7 @@ struct SynthGowinPass : public ScriptPass noalu = false; no_rw_check = false; setundef = false; + nodsp = false; } void execute(std::vector args, RTLIL::Design *design) override @@ -209,6 +228,10 @@ struct SynthGowinPass : public ScriptPass setundef = true; continue; } + if (args[argidx] == "-nodsp") { + nodsp = true; + continue; + } break; } extra_args(args, argidx, design); @@ -239,17 +262,40 @@ struct SynthGowinPass : public ScriptPass run(stringf("hierarchy -check %s", help_mode ? "-top " : top_opt)); } - if (flatten && check_label("flatten", "(unless -noflatten)")) - { - run("proc"); - run("flatten"); - run("tribuf -logic"); - run("deminout"); - } - if (check_label("coarse")) { - run("synth -run coarse" + no_rw_check_opt); + run("proc"); + if (flatten || help_mode) + run("flatten", "(unless -noflatten)"); + run("tribuf -logic"); + run("deminout"); + run("opt_expr"); + run("opt_clean"); + run("check"); + run("opt -nodffe -nosdff"); + run("fsm"); + run("opt"); + run("wreduce"); + run("peepopt"); + run("opt_clean"); + run("share"); + + if (help_mode) { + run("techmap -map +/mul2dsp.v [...]", "(unless -nodsp and if -family gw1n or gw2a)"); + run("techmap -map +/gowin/dsp_map.v", "(unless -nodsp and if -family gw1n or gw2a)"); + } else if (!nodsp && (family == "gw1n" || family == "gw2a")) { + for (const auto &rule : dsp_rules) { + run(stringf("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=%d -D DSP_B_MAXWIDTH=%d -D DSP_A_MINWIDTH=%d -D DSP_B_MINWIDTH=%d -D DSP_NAME=%s", + rule.a_maxwidth, rule.b_maxwidth, rule.a_minwidth, rule.b_minwidth, rule.prim)); + run("chtype -set $mul t:$__soft_mul"); + } + run("techmap -map +/gowin/dsp_map.v"); + } + + run("alumacc"); + run("opt"); + run("memory -nomap" + no_rw_check_opt); + run("opt_clean"); } if (check_label("map_ram")) @@ -263,7 +309,7 @@ struct SynthGowinPass : public ScriptPass if (nolutram) args += " -no-auto-distributed"; } - run(stringf("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt -D %s", family) + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); + run(stringf("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt%s", family == "gw5a" ? " -D gw5a" : "") + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run(stringf("techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map%s.v", family == "gw5a" ? "_gw5a" : "")); } diff --git a/techlibs/xilinx/xilinx_dsp.cc b/techlibs/xilinx/xilinx_dsp.cc index 22e6bce5b..194b9ac10 100644 --- a/techlibs/xilinx/xilinx_dsp.cc +++ b/techlibs/xilinx/xilinx_dsp.cc @@ -263,6 +263,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm) log("Analysing %s.%s for Xilinx DSP packing.\n", log_id(pm.module), log_id(st.dsp)); log_debug("preAdd: %s\n", log_id(st.preAdd, "--")); + log_debug("preSub: %s\n", log_id(st.preSub, "--")); log_debug("ffAD: %s\n", log_id(st.ffAD, "--")); log_debug("ffA2: %s\n", log_id(st.ffA2, "--")); log_debug("ffA1: %s\n", log_id(st.ffA1, "--")); @@ -278,17 +279,22 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm) Cell *cell = st.dsp; - if (st.preAdd) { - log(" preadder %s (%s)\n", log_id(st.preAdd), log_id(st.preAdd->type)); - bool A_SIGNED = st.preAdd->getParam(ID::A_SIGNED).as_bool(); - bool D_SIGNED = st.preAdd->getParam(ID::B_SIGNED).as_bool(); - if (st.sigA == st.preAdd->getPort(ID::B)) + if (st.preAdd || st.preSub) { + Cell* preAdder = st.preAdd ? st.preAdd : st.preSub; + + log(" preadder %s (%s)\n", log_id(preAdder), log_id(preAdder->type)); + bool A_SIGNED = preAdder->getParam(ID::A_SIGNED).as_bool(); + bool D_SIGNED = preAdder->getParam(ID::B_SIGNED).as_bool(); + if (st.sigA == preAdder->getPort(ID::B)) std::swap(A_SIGNED, D_SIGNED); st.sigA.extend_u0(30, A_SIGNED); st.sigD.extend_u0(25, D_SIGNED); cell->setPort(ID::A, st.sigA); cell->setPort(ID::D, st.sigD); - cell->setPort(ID(INMODE), Const::from_string("00100")); + if (preAdder->type == ID($add)) + cell->setPort(ID(INMODE), Const::from_string("00100")); + else + cell->setPort(ID(INMODE), Const::from_string("01100")); if (st.ffAD) { if (st.ffAD->type.in(ID($dffe), ID($sdffe))) { @@ -303,7 +309,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm) cell->setParam(ID(USE_DPORT), Const("TRUE")); - pm.autoremove(st.preAdd); + pm.autoremove(preAdder); } if (st.postAdd) { log(" postadder %s (%s)\n", log_id(st.postAdd), log_id(st.postAdd->type)); diff --git a/techlibs/xilinx/xilinx_dsp.pmg b/techlibs/xilinx/xilinx_dsp.pmg index ef0157621..6ec891290 100644 --- a/techlibs/xilinx/xilinx_dsp.pmg +++ b/techlibs/xilinx/xilinx_dsp.pmg @@ -6,6 +6,8 @@ // If ADREG matched, treat 'A' input as input of ADREG // ( 3) Match the driver of the 'A' and 'D' inputs for a possible $add cell // (pre-adder) +// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell +// (pre-adder) // ( 4) If pre-adder was present, find match 'A' input for A2REG // If pre-adder was not present, move ADREG to A2REG // If A2REG, then match 'A' input for A1REG @@ -152,13 +154,41 @@ code sigA sigD } endcode +// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell +// (pre-adder) +match preSub + if sigD.empty() || sigD.is_fully_zero() + // Ensure that preAdder not already used + if param(dsp, \USE_DPORT).decode_string() == "FALSE" + if port(dsp, \INMODE, Const(0, 5)).is_fully_zero() + + select preSub->type.in($sub) + // Output has to be 25 bits or less + select GetSize(port(preSub, \Y)) <= 25 + select nusers(port(preSub, \Y)) == 2 + // D port has to be 25 bits or less + select GetSize(port(preSub, \A)) <= 25 + // A port has to be 30 bits or less + select GetSize(port(preSub, \B)) <= 30 + index port(preSub, \Y) === sigA + + optional +endmatch + +code sigA sigD + if (preSub) { + sigD = port(preSub, \A); + sigA = port(preSub, \B); + } +endcode + // (4) If pre-adder was present, find match 'A' input for A2REG // If pre-adder was not present, move ADREG to A2REG // Then match 'A' input for A1REG code argQ ffAD sigA clock ffA2 ffA1 // Only search for ffA2 if there was a pre-adder // (otherwise ffA2 would have been matched as ffAD) - if (preAdd) { + if (preAdd || preSub) { if (param(dsp, \AREG).as_int() == 0) { argQ = sigA; subpattern(in_dffe); diff --git a/tests/arch/gowin/bug5688.ys b/tests/arch/gowin/bug5688.ys new file mode 100644 index 000000000..39019c4d6 --- /dev/null +++ b/tests/arch/gowin/bug5688.ys @@ -0,0 +1,31 @@ +read_verilog << EOT +`default_nettype none + +module top ( + input wire clk, + input wire [9:0] rd_addr, + output reg [15:0] rd_data, + input wire [9:0] wr_addr, + input wire [15:0] wr_data, + input wire wr_en +); + + (* ram_style = "block" *) reg [15:0] mem [0:1023]; + + // Read port — separate always block + always @(posedge clk) begin + rd_data <= mem[rd_addr]; + end + + // Write port — separate always block + always @(posedge clk) begin + if (wr_en) + mem[wr_addr] <= wr_data; + end + +endmodule + +EOT +synth_gowin -top top +splitnets +select -assert-any top/mem.0.0 %ci*:+DPX9B[ADA]:+DFF:+IBUF i:wr_en %i diff --git a/tests/arch/gowin/mul_gw1n.ys b/tests/arch/gowin/mul_gw1n.ys new file mode 100644 index 000000000..9b1748255 --- /dev/null +++ b/tests/arch/gowin/mul_gw1n.ys @@ -0,0 +1,53 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +# equivalence checking is somewhat slow (and missing simulation models) +synth_gowin -family gw1n +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT9X9 + + +# Make sure that DSPs are not inferred with -nodsp option +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +synth_gowin -family gw1n -nodsp +cd top # Constrain all select calls below inside the top module +select -assert-none t:MULT9X9 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32 +hierarchy -top top +proc +synth_gowin -family gw1n +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X18 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT36X36 + + +# We end up with two 18x18 multipliers +# 36x36 min width is 22 +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin +cd top # Constrain all select calls below inside the top module +select -assert-count 2 t:MULT18X18 diff --git a/tests/arch/gowin/mul_gw2a.ys b/tests/arch/gowin/mul_gw2a.ys new file mode 100644 index 000000000..895c580b7 --- /dev/null +++ b/tests/arch/gowin/mul_gw2a.ys @@ -0,0 +1,53 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +# equivalence checking is somewhat slow (and missing simulation models) +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT9X9 + + +# Make sure that DSPs are not inferred with -nodsp option +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +synth_gowin -family gw2a -nodsp +cd top # Constrain all select calls below inside the top module +select -assert-none t:MULT9X9 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32 +hierarchy -top top +proc +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X18 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT36X36 + + +# We end up with two 18x18 multipliers +# 36x36 min width is 22 +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 2 t:MULT18X18 diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index e3b746202..b01d34bba 100644 --- a/tests/arch/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module select -assert-count 4 t:SB_DFF select -assert-count 2 t:SB_DFFESR -select -assert-max 15 t:SB_LUT4 +select -assert-max 16 t:SB_LUT4 select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/ice40_dsp_const.ys b/tests/arch/ice40/ice40_dsp_const.ys index c9c76a1ac..735f945a1 100644 --- a/tests/arch/ice40/ice40_dsp_const.ys +++ b/tests/arch/ice40/ice40_dsp_const.ys @@ -74,6 +74,7 @@ EOT techmap -wb -D EQUIV -autoproc -map +/ice40/cells_sim.v +async2sync equiv_make top ref equiv select -assert-any -module equiv t:$equiv equiv_induct diff --git a/tests/arch/xilinx/dsp_preadder_sub.ys b/tests/arch/xilinx/dsp_preadder_sub.ys new file mode 100644 index 000000000..0e23ac373 --- /dev/null +++ b/tests/arch/xilinx/dsp_preadder_sub.ys @@ -0,0 +1,29 @@ +read_verilog < o) = 1; +endspecify +endmodule + +module top(input i, output o); + wire a, b, c, z; + $_AND_ a0(.A(b), .B(i), .Y(a)); + $_AND_ b0(.A(a), .B(c), .Y(b)); + $_AND_ c0(.A(b), .B(i), .Y(c)); + box1 u_box(.i(i), .o(z)); + assign o = c ^ z; +endmodule +EOT + +abc9 -lut 4 diff --git a/tests/techmap/abc_temp_dir_sanitization.ys b/tests/techmap/abc_temp_dir_sanitization.ys new file mode 100644 index 000000000..ed87ff980 --- /dev/null +++ b/tests/techmap/abc_temp_dir_sanitization.ys @@ -0,0 +1,13 @@ +read_verilog < + +#include "kernel/modtools.h" +#include "kernel/rtlil.h" + +YOSYS_NAMESPACE_BEGIN + +TEST(ModIndexSwapTest, has) +{ + Design* d = new Design; + Module* m = d->addModule("$m"); + Wire* o = m->addWire("$o", 2); + o->port_input = true; + Wire* i = m->addWire("$i", 2); + i->port_input = true; + m->fixup_ports(); + m->addNot("$not", i, o); + auto mi = ModIndex(m); + mi.reload_module(); + for (auto [sb, info] : mi.database) { + EXPECT_TRUE(mi.database.find(sb) != mi.database.end()); + } + m->swap_names(i, o); + for (auto [sb, info] : mi.database) { + EXPECT_TRUE(mi.database.find(sb) != mi.database.end()); + } +} + +TEST(ModIndexDeleteTest, has) +{ + if (log_files.empty()) log_files.emplace_back(stdout); + Design* d = new Design; + Module* m = d->addModule("$m"); + Wire* w = m->addWire("$w"); + Wire* o = m->addWire("$o"); + o->port_output = true; + m->fixup_ports(); + Cell* not_ = m->addNotGate("$not", w, o); + auto mi = ModIndex(m); + mi.reload_module(); + mi.dump_db(); + Wire* a = m->addWire("\\a"); + not_->setPort(ID::A, a); + EXPECT_TRUE(mi.ok()); +} + +YOSYS_NAMESPACE_END diff --git a/tests/various/.gitignore b/tests/various/.gitignore index e116179ae..9296a04c0 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -4,6 +4,8 @@ /plugin.so /plugin_search /plugin.so.dSYM +/ezcmdline_plugin.so +/ezcmdline_plugin.so.dSYM /temp /smtlib2_module.smt2 /smtlib2_module-filtered.smt2 diff --git a/tests/various/const_shift_empty_arg.ys b/tests/various/const_shift_empty_arg.ys new file mode 100644 index 000000000..4073e198d --- /dev/null +++ b/tests/various/const_shift_empty_arg.ys @@ -0,0 +1,49 @@ +# Regression test for #5684: const_shift_worker must not crash when arg1 is +# empty. + +read_json << EOF +{ + "modules": { + "sshl": { + "cells": { + "sshlCell": { + "connections": { + "A": [], + "B": [3], + "Y": [1] + }, + "parameters": { + "A_SIGNED": "1", + "A_WIDTH": "0", + "B_SIGNED": "0", + "B_WIDTH": "1", + "Y_WIDTH": "1" + }, + "port_directions": { + "A": "input", + "B": "input", + "Y": "output" + }, + "type": "$sshl" + } + }, + "ports": { + "A": { + "bits": [], + "direction": "input" + }, + "B": { + "bits": [3], + "direction": "input" + }, + "Y": { + "bits": [1], + "direction": "output" + } + } + } + } +} +EOF + +eval -set B 0 -show Y sshl diff --git a/tests/various/ezcmdline_dummy_solver b/tests/various/ezcmdline_dummy_solver new file mode 100755 index 000000000..db5b21b8e --- /dev/null +++ b/tests/various/ezcmdline_dummy_solver @@ -0,0 +1,61 @@ +#!/bin/sh +# Dummy SAT solver for ezCmdlineSAT tests. +# Accepts exactly two CNF shapes: +# - SAT: p cnf 1 1; clause: "1 0" -> exits 10 with v 1 +# - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20 +set -e + +if [ "$#" -ne 1 ]; then + echo "usage: $0 " >&2 + exit 1 +fi + +awk ' +BEGIN { + vars = 0; + clauses = 0; + clause_count = 0; + clause_data = ""; + current = ""; +} +$1 == "c" { + next; +} +$1 == "p" && $2 == "cnf" { + vars = $3; + clauses = $4; + next; +} +{ + for (i = 1; i <= NF; i++) { + lit = $i; + if (lit == 0) { + clause_count++; + if (clause_data != "") + clause_data = clause_data ";" current; + else + clause_data = current; + current = ""; + } else { + if (current == "") + current = lit; + else + current = current "," lit; + } + } +} +END { + if (vars == 1 && clause_count == 1 && clause_data == "1") { + print "s SATISFIABLE"; + print "v 1 0"; + exit 10; + } + if (vars == 1 && clause_count == 2 && clause_data == "1;-1") { + print "s UNSATISFIABLE"; + exit 20; + } + print "c unexpected CNF for dummy solver"; + print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data; + exit 1; +} +' "$1" diff --git a/tests/various/ezcmdline_plugin.cc b/tests/various/ezcmdline_plugin.cc new file mode 100644 index 000000000..b775829b3 --- /dev/null +++ b/tests/various/ezcmdline_plugin.cc @@ -0,0 +1,53 @@ +#include "kernel/yosys.h" +#include "libs/ezsat/ezcmdline.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct EzCmdlineTestPass : public Pass { + EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { } + void execute(std::vector args, RTLIL::Design *design) override + { + std::string cmd; + size_t argidx = 1; + + while (argidx < args.size()) { + if (args[argidx] == "-cmd" && argidx + 1 < args.size()) { + cmd = args[argidx + 1]; + argidx += 2; + continue; + } + break; + } + + extra_args(args, argidx, design); + + if (cmd.empty()) + log_error("Missing -cmd argument.\n"); + + ezCmdlineSAT sat(cmd); + sat.non_incremental(); + + // assume("A") adds a permanent CNF clause "A". + sat.assume(sat.VAR("A")); + + std::vector model_expressions; + std::vector model_values; + model_expressions.push_back(sat.VAR("A")); + + // Expect SAT with A=true. + if (!sat.solve(model_expressions, model_values)) + log_error("ezCmdlineSAT SAT case failed.\n"); + if (model_values.size() != 1 || !model_values[0]) + log_error("ezCmdlineSAT SAT model mismatch.\n"); + + // Passing NOT("A") here adds a temporary unit clause for this solve call, + // so the solver sees A && !A and must return UNSAT. + if (sat.solve(model_expressions, model_values, sat.NOT("A"))) + log_error("ezCmdlineSAT UNSAT case failed.\n"); + + log("ezcmdline_test passed!\n"); + } +} EzCmdlineTestPass; + +PRIVATE_NAMESPACE_END diff --git a/tests/various/ezcmdline_plugin.sh b/tests/various/ezcmdline_plugin.sh new file mode 100644 index 000000000..cad0475a8 --- /dev/null +++ b/tests/various/ezcmdline_plugin.sh @@ -0,0 +1,12 @@ +set -e + +DIR=$(cd "$(dirname "$0")" && pwd) +BASEDIR=$(cd "$DIR/../.." && pwd) +rm -f "$DIR/ezcmdline_plugin.so" +chmod +x "$DIR/ezcmdline_dummy_solver" +CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags) +DATDIR=$("$BASEDIR/yosys-config" --datdir) +DATDIR=${DATDIR//\//\\\/} +CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share} +"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc" +"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!" diff --git a/tests/various/json_param_defaults.v b/tests/various/json_param_defaults.v new file mode 100644 index 000000000..7d3b94a68 --- /dev/null +++ b/tests/various/json_param_defaults.v @@ -0,0 +1,10 @@ +module json_param_defaults #( + parameter WIDTH = 8, + parameter SIGNED = 1 +) ( + input [WIDTH-1:0] a, + output [WIDTH-1:0] y +); + wire [WIDTH-1:0] y_int = a << SIGNED; + assign y = y_int; +endmodule diff --git a/tests/various/json_param_defaults.ys b/tests/various/json_param_defaults.ys new file mode 100644 index 000000000..45e312de2 --- /dev/null +++ b/tests/various/json_param_defaults.ys @@ -0,0 +1,8 @@ +! mkdir -p temp +read_verilog -sv json_param_defaults.v +write_json temp/json_param_defaults.json +design -reset +read_json temp/json_param_defaults.json +write_verilog -noattr -defaultparams temp/json_param_defaults.v +! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v +! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v diff --git a/tests/various/specify.ys b/tests/various/specify.ys index d7260d524..86471de5e 100644 --- a/tests/various/specify.ys +++ b/tests/various/specify.ys @@ -43,7 +43,7 @@ select n:C_* -assert-count 2 equiv_make gold gate equiv hierarchy -top equiv equiv_struct -equiv_induct -seq 5 +equiv_induct -ignore-unknown-cells -seq 5 equiv_status -assert design -reset @@ -57,7 +57,7 @@ select n:B_* -assert-count 2 equiv_make gold gate equiv hierarchy -top equiv equiv_struct -equiv_induct -seq 5 +equiv_induct -ignore-unknown-cells -seq 5 equiv_status -assert design -reset diff --git a/tests/verilog/automatic_lifetime.ys b/tests/verilog/automatic_lifetime.ys new file mode 100644 index 000000000..84e21e088 --- /dev/null +++ b/tests/verilog/automatic_lifetime.ys @@ -0,0 +1,104 @@ +# Automatic reg as intermediate value in always @(*) +# The result must be provably equivalent to the direct expression. +# No latch or DFF must be created for tmp. +design -reset +read_verilog -sv <> 4) & 1'b1)); +endmodule +EOF +proc +async2sync +select -assert-none t:$dff t:$dlatch %% +sat -verify -prove-asserts -show-all + +# automatic in a clocked block — only the explicitly registered +# output (result) must get a DFF; the automatic temp must not. +design -reset +read_verilog -sv <