Skip to content
Rust

ts: make get_all_expressions a method #477

Sign in to view logs

ts: make get_all_expressions a method

ts: make get_all_expressions a method #477

Workflow file for this run

.github/workflows/test.yml at 3520c49
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
bmc:
name: Test BMC Example
runs-on: ubuntu-latest
timeout-minutes: 5
strategy:
matrix:
toolchain:
- stable
solver:
- bitwuzla
- yices2
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 -- --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-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 --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-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