Add formal and timed verification for cc_cdc_2phase_clearable

.github/actions/free-space/action.yml

@@ -0,0 +1,45 @@
+# Copyright (c) 2025 ETH Zurich and University of Bologna.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Author:  Philippe Sauter <phsauter@iis.ee.ethz.ch>
+
+name: 'Free Disk Space on Runner'
+description: 'Frees disk space on GitHub-hosted runners to make room for eg large Docker images'
+
+runs:
+  using: 'composite'
+  steps:
+    - name: Show disk usage before cleanup
+      shell: bash
+      run: |
+        echo "Disk usage before cleanup:"
+        df -h
+
+    - name: Prune Docker data
+      shell: bash
+      run: |
+        # Remove stopped containers, unused networks, dangling images, and build cache
+        docker system prune -af || true
+
+    - name: Remove large preinstalled SDKs and toolchains
+      shell: bash
+      run: |
+        # These paths are known big space hogs on ubuntu-latest runners
+        sudo rm -rf /usr/local/lib/android || true
+        sudo rm -rf /usr/share/dotnet || true
+        sudo rm -rf /opt/ghc || true
+        sudo rm -rf /opt/hostedtoolcache/CodeQL || true
+        sudo rm -rf /opt/hostedtoolcache/go || true
+
+    - name: Clean APT caches
+      shell: bash
+      run: |
+        sudo apt-get clean || true
+        sudo rm -rf /var/lib/apt/lists/* || true
+
+    - name: Show disk usage after cleanup
+      shell: bash
+      run: |
+        echo "Disk usage after cleanup:"
+        df -h

.github/actions/oseda-cmd/action.yml

@@ -0,0 +1,65 @@
+# Copyright (c) 2025 ETH Zurich and University of Bologna.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Author:  Philippe Sauter <phsauter@iis.ee.ethz.ch>
+
+name: 'OSEDA Command Action'
+description: 'Sets up OSEDA environment and runs commands in a Docker container'
+
+inputs:
+  cmd:
+    description: 'Command to run in the OSEDA container'
+    required: true
+  service_name:
+    description: 'Name of the Docker service (default: from ./docker-compose.yml)'
+    required: false
+    default: ''
+
+runs:
+  using: 'composite'
+  steps:
+    - name: Set up Docker environment
+      shell: bash
+      run: |
+        echo "UID=$(id -u)" >> "$GITHUB_ENV"
+        echo "GID=$(id -g)" >> "$GITHUB_ENV"
+
+    - name: Get image name from docker-compose
+      id: get-image
+      shell: bash
+      run: |
+        IMAGE=$(docker compose config | awk '/image:/{print $2}' | head -n 1)
+        if [ -z "$IMAGE" ]; then
+          echo "[ERROR] No image found in docker-compose.yml"
+          exit 1
+        fi
+        echo "IMAGE_NAME=$IMAGE" >> "$GITHUB_ENV"
+
+    - name: Pull Docker image
+      shell: bash
+      run: |
+        if ! docker image inspect "$IMAGE_NAME" >/dev/null 2>&1; then
+          docker compose pull
+        fi
+
+    - name: Determine service name if not provided
+      shell: bash
+      run: |
+        if [ -z "${{ inputs.service_name }}" ]; then
+          SERVICE_NAME=$(docker compose config --services | head -n 1)
+          echo "service_name=$SERVICE_NAME" >> "$GITHUB_ENV"
+        else
+          echo "service_name=${{ inputs.service_name }}" >> "$GITHUB_ENV"
+        fi
+
+    - name: Run commands in OSEDA container
+      shell: bash
+      run: |
+        # Avoid extra pulls now that we've already pulled
+        if ! docker compose ps --status running --services | grep -qx "${{ env.service_name }}"; then
+          docker compose up -d --pull=never
+        fi
+        docker compose exec -T "${{ env.service_name }}" \
+          bash -lc "source ~/.bashrc; ${{ inputs.cmd }}" | tee result.log
+        echo "result_log=$(pwd)/result.log" >> "$GITHUB_ENV"

.github/scripts/run_verible_lint.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+# Copyright 2026 ETH Zurich and University of Bologna.
+#
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+set -euo pipefail
+
+command -v verible-verilog-lint
+
+find src -type f \( -name '*.sv' -o -name '*.svh' -o -name '*.v' \) -print0 \
+  | xargs -0 verible-verilog-lint \
+      --waiver_files lint/common_cells.style.waiver \
+      --rules=-interface-name-style \
+      --lint_fatal=false

.github/workflows/ci.yml

@@ -6,20 +6,35 @@ name: ci
 
 on:
   push:
+    branches:
+      - 'v*-dev'
+      - master
   pull_request:
   workflow_dispatch:
 
 jobs:
-  elaborate:
-    name: Elaborate all RTL modules w/ Verilator
+  verilator-elaboration:
+    name: Verilator Elaboration
     runs-on: ubuntu-latest
-    container:
-      image: hpretl/iic-osic-tools:2026.04
-      options: --user root
     steps:
-      - uses: actions/checkout@v6
-      - name: Run Verilator elaboration check
-        # Use a login shell to ensure that the environment is set up correctly
-        shell: bash -l -e -o pipefail {0}
-        run: |
-          make vlt-elab
+      - name: Checkout repository
+        uses: actions/checkout@v6
+      - name: Free disk space
+        uses: ./.github/actions/free-space
+      - name: Run Verilator elaboration
+        uses: ./.github/actions/oseda-cmd
+        with:
+          cmd: "make vlt-elab"
+
+  verible-lint:
+    name: Verible Lint
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v6
+      - name: Free disk space
+        uses: ./.github/actions/free-space
+      - name: Run Verible lint
+        uses: ./.github/actions/oseda-cmd
+        with:
+          cmd: ".github/scripts/run_verible_lint.sh"

.gitignore

@@ -9,6 +9,8 @@ build
 formal/fifo
 formal/counter
 formal/fall_through_register
+formal/cdc_reset_ctrlr_half
+formal/cdc_reset_ctrlr_composed
 *.check
 *.vcd
 obj_dir/

.gitlab-ci.yml

@@ -44,11 +44,16 @@ sg-lint:
     PARAM2: ""
   timeout: 10min
   script:
-    - bender checkout
-    - bender script vsim -t test > compile.tcl
-    - $VSIM -c -quiet -do 'source compile.tcl; quit'
-    - $VSIM -c $TOPLEVEL -voptargs="-timescale 1ns/100ps" -do "run -all" $PARAM1 $PARAM2
-    - (! grep -n "Error:" transcript)
+    - |
+      if [ "$TOPLEVEL" = "cc_cdc_2phase_clearable_tb" ]; then
+        ./test/simulate_cdc_clearable.sh
+      else
+        bender checkout
+        bender script vsim -t test > compile.tcl
+        $VSIM -c -quiet -do 'source compile.tcl; quit'
+        $VSIM -c $TOPLEVEL -voptargs="-timescale 1ns/100ps" -do "run -all" $PARAM1 $PARAM2
+        (! grep -n "Error:" transcript)
+      fi
 
 tests:
   extends: .test-tpl
@@ -57,6 +62,7 @@ tests:
       - TOPLEVEL:
           - cc_addr_decode_tb
           - cc_cb_filter_tb
+          - cc_cdc_2phase_clearable_tb
           # - cc_cdc_fifo_clearable_tb
           - cc_clk_int_div_tb
           - cc_clk_int_div_static_tb
@@ -82,3 +88,7 @@ tests:
       #   PARAM1: [-GDEPTH=1, -GDEPTH=2, -GDEPTH=3, -GDEPTH=4, -GDEPTH=5]
       #   PARAM2: [-GGRAY=0, -GGRAY=1]
 
+formal:
+  timeout: 30min
+  script:
+    - make -B -C formal cdc_reset_ctrlr_half.check cdc_reset_ctrlr_composed.check

docker-compose.yml

@@ -0,0 +1,21 @@
+# Copyright (c) 2026 ETH Zurich and University of Bologna.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+#
+# Authors:
+# - Philippe Sauter <phsauter@iis.ee.ethz.ch>
+
+services:
+  pulp-docker:
+    image: hpretl/iic-osic-tools:2026.04
+    environment:
+      - UID=${UID}
+      - GID=${GID}
+    user: "${UID}:${GID}"
+    volumes:
+      - ./:/fosic/designs/common_cells
+    stdin_open: true
+    tty: true
+    working_dir: /fosic/designs/common_cells
+    entrypoint: /dockerstartup/scripts/ui_startup.sh
+    command: --skip bash

formal/Makefile

@@ -1,21 +1,28 @@
-# Copyright (c) 2019 ETH Zurich, University of Bologna
+# Copyright 2019 ETH Zurich and University of Bologna.
 #
 # Copyright and related rights are licensed under the Solderpad Hardware
 # License, Version 0.51 (the "License"); you may not use this file except in
-# compliance with the License.  You may obtain a copy of the License at
+# compliance with the License. You may obtain a copy of the License at
 # http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law
 # or agreed to in writing, software, hardware and materials distributed under
 # this 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.
 
-# Author: Robert Balas <balasr@iis.ee.ethz.ch>
+# Authors:
+# - Robert Balas <balasr@iis.ee.ethz.ch>
+# - Philippe Sauter <phsauter@iis.ee.ethz.ch>
+#
+# Description: Formal Verification Targets
+# Dispatch SymbiYosys proof runs for common_cells formal properties, including
+# reset-controller half and composed CDC clear-sequencing checks.
 
 YOSYS	?= yosys
-SBY	?= sby
+SBY	?= oseda sby
 RM	?= rm
 
-all: fifo.check counter.check fall_through_register.check
+all: fifo.check counter.check fall_through_register.check cdc_reset_ctrlr_half.check \
+	cdc_reset_ctrlr_composed.check
 
 fifo.check: fifo.sby ../src/cc_fifo.sv cc_fifo_properties.sv
 	$(SBY) -f $<
@@ -34,9 +41,24 @@ fall_through_register.check: fall_through_register.sby ../src/cc_fall_through_re
 	$(SBY) -f $<
 	touch $@
 
+cdc_reset_ctrlr_half.check: cdc_reset_ctrlr_half.sby cc_cdc_reset_ctrlr_half_properties.sv \
+				../src/cc_cdc_reset_ctrlr.sv ../src/cc_cdc_4phase.sv \
+				../src/cc_sync.sv ../src/cc_pkg.sv
+	SBY="$(SBY)" ./run_cdc_reset_ctrlr_half.sh
+	touch $@
+
+cdc_reset_ctrlr_composed.check: cdc_reset_ctrlr_composed.sby cc_cdc_reset_ctrlr_properties.sv \
+				cc_cdc_reset_ctrlr_half_properties.sv \
+				../src/cc_cdc_reset_ctrlr.sv ../src/cc_cdc_4phase.sv \
+				../src/cc_sync.sv ../src/cc_pkg.sv
+	SBY="$(SBY)" ./run_cdc_reset_ctrlr_composed.sh
+	touch $@
+
 .PHONY: clean
 clean:
 	$(RM) -r fifo.check fifo/
 #	$(RM) -r delta_counter.check delta_counter/
 	$(RM) -r counter.check counter/
 	$(RM) -r fall_through_register.check fall_through_register/
+	$(RM) -r cdc_reset_ctrlr_half.check cdc_reset_ctrlr_half/
+	$(RM) -r cdc_reset_ctrlr_composed.check cdc_reset_ctrlr_composed/