[Feature] Consume mosaic-flow release "MF20260908V1" and enable PyUVM

[ErickOF]

Summary

Update mosaic-module-template to consume the mosaic-flow release MF20260908V1 and adopt its PyUVM verification contract.

The template must demonstrate how normal SystemVerilog simulation, PyUVM, and formal verification reuse the same properties, assertions, and coverage models.

Dependency

This issue depends on publishing a qualified mosaic-flow release containing:

• PyUVM and cocotb support
• Open-source Verilator and Icarus adapters
• Commercial VCS and Xcelium adapters
• Shared property, assertion, and coverage filelists
• Formal cover reachability
• Simulator-native coverage collection

Required Changes

mosaic-flow revision

• Update the mosaic-flow gitlink to the MF20260908V1 release revision.
• Record the selected release or commit in the pull request.
• Verify that CI checks out exactly the revision recorded by the gitlink.

Module configuration

• Add PROPERTY_FILELIST, ASSERTION_FILELIST, and COVERAGE_FILELIST to config/design.mk.
• Add FORMAL_COVER_CONFIG.
• Configure PYUVM_FILELIST, PYUVM_TOP, PYUVM_TEST_MODULE, and PYUVM_TEST_PATH.
• Enable PYUVM_COVERAGE.
• Enable FLOW_pyuvm_open_source.
• Keep FLOW_pyuvm_commercial disabled by default.

Verification structure

• Add filelists/properties.f.
• Add filelists/assertions.f.
• Add filelists/coverage.f.
• Remove assertion and coverage sources from filelists/tb.f.
• Add reusable module-specific sequences under verif/properties/.
• Add reusable properties composed from those sequences.
• Keep assert property directives under verif/assertions/.
• Keep cover property directives under verif/coverage/.
• Add assertion and coverage bind wrappers.
• Add a representative PyUVM test under verif/pyuvm/.
• Keep Python functional coverage separate from simulator-native coverage.

Formal verification

• Reuse the assertion and coverage wrappers from simulation.
• Suppress simulation-oriented bind statements with MOSAIC_FORMAL.
• Instantiate the shared wrappers explicitly from the formal harness.
• Add a Yosys-compatible procedural fallback using MOSAIC_YOSYS_FORMAL.
• Add a separate SymbiYosys cover configuration.
• Ensure all representative cover statements are reachable.

GitHub Actions

• Include mosaic-flow/config/pyuvm-requirements.txt in the tool-cache key.
• Export $(PYUVM_ROOT)/bin when exposing pinned tool paths.
• Record Python, PyUVM, cocotb, and simulator versions.
• Run PyUVM as part of make open-source.
• Upload PyUVM logs, JUnit results, functional coverage, and native coverage.
• Keep commercial simulators outside GitHub-hosted CI.

Documentation

• Explain that PyUVM drives the DUT through cocotb and does not call SVA from Python.
• Document compilation and binding of properties, assertions, and coverage.
• Update the repository structure documentation.
• Update the project configuration reference.
• Update the module creation guide.
• Update the verification plan template.
• Update the release checklist with PyUVM and coverage evidence.
• Update multi-module CI examples and cache keys.

Acceptance Criteria

• make flow-config-check passes.
• make clean open-source passes locally.
• Native GitHub Actions pass.
• Containerized GitHub Actions pass.
• reports/pyuvm_open_source/status.txt contains PASS.
• PyUVM produces valid JUnit XML with at least one test and no failures.
• Verilator produces coverage.dat and coverage.info.
• Python functional coverage is written separately.
• Bound assertion and coverage sources appear in simulator evidence.
• Formal proof and cover reachability both pass.
• Normal simulation, PyUVM, and formal do not maintain duplicated SVA implementations.
• The mosaic-flow submodule remains clean after all validation.

Out of Scope

• Running VCS or Xcelium in public GitHub-hosted CI
• Commercial coverage sign-off
• Module-specific verification beyond the representative template fixture
• Publishing the upstream mosaic-flow release

[ErickOF]

Completed by PR #2 at commit 19730b3. The native and containerized open-source jobs both passed in workflow run https://github.com/ECASLab/mosaic-module-template/actions/runs/34297270904, including formal proof, cover reachability, PyUVM execution, and evidence validation.