diff --git a/README.md b/README.md index 75ad2239398..02de03d5d70 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,36 @@ +# ORCA Special Edition +This version of VTR is modified by @xilai based on the official version `79a5bc8d163ce15aa195a84459f6350690e1fbf5`. I changed the default compiler, updated Python packages, and updated Yosys and Parmys to fit our purpose. This is tested on ORCA. + +## Setup +1. Install build tools and Python packages. On July 22, 2023, I updated the build tools on ORCA, so if anyone needs to install them on ORCA, there's no need to do it again. (You still need to install python packages) + +``` +# some cmds to create a new python environment. I used conda, and it works well, and the official VTR project uses venv, so both should work. +sudo ./install_apt_packages.sh +pip install -U -r requirements.txt +``` + +2. Compile and verify functionality. +``` +make CMAKE_PARAMS="-DWITH_PARMYS=ON -DYOSYS_F4PGA_PLUGINS=ON -DYOSYS_PARMYS_PLUGIN=ON" +./vtr_flow/scripts/run_vtr_task.py regression_tests/vtr_reg_basic/basic_timing +``` + +The expected output is: +``` +k6_N10_mem32K_40nm/single_ff OK +k6_N10_mem32K_40nm/single_ff OK +k6_N10_mem32K_40nm/single_wire OK +k6_N10_mem32K_40nm/single_wire OK +k6_N10_mem32K_40nm/diffeq1 OK +k6_N10_mem32K_40nm/diffeq1 OK +k6_N10_mem32K_40nm/ch_intrinsics OK +k6_N10_mem32K_40nm/ch_intrinsics OK +``` + +## Special Notes +- F4PGA is currently incompatible with the latest version of Yosys (see issue [here](https://github.com/chipsalliance/yosys-f4pga-plugins/issues/552)); manually downgraded to match the [previous fork](https://github.com/abdelfattah-lab/vtr-verilog-to-routing)'s version. Upgrade when the issue is fixed. + # Verilog to Routing (VTR) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-Ready--to--Code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/verilog-to-routing/vtr-verilog-to-routing.git) [![Build Status](https://github.com/verilog-to-routing/vtr-verilog-to-routing/workflows/Test/badge.svg)](https://github.com/verilog-to-routing/vtr-verilog-to-routing/actions?query=workflow%3ATest) [![Documentation Status](https://readthedocs.org/projects/vtr/badge/?version=latest)](http://docs.verilogtorouting.org/en/latest/) diff --git a/build-instruction-custom.txt b/build-instruction-custom.txt new file mode 100644 index 00000000000..5688fc9bc98 --- /dev/null +++ b/build-instruction-custom.txt @@ -0,0 +1,35 @@ +All changes have already been made, and only run this command to compile the code: +# first (create a new virtual environment and) install python libs in requirements.txt +# build with new Parmys + Yosys frontend +make CMAKE_PARAMS="-DWITH_PARMYS=ON -DYOSYS_F4PGA_PLUGINS=ON -DYOSYS_PARMYS_PLUGIN=ON" + + + + + +@change log: +requirements.txt: + update click to newer version as the bug has alerady been fixed +yosys/Makefile: + change default compiler to gcc as clang does not work well on ORCA +libs/EXTERNAL/CMakeLists.txt: + update to fix system verilog parser bug + update Surelog to version 0f9cf823158bf626c8ebbbb29d7685bd7b1592fc + update f4pga-plugins to version 73038124b0a2943fe9d591c43f46292bcbf82105 +vtr_flow/scripts/run_vtr_flow.py, vtr_flow/scripts/python_libs/vtr/parmys/parmys.py: + add support for top module and search path + + + + + + +@other misc for reminder: + +alias: +vtrc: activate vtr conda env +vtrf: run_vtr_flow +vtrt: run_vtr_task + +flow: +vtrf \ No newline at end of file diff --git a/vtr_flow/misc/yosys/synthesis.tcl b/vtr_flow/misc/yosys/synthesis.tcl index 5015d587055..3850330ac7c 100644 --- a/vtr_flow/misc/yosys/synthesis.tcl +++ b/vtr_flow/misc/yosys/synthesis.tcl @@ -26,10 +26,10 @@ if {$env(PARSER) == "surelog" } { puts "Using Yosys read_systemverilog command" plugin -i systemverilog yosys -import - read_systemverilog XXX + read_systemverilog -I"SEARCHPATH" -debug XXX } elseif {$env(PARSER) == "default" } { puts "Using Yosys read_verilog command" - read_verilog -sv -nolatches XXX + read_verilog -I"SEARCHPATH" -sv -nolatches XXX } else { error "Invalid PARSER" } @@ -39,7 +39,7 @@ scc -select select -assert-none % select -clear -hierarchy -check -auto-top -purge_lib +hierarchy -check TOPMODULE -purge_lib opt_expr opt_clean @@ -80,6 +80,6 @@ opt -fast -noff stat -hierarchy -check -auto-top -purge_lib +hierarchy -check TOPMODULE -purge_lib write_blif -true + vcc -false + gnd -undef + unconn -blackbox ZZZ diff --git a/vtr_flow/scripts/python_libs/vtr/parmys/parmys.py b/vtr_flow/scripts/python_libs/vtr/parmys/parmys.py index cef45626828..381d7151eb3 100644 --- a/vtr_flow/scripts/python_libs/vtr/parmys/parmys.py +++ b/vtr_flow/scripts/python_libs/vtr/parmys/parmys.py @@ -53,6 +53,8 @@ def init_script_file( output_netlist, architecture_file_path, odin_config_full_path, + include_dir='.', + top_module='-auto-top' ): """initializing the raw yosys script file""" # specify the input files type @@ -70,6 +72,8 @@ def init_script_file( "CCC": odin_config_full_path, "ZZZ": output_netlist, "QQQ": architecture_file_path, + "SEARCHPATH": include_dir, + "TOPMODULE": top_module, }, ) @@ -207,6 +211,22 @@ def run( # Create a list showing all (.v) and (.vh) files circuit_list = create_circuits_list(circuit_file, include_files) + # parse search directory + if ('searchpath' in parmys_args): + if (parmys_args['searchpath'] is not None) and (parmys_args['searchpath'] != ''): + include_dir = parmys_args['searchpath'] + del parmys_args['searchpath'] + else: + include_dir = '.' + + # parse top module + # NOTE: the default value is '-auto-top' + top_module = '-auto-top' + if ('topmodule' in parmys_args): + if (parmys_args['topmodule'] is not None) and (parmys_args['topmodule'] != ''): + top_module = '-top ' + parmys_args['topmodule'] + del parmys_args['topmodule'] + odin_base_config = str(vtr.paths.odin_cfg_path) # Copy the config file @@ -230,6 +250,8 @@ def run( output_netlist.name, architecture_file_path, odin_config_full_path, + include_dir=include_dir, + top_module=top_module ) # set the parser diff --git a/vtr_flow/scripts/run_vtr_flow.py b/vtr_flow/scripts/run_vtr_flow.py index 3d584274e3f..91359bfab20 100755 --- a/vtr_flow/scripts/run_vtr_flow.py +++ b/vtr_flow/scripts/run_vtr_flow.py @@ -2,6 +2,7 @@ """ Module to run the VTR Flow """ + import sys from pathlib import Path import argparse @@ -11,11 +12,10 @@ from datetime import datetime from collections import OrderedDict import os - +import os # pylint: disable=wrong-import-position, import-error sys.path.insert(0, str(Path(__file__).resolve().parent / "python_libs")) import vtr - # pylint: enable=wrong-import-position, import-error BASIC_VERBOSITY = 1 @@ -23,6 +23,8 @@ VTR_STAGES = ["odin", "parmys", "abc", "ace", "vpr"] # pylint: disable=too-few-public-methods + + class VtrStageArgparseAction(argparse.Action): """ Class to parse the VTR stages to begin and end at. @@ -370,6 +372,18 @@ def vtr_command_argparser(prog=None): + "system-verilog]. The script used the Yosys conventional Verilog" + " parser if this argument is not specified.", ) + parmys.add_argument( + "-top", + default=None, + dest="topmodule", + help="Specify the name of the module in the design that should be considered as top", + ) + parmys.add_argument( + '-search', + default=os.getcwd(), + dest='searchpath', + help='search path for verilog files' + ) # # VPR arguments # @@ -732,7 +746,8 @@ def process_parmys_args(args): """ parmys_args = OrderedDict() parmys_args["parser"] = args.parser - + parmys_args["topmodule"] = args.topmodule + parmys_args['searchpath'] = args.searchpath return parmys_args diff --git a/yosys/.gitcommit b/yosys/.gitcommit index 6c5826ed776..46b7856fbc8 100644 --- a/yosys/.gitcommit +++ b/yosys/.gitcommit @@ -1 +1 @@ -dac5bd1983a +$Format:%h$ diff --git a/yosys/.github/ISSUE_TEMPLATE/bug_report.yml b/yosys/.github/ISSUE_TEMPLATE/bug_report.yml index e4c776ed914..27cfd09b7de 100644 --- a/yosys/.github/ISSUE_TEMPLATE/bug_report.yml +++ b/yosys/.github/ISSUE_TEMPLATE/bug_report.yml @@ -34,7 +34,6 @@ body: - macOS - Windows - BSD - - WebAssembly multiple: true validations: required: true @@ -43,7 +42,7 @@ body: attributes: value: > When providing steps to reproduce the issue, please ensure that the issue - is reproducible in the current git main of Yosys. Also ensure to + is reproducible in the current git master of Yosys. Also ensure to provide all necessary source files needed. diff --git a/yosys/.github/ISSUE_TEMPLATE/docs_report.yml b/yosys/.github/ISSUE_TEMPLATE/docs_report.yml deleted file mode 100644 index aa65c63b9c9..00000000000 --- a/yosys/.github/ISSUE_TEMPLATE/docs_report.yml +++ /dev/null @@ -1,55 +0,0 @@ -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/yosys/.github/PULL_REQUEST_TEMPLATE.md b/yosys/.github/PULL_REQUEST_TEMPLATE.md deleted file mode 100644 index 82daf609d36..00000000000 --- a/yosys/.github/PULL_REQUEST_TEMPLATE.md +++ /dev/null @@ -1,5 +0,0 @@ -_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/yosys/.github/actions/setup-build-env/action.yml b/yosys/.github/actions/setup-build-env/action.yml deleted file mode 100644 index 345b6db8ada..00000000000 --- a/yosys/.github/actions/setup-build-env/action.yml +++ /dev/null @@ -1,33 +0,0 @@ -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/yosys/.github/workflows/codeql.yml b/yosys/.github/workflows/codeql.yml index 24ae7c89883..2a046703bc0 100644 --- a/yosys/.github/workflows/codeql.yml +++ b/yosys/.github/workflows/codeql.yml @@ -14,11 +14,10 @@ jobs: run: sudo apt-get install bison flex libreadline-dev tcl-dev libffi-dev - name: Checkout repository - uses: actions/checkout@v4 - with: - submodules: true + uses: actions/checkout@v3 + - name: Initialize CodeQL - uses: github/codeql-action/init@v3 + uses: github/codeql-action/init@v2 with: languages: cpp queries: security-extended,security-and-quality @@ -27,4 +26,4 @@ jobs: run: make yosys -j6 - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@v3 + uses: github/codeql-action/analyze@v2 diff --git a/yosys/.github/workflows/emcc.yml b/yosys/.github/workflows/emcc.yml new file mode 100644 index 00000000000..295d9554b81 --- /dev/null +++ b/yosys/.github/workflows/emcc.yml @@ -0,0 +1,18 @@ +name: Emscripten Build + +on: [push, pull_request] + +jobs: + emcc: + runs-on: ubuntu-latest + steps: + - uses: mymindstorm/setup-emsdk@v11 + - uses: actions/checkout@v3 + - name: Build + run: | + make config-emcc + make YOSYS_VER=latest + - uses: actions/upload-artifact@v3 + with: + name: yosysjs + path: yosysjs-latest.zip diff --git a/yosys/.github/workflows/extra-builds.yml b/yosys/.github/workflows/extra-builds.yml deleted file mode 100644 index d7c6e13ff06..00000000000 --- a/yosys/.github/workflows/extra-builds.yml +++ /dev/null @@ -1,97 +0,0 @@ -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/yosys/.github/workflows/test-compile.yml b/yosys/.github/workflows/test-compile.yml deleted file mode 100644 index a892c91ceca..00000000000 --- a/yosys/.github/workflows/test-compile.yml +++ /dev/null @@ -1,79 +0,0 @@ -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++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/yosys/.github/workflows/test-linux.yml b/yosys/.github/workflows/test-linux.yml new file mode 100644 index 00000000000..eee556794af --- /dev/null +++ b/yosys/.github/workflows/test-linux.yml @@ -0,0 +1,116 @@ +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 + 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@v3 + + - name: Get iverilog + shell: bash + run: | + git clone https://github.com/steveicarus/iverilog.git + + - name: Cache iverilog + id: cache-iverilog + uses: actions/cache@v3 + with: + path: .local/ + key: ${{ matrix.os.id }}-${{ hashFiles('iverilog/.git/refs/heads/master') }} + + - 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 }} CCXXSTD=${{ 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 diff --git a/yosys/.github/workflows/test-macos.yml b/yosys/.github/workflows/test-macos.yml new file mode 100644 index 00000000000..04845723467 --- /dev/null +++ b/yosys/.github/workflows/test-macos.yml @@ -0,0 +1,73 @@ +name: Build and run tests (macOS) + +on: [push, pull_request] + +jobs: + test-macos: + runs-on: ${{ matrix.os.id }} + strategy: + matrix: + os: + - { id: macos-11, name: 'Big Sur' } + 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@v3 + + - name: Get iverilog + shell: bash + run: | + git clone https://github.com/steveicarus/iverilog.git + + - name: Cache iverilog + id: cache-iverilog + uses: actions/cache@v3 + with: + path: .local/ + key: ${{ matrix.os.id }}-${{ hashFiles('iverilog/.git/refs/heads/master') }} + + - 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/yosys/.github/workflows/test-verific.yml b/yosys/.github/workflows/test-verific.yml deleted file mode 100644 index 54d9487acfb..00000000000 --- a/yosys/.github/workflows/test-verific.yml +++ /dev/null @@ -1,95 +0,0 @@ -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/yosys/.github/workflows/update-flake-lock.yml b/yosys/.github/workflows/update-flake-lock.yml deleted file mode 100644 index c7aa6ecab70..00000000000 --- a/yosys/.github/workflows/update-flake-lock.yml +++ /dev/null @@ -1,22 +0,0 @@ -name: update-flake-lock -on: - workflow_dispatch: # allows manual triggering - schedule: - - cron: '0 0 * * 0' # runs weekly on Sunday at 00:00 - -jobs: - lockfile: - 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/yosys/.github/workflows/version.yml b/yosys/.github/workflows/version.yml index f73c68bdf12..c2a1756e9c6 100644 --- a/yosys/.github/workflows/version.yml +++ b/yosys/.github/workflows/version.yml @@ -10,10 +10,9 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout - uses: actions/checkout@v4 + uses: actions/checkout@v3 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/yosys/.github/workflows/vs.yml b/yosys/.github/workflows/vs.yml new file mode 100644 index 00000000000..428770e7200 --- /dev/null +++ b/yosys/.github/workflows/vs.yml @@ -0,0 +1,31 @@ +name: Visual Studio Build + +on: [push, pull_request] + +jobs: + yosys-vcxsrc: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + - name: Build + run: make vcxsrc YOSYS_VER=latest + - uses: actions/upload-artifact@v3 + with: + name: vcxsrc + path: yosys-win32-vcxsrc-latest.zip + + build: + runs-on: windows-2019 + needs: yosys-vcxsrc + steps: + - uses: actions/download-artifact@v3 + 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/yosys/.gitignore b/yosys/.gitignore index e82343e8947..49b886e7e43 100644 --- a/yosys/.gitignore +++ b/yosys/.gitignore @@ -1,11 +1,9 @@ *.o *.d -*.dwo .*.swp *.gch *.gcda *.gcno -*~ __pycache__ /.cproject /.project @@ -18,6 +16,7 @@ __pycache__ /coverage.info /coverage_html /Makefile.conf +/abc /viz.js /yosys /yosys.exe @@ -45,4 +44,3 @@ __pycache__ /tests/unit/bintest/ /tests/unit/objtest/ /tests/ystests -/result \ No newline at end of file diff --git a/yosys/.gitmodules b/yosys/.gitmodules deleted file mode 100644 index d88d4b1e5e9..00000000000 --- a/yosys/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "abc"] - path = abc - url = https://github.com/YosysHQ/abc diff --git a/yosys/CHANGELOG b/yosys/CHANGELOG index d8e13b041e5..585605abcdd 100644 --- a/yosys/CHANGELOG +++ b/yosys/CHANGELOG @@ -2,177 +2,6 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.42 .. Yosys 0.43-dev --------------------------- - -Yosys 0.41 .. Yosys 0.42 --------------------------- - * New commands and options - - Added "box_derive" pass to derive box modules. - - Added option "assert-mod-count" to "select" pass. - - Added option "-header","-push" and "-pop" to "log" pass. - * Intel support - - Dropped Quartus support in "synth_intel_alm" pass. - -Yosys 0.40 .. Yosys 0.41 --------------------------- - * New commands and options - - Added "cellmatch" pass for picking out standard cells automatically. - - * Various - - Extended the experimental incremental JSON API to allow arbitrary - smtlib subexpressions. - - Added support for using ABCs library merging when providing multiple - liberty files. - - * Verific support - - Expose library name as module attribute. - -Yosys 0.39 .. Yosys 0.40 --------------------------- - * New commands and options - - Added option "-vhdl2019" to "read" and "verific" pass. - - * Various - - Major documentation overhaul. - - Added port statistics to "stat" command. - - Added new formatting features to cxxrtl backend. - - * Verific support - - Added better support for VHDL constants import. - - Added support for VHDL 2009. - -Yosys 0.38 .. Yosys 0.39 --------------------------- - * New commands and options - - Added option "-extra-map" to "synth" pass. - - Added option "-dont_use" to "dfflibmap" pass. - - Added option "-href" to "show" command. - - Added option "-noscopeinfo" to "flatten" pass. - - Added option "-scopename" to "flatten" pass. - - * SystemVerilog - - Added support for packed multidimensional arrays. - - * Various - - Added "$scopeinfo" cells to preserve information about - the hierarchy during flattening. - - Added sequential area output to "stat -liberty". - - Added ability to record/replay diagnostics in cxxrtl backend. - - * Verific support - - Added attributes to module instantiation. - -Yosys 0.37 .. Yosys 0.38 --------------------------- - * New commands and options - - Added option "-tech" to "opt_lut" pass. - - Added option "-nokeep_prints" to "hierarchy" pass. - - Added option "-nolower" to "async2sync" and "clk2fflogic" pass. - - Added option "-lower" to "chformal" pass. - - * Various - - Added $check cell to represent assertions with messages. - - Allow capturing $print cell output in CXXRTL. - - Added API to overwrite existing pass from plugin. - - Follow the XDG Base Directory Specification for storing history files. - - Without a known top module, derive all deferred modules (hierarchy pass). - - Detect and error out on combinational loops in write_aiger. - - * Verific support - - Added option "-no-split-complex-ports" to "verific -import". - -Yosys 0.36 .. Yosys 0.37 --------------------------- - * New commands and options - - Added option "-nodisplay" to read_verilog. - - * SystemVerilog - - Correct hierarchical path names for structs and unions. - - * Various - - Print hierarchy for failed assertions in "sim" pass. - - Add "--present-only" option to "yosys-witness" to omit unused signals. - - Implement a generic record/replay interface for CXXRTL. - - Improved readability of emitted code with "write_verilog". - -Yosys 0.35 .. Yosys 0.36 --------------------------- - * New commands and options - - Added option "--" to pass arguments down to tcl when using -c option. - - Added ability on MacOS and Windows to pass options after arguments on cli. - - Added option "-cmp2softlogic" to synth_lattice. - - Added option "-lowpower" to "booth" pass. - - * QuickLogic support - - Added "K6N10f" support. - - Added "-nodsp", "-nocarry", "-nobram" and "-bramtypes" options to - "synth_quicklogic" pass. - - Added "ql_bram_merge" pass to merge 18K BRAM cells into TDP36K. - - Added "ql_bram_types" pass to change TDP36K depending on configuration. - - Added "ql_dsp_io_regs" pass to update QL_DSP2 depending on configuration. - - Added "ql_dsp_macc" pass to infer multiplier-accumulator DSP cells. - - Added "ql_dsp_simd" pass to merge DSP pairs to operate in SIMD mode. - - * ECP5,iCE40 and Gowin support - - Enabled abc9 by default, added "-noabc9" option to disable. - - * MachXO3 support - - Quality of results improvements. - - Enabled "booth" pass by default for it in "synth_lattice". - - * Various - - Improved "peepopt" by adding shiftadd pattern support. - - Added "--incremental" mode to smtbmc. - -Yosys 0.34 .. Yosys 0.35 --------------------------- - * Various - - Improvements on "peepopt" shiftmul matcher. - - Improvements on "ram_style" attributes handling. - - * Verific support - - Improved static elaboration for VHDL and mixed HDL designs. - - Expose "hdlname" attribute with original module name. - - Expose "architecture" attribute with VHDL architecture name. - -Yosys 0.33 .. Yosys 0.34 --------------------------- - * New commands and options - - Added option "-assert" to "sim" pass. - - Added option "-noinitstate" to "sim" pass. - - Added option "-dont_use" to "abc" pass. - - Added "dft_tag" pass to create tagging logic for data flow tracking. - - Added "future" pass to resolve future sampled value functions. - - Added "booth" pass to map $mul cells to Booth multipliers. - - Added option "-booth" to "synth" pass. - - * SystemVerilog - - Added support for assignments within expressions, e.g., `x[y++] = z;` or - `x = (y *= 2) - 1;`. - - * Verific support - - "src" attribute contain full location info. - - module parameters are kept after import. - - accurate access order semantics in memory inference. - - better "bind" support for mixed language projects. - - * Various - - "show" command displays dot instead of box for wire aliases. - -Yosys 0.32 .. Yosys 0.33 --------------------------- - * Various - - Added "$print" cell, produced by "$display" and "$write" - Verilog tasks. - - Added "$print" cell handling in CXXRTL. - - * Lattice FPGA support - - Added generic "synth_lattice" pass (for now MachXO2/XO3/XO3D) - - Removed "synth_machxo2" pass - - Pass "ecp5_gsr" renamed to "lattice_gsr" - - "synth_machxo2" equivalent is "synth_lattice -family xo2" - Yosys 0.31 .. Yosys 0.32 -------------------------- * Verific support diff --git a/yosys/CMakeLists.txt b/yosys/CMakeLists.txt index 455e575cc99..dd13b7c49ae 100644 --- a/yosys/CMakeLists.txt +++ b/yosys/CMakeLists.txt @@ -20,7 +20,7 @@ add_custom_command(OUTPUT yosys-bin # -C ${CMAKE_CURRENT_BINARY_DIR} # -f ${CMAKE_CURRENT_SOURCE_DIR}/Makefile #(out-of-tree) build directory PREFIX=${CMAKE_BINARY_DIR} -# -j${CUSTOM_BUILD_PARALLEL_LEVEL} + -j${CUSTOM_BUILD_PARALLEL_LEVEL} > /dev/null COMMAND ${MAKE_PROGRAM} install ENABLE_ABC=0 @@ -43,4 +43,4 @@ add_custom_target(yosys ALL DEPENDS yosys-bin) # INTERFACE_INCLUDE_DIRECTORIES ${YOSYS_INCLUDE_DIRS}) -#install(FILES ${BINARY_LIB_FILE1} DESTINATION ${CMAKE_CURRENT_BINARY_DIR}) +#install(FILES ${BINARY_LIB_FILE1} DESTINATION ${CMAKE_CURRENT_BINARY_DIR}) \ No newline at end of file diff --git a/yosys/CODEOWNERS b/yosys/CODEOWNERS index 879bb8dee21..a33a9a68ccb 100644 --- a/yosys/CODEOWNERS +++ b/yosys/CODEOWNERS @@ -10,7 +10,6 @@ # PATH (can use glob) USERNAME(S) -CODEOWNERS @nakengelhardt passes/cmds/scratchpad.cc @nakengelhardt frontends/rpc/ @whitequark backends/cxxrtl/ @whitequark @@ -19,8 +18,7 @@ passes/techmap/flowmap.cc @whitequark passes/opt/opt_lut.cc @whitequark passes/techmap/abc9*.cc @eddiehung @Ravenslofty backends/aiger/xaiger.cc @eddiehung -docs/ @KrystalDelusion -.github/workflows/*.yml @mmicko + ## External Contributors # Only users with write permission to the repository get review diff --git a/yosys/Makefile b/yosys/Makefile index 313de44d56d..144c9888341 100644 --- a/yosys/Makefile +++ b/yosys/Makefile @@ -1,8 +1,8 @@ -CONFIG := none -# CONFIG := clang +CONFIG := gcc # CONFIG := gcc # CONFIG := afl-gcc +# CONFIG := emcc # CONFIG := wasi # CONFIG := mxe # CONFIG := msys2-32 @@ -17,12 +17,10 @@ ENABLE_READLINE := 1 ENABLE_EDITLINE := 0 ENABLE_GHDL := 0 ENABLE_VERIFIC := 0 -ENABLE_VERIFIC_SYSTEMVERILOG := 1 -ENABLE_VERIFIC_VHDL := 1 -ENABLE_VERIFIC_HIER_TREE := 1 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1 ENABLE_VERIFIC_EDIF := 0 ENABLE_VERIFIC_LIBERTY := 0 +DISABLE_VERIFIC_EXTENSIONS := 0 +DISABLE_VERIFIC_VHDL := 0 ENABLE_COVER := 1 ENABLE_LIBYOSYS := 0 ENABLE_ZLIB := 1 @@ -92,16 +90,16 @@ all: top-all YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST))) VPATH := $(YOSYS_SRC) -CXXSTD ?= c++17 +CXXSTD ?= c++11 CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include -LIBS := $(LIBS) -lstdc++ -lm -PLUGIN_LINKFLAGS := -PLUGIN_LIBS := -EXE_LINKFLAGS := +LDLIBS := $(LDLIBS) -lstdc++ -lm +PLUGIN_LDFLAGS := +PLUGIN_LDLIBS := +EXE_LDFLAGS := ifeq ($(OS), MINGW) -EXE_LINKFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a -PLUGIN_LINKFLAGS += -L"$(LIBDIR)" -PLUGIN_LIBS := -lyosys_exe +EXE_LDFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a +PLUGIN_LDFLAGS += -L"$(LIBDIR)" +PLUGIN_LDLIBS := -lyosys_exe endif PKG_CONFIG ?= pkg-config @@ -111,7 +109,7 @@ STRIP ?= strip AWK ?= awk ifeq ($(OS), Darwin) -PLUGIN_LINKFLAGS += -undefined dynamic_lookup +PLUGIN_LDFLAGS += -undefined dynamic_lookup # homebrew search paths ifneq ($(shell :; command -v brew),) @@ -119,10 +117,10 @@ BREW_PREFIX := $(shell brew --prefix)/opt $(info $$BREW_PREFIX is [${BREW_PREFIX}]) ifeq ($(ENABLE_PYOSYS),1) CXXFLAGS += -I$(BREW_PREFIX)/boost/include/boost -LINKFLAGS += -L$(BREW_PREFIX)/boost/lib +LDFLAGS += -L$(BREW_PREFIX)/boost/lib endif CXXFLAGS += -I$(BREW_PREFIX)/readline/include -LINKFLAGS += -L$(BREW_PREFIX)/readline/lib +LDFLAGS += -L$(BREW_PREFIX)/readline/lib PKG_CONFIG_PATH := $(BREW_PREFIX)/libffi/lib/pkgconfig:$(PKG_CONFIG_PATH) PKG_CONFIG_PATH := $(BREW_PREFIX)/tcl-tk/lib/pkgconfig:$(PKG_CONFIG_PATH) export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX)/flex/bin:$(PATH) @@ -131,19 +129,19 @@ export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX else ifneq ($(shell :; command -v port),) PORT_PREFIX := $(patsubst %/bin/port,%,$(shell :; command -v port)) CXXFLAGS += -I$(PORT_PREFIX)/include -LINKFLAGS += -L$(PORT_PREFIX)/lib +LDFLAGS += -L$(PORT_PREFIX)/lib PKG_CONFIG_PATH := $(PORT_PREFIX)/lib/pkgconfig:$(PKG_CONFIG_PATH) export PATH := $(PORT_PREFIX)/bin:$(PATH) endif else -LINKFLAGS += -rdynamic +LDFLAGS += -rdynamic ifneq ($(OS), OpenBSD) -LIBS += -lrt +LDLIBS += -lrt endif endif -YOSYS_VER := 0.42+40 +YOSYS_VER := 0.32 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -159,8 +157,17 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 9b6afcf.. | wc -l`/;" Makefile - +# sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline f3c6b41.. | wc -l`/;" Makefile + +# set 'ABCREV = default' to use abc/ as it is +# +# Note: If you do ABC development, make sure that 'abc' in this directory +# is just a symlink to your actual ABC working directory, as 'make mrproper' +# will remove the 'abc' directory and you do not want to accidentally +# delete your work on ABC.. +ABCREV = bb64142 +ABCPULL = 1 +ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) # set ABCEXTERNAL = to use an external ABC instance @@ -208,38 +215,41 @@ ABC_ARCHFLAGS += "-DABC_NO_RLIMIT" endif ifeq ($(CONFIG),clang) -CXX = clang++ +CXX = clang +LD = clang++ CXXFLAGS += -std=$(CXXSTD) -Os -ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" +ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -Wno-c++11-narrowing $(ABC_ARCHFLAGS)" ifneq ($(SANITIZER),) $(info [Clang Sanitizer] $(SANITIZER)) CXXFLAGS += -g -O1 -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize=$(SANITIZER) -LINKFLAGS += -g -fsanitize=$(SANITIZER) +LDFLAGS += -g -fsanitize=$(SANITIZER) ifneq ($(findstring address,$(SANITIZER)),) ENABLE_COVER := 0 endif ifneq ($(findstring memory,$(SANITIZER)),) CXXFLAGS += -fPIE -fsanitize-memory-track-origins -LINKFLAGS += -fPIE -fsanitize-memory-track-origins +LDFLAGS += -fPIE -fsanitize-memory-track-origins endif ifneq ($(findstring cfi,$(SANITIZER)),) CXXFLAGS += -flto -LINKFLAGS += -flto +LDFLAGS += -flto endif endif else ifeq ($(CONFIG),gcc) -CXX = g++ +CXX = gcc +LD = gcc CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" else ifeq ($(CONFIG),gcc-static) -LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -static -LIBS := $(filter-out -lrt,$(LIBS)) +LD = $(CXX) +LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -static +LDLIBS := $(filter-out -lrt,$(LDLIBS)) CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) CXXFLAGS += -std=$(CXXSTD) -Os -ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(CXX)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ +ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(LD)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \ ARCHFLAGS="-DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING=1 -Wno-unused-but-set-variable $(ARCHFLAGS)" ABC_USE_NO_READLINE=1 ifeq ($(DISABLE_ABC_THREADS),1) ABCMKARGS += "ABC_USE_NO_PTHREADS=1" @@ -247,31 +257,75 @@ endif else ifeq ($(CONFIG),afl-gcc) CXX = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc +LD = AFL_QUIET=1 AFL_HARDEN=1 afl-gcc CXXFLAGS += -std=$(CXXSTD) -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" else ifeq ($(CONFIG),cygwin) -CXX = g++ +CXX = gcc +LD = gcc CXXFLAGS += -std=gnu++11 -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" +else ifeq ($(CONFIG),emcc) +CXX = emcc +LD = emcc +CXXFLAGS := -std=$(CXXSTD) $(filter-out -fPIC -ggdb,$(CXXFLAGS)) +ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8 -Wno-c++11-narrowing" +EMCC_CXXFLAGS := -Os -Wno-warn-absolute-paths +EMCC_LDFLAGS := --memory-init-file 0 --embed-file share +EMCC_LDFLAGS += -s NO_EXIT_RUNTIME=1 +EMCC_LDFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" +EMCC_LDFLAGS += -s TOTAL_MEMORY=134217728 +EMCC_LDFLAGS += -s EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' +# https://github.com/kripken/emscripten/blob/master/src/settings.js +CXXFLAGS += $(EMCC_CXXFLAGS) +LDFLAGS += $(EMCC_LDFLAGS) +LDLIBS = +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++ +CXX = clang +LD = clang++ AR = llvm-ar RANLIB = llvm-ranlib WASIFLAGS := -target wasm32-wasi --sysroot $(WASI_SYSROOT) $(WASIFLAGS) else -CXX = $(WASI_SDK)/bin/clang++ +CXX = $(WASI_SDK)/bin/clang +LD = $(WASI_SDK)/bin/clang++ AR = $(WASI_SDK)/bin/ar RANLIB = $(WASI_SDK)/bin/ranlib WASIFLAGS := --sysroot $(WASI_SDK)/share/wasi-sysroot $(WASIFLAGS) endif -CXXFLAGS := $(WASIFLAGS) -std=$(CXXSTD) -Os -D_WASI_EMULATED_PROCESS_CLOCKS $(filter-out -fPIC,$(CXXFLAGS)) -LINKFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LINKFLAGS)) -LIBS := -lwasi-emulated-process-clocks $(filter-out -lrt,$(LIBS)) +CXXFLAGS := $(WASIFLAGS) -std=$(CXXSTD) -Os $(filter-out -fPIC,$(CXXFLAGS)) +LDFLAGS := $(WASIFLAGS) -Wl,-z,stack-size=1048576 $(filter-out -rdynamic,$(LDFLAGS)) +LDLIBS := $(filter-out -lrt,$(LDLIBS)) ABCMKARGS += AR="$(AR)" RANLIB="$(RANLIB)" -ABCMKARGS += ARCHFLAGS="$(WASIFLAGS) -D_WASI_EMULATED_PROCESS_CLOCKS -DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING -DABC_NO_RLIMIT" +ABCMKARGS += ARCHFLAGS="$(WASIFLAGS) -DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING -DABC_NO_RLIMIT -Wno-c++11-narrowing" ABCMKARGS += OPTFLAGS="-Os" EXE = .wasm @@ -285,41 +339,40 @@ endif else ifeq ($(CONFIG),mxe) PKG_CONFIG = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-pkg-config CXX = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ +LD = /usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s -LIBS := $(filter-out -lrt,$(LIBS)) +LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s +LDLIBS := $(filter-out -lrt,$(LDLIBS)) ABCMKARGS += ARCHFLAGS="-DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" # TODO: Try to solve pthread linking issue in more appropriate way -ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" LINKFLAGS="-Wl,--allow-multiple-definition" ABC_USE_NO_READLINE=1 CC="/usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-gcc" +ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" LDFLAGS="-Wl,--allow-multiple-definition" ABC_USE_NO_READLINE=1 CC="/usr/local/src/mxe/usr/bin/i686-w64-mingw32.static-gcc" EXE = .exe else ifeq ($(CONFIG),msys2-32) CXX = i686-w64-mingw32-g++ +LD = i686-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s -LIBS := $(filter-out -lrt,$(LIBS)) +LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s +LDLIBS := $(filter-out -lrt,$(LDLIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" -ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)" +ABCMKARGS += LIBS="-lpthread -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe else ifeq ($(CONFIG),msys2-64) CXX = x86_64-w64-mingw32-g++ +LD = x86_64-w64-mingw32-g++ CXXFLAGS += -std=$(CXXSTD) -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) -LINKFLAGS := $(filter-out -rdynamic,$(LINKFLAGS)) -s -LIBS := $(filter-out -lrt,$(LIBS)) +LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s +LDLIBS := $(filter-out -lrt,$(LDLIBS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" -ABCMKARGS += LIBS="-lpthread -lshlwapi -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" +ABCMKARGS += LIBS="-lpthread -s" ABC_USE_NO_READLINE=0 CC="x86_64-w64-mingw32-gcc" CXX="$(CXX)" EXE = .exe -else ifeq ($(CONFIG),none) -CXXFLAGS += -std=$(CXXSTD) -Os -ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H $(ABC_ARCHFLAGS)" - -else -$(error Invalid CONFIG setting '$(CONFIG)'. Valid values: clang, gcc, mxe, msys2-32, msys2-64, none) +else ifneq ($(CONFIG),none) +$(error Invalid CONFIG setting '$(CONFIG)'. Valid values: clang, gcc, emcc, mxe, msys2-32, msys2-64) endif ifeq ($(ENABLE_LIBYOSYS),1) @@ -340,9 +393,9 @@ ifeq ($(BOOST_PYTHON_LIB),) $(error BOOST_PYTHON_LIB could not be detected. Please define manually) endif -LIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem -# python-config --ldflags includes LIBS for some reason -LINKFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags)) +LDLIBS += $(shell $(PYTHON_CONFIG) --libs) $(BOOST_PYTHON_LIB) -lboost_system -lboost_filesystem +# python-config --ldflags includes LDLIBS for some reason +LDFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags)) CXXFLAGS += $(shell $(PYTHON_CONFIG) --includes) -DWITH_PYTHON PY_WRAPPER_FILE = kernel/python_wrappers @@ -356,22 +409,22 @@ CXXFLAGS += -DYOSYS_ENABLE_READLINE ifeq ($(OS), $(filter $(OS),FreeBSD OpenBSD NetBSD)) CXXFLAGS += -I/usr/local/include endif -LIBS += -lreadline +LDLIBS += -lreadline ifeq ($(LINK_CURSES),1) -LIBS += -lcurses +LDLIBS += -lcurses ABCMKARGS += "ABC_READLINE_LIBRARIES=-lcurses -lreadline" endif ifeq ($(LINK_TERMCAP),1) -LIBS += -ltermcap +LDLIBS += -ltermcap ABCMKARGS += "ABC_READLINE_LIBRARIES=-lreadline -ltermcap" endif ifeq ($(CONFIG),mxe) -LIBS += -ltermcap +LDLIBS += -ltermcap endif else ifeq ($(ENABLE_EDITLINE),1) CXXFLAGS += -DYOSYS_ENABLE_EDITLINE -LIBS += -ledit -ltinfo -lbsd +LDLIBS += -ledit -ltinfo -lbsd else ABCMKARGS += "ABC_USE_NO_READLINE=1" endif @@ -390,9 +443,9 @@ CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-e ifeq ($(OS), MINGW) CXXFLAGS += -Ilibs/dlfcn-win32 endif -LIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) +LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) ifneq ($(OS), $(filter $(OS),FreeBSD OpenBSD NetBSD MINGW)) -LIBS += -ldl +LDLIBS += -ldl endif endif @@ -402,7 +455,7 @@ endif ifeq ($(ENABLE_ZLIB),1) CXXFLAGS += -DYOSYS_ENABLE_ZLIB -LIBS += -lz +LDLIBS += -lz endif @@ -419,21 +472,21 @@ endif ifeq ($(CONFIG),mxe) CXXFLAGS += -DYOSYS_ENABLE_TCL -LIBS += -ltcl86 -lwsock32 -lws2_32 -lnetapi32 -lz -luserenv +LDLIBS += -ltcl86 -lwsock32 -lws2_32 -lnetapi32 -lz -luserenv else CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags tcl || echo -I$(TCL_INCLUDE)) -DYOSYS_ENABLE_TCL -LIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo $(TCL_LIBS)) +LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo $(TCL_LIBS)) endif endif ifeq ($(ENABLE_GCOV),1) CXXFLAGS += --coverage -LINKFLAGS += --coverage +LDFLAGS += --coverage endif ifeq ($(ENABLE_GPROF),1) CXXFLAGS += -pg -LINKFLAGS += -pg +LDFLAGS += -pg endif ifeq ($(ENABLE_NDEBUG),1) @@ -453,11 +506,11 @@ CXXFLAGS += -DYOSYS_ENABLE_ABC ifeq ($(LINK_ABC),1) CXXFLAGS += -DYOSYS_LINK_ABC ifeq ($(DISABLE_ABC_THREADS),0) -LIBS += -lpthread +LDLIBS += -lpthread endif else ifeq ($(ABCEXTERNAL),) -TARGETS := $(PROGRAM_PREFIX)yosys-abc$(EXE) $(TARGETS) +TARGETS += $(PROGRAM_PREFIX)yosys-abc$(EXE) endif endif endif @@ -467,30 +520,14 @@ GHDL_PREFIX ?= $(PREFIX) GHDL_INCLUDE_DIR ?= $(GHDL_PREFIX)/include GHDL_LIB_DIR ?= $(GHDL_PREFIX)/lib CXXFLAGS += -I$(GHDL_INCLUDE_DIR) -DYOSYS_ENABLE_GHDL -LIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link) +LDLIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link) endif -LIBS_VERIFIC = +LDLIBS_VERIFIC = ifeq ($(ENABLE_VERIFIC),1) VERIFIC_DIR ?= /usr/local/src/verific_lib -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 ?= verilog database util containers hier_tree +ifneq ($(DISABLE_VERIFIC_VHDL),1) VERIFIC_COMPONENTS += vhdl CXXFLAGS += -DVERIFIC_VHDL_SUPPORT else @@ -506,19 +543,15 @@ ifeq ($(ENABLE_VERIFIC_LIBERTY),1) VERIFIC_COMPONENTS += synlib CXXFLAGS += -DVERIFIC_LIBERTY_SUPPORT endif -ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1) +ifneq ($(DISABLE_VERIFIC_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) -LIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz +LDLIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz else -LIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz +LDLIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz endif endif @@ -573,37 +606,31 @@ Q = S = endif +$(eval $(call add_include_file,kernel/yosys.h)) +$(eval $(call add_include_file,kernel/hashlib.h)) +$(eval $(call add_include_file,kernel/log.h)) +$(eval $(call add_include_file,kernel/rtlil.h)) $(eval $(call add_include_file,kernel/binding.h)) +$(eval $(call add_include_file,kernel/register.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)) +$(eval $(call add_include_file,kernel/celledges.h)) $(eval $(call add_include_file,kernel/consteval.h)) $(eval $(call add_include_file,kernel/constids.inc)) -$(eval $(call add_include_file,kernel/cost.h)) +$(eval $(call add_include_file,kernel/sigtools.h)) +$(eval $(call add_include_file,kernel/modtools.h)) +$(eval $(call add_include_file,kernel/macc.h)) +$(eval $(call add_include_file,kernel/utils.h)) +$(eval $(call add_include_file,kernel/satgen.h)) +$(eval $(call add_include_file,kernel/qcsat.h)) $(eval $(call add_include_file,kernel/ff.h)) $(eval $(call add_include_file,kernel/ffinit.h)) -$(eval $(call add_include_file,kernel/ffmerge.h)) -$(eval $(call add_include_file,kernel/fmt.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,kernel/fstdata.h)) endif -$(eval $(call add_include_file,kernel/hashlib.h)) -$(eval $(call add_include_file,kernel/json.h)) -$(eval $(call add_include_file,kernel/log.h)) -$(eval $(call add_include_file,kernel/macc.h)) -$(eval $(call add_include_file,kernel/modtools.h)) $(eval $(call add_include_file,kernel/mem.h)) -$(eval $(call add_include_file,kernel/qcsat.h)) -$(eval $(call add_include_file,kernel/register.h)) -$(eval $(call add_include_file,kernel/rtlil.h)) -$(eval $(call add_include_file,kernel/satgen.h)) -$(eval $(call add_include_file,kernel/scopeinfo.h)) -$(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,kernel/json.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) ifeq ($(ENABLE_ZLIB),1) @@ -616,10 +643,21 @@ $(eval $(call add_include_file,frontends/ast/ast.h)) $(eval $(call add_include_file,frontends/ast/ast_binding.h)) $(eval $(call add_include_file,frontends/blif/blifparse.h)) $(eval $(call add_include_file,backends/rtlil/rtlil_backend.h)) +$(eval $(call add_include_file,backends/cxxrtl/cxxrtl.h)) +$(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd.h)) +$(eval $(call add_include_file,backends/cxxrtl/cxxrtl_capi.cc)) +$(eval $(call add_include_file,backends/cxxrtl/cxxrtl_capi.h)) +$(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd_capi.cc)) +$(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd_capi.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 +ifeq ($(ENABLE_ABC),1) +ifneq ($(ABCEXTERNAL),) +kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' +endif +endif +OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o ifeq ($(ENABLE_ZLIB),1) OBJS += kernel/fstdata.o endif @@ -631,19 +669,18 @@ endif kernel/log.o: CXXFLAGS += -DYOSYS_SRC='"$(YOSYS_SRC)"' kernel/yosys.o: CXXFLAGS += -DYOSYS_DATDIR='"$(DATDIR)"' -DYOSYS_PROGRAM_PREFIX='"$(PROGRAM_PREFIX)"' -ifeq ($(ENABLE_ABC),1) -ifneq ($(ABCEXTERNAL),) -kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' -endif -endif OBJS += libs/bigint/BigIntegerAlgorithms.o libs/bigint/BigInteger.o libs/bigint/BigIntegerUtils.o OBJS += libs/bigint/BigUnsigned.o libs/bigint/BigUnsignedInABase.o OBJS += libs/sha1/sha1.o +ifneq ($(SMALL),1) + OBJS += libs/json11/json11.o +OBJS += libs/subcircuit/subcircuit.o + OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o @@ -658,10 +695,6 @@ OBJS += libs/fst/fastlz.o OBJS += libs/fst/lz4.o endif -ifneq ($(SMALL),1) - -OBJS += libs/subcircuit/subcircuit.o - include $(YOSYS_SRC)/frontends/*/Makefile.inc include $(YOSYS_SRC)/passes/*/Makefile.inc include $(YOSYS_SRC)/backends/*/Makefile.inc @@ -670,9 +703,6 @@ include $(YOSYS_SRC)/techlibs/*/Makefile.inc else include $(YOSYS_SRC)/frontends/verilog/Makefile.inc -ifeq ($(ENABLE_VERIFIC),1) -include $(YOSYS_SRC)/frontends/verific/Makefile.inc -endif include $(YOSYS_SRC)/frontends/rtlil/Makefile.inc include $(YOSYS_SRC)/frontends/ast/Makefile.inc include $(YOSYS_SRC)/frontends/blif/Makefile.inc @@ -709,20 +739,18 @@ top-all: $(TARGETS) $(EXTRA_TARGETS) @echo " Build successful." @echo "" -.PHONY: compile-only -compile-only: $(OBJS) $(GENFILES) $(EXTRA_TARGETS) - @echo "" - @echo " Compile successful." - @echo "" +ifeq ($(CONFIG),emcc) +yosys.js: $(filter-out yosysjs-$(YOSYS_VER).zip,$(EXTRA_TARGETS)) +endif $(PROGRAM_PREFIX)yosys$(EXE): $(OBJS) - $(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(LIBS) $(LIBS_VERIFIC) + $(P) $(LD) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS) $(LDLIBS_VERIFIC) libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) ifeq ($(OS), Darwin) - $(P) $(CXX) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) + $(P) $(LD) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) else - $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LINKFLAGS) $^ $(LIBS) $(LIBS_VERIFIC) + $(P) $(LD) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC) endif %.o: %.cc @@ -731,7 +759,7 @@ endif %.pyh: %.h $(Q) mkdir -p $(dir $@) - $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(CXX) $(CXXFLAGS) -x c++ -o $@ -E -P - + $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) $(CXXFLAGS) -x c++ -o $@ -E -P - ifeq ($(ENABLE_PYOSYS),1) $(PY_WRAPPER_FILE).cc: misc/$(PY_GEN_SCRIPT).py $(PY_WRAP_INCLUDES) @@ -752,52 +780,53 @@ kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile ifeq ($(ENABLE_VERIFIC),1) CXXFLAGS_NOVERIFIC = $(foreach v,$(CXXFLAGS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) -LIBS_NOVERIFIC = $(foreach v,$(LIBS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) +LDLIBS_NOVERIFIC = $(foreach v,$(LDLIBS),$(if $(findstring $(VERIFIC_DIR),$(v)),,$(v))) else CXXFLAGS_NOVERIFIC = $(CXXFLAGS) -LIBS_NOVERIFIC = $(LIBS) +LDLIBS_NOVERIFIC = $(LDLIBS) endif -$(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in $(YOSYS_SRC)/Makefile +$(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in $(P) $(SED) -e 's#@CXXFLAGS@#$(subst -Ilibs/dlfcn-win32,,$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(strip $(CXXFLAGS_NOVERIFIC))))#;' \ - -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LINKFLAGS@#$(strip $(LINKFLAGS) $(PLUGIN_LINKFLAGS))#;' -e 's#@LIBS@#$(strip $(LIBS_NOVERIFIC) $(PLUGIN_LIBS))#;' \ + -e 's#@CXX@#$(strip $(CXX))#;' -e 's#@LDFLAGS@#$(strip $(LDFLAGS) $(PLUGIN_LDFLAGS))#;' -e 's#@LDLIBS@#$(strip $(LDLIBS_NOVERIFIC) $(PLUGIN_LDLIBS))#;' \ -e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > $(PROGRAM_PREFIX)yosys-config $(Q) chmod +x $(PROGRAM_PREFIX)yosys-config -.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; \ +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; \ + 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) -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) +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.a - $(P) cp $< $(PROGRAM_PREFIX)yosys-libabc.a +$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc-$(ABCREV).a + $(P) cp abc/libabc-$(ABCREV).a $(PROGRAM_PREFIX)yosys-libabc.a ifneq ($(SEED),) SEEDOPT="-S $(SEED)" @@ -811,22 +840,9 @@ else ABCOPT="" endif -# When YOSYS_NOVERIFIC is set as a make variable, also export it to the -# enviornment, so that `YOSYS_NOVERIFIC=1 make test` _and_ -# `make test YOSYS_NOVERIFIC=1` will run with verific disabled. -ifeq ($(YOSYS_NOVERIFIC),1) -export YOSYS_NOVERIFIC -endif - test: $(TARGETS) $(EXTRA_TARGETS) ifeq ($(ENABLE_VERIFIC),1) -ifeq ($(YOSYS_NOVERIFIC),1) - @echo - @echo "Running tests without verific support due to YOSYS_NOVERIFIC=1" - @echo -else +cd tests/verific && bash run-test.sh $(SEEDOPT) -endif endif +cd tests/simple && bash run-test.sh $(SEEDOPT) +cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT) @@ -860,15 +876,12 @@ endif +cd tests/arch/gowin && bash run-test.sh $(SEEDOPT) +cd tests/arch/intel_alm && bash run-test.sh $(SEEDOPT) +cd tests/arch/nexus && bash run-test.sh $(SEEDOPT) - +cd tests/arch/quicklogic/pp3 && bash run-test.sh $(SEEDOPT) - +cd tests/arch/quicklogic/qlf_k6n10f && bash run-test.sh $(SEEDOPT) + +cd tests/arch/quicklogic && bash run-test.sh $(SEEDOPT) +cd tests/arch/gatemate && 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 +cd tests/xprop && bash run-test.sh $(SEEDOPT) - +cd tests/fmt && bash run-test.sh - +cd tests/cxxrtl && bash run-test.sh @echo "" @echo " Passed \"make test\"." @echo "" @@ -898,7 +911,7 @@ ystests: $(TARGETS) $(EXTRA_TARGETS) # Unit test unit-test: libyosys.so @$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CPPFLAGS="$(CPPFLAGS)" \ - CXXFLAGS="$(CXXFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)" + CXXFLAGS="$(CXXFLAGS)" LDLIBS="$(LDLIBS)" ROOTPATH="$(CURDIR)" clean-unit-test: @$(MAKE) -C $(UNITESTPATH) clean @@ -951,47 +964,17 @@ 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_examples docs/gen_images docs/guidelines docs/usage docs/reqs -docs/gen_examples: - $(Q) $(MAKE) -C docs examples - +PHONY: docs/gen_images docs/guidelines docs/gen_images: - $(Q) $(MAKE) -C docs images + $(Q) $(MAKE) -C docs/images all DOCS_GUIDELINE_FILES := GettingStarted CodingStyle -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): $(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 +docs/guidelines: + $(Q) mkdir -p docs/source/temp + $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp DOC_TARGET ?= html -docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs +docs: docs/source/cmd/abc.rst docs/gen_images docs/guidelines $(Q) $(MAKE) -C docs $(DOC_TARGET) clean: @@ -1009,8 +992,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: @@ -1027,17 +1010,16 @@ 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.creator + touch qtcreator.config 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++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 + 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 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 @@ -1075,6 +1057,14 @@ 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 @@ -1116,8 +1106,8 @@ echo-yosys-ver: echo-git-rev: @echo "$(GIT_REV)" -echo-cxx: - @echo "$(CXX)" +echo-abc-rev: + @echo "$(ABCREV)" -include libs/*/*.d -include frontends/*/*.d diff --git a/yosys/README.md b/yosys/README.md index bb1c4d443e4..5e5a8ec3e12 100644 --- a/yosys/README.md +++ b/yosys/README.md @@ -1,7 +1,7 @@ ``` yosys -- Yosys Open SYnthesis Suite -Copyright (C) 2012 - 2024 Claire Xenia Wolf +Copyright (C) 2012 - 2020 Claire Xenia Wolf Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above @@ -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++17 support (up-to-date CLANG or GCC is +You need a C++ compiler with C++11 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. @@ -105,17 +105,11 @@ 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 -The environment variable `CXX` can be used to control the C++ compiler used, or -run one of the following: +To configure the build system to use a specific compiler, use one of $ 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 - For other compilers and build configurations it might be necessary to make some changes to the config section of the Makefile. @@ -593,19 +587,11 @@ from SystemVerilog: - enums are supported (including inside packages) - but are currently not strongly typed -- packed structs and unions are supported - - arrays of packed structs/unions are currently not supported - - structure literals are currently not supported - -- multidimensional arrays are supported - - array assignment of unpacked arrays is currently not supported - - array literals are currently not supported +- packed structs and unions are supported. - SystemVerilog interfaces (SVIs) are supported. Modports for specifying whether ports are inputs or outputs are supported. -- Assignments within expressions are supported. - Building the documentation ========================== @@ -616,12 +602,10 @@ 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 install pdf2svg faketime + $ sudo apt-get install pdf2svg faketime PDFLaTeX, included with most LaTeX distributions, is also needed during the -build process for the website. Or, run the following: - - $ sudo apt install texlive-latex-base texlive-latex-extra latexmk +build process for the website. The Python package, Sphinx, is needed along with those listed in `docs/source/requirements.txt`: diff --git a/yosys/backends/aiger/aiger.cc b/yosys/backends/aiger/aiger.cc index f2cb5d9bcc7..bb804f230fb 100644 --- a/yosys/backends/aiger/aiger.cc +++ b/yosys/backends/aiger/aiger.cc @@ -54,8 +54,6 @@ struct AigerWriter vector> aig_gates; vector aig_latchin, aig_latchinit, aig_outputs; - vector bit2aig_stack; - size_t next_loop_check = 1024; int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0; int aig_b = 0, aig_c = 0, aig_j = 0, aig_f = 0; @@ -67,8 +65,6 @@ struct AigerWriter int initstate_ff = 0; dict ywmap_clocks; - vector ywmap_asserts; - vector ywmap_assumes; int mkgate(int a0, int a1) { @@ -85,23 +81,6 @@ struct AigerWriter return it->second; } - if (bit2aig_stack.size() == next_loop_check) { - for (size_t i = 0; i < next_loop_check; ++i) - { - SigBit report_bit = bit2aig_stack[i]; - if (report_bit != bit) - continue; - for (size_t j = i; j < next_loop_check; ++j) { - report_bit = bit2aig_stack[j]; - if (report_bit.is_wire() && report_bit.wire->name.isPublic()) - break; - } - log_error("Found combinational logic loop while processing signal %s.\n", log_signal(report_bit)); - } - next_loop_check *= 2; - } - bit2aig_stack.push_back(bit); - // NB: Cannot use iterator returned from aig_map.insert() // since this function is called recursively @@ -122,8 +101,6 @@ struct AigerWriter a = initstate_ff; } - bit2aig_stack.pop_back(); - if (bit == State::Sx || bit == State::Sz) log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n"); @@ -271,7 +248,6 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); asserts.push_back(make_pair(A, EN)); - ywmap_asserts.push_back(cell); continue; } @@ -282,7 +258,6 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); assumes.push_back(make_pair(A, EN)); - ywmap_assumes.push_back(cell); continue; } @@ -324,9 +299,6 @@ struct AigerWriter continue; } - if (cell->type == ID($scopeinfo)) - continue; - log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); } @@ -856,19 +828,6 @@ struct AigerWriter for (auto &it : init_lines) json.value(it.second); json.end_array(); - - json.name("asserts"); - json.begin_array(); - for (Cell *cell : ywmap_asserts) - json.value(witness_path(cell)); - json.end_array(); - - json.name("assumes"); - json.begin_array(); - for (Cell *cell : ywmap_assumes) - json.value(witness_path(cell)); - json.end_array(); - json.end_object(); } diff --git a/yosys/backends/blif/blif.cc b/yosys/backends/blif/blif.cc index 788b7f951f2..8e2c088c484 100644 --- a/yosys/backends/blif/blif.cc +++ b/yosys/backends/blif/blif.cc @@ -226,9 +226,6 @@ struct BlifDumper for (auto cell : module->cells()) { - if (cell->type == ID($scopeinfo)) - continue; - if (config->unbuf_types.count(cell->type)) { auto portnames = config->unbuf_types.at(cell->type); f << stringf(".names %s %s\n1 1\n", diff --git a/yosys/backends/btor/test_cells.sh b/yosys/backends/btor/test_cells.sh index f8bd797825e..0a011932d22 100755 --- a/yosys/backends/btor/test_cells.sh +++ b/yosys/backends/btor/test_cells.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env bash +#!/bin/bash set -ex diff --git a/yosys/backends/cxxrtl/Makefile.inc b/yosys/backends/cxxrtl/Makefile.inc index dd77d2ad360..aaa304502e0 100644 --- a/yosys/backends/cxxrtl/Makefile.inc +++ b/yosys/backends/cxxrtl/Makefile.inc @@ -1,11 +1,2 @@ OBJS += backends/cxxrtl/cxxrtl_backend.o - -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_time.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc)) -$(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h)) diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/yosys/backends/cxxrtl/cxxrtl.h similarity index 71% rename from yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h rename to yosys/backends/cxxrtl/cxxrtl.h index d1d6bd8dc68..5d0596f0d61 100644 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h +++ b/yosys/backends/cxxrtl/cxxrtl.h @@ -28,7 +28,6 @@ #include #include -#include #include #include #include @@ -39,10 +38,8 @@ #include #include #include -#include -// `cxxrtl::debug_item` has to inherit from `cxxrtl_object` to satisfy strict aliasing requirements. -#include +#include #ifndef __has_attribute # define __has_attribute(x) 0 @@ -147,7 +144,7 @@ struct value : public expr_base> { // These functions ensure that a conversion is never out of range, and should be always used, if at all // possible, instead of direct manipulation of the `data` member. For very large types, .slice() and // .concat() can be used to split them into more manageable parts. - template::value, int>::type = 0> + template CXXRTL_ALWAYS_INLINE IntegerT get() const { static_assert(std::numeric_limits::is_integer && !std::numeric_limits::is_signed, @@ -160,32 +157,15 @@ struct value : public expr_base> { return result; } - template::value, int>::type = 0> - CXXRTL_ALWAYS_INLINE - IntegerT get() const { - auto unsigned_result = get::type>(); - IntegerT result; - memcpy(&result, &unsigned_result, sizeof(IntegerT)); - return result; - } - - template::value, int>::type = 0> + template CXXRTL_ALWAYS_INLINE - void set(IntegerT value) { + void set(IntegerT other) { static_assert(std::numeric_limits::is_integer && !std::numeric_limits::is_signed, "set() requires T to be an unsigned integral type"); static_assert(std::numeric_limits::digits >= Bits, "set() requires the value to be at least as wide as T is"); for (size_t n = 0; n < chunks; n++) - data[n] = (value >> (n * chunk::bits)) & chunk::mask; - } - - template::value, int>::type = 0> - CXXRTL_ALWAYS_INLINE - void set(IntegerT value) { - typename std::make_unsigned::type unsigned_value; - memcpy(&unsigned_value, &value, sizeof(IntegerT)); - set(unsigned_value); + data[n] = (other >> (n * chunk::bits)) & chunk::mask; } // Operations with compile-time parameters. @@ -438,7 +418,6 @@ struct value : public expr_base> { carry = (shift_bits == 0) ? 0 : data[n] >> (chunk::bits - shift_bits); } - result.data[result.chunks - 1] &= result.msb_mask; return result; } @@ -449,12 +428,12 @@ struct value : public expr_base> { // Detect shifts definitely large than Bits early. for (size_t n = 1; n < amount.chunks; n++) if (amount.data[n] != 0) - return (Signed && is_neg()) ? value().bit_not() : value(); + return {}; // Past this point we can use the least significant chunk as the shift size. size_t shift_chunks = amount.data[0] / chunk::bits; size_t shift_bits = amount.data[0] % chunk::bits; if (shift_chunks >= chunks) - return (Signed && is_neg()) ? value().bit_not() : value(); + return {}; value result; chunk::type carry = 0; for (size_t n = 0; n < chunks - shift_chunks; n++) { @@ -463,13 +442,12 @@ struct value : public expr_base> { : data[chunks - 1 - n] << (chunk::bits - shift_bits); } if (Signed && is_neg()) { - size_t top_chunk_idx = amount.data[0] > Bits ? 0 : (Bits - amount.data[0]) / chunk::bits; - size_t top_chunk_bits = amount.data[0] > Bits ? 0 : (Bits - amount.data[0]) % chunk::bits; + size_t top_chunk_idx = (Bits - shift_bits) / chunk::bits; + size_t top_chunk_bits = (Bits - shift_bits) % chunk::bits; for (size_t n = top_chunk_idx + 1; n < chunks; n++) result.data[n] = chunk::mask; - if (amount.data[0] != 0) + if (shift_bits != 0) result.data[top_chunk_idx] |= chunk::mask << top_chunk_bits; - result.data[result.chunks - 1] &= result.msb_mask; } return result; } @@ -494,7 +472,6 @@ struct value : public expr_base> { carry = (shift_bits == 0) ? 0 : data[result.chunks + shift_chunks - 1 - n] << (chunk::bits - shift_bits); } - result.data[result.chunks - 1] &= result.msb_mask; return result; } @@ -530,14 +507,12 @@ struct value : public expr_base> { size_t count = 0; for (size_t n = 0; n < chunks; n++) { chunk::type x = data[chunks - 1 - n]; - // First add to `count` as if the chunk is zero - constexpr size_t msb_chunk_bits = Bits % chunk::bits != 0 ? Bits % chunk::bits : chunk::bits; - count += (n == 0 ? msb_chunk_bits : chunk::bits); - // If the chunk isn't zero, correct the `count` value and return - if (x != 0) { - for (; x != 0; count--) + if (x == 0) { + count += (n == 0 ? Bits % chunk::bits : chunk::bits); + } else { + // This loop implements the find first set idiom as recognized by LLVM. + for (; x != 0; count++) x >>= 1; - break; } } return count; @@ -566,7 +541,7 @@ struct value : public expr_base> { } value neg() const { - return value().sub(*this); + return value { 0u }.sub(*this); } bool ucmp(const value &other) const { @@ -600,38 +575,6 @@ struct value : public expr_base> { result.data[result.chunks - 1] &= result.msb_mask; return result; } - - std::pair, value> udivmod(value divisor) const { - value quotient; - value dividend = *this; - if (dividend.ucmp(divisor)) - return {/*quotient=*/value{0u}, /*remainder=*/dividend}; - int64_t divisor_shift = divisor.ctlz() - dividend.ctlz(); - assert(divisor_shift >= 0); - divisor = divisor.shl(value{(chunk::type) divisor_shift}); - for (size_t step = 0; step <= divisor_shift; step++) { - quotient = quotient.shl(value{1u}); - if (!dividend.ucmp(divisor)) { - dividend = dividend.sub(divisor); - quotient.set_bit(0, true); - } - divisor = divisor.shr(value{1u}); - } - return {quotient, /*remainder=*/dividend}; - } - - std::pair, value> sdivmod(const value &other) const { - value quotient; - value remainder; - value dividend = sext(); - value divisor = other.template sext(); - if (is_neg()) dividend = dividend.neg(); - if (other.is_neg()) divisor = divisor.neg(); - std::tie(quotient, remainder) = dividend.udivmod(divisor); - if (is_neg() != other.is_neg()) quotient = quotient.neg(); - if (is_neg()) remainder = remainder.neg(); - return {quotient.template trunc(), remainder.template trunc()}; - } }; // Expression template for a slice, usable as lvalue or rvalue, and composable with other expression templates here. @@ -798,13 +741,8 @@ struct wire { next.template set(other); } - // This method intentionally takes a mandatory argument (to make it more difficult to misuse in - // black box implementations, leading to missed observer events). It is generic over its argument - // to allow the `on_update` method to be non-virtual. - template - bool commit(ObserverT &observer) { + bool commit() { if (curr != next) { - observer.on_update(curr.chunks, curr.data, next.data); curr = next; return true; } @@ -878,17 +816,12 @@ struct memory { write { index, val, mask, priority }); } - // See the note for `wire::commit()`. - template - bool commit(ObserverT &observer) { + bool commit() { bool changed = false; for (const write &entry : write_queue) { value elem = data[entry.index]; elem = elem.update(entry.val, entry.mask); - if (data[entry.index] != elem) { - observer.on_update(value::chunks, data[0].data, elem.data, entry.index); - changed |= true; - } + changed |= (data[entry.index] != elem); data[entry.index] = elem; } write_queue.clear(); @@ -907,14 +840,14 @@ struct metadata { // In debug mode, using the wrong .as_*() function will assert. // In release mode, using the wrong .as_*() function will safely return a default value. - const uint64_t uint_value = 0; - const int64_t sint_value = 0; + const unsigned uint_value = 0; + const signed sint_value = 0; const std::string string_value = ""; const double double_value = 0.0; metadata() : value_type(MISSING) {} - metadata(uint64_t value) : value_type(UINT), uint_value(value) {} - metadata(int64_t value) : value_type(SINT), sint_value(value) {} + metadata(unsigned value) : value_type(UINT), uint_value(value) {} + metadata(signed value) : value_type(SINT), sint_value(value) {} metadata(const std::string &value) : value_type(STRING), string_value(value) {} metadata(const char *value) : value_type(STRING), string_value(value) {} metadata(double value) : value_type(DOUBLE), double_value(value) {} @@ -922,12 +855,12 @@ struct metadata { metadata(const metadata &) = default; metadata &operator=(const metadata &) = delete; - uint64_t as_uint() const { + unsigned as_uint() const { assert(value_type == UINT); return uint_value; } - int64_t as_sint() const { + signed as_sint() const { assert(value_type == SINT); return sint_value; } @@ -941,322 +874,10 @@ 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; -struct performer; - -// An object that allows formatting a string lazily. -struct lazy_fmt { - virtual std::string operator() () const = 0; -}; - -// Flavor of a `$check` cell. -enum class flavor { - // Corresponds to a `$assert` cell in other flows, and a Verilog `assert ()` statement. - ASSERT, - // Corresponds to a `$assume` cell in other flows, and a Verilog `assume ()` statement. - ASSUME, - // Corresponds to a `$live` cell in other flows, and a Verilog `assert (eventually)` statement. - ASSERT_EVENTUALLY, - // Corresponds to a `$fair` cell in other flows, and a Verilog `assume (eventually)` statement. - ASSUME_EVENTUALLY, - // Corresponds to a `$cover` cell in other flows, and a Verilog `cover ()` statement. - COVER, -}; - -// An object that can be passed to a `eval()` method in order to act on side effects. The default behavior implemented -// below is the same as the behavior of `eval(nullptr)`, except that `-print-output` option of `write_cxxrtl` is not -// taken into account. -struct performer { - // Called by generated formatting code to evaluate a Verilog `$time` expression. - virtual int64_t vlog_time() const { return 0; } - - // Called by generated formatting code to evaluate a Verilog `$realtime` expression. - virtual double vlog_realtime() const { return vlog_time(); } - - // Called when a `$print` cell is triggered. - virtual void on_print(const lazy_fmt &formatter, const metadata_map &attributes) { - std::cout << formatter(); - } - - // Called when a `$check` cell is triggered. - virtual void on_check(flavor type, bool condition, const lazy_fmt &formatter, const metadata_map &attributes) { - if (type == flavor::ASSERT || type == flavor::ASSUME) { - if (!condition) - std::cerr << formatter(); - CXXRTL_ASSERT(condition && "Check failed"); - } - } -}; - -// An object that can be passed to a `commit()` method in order to produce a replay log of every state change in -// the simulation. Unlike `performer`, `observer` does not use virtual calls as their overhead is unacceptable, and -// a comparatively heavyweight template-based solution is justified. -struct observer { - // Called when the `commit()` method for a wire is about to update the `chunks` chunks at `base` with `chunks` chunks - // at `value` that have a different bit pattern. It is guaranteed that `chunks` is equal to the wire chunk count and - // `base` points to the first chunk. - void on_update(size_t chunks, const chunk_t *base, const chunk_t *value) {} - - // Called when the `commit()` method for a memory is about to update the `chunks` chunks at `&base[chunks * index]` - // with `chunks` chunks at `value` that have a different bit pattern. It is guaranteed that `chunks` is equal to - // the memory element chunk count and `base` points to the first chunk of the first element of the memory. - void on_update(size_t chunks, const chunk_t *base, const chunk_t *value, size_t index) {} -}; - -// Must be kept in sync with `struct FmtPart` in kernel/fmt.h! -// Default member initializers would make this a non-aggregate-type in C++11, so they are commented out. -struct fmt_part { - enum { - LITERAL = 0, - INTEGER = 1, - STRING = 2, - UNICHAR = 3, - VLOG_TIME = 4, - } type; - - // LITERAL type - std::string str; - - // INTEGER/STRING/UNICHAR types - // + value val; - - // INTEGER/STRING/VLOG_TIME types - enum { - RIGHT = 0, - LEFT = 1, - NUMERIC = 2, - } justify; // = RIGHT; - char padding; // = '\0'; - size_t width; // = 0; - - // INTEGER type - unsigned base; // = 10; - bool signed_; // = 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; - // + int64_t itime; - // + double ftime; - - // Format the part as a string. - // - // The values of `vlog_time` and `vlog_realtime` are used for Verilog `$time` and `$realtime`, correspondingly. - template - std::string render(value val, performer *performer = nullptr) - { - // 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 LITERAL: - return str; - - case STRING: { - buf.reserve(Bits/8); - for (int i = 0; i < Bits; i += 8) { - char ch = 0; - for (int j = 0; j < 8 && i + j < int(Bits); j++) - if (val.bit(i + j)) - ch |= 1 << j; - if (ch != 0) - buf.append({ch}); - } - std::reverse(buf.begin(), buf.end()); - 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: { - 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) { - val_width = 1; - for (size_t index = 0; index < Bits; index++) - if (val.bit(index)) - val_width = index + 1; - } - - if (base == 2) { - 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 < 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 += (hex_upper ? "0123456789ABCDEF" : "0123456789abcdef")[value]; - } - } else if (base == 10) { - 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}); - else - 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++; - } - } 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; - } - - case VLOG_TIME: { - if (performer) { - buf = realtime ? std::to_string(performer->vlog_realtime()) : std::to_string(performer->vlog_time()); - } else { - buf = realtime ? std::to_string(0.0) : std::to_string(0); - } - break; - } - } - - std::string str; - assert(width == 0 || padding != '\0'); - 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; - } - return str; - } -}; - // Tag class to disambiguate values/wires and their aliases. struct debug_alias {}; @@ -1268,9 +889,6 @@ using debug_outline = ::_cxxrtl_outline; // // To avoid violating strict aliasing rules, this structure has to be a subclass of the one used // in the C API, or it would not be possible to cast between the pointers to these. -// -// The `attrs` member cannot be owned by this structure because a `cxxrtl_object` can be created -// from external C code. struct debug_item : ::cxxrtl_object { // Object types. enum : uint32_t { @@ -1295,7 +913,7 @@ struct debug_item : ::cxxrtl_object { template debug_item(value &item, size_t lsb_offset = 0, uint32_t flags_ = 0) { - static_assert(Bits == 0 || sizeof(item) == value::chunks * sizeof(chunk_t), + static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = VALUE; flags = flags_; @@ -1306,12 +924,11 @@ struct debug_item : ::cxxrtl_object { curr = item.data; next = item.data; outline = nullptr; - attrs = nullptr; } template debug_item(const value &item, size_t lsb_offset = 0) { - static_assert(Bits == 0 || sizeof(item) == value::chunks * sizeof(chunk_t), + static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = VALUE; flags = DRIVEN_COMB; @@ -1322,14 +939,12 @@ struct debug_item : ::cxxrtl_object { curr = const_cast(item.data); next = nullptr; outline = nullptr; - attrs = nullptr; } template debug_item(wire &item, size_t lsb_offset = 0, uint32_t flags_ = 0) { - static_assert(Bits == 0 || - (sizeof(item.curr) == value::chunks * sizeof(chunk_t) && - sizeof(item.next) == value::chunks * sizeof(chunk_t)), + static_assert(sizeof(item.curr) == value::chunks * sizeof(chunk_t) && + sizeof(item.next) == value::chunks * sizeof(chunk_t), "wire is not compatible with C layout"); type = WIRE; flags = flags_; @@ -1340,12 +955,11 @@ struct debug_item : ::cxxrtl_object { curr = item.curr.data; next = item.next.data; outline = nullptr; - attrs = nullptr; } template debug_item(memory &item, size_t zero_offset = 0) { - static_assert(Width == 0 || sizeof(item.data[0]) == value::chunks * sizeof(chunk_t), + static_assert(sizeof(item.data[0]) == value::chunks * sizeof(chunk_t), "memory is not compatible with C layout"); type = MEMORY; flags = 0; @@ -1356,12 +970,11 @@ struct debug_item : ::cxxrtl_object { curr = item.data ? item.data[0].data : nullptr; next = nullptr; outline = nullptr; - attrs = nullptr; } template debug_item(debug_alias, const value &item, size_t lsb_offset = 0) { - static_assert(Bits == 0 || sizeof(item) == value::chunks * sizeof(chunk_t), + static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = ALIAS; flags = DRIVEN_COMB; @@ -1372,14 +985,12 @@ struct debug_item : ::cxxrtl_object { curr = const_cast(item.data); next = nullptr; outline = nullptr; - attrs = nullptr; } template debug_item(debug_alias, const wire &item, size_t lsb_offset = 0) { - static_assert(Bits == 0 || - (sizeof(item.curr) == value::chunks * sizeof(chunk_t) && - sizeof(item.next) == value::chunks * sizeof(chunk_t)), + static_assert(sizeof(item.curr) == value::chunks * sizeof(chunk_t) && + sizeof(item.next) == value::chunks * sizeof(chunk_t), "wire is not compatible with C layout"); type = ALIAS; flags = DRIVEN_COMB; @@ -1390,12 +1001,11 @@ struct debug_item : ::cxxrtl_object { curr = const_cast(item.curr.data); next = nullptr; outline = nullptr; - attrs = nullptr; } template debug_item(debug_outline &group, const value &item, size_t lsb_offset = 0) { - static_assert(Bits == 0 || sizeof(item) == value::chunks * sizeof(chunk_t), + static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = OUTLINE; flags = DRIVEN_COMB; @@ -1406,7 +1016,6 @@ struct debug_item : ::cxxrtl_object { curr = const_cast(item.data); next = nullptr; outline = &group; - attrs = nullptr; } template @@ -1427,38 +1036,11 @@ struct debug_item : ::cxxrtl_object { }; static_assert(std::is_standard_layout::value, "debug_item is not compatible with C layout"); -} // namespace cxxrtl - -typedef struct _cxxrtl_attr_set { - cxxrtl::metadata_map map; -} *cxxrtl_attr_set; - -namespace cxxrtl { - -// Representation of an attribute set in the C++ interface. -using debug_attrs = ::_cxxrtl_attr_set; - struct debug_items { - // Debug items may be composed of multiple parts, but the attributes are shared between all of them. - // There are additional invariants, not all of which are not checked by this code: - // - Memories and non-memories cannot be mixed together. - // - Bit indices (considering `lsb_at` and `width`) must not overlap. - // - Row indices (considering `depth` and `zero_at`) must be the same. - // - The `INPUT` and `OUTPUT` flags must be the same for all parts. - // Other than that, the parts can be quite different, e.g. it is OK to mix a value, a wire, an alias, - // and an outline, in the debug information for a single name in four parts. std::map> table; - std::map> attrs_table; - - void add(const std::string &path, debug_item &&item, metadata_map &&item_attrs = {}) { - assert((path.empty() || path[path.size() - 1] != ' ') && path.find(" ") == std::string::npos); - std::unique_ptr &attrs = attrs_table[path]; - if (attrs.get() == nullptr) - attrs = std::unique_ptr(new debug_attrs); - for (auto attr : item_attrs) - attrs->map.insert(attr); - item.attrs = attrs.get(); - std::vector &parts = table[path]; + + void add(const std::string &name, debug_item &&item) { + std::vector &parts = table[name]; parts.emplace_back(item); std::sort(parts.begin(), parts.end(), [](const debug_item &a, const debug_item &b) { @@ -1466,82 +1048,31 @@ 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) + size_t count(const std::string &name) const { + if (table.count(name) == 0) return 0; - return table.at(path).size(); + return table.at(name).size(); } - const std::vector &at(const std::string &path) const { - return table.at(path); + const std::vector &parts_at(const std::string &name) const { + return table.at(name); } - // Like `at()`, but operates only on single-part debug items. - const debug_item &operator [](const std::string &path) const { - const std::vector &parts = table.at(path); + const debug_item &at(const std::string &name) const { + const std::vector &parts = table.at(name); assert(parts.size() == 1); return parts.at(0); } - bool is_memory(const std::string &path) const { - return at(path).at(0).type == debug_item::MEMORY; - } - - const metadata_map &attrs(const std::string &path) const { - return attrs_table.at(path)->map; + const debug_item &operator [](const std::string &name) const { + return at(name); } }; -// Only `module` scopes are defined. The type is implicit, since Yosys does not currently support -// any other scope types. -struct debug_scope { - std::string module_name; - std::unique_ptr module_attrs; - std::unique_ptr cell_attrs; -}; - -struct debug_scopes { - std::map table; - - void add(const std::string &path, const std::string &module_name, metadata_map &&module_attrs, metadata_map &&cell_attrs) { - assert((path.empty() || path[path.size() - 1] != ' ') && path.find(" ") == std::string::npos); - assert(table.count(path) == 0); - debug_scope &scope = table[path]; - scope.module_name = module_name; - scope.module_attrs = std::unique_ptr(new debug_attrs { module_attrs }); - scope.cell_attrs = std::unique_ptr(new debug_attrs { cell_attrs }); - } - - // 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); - } - - const debug_scope &operator [](const std::string &path) const { - return table.at(path); - } -}; - -// Tag class to disambiguate the default constructor used by the toplevel module that calls `reset()`, +// Tag class to disambiguate the default constructor used by the toplevel module that calls reset(), // and the constructor of interior modules that should not call it. struct interior {}; -// The core API of the `module` class consists of only four virtual methods: `reset()`, `eval()`, -// `commit`, and `debug_info()`. (The virtual destructor is made necessary by C++.) Every other method -// is a convenience method, and exists solely to simplify some common pattern for C++ API consumers. -// No behavior may be added to such convenience methods that other parts of CXXRTL can rely on, since -// there is no guarantee they will be called (and, for example, other CXXRTL libraries will often call -// the `eval()` and `commit()` directly instead, as well as being exposed in the C API). struct module { module() {} virtual ~module() {} @@ -1557,35 +1088,21 @@ struct module { virtual void reset() = 0; - // The `eval()` callback object, `performer`, is included in the virtual call signature since - // the generated code has broadly identical performance properties. - virtual bool eval(performer *performer = nullptr) = 0; - - // The `commit()` callback object, `observer`, is not included in the virtual call signature since - // the generated code is severely pessimized by it. To observe commit events, the non-virtual - // `commit(observer *)` overload must be called directly on a `module` subclass. + virtual bool eval() = 0; virtual bool commit() = 0; - size_t step(performer *performer = nullptr) { + size_t step() { size_t deltas = 0; bool converged = false; do { - converged = eval(performer); + converged = eval(); deltas++; } while (commit() && !converged); return deltas; } - virtual void debug_info(debug_items *items, debug_scopes *scopes, std::string path, metadata_map &&cell_attrs = {}) { - (void)items, (void)scopes, (void)path, (void)cell_attrs; - } - - // Compatibility method. -#if __has_attribute(deprecated) - __attribute__((deprecated("Use `debug_info(&items, /*scopes=*/nullptr, path);` instead."))) -#endif - void debug_info(debug_items &items, std::string path) { - debug_info(&items, /*scopes=*/nullptr, path); + virtual void debug_info(debug_items &items, std::string path = "") { + (void)items, (void)path; } }; @@ -2003,23 +1520,35 @@ CXXRTL_ALWAYS_INLINE std::pair, value> divmod_uu(const value &a, const value &b) { constexpr size_t Bits = max(BitsY, max(BitsA, BitsB)); value quotient; - value remainder; value dividend = a.template zext(); value divisor = b.template zext(); - std::tie(quotient, remainder) = dividend.udivmod(divisor); - return {quotient.template trunc(), remainder.template trunc()}; + if (dividend.ucmp(divisor)) + return {/*quotient=*/value { 0u }, /*remainder=*/dividend.template trunc()}; + uint32_t divisor_shift = dividend.ctlz() - divisor.ctlz(); + divisor = divisor.shl(value<32> { divisor_shift }); + for (size_t step = 0; step <= divisor_shift; step++) { + quotient = quotient.shl(value<1> { 1u }); + if (!dividend.ucmp(divisor)) { + dividend = dividend.sub(divisor); + quotient.set_bit(0, true); + } + divisor = divisor.shr(value<1> { 1u }); + } + return {quotient.template trunc(), /*remainder=*/dividend.template trunc()}; } template CXXRTL_ALWAYS_INLINE std::pair, value> divmod_ss(const value &a, const value &b) { - constexpr size_t Bits = max(BitsY, max(BitsA, BitsB)); - value quotient; - value remainder; - value dividend = a.template sext(); - value divisor = b.template sext(); - std::tie(quotient, remainder) = dividend.sdivmod(divisor); - return {quotient.template trunc(), remainder.template trunc()}; + value ua = a.template sext(); + value ub = b.template sext(); + if (ua.is_neg()) ua = ua.neg(); + if (ub.is_neg()) ub = ub.neg(); + value y, r; + std::tie(y, r) = divmod_uu(ua, ub); + if (a.is_neg() != b.is_neg()) y = y.neg(); + if (a.is_neg()) r = r.neg(); + return {y, r}; } template diff --git a/yosys/backends/cxxrtl/cxxrtl_backend.cc b/yosys/backends/cxxrtl/cxxrtl_backend.cc index 8dc14863d60..1b13985ab4e 100644 --- a/yosys/backends/cxxrtl/cxxrtl_backend.cc +++ b/yosys/backends/cxxrtl/cxxrtl_backend.cc @@ -24,8 +24,6 @@ #include "kernel/celltypes.h" #include "kernel/mem.h" #include "kernel/log.h" -#include "kernel/fmt.h" -#include "kernel/scopeinfo.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -219,7 +217,7 @@ bool is_internal_cell(RTLIL::IdString type) bool is_effectful_cell(RTLIL::IdString type) { - return type.in(ID($print), ID($check)); + return type.isPublic(); } bool is_cxxrtl_blackbox_cell(const RTLIL::Cell *cell) @@ -283,7 +281,6 @@ struct FlowGraph { CONNECT, CELL_SYNC, CELL_EVAL, - EFFECT_SYNC, PROCESS_SYNC, PROCESS_CASE, MEM_RDPORT, @@ -293,7 +290,6 @@ struct FlowGraph { Type type; RTLIL::SigSig connect = {}; const RTLIL::Cell *cell = nullptr; - std::vector cells; const RTLIL::Process *process = nullptr; const Mem *mem = nullptr; int portidx; @@ -481,15 +477,6 @@ struct FlowGraph { return node; } - Node *add_effect_sync_node(std::vector cells) - { - Node *node = new Node; - node->type = Node::Type::EFFECT_SYNC; - node->cells = cells; - nodes.push_back(node); - return node; - } - // Processes void add_case_rule_defs_uses(Node *node, const RTLIL::CaseRule *case_) { @@ -606,30 +593,22 @@ std::vector split_by(const std::string &str, const std::string &sep return result; } -std::string escape_c_string(const std::string &input) +std::string escape_cxx_string(const std::string &input) { - std::string output; - output.push_back('"'); + std::string output = "\""; for (auto c : input) { if (::isprint(c)) { if (c == '\\') output.push_back('\\'); output.push_back(c); } else { - 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); + 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)); } } 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())); @@ -637,20 +616,6 @@ std::string escape_cxx_string(const std::string &input) return output; } -std::string basename(const std::string &filepath) -{ -#ifdef _WIN32 - const std::string dir_seps = "\\/"; -#else - const std::string dir_seps = "/"; -#endif - size_t sep_pos = filepath.find_last_of(dir_seps); - if (sep_pos != std::string::npos) - return filepath.substr(sep_pos + 1); - else - return filepath; -} - template std::string get_hdl_name(T *object) { @@ -716,7 +681,6 @@ struct CxxrtlWorker { bool split_intf = false; std::string intf_filename; std::string design_ns = "cxxrtl_design"; - std::string print_output = "std::cout"; std::ostream *impl_f = nullptr; std::ostream *intf_f = nullptr; @@ -1138,7 +1102,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) && !conn.second.empty()) { + if (is_cxxrtl_sync_port(cell, conn.first)) { f << indent; dump_sigspec_lhs(conn.second, for_debug); f << " = " << mangle(cell) << access << mangle_wire_name(conn.first) << ".curr;\n"; @@ -1225,144 +1189,6 @@ struct CxxrtlWorker { } } - void dump_print(const RTLIL::Cell *cell) - { - Fmt fmt; - fmt.parse_rtlil(cell); - - f << indent << "if ("; - dump_sigspec_rhs(cell->getPort(ID::EN)); - f << " == value<1>{1u}) {\n"; - inc_indent(); - dict fmt_args; - f << indent << "struct : public lazy_fmt {\n"; - inc_indent(); - f << indent << "std::string operator() () const override {\n"; - inc_indent(); - fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) { - if (sig.size() == 0) - f << "value<0>()"; - else { - std::string arg_name = "arg" + std::to_string(fmt_args.size()); - fmt_args[arg_name] = sig; - f << arg_name; - } - }, "performer"); - dec_indent(); - f << indent << "}\n"; - f << indent << "struct performer *performer;\n"; - for (auto arg : fmt_args) - f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n"; - dec_indent(); - f << indent << "} formatter;\n"; - f << indent << "formatter.performer = performer;\n"; - for (auto arg : fmt_args) { - f << indent << "formatter." << arg.first << " = "; - dump_sigspec_rhs(arg.second); - f << ";\n"; - } - f << indent << "if (performer) {\n"; - inc_indent(); - f << indent << "static const metadata_map attributes = "; - dump_metadata_map(cell->attributes); - f << ";\n"; - f << indent << "performer->on_print(formatter, attributes);\n"; - dec_indent(); - f << indent << "} else {\n"; - inc_indent(); - f << indent << print_output << " << formatter();\n"; - dec_indent(); - f << indent << "}\n"; - dec_indent(); - f << indent << "}\n"; - } - - void dump_effect(const RTLIL::Cell *cell) - { - Fmt fmt; - fmt.parse_rtlil(cell); - - f << indent << "if ("; - dump_sigspec_rhs(cell->getPort(ID::EN)); - f << ") {\n"; - inc_indent(); - dict fmt_args; - f << indent << "struct : public lazy_fmt {\n"; - inc_indent(); - f << indent << "std::string operator() () const override {\n"; - inc_indent(); - fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) { - if (sig.size() == 0) - f << "value<0>()"; - else { - std::string arg_name = "arg" + std::to_string(fmt_args.size()); - fmt_args[arg_name] = sig; - f << arg_name; - } - }, "performer"); - dec_indent(); - f << indent << "}\n"; - f << indent << "struct performer *performer;\n"; - for (auto arg : fmt_args) - f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n"; - dec_indent(); - f << indent << "} formatter;\n"; - f << indent << "formatter.performer = performer;\n"; - for (auto arg : fmt_args) { - f << indent << "formatter." << arg.first << " = "; - dump_sigspec_rhs(arg.second); - f << ";\n"; - } - if (cell->hasPort(ID::A)) { - f << indent << "bool condition = (bool)"; - dump_sigspec_rhs(cell->getPort(ID::A)); - f << ";\n"; - } - f << indent << "if (performer) {\n"; - inc_indent(); - f << indent << "static const metadata_map attributes = "; - dump_metadata_map(cell->attributes); - f << ";\n"; - if (cell->type == ID($print)) { - f << indent << "performer->on_print(formatter, attributes);\n"; - } else if (cell->type == ID($check)) { - std::string flavor = cell->getParam(ID::FLAVOR).decode_string(); - f << indent << "performer->on_check("; - if (flavor == "assert") - f << "flavor::ASSERT"; - else if (flavor == "assume") - f << "flavor::ASSUME"; - else if (flavor == "live") - f << "flavor::ASSERT_EVENTUALLY"; - else if (flavor == "fair") - f << "flavor::ASSUME_EVENTUALLY"; - else if (flavor == "cover") - f << "flavor::COVER"; - else log_assert(false); - f << ", condition, formatter, attributes);\n"; - } else log_assert(false); - dec_indent(); - f << indent << "} else {\n"; - inc_indent(); - if (cell->type == ID($print)) { - f << indent << print_output << " << formatter();\n"; - } else if (cell->type == ID($check)) { - std::string flavor = cell->getParam(ID::FLAVOR).decode_string(); - if (flavor == "assert" || flavor == "assume") { - f << indent << "if (!condition) {\n"; - inc_indent(); - f << indent << "std::cerr << formatter();\n"; - dec_indent(); - f << indent << "}\n"; - f << indent << "CXXRTL_ASSERT(condition && \"Check failed\");\n"; - } - } else log_assert(false); - dec_indent(); - f << indent << "}\n"; - dec_indent(); - f << indent << "}\n"; - } - void dump_cell_eval(const RTLIL::Cell *cell, bool for_debug = false) { std::vector inlined_cells; @@ -1376,38 +1202,6 @@ struct CxxrtlWorker { f << " = "; dump_cell_expr(cell, for_debug); f << ";\n"; - // Effectful cells - } else if (is_effectful_cell(cell->type)) { - log_assert(!for_debug); - - // Sync effectful cells are grouped into EFFECT_SYNC nodes in the FlowGraph. - log_assert(!cell->getParam(ID::TRG_ENABLE).as_bool() || (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)); - - if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async effectful cell - f << indent << "auto " << mangle(cell) << "_next = "; - dump_sigspec_rhs(cell->getPort(ID::EN)); - f << ".concat("; - if (cell->type == ID($print)) - dump_sigspec_rhs(cell->getPort(ID::ARGS)); - else if (cell->type == ID($check)) - dump_sigspec_rhs(cell->getPort(ID::A)); - else log_assert(false); - f << ").val();\n"; - - f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_next) {\n"; - inc_indent(); - dump_effect(cell); - f << indent << mangle(cell) << " = " << mangle(cell) << "_next;\n"; - dec_indent(); - f << indent << "}\n"; - } else { // initial effectful cell - f << indent << "if (!" << mangle(cell) << ") {\n"; - inc_indent(); - dump_effect(cell); - f << indent << mangle(cell) << " = value<1>{1u};\n"; - dec_indent(); - f << indent << "}\n"; - } // Flip-flops } else if (is_ff_cell(cell->type)) { log_assert(!for_debug); @@ -1504,7 +1298,7 @@ struct CxxrtlWorker { f << indent; dump_sigspec_lhs(cell->getPort(ID::Q)); f << " = "; - dump_sigspec_rhs(cell->getPort(ID::Q)); + dump_sigspec_lhs(cell->getPort(ID::Q)); f << ".update("; dump_const(RTLIL::Const(RTLIL::S1, cell->getParam(ID::WIDTH).as_int())); f << ", "; @@ -1516,7 +1310,7 @@ struct CxxrtlWorker { f << indent; dump_sigspec_lhs(cell->getPort(ID::Q)); f << " = "; - dump_sigspec_rhs(cell->getPort(ID::Q)); + dump_sigspec_lhs(cell->getPort(ID::Q)); f << ".update("; dump_const(RTLIL::Const(RTLIL::S0, cell->getParam(ID::WIDTH).as_int())); f << ", "; @@ -1527,9 +1321,8 @@ struct CxxrtlWorker { } else if (is_internal_cell(cell->type)) { log_cmd_error("Unsupported internal cell `%s'.\n", cell->type.c_str()); // User cells - } else if (for_debug) { - // Outlines are called on demand when computing the value of a debug item. Nothing to do here. } else { + log_assert(!for_debug); log_assert(cell->known()); bool buffered_inputs = false; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; @@ -1589,11 +1382,11 @@ struct CxxrtlWorker { }; if (buffered_inputs) { // If we have any buffered inputs, there's no chance of converging immediately. - f << indent << mangle(cell) << access << "eval(performer);\n"; + f << indent << mangle(cell) << access << "eval();\n"; f << indent << "converged = false;\n"; assign_from_outputs(/*cell_converged=*/false); } else { - f << indent << "if (" << mangle(cell) << access << "eval(performer)) {\n"; + f << indent << "if (" << mangle(cell) << access << "eval()) {\n"; inc_indent(); assign_from_outputs(/*cell_converged=*/true); dec_indent(); @@ -1787,47 +1580,6 @@ struct CxxrtlWorker { } } - void dump_cell_effect_sync(std::vector &cells) - { - log_assert(!cells.empty()); - const auto &trg = cells[0]->getPort(ID::TRG); - const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY); - - f << indent << "if ("; - for (int i = 0; i < trg.size(); i++) { - RTLIL::SigBit trg_bit = trg[i]; - trg_bit = sigmaps[trg_bit.wire->module](trg_bit); - log_assert(trg_bit.wire); - - if (i != 0) - f << " || "; - - if (trg_polarity[i] == State::S1) - f << "posedge_"; - else - f << "negedge_"; - f << mangle(trg_bit); - } - f << ") {\n"; - inc_indent(); - std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) { - return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int(); - }); - for (auto cell : cells) { - log_assert(cell->getParam(ID::TRG_ENABLE).as_bool()); - log_assert(cell->getPort(ID::TRG) == trg); - log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity); - - std::vector inlined_cells; - collect_cell_eval(cell, /*for_debug=*/false, inlined_cells); - dump_inlined_cells(inlined_cells); - dump_effect(cell); - } - dec_indent(); - - f << indent << "}\n"; - } - void dump_mem_rdport(const Mem *mem, int portidx, bool for_debug = false) { auto &port = mem->rd_ports[portidx]; @@ -2147,10 +1899,6 @@ struct CxxrtlWorker { } } for (auto cell : module->cells()) { - // Async and initial effectful cells have additional state, which must be reset as well. - if (is_effectful_cell(cell->type)) - if (!cell->getParam(ID::TRG_ENABLE).as_bool() || cell->getParam(ID::TRG_WIDTH).as_int() == 0) - f << indent << mangle(cell) << " = {};\n"; if (is_internal_cell(cell->type)) continue; f << indent << mangle(cell); @@ -2198,9 +1946,6 @@ struct CxxrtlWorker { case FlowGraph::Node::Type::CELL_EVAL: dump_cell_eval(node.cell); break; - case FlowGraph::Node::Type::EFFECT_SYNC: - dump_cell_effect_sync(node.cells); - break; case FlowGraph::Node::Type::PROCESS_CASE: dump_process_case(node.process); break; @@ -2264,116 +2009,27 @@ struct CxxrtlWorker { if (wire_type.type == WireType::MEMBER && edge_wires[wire]) f << indent << "prev_" << mangle(wire) << " = " << mangle(wire) << ";\n"; if (wire_type.is_buffered()) - f << indent << "if (" << mangle(wire) << ".commit(observer)) changed = true;\n"; + f << indent << "if (" << mangle(wire) << ".commit()) changed = true;\n"; } if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { for (auto &mem : mod_memories[module]) { if (!writable_memories.count({module, mem.memid})) continue; - f << indent << "if (" << mangle(&mem) << ".commit(observer)) changed = true;\n"; + f << indent << "if (" << mangle(&mem) << ".commit()) changed = true;\n"; } for (auto cell : module->cells()) { if (is_internal_cell(cell->type)) continue; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; - f << indent << "if (" << mangle(cell) << access << "commit(observer)) changed = true;\n"; + f << indent << "if (" << mangle(cell) << access << "commit()) changed = true;\n"; } } f << indent << "return changed;\n"; dec_indent(); } - 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()"; - } 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); - if (serialize) { - dump_serialized_metadata(attributes); - } else { - dump_metadata_map(attributes); - } - } - void dump_debug_info_method(RTLIL::Module *module) { - size_t count_scopes = 0; size_t count_public_wires = 0; size_t count_member_wires = 0; size_t count_undriven = 0; @@ -2386,195 +2042,139 @@ struct CxxrtlWorker { size_t count_skipped_wires = 0; inc_indent(); f << indent << "assert(path.empty() || path[path.size() - 1] == ' ');\n"; - f << indent << "if (scopes) {\n"; - inc_indent(); - // The module is responsible for adding its own scope. - f << indent << "scopes->add(path.empty() ? path : path.substr(0, path.size() - 1), "; - f << escape_cxx_string(get_hdl_name(module)) << ", "; - dump_debug_attrs(module, /*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. - for (auto cell : module->cells()) { - if (cell->type != ID($scopeinfo)) continue; - if (cell->getParam(ID::TYPE).decode_string() == "module") { - auto module_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Module); - auto cell_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Cell); - cell_attrs.erase(ID::module_not_derived); - f << indent << "scopes->add(path, " << escape_cxx_string(get_hdl_name(cell)) << ", "; - f << escape_cxx_string(cell->get_string_attribute(ID(module))) << ", "; - dump_serialized_metadata(module_attrs); - f << ", "; - dump_serialized_metadata(cell_attrs); - f << ");\n"; - } else log_assert(false && "Unknown $scopeinfo type"); - count_scopes++; - } - dec_indent(); - f << indent << "}\n"; - f << indent << "if (items) {\n"; - inc_indent(); - for (auto wire : module->wires()) { - const auto &debug_wire_type = debug_wire_types[wire]; - if (!wire->name.isPublic()) - continue; - count_public_wires++; - switch (debug_wire_type.type) { - case WireType::BUFFERED: - case WireType::MEMBER: { - // Member wire - std::vector flags; - - if (wire->port_input && wire->port_output) - flags.push_back("INOUT"); - else if (wire->port_output) - flags.push_back("OUTPUT"); - else if (wire->port_input) - flags.push_back("INPUT"); - - bool has_driven_sync = false; - bool has_driven_comb = false; - bool has_undriven = false; - if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { - for (auto bit : SigSpec(wire)) - if (!bit_has_state.count(bit)) - has_undriven = true; - else if (bit_has_state[bit]) - has_driven_sync = true; - else - has_driven_comb = true; - } else if (wire->port_output) { - switch (cxxrtl_port_type(module, wire->name)) { - case CxxrtlPortType::SYNC: - has_driven_sync = true; - break; - case CxxrtlPortType::COMB: - has_driven_comb = true; - break; - case CxxrtlPortType::UNKNOWN: - has_driven_sync = has_driven_comb = true; - break; - } - } else { - has_undriven = true; - } - if (has_undriven) - flags.push_back("UNDRIVEN"); - if (!has_driven_sync && !has_driven_comb && has_undriven) - count_undriven++; - if (has_driven_sync) - flags.push_back("DRIVEN_SYNC"); - if (has_driven_sync && !has_driven_comb && !has_undriven) - count_driven_sync++; - if (has_driven_comb) - flags.push_back("DRIVEN_COMB"); - if (!has_driven_sync && has_driven_comb && !has_undriven) - count_driven_comb++; - if (has_driven_sync + has_driven_comb + has_undriven > 1) - count_mixed_driver++; - - f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; - 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; - } + for (auto wire : module->wires()) { + const auto &debug_wire_type = debug_wire_types[wire]; + if (!wire->name.isPublic()) + continue; + count_public_wires++; + switch (debug_wire_type.type) { + case WireType::BUFFERED: + case WireType::MEMBER: { + // Member wire + std::vector flags; + + if (wire->port_input && wire->port_output) + flags.push_back("INOUT"); + else if (wire->port_output) + flags.push_back("OUTPUT"); + else if (wire->port_input) + flags.push_back("INPUT"); + + bool has_driven_sync = false; + bool has_driven_comb = false; + bool has_undriven = false; + if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { + for (auto bit : SigSpec(wire)) + if (!bit_has_state.count(bit)) + has_undriven = true; + else if (bit_has_state[bit]) + has_driven_sync = true; + else + has_driven_comb = true; + } else if (wire->port_output) { + switch (cxxrtl_port_type(module, wire->name)) { + case CxxrtlPortType::SYNC: + has_driven_sync = true; + break; + case CxxrtlPortType::COMB: + has_driven_comb = true; + break; + case CxxrtlPortType::UNKNOWN: + has_driven_sync = has_driven_comb = true; + break; } - f << ");\n"; - count_member_wires++; - break; - } - case WireType::ALIAS: { - // Alias of a member wire - const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); - f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; - 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); - if (wire->start_offset != 0) - f << ", " << wire->start_offset; - f << ");\n"; - count_alias_wires++; - break; - } - case WireType::CONST: { - // Wire tied to a constant - f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; - dump_const(debug_wire_type.sig_subst.as_const()); - f << ";\n"; - f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", "; - 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)) << ", "; - 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; + } else { + has_undriven = true; } - default: { - // Localized or inlined wire with no debug information - count_skipped_wires++; - break; + if (has_undriven) + flags.push_back("UNDRIVEN"); + if (!has_driven_sync && !has_driven_comb && has_undriven) + count_undriven++; + if (has_driven_sync) + flags.push_back("DRIVEN_SYNC"); + if (has_driven_sync && !has_driven_comb && !has_undriven) + count_driven_sync++; + if (has_driven_comb) + flags.push_back("DRIVEN_COMB"); + if (!has_driven_sync && has_driven_comb && !has_undriven) + count_driven_comb++; + if (has_driven_sync + has_driven_comb + has_undriven > 1) + count_mixed_driver++; + + f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset; + bool first = true; + for (auto flag : flags) { + if (first) { + first = false; + f << ", "; + } else { + f << "|"; + } + f << "debug_item::" << flag; } + f << "));\n"; + count_member_wires++; + break; } - } - if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { - for (auto &mem : mod_memories[module]) { - if (!mem.memid.isPublic()) - continue; - f << indent << "items->add(path, " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)) << ", "; - if (mem.packed) { - dump_debug_attrs(mem.cell); - } else { - dump_debug_attrs(mem.mem); - } - f << ", " << mangle(&mem) << ", "; - f << mem.start_offset << ");\n"; + case WireType::ALIAS: { + // Alias of a member wire + const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire(); + f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item("; + // If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream + // tooling has no way to find out about the outline. + if (debug_wire_types[aliasee].is_outline()) + f << "debug_eval_outline"; + else + f << "debug_alias()"; + f << ", " << mangle(aliasee) << ", " << wire->start_offset << "));\n"; + count_alias_wires++; + break; + } + case WireType::CONST: { + // Wire tied to a constant + f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = "; + dump_const(debug_wire_type.sig_subst.as_const()); + f << ";\n"; + f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); + f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "));\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 << "));\n"; + count_inline_wires++; + break; + } + default: { + // Localized or inlined wire with no debug information + count_skipped_wires++; + break; } } - dec_indent(); - f << indent << "}\n"; + } if (!module->get_bool_attribute(ID(cxxrtl_blackbox))) { + for (auto &mem : mod_memories[module]) { + if (!mem.memid.isPublic()) + continue; + f << indent << "items.add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)); + f << ", debug_item(" << mangle(&mem) << ", "; + f << mem.start_offset << "));\n"; + } for (auto cell : module->cells()) { if (is_internal_cell(cell->type)) continue; const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : "."; - f << indent << mangle(cell) << access; - f << "debug_info(items, scopes, path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ", "; - dump_debug_attrs(cell, /*serialize=*/false); - f << ");\n"; + f << indent << mangle(cell) << access << "debug_info(items, "; + f << "path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ");\n"; } } dec_indent(); log_debug("Debug information statistics for module `%s':\n", log_id(module)); - log_debug(" Scopes: %zu", count_scopes); log_debug(" Public wires: %zu, of which:\n", count_public_wires); log_debug(" Member wires: %zu, of which:\n", count_member_wires); log_debug(" Undriven: %zu (incl. inputs)\n", count_undriven); @@ -2590,6 +2190,33 @@ struct CxxrtlWorker { } } + 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.begins_with("\\")) + continue; + f << indent << "{ " << escape_cxx_string(metadata_item.first.str().substr(1)) << ", "; + 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 { + f << metadata_item.second.as_int(/*is_signed=*/metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED); + if (!(metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED)) + f << "u"; + } + f << " },\n"; + } + dec_indent(); + f << indent << "})"; + } + void dump_module_intf(RTLIL::Module *module) { dump_attrs(module); @@ -2607,27 +2234,20 @@ struct CxxrtlWorker { dump_reset_method(module); f << indent << "}\n"; f << "\n"; - // No default argument, to prevent unintentional `return bb_foo::eval();` calls that drop performer. - f << indent << "bool eval(performer *performer) override {\n"; + f << indent << "bool eval() override {\n"; dump_eval_method(module); f << indent << "}\n"; f << "\n"; - f << indent << "virtual bool commit(observer &observer) {\n"; + f << indent << "bool commit() override {\n"; dump_commit_method(module); f << indent << "}\n"; f << "\n"; - f << indent << "bool commit() override {\n"; - f << indent << indent << "observer observer;\n"; - f << indent << indent << "return commit(observer);\n"; - f << indent << "}\n"; if (debug_info) { - f << "\n"; - f << indent << "void debug_info(debug_items *items, debug_scopes *scopes, " - << "std::string path, metadata_map &&cell_attrs = {}) override {\n"; + f << indent << "void debug_info(debug_items &items, std::string path = \"\") override {\n"; dump_debug_info_method(module); f << indent << "}\n"; + f << "\n"; } - f << "\n"; f << indent << "static std::unique_ptr<" << mangle(module); f << template_params(module, /*is_decl=*/false) << "> "; f << "create(std::string name, metadata_map parameters, metadata_map attributes);\n"; @@ -2671,15 +2291,6 @@ struct CxxrtlWorker { f << "\n"; bool has_cells = false; for (auto cell : module->cells()) { - // Async and initial effectful cells have additional state, which requires storage. - if (is_effectful_cell(cell->type)) { - if (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0) - f << indent << "value<1> " << mangle(cell) << ";\n"; // async initial cell - if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($print)) - f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n"; // {EN, ARGS} - if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($check)) - f << indent << "value<2> " << mangle(cell) << ";\n"; // {EN, A} - } if (is_internal_cell(cell->type)) continue; dump_attrs(cell); @@ -2708,18 +2319,8 @@ struct CxxrtlWorker { f << indent << "};\n"; f << "\n"; f << indent << "void reset() override;\n"; - f << "\n"; - f << indent << "bool eval(performer *performer = nullptr) override;\n"; - f << "\n"; - f << indent << "template\n"; - f << indent << "bool commit(ObserverT &observer) {\n"; - dump_commit_method(module); - f << indent << "}\n"; - f << "\n"; - f << indent << "bool commit() override {\n"; - f << indent << indent << "observer observer;\n"; - f << indent << indent << "return commit<>(observer);\n"; - f << indent << "}\n"; + f << indent << "bool eval() override;\n"; + f << indent << "bool commit() override;\n"; if (debug_info) { if (debug_eval) { f << "\n"; @@ -2732,8 +2333,7 @@ struct CxxrtlWorker { } } f << "\n"; - f << indent << "void debug_info(debug_items *items, debug_scopes *scopes, " - << "std::string path, metadata_map &&cell_attrs = {}) override;\n"; + f << indent << "void debug_info(debug_items &items, std::string path = \"\") override;\n"; } dec_indent(); f << indent << "}; // struct " << mangle(module) << "\n"; @@ -2749,24 +2349,27 @@ struct CxxrtlWorker { dump_reset_method(module); f << indent << "}\n"; f << "\n"; - f << indent << "bool " << mangle(module) << "::eval(performer *performer) {\n"; + f << indent << "bool " << mangle(module) << "::eval() {\n"; dump_eval_method(module); f << indent << "}\n"; + f << "\n"; + f << indent << "bool " << mangle(module) << "::commit() {\n"; + dump_commit_method(module); + f << indent << "}\n"; + f << "\n"; if (debug_info) { if (debug_eval) { - f << "\n"; f << indent << "void " << mangle(module) << "::debug_eval() {\n"; dump_debug_eval_method(module); f << indent << "}\n"; + f << "\n"; } - f << "\n"; f << indent << "CXXRTL_EXTREMELY_COLD\n"; - f << indent << "void " << mangle(module) << "::debug_info(debug_items *items, debug_scopes *scopes, " - << "std::string path, metadata_map &&cell_attrs) {\n"; + f << indent << "void " << mangle(module) << "::debug_info(debug_items &items, std::string path) {\n"; dump_debug_info_method(module); f << indent << "}\n"; + f << "\n"; } - f << "\n"; } void dump_design(RTLIL::Design *design) @@ -2806,7 +2409,7 @@ struct CxxrtlWorker { f << "#define " << include_guard << "\n"; f << "\n"; if (top_module != nullptr && debug_info) { - f << "#include \n"; + f << "#include \n"; f << "\n"; f << "#ifdef __cplusplus\n"; f << "extern \"C\" {\n"; @@ -2824,7 +2427,7 @@ struct CxxrtlWorker { } f << "#ifdef __cplusplus\n"; f << "\n"; - f << "#include \n"; + f << "#include \n"; f << "\n"; f << "using namespace cxxrtl;\n"; f << "\n"; @@ -2841,17 +2444,17 @@ struct CxxrtlWorker { } if (split_intf) - f << "#include \"" << basename(intf_filename) << "\"\n"; + f << "#include \"" << intf_filename << "\"\n"; else - f << "#include \n"; + f << "#include \n"; f << "\n"; f << "#if defined(CXXRTL_INCLUDE_CAPI_IMPL) || \\\n"; f << " defined(CXXRTL_INCLUDE_VCD_CAPI_IMPL)\n"; - f << "#include \n"; + f << "#include \n"; f << "#endif\n"; f << "\n"; f << "#if defined(CXXRTL_INCLUDE_VCD_CAPI_IMPL)\n"; - f << "#include \n"; + f << "#include \n"; f << "#endif\n"; f << "\n"; f << "using namespace cxxrtl_yosys;\n"; @@ -2998,16 +2601,6 @@ struct CxxrtlWorker { register_edge_signal(sigmap, cell->getPort(ID::CLK), cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn); } - - // Effectful cells may be triggered on posedge/negedge events. - if (is_effectful_cell(cell->type) && cell->getParam(ID::TRG_ENABLE).as_bool()) { - for (size_t i = 0; i < (size_t)cell->getParam(ID::TRG_WIDTH).as_int(); i++) { - RTLIL::SigBit trg = cell->getPort(ID::TRG).extract(i, 1); - if (is_valid_clock(trg)) - register_edge_signal(sigmap, trg, - cell->parameters[ID::TRG_POLARITY][i] == RTLIL::S1 ? RTLIL::STp : RTLIL::STn); - } - } } for (auto &mem : memories) { @@ -3141,12 +2734,8 @@ struct CxxrtlWorker { // Discover nodes reachable from primary outputs (i.e. members) and collect reachable wire users. pool worklist; for (auto node : flow.nodes) { - if (node->type == FlowGraph::Node::Type::CELL_EVAL && !is_internal_cell(node->cell->type)) - worklist.insert(node); // node evaluates a submodule - else if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type)) - worklist.insert(node); // node has async effects - else if (node->type == FlowGraph::Node::Type::EFFECT_SYNC) - worklist.insert(node); // node has sync effects + if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type)) + worklist.insert(node); // node has effects else if (node->type == FlowGraph::Node::Type::MEM_WRPORTS) worklist.insert(node); // node is memory write else if (node->type == FlowGraph::Node::Type::PROCESS_SYNC && is_memwr_process(node->process)) @@ -3203,23 +2792,9 @@ struct CxxrtlWorker { } // Emit reachable nodes in eval(). - // Accumulate sync effectful cells per trigger condition. - dict, std::vector> effect_sync_cells; for (auto node : node_order) - if (live_nodes[node]) { - if (node->type == FlowGraph::Node::Type::CELL_EVAL && - is_effectful_cell(node->cell->type) && - node->cell->getParam(ID::TRG_ENABLE).as_bool() && - node->cell->getParam(ID::TRG_WIDTH).as_int() != 0) - effect_sync_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell); - else - schedule[module].push_back(*node); - } - - for (auto &it : effect_sync_cells) { - auto node = flow.add_effect_sync_node(it.second); - schedule[module].push_back(*node); - } + if (live_nodes[node]) + schedule[module].push_back(*node); // For maximum performance, the state of the simulation (which is the same as the set of its double buffered // wires, since using a singly buffered wire for any kind of state introduces a race condition) should contain @@ -3263,7 +2838,6 @@ 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); @@ -3524,8 +3098,7 @@ struct CxxrtlBackend : public Backend { log(" value<8> p_i_data;\n"); log(" wire<8> p_o_data;\n"); log("\n"); - log(" bool eval(performer *performer) override;\n"); - log(" virtual bool commit(observer &observer);\n"); + log(" bool eval() override;\n"); log(" bool commit() override;\n"); log("\n"); log(" static std::unique_ptr\n"); @@ -3538,11 +3111,11 @@ struct CxxrtlBackend : public Backend { log(" namespace cxxrtl_design {\n"); log("\n"); log(" struct stderr_debug : public bb_p_debug {\n"); - log(" bool eval(performer *performer) override {\n"); + log(" bool eval() override {\n"); log(" if (posedge_p_clk() && p_en)\n"); log(" fprintf(stderr, \"debug: %%02x\\n\", p_i_data.data[0]);\n"); log(" p_o_data.next = p_i_data;\n"); - log(" return bb_p_debug::eval(performer);\n"); + log(" return bb_p_debug::eval();\n"); log(" }\n"); log(" };\n"); log("\n"); @@ -3640,11 +3213,6 @@ struct CxxrtlBackend : public Backend { log(" place the generated code into namespace . if not specified,\n"); log(" \"cxxrtl_design\" is used.\n"); log("\n"); - log(" -print-output \n"); - log(" $print cells in the generated code direct their output to .\n"); - log(" must be one of \"std::cout\", \"std::cerr\". if not specified,\n"); - log(" \"std::cout\" is used. explicitly provided performer overrides this.\n"); - log("\n"); log(" -nohierarchy\n"); log(" use design hierarchy as-is. in most designs, a top module should be\n"); log(" present as it is exposed through the C API and has unbuffered outputs\n"); @@ -3783,14 +3351,6 @@ struct CxxrtlBackend : public Backend { worker.design_ns = args[++argidx]; continue; } - if (args[argidx] == "-print-output" && argidx+1 < args.size()) { - worker.print_output = args[++argidx]; - if (!(worker.print_output == "std::cout" || worker.print_output == "std::cerr")) { - log_cmd_error("Invalid output stream \"%s\".\n", worker.print_output.c_str()); - worker.print_output = "std::cout"; - } - continue; - } break; } extra_args(f, filename, args, argidx); diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc b/yosys/backends/cxxrtl/cxxrtl_capi.cc similarity index 58% rename from yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc rename to yosys/backends/cxxrtl/cxxrtl_capi.cc index 34801c2d118..227173ba87f 100644 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.cc +++ b/yosys/backends/cxxrtl/cxxrtl_capi.cc @@ -16,10 +16,10 @@ * */ -// This file is a part of the CXXRTL C API. It should be used together with `cxxrtl/capi/cxxrtl_capi.h`. +// This file is a part of the CXXRTL C API. It should be used together with `cxxrtl_capi.h`. -#include -#include +#include +#include struct _cxxrtl_handle { std::unique_ptr module; @@ -35,19 +35,19 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design) { return cxxrtl_create_at(design, ""); } -cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path_) { - std::string top_path = top_path_; - if (!top_path.empty()) { +cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *root) { + std::string path = root; + if (!path.empty()) { // module::debug_info() accepts either an empty path, or a path ending in space to simplify // the logic in generated code. While this is sketchy at best to expose in the C++ API, this // would be a lot worse in the C API, so don't expose it here. - assert(top_path.back() != ' '); - top_path += ' '; + assert(path.back() != ' '); + path += ' '; } cxxrtl_handle handle = new _cxxrtl_handle; handle->module = std::move(design->module); - handle->module->debug_info(&handle->objects, nullptr, top_path); + handle->module->debug_info(handle->objects, path); delete design; return handle; } @@ -90,46 +90,3 @@ void cxxrtl_enum(cxxrtl_handle handle, void *data, void cxxrtl_outline_eval(cxxrtl_outline outline) { outline->eval(); } - -int cxxrtl_attr_type(cxxrtl_attr_set attrs_, const char *name) { - auto attrs = (cxxrtl::metadata_map*)attrs_; - if (!attrs->count(name)) - return CXXRTL_ATTR_NONE; - switch (attrs->at(name).value_type) { - case cxxrtl::metadata::UINT: - return CXXRTL_ATTR_UNSIGNED_INT; - case cxxrtl::metadata::SINT: - return CXXRTL_ATTR_SIGNED_INT; - case cxxrtl::metadata::STRING: - return CXXRTL_ATTR_STRING; - case cxxrtl::metadata::DOUBLE: - return CXXRTL_ATTR_DOUBLE; - default: - // Present unsupported attribute type the same way as no attribute at all. - return CXXRTL_ATTR_NONE; - } -} - -uint64_t cxxrtl_attr_get_unsigned_int(cxxrtl_attr_set attrs_, const char *name) { - auto &attrs = *(cxxrtl::metadata_map*)attrs_; - assert(attrs.count(name) && attrs.at(name).value_type == cxxrtl::metadata::UINT); - return attrs[name].as_uint(); -} - -int64_t cxxrtl_attr_get_signed_int(cxxrtl_attr_set attrs_, const char *name) { - auto &attrs = *(cxxrtl::metadata_map*)attrs_; - assert(attrs.count(name) && attrs.at(name).value_type == cxxrtl::metadata::SINT); - return attrs[name].as_sint(); -} - -const char *cxxrtl_attr_get_string(cxxrtl_attr_set attrs_, const char *name) { - auto &attrs = *(cxxrtl::metadata_map*)attrs_; - assert(attrs.count(name) && attrs.at(name).value_type == cxxrtl::metadata::STRING); - return attrs[name].as_string().c_str(); -} - -double cxxrtl_attr_get_double(cxxrtl_attr_set attrs_, const char *name) { - auto &attrs = *(cxxrtl::metadata_map*)attrs_; - assert(attrs.count(name) && attrs.at(name).value_type == cxxrtl::metadata::DOUBLE); - return attrs[name].as_double(); -} diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h b/yosys/backends/cxxrtl/cxxrtl_capi.h similarity index 80% rename from yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h rename to yosys/backends/cxxrtl/cxxrtl_capi.h index ae42733ad7f..2df2b7287f4 100644 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h +++ b/yosys/backends/cxxrtl/cxxrtl_capi.h @@ -55,8 +55,8 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design); // Create a design handle at a given hierarchy position from a design toplevel. // // This operation is similar to `cxxrtl_create`, except the full hierarchical name of every object -// is prepended with `top_path`. -cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *top_path); +// is prepended with `root`. +cxxrtl_handle cxxrtl_create_at(cxxrtl_toplevel design, const char *root); // Release all resources used by a design and its handle. void cxxrtl_destroy(cxxrtl_handle handle); @@ -240,11 +240,6 @@ struct cxxrtl_object { // through wires, the bits are double buffered. To avoid race conditions, user code should // always read from `curr` and write to `next`. The `curr` pointer is always valid; for objects // that cannot be modified, or cannot be modified in a race-free way, `next` is NULL. - // - // In case where `width == 0`, `curr` is a non-NULL pointer unique for the wire. That is, - // there is a 1-to-1 correspondence between simulation objects and `curr` pointers, regardless - // of whether they have storage or not. (Aliases' `curr` pointer equals that of some other - // simulated object.) uint32_t *curr; uint32_t *next; @@ -254,15 +249,6 @@ struct cxxrtl_object { // this field to NULL. struct _cxxrtl_outline *outline; - // Opaque reference to an attribute set. - // - // See the documentation of `cxxrtl_attr_set` for details. When creating a `cxxrtl_object`, set - // this field to NULL. - // - // The lifetime of the pointers returned by `cxxrtl_attr_*` family of functions is the same as - // the lifetime of this structure. - struct _cxxrtl_attr_set *attrs; - // More description fields may be added in the future, but the existing ones will never change. }; @@ -318,62 +304,6 @@ typedef struct _cxxrtl_outline *cxxrtl_outline; // re-evaluated, otherwise the bits read from that object are meaningless. void cxxrtl_outline_eval(cxxrtl_outline outline); -// Opaque reference to an attribute set. -// -// An attribute set is a map between attribute names (always strings) and values (which may have -// several different types). To find out the type of an attribute, use `cxxrtl_attr_type`, and -// to retrieve the value of an attribute, use `cxxrtl_attr_as_string`. -typedef struct _cxxrtl_attr_set *cxxrtl_attr_set; - -// Type of an attribute. -enum cxxrtl_attr_type { - // Attribute is not present. - CXXRTL_ATTR_NONE = 0, - - // Attribute has an unsigned integer value. - CXXRTL_ATTR_UNSIGNED_INT = 1, - - // Attribute has an unsigned integer value. - CXXRTL_ATTR_SIGNED_INT = 2, - - // Attribute has a string value. - CXXRTL_ATTR_STRING = 3, - - // Attribute has a double precision floating point value. - CXXRTL_ATTR_DOUBLE = 4, - - // More attribute types may be defined in the future, but the existing values will never change. -}; - -// Determine the presence and type of an attribute in an attribute set. -// -// This function returns one of the possible `cxxrtl_attr_type` values. -int cxxrtl_attr_type(cxxrtl_attr_set attrs, const char *name); - -// Retrieve an unsigned integer valued attribute from an attribute set. -// -// This function asserts that `cxxrtl_attr_type(attrs, name) == CXXRTL_ATTR_UNSIGNED_INT`. -// If assertions are disabled, returns 0 if the attribute is missing or has an incorrect type. -uint64_t cxxrtl_attr_get_unsigned_int(cxxrtl_attr_set attrs, const char *name); - -// Retrieve a signed integer valued attribute from an attribute set. -// -// This function asserts that `cxxrtl_attr_type(attrs, name) == CXXRTL_ATTR_SIGNED_INT`. -// If assertions are disabled, returns 0 if the attribute is missing or has an incorrect type. -int64_t cxxrtl_attr_get_signed_int(cxxrtl_attr_set attrs, const char *name); - -// Retrieve a string valued attribute from an attribute set. The returned string is zero-terminated. -// -// This function asserts that `cxxrtl_attr_type(attrs, name) == CXXRTL_ATTR_STRING`. If assertions -// are disabled, returns NULL if the attribute is missing or has an incorrect type. -const char *cxxrtl_attr_get_string(cxxrtl_attr_set attrs, const char *name); - -// Retrieve a double precision floating point valued attribute from an attribute set. -// -// This function asserts that `cxxrtl_attr_type(attrs, name) == CXXRTL_ATTR_DOUBLE`. If assertions -// are disabled, returns NULL if the attribute is missing or has an incorrect type. -double cxxrtl_attr_get_double(cxxrtl_attr_set attrs, const char *name); - #ifdef __cplusplus } #endif diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h b/yosys/backends/cxxrtl/cxxrtl_vcd.h similarity index 99% rename from yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h rename to yosys/backends/cxxrtl/cxxrtl_vcd.h index cb2ccf5fc26..b76922bbd8a 100644 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_vcd.h +++ b/yosys/backends/cxxrtl/cxxrtl_vcd.h @@ -19,7 +19,7 @@ #ifndef CXXRTL_VCD_H #define CXXRTL_VCD_H -#include +#include namespace cxxrtl { diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc b/yosys/backends/cxxrtl/cxxrtl_vcd_capi.cc similarity index 95% rename from yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc rename to yosys/backends/cxxrtl/cxxrtl_vcd_capi.cc index 0949a9363eb..52a9198b869 100644 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.cc +++ b/yosys/backends/cxxrtl/cxxrtl_vcd_capi.cc @@ -16,10 +16,10 @@ * */ -// This file is a part of the CXXRTL C API. It should be used together with `cxxrtl/capi/cxxrtl_capi_vcd.h`. +// This file is a part of the CXXRTL C API. It should be used together with `cxxrtl_vcd_capi.h`. -#include -#include +#include +#include extern const cxxrtl::debug_items &cxxrtl_debug_items_from_handle(cxxrtl_handle handle); diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h b/yosys/backends/cxxrtl/cxxrtl_vcd_capi.h similarity index 97% rename from yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h rename to yosys/backends/cxxrtl/cxxrtl_vcd_capi.h index 844f3cb8c83..d55afe2230e 100644 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_vcd.h +++ b/yosys/backends/cxxrtl/cxxrtl_vcd_capi.h @@ -16,8 +16,8 @@ * */ -#ifndef CXXRTL_CAPI_VCD_H -#define CXXRTL_CAPI_VCD_H +#ifndef CXXRTL_VCD_CAPI_H +#define CXXRTL_VCD_CAPI_H // This file is a part of the CXXRTL C API. It should be used together with `cxxrtl_vcd_capi.cc`. // @@ -27,7 +27,7 @@ #include #include -#include +#include #ifdef __cplusplus extern "C" { diff --git a/yosys/backends/cxxrtl/runtime/README.txt b/yosys/backends/cxxrtl/runtime/README.txt deleted file mode 100644 index 9ae7051cdcc..00000000000 --- a/yosys/backends/cxxrtl/runtime/README.txt +++ /dev/null @@ -1,18 +0,0 @@ -This directory contains the runtime components of CXXRTL and should be placed on the include path -when building the simulation using the `-I${YOSYS}/backends/cxxrtl/runtime` option. These components -are not used in the Yosys binary; they are only built as a part of the simulation binary. - -The interfaces declared in `cxxrtl_capi*.h` contain the stable C API. These interfaces will not be -changed in backward-incompatible ways unless no other option is available, and any breaking changes -will be made in a way that causes the downstream code to fail in a visible way. The ABI of these -interfaces is considered stable as well, and it will not use features complicating its use via -libraries such as libffi or ctypes. - -The implementations in `cxxrtl_capi*.cc` are considered private; they are still placed in the include -path to enable build-system-less builds (where the CXXRTL runtime component is included in the C++ -file of the simulation toplevel). - -The interfaces declared in `cxxrtl*.h` (without `capi`) are unstable and may change without notice. - -For clarity, all of the files in this directory and its subdirectories have unique names regardless -of the directory where they are placed. \ No newline at end of file diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h deleted file mode 100644 index 9aa3e105d2c..00000000000 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ /dev/null @@ -1,873 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2023 Catherine - * - * Permission to use, copy, modify, and/or distribute this software for any - * purpose with or without fee is hereby granted. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES - * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF - * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR - * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES - * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN - * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF - * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. - * - */ - -#ifndef CXXRTL_REPLAY_H -#define CXXRTL_REPLAY_H - -#if !defined(WIN32) -#include -#define O_BINARY 0 -#else -#include -#endif - -#include -#include -#include -#include -#include - -#include -#include - -// Theory of operation -// =================== -// -// Log format -// ---------- -// -// The replay log is a simple data format based on a sequence of 32-bit words. The following BNF-like grammar describes -// enough detail to understand the overall structure of the log data and be able to read hex dumps. For a greater -// degree of detail see the source code. The format is considered fully internal to CXXRTL and is subject to change -// without notice. -// -// ::= + -// ::= 0x52585843 0x00004c54 -// ::= * -// ::= ( | )* -// ::= 0xc0000000 ... -// ::= 0xc0000001 ... -// ::= 0x0??????? + | 0x1??????? + | 0x2??????? | 0x3??????? -// , ::= 0x???????? -// ::= | | | -// ::= 0xc0000010 -// ::= 0xc0000011 -// ::= 0xc0000012 -// ::= 0xc0000013 -// ::= 0xFFFFFFFF -// -// The replay log contains sample data, however, it does not cover the entire design. Rather, it only contains sample -// data for the subset of debug items containing _design state_: inputs and registers/latches. This keeps its size to -// a minimum, and recording speed to a maximum. The player samples any missing data by setting the design state items -// to the same values they had during recording, and re-evaluating the design. -// -// Packets for diagnostics (prints, breakpoints, assertions, and assumptions) are used solely for diagnostics emitted -// by the C++ testbench driving the simulation, and are not recorded while evaluating the design. (Diagnostics emitted -// by the RTL can be reconstructed at replay time, so recording them would be a waste of space.) -// -// Limits -// ------ -// -// The log may contain: -// -// * Up to 2**28-1 debug items containing design state. -// * Up to 2**32 chunks per debug item. -// * Up to 2**32 rows per memory. -// * Up to 2**32 samples. -// -// Of these limits, the last two are most likely to be eventually exceeded by practical recordings. However, other -// performance considerations will likely limit the size of such practical recordings first, so the log data format -// will undergo a breaking change at that point. -// -// Operations -// ---------- -// -// As suggested by the name "replay log", this format is designed for recording (writing) once and playing (reading) -// many times afterwards, such that reading the format can be done linearly and quickly. The log format is designed to -// support three primary read operations: -// -// 1. Initialization -// 2. Rewinding (to time T) -// 3. Replaying (for N samples) -// -// During initialization, the player establishes the mapping between debug item names and their 28-bit identifiers in -// the log. It is done once. -// -// During rewinding, the player begins reading at the latest non-incremental sample that still lies before the requested -// sample time. It continues reading incremental samples after that point until it reaches the requested sample time. -// This process is very cheap as the design is not evaluated; it is essentially a (convoluted) memory copy operation. -// -// During replaying, the player evaluates the design at the current time, which causes all debug items to assume -// the values they had before recording. This process is expensive. Once done, the player advances to the next state -// by reading the next (complete or incremental) sample, as above. Since a range of samples is replayed, this process -// is repeated several times in a row. -// -// In principle, when replaying, the player could only read the state of the inputs and the time delta and use a normal -// eval/commit loop to progress the simulation, which is fully deterministic so its calculated design state should be -// exactly the same as the recorded design state. In practice, it is both faster and more reliable (in presence of e.g. -// user-defined black boxes) to read the recorded values instead of calculating them. -// -// Note: The operations described above are conceptual and do not correspond exactly to methods on `cxxrtl::player`. -// The `cxxrtl::player::replay()` method does not evaluate the design. This is so that delta cycles could be ignored -// if they are not of interest while replaying. - -namespace cxxrtl { - -// A single diagnostic that can be manipulated as an object (including being written to and read from a file). -// This differs from the base CXXRTL interface, where diagnostics can only be emitted via a procedure call, and are -// not materialized as objects. -struct diagnostic { - // The `BREAK` flavor corresponds to a breakpoint, which is a diagnostic type that can currently only be emitted - // by the C++ testbench code. - enum flavor { - BREAK = 0, - PRINT = 1, - ASSERT = 2, - ASSUME = 3, - }; - - flavor type; - std::string message; - std::string location; // same format as the `src` attribute of `$print` or `$check` cell - - diagnostic() - : type(BREAK) {} - - diagnostic(flavor type, const std::string &message, const std::string &location) - : type(type), message(message), location(location) {} - - diagnostic(flavor type, const std::string &message, const char *file, unsigned line) - : type(type), message(message), location(std::string(file) + ':' + std::to_string(line)) {} -}; - -// A spool stores CXXRTL design state changes in a file. -class spool { -public: - // Unique pointer to a specific sample within a replay log. (Timestamps are not unique.) - typedef uint32_t pointer_t; - - // Numeric identifier assigned to a debug item within a replay log. Range limited to [1, MAXIMUM_IDENT]. - typedef uint32_t ident_t; - - static constexpr uint16_t VERSION = 0x0400; - - static constexpr uint64_t HEADER_MAGIC = 0x00004c5452585843; - static constexpr uint64_t VERSION_MASK = 0xffff000000000000; - - static constexpr uint32_t PACKET_DEFINE = 0xc0000000; - - static constexpr uint32_t PACKET_SAMPLE = 0xc0000001; - enum sample_flag : uint32_t { - EMPTY = 0, - INCREMENTAL = 1, - }; - - static constexpr uint32_t MAXIMUM_IDENT = 0x0fffffff; - static constexpr uint32_t CHANGE_MASK = 0x30000000; - - static constexpr uint32_t PACKET_CHANGE = 0x00000000/* | ident */; - static constexpr uint32_t PACKET_CHANGEI = 0x10000000/* | ident */; - static constexpr uint32_t PACKET_CHANGEL = 0x20000000/* | ident */; - static constexpr uint32_t PACKET_CHANGEH = 0x30000000/* | ident */; - - static constexpr uint32_t PACKET_DIAGNOSTIC = 0xc0000010/* | diagnostic::flavor */; - static constexpr uint32_t DIAGNOSTIC_MASK = 0x0000000f; - - static constexpr uint32_t PACKET_END = 0xffffffff; - - // Writing spools. - - class writer { - int fd; - size_t position; - std::vector buffer; - - // These functions aren't overloaded because of implicit numeric conversions. - - void emit_word(uint32_t word) { - if (position + 1 == buffer.size()) - flush(); - buffer[position++] = word; - } - - void emit_dword(uint64_t dword) { - emit_word(dword >> 0); - emit_word(dword >> 32); - } - - void emit_ident(ident_t ident) { - assert(ident <= MAXIMUM_IDENT); - emit_word(ident); - } - - void emit_size(size_t size) { - assert(size <= std::numeric_limits::max()); - emit_word(size); - } - - // Same implementation as `emit_size()`, different declared intent. - void emit_index(size_t index) { - assert(index <= std::numeric_limits::max()); - emit_word(index); - } - - void emit_string(std::string str) { - // Align to a word boundary, and add at least one terminating \0. - str.resize(str.size() + (sizeof(uint32_t) - (str.size() + sizeof(uint32_t)) % sizeof(uint32_t))); - for (size_t index = 0; index < str.size(); index += sizeof(uint32_t)) { - uint32_t word; - memcpy(&word, &str[index], sizeof(uint32_t)); - emit_word(word); - } - } - - void emit_time(const time ×tamp) { - const value &raw_timestamp(timestamp); - emit_word(raw_timestamp.data[0]); - emit_word(raw_timestamp.data[1]); - emit_word(raw_timestamp.data[2]); - } - - public: - // Creates a writer, and transfers ownership of `fd`, which must be open for appending. - // - // The buffer size is currently fixed to a "reasonably large" size, determined empirically by measuring writer - // performance on a representative design; large but not so large it would e.g. cause address space exhaustion - // on 32-bit platforms. - writer(spool &spool) : fd(spool.take_write()), position(0), buffer(32 * 1024 * 1024) { - assert(fd != -1); -#if !defined(WIN32) - int result = ftruncate(fd, 0); -#else - int result = _chsize_s(fd, 0); -#endif - assert(result == 0); - } - - writer(writer &&moved) : fd(moved.fd), position(moved.position), buffer(moved.buffer) { - moved.fd = -1; - moved.position = 0; - } - - writer(const writer &) = delete; - writer &operator=(const writer &) = delete; - - // Both write() calls and fwrite() calls are too expensive to perform implicitly. The API consumer must determine - // the optimal time to flush the writer and do that explicitly for best performance. - void flush() { - assert(fd != -1); - size_t data_size = position * sizeof(uint32_t); - size_t data_written = write(fd, buffer.data(), data_size); - assert(data_size == data_written); - position = 0; - } - - ~writer() { - if (fd != -1) { - flush(); - close(fd); - } - } - - void write_magic() { - // `CXXRTL` followed by version in binary. This header will read backwards on big-endian machines, which allows - // detection of this case, both visually and programmatically. - emit_dword(((uint64_t)VERSION << 48) | HEADER_MAGIC); - } - - void write_define(ident_t ident, const std::string &name, size_t part_index, size_t chunks, size_t depth) { - emit_word(PACKET_DEFINE); - emit_ident(ident); - emit_string(name); - emit_index(part_index); - emit_size(chunks); - emit_size(depth); - } - - void write_sample(bool incremental, pointer_t pointer, const time ×tamp) { - uint32_t flags = (incremental ? sample_flag::INCREMENTAL : 0); - emit_word(PACKET_SAMPLE); - emit_word(flags); - emit_word(pointer); - emit_time(timestamp); - } - - void write_change(ident_t ident, size_t chunks, const chunk_t *data) { - assert(ident <= MAXIMUM_IDENT); - - if (chunks == 1 && *data == 0) { - emit_word(PACKET_CHANGEL | ident); - } else if (chunks == 1 && *data == 1) { - emit_word(PACKET_CHANGEH | ident); - } else { - emit_word(PACKET_CHANGE | ident); - for (size_t offset = 0; offset < chunks; offset++) - emit_word(data[offset]); - } - } - - void write_change(ident_t ident, size_t chunks, const chunk_t *data, size_t index) { - assert(ident <= MAXIMUM_IDENT); - - emit_word(PACKET_CHANGEI | ident); - emit_index(index); - for (size_t offset = 0; offset < chunks; offset++) - emit_word(data[offset]); - } - - void write_diagnostic(const diagnostic &diagnostic) { - emit_word(PACKET_DIAGNOSTIC | diagnostic.type); - emit_string(diagnostic.message); - emit_string(diagnostic.location); - } - - void write_end() { - emit_word(PACKET_END); - } - }; - - // Reading spools. - - class reader { - FILE *f; - - uint32_t absorb_word() { - // If we're at end of file, `fread` will not write to `word`, and `PACKET_END` will be returned. - uint32_t word = PACKET_END; - fread(&word, sizeof(word), 1, f); - return word; - } - - uint64_t absorb_dword() { - uint32_t lo = absorb_word(); - uint32_t hi = absorb_word(); - return ((uint64_t)hi << 32) | lo; - } - - ident_t absorb_ident() { - ident_t ident = absorb_word(); - assert(ident <= MAXIMUM_IDENT); - return ident; - } - - size_t absorb_size() { - return absorb_word(); - } - - size_t absorb_index() { - return absorb_word(); - } - - std::string absorb_string() { - std::string str; - do { - size_t end = str.size(); - str.resize(end + 4); - uint32_t word = absorb_word(); - memcpy(&str[end], &word, sizeof(uint32_t)); - } while (str.back() != '\0'); - // Strings have no embedded zeroes besides the terminating one(s). - return str.substr(0, str.find('\0')); - } - - time absorb_time() { - value raw_timestamp; - raw_timestamp.data[0] = absorb_word(); - raw_timestamp.data[1] = absorb_word(); - raw_timestamp.data[2] = absorb_word(); - return time(raw_timestamp); - } - - public: - typedef uint64_t pos_t; - - // Creates a reader, and transfers ownership of `fd`, which must be open for reading. - reader(spool &spool) : f(fdopen(spool.take_read(), "r")) { - assert(f != nullptr); - } - - reader(reader &&moved) : f(moved.f) { - moved.f = nullptr; - } - - reader(const reader &) = delete; - reader &operator=(const reader &) = delete; - - ~reader() { - if (f != nullptr) - fclose(f); - } - - pos_t position() { - return ftell(f); - } - - void rewind(pos_t position) { - fseek(f, position, SEEK_SET); - } - - void read_magic() { - uint64_t magic = absorb_dword(); - assert((magic & ~VERSION_MASK) == HEADER_MAGIC); - assert((magic >> 48) == VERSION); - } - - bool read_define(ident_t &ident, std::string &name, size_t &part_index, size_t &chunks, size_t &depth) { - uint32_t header = absorb_word(); - if (header == PACKET_END) - return false; - assert(header == PACKET_DEFINE); - ident = absorb_ident(); - name = absorb_string(); - part_index = absorb_index(); - chunks = absorb_size(); - depth = absorb_size(); - return true; - } - - bool read_sample(bool &incremental, pointer_t &pointer, time ×tamp) { - uint32_t header = absorb_word(); - if (header == PACKET_END) - return false; - assert(header == PACKET_SAMPLE); - uint32_t flags = absorb_word(); - incremental = (flags & sample_flag::INCREMENTAL); - pointer = absorb_word(); - timestamp = absorb_time(); - return true; - } - - bool read_header(uint32_t &header) { - header = absorb_word(); - return header != PACKET_END; - } - - // This method must be separate from `read_change_data` because `chunks` and `depth` can only be looked up - // if `ident` is known. - bool read_change_ident(uint32_t header, ident_t &ident) { - if ((header & ~(CHANGE_MASK | MAXIMUM_IDENT)) != 0) - return false; // some other packet - ident = header & MAXIMUM_IDENT; - return true; - } - - void read_change_data(uint32_t header, size_t chunks, size_t depth, chunk_t *data) { - uint32_t index = 0; - switch (header & CHANGE_MASK) { - case PACKET_CHANGEL: - *data = 0; - return; - case PACKET_CHANGEH: - *data = 1; - return; - case PACKET_CHANGE: - break; - case PACKET_CHANGEI: - index = absorb_word(); - assert(index < depth); - break; - default: - assert(false && "Unrecognized change packet"); - } - for (size_t offset = 0; offset < chunks; offset++) - data[chunks * index + offset] = absorb_word(); - } - - bool read_diagnostic(uint32_t header, diagnostic &diagnostic) { - if ((header & ~DIAGNOSTIC_MASK) != PACKET_DIAGNOSTIC) - return false; // some other packet - uint32_t type = header & DIAGNOSTIC_MASK; - assert(type == diagnostic::BREAK || type == diagnostic::PRINT || - type == diagnostic::ASSERT || type == diagnostic::ASSUME); - diagnostic.type = (diagnostic::flavor)type; - diagnostic.message = absorb_string(); - diagnostic.location = absorb_string(); - return true; - } - }; - - // Opening spools. For certain uses of the record/replay mechanism, two distinct open files (two open files, i.e. - // two distinct file pointers, and not just file descriptors, which share the file pointer if duplicated) are used, - // for a reader and writer thread. This class manages the lifetime of the descriptors for these files. When only - // one of them is used, the other is closed harmlessly when the spool is destroyed. -private: - std::atomic writefd; - std::atomic readfd; - -public: - spool(const std::string &filename) - : writefd(open(filename.c_str(), O_CREAT|O_BINARY|O_WRONLY|O_APPEND, 0644)), - readfd(open(filename.c_str(), O_BINARY|O_RDONLY)) { - assert(writefd.load() != -1 && readfd.load() != -1); - } - - spool(spool &&moved) : writefd(moved.writefd.exchange(-1)), readfd(moved.readfd.exchange(-1)) {} - - spool(const spool &) = delete; - spool &operator=(const spool &) = delete; - - ~spool() { - int fd; - if ((fd = writefd.exchange(-1)) != -1) - close(fd); - if ((fd = readfd.exchange(-1)) != -1) - close(fd); - } - - // Atomically acquire a write file descriptor for the spool. Can be called once, and will return -1 the next time - // it is called. Thread-safe. - int take_write() { - return writefd.exchange(-1); - } - - // Atomically acquire a read file descriptor for the spool. Can be called once, and will return -1 the next time - // it is called. Thread-safe. - int take_read() { - return readfd.exchange(-1); - } -}; - -// A CXXRTL recorder samples design state, producing complete or incremental updates, and writes them to a spool. -class recorder { - struct variable { - spool::ident_t ident; /* <= spool::MAXIMUM_IDENT */ - size_t chunks; - size_t depth; /* == 1 for wires */ - chunk_t *curr; - bool memory; - }; - - spool::writer writer; - std::vector variables; - std::vector inputs; // values of inputs must be recorded explicitly, as their changes are not observed - std::unordered_map ident_lookup; - bool streaming = false; // whether variable definitions have been written - spool::pointer_t pointer = 0; - time timestamp; - -public: - template - recorder(Args &&...args) : writer(std::forward(args)...) {} - - void start(module &module, std::string top_path = "") { - debug_items items; - module.debug_info(&items, /*scopes=*/nullptr, top_path); - start(items); - } - - void start(const debug_items &items) { - assert(!streaming); - - writer.write_magic(); - for (auto item : items.table) - for (size_t part_index = 0; part_index < item.second.size(); part_index++) { - auto &part = item.second[part_index]; - if ((part.flags & debug_item::INPUT) || (part.flags & debug_item::DRIVEN_SYNC) || - (part.type == debug_item::MEMORY)) { - variable var; - var.ident = variables.size() + 1; - var.chunks = (part.width + sizeof(chunk_t) * 8 - 1) / (sizeof(chunk_t) * 8); - var.depth = part.depth; - var.curr = part.curr; - var.memory = (part.type == debug_item::MEMORY); - ident_lookup[var.curr] = var.ident; - - assert(variables.size() < spool::MAXIMUM_IDENT); - if (part.flags & debug_item::INPUT) - inputs.push_back(variables.size()); - variables.push_back(var); - - writer.write_define(var.ident, item.first, part_index, var.chunks, var.depth); - } - } - writer.write_end(); - streaming = true; - } - - const time &latest_time() { - return timestamp; - } - - const time &advance_time(const time &delta) { - assert(!delta.is_negative()); - timestamp += delta; - return timestamp; - } - - void record_complete() { - assert(streaming); - - writer.write_sample(/*incremental=*/false, pointer++, timestamp); - for (auto var : variables) { - assert(var.ident != 0); - if (!var.memory) - writer.write_change(var.ident, var.chunks, var.curr); - else - for (size_t index = 0; index < var.depth; index++) - writer.write_change(var.ident, var.chunks, &var.curr[var.chunks * index], index); - } - writer.write_end(); - } - - // This function is generic over ModuleT to encourage observer callbacks to be inlined into the commit function. - template - bool record_incremental(ModuleT &module) { - assert(streaming); - - struct : observer { - std::unordered_map *ident_lookup; - spool::writer *writer; - - CXXRTL_ALWAYS_INLINE - void on_update(size_t chunks, const chunk_t *base, const chunk_t *value) { - writer->write_change(ident_lookup->at(base), chunks, value); - } - - CXXRTL_ALWAYS_INLINE - void on_update(size_t chunks, const chunk_t *base, const chunk_t *value, size_t index) { - writer->write_change(ident_lookup->at(base), chunks, value, index); - } - } record_observer; - record_observer.ident_lookup = &ident_lookup; - record_observer.writer = &writer; - - writer.write_sample(/*incremental=*/true, pointer++, timestamp); - for (auto input_index : inputs) { - variable &var = variables.at(input_index); - assert(!var.memory); - writer.write_change(var.ident, var.chunks, var.curr); - } - bool changed = module.commit(record_observer); - writer.write_end(); - return changed; - } - - void record_diagnostic(const diagnostic &diagnostic) { - assert(streaming); - - // Emit an incremental delta cycle per diagnostic to simplify the logic of the recorder. This is inefficient, but - // diagnostics should be rare enough that this inefficiency does not matter. If it turns out to be an issue, this - // code should be changed to accumulate diagnostics to a buffer that is flushed in `record_{complete,incremental}` - // and also in `advance_time` before the timestamp is changed. (Right now `advance_time` never writes to the spool.) - writer.write_sample(/*incremental=*/true, pointer++, timestamp); - writer.write_diagnostic(diagnostic); - writer.write_end(); - } - - void flush() { - writer.flush(); - } -}; - -// A CXXRTL player reads samples from a spool, and changes the design state accordingly. To start reading samples, -// a spool must have been initialized: the recorder must have been started and an initial complete sample must have -// been written. -class player { - struct variable { - size_t chunks; - size_t depth; /* == 1 for wires */ - chunk_t *curr; - }; - - spool::reader reader; - std::unordered_map variables; - bool streaming = false; // whether variable definitions have been read - bool initialized = false; // whether a sample has ever been read - spool::pointer_t pointer = 0; - time timestamp; - - std::map> index_by_pointer; - std::map> index_by_timestamp; - - bool peek_sample(spool::pointer_t &pointer, time ×tamp) { - bool incremental; - auto position = reader.position(); - bool success = reader.read_sample(incremental, pointer, timestamp); - reader.rewind(position); - return success; - } - -public: - template - player(Args &&...args) : reader(std::forward(args)...) {} - - // The `top_path` must match the one given to the recorder. - void start(module &module, std::string top_path = "") { - debug_items items; - module.debug_info(&items, /*scopes=*/nullptr, top_path); - start(items); - } - - void start(const debug_items &items) { - assert(!streaming); - - reader.read_magic(); - while (true) { - spool::ident_t ident; - std::string name; - size_t part_index; - size_t chunks; - size_t depth; - if (!reader.read_define(ident, name, part_index, chunks, depth)) - break; - assert(variables.count(ident) == 0); - assert(items.count(name) != 0); - assert(part_index < items.count(name)); - - const debug_item &part = items.at(name).at(part_index); - assert(chunks == (part.width + sizeof(chunk_t) * 8 - 1) / (sizeof(chunk_t) * 8)); - assert(depth == part.depth); - - variable &var = variables[ident]; - var.chunks = chunks; - var.depth = depth; - var.curr = part.curr; - } - assert(variables.size() > 0); - streaming = true; - - // Establish the initial state of the design. - std::vector diagnostics; - initialized = replay(&diagnostics); - assert(initialized && diagnostics.empty()); - } - - // Returns the pointer of the current sample. - spool::pointer_t current_pointer() { - assert(initialized); - return pointer; - } - - // Returns the time of the current sample. - const time ¤t_time() { - assert(initialized); - return timestamp; - } - - // Returns `true` if there is a next sample to read, and sets `pointer` to its pointer if there is. - bool get_next_pointer(spool::pointer_t &pointer) { - assert(streaming); - time timestamp; - return peek_sample(pointer, timestamp); - } - - // Returns `true` if there is a next sample to read, and sets `timestamp` to its time if there is. - bool get_next_time(time ×tamp) { - assert(streaming); - uint32_t pointer; - return peek_sample(pointer, timestamp); - } - - // If this function returns `true`, then `current_pointer() == at_pointer`, and the module contains values that - // correspond to this pointer in the replay log. To obtain a valid pointer, call `current_pointer()`; while pointers - // are monotonically increasing for each consecutive sample, using arithmetic operations to create a new pointer is - // not allowed. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in this sample. - bool rewind_to(spool::pointer_t at_pointer, std::vector *diagnostics) { - assert(initialized); - - // The pointers in the replay log start from one that is greater than `at_pointer`. In this case the pointer will - // never be reached. - assert(index_by_pointer.size() > 0); - if (at_pointer < index_by_pointer.rbegin()->first) - return false; - - // Find the last complete sample whose pointer is less than or equal to `at_pointer`. Note that the comparison - // function used here is `std::greater`, inverting the direction of `lower_bound`. - auto position_it = index_by_pointer.lower_bound(at_pointer); - assert(position_it != index_by_pointer.end()); - reader.rewind(position_it->second); - - // Replay samples until eventually arriving to `at_pointer` or encountering end of file. - while(replay(diagnostics)) { - if (pointer == at_pointer) - return true; - - if (diagnostics) - diagnostics->clear(); - } - return false; - } - - // If this function returns `true`, then `current_time() <= at_or_before_timestamp`, and the module contains values - // that correspond to `current_time()` in the replay log. If `current_time() == at_or_before_timestamp` and there - // are several consecutive samples with the same time, the module contains values that correspond to the first of - // these samples. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in this sample. - bool rewind_to_or_before(const time &at_or_before_timestamp, std::vector *diagnostics) { - assert(initialized); - - // The timestamps in the replay log start from one that is greater than `at_or_before_timestamp`. In this case - // the timestamp will never be reached. Otherwise, this function will always succeed. - assert(index_by_timestamp.size() > 0); - if (at_or_before_timestamp < index_by_timestamp.rbegin()->first) - return false; - - // Find the last complete sample whose timestamp is less than or equal to `at_or_before_timestamp`. Note that - // the comparison function used here is `std::greater`, inverting the direction of `lower_bound`. - auto position_it = index_by_timestamp.lower_bound(at_or_before_timestamp); - assert(position_it != index_by_timestamp.end()); - reader.rewind(position_it->second); - - // Replay samples until eventually arriving to or past `at_or_before_timestamp` or encountering end of file. - while (replay(diagnostics)) { - if (timestamp == at_or_before_timestamp) - break; - - time next_timestamp; - if (!get_next_time(next_timestamp)) - break; - if (next_timestamp > at_or_before_timestamp) - break; - - if (diagnostics) - diagnostics->clear(); - } - return true; - } - - // If this function returns `true`, then `current_pointer()` and `current_time()` are updated for the next sample - // and the module now contains values that correspond to that sample. If it returns `false`, there was no next sample - // to read. The `diagnostics` argument, if not `nullptr`, receives the diagnostics recorded in the next sample. - bool replay(std::vector *diagnostics) { - assert(streaming); - - bool incremental; - auto position = reader.position(); - if (!reader.read_sample(incremental, pointer, timestamp)) - return false; - - // The very first sample that is read must be a complete sample. This is required for the rewind functions to work. - assert(initialized || !incremental); - - // It is possible (though not very useful) to have several complete samples with the same timestamp in a row. - // Ensure that we associate the timestamp with the position of the first such complete sample. (This condition - // works because the player never jumps over a sample.) - if (!incremental && !index_by_pointer.count(pointer)) { - assert(!index_by_timestamp.count(timestamp)); - index_by_pointer[pointer] = position; - index_by_timestamp[timestamp] = position; - } - - uint32_t header; - while (reader.read_header(header)) { - spool::ident_t ident; - diagnostic diag; - if (reader.read_change_ident(header, ident)) { - variable &var = variables.at(ident); - reader.read_change_data(header, var.chunks, var.depth, var.curr); - } else if (reader.read_diagnostic(header, diag)) { - if (diagnostics) - diagnostics->push_back(diag); - } else assert(false && "Unrecognized packet header"); - } - return true; - } -}; - -} - -#endif diff --git a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_time.h b/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_time.h deleted file mode 100644 index f37c2b65640..00000000000 --- a/yosys/backends/cxxrtl/runtime/cxxrtl/cxxrtl_time.h +++ /dev/null @@ -1,231 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2023 Catherine - * - * Permission to use, copy, modify, and/or distribute this software for any - * purpose with or without fee is hereby granted. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES - * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF - * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR - * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES - * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN - * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF - * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. - * - */ - -#ifndef CXXRTL_TIME_H -#define CXXRTL_TIME_H - -#include -#include - -#include - -namespace cxxrtl { - -// A timestamp or a difference in time, stored as a 96-bit number of femtoseconds (10e-15 s). The range and resolution -// of this format can represent any VCD timestamp within approx. ±1255321.2 years, without the need for a timescale. -class time { -public: - static constexpr size_t bits = 96; // 3 chunks - -private: - static constexpr size_t resolution_digits = 15; - - static_assert(sizeof(chunk_t) == 4, "a chunk is expected to be 32-bit"); - static constexpr value resolution = value { - chunk_t(1000000000000000ull & 0xffffffffull), chunk_t(1000000000000000ull >> 32), 0u - }; - - // Signed number of femtoseconds from the beginning of time. - value raw; - -public: - constexpr time() {} - - explicit constexpr time(const value &raw) : raw(raw) {} - explicit operator const value &() const { return raw; } - - static constexpr time maximum() { - return time(value { 0xffffffffu, 0xffffffffu, 0x7fffffffu }); - } - - time(int64_t secs, int64_t femtos) { - value<64> secs_val; - secs_val.set(secs); - value<64> femtos_val; - femtos_val.set(femtos); - raw = secs_val.sext().mul(resolution).add(femtos_val.sext()); - } - - bool is_zero() const { - return raw.is_zero(); - } - - // Extracts the sign of the value. - bool is_negative() const { - return raw.is_neg(); - } - - // Extracts the number of whole seconds. Negative if the value is negative. - int64_t secs() const { - return raw.sdivmod(resolution).first.trunc<64>().get(); - } - - // Extracts the number of femtoseconds in the fractional second. Negative if the value is negative. - int64_t femtos() const { - return raw.sdivmod(resolution).second.trunc<64>().get(); - } - - bool operator==(const time &other) const { - return raw == other.raw; - } - - bool operator!=(const time &other) const { - return raw != other.raw; - } - - bool operator>(const time &other) const { - return other.raw.scmp(raw); - } - - bool operator>=(const time &other) const { - return !raw.scmp(other.raw); - } - - bool operator<(const time &other) const { - return raw.scmp(other.raw); - } - - bool operator<=(const time &other) const { - return !other.raw.scmp(raw); - } - - time operator+(const time &other) const { - return time(raw.add(other.raw)); - } - - time &operator+=(const time &other) { - *this = *this + other; - return *this; - } - - time operator-() const { - return time(raw.neg()); - } - - time operator-(const time &other) const { - return *this + (-other); - } - - time &operator-=(const time &other) { - *this = *this - other; - return *this; - } - - operator std::string() const { - char buf[48]; // x=2**95; len(f"-{x/1_000_000_000_000_000}.{x^1_000_000_000_000_000}") == 48 - int64_t secs = this->secs(); - int64_t femtos = this->femtos(); - snprintf(buf, sizeof(buf), "%s%" PRIi64 ".%015" PRIi64, - is_negative() ? "-" : "", secs >= 0 ? secs : -secs, femtos >= 0 ? femtos : -femtos); - return buf; - } - -#if __cplusplus >= 201603L - [[nodiscard("ignoring parse errors")]] -#endif - bool parse(const std::string &str) { - enum { - parse_sign_opt, - parse_integral, - parse_fractional, - } state = parse_sign_opt; - bool negative = false; - int64_t integral = 0; - int64_t fractional = 0; - size_t frac_digits = 0; - for (auto chr : str) { - switch (state) { - case parse_sign_opt: - state = parse_integral; - if (chr == '+' || chr == '-') { - negative = (chr == '-'); - break; - } - /* fallthrough */ - case parse_integral: - if (chr >= '0' && chr <= '9') { - integral *= 10; - integral += chr - '0'; - } else if (chr == '.') { - state = parse_fractional; - } else { - return false; - } - break; - case parse_fractional: - if (chr >= '0' && chr <= '9' && frac_digits < resolution_digits) { - fractional *= 10; - fractional += chr - '0'; - frac_digits++; - } else { - return false; - } - break; - } - } - if (frac_digits == 0) - return false; - while (frac_digits++ < resolution_digits) - fractional *= 10; - *this = negative ? -time { integral, fractional} : time { integral, fractional }; - return true; - } -}; - -// Out-of-line definition required until C++17. -constexpr value time::resolution; - -std::ostream &operator<<(std::ostream &os, const time &val) { - os << (std::string)val; - return os; -} - -// These literals are (confusingly) compatible with the ones from `std::chrono`: the `std::chrono` literals do not -// have an underscore (e.g. 1ms) and the `cxxrtl::time` literals do (e.g. 1_ms). This syntactic difference is -// a requirement of the C++ standard. Despite being compatible the literals should not be mixed in the same namespace. -namespace time_literals { - -time operator""_s(unsigned long long seconds) { - return time { (int64_t)seconds, 0 }; -} - -time operator""_ms(unsigned long long milliseconds) { - return time { 0, (int64_t)milliseconds * 1000000000000 }; -} - -time operator""_us(unsigned long long microseconds) { - return time { 0, (int64_t)microseconds * 1000000000 }; -} - -time operator""_ns(unsigned long long nanoseconds) { - return time { 0, (int64_t)nanoseconds * 1000000 }; -} - -time operator""_ps(unsigned long long picoseconds) { - return time { 0, (int64_t)picoseconds * 1000 }; -} - -time operator""_fs(unsigned long long femtoseconds) { - return time { 0, (int64_t)femtoseconds }; -} - -}; - -}; - -#endif diff --git a/yosys/backends/edif/edif.cc b/yosys/backends/edif/edif.cc index 553eb23d645..00fd7f54e39 100644 --- a/yosys/backends/edif/edif.cc +++ b/yosys/backends/edif/edif.cc @@ -213,9 +213,6 @@ struct EdifBackend : public Backend { for (auto cell : module->cells()) { - if (cell->type == ID($scopeinfo)) - continue; - if (design->module(cell->type) == nullptr || design->module(cell->type)->get_blackbox_attribute()) { lib_cell_ports[cell->type]; for (auto p : cell->connections()) diff --git a/yosys/backends/firrtl/firrtl.cc b/yosys/backends/firrtl/firrtl.cc index dc76dbeecf5..fc1d628915c 100644 --- a/yosys/backends/firrtl/firrtl.cc +++ b/yosys/backends/firrtl/firrtl.cc @@ -980,9 +980,6 @@ struct FirrtlWorker register_reverse_wire_map(y_id, cell->getPort(ID::Y)); continue; } - - if (cell->type == ID($scopeinfo)) - continue; log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell)); } diff --git a/yosys/backends/firrtl/test.sh b/yosys/backends/firrtl/test.sh index dd675e91712..fe7e3a32912 100644 --- a/yosys/backends/firrtl/test.sh +++ b/yosys/backends/firrtl/test.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env bash +#!/bin/bash set -ex cd ../../ diff --git a/yosys/backends/jny/jny.cc b/yosys/backends/jny/jny.cc index 1c163dba52e..9989feed599 100644 --- a/yosys/backends/jny/jny.cc +++ b/yosys/backends/jny/jny.cc @@ -124,7 +124,7 @@ struct JnyWriter design->sort(); f << "{\n"; - f << " \"$schema\": \"https://raw.githubusercontent.com/YosysHQ/yosys/main/misc/jny.schema.json\",\n"; + f << " \"$schema\": \"https://raw.githubusercontent.com/YosysHQ/yosys/master/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/main/misc/jny.schema.json\"\n"); + log("which is located at \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\"\n"); log("\n"); } diff --git a/yosys/backends/json/json.cc b/yosys/backends/json/json.cc index 2f442c494f7..fd2c922fd5d 100644 --- a/yosys/backends/json/json.cc +++ b/yosys/backends/json/json.cc @@ -192,10 +192,6 @@ struct JsonWriter for (auto c : module->cells()) { if (use_selection && !module->selected(c)) continue; - // Eventually we will want to emit $scopeinfo, but currently this - // will break JSON netlist consumers like nextpnr - if (c->type == ID($scopeinfo)) - continue; f << stringf("%s\n", first ? "" : ","); f << stringf(" %s: {\n", get_name(c->name).c_str()); f << stringf(" \"hide_name\": %s,\n", c->name[0] == '$' ? "1" : "0"); diff --git a/yosys/backends/simplec/test00.sh b/yosys/backends/simplec/test00.sh index 9895a97e46b..ede75727378 100644 --- a/yosys/backends/simplec/test00.sh +++ b/yosys/backends/simplec/test00.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env bash +#!/bin/bash set -ex ../../yosys -p 'synth -top test; write_simplec -verbose -i8 test00_uut.c' test00_uut.v clang -o test00_tb test00_tb.c diff --git a/yosys/backends/smt2/smt2.cc b/yosys/backends/smt2/smt2.cc index c702d5e7e54..5e63e62370d 100644 --- a/yosys/backends/smt2/smt2.cc +++ b/yosys/backends/smt2/smt2.cc @@ -1117,18 +1117,7 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - bool private_name = cell->name[0] == '$'; - - if (!private_name && cell->has_attribute(ID::hdlname)) { - for (auto const &part : cell->get_hdlname_attribute()) { - if (part == "_witness_") { - private_name = true; - break; - } - } - } - - if (private_name && cell->attributes.count(ID::src)) + if (cell->name[0] == '$' && cell->attributes.count(ID::src)) decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); else decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); diff --git a/yosys/backends/smt2/smtbmc.py b/yosys/backends/smt2/smtbmc.py index c3bdcebbe96..02e15a1b502 100644 --- a/yosys/backends/smt2/smtbmc.py +++ b/yosys/backends/smt2/smtbmc.py @@ -17,7 +17,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import os, sys, getopt, re, bisect, json +import os, sys, getopt, re, bisect ##yosys-sys-path## from smtio import SmtIo, SmtOpts, MkVcd from ywio import ReadWitness, WriteWitness, WitnessValues @@ -56,9 +56,6 @@ keep_going = False check_witness = False detect_loops = False -incremental = None -track_assumes = False -minimize_assumes = False so = SmtOpts() @@ -188,17 +185,6 @@ def help(): check if states are unique in temporal induction counter examples (this feature is experimental and incomplete) - --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(): @@ -210,8 +196,7 @@ 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", - "track-assumes", "minimize-assumes"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"]) except: usage() @@ -297,13 +282,6 @@ def usage(): check_witness = True elif o == "--detect-loops": detect_loops = True - 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: @@ -312,7 +290,7 @@ def usage(): if len(args) != 1: usage() -if sum([tempind, gentrace, covermode, incremental is not None]) > 1: +if sum([tempind, gentrace, covermode]) > 1: usage() constr_final_start = None @@ -462,17 +440,12 @@ 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 def print_msg(msg): - if incremental: - incremental.print_msg(msg) - else: - print("%s %s" % (smt.timestamp(), msg), flush=True) + print("%s %s" % (smt.timestamp(), msg)) + sys.stdout.flush() print_msg("Solver: %s" % (so.solver)) @@ -667,14 +640,15 @@ def print_msg(msg): num_steps = max(num_steps, step+2) step += 1 -ywfile_hierwitness_cache = None +if inywfile is not None: + if not got_topt: + skip_steps = 0 + num_steps = 0 -def ywfile_hierwitness(): - global ywfile_hierwitness_cache - if ywfile_hierwitness_cache is None: - ywfile_hierwitness = smt.hierwitness(topmod, allregs=True, blackbox=True) + with open(inywfile, "r") as f: + inyw = ReadWitness(f) - inits, seqs, clocks, mems = ywfile_hierwitness + inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True) smt_wires = defaultdict(list) smt_mems = defaultdict(list) @@ -685,165 +659,90 @@ def ywfile_hierwitness(): for mem in mems: smt_mems[mem["path"]].append(mem) - 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 isinstance(exprs, (tuple, list)): - exprs = tuple(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) + addr_re = re.compile(r'\\\[[0-9]+\]$') + bits_re = re.compile(r'[01?]*$') - output.append((0, sig.width, smt_expr)) + for t, step in inyw.steps(): + present_signals, missing = step.present_signals(inyw.sigmap) + for sig in present_signals: + bits = step[sig] + if not bits_re.match(bits): + raise ValueError("unsupported bit value in Yosys witness file") - output.sort() + 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"] - output = [chunk for chunk in output if chunk[0] != chunk[1]] + smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 - pos = 0 + offset = max(offset, 0) - for start, end, smt_expr in output: - assert start == pos - pos = end + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue - assert pos == sig.width + smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire) - if len(output) == 1: - return output[0][-1] - return smt_concat(smt_expr for start, end, smt_expr in reversed(output)) + 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) -def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): - global ywfile_hierwitness_cache - if map_steps is None: - map_steps = {} + bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] - with open(inywfile, "r") as f: - inyw = ReadWitness(f) + if bit_slice.count("?") == len(bit_slice): + continue - inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + 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) - bits_re = re.compile(r'[01?]*$') - max_t = -1 + smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - 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") + constr_assumes[t].append((inywfile, smt_constr)) - if bits.count('?') == len(bits): - continue + 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 = ywfile_signal(sig, map_steps.get(t, t)) + smt_expr = smt.net_expr(topmod, f"s{t}", mem["smtpath"]) - smt_expr, bits = smt_extract_mask(smt_expr, bits) + 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) - smt_constr = "(= %s #b%s)" % (smt_expr, bits) - constr_assumes[t].append((inywfile, smt_constr)) + if len(bits) < width: + slice_high = sig.offset + len(bits) - 1 + smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) - max_t = t - return max_t + bit_slice = bits -if inywfile is not None: - if not got_topt: - skip_steps = 0 - num_steps = 0 + 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) - max_t = ywfile_constraints(inywfile, constr_assumes) + smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + constr_assumes[t].append((inywfile, smt_constr)) - if not got_topt: - if not check_witness: - skip_steps = max(skip_steps, max_t) - num_steps = max(num_steps, max_t+1) + if not got_topt: + if not check_witness: + skip_steps = max(skip_steps, t) + num_steps = max(num_steps, t+1) if btorwitfile is not None: with open(btorwitfile, "r") as f: @@ -942,7 +841,7 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): skip_steps = step num_steps = step+1 -def collect_mem_trace_data(steps, vcd=None): +def collect_mem_trace_data(steps_start, steps_stop, vcd=None): mem_trace_data = dict() for mempath in sorted(smt.hiermems(topmod)): @@ -950,16 +849,16 @@ def collect_mem_trace_data(steps, vcd=None): expr_id = list() expr_list = list() - for seq, i in enumerate(steps): + for i in range(steps_start, steps_stop): for j in range(rports): - expr_id.append(('R', seq, j, 'A')) - expr_id.append(('R', seq, j, 'D')) + expr_id.append(('R', i-steps_start, j, 'A')) + expr_id.append(('R', i-steps_start, j, 'D')) expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j)) expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j)) for j in range(wports): - expr_id.append(('W', seq, j, 'A')) - expr_id.append(('W', seq, j, 'D')) - expr_id.append(('W', seq, j, 'M')) + expr_id.append(('W', i-steps_start, j, 'A')) + expr_id.append(('W', i-steps_start, j, 'D')) + expr_id.append(('W', i-steps_start, j, 'M')) expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j)) expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j)) expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j)) @@ -1044,14 +943,14 @@ def collect_mem_trace_data(steps, vcd=None): netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int_addr) vcd.add_net([topmod] + netpath, width) - for seq, i in enumerate(steps): + for i in range(steps_start, steps_stop): if i not in mem_trace_data: mem_trace_data[i] = list() - mem_trace_data[i].append((netpath, int_addr, "".join(tdata[seq]))) + mem_trace_data[i].append((netpath, int_addr, "".join(tdata[i-steps_start]))) return mem_trace_data -def write_vcd_trace(steps, index, seq_time=False): +def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) print_msg("Writing trace to VCD file: %s" % (filename)) @@ -1072,10 +971,10 @@ def write_vcd_trace(steps, index, seq_time=False): vcd.add_clock([topmod] + netpath, edge) path_list.append(netpath) - mem_trace_data = collect_mem_trace_data(steps, vcd) + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop, vcd) - for seq, i in enumerate(steps): - vcd.set_time(seq if seq_time else i) + for i in range(steps_start, steps_stop): + vcd.set_time(i) value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i) for path, value in zip(path_list, value_list): vcd.set_net([topmod] + path, value) @@ -1083,14 +982,7 @@ def write_vcd_trace(steps, index, seq_time=False): for path, addr, value in mem_trace_data[i]: vcd.set_net([topmod] + path, value) - if seq_time: - end_time = len(steps) - elif steps: - end_time = steps[-1] + 1 - else: - end_time = 0 - - vcd.set_time(end_time) + vcd.set_time(steps_stop) def detect_state_loop(steps_start, steps_stop): print_msg(f"Checking for loops in found induction counter example") @@ -1135,7 +1027,7 @@ def escape_identifier(identifier): -def write_vlogtb_trace(steps, index): +def write_vlogtb_trace(steps_start, steps_stop, index): filename = vlogtbfile.replace("%", index) print_msg("Writing trace to Verilog testbench: %s" % (filename)) @@ -1200,7 +1092,7 @@ def write_vlogtb_trace(steps, index): print(" initial begin", file=f) regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True)) - regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps[0]))) + regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start))) print("`ifndef VERILATOR", file=f) print(" #1;", file=f) @@ -1215,7 +1107,7 @@ def write_vlogtb_trace(steps, index): anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod)) for info in anyconsts: if info[3] is not None: - modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps[0])), info[0]) + modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0]) value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate))) print(" UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f); @@ -1225,7 +1117,7 @@ def write_vlogtb_trace(steps, index): addr_expr_list = list() data_expr_list = list() - for i in steps: + for i in range(steps_start, steps_stop): for j in range(rports): addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j)) data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j)) @@ -1246,7 +1138,7 @@ def write_vlogtb_trace(steps, index): print("", file=f) anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod)) - for i in steps: + for i in range(steps_start, steps_stop): pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs] pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i))) @@ -1278,14 +1170,14 @@ def write_vlogtb_trace(steps, index): print(" end", file=f) print(" always @(posedge clock) begin", file=f) - print(" genclock <= cycle < %d;" % (steps[-1]), file=f) + print(" genclock <= cycle < %d;" % (steps_stop-1), file=f) print(" cycle <= cycle + 1;", file=f) print(" end", file=f) print("endmodule", file=f) -def write_constr_trace(steps, index): +def write_constr_trace(steps_start, steps_stop, index): filename = outconstr.replace("%", index) print_msg("Writing trace to constraints file: %s" % (filename)) @@ -1302,7 +1194,7 @@ def write_constr_trace(steps, index): constr_prefix = smtctop[1] + "." if smtcinit: - steps = [steps[-1]] + steps_start = steps_stop - 1 with open(filename, "w") as f: primary_inputs = list() @@ -1311,13 +1203,13 @@ def write_constr_trace(steps, index): width = smt.modinfo[constr_topmod].wsize[name] primary_inputs.append((name, width)) - if steps[0] == 0 or smtcinit: + if steps_start == 0 or smtcinit: print("initial", file=f) else: - print("state %d" % steps[0], file=f) + print("state %d" % steps_start, file=f) regnames = sorted(smt.hiernets(constr_topmod, regs_only=True)) - regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps[0]))) + regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start))) for name, val in zip(regnames, regvals): print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f) @@ -1328,7 +1220,7 @@ def write_constr_trace(steps, index): addr_expr_list = list() data_expr_list = list() - for i in steps: + for i in range(steps_start, steps_stop): for j in range(rports): addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j)) data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j)) @@ -1344,7 +1236,7 @@ def write_constr_trace(steps, index): for addr, data in addr_data.items(): print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f) - for k in steps: + for k in range(steps_start, steps_stop): if not smtcinit: print("", file=f) print("state %d" % k, file=f) @@ -1355,14 +1247,11 @@ def write_constr_trace(steps, index): for name, val in zip(pi_names, pi_values): print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f) -def write_yw_trace(steps, index, allregs=False, filename=None): - if filename is None: - if outywfile is None: - return - filename = outywfile.replace("%", index) - print_msg("Writing trace to Yosys witness file: %s" % (filename)) +def write_yw_trace(steps_start, steps_stop, index, allregs=False): + filename = outywfile.replace("%", index) + print_msg("Writing trace to Yosys witness file: %s" % (filename)) - mem_trace_data = collect_mem_trace_data(steps) + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) with open(filename, "w") as f: inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs) @@ -1406,28 +1295,18 @@ def write_yw_trace(steps, index, allregs=False, filename=None): sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True) mem_init_values.append((sig, overlap_bits.replace("x", "?"))) - exprs = [] - all_sigs = [] - - for i, k in enumerate(steps): + for k in range(steps_start, steps_stop): step_values = WitnessValues() - if not i: + if k == steps_start: for sig, value in mem_init_values: step_values[sig] = value sigs = inits + seqs else: sigs = seqs - exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs) - - all_sigs.append((step_values, sigs)) - - bvs = iter(smt.get_list(exprs)) - - for (step_values, sigs) in all_sigs: for sig in sigs: - value = smt.bv2bin(next(bvs)) + value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig))) step_values[sig["sig"]] = value yw.step(step_values) @@ -1435,24 +1314,17 @@ def write_yw_trace(steps, index, allregs=False, filename=None): def write_trace(steps_start, steps_stop, index, allregs=False): - if steps_stop is None: - steps = steps_start - seq_time = True - else: - steps = list(range(steps_start, steps_stop)) - seq_time = False - if vcdfile is not None: - write_vcd_trace(steps, index, seq_time=seq_time) + write_vcd_trace(steps_start, steps_stop, index) if vlogtbfile is not None: - write_vlogtb_trace(steps, index) + write_vlogtb_trace(steps_start, steps_stop, index) if outconstr is not None: - write_constr_trace(steps, index) + write_constr_trace(steps_start, steps_stop, index) if outywfile is not None: - write_yw_trace(steps, index, allregs) + write_yw_trace(steps_start, steps_stop, index, allregs) def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()): @@ -1570,44 +1442,6 @@ 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()] @@ -1762,18 +1596,7 @@ 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() - -elif tempind: +if tempind: retstatus = "FAILED" skip_counter = step_size for step in range(num_steps, -1, -1): @@ -1782,7 +1605,7 @@ def report_tracked_assumptions(msg): break smt_state(step) - smt_assert_design_assumes(step) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, 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)) @@ -1825,7 +1648,6 @@ def report_tracked_assumptions(msg): else: print_msg("Temporal induction successful.") - report_tracked_assumptions("Used assumptions:") retstatus = "PASSED" break @@ -1851,7 +1673,7 @@ def report_tracked_assumptions(msg): while step < num_steps: smt_state(step) - smt_assert_design_assumes(step) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1872,7 +1694,6 @@ def report_tracked_assumptions(msg): 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 @@ -1881,14 +1702,13 @@ def report_tracked_assumptions(msg): print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_design_assumes(i) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, 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 @@ -1944,7 +1764,7 @@ def report_tracked_assumptions(msg): retstatus = "PASSED" while step < num_steps: smt_state(step) - smt_assert_design_assumes(step) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) smt_assert_consequent(get_constr_expr(constr_assumes, step)) @@ -1974,7 +1794,7 @@ def report_tracked_assumptions(msg): if step+i < num_steps: smt_state(step+i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i)) - smt_assert_design_assumes(step + i) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, 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)) @@ -1988,8 +1808,7 @@ def report_tracked_assumptions(msg): print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) if smt_check_sat() == "unsat": - print_msg("Assumptions are unsatisfiable!") - report_tracked_assumptions("Conficting assumptions:") + print("%s Assumptions are unsatisfiable!" % smt.timestamp()) retstatus = "PREUNSAT" break @@ -2042,14 +1861,13 @@ def report_tracked_assumptions(msg): print_msg("Appending additional step %d." % i) smt_state(i) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) - smt_assert_design_assumes(i) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, 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_msg("Cannot append steps without violating assumptions!") - report_tracked_assumptions("Conflicting assumptions:") + print("%s Cannot append steps without violating assumptions!" % smt.timestamp()) retstatus = "FAILED" break print_anyconsts(step) @@ -2136,6 +1954,5 @@ def report_tracked_assumptions(msg): smt.write("(exit)") smt.wait() -if not incremental: - print_msg("Status: %s" % retstatus) - sys.exit(0 if retstatus == "PASSED" else 1) +print_msg("Status: %s" % retstatus) +sys.exit(0 if retstatus == "PASSED" else 1) diff --git a/yosys/backends/smt2/smtbmc_incremental.py b/yosys/backends/smt2/smtbmc_incremental.py deleted file mode 100644 index 0bd280b4a48..00000000000 --- a/yosys/backends/smt2/smtbmc_incremental.py +++ /dev/null @@ -1,616 +0,0 @@ -from collections import defaultdict -import json -import typing -import ywio - -if typing.TYPE_CHECKING: - import smtbmc -else: - import sys - - smtbmc = sys.modules["__main__"] - - -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 - - self.state_set = set() - self.map_cache = {} - - self._cached_hierwitness = {} - self._witness_index = None - - self._yw_constraints = {} - self._define_sorts = {} - - def setup(self): - generic_assert_map = smtbmc.get_assert_map( - smtbmc.topmod, "state", smtbmc.topmod - ) - self.inv_generic_assert_map = { - tuple(data[1:]): key for key, data in generic_assert_map.items() - } - assert len(self.inv_generic_assert_map) == len(generic_assert_map) - - def print_json(self, **kwargs): - print(json.dumps(kwargs), flush=True) - - def print_msg(self, msg): - self.print_json(msg=msg) - - def get_cached_assert(self, step, name): - try: - assert_map = self.map_cache[step] - except KeyError: - assert_map = self.map_cache[step] = smtbmc.get_assert_map( - smtbmc.topmod, f"s{step}", smtbmc.topmod - ) - return assert_map[self.inv_generic_assert_map[name]][0] - - def arg_step(self, cmd, declare=False, name="step", optional=False): - step = cmd.get(name, None) - if step is None and optional: - return None - if not isinstance(step, int): - if optional: - raise InteractiveError(f"{name} must be an integer") - else: - raise InteractiveError(f"integer {name} argument required") - if declare and step in self.state_set: - raise InteractiveError(f"step {step} already declared") - if not declare and step not in self.state_set: - raise InteractiveError(f"step {step} not declared") - return step - - def expr_arg_len(self, expr, min_len, max_len=-1): - if max_len == -1: - max_len = min_len - arg_len = len(expr) - 1 - - if min_len is not None and arg_len < min_len: - if min_len == max_len: - raise InteractiveError( - f"{json.dumps(expr[0])} expression must have " - f"{min_len} argument{'s' if min_len != 1 else ''}" - ) - else: - 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 InteractiveError( - f"{json.dumps(expr[0])} expression can have at most " - f"{min_len} argument{'s' if max_len != 1 else ''}" - ) - - def expr_step(self, expr, smt_out): - self.expr_arg_len(expr, 1) - step = expr[1] - if step not in self.state_set: - raise InteractiveError(f"step {step} not declared") - smt_out.append(f"s{step}") - return "module", smtbmc.topmod - - 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[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:] - 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" - - def expr_mod_constraint2(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]) - smt_out.append(" ") - self.expr(expr[2], smt_out, required_sort=arg_sort) - module = arg_sort[1] - suffix = expr[0][3:] - smt_out[position] = f"(|{module}{suffix}| " - smt_out.append(")") - return "Bool" - - def expr_not(self, expr, smt_out): - self.expr_arg_len(expr, 1) - - smt_out.append("(not ") - self.expr(expr[1], smt_out, required_sort="Bool") - smt_out.append(")") - return "Bool" - - def expr_eq(self, expr, smt_out): - self.expr_arg_len(expr, 2) - - smt_out.append("(= ") - arg_sort = self.expr(expr[1], smt_out) - if ( - smtbmc.smt.unroll - and isinstance(arg_sort, (list, tuple)) - and arg_sort[0] == "module" - ): - raise InteractiveError("state equality not supported in unroll mode") - - smt_out.append(" ") - self.expr(expr[2], smt_out, required_sort=arg_sort) - smt_out.append(")") - return "Bool" - - def expr_andor(self, expr, smt_out): - if len(expr) == 1: - smt_out.push({"and": "true", "or": "false"}[expr[0]]) - elif len(expr) == 2: - self.expr(expr[1], smt_out, required_sort="Bool") - else: - sep = f"({expr[0]} " - for arg in expr[1:]: - smt_out.append(sep) - sep = " " - self.expr(arg, smt_out, required_sort="Bool") - 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] - elif len(expr) == 3: - name = expr[1] - step = expr[2] - - if step not in self.state_set: - raise InteractiveError(f"step {step} not declared") - - if name not in self._yw_constraints: - raise InteractiveError(f"no yw file loaded as name {name!r}") - - constraints = self._yw_constraints[name].get(step, []) - - if len(constraints) == 0: - smt_out.append("true") - elif len(constraints) == 1: - smt_out.append(constraints[0]) - else: - sep = "(and " - for constraint in constraints: - smt_out.append(sep) - sep = " " - smt_out.append(constraint) - smt_out.append(")") - - 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) - - smtlib_expr = expr[1] - sort = expr[2] - - if not isinstance(smtlib_expr, str): - raise InteractiveError( - "raw SMT-LIB expression has to be a string, " - f"got {json.dumps(smtlib_expr)}" - ) - - 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 - - def expr_label(self, expr, smt_out): - if len(expr) != 3: - raise InteractiveError( - f'expected ["!", label, sub_expr], got {json.dumps(expr)}' - ) - label = expr[1] - subexpr = expr[2] - - if not isinstance(label, str): - raise InteractiveError("expression label has to be a string") - - 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, - "mod_a": expr_mod_constraint, - "mod_u": expr_mod_constraint, - "mod_t": expr_mod_constraint2, - "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, - } - - def expr(self, expr, smt_out, required_sort=None): - if not isinstance(expr, (list, tuple)) or not expr: - raise InteractiveError( - f"expression must be a non-empty JSON array, found: {json.dumps(expr)}" - ) - name = expr[0] - - handler = self.expr_handlers.get(name) - if handler: - sort = handler(self, expr, smt_out) - - if required_sort is not None: - if isinstance(required_sort, (list, tuple)): - if ( - not isinstance(sort, (list, tuple)) - or len(sort) != len(required_sort) - or any( - r is not None and r != s - for r, s in zip(required_sort, sort) - ) - ): - raise InteractiveError( - f"required sort {json.dumps(required_sort)} " - f"found sort {json.dumps(sort)}" - ) - return sort - 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 = [] - output_sort = self.expr(expr, smt_out, required_sort=required_sort) - out = "".join(smt_out) - return out, output_sort - - def cmd_new_step(self, cmd): - step = self.arg_step(cmd, declare=True) - self.state_set.add(step) - smtbmc.smt_state(step) - - def cmd_assert(self, cmd): - name = cmd.get("cmd") - - assert_fn = { - "assert_antecedent": smtbmc.smt_assert_antecedent, - "assert_consequent": smtbmc.smt_assert_consequent, - "assert": smtbmc.smt_assert, - }[name] - - 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() - - def cmd_pop(self, cmd): - smtbmc.smt_pop() - - def cmd_check(self, cmd): - return smtbmc.smt_check_sat() - - 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)) - if self._cached_hierwitness[allregs] is not None: - return self._cached_hierwitness[allregs] - inits, seqs, clocks, mems = smtbmc.smt.hierwitness(smtbmc.topmod, allregs) - self._cached_hierwitness[allregs] = result = dict( - inits=inits, seqs=seqs, clocks=clocks, mems=mems - ) - return result - - def cmd_write_yw_trace(self, cmd): - steps = cmd.get("steps") - allregs = bool(cmd.get("allregs", False)) - - if steps is None: - steps = sorted(self.state_set) - - path = cmd.get("path") - - smtbmc.write_yw_trace(steps, self.traceidx, allregs=allregs, filename=path) - - if path is None: - self.traceidx += 1 - - def cmd_read_yw_trace(self, cmd): - steps = cmd.get("steps") - path = cmd.get("path") - name = cmd.get("name") - skip_x = cmd.get("skip_x", False) - if path is None: - raise InteractiveError("path required") - - constraints = defaultdict(list) - - if steps is None: - steps = sorted(self.state_set) - - map_steps = {i: int(j) for i, j in enumerate(steps)} - - last_step = smtbmc.ywfile_constraints( - path, constraints, map_steps=map_steps, skip_x=skip_x - ) - - self._yw_constraints[name] = { - map_steps.get(i, i): [smtexpr for cexfile, smtexpr in constraint_list] - for i, constraint_list in constraints.items() - } - - 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 - - cmd_handlers = { - "new_step": cmd_new_step, - "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, - } - - def handle_command(self, cmd): - if not isinstance(cmd, dict) or "cmd" not in cmd: - raise InteractiveError('object with "cmd" key required') - - name = cmd.get("cmd", None) - - handler = self.cmd_handlers.get(name) - if handler: - return handler(self, cmd) - else: - raise InteractiveError(f"unknown command: {name}") - - def mainloop(self): - self.setup() - while True: - try: - cmd = input().strip() - if not cmd or cmd.startswith("#") or cmd.startswith("//"): - continue - try: - cmd = json.loads(cmd) - except json.decoder.JSONDecodeError as e: - self.print_json(err=f"invalid JSON: {e}") - continue - except EOFError: - break - - try: - result = self.handle_command(cmd) - except InteractiveError as e: - self.print_json(err=str(e)) - continue - except Exception as e: - self.print_json(err=f"internal error: {e}") - raise - else: - self.print_json(ok=result) diff --git a/yosys/backends/smt2/smtio.py b/yosys/backends/smt2/smtio.py index 5fc3ab5a424..0ec7f08f4dc 100644 --- a/yosys/backends/smt2/smtio.py +++ b/yosys/backends/smt2/smtio.py @@ -79,20 +79,6 @@ def except_hook(exctype, value, traceback): sys.excepthook = except_hook -def recursion_helper(iteration, *request): - stack = [iteration(*request)] - - while stack: - top = stack.pop() - try: - request = next(top) - except StopIteration: - continue - - stack.append(top) - stack.append(iteration(*request)) - - hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -114,7 +100,6 @@ def __init__(self): self.clocks = dict() self.cells = dict() self.asserts = dict() - self.assumes = dict() self.covers = dict() self.maximize = set() self.minimize = set() @@ -142,7 +127,6 @@ 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 @@ -160,7 +144,6 @@ 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" @@ -315,22 +298,10 @@ def replace_in_stmt(self, stmt, pat, repl): return stmt def unroll_stmt(self, stmt): - result = [] - recursion_helper(self._unroll_stmt_into, stmt, result) - return result.pop() - - def _unroll_stmt_into(self, stmt, output, depth=128): if not isinstance(stmt, list): - output.append(stmt) - return + return stmt - new_stmt = [] - for s in stmt: - if depth: - yield from self._unroll_stmt_into(s, new_stmt, depth - 1) - else: - yield s, new_stmt - stmt = new_stmt + stmt = [self.unroll_stmt(s) for s in stmt] if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls: assert stmt[1] in self.unroll_objs @@ -359,19 +330,12 @@ def _unroll_stmt_into(self, stmt, output, depth=128): decl[2] = list() if len(decl) > 0: - tmp = [] - if depth: - yield from self._unroll_stmt_into(decl, tmp, depth - 1) - else: - yield decl, tmp - - decl = tmp.pop() + decl = self.unroll_stmt(decl) self.write(self.unparse(decl), unroll=False) - output.append(self.unroll_cache[key]) - return + return self.unroll_cache[key] - output.append(stmt) + return stmt def p_thread_main(self): while True: @@ -605,12 +569,6 @@ 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]) @@ -794,13 +752,8 @@ 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(f"> {check_stmt}") + print("> (check-sat)") if self.debug_file and not self.nocomments: print("; running check-sat..", file=self.debug_file) self.debug_file.flush() @@ -814,7 +767,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(f"{check_stmt}\n", True) + self.p_write("(check-sat)\n", True) if self.timeinfo: i = 0 @@ -882,7 +835,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_stmt, file=self.debug_file) + print("(check-sat)", file=self.debug_file) self.debug_file.flush() if result not in expected: @@ -959,55 +912,6 @@ 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] @@ -1016,7 +920,7 @@ def get_list(self, expr_list): if len(expr_list) == 0: return [] self.write("(get-value (%s))" % " ".join(expr_list)) - return [n[1] for n in self.parse(self.read()) if n] + return [n[1] for n in self.parse(self.read())] def get_path(self, mod, path): assert mod in self.modinfo @@ -1154,7 +1058,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", "smt2-option="] + self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] self.solver = "yices" self.solver_opts = list() self.debug_print = False @@ -1167,7 +1071,6 @@ def __init__(self): self.logic = None self.info_stmts = list() self.nocomments = False - self.smt2_options = {} def handle(self, o, a): if o == "-s": @@ -1194,13 +1097,6 @@ 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