Skip to content

Commit ff5bcef

Browse files
committed
[ci] Have an OSS-Formal CI Pass
This commit introduces a new ci job which invokes the OS formal flow. It uses the nix flake, which contains all the necessary dependencies. With everything already in cache this takes less than an hour on pomona.
1 parent 25c064c commit ff5bcef

File tree

1 file changed

+57
-0
lines changed

1 file changed

+57
-0
lines changed

.github/workflows/ci-formal.yml

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
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+
- '.github/**'
18+
merge_group:
19+
types:
20+
- checks_requested
21+
pull_request:
22+
paths:
23+
- 'flake.nix'
24+
- 'flake.lock'
25+
- 'dv/formal/**'
26+
- 'rtl/**'
27+
- 'vendor/**'
28+
- '.github/**'
29+
30+
jobs:
31+
fv:
32+
name: Run the Open-Source FV flow
33+
runs-on: nixos
34+
steps:
35+
- uses: actions/checkout@v4
36+
37+
- name: Setup env
38+
run: |
39+
echo "NIX_CONFIG=accept-flake-config = true" >> $GITHUB_ENV
40+
41+
- name: Install Nix
42+
uses: cachix/install-nix-action@v27
43+
with:
44+
extra_nix_config: |
45+
substituters = https://nix-cache.lowrisc.org/public/ https://cache.nixos.org/
46+
trusted-public-keys = nix-cache.lowrisc.org-public-1:O6JLD0yXzaJDPiQW1meVu32JIDViuaPtGDfjlOopU7o= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
47+
48+
- name: Run OSS Env
49+
run: |
50+
source <(nix print-dev-env .#oss-dev)
51+
52+
cd dv/formal
53+
make build/aig-manip
54+
make build/all.aig SHELL=bash
55+
python3 conductor.py prove --check-complete
56+
# add --max-mem <gb> to restrict to some upper bound on memory usage. Hard minimum is 20 but 128 is a more realistic minimum
57+

0 commit comments

Comments
 (0)