[Update] Enable reusable PyUVM verification

.github/scripts/check-pyuvm-evidence.sh

@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Validate the portable PyUVM release-evidence contract after a successful run.
+report_dir="${1:-reports/pyuvm_open_source}"
+
+if [[ ! -s "${report_dir}/status.txt" ]]; then
+    echo "Missing PyUVM evidence: status.txt" >&2
+    exit 1
+fi
+
+status="$(<"${report_dir}/status.txt")"
+if [[ "${status}" == "SKIP" ]]; then
+    echo "PyUVM evidence check skipped by module flow policy"
+    exit 0
+fi
+if [[ "${status}" != "PASS" ]]; then
+    echo "PyUVM status is not PASS" >&2
+    exit 1
+fi
+
+required_files=(
+    compile.log
+    simulation.log
+    results.xml
+    functional-coverage.json
+    coverage.dat
+    coverage.info
+    versions.log
+)
+
+for required_file in "${required_files[@]}"; do
+    if [[ ! -s "${report_dir}/${required_file}" ]]; then
+        echo "Missing PyUVM evidence: ${required_file}" >&2
+        exit 1
+    fi
+done
+
+# Source-area checks prove that native coverage includes the shared HDL layers,
+# rather than recording only Python-driven activity in the DUT.
+if ! grep -Fq "/verif/assertions/" "${report_dir}/coverage.info"; then
+    echo "PyUVM native coverage does not include shared assertions" >&2
+    exit 1
+fi
+if ! grep -Fq "/verif/coverage/" "${report_dir}/coverage.info"; then
+    echo "PyUVM native coverage does not include HDL coverage models" >&2
+    exit 1
+fi
+
+python3 - "${report_dir}" <<'PY'
+import json
+import sys
+import xml.etree.ElementTree as ET
+from pathlib import Path
+
+report_dir = Path(sys.argv[1])
+root = ET.parse(report_dir / "results.xml").getroot()
+suites = [root] if root.tag == "testsuite" else list(root.iter("testsuite"))
+tests = sum(int(suite.get("tests", "0")) for suite in suites)
+failures = sum(int(suite.get("failures", "0")) for suite in suites)
+errors = sum(int(suite.get("errors", "0")) for suite in suites)
+if tests < 1 or failures or errors:
+    raise SystemExit(
+        f"PyUVM JUnit is not clean: tests={tests}, failures={failures}, errors={errors}"
+    )
+
+functional_coverage = json.loads(
+    (report_dir / "functional-coverage.json").read_text(encoding="utf-8")
+)
+if not functional_coverage:
+    raise SystemExit("PyUVM functional coverage is empty")
+PY
+
+echo "PyUVM evidence is complete"

.github/workflows/rtl-simulation.yml

@@ -67,7 +67,7 @@ jobs:
         uses: actions/cache@v5
         with:
           path: ~/.cache/mosaic
-          key: mosaic-tools-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('mosaic-flow/config/tool-versions.env') }}
+          key: mosaic-tools-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('mosaic-flow/config/tool-versions.env', 'mosaic-flow/config/pyuvm-requirements.txt') }}
 
       - name: Set up pinned open-source tools
         run: make setup-open-source
@@ -76,7 +76,7 @@ jobs:
         run: |
           # shellcheck disable=SC2016
           make --no-print-directory --silent \
-            --eval='mosaic-export-tool-paths: ; @printf "%s\n" "$(VERIBLE_ROOT)/bin" "$(SLANG_ROOT)/bin" "$(OSS_CAD_SUITE_ROOT)/bin"' \
+            --eval='mosaic-export-tool-paths: ; @printf "%s\n" "$(PYUVM_ROOT)/bin" "$(VERIBLE_ROOT)/bin" "$(SLANG_ROOT)/bin" "$(OSS_CAD_SUITE_ROOT)/bin"' \
             mosaic-export-tool-paths >> "${GITHUB_PATH}"
 
       - name: Record tool versions
@@ -90,13 +90,18 @@ jobs:
             eqy --version
             verible-verilog-lint --version
             slang --version
+            python --version
+            python -c 'import cocotb, pyuvm; print(f"cocotb {cocotb.__version__}"); print(f"pyuvm {pyuvm.__version__}")'
           } | tee reports/tool_versions/versions.log
 
       - name: Run portable open-source RTL flow
         run: |
           set -o pipefail
           make open-source 2>&1 | tee ci-artifacts/native-flow.log
 
