experiments: run fpga repairs with bitwuzla as well #714
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: Bug Fix Unittests | |
on: | |
push: | |
pull_request: | |
jobs: | |
test-rust: | |
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 }} | |
- name: Install Tabby OSS Cad Suite (from YosysHQ) | |
uses: YosysHQ/setup-oss-cad-suite@v2 | |
with: | |
version: '2022-06-22' | |
- uses: actions/checkout@v4 | |
with: | |
submodules: true | |
- name: Build | |
working-directory: synth | |
run: cargo build --verbose | |
- name: Run tests | |
working-directory: synth | |
run: cargo test --verbose | |
- name: Check Formatting | |
working-directory: synth | |
run: cargo fmt --check | |
test-python: | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: true | |
- name: Install Tabby OSS Cad Suite (from YosysHQ) | |
uses: YosysHQ/setup-oss-cad-suite@v2 | |
with: | |
version: '2022-06-22' | |
- name: Install CVC4 | |
run: sudo apt-get install -y cvc4 | |
- name: Print Solver Versions | |
run: | | |
z3 -version | |
cvc4 --version | |
verilator -version | |
- name: Compile Synthesizer | |
working-directory: synth | |
run: cargo build --release | |
- name: Set up Python | |
uses: actions/setup-python@v4 | |
with: | |
python-version: "3.10" | |
- name: Create Virtual Environment and Install Requirements | |
run: | | |
python3 -m venv venv | |
source venv/bin/activate | |
pip install -r requirements.txt | |
- name: Run Python Unittests | |
timeout-minutes: 15 | |
run: | | |
source venv/bin/activate | |
# avoid a race condition by ensuring that file exists | |
mkdir -p working-dir | |
pytest -n auto test.py | |
test-benchmarks: | |
name: Common Benchmark Tests | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v3 | |
- name: Install Icarus Verilog | |
run: sudo apt-get install -y iverilog | |
- name: Set up Python | |
uses: actions/setup-python@v3 | |
with: | |
python-version: "3.10" | |
- name: Create Virtual Environment and Install Requirements | |
run: | | |
python3 -m venv venv | |
source venv/bin/activate | |
pip install -r requirements.txt | |
- name: Check Benchmark Configuration Data | |
run: | | |
source venv/bin/activate | |
./scripts/load_all_benchmarks.py | |
test-repair-check: | |
name: Check Repairs Tests | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: true | |
- name: Install Icarus Verilog | |
run: sudo apt-get install -y iverilog | |
- name: Set up Python | |
uses: actions/setup-python@v3 | |
with: | |
python-version: "3.10" | |
- name: Install Tabby OSS Cad Suite (from YosysHQ) | |
uses: YosysHQ/setup-oss-cad-suite@v2 | |
with: | |
version: '2022-06-22' | |
- name: Create Virtual Environment and Install Requirements | |
run: | | |
python3 -m venv venv | |
source venv/bin/activate | |
pip install -r requirements.txt | |
- name: Check Repairs found by CirFix for the mux_4_1 benchmark (and also RTL-Repair results) | |
run: | | |
source venv/bin/activate | |
./scripts/check_repairs.py --working-dir=tmp --results=results/test-results --sim=iverilog | |
cat tmp/mux_4_1_wadden_buggy1_oracle-full_repair_2021-07-20-23:50:05.log | |
cat tmp/axis-adapter-s3_s3_csv/result.toml | |
test-cirfix: | |
name: Test CirFix Quick Repairs | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: true | |
- name: Install Icarus Verilog | |
run: sudo apt-get install -y iverilog | |
- name: Set up Python | |
uses: actions/setup-python@v3 | |
with: | |
python-version: "3.10" | |
- name: Create Virtual Environment and Install Requirements | |
run: | | |
python3 -m venv venv | |
source venv/bin/activate | |
pip install -r requirements.txt | |
- name: Repair first_counter_overflow_wadden_buggy1 | |
timeout-minutes: 3 | |
run: | | |
source venv/bin/activate | |
cd cirfix | |
cd prototype | |
python3 repair.py --project=../../benchmarks/cirfix/first_counter_overflow --bug=wadden_buggy1 --log --working-dir=first_counter_overflow_wadden_buggy1 --seed="repair_2020-09-23-11:24:14" --simulator=iverilog | |
- name: Repair padder_ssscrazy_buggy1 | |
timeout-minutes: 3 | |
run: | | |
source venv/bin/activate | |
cd cirfix | |
cd prototype | |
python3 repair.py --project=../../benchmarks/cirfix/opencores/sha3/low_throughput_core/padder.toml --bug=ssscrazy_buggy1 --log --working-dir=padder_ssscrazy_buggy1 --seed="repair_2020-09-24-15:16:49" --simulator=iverilog | |
- name: Repair first_counter_overflow_wadden_buggy1 using the run.py script | |
timeout-minutes: 3 | |
run: | | |
source venv/bin/activate | |
cd cirfix | |
./run.py --working-dir=counter-wadden1 --experiment=first-counter-wadden-1 --threads=2 --simulator=iverilog |