CI: the four jobs of the TopLevel, mirrored in the parent repository

.github/workflows/ci.yml

@@ -0,0 +1,120 @@
+name: ci
+
+# One run per commit: a pull request (a new commit cancels the run of the previous one) or a push to
+# main. The four jobs have fixed names, which a ruleset of the organization can require as checks.
+on:
+  pull_request:
+  push:
+    branches: [main]
+
+concurrency:
+  group: ci-${{ github.event.pull_request.number || github.sha }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+permissions:
+  contents: read
+
+jobs:
+  vhdl-syntax:
+    name: vhdl-syntax
+    runs-on: ubuntu-26.04
+    timeout-minutes: 15
+    # GHDL, Yosys, SymbiYosys, z3, uv and riscv-tools of insper-riscv/Infra.
+    container:
+      image: ghcr.io/insper-riscv/ci-vhdl:latest
+
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          submodules: recursive
+
+      - name: Every referenced path exists, in this repository and in each submodule
+        run: make paths
+
+      - name: VHDL syntax check of every repository (GHDL, dependency order)
+        run: make check
+
+  unit-tests:
+    name: unit-tests
+    runs-on: ubuntu-26.04
+    timeout-minutes: 60
+    container:
+      image: ghcr.io/insper-riscv/ci-vhdl:latest
+
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          submodules: recursive
+
+      - name: Per-entity cocotb tests of each repository and the memory map check
+        run: make unit-tests
+
+      - name: Test programs of the Tests repository, in simulation
+        run: make sim
+
+      - name: Upload waveforms
+        if: failure()
+        uses: actions/upload-artifact@v7
+        with:
+          name: waveforms
+          path: "**/*.ghw"
+          if-no-files-found: ignore
+
+  formal:
+    name: formal
+    runs-on: ubuntu-26.04
+    timeout-minutes: 45
+    container:
+      image: ghcr.io/insper-riscv/ci-vhdl:latest
+
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          submodules: recursive
+
+      - name: Prove every make target named formal* of each repository
+        # A repository without proofs passes with a message; the proofs join by adding a formal target to it.
+        run: make formal
+
+      - name: Upload the logs
+        if: failure()
+        uses: actions/upload-artifact@v7
+        with:
+          name: formal-logs
+          path: |
+            */build/formal/**/*.log
+          if-no-files-found: ignore
+
+  python-static-analysis:
+    name: python-static-analysis
+    runs-on: ubuntu-26.04
+    timeout-minutes: 15
+    # The tools come pinned in the image, with the settings of [tool.ruff] and [tool.complexipy] of pyproject.toml.
+    container:
+      image: ghcr.io/insper-riscv/ci-vhdl:latest
+
+    steps:
+      - uses: actions/checkout@v7
+
+      - name: ruff lint
+        run: ruff check .
+
+      - name: ruff format
+        if: ${{ !cancelled() }}
+        run: ruff format . --check
+
+      - name: pycodestyle
+        if: ${{ !cancelled() }}
+        run: pycodestyle --max-line-length=79 --max-doc-length=72 --ignore=E203,W503 --exclude=Common-Components,build,.venv,sim_build,__pycache__ .
+
+      - name: pydocstyle
+        if: ${{ !cancelled() }}
+        run: pydocstyle --convention=pep257 --match-dir='^(?!(Common-Components|build|\.venv|sim_build|__pycache__)).*' .
+
+      - name: complexipy
+        if: ${{ !cancelled() }}
+        run: complexipy .
+
+      - name: semgrep
+        if: ${{ !cancelled() }}
+        run: semgrep scan --config p/python --error .

Makefile

@@ -1,67 +1,54 @@
 # The parent repository: it pins Core, Memory, Peripherals, TopLevel and Tests, and
 # this Makefile runs them together. Each of them has its own Makefile and uv project;
-# `git submodule update --init --recursive` first.
+# `git submodule update --init --recursive` first. The repositories sit side by side
+# here, which is how their own Makefiles and configurations name each other (../Core).
+# The riscv-tools command comes from the toolchain image of insper-riscv/Infra.
 SHELL := /bin/bash
 
 SUBREPOS := Core Memory Peripherals TopLevel
-GHDL     := ghdl
-STD      := --std=08
-WDIR     := build/ghdl
+# The Python of the image where riscv_tools is installed (the host tests of Tests import it).
+PYTOOLS  ?= /opt/riscv-tools/riscv-tools/bin/python
 
-.PHONY: all sync check subrepos sim paths clean
+.PHONY: all sync paths check unit-tests formal sim clean
 
-all: paths check subrepos sim
+all: paths check unit-tests formal sim
 
 sync:
 	@set -e; for s in $(SUBREPOS) Tests; do (cd $$s && uv sync -q); done
 
-# ---------------------------------------------------------------
-# VHDL syntax check (GHDL), every source of the tree in ONE library: it also catches
-# two repositories defining the same entity (as a stale ROM_simulation once did).
-# Run with:  make check
-# ---------------------------------------------------------------
-# 1) All .vhd/.vhdl of the repositories that hold VHDL. The Quartus IPs (Memory/ips)
-#    and the PLL need Intel libraries and are left out.
-CHECK_SRCS := $(shell find TopLevel/platforms/internal-mem/rtl Memory/sim Peripherals/common Peripherals/GPIO Peripherals/TIMER Peripherals/UART Core/common Core/I Core/M Core/cores -type f \( -name '*.vhd' -o -name '*.vhdl' \) | sort)
-
-# 2) Dependency order (topological sort, riscv-tools vhdl-sort)
-ORDERED_SRCS := $(shell uv run --project Tests riscv-tools vhdl-sort $(CHECK_SRCS))
-
-.PHONY: print-check
-print-check:
-	@echo "Files the check analyzes:"; echo
-	@printf '  %s\n' $(ORDERED_SRCS)
+# Every file path that the configuration of each repository lists exists (the paths.yaml of each one).
+paths:
+	@set -e; for s in $(SUBREPOS); do $(MAKE) -C $$s paths; done
 
+# VHDL syntax check (GHDL) of every repository, in dependency order. The TopLevel analyzes the sources of
+# Common-Components, Core, Memory and Peripherals together in one library, so it also catches two
+# repositories defining the same entity; the Core also elaborates each of its profiles.
 check:
-	@echo "Checking VHDL syntax with GHDL..."
-	@mkdir -p $(WDIR)
-	@rm -rf $(WDIR)/*
-	@$(GHDL) -a $(STD) --work=work --workdir=$(WDIR) $(ORDERED_SRCS)
-	@echo "VHDL syntax check passed"
+	$(MAKE) -C Core profiles
+	$(MAKE) -C Memory check
+	$(MAKE) -C Peripherals check
+	$(MAKE) -C TopLevel check
+
+# The per-entity cocotb tests of each repository, and the memory map check of the TopLevel.
+unit-tests: sync
+	$(MAKE) -C Core test
+	$(MAKE) -C Memory test
+	$(MAKE) -C Peripherals test
+	$(MAKE) -C TopLevel memory-map test
+
+# Every make target named formal* of each repository (SymbiYosys and z3); a repository without proofs is skipped.
+formal:
+	@set -e; for s in $(SUBREPOS); do \
+	  for t in $$(sed -n 's/^\(formal[a-z-]*\):.*/\1/p' $$s/Makefile); do $(MAKE) -C $$s $$t; done; \
+	done
 
-# ---------------------------------------------------------------
-# Each repository's own checks and tests, at the pinned versions. They find each
-# other as siblings (../Core, ../Memory, ...), which is how the submodules sit.
-# ---------------------------------------------------------------
-subrepos: sync
-	$(MAKE) -C Core paths check profiles test
-	$(MAKE) -C Memory paths check test
-	$(MAKE) -C Peripherals paths check test
-	$(MAKE) -C TopLevel all
-
-# ---------------------------------------------------------------
 # The Tests project's generic simulation suite, including uart-tx, uart-echo
 # and uart-errors through the generic top's serial pins.
-# ---------------------------------------------------------------
 sim: sync
-	cd Tests && uv run python -m unittest discover -s tests/host -v \
-	  && uv run riscv-tools --config tools/riscv_build/config.yaml generate-header \
-	  && uv run riscv-tools --config tools/riscv_build/config.yaml compile --emit hex \
-	  && uv run riscv-tools --config tools/riscv_build/config.yaml sim
-
-# Every file path the configuration lists exists (paths.yaml).
-paths: sync
-	cd Tests && uv run riscv-tools --root .. check-paths --manifest paths.yaml
+	cd Tests && $(PYTOOLS) -m unittest discover -s tests/host -v \
+	  && riscv-tools --config tools/riscv_build/config.yaml generate-header \
+	  && riscv-tools --config tools/riscv_build/config.yaml compile --emit hex \
+	  && riscv-tools --config tools/riscv_build/config.yaml sim
 
 clean:
 	rm -rf build