+      - name: Validate native PyUVM evidence
+        run: ./.github/scripts/check-pyuvm-evidence.sh
+
       - name: Upload RTL reports
         if: always()
         uses: actions/upload-artifact@v7
@@ -186,6 +191,9 @@ jobs:
             "mosaic-module-ci:${GITHUB_SHA}" clean open-source \
             2>&1 | tee ci-artifacts/container-flow.log
 
+      - name: Validate container PyUVM evidence
+        run: ./.github/scripts/check-pyuvm-evidence.sh
+
       - name: Upload container RTL reports
         if: always()
         uses: actions/upload-artifact@v7

Dockerfile

@@ -10,8 +10,10 @@ RUN apt-get update \
         curl \
         g++ \
         git \
+        libpython3.12t64 \
         make \
         python3 \
+        python3-venv \
     && rm -rf /var/lib/apt/lists/*
 
 COPY --from=mosaic-flow /VERSION /opt/mosaic-flow/VERSION
@@ -24,7 +26,8 @@ RUN --mount=type=cache,id=oss-cad-suite,target=/opt/mosaic-tools/downloads \
     MOSAIC_TOOLS_ROOT=/opt/mosaic-tools /opt/mosaic-flow/ci/setup_open_source_tools.sh
 
 ENV FLOW_ROOT=/opt/mosaic-flow \
-    MOSAIC_TOOLS_ROOT=/opt/mosaic-tools
+    MOSAIC_TOOLS_ROOT=/opt/mosaic-tools \
+    PYTHONPYCACHEPREFIX=/tmp/mosaic-pycache
 
 ARG MOSAIC_FLOW_REVISION=unknown
 LABEL org.opencontainers.image.description="Open-source RTL verification environment for MOSAIC modules" \

README.md

@@ -21,9 +21,10 @@ make flow-config-check
 make clean open-source
 ```
 
-The first open-source target installs the pinned OSS CAD Suite, Verible, and
-Slang releases under `${XDG_CACHE_HOME:-$HOME/.cache}/mosaic`. Set
-`MOSAIC_TOOLS_ROOT` to use another cache location.
+The first open-source target installs the pinned OSS CAD Suite, Verible, Slang,
+PyUVM, and cocotb releases under
+`${XDG_CACHE_HOME:-$HOME/.cache}/mosaic`. Set `MOSAIC_TOOLS_ROOT` to use another
+cache location.
 
 ## Repository contract
 
@@ -42,7 +43,7 @@ The module must remain independently verifiable before system integration.
 
 ```text
 rtl/                  Synthesizable SystemVerilog
-verif/                Tests, assertions, formal harnesses, models, and coverage
+verif/                TB, PyUVM, properties, assertions, formal, and coverage
 filelists/            Ordered design and verification source lists
 config/               Module identity and flow policy
 flows/                Module-owned inputs grouped by shared flow name
@@ -74,8 +75,8 @@ is documented in [Project configuration](docs/project-configuration.md).
 Start from [Creating a module](docs/creating-a-module.md). At minimum:
 
 1. Rename the example RTL and verification hierarchy.
-2. Replace the example datapath and smoke verification.
-3. Update file lists and all module tops.
+2. Replace the example datapath, testbench, and PyUVM smoke verification.
+3. Update the RTL, property, assertion, coverage, simulation, and formal lists.
 4. Define timing, CDC, DFT, low-power, formal, and physical intent.
 5. Review flow states and dependencies.
 6. Replace template documentation with module-specific records.
@@ -117,6 +118,8 @@ evidence and every disabled flow is justified by project policy. Use the
 keep all accepted exceptions in [Reviewed waivers](docs/waivers.md).
 
 The open-source gate covers style, formatting, elaboration, lint, generic
-synthesis, formal verification, RTL-to-netlist equivalence, and simulation.
-Technology-mapped synthesis, timing, power, CDC, DFT, and low-power signoff use
-the configured local implementation environment.
+synthesis, formal proof and cover reachability, RTL-to-netlist equivalence,
+SystemVerilog simulation, PyUVM, and native HDL coverage. PyUVM functional
+coverage remains a separate report and must be reviewed alongside native
+coverage. Technology-mapped synthesis, timing, power, CDC, DFT, and low-power
+signoff use the configured local implementation environment.

config/design.mk

@@ -5,10 +5,25 @@ export DUT_INSTANCE := $(TB_TOP)/dut
 export FLOW_CONFIG_ROOT := $(MODULE_ROOT)/flows
 export RTL_FILELIST := $(MODULE_ROOT)/filelists/rtl.f
 export TB_FILELIST := $(MODULE_ROOT)/filelists/tb.f
+
+# Keep temporal declarations, checking, and coverage independently selectable
+# while preserving their required compilation order.
+export PROPERTY_FILELIST := $(MODULE_ROOT)/filelists/properties.f
+export ASSERTION_FILELIST := $(MODULE_ROOT)/filelists/assertions.f
+export COVERAGE_FILELIST := $(MODULE_ROOT)/filelists/coverage.f
+
+# PyUVM drives the synthesizable DUT directly. The shared adapter appends the
+# property, assertion, and coverage filelists above.
+export PYUVM_FILELIST := $(MODULE_ROOT)/filelists/rtl.f
+export PYUVM_TOP := $(DESIGN_TOP)
+export PYUVM_TEST_MODULE := test_mosaic_module
+export PYUVM_TEST_PATH := $(MODULE_ROOT)/verif/pyuvm
+export PYUVM_COVERAGE := enabled
 export VERILATOR_WAIVER_FILE := $(FLOW_CONFIG_ROOT)/verilator_lint/waivers.vlt
 export VERIBLE_WAIVER_FILE := $(FLOW_CONFIG_ROOT)/verible/waivers.txt
 export VERIBLE_RULES_FILE := $(FLOW_CONFIG_ROOT)/verible/rules
 export FORMAL_CONFIG := $(FLOW_CONFIG_ROOT)/symbiyosys/formal.sby
+export FORMAL_COVER_CONFIG := $(FLOW_CONFIG_ROOT)/symbiyosys/formal_cover.sby
 export EQUIVALENCE_CONFIG := $(FLOW_CONFIG_ROOT)/eqy/equivalence.eqy
 export OPENROAD_CONFIG := $(FLOW_CONFIG_ROOT)/openroad/config.mk
 export SYNTHESIS_CONSTRAINT_FILE := $(FLOW_CONFIG_ROOT)/synthesis/timing.sdc

config/flows.mk

@@ -7,9 +7,11 @@ FLOW_yosys_synthesis := enabled
 FLOW_symbiyosys_formal := enabled
 FLOW_eqy_equivalence := enabled
 FLOW_verilator_sim := enabled
+FLOW_pyuvm_open_source := enabled
 FLOW_openroad := disabled
 
 FLOW_vcs_sim := enabled
+FLOW_pyuvm_commercial := disabled
 FLOW_vc_lint := enabled
 FLOW_vc_cdc := enabled
 FLOW_sg_cdc := disabled

docs/README.md

@@ -41,8 +41,8 @@ keep module-specific decisions here.
    file lists, flow selection, dependencies, constraints, and site inputs.
 5. [Interface specification](interface.md) defines the hardware contract that
    consumers may rely on.
-6. [Verification plan](verification-plan.md) maps requirements to simulation,
-   assertions, formal properties, and coverage.
+6. [Verification plan](verification-plan.md) maps requirements to SystemVerilog
+   simulation, PyUVM, shared assertions, formal properties, and coverage.
 7. [Reviewed waivers](waivers.md) records every accepted tool exception.
 8. [Release checklist](release-checklist.md) defines the evidence required
    before publishing a module revision.
@@ -57,13 +57,18 @@ keep module-specific decisions here.
 | Enable or disable checks | `config/flows.mk` |
 | Add RTL sources | `filelists/rtl.f` |
 | Add simulation sources | `filelists/tb.f` |
-| Define formal proof | `flows/symbiyosys/formal.sby` |
+| Define shared properties | `filelists/properties.f` |
+| Define assertions | `filelists/assertions.f` |
+| Define HDL coverage | `filelists/coverage.f` |
+| Add PyUVM tests | `verif/pyuvm/` |
+| Define formal proof and covers | `flows/symbiyosys/` |
 | Define synthesis timing | `flows/synthesis/timing.sdc` |
 | Define CDC intent | `flows/cdc/constraints.tcl` |
 | Define DFT intent | `flows/sg_dft/constraints.tcl` |
 | Define power intent | `flows/vc_lp/power.upf` |
 | Validate project policy | `make flow-config-check` |
 | Run portable acceptance | `make clean open-source` |
+| Validate PyUVM evidence | `./.github/scripts/check-pyuvm-evidence.sh` |
 | Inspect results | `reports/<flow-id>/` |
 
 ## Documentation completion rule

docs/creating-a-module.md

@@ -31,12 +31,16 @@ At minimum, rename and update:
 
 - `rtl/mosaic_module.sv`
 - `verif/tb/mosaic_module_tb.sv`
+- `verif/pyuvm/test_mosaic_module.py`
+- Both files under `verif/properties/`
 - `verif/assertions/mosaic_module_sva.sv`
 - `verif/assertions/mosaic_module_bind.sv`
+- Both files under `verif/coverage/`
 - `verif/formal/mosaic_module_formal.sv`
-- All three files under `filelists/`
+- Every file under `filelists/`
 - `config/design.mk`
 - `flows/symbiyosys/formal.sby`
+- `flows/symbiyosys/formal_cover.sby`
 - `flows/eqy/equivalence.eqy`
 - `flows/openroad/config.mk`
 - `flows/vc_lp/power.upf`
@@ -80,17 +84,24 @@ simulator and linter accepts them. Do not add delays to synthesizable RTL.
 Update `filelists/rtl.f` in dependency order. Add packages before modules that
 import them and include directories before files that require them.
 
-Update `filelists/tb.f` with the unit testbench, assertions, and verification
-dependencies. Keep the simulation top consistent with `TB_TOP`.
+Update `filelists/properties.f`, `filelists/assertions.f`, and
+`filelists/coverage.f` without duplicating those sources in `filelists/tb.f`.
+The shared adapters append the reusable verification layers in that order.
 
-Update `filelists/formal.f` and the source list in
-`flows/symbiyosys/formal.sby`. Keep the formal top consistent with `FORMAL_TOP`.
+Update `filelists/tb.f` with RTL and the unit testbench. Keep the simulation top
+consistent with `TB_TOP`. Set `PYUVM_FILELIST` to the sources required by
+`PYUVM_TOP`, normally `filelists/rtl.f`.
+
+Update `filelists/formal.f` and both source lists under `flows/symbiyosys/`.
+Keep the proof and cover tops consistent with `FORMAL_TOP`.
 
 Run an early frontend check:
 
 ```sh
 make open-elaborate
 make open-lint
+make open-pyuvm
+make open-formal
 ```
 
 ## Replace the smoke verification
@@ -101,14 +112,22 @@ behavior. Replace it with tests and checking derived from the new interface.
 Update all of these together:
 
 - Unit-level stimulus and scoreboards
-- Bound assertions
-- Formal harness assumptions and assertions
-- Cover properties or functional coverage
+- PyUVM stimulus, checking, and functional coverage
+- Shared sequences and properties
+- Bound assertion and HDL coverage wrappers
+- Formal assumptions plus explicit reuse of the same wrappers
 - [Verification plan](verification-plan.md)
 
 Avoid assumptions that remove legal interface behavior from formal analysis.
 Use negative tests to prove the testbench and assertions detect injected faults.
 
+PyUVM does not call SVA from Python. Cocotb drives and observes the DUT while
+the selected HDL simulator compiles the property, assertion, and coverage
+filelists and evaluates their bound wrappers concurrently. Keep Python
+functional coverage separate from simulator-native assertion, line, branch,
+and toggle coverage. See
+[Project configuration](project-configuration.md#pyuvm-and-shared-verification).
+
 ### Parameterized modules
 
 The current portable flow synthesizes and compares one `DESIGN_TOP` using its
@@ -208,6 +227,7 @@ Prepare tools and run from a clean generated state:
 ```sh
 make setup-open-source
 make clean open-source
+./.github/scripts/check-pyuvm-evidence.sh
 ```
 
 Build and validate the container path:
@@ -225,6 +245,8 @@ docker run --rm \
   --env HOME=/tmp \
   --volume "$PWD:/workspace" \
   module-ci:local clean open-source
+
+./.github/scripts/check-pyuvm-evidence.sh
 ```
 
 In the licensed environment, qualify all enabled Synopsys adapters and run the