Skip to content

Commit 967ea07

Browse files
committed
--check-complete, split formal/non-formal CI
1 parent bfb5916 commit 967ea07

3 files changed

Lines changed: 203 additions & 147 deletions

File tree

.github/workflows/ci-formal.yml

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
# Copyright lowRISC contributors.
2+
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
3+
# SPDX-License-Identifier: Apache-2.0
4+
5+
# GitHub Actions CI build configuration
6+
7+
name: Ibex OSS Formal CI
8+
9+
on:
10+
push:
11+
- paths:
12+
- "flake.nix"
13+
- "flake.lock"
14+
- "dv/formal/**"
15+
- "rtl/**"
16+
- "vendor/**"
17+
merge_group:
18+
types:
19+
- checks_requested
20+
pull_request:
21+
- paths:
22+
- "flake.nix"
23+
- "flake.lock"
24+
- "dv/formal/**"
25+
- "rtl/**"
26+
- "vendor/**"
27+
28+
jobs:
29+
fv:
30+
name: Run the Open-Source FV flow
31+
runs-on: nixos-25.05
32+
steps:
33+
- uses: actions/checkout@v4
34+
35+
- name: Setup env
36+
run: |
37+
echo "NIX_CONFIG=accept-flake-config = true" >> $GITHUB_ENV
38+
39+
- name: Install Nix
40+
uses: cachix/install-nix-action@v27
41+
with:
42+
extra_nix_config: |
43+
substituters = https://nix-cache.lowrisc.org/public/ https://cache.nixos.org/
44+
trusted-public-keys = nix-cache.lowrisc.org-public-1:O6JLD0yXzaJDPiQW1meVu32JIDViuaPtGDfjlOopU7o= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
45+
46+
- name: Setup Cache
47+
if: github.event_name != 'pull_request'
48+
run: |
49+
# Obtain OIDC token from GitHub
50+
GITHUB_ID_TOKEN=$(curl -sSf -H "Authorization: Bearer $ACTIONS_ID_TOKEN_REQUEST_TOKEN" "$ACTIONS_ID_TOKEN_REQUEST_URL&audience=https://ca.lowrisc.org" | jq -r .value)
51+
echo "::add-mask::$GITHUB_ID_TOKEN"
52+
# Exchange for a token for nix cache
53+
NIX_CACHE_TOKEN=$(curl -sSf -H "Authorization: Bearer $GITHUB_ID_TOKEN" "https://ca.lowrisc.org/api/nix-caches/public/token")
54+
echo "::add-mask::$NIX_CACHE_TOKEN"
55+
nix profile install nixpkgs#attic-client
56+
attic login --set-default lowrisc https://nix-cache.lowrisc.org/ "$NIX_CACHE_TOKEN"
57+
58+
- name: Run OSS Env
59+
run: |
60+
source <(nix print-dev-env .#oss-dev)
61+
62+
if ${{ github.event_name != 'pull_request' }}; then
63+
attic push public result*
64+
fi
65+
66+
cd dv/formal
67+
make build/aig-manip
68+
make build/all.aig SHELL=bash
69+
python3 conductor.py prove --check-all
70+

.github/workflows/ci.yml

Lines changed: 119 additions & 144 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ name: Ibex CI
88

99
on:
1010
push:
11-
branches:
11+
tags:
1212
- "*"
1313
merge_group:
1414
types:
@@ -23,154 +23,129 @@ on:
2323
# improve end-to-end CI times.
2424

2525
jobs:
26-
# lint_dv:
27-
# name: Run quality checks (Lint and DV)
28-
# runs-on: ubuntu-22.04
29-
# steps:
30-
# - uses: actions/checkout@v4
31-
# with:
32-
# # Fetch all history so that we can run git diff on the base branch
33-
# fetch-depth: 0
34-
35-
# - name: Setup environment variables
36-
# run: |
37-
# # Filter out empty lines or comments
38-
# grep -v '^\(#\|$\)' ci/vars.env >> $GITHUB_ENV
39-
40-
# - name: Install build dependencies
41-
# run: |
42-
# ci/install-build-deps.sh
43-
44-
# - name: Display environment
45-
# run: |
46-
# echo $PATH
47-
# python3 --version
48-
# echo -n "fusesoc "
49-
# fusesoc --version
50-
# verilator --version
51-
# riscv32-unknown-elf-gcc --version
52-
# verible-verilog-lint --version
53-
54-
# # Verible format is experimental so only run on default config for now,
55-
# # will eventually become part of the per-config CI
56-
# - name: Format all source code with Verible format (experimental)
57-
# run: |
58-
# set +e
59-
# fusesoc --cores-root . run --no-export --target=format --tool=veribleformat lowrisc:ibex:ibex_top_tracing
60-
# if [ $? != 0 ]; then
61-
# echo -n "::error::"
62-
# echo "Verilog format with Verible failed. Run 'fusesoc --cores-root . run --no-export --target=format --tool=veribleformat lowrisc:ibex:ibex_top_tracing' to check and fix all errors."
63-
# echo "This flow is currently experimental and failures can be ignored."
64-
# fi
65-
# # Show diff of what verilog_format would have changed, and then revert.
66-
# git diff --no-pager
67-
# git reset --hard HEAD
68-
# continue-on-error: true
69-
70-
# - name: Use clang-format to check C/C++ coding style
71-
# # This check is not idempotent, but checks changes to a base branch.
72-
# # Run it only on pull requests.
73-
# if: github.event_name == 'pull_request'
74-
# run: |
75-
# set +e
76-
# fork_origin=${{ github.event.pull_request.base.sha }}
77-
# changed_files=$(git diff --name-only $fork_origin | grep -v '^vendor' | grep -E '\.(cpp|cc|c|h)$')
78-
# test -z "$changed_files" || git diff -U0 $fork_origin $changed_files | clang-format-diff -p1 | tee clang-format-output
79-
# if [ -s clang-format-output ]; then
80-
# echo -n "::error::"
81-
# echo "C/C++ lint failed. Use 'git clang-format' with appropriate options to reformat the changed code."
82-
# exit 1
83-
# fi
84-
85-
# - name: Build and run CSR testbench with Verilator
86-
# run: |
87-
# # Build and run CSR testbench, chosen Ibex configuration does not effect
88-
# # this so doesn't need to be part of per-config CI
89-
# fusesoc --cores-root=. run --target=sim --tool=verilator lowrisc:ibex:tb_cs_registers
90-
91-
# - name: Get RISC-V Compliance test suite
92-
# run: |
93-
# cd build
94-
# git clone https://github.com/riscv/riscv-compliance.git
95-
# cd riscv-compliance
96-
# git checkout "$RISCV_COMPLIANCE_GIT_VERSION"
97-
98-
# - name: Build tests for verilator co-simulation
99-
# run: |
100-
# # Build CoreMark without performance counter dump for co-simulation testing
101-
# make -C ./examples/sw/benchmarks/coremark SUPPRESS_PCOUNT_DUMP=1
102-
# make -C ./examples/sw/simple_system/pmp_smoke_test
103-
# make -C ./examples/sw/simple_system/dit_test
104-
# make -C ./examples/sw/simple_system/dummy_instr_test
105-
106-
# # Run Ibex RTL CI per supported configuration
107-
# - name: Run Ibex RTL CI for small configuration
108-
# uses: ./.github/actions/ibex-rtl-ci-steps
109-
# with:
110-
# ibex_config: small
111-
# - name: Run Ibex RTL CI for opentitan configuration
112-
# uses: ./.github/actions/ibex-rtl-ci-steps
113-
# with:
114-
# ibex_config: opentitan
115-
# - name: Run Ibex RTL CI for maxperf configuration
116-
# uses: ./.github/actions/ibex-rtl-ci-steps
117-
# with:
118-
# ibex_config: maxperf
119-
# - name: Run Ibex RTL CI for maxperf-pmp-bmbalanced configuration
120-
# uses: ./.github/actions/ibex-rtl-ci-steps
121-
# with:
122-
# ibex_config: maxperf-pmp-bmbalanced
123-
# - name: Run Ibex RTL CI for maxperf-pmp-bmfull configuration
124-
# uses: ./.github/actions/ibex-rtl-ci-steps
125-
# with:
126-
# ibex_config: maxperf-pmp-bmfull
127-
# - name: Run Ibex RTL CI for experimental-branch-predictor configuration
128-
# uses: ./.github/actions/ibex-rtl-ci-steps
129-
# with:
130-
# ibex_config: experimental-branch-predictor
131-
132-
# # Run lint on simple system
133-
# - name: Run Verilator lint on simple system
134-
# run: |
135-
# set +e
136-
# fusesoc --cores-root . run --target=lint --tool=verilator lowrisc:ibex:ibex_simple_system
137-
# if [ $? != 0 ]; then
138-
# echo -n "::error::"
139-
# echo "Verilog lint with Verilator failed. Run 'fusesoc --cores-root . run --target=lint --tool=verilator lowrisc:ibex:ibex_simple_system' to check and fix all errors."
140-
# exit 1
141-
# fi
142-
143-
# - name: Run Verible lint on simple system
144-
# run: |
145-
# set +e
146-
# fusesoc --cores-root . run --target=lint --tool=veriblelint lowrisc:ibex:ibex_simple_system
147-
# if [ $? != 0 ]; then
148-
# echo -n "::error::"
149-
# echo "Verilog lint with Verible failed. Run 'fusesoc --cores-root . run --target=lint --tool=veriblelint lowrisc:ibex:ibex_simple_system' to check and fix all errors."
150-
# exit 1
151-
# fi
152-
153-
fv:
154-
name: Run the Open-Source FV flow
155-
runs-on: nixos-25.05
26+
lint_dv:
27+
name: Run quality checks (Lint and DV)
28+
runs-on: ubuntu-22.04
15629
steps:
15730
- uses: actions/checkout@v4
31+
with:
32+
# Fetch all history so that we can run git diff on the base branch
33+
fetch-depth: 0
34+
35+
- name: Setup environment variables
36+
run: |
37+
# Filter out empty lines or comments
38+
grep -v '^\(#\|$\)' ci/vars.env >> $GITHUB_ENV
39+
40+
- name: Install build dependencies
41+
run: |
42+
ci/install-build-deps.sh
43+
44+
- name: Display environment
45+
run: |
46+
echo $PATH
47+
python3 --version
48+
echo -n "fusesoc "
49+
fusesoc --version
50+
verilator --version
51+
riscv32-unknown-elf-gcc --version
52+
verible-verilog-lint --version
53+
54+
# Verible format is experimental so only run on default config for now,
55+
# will eventually become part of the per-config CI
56+
- name: Format all source code with Verible format (experimental)
57+
run: |
58+
set +e
59+
fusesoc --cores-root . run --no-export --target=format --tool=veribleformat lowrisc:ibex:ibex_top_tracing
60+
if [ $? != 0 ]; then
61+
echo -n "::error::"
62+
echo "Verilog format with Verible failed. Run 'fusesoc --cores-root . run --no-export --target=format --tool=veribleformat lowrisc:ibex:ibex_top_tracing' to check and fix all errors."
63+
echo "This flow is currently experimental and failures can be ignored."
64+
fi
65+
# Show diff of what verilog_format would have changed, and then revert.
66+
git diff --no-pager
67+
git reset --hard HEAD
68+
continue-on-error: true
69+
70+
- name: Use clang-format to check C/C++ coding style
71+
# This check is not idempotent, but checks changes to a base branch.
72+
# Run it only on pull requests.
73+
if: github.event_name == 'pull_request'
74+
run: |
75+
set +e
76+
fork_origin=${{ github.event.pull_request.base.sha }}
77+
changed_files=$(git diff --name-only $fork_origin | grep -v '^vendor' | grep -E '\.(cpp|cc|c|h)$')
78+
test -z "$changed_files" || git diff -U0 $fork_origin $changed_files | clang-format-diff -p1 | tee clang-format-output
79+
if [ -s clang-format-output ]; then
80+
echo -n "::error::"
81+
echo "C/C++ lint failed. Use 'git clang-format' with appropriate options to reformat the changed code."
82+
exit 1
83+
fi
84+
85+
- name: Build and run CSR testbench with Verilator
86+
run: |
87+
# Build and run CSR testbench, chosen Ibex configuration does not effect
88+
# this so doesn't need to be part of per-config CI
89+
fusesoc --cores-root=. run --target=sim --tool=verilator lowrisc:ibex:tb_cs_registers
15890
159-
- name: Setup env
91+
- name: Get RISC-V Compliance test suite
16092
run: |
161-
echo "NIX_CONFIG=accept-flake-config = true" >> $GITHUB_ENV
93+
cd build
94+
git clone https://github.com/riscv/riscv-compliance.git
95+
cd riscv-compliance
96+
git checkout "$RISCV_COMPLIANCE_GIT_VERSION"
16297
163-
- name: Install Nix
164-
uses: cachix/install-nix-action@v27
98+
- name: Build tests for verilator co-simulation
99+
run: |
100+
# Build CoreMark without performance counter dump for co-simulation testing
101+
make -C ./examples/sw/benchmarks/coremark SUPPRESS_PCOUNT_DUMP=1
102+
make -C ./examples/sw/simple_system/pmp_smoke_test
103+
make -C ./examples/sw/simple_system/dit_test
104+
make -C ./examples/sw/simple_system/dummy_instr_test
105+
106+
# Run Ibex RTL CI per supported configuration
107+
- name: Run Ibex RTL CI for small configuration
108+
uses: ./.github/actions/ibex-rtl-ci-steps
109+
with:
110+
ibex_config: small
111+
- name: Run Ibex RTL CI for opentitan configuration
112+
uses: ./.github/actions/ibex-rtl-ci-steps
113+
with:
114+
ibex_config: opentitan
115+
- name: Run Ibex RTL CI for maxperf configuration
116+
uses: ./.github/actions/ibex-rtl-ci-steps
165117
with:
166-
extra_nix_config: |
167-
substituters = https://nix-cache.lowrisc.org/public/ https://cache.nixos.org/
168-
trusted-public-keys = nix-cache.lowrisc.org-public-1:O6JLD0yXzaJDPiQW1meVu32JIDViuaPtGDfjlOopU7o= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
118+
ibex_config: maxperf
119+
- name: Run Ibex RTL CI for maxperf-pmp-bmbalanced configuration
120+
uses: ./.github/actions/ibex-rtl-ci-steps
121+
with:
122+
ibex_config: maxperf-pmp-bmbalanced
123+
- name: Run Ibex RTL CI for maxperf-pmp-bmfull configuration
124+
uses: ./.github/actions/ibex-rtl-ci-steps
125+
with:
126+
ibex_config: maxperf-pmp-bmfull
127+
- name: Run Ibex RTL CI for experimental-branch-predictor configuration
128+
uses: ./.github/actions/ibex-rtl-ci-steps
129+
with:
130+
ibex_config: experimental-branch-predictor
169131

170-
- name: Run OSS Env
132+
# Run lint on simple system
133+
- name: Run Verilator lint on simple system
134+
run: |
135+
set +e
136+
fusesoc --cores-root . run --target=lint --tool=verilator lowrisc:ibex:ibex_simple_system
137+
if [ $? != 0 ]; then
138+
echo -n "::error::"
139+
echo "Verilog lint with Verilator failed. Run 'fusesoc --cores-root . run --target=lint --tool=verilator lowrisc:ibex:ibex_simple_system' to check and fix all errors."
140+
exit 1
141+
fi
142+
143+
- name: Run Verible lint on simple system
171144
run: |
172-
source <(nix print-dev-env .#oss-dev)
173-
cd dv/formal
174-
make build/aig-manip
175-
make build/all.aig SHELL=bash
176-
python3 conductor.py prove
145+
set +e
146+
fusesoc --cores-root . run --target=lint --tool=veriblelint lowrisc:ibex:ibex_simple_system
147+
if [ $? != 0 ]; then
148+
echo -n "::error::"
149+
echo "Verilog lint with Verible failed. Run 'fusesoc --cores-root . run --target=lint --tool=veriblelint lowrisc:ibex:ibex_simple_system' to check and fix all errors."
150+
exit 1
151+
fi

0 commit comments

Comments
 (0)