diff --git a/.github/ISSUE_TEMPLATE/docs_report.yml b/.github/ISSUE_TEMPLATE/docs_report.yml new file mode 100644 index 000000000..aa65c63b9 --- /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 000000000..82daf609d --- /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 000000000..345b6db8a --- /dev/null +++ b/.github/actions/setup-build-env/action.yml @@ -0,0 +1,33 @@ +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 + + - 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 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 4a77d2234..24ae7c898 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 7c6409c1b..000000000 --- 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 000000000..d7c6e13ff --- /dev/null +++ b/.github/workflows/extra-builds.yml @@ -0,0 +1,97 @@ +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 000000000..375ea7fc5 --- /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-22.04 + compiler: 'clang-11' + 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++11 + shell: bash + run: | + make config-$CC_SHORT + make -j$procs CXXSTD=c++11 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-docs.yml b/.github/workflows/test-docs.yml deleted file mode 100644 index 00e5309bf..000000000 --- a/.github/workflows/test-docs.yml +++ /dev/null @@ -1,42 +0,0 @@ -name: Build and test doc code samples - -on: - pull_request: - branches: - - main - -jobs: - test-docs: - runs-on: ubuntu-latest - 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 python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev - - - name: Setup GCC - uses: Dup4/actions-setup-gcc@v1 - - - 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: Checkout Yosys - uses: actions/checkout@v3 - - - name: Build yosys - shell: bash - run: | - make config-gcc - make -j${{ env.procs }} - - - name: Run tests - shell: bash - run: | - make -C docs test -j${{ env.procs }} diff --git a/.github/workflows/test-linux.yml b/.github/workflows/test-linux.yml deleted file mode 100644 index c4441a884..000000000 --- a/.github/workflows/test-linux.yml +++ /dev/null @@ -1,130 +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: Store build artifact - if: (matrix.cpp_std == 'c++11') && (matrix.compiler == 'gcc-11') - uses: actions/upload-artifact@v4 - with: - name: compiled-yosys - path: yosys - - - 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 8ca658c39..000000000 --- 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: | - HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1 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 000000000..54d9487ac --- /dev/null +++ b/.github/workflows/test-verific.yml @@ -0,0 +1,95 @@ +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] + 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_CCACHE := 1" >> Makefile.conf + make -j${{ env.procs }} + + - name: Install Yosys + run: | + make install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX= + + - name: Checkout Documentation + if: ${{ github.ref == 'refs/heads/main' }} + uses: actions/checkout@v4 + with: + path: 'yosys-cmd-ref' + repository: 'YosysHQ-Docs/yosys-cmd-ref' + fetch-depth: 0 + token: ${{ secrets.CI_DOCS_UPDATE_PAT }} + persist-credentials: true + + - name: Update documentation + if: ${{ github.ref == 'refs/heads/main' }} + run: | + make docs + rm -rf docs/build + cd yosys-cmd-ref + rm -rf * + git checkout README.md + cp -R ../docs/* . + rm -rf util/__pycache__ + git add -A . + git diff-index --quiet HEAD || git commit -m "Update" + git push + + - 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 diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml new file mode 100644 index 000000000..1d4741c8c --- /dev/null +++ b/.github/workflows/update-flake-lock.yml @@ -0,0 +1,21 @@ +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: + pr-title: "Update flake.lock" # Title of PR to be created + pr-labels: | # Labels to be set on the PR + dependencies + automated \ No newline at end of file diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml index 47a7fe1a3..f73c68bdf 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 799c5f259..000000000 --- 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 d6d200d92..000000000 --- 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 @@ -263,45 +253,6 @@ CXX = g++ CXXFLAGS += -std=gnu++11 -Os 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" -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++ @@ -366,7 +317,7 @@ CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" else -$(error Invalid CONFIG setting '$(CONFIG)'. Valid values: clang, gcc, emcc, mxe, msys2-32, msys2-64, none) +$(error Invalid CONFIG setting '$(CONFIG)'. Valid values: clang, gcc, mxe, msys2-32, msys2-64, none) endif ifeq ($(ENABLE_LIBYOSYS),1) @@ -504,7 +455,7 @@ LIBS += -lpthread endif else ifeq ($(ABCEXTERNAL),) -TARGETS += $(PROGRAM_PREFIX)yosys-abc$(EXE) +TARGETS := $(PROGRAM_PREFIX)yosys-abc$(EXE) $(TARGETS) endif endif endif @@ -629,6 +580,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)) @@ -735,9 +687,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) @@ -788,41 +742,40 @@ $(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in -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: +.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:%h\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \ + echo "'abc' comes from a tarball. Continuing."; \ + exit 0; \ + elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && grep -q '\$$Format:%h\$$' "$(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 + +abc/abc$(EXE) abc/libabc.a: check-git-abc $(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; \ - 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) + $(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) -ifeq ($(ABCREV),default) -.PHONY: abc/abc-$(ABCREV)$(EXE) -.PHONY: abc/libabc-$(ABCREV).a -endif +$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc$(EXE) + $(P) cp $< $(PROGRAM_PREFIX)yosys-abc$(EXE) -$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE) - $(P) cp abc/abc-$(ABCREV)$(EXE) $(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)" @@ -984,16 +937,33 @@ docs/gen_images: $(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 -# many of these will return an error which can be safely ignored, so we prefix -# the command with a '-' -DOCS_USAGE_PROGS := yosys yosys-config yosys-filterlib yosys-abc yosys-smtbmc yosys-witness -docs/usage: $(addprefix docs/source/temp/,$(DOCS_USAGE_PROGS)) -docs/source/temp/%: docs/guidelines - -$(Q) ./$(PROGRAM_PREFIX)$* --help > $@ 2>&1 +# some commands return an error and print the usage text to stderr +define DOC_USAGE_STDERR +docs/source/generated/$(1): $(PROGRAM_PREFIX)$(1) docs/source/generated + -$(Q) ./$$< --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): $(PROGRAM_PREFIX)$(1) docs/source/generated + $(Q) ./$$< --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 @@ -1017,7 +987,9 @@ 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 clean + -$(MAKE) -C docs/images clean + rm -rf docs/source/cmd docs/util/__pycache__ clean-abc: $(MAKE) -C abc DEP= clean @@ -1033,11 +1005,12 @@ 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} @@ -1080,14 +1053,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 @@ -1129,9 +1094,6 @@ echo-yosys-ver: echo-git-rev: @echo "$(GIT_REV)" -echo-abc-rev: - @echo "$(ABCREV)" - echo-cxx: @echo "$(CXX)" diff --git a/abc b/abc new file mode 160000 index 000000000..237d81397 --- /dev/null +++ b/abc @@ -0,0 +1 @@ +Subproject commit 237d81397fcc85dd3894bf1a449d2955cd3df02d diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 877a829d3..9ddbd33b0 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())); @@ -2275,46 +2283,92 @@ struct CxxrtlWorker { dec_indent(); } - 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) << ")"; - } - f << " },\n"; + 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; } - dec_indent(); - f << 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; + } + 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_debug_attrs(const RTLIL::AttrObject *object) + void dump_metadata_map(const dict &metadata_map) { + if (metadata_map.empty()) { + f << "metadata_map()"; + } 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"; + } + dec_indent(); + f << indent << "})"; + } + } + + 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 << "debug_item::" << flag; - } - 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 << ");\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/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h index b834cd120..057d34cf9 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); } diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index b8233b007..9aa3e105d 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -512,9 +512,10 @@ public: 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/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e6b4088db..995a714c9 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -199,7 +199,6 @@ def help(): --minimize-assumes when using --track-assumes, solve for a minimal set of sufficient assumptions. - """ + so.helpmsg()) def usage(): @@ -670,18 +669,12 @@ if aimfile is not None: 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) @@ -692,9 +685,128 @@ 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 + return ywfile_hierwitness_cache + +def_bits_re = re.compile(r'([01]+)') + +def smt_extract_mask(smt_expr, mask): + chunks = [] + def_bits = '' + + mask_index_order = mask[::-1] + + for matched in def_bits_re.finditer(mask_index_order): + chunks.append(matched.span()) + def_bits += matched[0] + + if not chunks: + return + + 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) + )) + + return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1] + +def smt_concat(exprs): + if not exprs: + return "" + if len(exprs) == 1: + return exprs[1] + return "(concat %s)" % ' '.join(exprs) + +def ywfile_signal(sig, step, mask=None): + assert sig.width > 0 + + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + sig_end = sig.offset + sig.width + + output = [] + + if sig.path in smt_wires: + for wire in smt_wires[sig.path]: + width, offset = wire["width"], wire["offset"] + + smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + + offset = max(offset, 0) + + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue + + smt_expr = smt.witness_net_expr(topmod, f"s{step}", wire) + + 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 + + output.append(((common_offset - sig.offset), (common_end - sig.offset), smt_expr)) + + 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(): @@ -706,77 +818,14 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): if not bits_re.match(bits): raise ValueError("unsupported bit value in Yosys witness file") - 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"] + smt_expr = ywfile_signal(sig, map_steps.get(t, t)) - smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + smt_expr, bits = smt_extract_mask(smt_expr, bits) - offset = max(offset, 0) + smt_constr = "(= %s #b%s)" % (smt_expr, bits) + constr_assumes[t].append((inywfile, smt_constr)) - end = width + offset - common_offset = max(sig.offset, offset) - common_end = min(sig_end, end) - if common_end <= common_offset: - continue - - smt_expr = smt.witness_net_expr(topmod, f"s{map_steps.get(t, t)}", wire) - - 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) - - bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] - - if bit_slice.count("?") == len(bit_slice): - continue - - 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) - - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - - constr_assumes[t].append((inywfile, smt_constr)) - - 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{map_steps.get(t, t)}", 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 len(bits) < width: - slice_high = sig.offset + len(bits) - 1 - smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) - - bit_slice = bits - - 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) - - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - constr_assumes[t].append((inywfile, smt_constr)) max_t = t - return max_t if inywfile is not None: @@ -1367,11 +1416,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 diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index f43e878f3..0bd280b4a 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 @@ -34,6 +34,7 @@ class Incremental: self._witness_index = None self._yw_constraints = {} + self._define_sorts = {} def setup(self): generic_assert_map = smtbmc.get_assert_map( @@ -175,11 +176,7 @@ class Incremental: 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:]: @@ -189,7 +186,51 @@ class Incremental: 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] @@ -219,6 +260,40 @@ class Incremental: 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) @@ -231,10 +306,15 @@ class Incremental: 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 @@ -258,6 +338,14 @@ class Incremental: 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, @@ -270,8 +358,15 @@ class Incremental: "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, } @@ -305,10 +400,13 @@ class Incremental: 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) @@ -338,7 +436,6 @@ class Incremental: expr = cmd.get("expr") key = cmd.get("key") - key = mkkey(key) result = smtbmc.smt.smt2_assumptions.pop(key, None) @@ -348,7 +445,7 @@ class Incremental: return result def cmd_get_unsat_assumptions(self, cmd): - return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get('minimize'))) + return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get("minimize"))) def cmd_push(self, cmd): smtbmc.smt_push() @@ -370,6 +467,27 @@ class Incremental: 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)) if self._cached_hierwitness[allregs] is not None: @@ -451,6 +569,7 @@ class Incremental: "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, diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e32f43c60..5fc3ab5a4 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -160,6 +160,7 @@ class SmtIo: 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" @@ -959,6 +960,8 @@ class SmtIo: 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 = [] @@ -973,6 +976,10 @@ class SmtIo: 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: @@ -998,6 +1005,7 @@ class SmtIo: 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): @@ -1146,7 +1154,7 @@ class SmtIo: 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 @@ -1159,6 +1167,7 @@ class SmtOpts: self.logic = None self.info_stmts = list() self.nocomments = False + self.smt2_options = {} def handle(self, o, a): if o == "-s": @@ -1185,6 +1194,13 @@ class SmtOpts: 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