update todo #508
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Rust | |
| on: | |
| push: | |
| pull_request: | |
| env: | |
| CARGO_TERM_COLOR: always | |
| jobs: | |
| tests: | |
| name: Unit Tests | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Update Rust to ${{ matrix.toolchain }} | |
| run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }} | |
| - uses: actions/checkout@v4 | |
| - name: Build | |
| run: cargo build --verbose | |
| - name: Run tests | |
| run: cargo test --verbose | |
| bmc: | |
| name: Test BMC Example | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 15 | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| solver: | |
| - bitwuzla | |
| - yices2 | |
| steps: | |
| - name: Install Yices2 | |
| if: ${{ matrix.solver == 'yices2' }} | |
| run: | | |
| mkdir /tmp/yices2 | |
| cd /tmp/yices2 | |
| wget -q https://yices.csl.sri.com/releases/2.6.5/yices-2.6.5-x86_64-pc-linux-gnu-static-gmp.tar.gz -O yices.tar.gz | |
| tar -xf yices.tar.gz | |
| mv yices-*/* . | |
| echo "/tmp/yices2/bin" >> "$GITHUB_PATH" | |
| - name: Install Bitwuzla | |
| if: ${{ matrix.solver == 'bitwuzla' }} | |
| run: | | |
| sudo apt-get install -y meson | |
| mkdir /tmp/bitwuzla | |
| cd /tmp/bitwuzla | |
| wget -q https://github.com/bitwuzla/bitwuzla/archive/refs/tags/0.6.1.zip -O bitwuzla.zip | |
| unzip -q bitwuzla.zip | |
| mv bitwuzla-*/* . | |
| ./configure.py | |
| cd build | |
| ninja | |
| sudo ninja install | |
| - name: Install btor sim | |
| run: | | |
| mkdir /tmp/btor | |
| cd /tmp/btor | |
| git clone https://github.com/hwmcc/btor2tools.git | |
| cd btor2tools | |
| ./configure.sh | |
| cd build | |
| make | |
| echo "/tmp/btor/btor2tools/build/bin/" >> "$GITHUB_PATH" | |
| - name: Update Rust to ${{ matrix.toolchain }} | |
| run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }} | |
| - uses: actions/checkout@v4 | |
| - name: Build | |
| run: cargo build --verbose --examples --release | |
| - name: bmc Quiz1 | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz1.btor > Quiz1.wit | |
| btorsim inputs/chiseltest/Quiz1.btor Quiz1.wit | |
| - name: bmc Quiz1 (with additional assumption) | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz1.unsat.btor | |
| - name: bmc const array example | |
| if: ${{ matrix.solver != 'yices2' }} # yices2 returns memory values that cannot be parsed | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/const_array_example.btor > const_array_example.wit | |
| btorsim inputs/chiseltest/const_array_example.btor const_array_example.wit | |
| - name: bmc Quiz2 | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz2.sat.btor > Quiz2.sat.wit | |
| btorsim inputs/chiseltest/Quiz2.sat.btor Quiz2.sat.wit | |
| - name: bmc Quiz2 (with counter reset value) | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz2.unsat.btor | |
| - name: bmc Quiz4 | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz4.sat.btor > Quiz4.sat.wit | |
| btorsim inputs/chiseltest/Quiz4.sat.btor Quiz4.sat.wit | |
| - name: bmc Quiz4 (with counter reset value) | |
| run: | | |
| cargo run --release --example bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz4.unsat.btor | |
| sim: | |
| name: Test SIM Example | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Update Rust to ${{ matrix.toolchain }} | |
| run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }} | |
| - uses: actions/checkout@v4 | |
| - name: Build | |
| run: cargo build --verbose --examples --release | |
| - name: simulate mux | |
| run: | | |
| cargo run --release --example sim -- --testbench=inputs/repair/mux_4_1.original.tb.csv inputs/repair/mux_4_1.original.btor | |
| # TODO: re-enable once we can parse large decimal input number | |
| #- name: simulate sha3 (keccak) | |
| # run: | | |
| # cargo run --release --example sim -- --testbench=inputs/repair/keccak.original.tb.csv inputs/repair/keccak.original.btor | |
| - name: simulate sdram controller | |
| run: | | |
| cargo run --release --example sim -- --testbench=inputs/repair/sdram_controller.original.tb.csv inputs/repair/sdram_controller.original.btor | |
| - name: simulate i2c controller | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/i2c_m.tb.csv inputs/repair/i2c_m.original.replace_literals.btor | |
| - name: simulate axis fifo (d4) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis-fifo-wrapper.original.tb.csv inputs/repair/axis-fifo-wrapper.original.btor | |
| - name: simulate axis adapter (s3) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis-adapter.original.tb.csv inputs/repair/axis-adapter.original.btor | |
| - name: simulate axis frame len (d13) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis_frame_len.original.tb.csv inputs/repair/axis_frame_len.original.btor | |
| - name: simulate axis fifo (d12) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis-fifo.original.tb.csv inputs/repair/axis-fifo.original.btor | |
| - name: simulate sd spi (c1, c3, d9) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/zipcpu_sdspi.original.tb.csv inputs/repair/zipcpu_sdspi.original.btor | |
| - name: simulate axis frame fifo (d11) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis-frame-fifo.original.tb.csv inputs/repair/axis-frame-fifo.original.btor | |
| - name: simulate axis switch (d8) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis-switch.original.tb.csv inputs/repair/axis-switch.original.btor | |
| - name: simulate axis async fifo (c4) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axis-async-fifo-wrapper.original.tb.csv inputs/repair/axis-async-fifo-wrapper.original.btor | |
| - name: simulate axi lite (s1) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axi-lite-xlnx.original.tb0.csv inputs/repair/axi-lite-xlnx.original.btor | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axi-lite-xlnx.original.tb1.csv inputs/repair/axi-lite-xlnx.original.btor | |
| - name: simulate axis stream (s2) | |
| run: | | |
| cargo run --release --example sim -- --init=zero --testbench=inputs/repair/axi-stream-xlnx.original.tb.csv inputs/repair/axi-stream-xlnx.original.btor | |
| semver: | |
| name: Check Semantic Versioning | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: obi1kenobi/cargo-semver-checks-action@v2 | |
| format: | |
| name: Check Formatting | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: cargo fmt --check |