Repository navigation
[Feature] Consume mosaic-flow release "MF20260908V1" and enable PyUVM #1
Copy link
Copy link
Closed
Labels
enhancementNew feature or requestNew feature or request
Description
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-flowgitlink to theMF20260908V1release 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, andCOVERAGE_FILELISTtoconfig/design.mk. - Add
FORMAL_COVER_CONFIG. - Configure
PYUVM_FILELIST,PYUVM_TOP,PYUVM_TEST_MODULE, andPYUVM_TEST_PATH. - Enable
PYUVM_COVERAGE. - Enable
FLOW_pyuvm_open_source. - Keep
FLOW_pyuvm_commercialdisabled 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 propertydirectives underverif/assertions/. - Keep
cover propertydirectives underverif/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
bindstatements withMOSAIC_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.txtin the tool-cache key. - Export
$(PYUVM_ROOT)/binwhen 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-checkpasses. -
make clean open-sourcepasses locally. - Native GitHub Actions pass.
- Containerized GitHub Actions pass.
-
reports/pyuvm_open_source/status.txtcontainsPASS. - PyUVM produces valid JUnit XML with at least one test and no failures.
- Verilator produces
coverage.datandcoverage.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-flowsubmodule 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-flowrelease
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request
Activity
[-][Update] Consume mosaic-flow release "MF20260908V1" and enable PyUVM[/-][+][Feature] Consume mosaic-flow release "MF20260908V1" and enable PyUVM[/+]ErickOF commentedon Sep 9, 2026
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.