formal.yml

# Authors:
#   Unai Martinez-Corral
#     <umartinezcorral@antmicro.com>
#     <unai.martinezcorral@ehu.eus>
#   Torsten Meissner
#
# Copyright Unai Martinez-Corral
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#     http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
#
# SPDX-License-Identifier: Apache-2.0

name: 'formal'

on:
  pull_request:
  push:
  schedule:
    - cron: '0 0 * * 5'
  workflow_dispatch:
  repository_dispatch:
    types: [ formal ]

env:
  DOCKER_BUILDKIT: 1

jobs:
# TODO: Handle 'pull' in 'config.yml' (and command 'jobs').
# Then, use the reusable workflow 'common.py' here.

  matrix:
    runs-on: ubuntu-latest
    outputs:
      matrix: ${{ steps.generate.outputs.matrix }}
    steps:
    - name: 🧰 Checkout
      uses: actions/checkout@v4

    - name: 🛠️ Setup
      run: ./utils/setup.sh

    - name: 🔧 Generate matrix
      id: generate
      run: pyHDLC jobs formal


  jobs:
    needs: matrix
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        include: ${{ fromJson(needs.matrix.outputs.matrix) }}

    name: ${{ matrix.arch }}/${{ matrix.os }} | ${{ matrix.imgs }}
    steps:

    - name: 🧰 Checkout
      uses: actions/checkout@v4
      with:
        submodules: recursive

    - name: 🚧 Build, test and release
      uses: ./utils/build-test-release
      with:
        gcr_token: '${{ secrets.GCR_JSON_KEY }}'
        gh_token: '${{ github.token }}'
        docker_user: '${{ secrets.DOCKER_USER }}'
        docker_pass: '${{ secrets.DOCKER_PASS }}'
        skip-release: ${{ github.event_name == 'pull_request' }}
        architecture: ${{ matrix.arch }}
        collection: ${{ matrix.os }}
        images: ${{ matrix.imgs }}
        pull: >-
          ghdl/yosys
          pkg/z3
          pkg/sby
          pkg/yices2
          pkg/boolector
          pkg/cvc
          pkg/superprove
          pkg/pono