cond synth: print out smt expressions #583
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 | |
| BITWUZLA_VERSION: 0.6.1 | |
| YICES_VERSION: 2.6.5 | |
| 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 Tool | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 15 | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| solver: | |
| - bitwuzla | |
| - yices2 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Set Up Yices | |
| if: ${{ matrix.solver == 'yices2' }} | |
| uses: ./.github/workflows/setup-yices | |
| with: | |
| version: ${{ env.YICES_VERSION }} | |
| - name: Set Up Bitwuzla | |
| if: ${{ matrix.solver == 'bitwuzla' }} | |
| uses: ./.github/workflows/setup-bitwuzla | |
| with: | |
| version: ${{ env.BITWUZLA_VERSION }} | |
| - 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 }} | |
| - name: Build | |
| run: cargo build --verbose --release -p bmc | |
| - name: bmc Quiz1 | |
| run: | | |
| cargo run --release -p 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 -p 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 -p 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 -p 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 -p bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz2.unsat.btor | |
| - name: bmc Quiz4 | |
| run: | | |
| cargo run --release -p 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 -p bmc -- --solver=${{ matrix.solver }} inputs/chiseltest/Quiz4.unsat.btor | |
| sim: | |
| name: Test Simulator Tool | |
| 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 --release -p sim | |
| - name: simulate mux | |
| run: | | |
| cargo run --release -p 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 -p sim -- --testbench=inputs/repair/keccak.original.tb.csv inputs/repair/keccak.original.btor | |
| - name: simulate sdram controller | |
| run: | | |
| cargo run --release -p sim -- --testbench=inputs/repair/sdram_controller.original.tb.csv inputs/repair/sdram_controller.original.btor | |
| - name: simulate i2c controller | |
| run: | | |
| cargo run --release -p 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 -p 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 -p 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 -p 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 -p 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 -p 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 -p 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 -p 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 -p 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 -p sim -- --init=zero --testbench=inputs/repair/axi-lite-xlnx.original.tb0.csv inputs/repair/axi-lite-xlnx.original.btor | |
| cargo run --release -p 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 -p sim -- --init=zero --testbench=inputs/repair/axi-stream-xlnx.original.tb.csv inputs/repair/axi-stream-xlnx.original.btor | |
| rewrite-condition: | |
| name: Test E-Graph Rewrite Condition Synthesizer | |
| 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: Set Up Bitwuzla | |
| uses: ./.github/workflows/setup-bitwuzla | |
| with: | |
| version: ${{ env.BITWUZLA_VERSION }} | |
| - name: Build | |
| run: cargo build --verbose --release -p patronus-egraphs-cond-synth | |
| - name: synthesize commute-add condition | |
| run: | | |
| cargo run --release -p patronus-egraphs-cond-synth -- --bdd-formula commute-add | |
| semver: | |
| name: Check Semantic Versioning of Patronus | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: obi1kenobi/cargo-semver-checks-action@v2 | |
| with: | |
| package: patronus | |
| format: | |
| name: Check Formatting | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: cargo fmt --check |