interpreter: implement array ite and const #168
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-latest | |
| 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@v3 | |
| - name: Build | |
| run: cargo build --verbose | |
| - name: Run tests | |
| run: cargo test --verbose | |
| examples: | |
| name: Try Examples | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - uses: YosysHQ/setup-oss-cad-suite@v2 | |
| with: | |
| version: '2023-11-15' | |
| - name: Update Rust to ${{ matrix.toolchain }} | |
| run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }} | |
| - uses: actions/checkout@v3 | |
| - name: Build | |
| run: cargo build --verbose --examples --release | |
| - name: bmc Quiz1 | |
| run: | | |
| cargo run --release --example bmc -- 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 -- inputs/chiseltest/Quiz1.unsat.btor | |
| - name: bmc const array example | |
| run: | | |
| cargo run --release --example bmc -- 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 -- 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 -- inputs/chiseltest/Quiz2.unsat.btor | |
| - name: bmc Quiz4 | |
| run: | | |
| cargo run --release --example bmc -- 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 -- inputs/chiseltest/Quiz4.unsat.btor | |
| - 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 | |
| - 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 | |
| semver: | |
| name: Check Semantic Versioning | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - uses: obi1kenobi/cargo-semver-checks-action@v2 | |
| format: | |
| name: Check Formatting | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - run: cargo fmt --check |