diff --git a/.gitcommit b/.gitcommit index 46b7856fbc8..6828f88dcb0 100644 --- a/.gitcommit +++ b/.gitcommit @@ -1 +1 @@ -$Format:%h$ +$Format:%H$ diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml index 27cfd09b7de..e4c776ed914 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.yml +++ b/.github/ISSUE_TEMPLATE/bug_report.yml @@ -34,6 +34,7 @@ body: - macOS - Windows - BSD + - WebAssembly multiple: true validations: required: true @@ -42,7 +43,7 @@ body: attributes: value: > When providing steps to reproduce the issue, please ensure that the issue - is reproducible in the current git master of Yosys. Also ensure to + is reproducible in the current git main of Yosys. Also ensure to provide all necessary source files needed. diff --git a/.github/ISSUE_TEMPLATE/docs_report.yml b/.github/ISSUE_TEMPLATE/docs_report.yml new file mode 100644 index 00000000000..aa65c63b9c9 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/docs_report.yml @@ -0,0 +1,55 @@ +name: Documentation Report +description: Report a problem with the Yosys documentation +labels: ["pending-verification"] +body: + - type: markdown + attributes: + value: > + + If you have a general question, please ask it in the [Discussions](https://github.com/YosysHQ/yosys/discussions) area + or join our [IRC Channel](https://web.libera.chat/#yosys) or [Community Slack](https://join.slack.com/t/yosyshq/shared_invite/zt-1aopkns2q-EiQ97BeQDt_pwvE41sGSuA). + + + If you have found a bug in Yosys, or in building the documentation, + please fill out the Bug Report issue form, this form is for problems + with the live documentation on [Read the + Docs](https://yosyshq.readthedocs.io/projects/yosys/). Please only + report problems that appear on the latest version of the documentation. + + + Please contact [YosysHQ GmbH](https://www.yosyshq.com/) if you need + commercial support for Yosys. + + - type: input + id: docs_url + attributes: + label: Link to page + description: "Please provide a link to the page where the problem was found." + placeholder: "e.g. https://yosyshq.readthedocs.io/projects/yosys/" + validations: + required: true + + - type: input + id: build_number + attributes: + label: Build number + description: "If possible, please provide the latest build number from https://readthedocs.org/projects/yosys/builds/." + placeholder: "e.g. Build #24078236" + validations: + required: false + + - type: textarea + id: problem + attributes: + label: Issue + description: "Please describe what is incorrect, invalid, or missing." + validations: + required: true + + - type: textarea + id: expected + attributes: + label: Expected + description: "If applicable, please describe what should appear instead." + validations: + required: false diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 00000000000..82daf609d36 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -0,0 +1,5 @@ +_What are the reasons/motivation for this change?_ + +_Explain how this is achieved._ + +_If applicable, please suggest to reviewers how they can test the change._ diff --git a/.github/actions/setup-build-env/action.yml b/.github/actions/setup-build-env/action.yml new file mode 100644 index 00000000000..c5a0d14abdf --- /dev/null +++ b/.github/actions/setup-build-env/action.yml @@ -0,0 +1,34 @@ +name: Build environment setup +description: Configure build env for Yosys builds +runs: + using: composite + steps: + - name: Install Linux Dependencies + if: runner.os == 'Linux' + shell: bash + run: | + sudo apt-get update + sudo apt-get install gperf build-essential bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev + + - name: Install macOS Dependencies + if: runner.os == 'macOS' + shell: bash + run: | + HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1 brew install bison flex gawk libffi pkg-config bash autoconf llvm + + - name: Linux runtime environment + if: runner.os == 'Linux' + shell: bash + run: | + echo "${{ github.workspace }}/.local/bin" >> $GITHUB_PATH + echo "procs=$(nproc)" >> $GITHUB_ENV + + - name: macOS runtime environment + if: runner.os == 'macOS' + shell: bash + run: | + echo "${{ github.workspace }}/.local/bin" >> $GITHUB_PATH + echo "$(brew --prefix llvm)/bin" >> $GITHUB_PATH + echo "$(brew --prefix bison)/bin" >> $GITHUB_PATH + echo "$(brew --prefix flex)/bin" >> $GITHUB_PATH + echo "procs=$(sysctl -n hw.ncpu)" >> $GITHUB_ENV diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 4a77d223429..24ae7c89883 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -15,7 +15,8 @@ jobs: - name: Checkout repository uses: actions/checkout@v4 - + with: + submodules: true - name: Initialize CodeQL uses: github/codeql-action/init@v3 with: diff --git a/.github/workflows/emcc.yml b/.github/workflows/emcc.yml deleted file mode 100644 index 7c6409c1be2..00000000000 --- a/.github/workflows/emcc.yml +++ /dev/null @@ -1,18 +0,0 @@ -name: Emscripten Build - -on: [push, pull_request] - -jobs: - emcc: - runs-on: ubuntu-latest - steps: - - uses: mymindstorm/setup-emsdk@v14 - - uses: actions/checkout@v4 - - name: Build - run: | - make config-emcc - make YOSYS_VER=latest - - uses: actions/upload-artifact@v4 - with: - name: yosysjs - path: yosysjs-latest.zip diff --git a/.github/workflows/extra-builds.yml b/.github/workflows/extra-builds.yml new file mode 100644 index 00000000000..1a00d016347 --- /dev/null +++ b/.github/workflows/extra-builds.yml @@ -0,0 +1,101 @@ +name: Test extra build flows + +on: [push, pull_request] + +jobs: + pre_job: + runs-on: ubuntu-latest + outputs: + should_skip: ${{ steps.skip_check.outputs.should_skip }} + steps: + - id: skip_check + uses: fkirc/skip-duplicate-actions@v5 + with: + paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' + # cancel previous builds if a new commit is pushed + cancel_others: 'true' + # only run on push *or* pull_request, not both + concurrent_skipping: 'same_content_newer' + + vs-prep: + name: Prepare Visual Studio build + runs-on: ubuntu-latest + needs: [pre_job] + if: needs.pre_job.outputs.should_skip != 'true' + steps: + - uses: actions/checkout@v4 + with: + submodules: true + - name: Build + run: make vcxsrc YOSYS_VER=latest + - uses: actions/upload-artifact@v4 + with: + name: vcxsrc + path: yosys-win32-vcxsrc-latest.zip + + vs-build: + name: Visual Studio build + runs-on: windows-2019 + needs: [vs-prep, pre_job] + if: needs.pre_job.outputs.should_skip != 'true' + steps: + - uses: actions/download-artifact@v4 + with: + name: vcxsrc + path: . + - name: unzip + run: unzip yosys-win32-vcxsrc-latest.zip + - name: setup-msbuild + uses: microsoft/setup-msbuild@v2 + - name: MSBuild + working-directory: yosys-win32-vcxsrc-latest + run: msbuild YosysVS.sln /p:PlatformToolset=v142 /p:Configuration=Release /p:WindowsTargetPlatformVersion=10.0.17763.0 + + wasi-build: + name: WASI build + needs: pre_job + if: needs.pre_job.outputs.should_skip != 'true' + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + submodules: true + - name: Build + run: | + WASI_SDK=wasi-sdk-19.0 + WASI_SDK_URL=https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-19/wasi-sdk-19.0-linux.tar.gz + if ! [ -d ${WASI_SDK} ]; then curl -L ${WASI_SDK_URL} | tar xzf -; fi + + mkdir -p build + cat > build/Makefile.conf <> $GITHUB_ENV + + - name: Cache iverilog + id: cache-iverilog + uses: actions/cache@v4 + with: + path: .local/ + key: ${{ matrix.os }}-${{ env.IVERILOG_GIT }} + + - name: Build iverilog + if: steps.cache-iverilog.outputs.cache-hit != 'true' + shell: bash + run: | + mkdir -p ${{ github.workspace }}/.local/ + cd iverilog + autoconf + CC=gcc CXX=g++ ./configure --prefix=${{ github.workspace }}/.local + make -j$procs + make install + + - name: Download build artifact + uses: actions/download-artifact@v4 + with: + name: build-${{ matrix.os }} + + - name: Uncompress build + shell: bash + run: + tar -xvf build.tar + + - name: Log yosys-config output + run: | + ./yosys-config || true + + - name: Run tests + shell: bash + run: | + make -j$procs test TARGETS= EXTRA_TARGETS= CONFIG=$CC + + - name: Report errors + if: ${{ failure() }} + shell: bash + run: | + find tests/**/*.err -print -exec cat {} \; + + test-docs: + name: Run docs tests + runs-on: ${{ matrix.os }} + needs: [build-yosys, pre_docs_job] + if: needs.pre_docs_job.outputs.should_skip != 'true' + env: + CC: clang + strategy: + matrix: + os: [ubuntu-latest] + fail-fast: false + steps: + - name: Checkout Yosys + uses: actions/checkout@v4 + + - name: Setup environment + uses: ./.github/actions/setup-build-env + + - name: Download build artifact + uses: actions/download-artifact@v4 + with: + name: build-${{ matrix.os }} + + - name: Uncompress build + shell: bash + run: + tar -xvf build.tar + + - name: Log yosys-config output + run: | + ./yosys-config || true + + - name: Run tests + shell: bash + run: | + make -C docs test -j${{ env.procs }} diff --git a/.github/workflows/test-compile.yml b/.github/workflows/test-compile.yml new file mode 100644 index 00000000000..089e65ca757 --- /dev/null +++ b/.github/workflows/test-compile.yml @@ -0,0 +1,79 @@ +name: Compiler testing + +on: [push, pull_request] + +jobs: + pre_job: + runs-on: ubuntu-latest + outputs: + should_skip: ${{ steps.skip_check.outputs.should_skip }} + steps: + - id: skip_check + uses: fkirc/skip-duplicate-actions@v5 + with: + paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' + # cancel previous builds if a new commit is pushed + cancel_others: 'true' + # only run on push *or* pull_request, not both + concurrent_skipping: 'same_content_newer' + + test-compile: + runs-on: ${{ matrix.os }} + needs: pre_job + if: needs.pre_job.outputs.should_skip != 'true' + env: + CXXFLAGS: ${{ startsWith(matrix.compiler, 'gcc') && '-Wp,-D_GLIBCXX_ASSERTIONS' || ''}} + CC_SHORT: ${{ startsWith(matrix.compiler, 'gcc') && 'gcc' || 'clang' }} + strategy: + matrix: + os: + - ubuntu-latest + compiler: + # oldest supported + - 'clang-14' + - 'gcc-10' + # newest + - 'clang' + - 'gcc' + include: + # macOS + - os: macos-13 + compiler: 'clang' + # oldest clang not available on ubuntu-latest + - os: ubuntu-20.04 + compiler: 'clang-10' + fail-fast: false + steps: + - name: Checkout Yosys + uses: actions/checkout@v4 + with: + submodules: true + + - name: Setup environment + uses: ./.github/actions/setup-build-env + + - name: Setup Cpp + uses: aminya/setup-cpp@v1 + with: + compiler: ${{ matrix.compiler }} + + - name: Tool versions + shell: bash + run: | + $CC --version + $CXX --version + + # minimum standard + - name: Build C++17 + shell: bash + run: | + make config-$CC_SHORT + make -j$procs CXXSTD=c++17 compile-only + + # maximum standard, only on newest compilers + - name: Build C++20 + if: ${{ matrix.compiler == 'clang' || matrix.compiler == 'gcc'}} + shell: bash + run: | + make config-$CC_SHORT + make -j$procs CXXSTD=c++20 compile-only diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml deleted file mode 100644 index b3a6bd8468e..00000000000 --- a/.github/workflows/test-linux.yml +++ /dev/null @@ -1,123 +0,0 @@ -name: Build and run tests (Linux) - -on: [push, pull_request] - -jobs: - test-linux: - runs-on: ${{ matrix.os.id }} - strategy: - matrix: - os: - - { id: ubuntu-20.04, name: focal } - compiler: - - 'clang-12' - - 'gcc-11' - cpp_std: - - 'c++11' - - 'c++14' - - 'c++17' - - 'c++20' - include: - # Limit the older compilers to C++11 mode - - os: { id: ubuntu-20.04, name: focal } - compiler: 'clang-11' - cpp_std: 'c++11' - - os: { id: ubuntu-20.04, name: focal } - compiler: 'gcc-10' - cpp_std: 'c++11' - fail-fast: false - steps: - - name: Install Dependencies - shell: bash - run: | - sudo apt-get update - sudo apt-get install gperf build-essential bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev - - - name: Setup GCC - if: startsWith(matrix.compiler, 'gcc') - shell: bash - run: | - CXX=${CC/#gcc/g++} - sudo apt-add-repository ppa:ubuntu-toolchain-r/test - sudo apt-get update - sudo apt-get install $CC $CXX - echo "CC=$CC" >> $GITHUB_ENV - echo "CXX=$CXX" >> $GITHUB_ENV - echo "CXXFLAGS=-Wp,-D_GLIBCXX_ASSERTIONS" >> $GITHUB_ENV - env: - CC: ${{ matrix.compiler }} - - - name: Setup Clang - if: startsWith(matrix.compiler, 'clang') - shell: bash - run: | - wget https://apt.llvm.org/llvm-snapshot.gpg.key - sudo apt-key add llvm-snapshot.gpg.key - rm llvm-snapshot.gpg.key - sudo apt-add-repository "deb https://apt.llvm.org/${{ matrix.os.name }}/ llvm-toolchain-${{ matrix.os.name }} main" - sudo apt-get update - CXX=${CC/#clang/clang++} - sudo apt-get install $CC $CXX - echo "CC=$CC" >> $GITHUB_ENV - echo "CXX=$CXX" >> $GITHUB_ENV - env: - CC: ${{ matrix.compiler }} - - - name: Runtime environment - shell: bash - env: - WORKSPACE: ${{ github.workspace }} - run: | - echo "GITHUB_WORKSPACE=`pwd`" >> $GITHUB_ENV - echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH - echo "procs=$(nproc)" >> $GITHUB_ENV - - - name: Tool versions - shell: bash - run: | - $CC --version - $CXX --version - - - name: Checkout Yosys - uses: actions/checkout@v4 - - - name: Get iverilog - shell: bash - run: | - git clone https://github.com/steveicarus/iverilog.git - cd iverilog - echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV - - - name: Cache iverilog - id: cache-iverilog - uses: actions/cache@v4 - with: - path: .local/ - key: ${{ matrix.os.id }}-${{ env.IVERILOG_GIT }} - - - name: Build iverilog - if: steps.cache-iverilog.outputs.cache-hit != 'true' - shell: bash - run: | - mkdir -p $GITHUB_WORKSPACE/.local/ - cd iverilog - autoconf - CC=gcc CXX=g++ ./configure --prefix=$GITHUB_WORKSPACE/.local - make -j${{ env.procs }} - make install - - - name: Build yosys - shell: bash - run: | - make config-${CC%%-*} - make -j${{ env.procs }} CXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC - - - name: Run tests - if: (matrix.cpp_std == 'c++11') && (matrix.compiler == 'gcc-11') - shell: bash - run: | - make -j${{ env.procs }} test CXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC - - - name: Log yosys-config output - run: | - ./yosys-config || true diff --git a/.github/workflows/test-macos.yml b/.github/workflows/test-macos.yml deleted file mode 100644 index 9b806a58083..00000000000 --- a/.github/workflows/test-macos.yml +++ /dev/null @@ -1,75 +0,0 @@ -name: Build and run tests (macOS) - -on: [push, pull_request] - -jobs: - test-macos: - runs-on: ${{ matrix.os.id }} - strategy: - matrix: - os: - - { id: macos-13, name: 'Ventura' } - cpp_std: - - 'c++11' - - 'c++17' - fail-fast: false - steps: - - name: Install Dependencies - run: | - brew install bison flex gawk libffi pkg-config bash - - - name: Runtime environment - shell: bash - env: - WORKSPACE: ${{ github.workspace }} - run: | - echo "GITHUB_WORKSPACE=`pwd`" >> $GITHUB_ENV - echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH - echo "$(brew --prefix bison)/bin" >> $GITHUB_PATH - echo "$(brew --prefix flex)/bin" >> $GITHUB_PATH - echo "procs=$(sysctl -n hw.ncpu)" >> $GITHUB_ENV - - - name: Tool versions - shell: bash - run: | - cc --version - - - name: Checkout Yosys - uses: actions/checkout@v4 - - - name: Get iverilog - shell: bash - run: | - git clone https://github.com/steveicarus/iverilog.git - cd iverilog - echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV - - - name: Cache iverilog - id: cache-iverilog - uses: actions/cache@v4 - with: - path: .local/ - key: ${{ matrix.os.id }}-${{ env.IVERILOG_GIT }} - - - name: Build iverilog - if: steps.cache-iverilog.outputs.cache-hit != 'true' - shell: bash - run: | - mkdir -p $GITHUB_WORKSPACE/.local/ - cd iverilog - autoconf - CC=gcc CXX=g++ ./configure --prefix=$GITHUB_WORKSPACE/.local/ - make -j${{ env.procs }} - make install - - - name: Build yosys - shell: bash - run: | - make config-clang - make -j${{ env.procs }} CXXSTD=${{ matrix.cpp_std }} CC=cc CXX=cc LD=cc - - - name: Run tests - if: matrix.cpp_std == 'c++11' - shell: bash - run: | - make -j${{ env.procs }} test CXXSTD=${{ matrix.cpp_std }} CC=cc CXX=cc LD=cc diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml new file mode 100644 index 00000000000..627a70d4794 --- /dev/null +++ b/.github/workflows/test-verific.yml @@ -0,0 +1,120 @@ +name: Build and run tests with Verific (Linux) + +on: [push, pull_request] + +jobs: + pre-job: + runs-on: ubuntu-latest + outputs: + should_skip: ${{ steps.skip_check.outputs.should_skip }} + steps: + - id: skip_check + uses: fkirc/skip-duplicate-actions@v5 + with: + paths_ignore: '["**/README.md"]' + # don't cancel previous builds + cancel_others: 'true' + # only run on push *or* pull_request, not both + concurrent_skipping: 'same_content_newer' + # we have special actions when running on main, so this should be off + skip_after_successful_duplicate: 'false' + + test-verific: + needs: pre-job + if: needs.pre-job.outputs.should_skip != 'true' + 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: Build Yosys + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j${{ env.procs }} ENABLE_LTO=1 + + - name: Install Yosys + run: | + make install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX= + + - name: Checkout SBY + uses: actions/checkout@v4 + with: + repository: 'YosysHQ/sby' + path: 'sby' + + - name: Build SBY + run: | + make -C sby install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX= + + - name: Run Yosys tests + run: | + make -j${{ env.procs }} test + + - name: Run Verific specific Yosys tests + run: | + make -C tests/sva + cd tests/svtypes && bash run-test.sh + + - name: Run SBY tests + if: ${{ github.ref == 'refs/heads/main' }} + run: | + make -C sby run_ci + + prepare-docs: + name: Generate docs artifact + needs: [pre-job, test-verific] + if: needs.pre-job.outputs.should_skip != 'true' + 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: Build Yosys + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j${{ env.procs }} ENABLE_LTO=1 + + - name: Prepare docs + shell: bash + run: + make docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs TARGETS= EXTRA_TARGETS= + + - name: Upload artifact + uses: actions/upload-artifact@v4 + with: + name: cmd-ref-${{ github.sha }} + path: | + docs/source/cmd + docs/source/generated + docs/source/_images + docs/source/code_examples + + - name: Trigger RTDs build + if: ${{ github.ref == 'refs/heads/main' }} + uses: dfm/rtds-action@v1.1.0 + with: + webhook_url: ${{ secrets.RTDS_WEBHOOK_URL }} + webhook_token: ${{ secrets.RTDS_WEBHOOK_TOKEN }} + commit_ref: ${{ github.ref }} diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml new file mode 100644 index 00000000000..c7aa6ecab70 --- /dev/null +++ b/.github/workflows/update-flake-lock.yml @@ -0,0 +1,22 @@ +name: update-flake-lock +on: + workflow_dispatch: # allows manual triggering + schedule: + - cron: '0 0 * * 0' # runs weekly on Sunday at 00:00 + +jobs: + lockfile: + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@v4 + - 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 index 47a7fe1a39f..f73c68bdf12 100644 --- a/.github/workflows/version.yml +++ b/.github/workflows/version.yml @@ -13,6 +13,7 @@ jobs: uses: actions/checkout@v4 with: fetch-depth: 0 + submodules: true - name: Take last commit id: log run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT diff --git a/.github/workflows/vs.yml b/.github/workflows/vs.yml deleted file mode 100644 index 799c5f259f4..00000000000 --- a/.github/workflows/vs.yml +++ /dev/null @@ -1,31 +0,0 @@ -name: Visual Studio Build - -on: [push, pull_request] - -jobs: - yosys-vcxsrc: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - name: Build - run: make vcxsrc YOSYS_VER=latest - - uses: actions/upload-artifact@v4 - with: - name: vcxsrc - path: yosys-win32-vcxsrc-latest.zip - - build: - runs-on: windows-2019 - needs: yosys-vcxsrc - steps: - - uses: actions/download-artifact@v4 - with: - name: vcxsrc - path: . - - name: unzip - run: unzip yosys-win32-vcxsrc-latest.zip - - name: setup-msbuild - uses: microsoft/setup-msbuild@v1 - - name: MSBuild - working-directory: yosys-win32-vcxsrc-latest - run: msbuild YosysVS.sln /p:PlatformToolset=v142 /p:Configuration=Release /p:WindowsTargetPlatformVersion=10.0.17763.0 diff --git a/.github/workflows/wasi.yml b/.github/workflows/wasi.yml deleted file mode 100644 index d6d200d92c2..00000000000 --- a/.github/workflows/wasi.yml +++ /dev/null @@ -1,30 +0,0 @@ -name: WASI Build - -on: [push, pull_request] - -jobs: - wasi: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - name: Build - run: | - WASI_SDK=wasi-sdk-19.0 - WASI_SDK_URL=https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-19/wasi-sdk-19.0-linux.tar.gz - if ! [ -d ${WASI_SDK} ]; then curl -L ${WASI_SDK_URL} | tar xzf -; fi - - mkdir -p build - cat > build/Makefile.conf < to use an external ABC instance @@ -214,10 +217,17 @@ ifeq ($(OS), OpenBSD) ABC_ARCHFLAGS += "-DABC_NO_RLIMIT" endif +# This gets overridden later. +LTOFLAGS := $(GCC_LTO) + ifeq ($(CONFIG),clang) CXX = clang++ -CXXFLAGS += -std=$(CXXSTD) -Os -ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -Wno-c++11-narrowing $(ABC_ARCHFLAGS)" +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) +ifeq ($(ENABLE_LTO),1) +LINKFLAGS += -fuse-ld=lld +endif +ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" +LTOFLAGS := $(CLANG_LTO) ifneq ($(SANITIZER),) $(info [Clang Sanitizer] $(SANITIZER)) @@ -233,19 +243,20 @@ endif ifneq ($(findstring cfi,$(SANITIZER)),) CXXFLAGS += -flto LINKFLAGS += -flto +LTOFLAGS = endif endif else ifeq ($(CONFIG),gcc) CXX = g++ -CXXFLAGS += -std=$(CXXSTD) -Os +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" else ifeq ($(CONFIG),gcc-static) LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -static LIBS := $(filter-out -lrt,$(LIBS)) CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -CXXFLAGS += -std=$(CXXSTD) -Os +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(CXX)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ ARCHFLAGS="-DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING=1 -Wno-unused-but-set-variable $(ARCHFLAGS)" ABC_USE_NO_READLINE=1 ifeq ($(DISABLE_ABC_THREADS),1) @@ -254,53 +265,14 @@ endif else ifeq ($(CONFIG),afl-gcc) CXX = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc -CXXFLAGS += -std=$(CXXSTD) -Os +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),cygwin) CXX = g++ -CXXFLAGS += -std=gnu++11 -Os +CXXFLAGS += -std=gnu++11 $(OPT_LEVEL) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" -else ifeq ($(CONFIG),emcc) -CXX = emcc -CXXFLAGS := -std=$(CXXSTD) $(filter-out -fPIC -ggdb,$(CXXFLAGS)) -ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8 -Wno-c++11-narrowing" -EMCC_CXXFLAGS := -Os -Wno-warn-absolute-paths -EMCC_LINKFLAGS := --embed-file share -EMCC_LINKFLAGS += -s NO_EXIT_RUNTIME=1 -EMCC_LINKFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" -EMCC_LINKFLAGS += -s TOTAL_MEMORY=134217728 -EMCC_LINKFLAGS += -s EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' -# https://github.com/kripken/emscripten/blob/master/src/settings.js -CXXFLAGS += $(EMCC_CXXFLAGS) -LINKFLAGS += $(EMCC_LINKFLAGS) -LIBS = -EXE = .js - -DISABLE_SPAWN := 1 - -TARGETS := $(filter-out $(PROGRAM_PREFIX)yosys-config,$(TARGETS)) -EXTRA_TARGETS += yosysjs-$(YOSYS_VER).zip - -ifeq ($(ENABLE_ABC),1) -LINK_ABC := 1 -DISABLE_ABC_THREADS := 1 -endif - -viz.js: - wget -O viz.js.part https://github.com/mdaines/viz.js/releases/download/0.0.3/viz.js - mv viz.js.part viz.js - -yosysjs-$(YOSYS_VER).zip: yosys.js viz.js misc/yosysjs/* - rm -rf yosysjs-$(YOSYS_VER) yosysjs-$(YOSYS_VER).zip - mkdir -p yosysjs-$(YOSYS_VER) - cp viz.js misc/yosysjs/* yosys.js yosys.wasm yosysjs-$(YOSYS_VER)/ - zip -r yosysjs-$(YOSYS_VER).zip yosysjs-$(YOSYS_VER) - -yosys.html: misc/yosys.html - $(P) cp misc/yosys.html yosys.html - else ifeq ($(CONFIG),wasi) ifeq ($(WASI_SDK),) CXX = clang++ @@ -313,11 +285,11 @@ AR = $(WASI_SDK)/bin/ar RANLIB = $(WASI_SDK)/bin/ranlib WASIFLAGS := --sysroot $(WASI_SDK)/share/wasi-sysroot $(WASIFLAGS) endif -CXXFLAGS := $(WASIFLAGS) -std=$(CXXSTD) -Os -D_WASI_EMULATED_PROCESS_CLOCKS $(filter-out -fPIC,$(CXXFLAGS)) +CXXFLAGS := $(WASIFLAGS) -std=$(CXXSTD) $(OPT_LEVEL) -D_WASI_EMULATED_PROCESS_CLOCKS $(filter-out -fPIC,$(CXXFLAGS)) LINKFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LINKFLAGS)) LIBS := -lwasi-emulated-process-clocks $(filter-out -lrt,$(LIBS)) ABCMKARGS += AR="$(AR)" RANLIB="$(RANLIB)" -ABCMKARGS += ARCHFLAGS="$(WASIFLAGS) -D_WASI_EMULATED_PROCESS_CLOCKS -DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING -DABC_NO_RLIMIT -Wno-c++11-narrowing" +ABCMKARGS += ARCHFLAGS="$(WASIFLAGS) -D_WASI_EMULATED_PROCESS_CLOCKS -DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING -DABC_NO_RLIMIT" ABCMKARGS += OPTFLAGS="-Os" EXE = .wasm @@ -331,7 +303,7 @@ endif else ifeq ($(CONFIG),mxe) PKG_CONFIG = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-pkg-config CXX = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ -CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s LIBS := $(filter-out -lrt,$(LIBS)) @@ -342,7 +314,7 @@ EXE = .exe else ifeq ($(CONFIG),msys2-32) CXX = i686-w64-mingw32-g++ -CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s LIBS := $(filter-out -lrt,$(LIBS)) @@ -352,7 +324,7 @@ EXE = .exe else ifeq ($(CONFIG),msys2-64) CXX = x86_64-w64-mingw32-g++ -CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s LIBS := $(filter-out -lrt,$(LIBS)) @@ -360,8 +332,19 @@ ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe -else ifneq ($(CONFIG),none) -$(error Invalid CONFIG setting '$(CONFIG)'. Valid values: clang, gcc, emcc, mxe, msys2-32, msys2-64) +else ifeq ($(CONFIG),none) +CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL) +ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" +LTOFLAGS = + +else +$(error Invalid CONFIG setting '$(CONFIG)'. Valid values: clang, gcc, mxe, msys2-32, msys2-64, none) +endif + + +ifeq ($(ENABLE_LTO),1) +CXXFLAGS += $(LTOFLAGS) +LINKFLAGS += $(LTOFLAGS) endif ifeq ($(ENABLE_LIBYOSYS),1) @@ -478,16 +461,8 @@ CXXFLAGS += -pg LINKFLAGS += -pg endif -ifeq ($(ENABLE_NDEBUG),1) -CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os -ggdb,$(CXXFLAGS)) -endif - ifeq ($(ENABLE_DEBUG),1) -ifeq ($(CONFIG),clang) -CXXFLAGS := -O0 -DDEBUG $(filter-out -Os,$(CXXFLAGS)) -else -CXXFLAGS := -Og -DDEBUG $(filter-out -Os,$(CXXFLAGS)) -endif +CXXFLAGS := -Og -DDEBUG $(filter-out $(OPT_LEVEL),$(CXXFLAGS)) endif ifeq ($(ENABLE_ABC),1) @@ -499,7 +474,7 @@ LIBS += -lpthread endif else ifeq ($(ABCEXTERNAL),) -TARGETS += $(PROGRAM_PREFIX)yosys-abc$(EXE) +TARGETS := $(PROGRAM_PREFIX)yosys-abc$(EXE) $(TARGETS) endif endif endif @@ -515,8 +490,24 @@ endif LIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= /usr/local/src/verific_lib -VERIFIC_COMPONENTS ?= verilog database util containers hier_tree -ifneq ($(DISABLE_VERIFIC_VHDL),1) +VERIFIC_COMPONENTS ?= database util containers +ifeq ($(ENABLE_VERIFIC_HIER_TREE),1) +VERIFIC_COMPONENTS += hier_tree +CXXFLAGS += -DVERIFIC_HIER_TREE_SUPPORT +else +ifneq ($(wildcard $(VERIFIC_DIR)/hier_tree),) +VERIFIC_COMPONENTS += hier_tree +endif +endif +ifeq ($(ENABLE_VERIFIC_SYSTEMVERILOG),1) +VERIFIC_COMPONENTS += verilog +CXXFLAGS += -DVERIFIC_SYSTEMVERILOG_SUPPORT +else +ifneq ($(wildcard $(VERIFIC_DIR)/verilog),) +VERIFIC_COMPONENTS += verilog +endif +endif +ifeq ($(ENABLE_VERIFIC_VHDL),1) VERIFIC_COMPONENTS += vhdl CXXFLAGS += -DVERIFIC_VHDL_SUPPORT else @@ -532,9 +523,13 @@ ifeq ($(ENABLE_VERIFIC_LIBERTY),1) VERIFIC_COMPONENTS += synlib CXXFLAGS += -DVERIFIC_LIBERTY_SUPPORT endif -ifneq ($(DISABLE_VERIFIC_EXTENSIONS),1) +ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1) VERIFIC_COMPONENTS += extensions CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS +else +ifneq ($(wildcard $(VERIFIC_DIR)/extensions),) +VERIFIC_COMPONENTS += extensions +endif endif CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC ifeq ($(OS), Darwin) @@ -596,6 +591,7 @@ S = endif $(eval $(call add_include_file,kernel/binding.h)) +$(eval $(call add_include_file,kernel/bitpattern.h)) $(eval $(call add_include_file,kernel/cellaigs.h)) $(eval $(call add_include_file,kernel/celledges.h)) $(eval $(call add_include_file,kernel/celltypes.h)) @@ -624,6 +620,7 @@ $(eval $(call add_include_file,kernel/sigtools.h)) $(eval $(call add_include_file,kernel/timinginfo.h)) $(eval $(call add_include_file,kernel/utils.h)) $(eval $(call add_include_file,kernel/yosys.h)) +$(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)) @@ -640,7 +637,7 @@ $(eval $(call add_include_file,backends/rtlil/rtlil_backend.h)) OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o OBJS += kernel/binding.o -OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/scopeinfo.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o +OBJS += kernel/cellaigs.o kernel/celledges.o kernel/cost.o kernel/satgen.o kernel/scopeinfo.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o ifeq ($(ENABLE_ZLIB),1) OBJS += kernel/fstdata.o endif @@ -730,9 +727,11 @@ top-all: $(TARGETS) $(EXTRA_TARGETS) @echo " Build successful." @echo "" -ifeq ($(CONFIG),emcc) -yosys.js: $(filter-out yosysjs-$(YOSYS_VER).zip,$(EXTRA_TARGETS)) -endif +.PHONY: compile-only +compile-only: $(OBJS) $(GENFILES) $(EXTRA_TARGETS) + @echo "" + @echo " Compile successful." + @echo "" $(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(LIBS) $(LIBS_VERIFIC) @@ -777,47 +776,46 @@ CXXFLAGS_NOVERIFIC = $(CXXFLAGS) LIBS_NOVERIFIC = $(LIBS) endif -$(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in +$(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in $(YOSYS_SRC)/Makefile $(P) $(SED) -e 's#@CXXFLAGS@#$(subst -Ilibs/dlfcn-win32,,$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(strip $(CXXFLAGS_NOVERIFIC))))#;' \ -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LINKFLAGS@#$(strip $(LINKFLAGS) $(PLUGIN_LINKFLAGS))#;' -e 's#@LIBS@#$(strip $(LIBS_NOVERIFIC) $(PLUGIN_LIBS))#;' \ -e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > $(PROGRAM_PREFIX)yosys-config $(Q) chmod +x $(PROGRAM_PREFIX)yosys-config -abc/abc-$(ABCREV)$(EXE) abc/libabc-$(ABCREV).a: - $(P) -ifneq ($(ABCREV),default) - $(Q) if test -d abc/.hg; then \ - echo 'REEBE: NOP qverpgbel vf n ut jbexvat pbcl! Erzbir nop/ naq er-eha "znxr".' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \ - fi - $(Q) if test -d abc && test -d abc/.git && ! git -C abc diff-index --quiet HEAD; then \ - echo 'REEBE: NOP pbagnvaf ybpny zbqvsvpngvbaf! Frg NOPERI=qrsnhyg va Lbflf Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \ - fi - $(Q) if test -d abc && ! test -d abc/.git && ! test "`cat abc/.gitcommit | cut -c1-7`" = "$(ABCREV)"; then \ - echo 'REEBE: Qbjaybnqrq NOP irefvbaf qbrf abg zngpu! Qbjaybnq sebz:' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; echo $(ABCURL)/archive/$(ABCREV).tar.gz; false; \ +.PHONY: check-git-abc + +check-git-abc: + @if [ ! -d "$(YOSYS_SRC)/abc" ]; then \ + echo "Error: The 'abc' directory does not exist."; \ + echo "Initialize the submodule: Run 'git submodule update --init' to set up 'abc' as a submodule."; \ + exit 1; \ + elif git -C "$(YOSYS_SRC)" submodule status abc 2>/dev/null | grep -q '^ '; then \ + exit 0; \ + elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && ! grep -q '\$$Format:%[hH]\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \ + echo "'abc' comes from a tarball. Continuing."; \ + exit 0; \ + elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && grep -q '\$$Format:%[hH]\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \ + echo "Error: 'abc' is not configured as a git submodule."; \ + echo "To resolve this:"; \ + echo "1. Back up your changes: Save any modifications from the 'abc' directory to another location."; \ + echo "2. Remove the existing 'abc' directory: Delete the 'abc' directory and all its contents."; \ + echo "3. Initialize the submodule: Run 'git submodule update --init' to set up 'abc' as a submodule."; \ + echo "4. Reapply your changes: Move your saved changes back to the 'abc' directory, if necessary."; \ + exit 1; \ + else \ + echo "Initialize the submodule: Run 'git submodule update --init' to set up 'abc' as a submodule."; \ + exit 1; \ fi -# set a variable so the test fails if git fails to run - when comparing outputs directly, empty string would match empty string - $(Q) if test -d abc && ! test -d abc/.git && test "`cat abc/.gitcommit | cut -c1-7`" = "$(ABCREV)"; then \ - echo "Compiling local copy of ABC"; \ - elif ! (cd abc 2> /dev/null && rev="`git rev-parse $(ABCREV)`" && test "`git rev-parse HEAD`" = "$$rev"); then \ - test $(ABCPULL) -ne 0 || { echo 'REEBE: NOP abg hc gb qngr naq NOPCHYY frg gb 0 va Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; exit 1; }; \ - echo "Pulling ABC from $(ABCURL):"; set -x; \ - test -d abc || git clone $(ABCURL) abc; \ - cd abc && $(MAKE) DEP= clean && git fetch $(ABCURL) && git checkout $(ABCREV); \ - fi -endif - $(Q) rm -f abc/abc-[0-9a-f]* - $(Q) $(MAKE) -C abc $(S) $(ABCMKARGS) $(if $(filter %.a,$@),PROG="abc-$(ABCREV)",PROG="abc-$(ABCREV)$(EXE)") MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: " $(if $(filter %.a,$@),libabc-$(ABCREV).a) -ifeq ($(ABCREV),default) -.PHONY: abc/abc-$(ABCREV)$(EXE) -.PHONY: abc/libabc-$(ABCREV).a -endif +abc/abc$(EXE) abc/libabc.a: | check-git-abc + $(P) + $(Q) mkdir -p abc && $(MAKE) -C $(PROGRAM_PREFIX)abc -f "$(realpath $(YOSYS_SRC)/abc/Makefile)" ABCSRC="$(realpath $(YOSYS_SRC)/abc/)" $(S) $(ABCMKARGS) $(if $(filter %.a,$@),PROG="abc",PROG="abc$(EXE)") MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: " $(if $(filter %.a,$@),libabc.a) -$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE) - $(P) cp abc/abc-$(ABCREV)$(EXE) $(PROGRAM_PREFIX)yosys-abc$(EXE) +$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc$(EXE) + $(P) cp $< $(PROGRAM_PREFIX)yosys-abc$(EXE) -$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc-$(ABCREV).a - $(P) cp abc/libabc-$(ABCREV).a $(PROGRAM_PREFIX)yosys-libabc.a +$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc.a + $(P) cp $< $(PROGRAM_PREFIX)yosys-libabc.a ifneq ($(SEED),) SEEDOPT="-S $(SEED)" @@ -883,6 +881,7 @@ endif +cd tests/arch/quicklogic/pp3 && bash run-test.sh $(SEEDOPT) +cd tests/arch/quicklogic/qlf_k6n10f && bash run-test.sh $(SEEDOPT) +cd tests/arch/gatemate && bash run-test.sh $(SEEDOPT) + +cd tests/arch/microchip && bash run-test.sh $(SEEDOPT) +cd tests/rpc && bash run-test.sh +cd tests/memfile && bash run-test.sh +cd tests/verilog && bash run-test.sh @@ -971,17 +970,47 @@ docs/source/cmd/abc.rst: $(TARGETS) $(EXTRA_TARGETS) mkdir -p docs/source/cmd ./$(PROGRAM_PREFIX)yosys -p 'help -write-rst-command-reference-manual' -PHONY: docs/gen_images docs/guidelines +PHONY: docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs +docs/gen_examples: + $(Q) $(MAKE) -C docs examples + docs/gen_images: - $(Q) $(MAKE) -C docs/images all + $(Q) $(MAKE) -C docs images DOCS_GUIDELINE_FILES := GettingStarted CodingStyle -docs/guidelines: - $(Q) mkdir -p docs/source/temp - $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp +docs/guidelines docs/source/generated: + $(Q) mkdir -p docs/source/generated + $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/generated + +# some commands return an error and print the usage text to stderr +define DOC_USAGE_STDERR +docs/source/generated/$(1): $(TARGETS) docs/source/generated + -$(Q) ./$(PROGRAM_PREFIX)$(1) --help 2> $$@ +endef +DOCS_USAGE_STDERR := yosys-config yosys-filterlib + +# The in-tree ABC (yosys-abc) is only built when ABCEXTERNAL is not set. +ifeq ($(ABCEXTERNAL),) +DOCS_USAGE_STDERR += yosys-abc +endif + +$(foreach usage,$(DOCS_USAGE_STDERR),$(eval $(call DOC_USAGE_STDERR,$(usage)))) + +# others print to stdout +define DOC_USAGE_STDOUT +docs/source/generated/$(1): $(TARGETS) docs/source/generated + $(Q) ./$(PROGRAM_PREFIX)$(1) --help > $$@ +endef +DOCS_USAGE_STDOUT := yosys yosys-smtbmc yosys-witness +$(foreach usage,$(DOCS_USAGE_STDOUT),$(eval $(call DOC_USAGE_STDOUT,$(usage)))) + +docs/usage: $(addprefix docs/source/generated/,$(DOCS_USAGE_STDOUT) $(DOCS_USAGE_STDERR)) + +docs/reqs: + $(Q) $(MAKE) -C docs reqs DOC_TARGET ?= html -docs: docs/source/cmd/abc.rst docs/gen_images docs/guidelines +docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs $(Q) $(MAKE) -C docs $(DOC_TARGET) clean: @@ -999,8 +1028,8 @@ clean: rm -rf vloghtb/Makefile vloghtb/refdat vloghtb/rtl vloghtb/scripts vloghtb/spec vloghtb/check_yosys vloghtb/vloghammer_tb.tar.bz2 vloghtb/temp vloghtb/log_test_* rm -f tests/svinterfaces/*.log_stdout tests/svinterfaces/*.log_stderr tests/svinterfaces/dut_result.txt tests/svinterfaces/reference_result.txt tests/svinterfaces/a.out tests/svinterfaces/*_syn.v tests/svinterfaces/*.diff rm -f tests/tools/cmp_tbdata - $(MAKE) -C docs clean - $(MAKE) -C docs/images clean + -$(MAKE) -C docs clean + -$(MAKE) -C docs/images clean rm -rf docs/source/cmd docs/util/__pycache__ clean-abc: @@ -1017,16 +1046,17 @@ coverage: genhtml coverage.info --output-directory coverage_html qtcreator: + echo "$(CXXFLAGS)" | grep -o '\-D[^ ]*' | tr ' ' '\n' | sed 's/-D/#define /' | sed 's/=/ /'> qtcreator.config { for file in $(basename $(OBJS)); do \ for prefix in cc y l; do if [ -f $${file}.$${prefix} ]; then echo $$file.$${prefix}; fi; done \ done; find backends frontends kernel libs passes -type f \( -name '*.h' -o -name '*.hh' \); } > qtcreator.files { echo .; find backends frontends kernel libs passes -type f \( -name '*.h' -o -name '*.hh' \) -printf '%h\n' | sort -u; } > qtcreator.includes - touch qtcreator.config qtcreator.creator + touch qtcreator.creator vcxsrc: $(GENFILES) $(EXTRA_TARGETS) rm -rf yosys-win32-vcxsrc-$(YOSYS_VER){,.zip} set -e; for f in `ls $(filter %.cc %.cpp,$(GENFILES)) $(addsuffix .cc,$(basename $(OBJS))) $(addsuffix .cpp,$(basename $(OBJS))) 2> /dev/null`; do \ - echo "Analyse: $$f" >&2; cpp -std=c++11 -MM -I. -D_YOSYS_ $$f; done | sed 's,.*:,,; s,//*,/,g; s,/[^/]*/\.\./,/,g; y, \\,\n\n,;' | grep '^[^/]' | sort -u | grep -v kernel/version_ > srcfiles.txt + echo "Analyse: $$f" >&2; cpp -std=c++17 -MM -I. -D_YOSYS_ $$f; done | sed 's,.*:,,; s,//*,/,g; s,/[^/]*/\.\./,/,g; y, \\,\n\n,;' | grep '^[^/]' | sort -u | grep -v kernel/version_ > srcfiles.txt bash misc/create_vcxsrc.sh yosys-win32-vcxsrc $(YOSYS_VER) $(GIT_REV) echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"Yosys (Version Information Unavailable)\"; }" > kernel/version.cc zip yosys-win32-vcxsrc-$(YOSYS_VER)/genfiles.zip $(GENFILES) kernel/version.cc @@ -1064,14 +1094,6 @@ config-gcc-static: clean config-afl-gcc: clean echo 'CONFIG := afl-gcc' > Makefile.conf -config-emcc: clean - echo 'CONFIG := emcc' > Makefile.conf - echo 'ENABLE_TCL := 0' >> Makefile.conf - echo 'ENABLE_ABC := 0' >> Makefile.conf - echo 'ENABLE_PLUGINS := 0' >> Makefile.conf - echo 'ENABLE_READLINE := 0' >> Makefile.conf - echo 'ENABLE_ZLIB := 0' >> Makefile.conf - config-wasi: clean echo 'CONFIG := wasi' > Makefile.conf echo 'ENABLE_TCL := 0' >> Makefile.conf @@ -1113,8 +1135,8 @@ echo-yosys-ver: echo-git-rev: @echo "$(GIT_REV)" -echo-abc-rev: - @echo "$(ABCREV)" +echo-cxx: + @echo "$(CXX)" -include libs/*/*.d -include frontends/*/*.d diff --git a/README.md b/README.md index 660bd5c6d57..7437bb2832b 100644 --- a/README.md +++ b/README.md @@ -71,7 +71,7 @@ Many Linux distributions also provide Yosys binaries, some more up to date than Building from Source ==================== -You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is +You need a C++ compiler with C++17 support (up-to-date CLANG or GCC is recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make. TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile). Xdot (graphviz) is used by the ``show`` command in yosys to display schematics. @@ -79,7 +79,7 @@ Xdot (graphviz) is used by the ``show`` command in yosys to display schematics. For example on Ubuntu Linux 16.04 LTS the following commands will install all prerequisites for building yosys: - $ sudo apt-get install build-essential clang bison flex \ + $ sudo apt-get install build-essential clang lld bison flex \ libreadline-dev gawk tcl-dev libffi-dev git \ graphviz xdot pkg-config python3 libboost-system-dev \ libboost-python-dev libboost-filesystem-dev zlib1g-dev @@ -105,11 +105,28 @@ For Cygwin use the following command to install all prerequisites, or select the setup-x86_64.exe -q --packages=bison,flex,gcc-core,gcc-g++,git,libffi-devel,libreadline-devel,make,pkg-config,python3,tcl-devel,boost-build,zlib-devel -To configure the build system to use a specific compiler, use one of +The environment variable `CXX` can be used to control the C++ compiler used, or +run one of the following: $ make config-clang $ make config-gcc +Note that these will result in `make` ignoring the `CXX` environment variable, +unless `CXX` is assigned in the call to make, e.g. + + $ make CXX=$CXX + +The Makefile has many variables influencing the build process. These can be +adjusted by modifying the Makefile.conf file which is created at the +`make config-...` step (see above), or they can be set by passing an option +to the make command directly. + +For example, if you have clang, and (a compatible version of) `ld.lld` +available in PATH, it's recommended to speed up incremental builds with +lld by enabling LTO: + + $ make ENABLE_LTO=1 + For other compilers and build configurations it might be necessary to make some changes to the config section of the Makefile. @@ -610,10 +627,12 @@ Simply visit https://yosys.readthedocs.io/en/latest/ instead. In addition to those packages listed above for building Yosys from source, the following are used for building the website: - $ sudo apt-get install pdf2svg faketime + $ sudo apt install pdf2svg faketime PDFLaTeX, included with most LaTeX distributions, is also needed during the -build process for the website. +build process for the website. Or, run the following: + + $ sudo apt install texlive-latex-base texlive-latex-extra latexmk The Python package, Sphinx, is needed along with those listed in `docs/source/requirements.txt`: diff --git a/abc b/abc new file mode 160000 index 00000000000..2188bc71228 --- /dev/null +++ b/abc @@ -0,0 +1 @@ +Subproject commit 2188bc71228b0788569d83ad2b7e7b91ca5dcc09 diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 877a829d37a..8dc14863d60 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -606,22 +606,30 @@ std::vector split_by(const std::string &str, const std::string &sep return result; } -std::string escape_cxx_string(const std::string &input) +std::string escape_c_string(const std::string &input) { - std::string output = "\""; + std::string output; + output.push_back('"'); for (auto c : input) { if (::isprint(c)) { if (c == '\\') output.push_back('\\'); output.push_back(c); } else { - char l = c & 0xf, h = (c >> 4) & 0xf; - output.append("\\x"); - output.push_back((h < 10 ? '0' + h : 'a' + h - 10)); - output.push_back((l < 10 ? '0' + l : 'a' + l - 10)); + char l = c & 0x3, m = (c >> 3) & 0x3, h = (c >> 6) & 0x3; + output.append("\\"); + output.push_back('0' + h); + output.push_back('0' + m); + output.push_back('0' + l); } } output.push_back('"'); + return output; +} + +std::string escape_cxx_string(const std::string &input) +{ + std::string output = escape_c_string(input); if (output.find('\0') != std::string::npos) { output.insert(0, "std::string {"); output.append(stringf(", %zu}", input.size())); @@ -1130,7 +1138,7 @@ struct CxxrtlWorker { f << indent << "// cell " << cell->name.str() << " syncs\n"; for (auto conn : cell->connections()) if (cell->output(conn.first)) - if (is_cxxrtl_sync_port(cell, conn.first)) { + if (is_cxxrtl_sync_port(cell, conn.first) && !conn.second.empty()) { f << indent; dump_sigspec_lhs(conn.second, for_debug); f << " = " << mangle(cell) << access << mangle_wire_name(conn.first) << ".curr;\n"; @@ -2275,46 +2283,92 @@ struct CxxrtlWorker { dec_indent(); } - void dump_metadata_map(const dict &metadata_map) - { + void dump_serialized_metadata(const dict &metadata_map) { + // Creating thousands metadata_map objects using initializer lists in a single function results in one of: + // 1. Megabytes of stack usage (with __attribute__((optnone))). + // 2. Minutes of compile time (without __attribute__((optnone))). + // So, don't create them. + std::string data; + auto put_u64 = [&](uint64_t value) { + for (size_t count = 0; count < 8; count++) { + data += (char)(value >> 56); + value <<= 8; + } + }; + for (auto metadata_item : metadata_map) { + if (!metadata_item.first.isPublic()) + continue; + if (metadata_item.second.size() > 64 && (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) == 0) { + f << indent << "/* attribute " << metadata_item.first.str().substr(1) << " is over 64 bits wide */\n"; + continue; + } + data += metadata_item.first.str().substr(1) + '\0'; + // In Yosys, a real is a type of string. + if (metadata_item.second.flags & RTLIL::CONST_FLAG_REAL) { + double dvalue = std::stod(metadata_item.second.decode_string()); + uint64_t uvalue; + static_assert(sizeof(dvalue) == sizeof(uvalue), "double must be 64 bits in size"); + memcpy(&uvalue, &dvalue, sizeof(uvalue)); + data += 'd'; + put_u64(uvalue); + } else if (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) { + data += 's'; + data += metadata_item.second.decode_string(); + data += '\0'; + } else if (metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED) { + data += 'i'; + put_u64((uint64_t)metadata_item.second.as_int(/*is_signed=*/true)); + } else { + data += 'u'; + put_u64(metadata_item.second.as_int(/*is_signed=*/false)); + } + } + f << escape_c_string(data); + } + + void dump_metadata_map(const dict &metadata_map) { if (metadata_map.empty()) { f << "metadata_map()"; - return; - } - f << "metadata_map({\n"; - inc_indent(); - for (auto metadata_item : metadata_map) { - if (!metadata_item.first.isPublic()) - continue; - if (metadata_item.second.size() > 64 && (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) == 0) { - f << indent << "/* attribute " << metadata_item.first.str().substr(1) << " is over 64 bits wide */\n"; - continue; - } - f << indent << "{ " << escape_cxx_string(metadata_item.first.str().substr(1)) << ", "; - // In Yosys, a real is a type of string. - if (metadata_item.second.flags & RTLIL::CONST_FLAG_REAL) { - f << std::showpoint << std::stod(metadata_item.second.decode_string()) << std::noshowpoint; - } else if (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) { - f << escape_cxx_string(metadata_item.second.decode_string()); - } else if (metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED) { - f << "INT64_C(" << metadata_item.second.as_int(/*is_signed=*/true) << ")"; - } else { - f << "UINT64_C(" << metadata_item.second.as_int(/*is_signed=*/false) << ")"; + } else { + f << "metadata_map({\n"; + inc_indent(); + for (auto metadata_item : metadata_map) { + if (!metadata_item.first.isPublic()) + continue; + if (metadata_item.second.size() > 64 && (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) == 0) { + f << indent << "/* attribute " << metadata_item.first.str().substr(1) << " is over 64 bits wide */\n"; + continue; + } + f << indent << "{ " << escape_cxx_string(metadata_item.first.str().substr(1)) << ", "; + // In Yosys, a real is a type of string. + if (metadata_item.second.flags & RTLIL::CONST_FLAG_REAL) { + f << std::showpoint << std::stod(metadata_item.second.decode_string()) << std::noshowpoint; + } else if (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) { + f << escape_cxx_string(metadata_item.second.decode_string()); + } else if (metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED) { + f << "INT64_C(" << metadata_item.second.as_int(/*is_signed=*/true) << ")"; + } else { + f << "UINT64_C(" << metadata_item.second.as_int(/*is_signed=*/false) << ")"; + } + f << " },\n"; } - f << " },\n"; - } - dec_indent(); - f << indent << "})"; + dec_indent(); + f << indent << "})"; + } } - void dump_debug_attrs(const RTLIL::AttrObject *object) + void dump_debug_attrs(const RTLIL::AttrObject *object, bool serialize = true) { dict attributes = object->attributes; // Inherently necessary to get access to the object, so a waste of space to emit. attributes.erase(ID::hdlname); // Internal Yosys attribute that should be removed but isn't. attributes.erase(ID::module_not_derived); - dump_metadata_map(attributes); + if (serialize) { + dump_serialized_metadata(attributes); + } else { + dump_metadata_map(attributes); + } } void dump_debug_info_method(RTLIL::Module *module) @@ -2337,7 +2391,7 @@ struct CxxrtlWorker { // The module is responsible for adding its own scope. f << indent << "scopes->add(path.empty() ? path : path.substr(0, path.size() - 1), "; f << escape_cxx_string(get_hdl_name(module)) << ", "; - dump_debug_attrs(module); + dump_debug_attrs(module, /*serialize=*/false); f << ", std::move(cell_attrs));\n"; count_scopes++; // If there were any submodules that were flattened, the module is also responsible for adding them. @@ -2347,11 +2401,11 @@ struct CxxrtlWorker { auto module_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Module); auto cell_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Cell); cell_attrs.erase(ID::module_not_derived); - f << indent << "scopes->add(path + " << escape_cxx_string(get_hdl_name(cell)) << ", "; + f << indent << "scopes->add(path, " << escape_cxx_string(get_hdl_name(cell)) << ", "; f << escape_cxx_string(cell->get_string_attribute(ID(module))) << ", "; - dump_metadata_map(module_attrs); + dump_serialized_metadata(module_attrs); f << ", "; - dump_metadata_map(cell_attrs); + dump_serialized_metadata(cell_attrs); f << ");\n"; } else log_assert(false && "Unknown $scopeinfo type"); count_scopes++; @@ -2419,20 +2473,22 @@ struct CxxrtlWorker { if (has_driven_sync + has_driven_comb + has_undriven > 1) count_mixed_driver++; - f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset; - bool first = true; - for (auto flag : flags) { - if (first) { - first = false; - f << ", "; - } else { - f << "|"; + f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; + dump_debug_attrs(wire); + f << ", " << mangle(wire); + if (wire->start_offset != 0 || !flags.empty()) { + f << ", " << wire->start_offset; + bool first = true; + for (auto flag : flags) { + if (first) { + first = false; + f << ", "; + } else { + f << "|"; + } + f << "debug_item::" << flag; } - f << "debug_item::" << flag; } - f << "), "; - dump_debug_attrs(wire); f << ");\n"; count_member_wires++; break; @@ -2440,16 +2496,18 @@ struct CxxrtlWorker { case WireType::ALIAS: { // Alias of a member wire const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); - f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item("; + f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; + dump_debug_attrs(aliasee); + f << ", "; // If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream // tooling has no way to find out about the outline. if (debug_wire_types[aliasee].is_outline()) f << "debug_eval_outline"; else f << "debug_alias()"; - f << ", " << mangle(aliasee) << ", " << wire->start_offset << "), "; - dump_debug_attrs(aliasee); + f << ", " << mangle(aliasee); + if (wire->start_offset != 0) + f << ", " << wire->start_offset; f << ");\n"; count_alias_wires++; break; @@ -2459,18 +2517,22 @@ struct CxxrtlWorker { f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; dump_const(debug_wire_type.sig_subst.as_const()); f << ";\n"; - f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "), "; + f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; dump_debug_attrs(wire); + f << ", const_" << mangle(wire); + if (wire->start_offset != 0) + f << ", " << wire->start_offset; f << ");\n"; count_const_wires++; break; } case WireType::OUTLINE: { // Localized or inlined, but rematerializable wire - f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire)); - f << ", debug_item(debug_eval_outline, " << mangle(wire) << ", " << wire->start_offset << "), "; + f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; dump_debug_attrs(wire); + f << ", debug_eval_outline, " << mangle(wire); + if (wire->start_offset != 0) + f << ", " << wire->start_offset; f << ");\n"; count_inline_wires++; break; @@ -2486,15 +2548,14 @@ struct CxxrtlWorker { for (auto &mem : mod_memories[module]) { if (!mem.memid.isPublic()) continue; - f << indent << "items->add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)); - f << ", debug_item(" << mangle(&mem) << ", "; - f << mem.start_offset << "), "; + f << indent << "items->add(path, " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)) << ", "; if (mem.packed) { dump_debug_attrs(mem.cell); } else { dump_debug_attrs(mem.mem); } - f << ");\n"; + f << ", " << mangle(&mem) << ", "; + f << mem.start_offset << ");\n"; } } dec_indent(); @@ -2506,7 +2567,7 @@ struct CxxrtlWorker { const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; f << indent << mangle(cell) << access; f << "debug_info(items, scopes, path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ", "; - dump_debug_attrs(cell); + dump_debug_attrs(cell, /*serialize=*/false); f << ");\n"; } } @@ -3202,6 +3263,7 @@ struct CxxrtlWorker { debug_wire_type = wire_type; // wire is a member if (!debug_alias) continue; + if (wire->port_input || wire->port_output) continue; // preserve input/output metadata in flags const RTLIL::Wire *it = wire; while (flow.is_inlinable(it)) { log_assert(flow.wire_comb_defs[it].size() == 1); diff --git a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc index 3c62401ddea..34801c2d118 100644 --- a/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc +++ b/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc @@ -47,7 +47,7 @@ cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path_) { cxxrtl_handle handle = new _cxxrtl_handle; handle->module = std::move(design->module); - handle->module->debug_info(handle->objects, top_path); + handle->module->debug_info(&handle->objects, nullptr, top_path); delete design; return handle; } diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h index b834cd12019..d1d6bd8dc68 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h @@ -625,11 +625,11 @@ struct value : public expr_base> { value remainder; value dividend = sext(); value divisor = other.template sext(); - if (dividend.is_neg()) dividend = dividend.neg(); - if (divisor.is_neg()) divisor = divisor.neg(); + if (is_neg()) dividend = dividend.neg(); + if (other.is_neg()) divisor = divisor.neg(); std::tie(quotient, remainder) = dividend.udivmod(divisor); - if (dividend.is_neg() != divisor.is_neg()) quotient = quotient.neg(); - if (dividend.is_neg()) remainder = remainder.neg(); + if (is_neg() != other.is_neg()) quotient = quotient.neg(); + if (is_neg()) remainder = remainder.neg(); return {quotient.template trunc(), remainder.template trunc()}; } }; @@ -941,6 +941,55 @@ struct metadata { assert(value_type == DOUBLE); return double_value; } + + // Internal CXXRTL use only. + static std::map deserialize(const char *ptr) { + std::map result; + std::string name; + // Grammar: + // string ::= [^\0]+ \0 + // metadata ::= [uid] .{8} | s + // map ::= ( )* \0 + for (;;) { + if (*ptr) { + name += *ptr++; + } else if (!name.empty()) { + ptr++; + auto get_u64 = [&]() { + uint64_t result = 0; + for (size_t count = 0; count < 8; count++) + result = (result << 8) | *ptr++; + return result; + }; + char type = *ptr++; + if (type == 'u') { + uint64_t value = get_u64(); + result.emplace(name, value); + } else if (type == 'i') { + int64_t value = (int64_t)get_u64(); + result.emplace(name, value); + } else if (type == 'd') { + double dvalue; + uint64_t uvalue = get_u64(); + static_assert(sizeof(dvalue) == sizeof(uvalue), "double must be 64 bits in size"); + memcpy(&dvalue, &uvalue, sizeof(dvalue)); + result.emplace(name, dvalue); + } else if (type == 's') { + std::string value; + while (*ptr) + value += *ptr++; + ptr++; + result.emplace(name, value); + } else { + assert(false && "Unknown type specifier"); + return result; + } + name.clear(); + } else { + return result; + } + } + } }; typedef std::map metadata_map; @@ -1010,22 +1059,24 @@ struct observer { // Default member initializers would make this a non-aggregate-type in C++11, so they are commented out. struct fmt_part { enum { - STRING = 0, + LITERAL = 0, INTEGER = 1, - CHARACTER = 2, - VLOG_TIME = 3, + STRING = 2, + UNICHAR = 3, + VLOG_TIME = 4, } type; - // STRING type + // LITERAL type std::string str; - // INTEGER/CHARACTER types + // INTEGER/STRING/UNICHAR types // + value val; - // INTEGER/CHARACTER/VLOG_TIME types + // INTEGER/STRING/VLOG_TIME types enum { RIGHT = 0, LEFT = 1, + NUMERIC = 2, } justify; // = RIGHT; char padding; // = '\0'; size_t width; // = 0; @@ -1033,7 +1084,14 @@ struct fmt_part { // INTEGER type unsigned base; // = 10; bool signed_; // = false; - bool plus; // = false; + enum { + MINUS = 0, + PLUS_MINUS = 1, + SPACE_MINUS = 2, + } sign; // = MINUS; + bool hex_upper; // = false; + bool show_base; // = false; + bool group; // = false; // VLOG_TIME type bool realtime; // = false; @@ -1049,11 +1107,12 @@ struct fmt_part { // We might want to replace some of these bit() calls with direct // chunk access if it turns out to be slow enough to matter. std::string buf; + std::string prefix; switch (type) { - case STRING: + case LITERAL: return str; - case CHARACTER: { + case STRING: { buf.reserve(Bits/8); for (int i = 0; i < Bits; i += 8) { char ch = 0; @@ -1067,35 +1126,76 @@ struct fmt_part { break; } + case UNICHAR: { + uint32_t codepoint = val.template get(); + if (codepoint >= 0x10000) + buf += (char)(0xf0 | (codepoint >> 18)); + else if (codepoint >= 0x800) + buf += (char)(0xe0 | (codepoint >> 12)); + else if (codepoint >= 0x80) + buf += (char)(0xc0 | (codepoint >> 6)); + else + buf += (char)codepoint; + if (codepoint >= 0x10000) + buf += (char)(0x80 | ((codepoint >> 12) & 0x3f)); + if (codepoint >= 0x800) + buf += (char)(0x80 | ((codepoint >> 6) & 0x3f)); + if (codepoint >= 0x80) + buf += (char)(0x80 | ((codepoint >> 0) & 0x3f)); + break; + } + case INTEGER: { - size_t width = Bits; + bool negative = signed_ && val.is_neg(); + if (negative) { + prefix = "-"; + val = val.neg(); + } else { + switch (sign) { + case MINUS: break; + case PLUS_MINUS: prefix = "+"; break; + case SPACE_MINUS: prefix = " "; break; + } + } + + size_t val_width = Bits; if (base != 10) { - width = 0; + val_width = 1; for (size_t index = 0; index < Bits; index++) if (val.bit(index)) - width = index + 1; + val_width = index + 1; } if (base == 2) { - for (size_t i = width; i > 0; i--) - buf += (val.bit(i - 1) ? '1' : '0'); + if (show_base) + prefix += "0b"; + for (size_t index = 0; index < val_width; index++) { + if (group && index > 0 && index % 4 == 0) + buf += '_'; + buf += (val.bit(index) ? '1' : '0'); + } } else if (base == 8 || base == 16) { + if (show_base) + prefix += (base == 16) ? (hex_upper ? "0X" : "0x") : "0o"; size_t step = (base == 16) ? 4 : 3; - for (size_t index = 0; index < width; index += step) { + for (size_t index = 0; index < val_width; index += step) { + if (group && index > 0 && index % (4 * step) == 0) + buf += '_'; uint8_t value = val.bit(index) | (val.bit(index + 1) << 1) | (val.bit(index + 2) << 2); if (step == 4) value |= val.bit(index + 3) << 3; - buf += "0123456789abcdef"[value]; + buf += (hex_upper ? "0123456789ABCDEF" : "0123456789abcdef")[value]; } - std::reverse(buf.begin(), buf.end()); } else if (base == 10) { - bool negative = signed_ && val.is_neg(); - if (negative) - val = val.neg(); + if (show_base) + prefix += "0d"; if (val.is_zero()) buf += '0'; value<(Bits > 4 ? Bits : 4)> xval = val.template zext<(Bits > 4 ? Bits : 4)>(); + size_t index = 0; while (!xval.is_zero()) { + if (group && index > 0 && index % 3 == 0) + buf += '_'; value<(Bits > 4 ? Bits : 4)> quotient, remainder; if (Bits >= 4) std::tie(quotient, remainder) = xval.udivmod(value<(Bits > 4 ? Bits : 4)>{10u}); @@ -1103,11 +1203,18 @@ struct fmt_part { std::tie(quotient, remainder) = std::make_pair(value<(Bits > 4 ? Bits : 4)>{0u}, xval); buf += '0' + remainder.template trunc<4>().template get(); xval = quotient; + index++; } - if (negative || plus) - buf += negative ? '-' : '+'; - std::reverse(buf.begin(), buf.end()); } else assert(false && "Unsupported base for fmt_part"); + if (justify == NUMERIC && group && padding == '0') { + int group_size = base == 10 ? 3 : 4; + while (prefix.size() + buf.size() < width) { + if (buf.size() % (group_size + 1) == group_size) + buf += '_'; + buf += '0'; + } + } + std::reverse(buf.begin(), buf.end()); break; } @@ -1123,17 +1230,29 @@ struct fmt_part { std::string str; assert(width == 0 || padding != '\0'); - if (justify == RIGHT && buf.size() < width) { - size_t pad_width = width - buf.size(); - if (padding == '0' && (buf.front() == '+' || buf.front() == '-')) { - str += buf.front(); - buf.erase(0, 1); - } - str += std::string(pad_width, padding); + if (prefix.size() + buf.size() < width) { + size_t pad_width = width - prefix.size() - buf.size(); + switch (justify) { + case LEFT: + str += prefix; + str += buf; + str += std::string(pad_width, padding); + break; + case RIGHT: + str += std::string(pad_width, padding); + str += prefix; + str += buf; + break; + case NUMERIC: + str += prefix; + str += std::string(pad_width, padding); + str += buf; + break; + } + } else { + str += prefix; + str += buf; } - str += buf; - if (justify == LEFT && buf.size() < width) - str += std::string(width - buf.size(), padding); return str; } }; @@ -1347,6 +1466,12 @@ struct debug_items { }); } + // This overload exists to reduce excessive stack slot allocation in `CXXRTL_EXTREMELY_COLD void debug_info()`. + template + void add(const std::string &base_path, const char *path, const char *serialized_item_attrs, T&&... args) { + add(base_path + path, debug_item(std::forward(args)...), metadata::deserialize(serialized_item_attrs)); + } + size_t count(const std::string &path) const { if (table.count(path) == 0) return 0; @@ -1393,6 +1518,11 @@ struct debug_scopes { scope.cell_attrs = std::unique_ptr(new debug_attrs { cell_attrs }); } + // This overload exists to reduce excessive stack slot allocation in `CXXRTL_EXTREMELY_COLD void debug_info()`. + void add(const std::string &base_path, const char *path, const char *module_name, const char *serialized_module_attrs, const char *serialized_cell_attrs) { + add(base_path + path, module_name, metadata::deserialize(serialized_module_attrs), metadata::deserialize(serialized_cell_attrs)); + } + size_t contains(const std::string &path) const { return table.count(path); } @@ -1452,7 +1582,7 @@ struct module { // Compatibility method. #if __has_attribute(deprecated) - __attribute__((deprecated("Use `debug_info(path, &items, /*scopes=*/nullptr);` instead. (`path` could be \"top \".)"))) + __attribute__((deprecated("Use `debug_info(&items, /*scopes=*/nullptr, path);` instead."))) #endif void debug_info(debug_items &items, std::string path) { debug_info(&items, /*scopes=*/nullptr, path); diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index b8233b007c6..9aa3e105d2c 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -512,9 +512,10 @@ class spool { spool &operator=(const spool &) = delete; ~spool() { - if (int fd = writefd.exchange(-1)) + int fd; + if ((fd = writefd.exchange(-1)) != -1) close(fd); - if (int fd = readfd.exchange(-1)) + if ((fd = readfd.exchange(-1)) != -1) close(fd); } diff --git a/backends/jny/jny.cc b/backends/jny/jny.cc index 9989feed599..1c163dba52e 100644 --- a/backends/jny/jny.cc +++ b/backends/jny/jny.cc @@ -124,7 +124,7 @@ struct JnyWriter design->sort(); f << "{\n"; - f << " \"$schema\": \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\",\n"; + f << " \"$schema\": \"https://raw.githubusercontent.com/YosysHQ/yosys/main/misc/jny.schema.json\",\n"; f << stringf(" \"generator\": \"%s\",\n", escape_string(yosys_version_str).c_str()); f << " \"version\": \"0.0.1\",\n"; f << " \"invocation\": \"" << escape_string(invk) << "\",\n"; @@ -426,7 +426,7 @@ struct JnyBackend : public Backend { log(" Don't include property information in the netlist output.\n"); log("\n"); log("The JSON schema for JNY output files is located in the \"jny.schema.json\" file\n"); - log("which is located at \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\"\n"); + log("which is located at \"https://raw.githubusercontent.com/YosysHQ/yosys/main/misc/jny.schema.json\"\n"); log("\n"); } diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc index 574eb3aaad1..032954d8cd6 100644 --- a/backends/rtlil/rtlil_backend.cc +++ b/backends/rtlil/rtlil_backend.cc @@ -51,6 +51,9 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi } } f << stringf("%d'", width); + if (data.flags & RTLIL::CONST_FLAG_SIGNED) { + f << stringf("s"); + } if (data.is_fully_undef_x_only()) { f << "x"; } else { diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index cc47bc3762a..c3bdcebbe96 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -57,6 +57,8 @@ check_witness = False detect_loops = False incremental = None +track_assumes = False +minimize_assumes = False so = SmtOpts() @@ -189,6 +191,14 @@ def help(): --incremental run in incremental mode (experimental) + --track-assumes + track individual assumptions and report a subset of used + assumptions that are sufficient for the reported outcome. This + can be used to debug PREUNSAT failures as well as to find a + smaller set of sufficient assumptions. + + --minimize-assumes + when using --track-assumes, solve for a minimal set of sufficient assumptions. """ + so.helpmsg()) def usage(): @@ -200,7 +210,8 @@ def usage(): opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:higcm:", so.longopts + ["help", "final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops", "incremental"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops", "incremental", + "track-assumes", "minimize-assumes"]) except: usage() @@ -289,6 +300,10 @@ def usage(): elif o == "--incremental": from smtbmc_incremental import Incremental incremental = Incremental() + elif o == "--track-assumes": + track_assumes = True + elif o == "--minimize-assumes": + minimize_assumes = True elif so.handle(o, a): pass else: @@ -447,6 +462,9 @@ def replace_netref(match): smt = SmtIo(opts=so) +if track_assumes: + smt.smt2_options[':produce-unsat-assumptions'] = 'true' + if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None: smt.produce_models = False @@ -651,18 +669,12 @@ def print_msg(msg): ywfile_hierwitness_cache = None -def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): +def ywfile_hierwitness(): global ywfile_hierwitness_cache - if map_steps is None: - map_steps = {} + if ywfile_hierwitness_cache is None: + ywfile_hierwitness = smt.hierwitness(topmod, allregs=True, blackbox=True) - with open(inywfile, "r") as f: - inyw = ReadWitness(f) - - if ywfile_hierwitness_cache is None: - ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) - - inits, seqs, clocks, mems = ywfile_hierwitness_cache + inits, seqs, clocks, mems = ywfile_hierwitness smt_wires = defaultdict(list) smt_mems = defaultdict(list) @@ -673,91 +685,152 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): for mem in mems: smt_mems[mem["path"]].append(mem) - addr_re = re.compile(r'\\\[[0-9]+\]$') - bits_re = re.compile(r'[01?]*$') + ywfile_hierwitness_cache = inits, seqs, clocks, mems, smt_wires, smt_mems - max_t = -1 + return ywfile_hierwitness_cache - for t, step in inyw.steps(): - present_signals, missing = step.present_signals(inyw.sigmap) - for sig in present_signals: - bits = step[sig] - if skip_x: - bits = bits.replace('x', '?') - if not bits_re.match(bits): - raise ValueError("unsupported bit value in Yosys witness file") +def_bits_re = re.compile(r'([01]+)') - sig_end = sig.offset + len(bits) - if sig.path in smt_wires: - for wire in smt_wires[sig.path]: - width, offset = wire["width"], wire["offset"] +def smt_extract_mask(smt_expr, mask): + chunks = [] + def_bits = '' - smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + mask_index_order = mask[::-1] - offset = max(offset, 0) + for matched in def_bits_re.finditer(mask_index_order): + chunks.append(matched.span()) + def_bits += matched[0] - end = width + offset - common_offset = max(sig.offset, offset) - common_end = min(sig_end, end) - if common_end <= common_offset: - continue + if not chunks: + return - smt_expr = smt.witness_net_expr(topmod, f"s{map_steps.get(t, t)}", wire) + if len(chunks) == 1: + start, end = chunks[0] + if start == 0 and end == len(mask_index_order): + combined_chunks = smt_expr + else: + combined_chunks = '((_ extract %d %d) %s)' % (end - 1, start, smt_expr) + else: + combined_chunks = '(let ((x %s)) (concat %s))' % (smt_expr, ' '.join( + '((_ extract %d %d) x)' % (end - 1, start) + for start, end in reversed(chunks) + )) - if not smt_bool: - slice_high = common_end - offset - 1 - slice_low = common_offset - offset - smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr) + return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1] - bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] +def smt_concat(exprs): + if not isinstance(exprs, (tuple, list)): + exprs = tuple(exprs) + if not exprs: + return "" + if len(exprs) == 1: + return exprs[1] + return "(concat %s)" % ' '.join(exprs) - if bit_slice.count("?") == len(bit_slice): - continue +def ywfile_signal(sig, step, mask=None): + assert sig.width > 0 - if smt_bool: - assert width == 1 - smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false") - else: - if "?" in bit_slice: - mask = bit_slice.replace("0", "1").replace("?", "0") - bit_slice = bit_slice.replace("?", "0") - smt_expr = "(bvand %s #b%s)" % (smt_expr, mask) + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + sig_end = sig.offset + sig.width - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + output = [] - constr_assumes[t].append((inywfile, smt_constr)) + if sig.path in smt_wires: + for wire in smt_wires[sig.path]: + width, offset = wire["width"], wire["offset"] - if sig.memory_path: - if sig.memory_path in smt_mems: - for mem in smt_mems[sig.memory_path]: - width, size, bv = mem["width"], mem["size"], mem["statebv"] + smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 - smt_expr = smt.net_expr(topmod, f"s{map_steps.get(t, t)}", mem["smtpath"]) + offset = max(offset, 0) - if bv: - word_low = sig.memory_addr * width - word_high = word_low + width - 1 - smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr) - else: - addr_width = (size - 1).bit_length() - addr_bits = f"{sig.memory_addr:0{addr_width}b}" - smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits) + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue - if len(bits) < width: - slice_high = sig.offset + len(bits) - 1 - smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + smt_expr = smt.witness_net_expr(topmod, f"s{step}", wire) - bit_slice = bits + if not smt_bool: + slice_high = common_end - offset - 1 + slice_low = common_offset - offset + smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr) + else: + smt_expr = "(ite %s #b1 #b0)" % smt_expr - if "?" in bit_slice: - mask = bit_slice.replace("0", "1").replace("?", "0") - bit_slice = bit_slice.replace("?", "0") - smt_expr = "(bvand %s #b%s)" % (smt_expr, mask) + output.append(((common_offset - sig.offset), (common_end - sig.offset), smt_expr)) - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - constr_assumes[t].append((inywfile, smt_constr)) - max_t = t + if sig.memory_path: + if sig.memory_path in smt_mems: + for mem in smt_mems[sig.memory_path]: + width, size, bv = mem["width"], mem["size"], mem["statebv"] + + smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"]) + + if bv: + word_low = sig.memory_addr * width + word_high = word_low + width - 1 + smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr) + else: + addr_width = (size - 1).bit_length() + addr_bits = f"{sig.memory_addr:0{addr_width}b}" + smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits) + + if sig.width < width: + slice_high = sig.offset + sig.width - 1 + smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + + output.append((0, sig.width, smt_expr)) + + output.sort() + + output = [chunk for chunk in output if chunk[0] != chunk[1]] + + pos = 0 + + for start, end, smt_expr in output: + assert start == pos + pos = end + + assert pos == sig.width + + if len(output) == 1: + return output[0][-1] + return smt_concat(smt_expr for start, end, smt_expr in reversed(output)) + +def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache + if map_steps is None: + map_steps = {} + + with open(inywfile, "r") as f: + inyw = ReadWitness(f) + + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + + bits_re = re.compile(r'[01?]*$') + max_t = -1 + for t, step in inyw.steps(): + present_signals, missing = step.present_signals(inyw.sigmap) + for sig in present_signals: + bits = step[sig] + if skip_x: + bits = bits.replace('x', '?') + if not bits_re.match(bits): + raise ValueError("unsupported bit value in Yosys witness file") + + if bits.count('?') == len(bits): + continue + + smt_expr = ywfile_signal(sig, map_steps.get(t, t)) + + smt_expr, bits = smt_extract_mask(smt_expr, bits) + + smt_constr = "(= %s #b%s)" % (smt_expr, bits) + constr_assumes[t].append((inywfile, smt_constr)) + + max_t = t return max_t if inywfile is not None: @@ -1348,11 +1421,11 @@ def write_yw_trace(steps, index, allregs=False, filename=None): exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs) - all_sigs.append(sigs) + all_sigs.append((step_values, sigs)) bvs = iter(smt.get_list(exprs)) - for sigs in all_sigs: + for (step_values, sigs) in all_sigs: for sig in sigs: value = smt.bv2bin(next(bvs)) step_values[sig["sig"]] = value @@ -1497,6 +1570,44 @@ def get_active_assert_map(step, active): return assert_map +assume_enables = {} + +def declare_assume_enables(): + def recurse(mod, path, key_base=()): + for expr, desc in smt.modinfo[mod].assumes.items(): + enable = f"|assume_enable {len(assume_enables)}|" + smt.smt2_assumptions[(expr, key_base)] = enable + smt.write(f"(declare-const {enable} Bool)") + assume_enables[(expr, key_base)] = (enable, path, desc) + + for cell, submod in smt.modinfo[mod].cells.items(): + recurse(submod, f"{path}.{cell}", (mod, cell, key_base)) + + recurse(topmod, topmod) + +if track_assumes: + declare_assume_enables() + +def smt_assert_design_assumes(step): + if not track_assumes: + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + return + + if not assume_enables: + return + + def expr_for_assume(assume_key, base=None): + expr, key_base = assume_key + expr_prefix = f"(|{expr}| " + expr_suffix = ")" + while key_base: + mod, cell, key_base = key_base + expr_prefix += f"(|{mod}_h {cell}| " + expr_suffix += ")" + return f"{expr_prefix} s{step}{expr_suffix}" + + for assume_key, (enable, path, desc) in assume_enables.items(): + smt_assert_consequent(f"(=> {enable} {expr_for_assume(assume_key)})") states = list() asserts_antecedent_cache = [list()] @@ -1651,6 +1762,13 @@ def smt_check_sat(expected=["sat", "unsat"]): smt_forall_assert() return smt.check_sat(expected=expected) +def report_tracked_assumptions(msg): + if track_assumes: + print_msg(msg) + for key in smt.get_unsat_assumptions(minimize=minimize_assumes): + enable, path, descr = assume_enables[key] + print_msg(f" In {path}: {descr}") + if incremental: incremental.mainloop() @@ -1664,7 +1782,7 @@ def smt_check_sat(expected=["sat", "unsat"]): break smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1707,6 +1825,7 @@ def smt_check_sat(expected=["sat", "unsat"]): else: print_msg("Temporal induction successful.") + report_tracked_assumptions("Used assumptions:") retstatus = "PASSED" break @@ -1732,7 +1851,7 @@ def smt_check_sat(expected=["sat", "unsat"]): while step < num_steps: smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1753,6 +1872,7 @@ def smt_check_sat(expected=["sat", "unsat"]): smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc))) if smt_check_sat() == "unsat": + report_tracked_assumptions("Used assumptions:") smt_pop() break @@ -1761,13 +1881,14 @@ def smt_check_sat(expected=["sat", "unsat"]): print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + smt_assert_design_assumes(i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + report_tracked_assumptions("Conflicting assumptions:") found_failed_assert = True retstatus = "FAILED" break @@ -1823,7 +1944,7 @@ def smt_check_sat(expected=["sat", "unsat"]): retstatus = "PASSED" while step < num_steps: smt_state(step) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_design_assumes(step) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1853,7 +1974,7 @@ def smt_check_sat(expected=["sat", "unsat"]): if step+i < num_steps: smt_state(step+i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i)) + smt_assert_design_assumes(step + i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i)) smt_assert_consequent(get_constr_expr(constr_assumes, step+i)) @@ -1867,7 +1988,8 @@ def smt_check_sat(expected=["sat", "unsat"]): print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) if smt_check_sat() == "unsat": - print("%s Assumptions are unsatisfiable!" % smt.timestamp()) + print_msg("Assumptions are unsatisfiable!") + report_tracked_assumptions("Conficting assumptions:") retstatus = "PREUNSAT" break @@ -1920,13 +2042,14 @@ def smt_check_sat(expected=["sat", "unsat"]): print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + smt_assert_design_assumes(i) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": - print("%s Cannot append steps without violating assumptions!" % smt.timestamp()) + print_msg("Cannot append steps without violating assumptions!") + report_tracked_assumptions("Conflicting assumptions:") retstatus = "FAILED" break print_anyconsts(step) diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index 1a2a4570312..0bd280b4a48 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -1,7 +1,7 @@ from collections import defaultdict import json import typing -from functools import partial +import ywio if typing.TYPE_CHECKING: import smtbmc @@ -15,6 +15,14 @@ class InteractiveError(Exception): pass +def mkkey(data): + if isinstance(data, list): + return tuple(map(mkkey, data)) + elif isinstance(data, dict): + raise InteractiveError(f"JSON objects found in assumption key: {data!r}") + return data + + class Incremental: def __init__(self): self.traceidx = 0 @@ -26,6 +34,7 @@ def __init__(self): self._witness_index = None self._yw_constraints = {} + self._define_sorts = {} def setup(self): generic_assert_map = smtbmc.get_assert_map( @@ -73,17 +82,17 @@ def expr_arg_len(self, expr, min_len, max_len=-1): if min_len is not None and arg_len < min_len: if min_len == max_len: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression must have " f"{min_len} argument{'s' if min_len != 1 else ''}" ) else: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression must have at least " f"{min_len} argument{'s' if min_len != 1 else ''}" ) if max_len is not None and arg_len > max_len: - raise ( + raise InteractiveError( f"{json.dumps(expr[0])} expression can have at most " f"{min_len} argument{'s' if max_len != 1 else ''}" ) @@ -96,14 +105,31 @@ def expr_step(self, expr, smt_out): smt_out.append(f"s{step}") return "module", smtbmc.topmod - def expr_mod_constraint(self, expr, smt_out): - self.expr_arg_len(expr, 1) + def expr_cell(self, expr, smt_out): + self.expr_arg_len(expr, 2) position = len(smt_out) smt_out.append(None) - arg_sort = self.expr(expr[1], smt_out, required_sort=["module", None]) + arg_sort = self.expr(expr[2], smt_out, required_sort=["module", None]) + smt_out.append(")") module = arg_sort[1] + cell = expr[1] + submod = smtbmc.smt.modinfo[module].cells.get(cell) + if submod is None: + raise InteractiveError(f"module {module!r} has no cell {cell!r}") + smt_out[position] = f"(|{module}_h {cell}| " + return ("module", submod) + + def expr_mod_constraint(self, expr, smt_out): suffix = expr[0][3:] - smt_out[position] = f"(|{module}{suffix}| " + self.expr_arg_len(expr, 1, 2 if suffix in ["_a", "_u", "_c"] else 1) + position = len(smt_out) + smt_out.append(None) + arg_sort = self.expr(expr[-1], smt_out, required_sort=["module", None]) + module = arg_sort[1] + if len(expr) == 3: + smt_out[position] = f"(|{module}{suffix} {expr[1]}| " + else: + smt_out[position] = f"(|{module}{suffix}| " smt_out.append(")") return "Bool" @@ -150,11 +176,7 @@ def expr_andor(self, expr, smt_out): if len(expr) == 1: smt_out.push({"and": "true", "or": "false"}[expr[0]]) elif len(expr) == 2: - arg_sort = self.expr(expr[1], smt_out) - if arg_sort != "Bool": - raise InteractiveError( - f"arguments of {json.dumps(expr[0])} must have sort Bool" - ) + self.expr(expr[1], smt_out, required_sort="Bool") else: sep = f"({expr[0]} " for arg in expr[1:]: @@ -164,7 +186,51 @@ def expr_andor(self, expr, smt_out): smt_out.append(")") return "Bool" + def expr_bv_binop(self, expr, smt_out): + self.expr_arg_len(expr, 2) + + smt_out.append(f"({expr[0]} ") + arg_sort = self.expr(expr[1], smt_out, required_sort=("BitVec", None)) + smt_out.append(" ") + self.expr(expr[2], smt_out, required_sort=arg_sort) + smt_out.append(")") + return arg_sort + + def expr_extract(self, expr, smt_out): + self.expr_arg_len(expr, 3) + + hi = expr[1] + lo = expr[2] + + smt_out.append(f"((_ extract {hi} {lo}) ") + + arg_sort = self.expr(expr[3], smt_out, required_sort=("BitVec", None)) + smt_out.append(")") + + if not (isinstance(hi, int) and 0 <= hi < arg_sort[1]): + raise InteractiveError( + f"high bit index must be 0 <= index < {arg_sort[1]}, is {hi!r}" + ) + if not (isinstance(lo, int) and 0 <= lo <= hi): + raise InteractiveError( + f"low bit index must be 0 <= index < {hi}, is {lo!r}" + ) + + return "BitVec", hi - lo + 1 + + def expr_bv(self, expr, smt_out): + self.expr_arg_len(expr, 1) + + arg = expr[1] + if not isinstance(arg, str) or arg.count("0") + arg.count("1") != len(arg): + raise InteractiveError("bv argument must contain only 0 or 1 bits") + + smt_out.append("#b" + arg) + + return "BitVec", len(arg) + def expr_yw(self, expr, smt_out): + self.expr_arg_len(expr, 1, 2) if len(expr) == 2: name = None step = expr[1] @@ -194,6 +260,40 @@ def expr_yw(self, expr, smt_out): return "Bool" + def expr_yw_sig(self, expr, smt_out): + self.expr_arg_len(expr, 3, 4) + + step = expr[1] + path = expr[2] + offset = expr[3] + width = expr[4] if len(expr) == 5 else 1 + + if not isinstance(offset, int) or offset < 0: + raise InteractiveError( + f"offset must be a non-negative integer, got {json.dumps(offset)}" + ) + + if not isinstance(width, int) or width <= 0: + raise InteractiveError( + f"width must be a positive integer, got {json.dumps(width)}" + ) + + if not isinstance(path, list) or not all(isinstance(s, str) for s in path): + raise InteractiveError( + f"path must be a string list, got {json.dumps(path)}" + ) + + if step not in self.state_set: + raise InteractiveError(f"step {step} not declared") + + smt_expr = smtbmc.ywfile_signal( + ywio.WitnessSig(path=path, offset=offset, width=width), step + ) + + smt_out.append(smt_expr) + + return "BitVec", width + def expr_smtlib(self, expr, smt_out): self.expr_arg_len(expr, 2) @@ -206,10 +306,15 @@ def expr_smtlib(self, expr, smt_out): f"got {json.dumps(smtlib_expr)}" ) - if not isinstance(sort, str): - raise InteractiveError( - f"raw SMT-LIB sort has to be a string, got {json.dumps(sort)}" - ) + if ( + isinstance(sort, list) + and len(sort) == 2 + and sort[0] == "BitVec" + and (sort[1] is None or isinstance(sort[1], int)) + ): + sort = tuple(sort) + elif not isinstance(sort, str): + raise InteractiveError(f"unsupported raw SMT-LIB sort {json.dumps(sort)}") smt_out.append(smtlib_expr) return sort @@ -223,20 +328,27 @@ def expr_label(self, expr, smt_out): subexpr = expr[2] if not isinstance(label, str): - raise InteractiveError(f"expression label has to be a string") + raise InteractiveError("expression label has to be a string") smt_out.append("(! ") - smt_out.appedd(label) - smt_out.append(" ") - sort = self.expr(subexpr, smt_out) - + smt_out.append(" :named ") + smt_out.append(label) smt_out.append(")") return sort + def expr_def(self, expr, smt_out): + self.expr_arg_len(expr, 1) + sort = self._define_sorts.get(expr[1]) + if sort is None: + raise InteractiveError(f"unknown definition {json.dumps(expr)}") + smt_out.append(expr[1]) + return sort + expr_handlers = { "step": expr_step, + "cell": expr_cell, "mod_h": expr_mod_constraint, "mod_is": expr_mod_constraint, "mod_i": expr_mod_constraint, @@ -246,8 +358,15 @@ def expr_label(self, expr, smt_out): "not": expr_not, "and": expr_andor, "or": expr_andor, + "bv": expr_bv, + "bvand": expr_bv_binop, + "bvor": expr_bv_binop, + "bvxor": expr_bv_binop, + "extract": expr_extract, + "def": expr_def, "=": expr_eq, "yw": expr_yw, + "yw_sig": expr_yw_sig, "smtlib": expr_smtlib, "!": expr_label, } @@ -281,10 +400,13 @@ def expr(self, expr, smt_out, required_sort=None): raise InteractiveError(f"unknown expression {json.dumps(expr[0])}") def expr_smt(self, expr, required_sort): + return self.expr_smt_and_sort(expr, required_sort)[0] + + def expr_smt_and_sort(self, expr, required_sort=None): smt_out = [] - self.expr(expr, smt_out, required_sort=required_sort) + output_sort = self.expr(expr, smt_out, required_sort=required_sort) out = "".join(smt_out) - return out + return out, output_sort def cmd_new_step(self, cmd): step = self.arg_step(cmd, declare=True) @@ -302,6 +424,29 @@ def cmd_assert(self, cmd): assert_fn(self.expr_smt(cmd.get("expr"), "Bool")) + def cmd_assert_design_assumes(self, cmd): + step = self.arg_step(cmd) + smtbmc.smt_assert_design_assumes(step) + + def cmd_get_design_assume(self, cmd): + key = mkkey(cmd.get("key")) + return smtbmc.assume_enables.get(key) + + def cmd_update_assumptions(self, cmd): + expr = cmd.get("expr") + key = cmd.get("key") + + key = mkkey(key) + + result = smtbmc.smt.smt2_assumptions.pop(key, None) + if expr is not None: + expr = self.expr_smt(expr, "Bool") + smtbmc.smt.smt2_assumptions[key] = expr + return result + + def cmd_get_unsat_assumptions(self, cmd): + return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get("minimize"))) + def cmd_push(self, cmd): smtbmc.smt_push() @@ -313,11 +458,35 @@ def cmd_check(self, cmd): def cmd_smtlib(self, cmd): command = cmd.get("command") + response = cmd.get("response", False) if not isinstance(command, str): raise InteractiveError( f"raw SMT-LIB command must be a string, found {json.dumps(command)}" ) smtbmc.smt.write(command) + if response: + return smtbmc.smt.read() + + def cmd_define(self, cmd): + expr = cmd.get("expr") + if expr is None: + raise InteractiveError("'define' copmmand requires 'expr' parameter") + + expr, sort = self.expr_smt_and_sort(expr) + + if isinstance(sort, tuple) and sort[0] == "module": + raise InteractiveError("'define' does not support module sorts") + + define_name = f"|inc def {len(self._define_sorts)}|" + + self._define_sorts[define_name] = sort + + if isinstance(sort, tuple): + sort = f"(_ {' '.join(map(str, sort))})" + + smtbmc.smt.write(f"(define-const {define_name} {sort} {expr})") + + return {"name": define_name} def cmd_design_hierwitness(self, cmd=None): allregs = (cmd is None) or bool(cmd.get("allreges", False)) @@ -369,6 +538,21 @@ def cmd_read_yw_trace(self, cmd): return dict(last_step=last_step) + def cmd_modinfo(self, cmd): + fields = cmd.get("fields", []) + + mod = cmd.get("mod") + if mod is None: + mod = smtbmc.topmod + modinfo = smtbmc.smt.modinfo.get(mod) + if modinfo is None: + return None + + result = dict(name=mod) + for field in fields: + result[field] = getattr(modinfo, field, None) + return result + def cmd_ping(self, cmd): return cmd @@ -377,13 +561,19 @@ def cmd_ping(self, cmd): "assert": cmd_assert, "assert_antecedent": cmd_assert, "assert_consequent": cmd_assert, + "assert_design_assumes": cmd_assert_design_assumes, + "get_design_assume": cmd_get_design_assume, + "update_assumptions": cmd_update_assumptions, + "get_unsat_assumptions": cmd_get_unsat_assumptions, "push": cmd_push, "pop": cmd_pop, "check": cmd_check, "smtlib": cmd_smtlib, + "define": cmd_define, "design_hierwitness": cmd_design_hierwitness, "write_yw_trace": cmd_write_yw_trace, "read_yw_trace": cmd_read_yw_trace, + "modinfo": cmd_modinfo, "ping": cmd_ping, } diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index c904aea9531..5fc3ab5a424 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -114,6 +114,7 @@ def __init__(self): self.clocks = dict() self.cells = dict() self.asserts = dict() + self.assumes = dict() self.covers = dict() self.maximize = set() self.minimize = set() @@ -141,6 +142,7 @@ def __init__(self, opts=None): self.recheck = False self.smt2cache = [list()] self.smt2_options = dict() + self.smt2_assumptions = dict() self.p = None self.p_index = solvers_index solvers_index += 1 @@ -158,6 +160,7 @@ def __init__(self, opts=None): self.noincr = opts.noincr self.info_stmts = opts.info_stmts self.nocomments = opts.nocomments + self.smt2_options.update(opts.smt2_options) else: self.solver = "yices" @@ -602,6 +605,12 @@ def info(self, stmt): else: self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-assume": + if len(fields) > 4: + self.modinfo[self.curmod].assumes["%s_u %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].assumes["%s_u %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-maximize": self.modinfo[self.curmod].maximize.add(fields[2]) @@ -785,8 +794,13 @@ def read(self): return stmt def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]): + if self.smt2_assumptions: + assume_exprs = " ".join(self.smt2_assumptions.values()) + check_stmt = f"(check-sat-assuming ({assume_exprs}))" + else: + check_stmt = "(check-sat)" if self.debug_print: - print("> (check-sat)") + print(f"> {check_stmt}") if self.debug_file and not self.nocomments: print("; running check-sat..", file=self.debug_file) self.debug_file.flush() @@ -800,7 +814,7 @@ def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted for cache_stmt in cache_ctx: self.p_write(cache_stmt + "\n", False) - self.p_write("(check-sat)\n", True) + self.p_write(f"{check_stmt}\n", True) if self.timeinfo: i = 0 @@ -868,7 +882,7 @@ def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) - print("(check-sat)", file=self.debug_file) + print(check_stmt, file=self.debug_file) self.debug_file.flush() if result not in expected: @@ -945,6 +959,55 @@ def bv2bin(self, v): def bv2int(self, v): return int(self.bv2bin(v), 2) + def get_raw_unsat_assumptions(self): + if not self.smt2_assumptions: + return [] + self.write("(get-unsat-assumptions)") + exprs = set(self.unparse(part) for part in self.parse(self.read())) + unsat_assumptions = [] + for key, value in self.smt2_assumptions.items(): + # normalize expression + value = self.unparse(self.parse(value)) + if value in exprs: + exprs.remove(value) + unsat_assumptions.append(key) + return unsat_assumptions + + def get_unsat_assumptions(self, minimize=False): + if not minimize: + return self.get_raw_unsat_assumptions() + orig_assumptions = self.smt2_assumptions + + self.smt2_assumptions = dict(orig_assumptions) + + required_assumptions = {} + + while True: + candidate_assumptions = {} + for key in self.get_raw_unsat_assumptions(): + if key not in required_assumptions: + candidate_assumptions[key] = self.smt2_assumptions[key] + + while candidate_assumptions: + + candidate_key, candidate_assume = candidate_assumptions.popitem() + + self.smt2_assumptions = {} + for key, assume in candidate_assumptions.items(): + self.smt2_assumptions[key] = assume + for key, assume in required_assumptions.items(): + self.smt2_assumptions[key] = assume + result = self.check_sat() + + if result == 'unsat': + candidate_assumptions = None + else: + required_assumptions[candidate_key] = candidate_assume + + if candidate_assumptions is not None: + self.smt2_assumptions = orig_assumptions + return list(required_assumptions) + def get(self, expr): self.write("(get-value (%s))" % (expr)) return self.parse(self.read())[0][1] @@ -1091,7 +1154,7 @@ def wait(self): class SmtOpts: def __init__(self): self.shortopts = "s:S:v" - self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] + self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments", "smt2-option="] self.solver = "yices" self.solver_opts = list() self.debug_print = False @@ -1104,6 +1167,7 @@ def __init__(self): self.logic = None self.info_stmts = list() self.nocomments = False + self.smt2_options = {} def handle(self, o, a): if o == "-s": @@ -1130,6 +1194,13 @@ def handle(self, o, a): self.info_stmts.append(a) elif o == "--nocomments": self.nocomments = True + elif o == "--smt2-option": + args = a.split('=', 1) + if len(args) != 2: + print("--smt2-option expects an