Skip to content
Rust

add output serialization test #505

Sign in to view logs

add output serialization test

add output serialization test #505

Workflow file for this run

.github/workflows/test.yml at bf32cc3
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