diff --git a/.github/scripts/check-pyuvm-evidence.sh b/.github/scripts/check-pyuvm-evidence.sh new file mode 100755 index 0000000..e09b4bb --- /dev/null +++ b/.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" diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index 8775826..e9f2eb0 100644 --- a/.github/workflows/rtl-simulation.yml +++ b/.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,6 +90,8 @@ 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 @@ -97,6 +99,9 @@ jobs: 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 diff --git a/Dockerfile b/Dockerfile index 629906a..70c5e63 100644 --- a/Dockerfile +++ b/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" \ diff --git a/README.md b/README.md index e29c67b..355d881 100644 --- a/README.md +++ b/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. diff --git a/config/design.mk b/config/design.mk index 194f94e..de3b059 100755 --- a/config/design.mk +++ b/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 diff --git a/config/flows.mk b/config/flows.mk index 3f24c86..77b15a7 100644 --- a/config/flows.mk +++ b/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 diff --git a/docs/README.md b/docs/README.md index 5835f84..e70a96f 100644 --- a/docs/README.md +++ b/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//` | ## Documentation completion rule diff --git a/docs/creating-a-module.md b/docs/creating-a-module.md index 8d7e9d9..d7fc563 100644 --- a/docs/creating-a-module.md +++ b/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 diff --git a/docs/multi-module-repositories.md b/docs/multi-module-repositories.md index 660c72a..67d72ec 100644 --- a/docs/multi-module-repositories.md +++ b/docs/multi-module-repositories.md @@ -232,7 +232,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: Validate module policy run: | @@ -246,6 +246,11 @@ jobs: FLOW_ROOT="${GITHUB_WORKSPACE}/mosaic-flow" \ clean open-source + - name: Validate module PyUVM evidence + run: | + ./.github/scripts/check-pyuvm-evidence.sh \ + "${{ matrix.path }}/reports/pyuvm_open_source" + - name: Upload module reports if: always() uses: actions/upload-artifact@v7 @@ -270,6 +275,8 @@ workflow for every manifest entry: - Native tool setup uses the pinned `mosaic-flow` revision. - Tool versions are recorded below the module's `reports/tool_versions/` tree. - Native flow logs are written below the module's `ci-artifacts/` tree. +- Enabled PyUVM flows retain clean JUnit, native HDL coverage, functional + coverage, and version evidence below the module's report tree. - The container image embeds the same pinned methodology revision. - The container runs with `--workdir /workspace/${{ matrix.path }}`. - Native and container report artifacts include the module name. @@ -305,6 +312,8 @@ current module root. Consequently, each matrix child independently performs: - SymbiYosys formal verification - EQY RTL-to-netlist equivalence - Verilator simulation +- PyUVM with the configured open-source simulator +- Native HDL coverage and PyUVM functional coverage evidence - The aggregate open-source quality gate The module's `config/flows.mk` decides which checks are enabled. Dependencies @@ -314,30 +323,34 @@ matrix child. ## Regression configuration -The current simulator contract executes one `TB_TOP` per module. Configure that -top as a self-checking unit regression rather than as a single manual test. +The normal simulator contract executes one `TB_TOP` per module, while PyUVM +executes the decorated tests in `PYUVM_TEST_MODULE` against `PYUVM_TOP`. +Configure both paths as self-checking unit regressions. For each module: 1. Set `TB_TOP` in `config/design.mk` to the regression top. -2. List the DUT, assertions, testbench components, and tests in - `filelists/tb.f`. -3. Make the regression top execute every required scenario. -4. Make every mismatch, assertion failure, timeout, or incomplete test return a +2. Set `PYUVM_TOP`, `PYUVM_TEST_MODULE`, and `PYUVM_TEST_PATH` for the Python + environment. +3. Keep DUT and testbench sources in their primary lists, then keep shared + properties, assertions, and coverage in their dedicated filelists. +4. Make both regression environments execute every required scenario. +5. Make every mismatch, assertion failure, timeout, or incomplete test return a nonzero simulation status. -5. Record the test inventory and expected coverage in +6. Record the test inventory and expected native plus functional coverage in `docs/verification-plan.md`. -6. Keep test-generated files under the module's `work/` directory. +7. Keep test-generated files under the module's `work/` and `reports/` + directories. The regression must not rely on another module's job output. If the DUT imports a shared package or instantiates another source module, include that dependency in the module's file lists so a clean job can compile it independently. -The current shared simulator adapters do not schedule a list of independent -test executables. A future per-test process matrix requires an explicit -`mosaic-flow` extension with a test-list contract, result aggregation, and one -final status. Until that extension exists, keep the supported one-regression-top -model. +The normal simulator adapter does not schedule a list of independent test +executables. PyUVM may discover several decorated tests in one Python module, +but still aggregates them into one flow status. A future process-level test +matrix requires an explicit `mosaic-flow` extension with a test-list contract, +result aggregation, and one final status. ## Container execution diff --git a/docs/project-configuration.md b/docs/project-configuration.md index d56d740..195672d 100644 --- a/docs/project-configuration.md +++ b/docs/project-configuration.md @@ -23,6 +23,8 @@ These values must agree with the RTL and verification hierarchy: | `DESIGN_TOP` | Synthesizable top | `mosaic_module` | | `TB_TOP` | Simulation top | `mosaic_module_tb` | | `FORMAL_TOP` | Formal harness top | `mosaic_module_formal` | +| `PYUVM_TOP` | HDL top exposed to cocotb | `mosaic_module` | +| `PYUVM_TEST_MODULE` | Importable Python test module | `test_mosaic_module` | | `DUT_INSTANCE` | Hierarchical DUT for SAIF annotation | `mosaic_module_tb/dut` | `DUT_INSTANCE` uses the hierarchy syntax expected by PrimePower activity @@ -34,9 +36,10 @@ the simulation source name is sufficient. `FLOW_CONFIG_ROOT` points to the module-owned `flows/` directory. Other exported paths identify: -- RTL and simulation file lists +- RTL, simulation, property, assertion, and coverage file lists +- PyUVM test path, Python module, HDL top, and DUT file list - Verible and Verilator waiver policy -- Formal and equivalence configuration +- Formal proof, formal cover, and equivalence configuration - OpenROAD design configuration - Synthesis, CDC, DFT, and UPF intent - Report and work roots @@ -54,6 +57,7 @@ Every canonical flow has an explicit module policy: ```make FLOW_verilator_sim := enabled +FLOW_pyuvm_open_source := enabled FLOW_openroad := disabled ``` @@ -61,8 +65,10 @@ Only `enabled` and `disabled` are valid. Disabled flows record `SKIP` when their target is invoked. The quality gate requires `PASS` for enabled flows and `SKIP` for disabled flows. -The template enables the portable RTL gate, disables optional OpenROAD, selects -VC CDC, and leaves commercial flows enabled for local qualification. +The template enables normal Verilator simulation and open-source PyUVM in the +portable RTL gate. It disables optional OpenROAD, selects VC CDC, keeps +commercial PyUVM disabled, and leaves the other commercial flows enabled for +local qualification. Run: @@ -72,6 +78,63 @@ make flow-config-check Review the output after every state or dependency change. +## PyUVM and shared verification + +PyUVM does not import or invoke SystemVerilog assertions. The Python test drives +and observes `PYUVM_TOP` through cocotb. During model construction, the shared +adapter compiles the following HDL layers in order: + +1. `PYUVM_FILELIST` for the DUT and required packages +2. `PROPERTY_FILELIST` for shared sequence and property definitions +3. `ASSERTION_FILELIST` for assertion checkers and bind wrappers +4. `COVERAGE_FILELIST` for HDL coverage models and bind wrappers + +The simulator therefore evaluates SVA and HDL coverage concurrently with the +Python-driven test. A terminating SVA failure also fails the PyUVM flow. Normal +SystemVerilog simulation uses the same property, assertion, and coverage lists. +The SymbiYosys proof and cover configurations explicitly instantiate the same +wrappers because open-source formal frontends do not reliably apply +simulation-oriented `bind` statements. + +The main module-owned settings are: + +| Variable | Purpose | +| --- | --- | +| `PROPERTY_FILELIST` | Shared sequences and temporal property definitions | +| `ASSERTION_FILELIST` | Assertion checker and bind wrapper sources | +| `COVERAGE_FILELIST` | HDL coverage model and bind wrapper sources | +| `PYUVM_FILELIST` | DUT sources compiled for the PyUVM HDL top | +| `PYUVM_TOP` | HDL top visible to cocotb | +| `PYUVM_TEST_MODULE` | Importable Python module containing decorated PyUVM tests | +| `PYUVM_TEST_PATH` | Directory prepended to the Python import path | +| `PYUVM_COVERAGE` | Enables simulator-native coverage when set to `enabled` | +| `FORMAL_COVER_CONFIG` | SymbiYosys cover reachability configuration | + +Run the portable PyUVM flow directly with: + +```sh +make open-pyuvm +``` + +The commercial policy is disabled in the template. In an authorized licensed +environment, enable `FLOW_pyuvm_commercial` and select the qualified backend: + +```sh +make PYUVM_COMMERCIAL_SIMULATOR=vcs commercial-pyuvm +make PYUVM_COMMERCIAL_SIMULATOR=xcelium commercial-pyuvm +``` + +Both commercial backends consume the same Python test and shared SystemVerilog +verification layers. Simulator-specific compatibility and coverage options +must be qualified before they become release evidence. + +`reports/pyuvm_open_source/coverage.dat` and `coverage.info` are native HDL +coverage evidence. `functional-coverage.json` is produced by the Python test +and remains a separate verification artifact. Neither form replaces the other. +The complete adapter contract and optional simulator settings are documented in +the shared +[configuration reference](../mosaic-flow/docs/configuration.md#design-and-path-variables). + ## Dependencies Dependencies use canonical flow IDs and replace the complete shared dependency diff --git a/docs/release-checklist.md b/docs/release-checklist.md index 68e9f5d..ed9399c 100644 --- a/docs/release-checklist.md +++ b/docs/release-checklist.md @@ -34,11 +34,18 @@ gate alone is not sufficient ASIC release evidence. test, assertion, formal property, or reviewed combination. - [ ] All supported parameter configurations have evidence. - [ ] Positive, negative, reset, error, and boundary tests pass. -- [ ] Assertions run in simulation and reach meaningful antecedents. +- [ ] Enabled SystemVerilog and PyUVM regressions pass. +- [ ] Normal simulation, PyUVM, and formal consume the reviewed shared property, + assertion, and coverage sources without duplicated checking logic. +- [ ] Assertions run in simulation and PyUVM and reach meaningful antecedents. - [ ] Formal assumptions are reviewed for overconstraint. - [ ] Formal proofs pass at justified depth or by complete proof. +- [ ] Formal cover mode demonstrates required scenario reachability. - [ ] RTL-to-Yosys-netlist equivalence passes. +- [ ] Native HDL and Python functional coverage are reviewed independently. - [ ] Functional and code coverage goals are met or deviations are approved. +- [ ] VCS or Xcelium PyUVM evidence passes when commercial PyUVM belongs to the + module's release scope. ## Constraints and static checks @@ -83,6 +90,8 @@ gate alone is not sufficient ASIC release evidence. ## Reproducibility and evidence - [ ] Native `make clean open-source` passes. +- [ ] PyUVM status, JUnit, native coverage, functional coverage, and version + evidence pass `./.github/scripts/check-pyuvm-evidence.sh` when enabled. - [ ] The pinned Docker image builds and its portable gate passes. - [ ] GitHub Actions passes using the recorded gitlink revision. - [ ] Commercial gates pass in the authorized local or self-hosted environment. diff --git a/docs/repository-structure.md b/docs/repository-structure.md index f984ca8..f8fa7fd 100644 --- a/docs/repository-structure.md +++ b/docs/repository-structure.md @@ -8,7 +8,9 @@ intent from the independently versioned shared methodology. ```text module-repository/ -|-- .github/workflows/ Portable module CI +|-- .github/ Portable module CI and evidence checks +| |-- scripts/ CI-owned release-evidence validators +| `-- workflows/ Native and containerized quality gates |-- config/ Cross-flow module configuration |-- docs/ Design contract and engineering records |-- filelists/ Ordered source manifests @@ -16,7 +18,7 @@ module-repository/ |-- mosaic-flow/ Pinned methodology Git submodule |-- reports/ Generated reviewable results |-- rtl/ Synthesizable SystemVerilog -|-- verif/ Simulation, assertions, formal, models, coverage +|-- verif/ TB, PyUVM, properties, assertions, formal, coverage |-- work/ Disposable tool databases and generated artifacts |-- Dockerfile Reproducible portable-tool environment |-- Makefile Thin importer of the shared Make API @@ -37,11 +39,13 @@ Organize verification by purpose: ```text verif/ -|-- assertions/ Bound SystemVerilog assertions +|-- properties/ Shared sequences and temporal properties +|-- assertions/ Assertion checker and simulation bind wrapper +|-- coverage/ HDL coverage model and simulation bind wrapper |-- formal/ Formal harnesses and assumptions -|-- tb/ Unit-level simulation testbench and tests -|-- models/ Optional reference models -`-- coverage/ Optional coverage models and plans +|-- pyuvm/ Python tests, agents, monitors, and scoreboards +|-- tb/ Unit-level SystemVerilog testbench and tests +`-- models/ Optional reference models ``` Shared verification libraries may be dependencies, but this repository remains @@ -52,12 +56,17 @@ responsible for proving its module without relying on a full MOSAIC integration. File lists are ordered source manifests and form part of the build contract: - `rtl.f` contains synthesizable sources and include directories. -- `tb.f` contains or imports RTL plus simulation and assertion sources. -- `formal.f` may support formal tools or local utilities even when a specific - `.sby` file lists its own sources. +- `properties.f` supplies include paths or sources shared by checking layers. +- `assertions.f` contains assertion checkers and their bind wrappers. +- `coverage.f` contains HDL coverage models and their bind wrappers. +- `tb.f` imports RTL plus SystemVerilog testbench sources. +- `formal.f` composes RTL, shared properties, assertions, and the formal harness. Use paths that resolve from the repository root. Keep tool-specific command-line options out of shared file lists unless every consuming adapter supports them. +Normal simulation and PyUVM append the property, assertion, and coverage lists +to their primary source list. Formal configurations compile the same wrappers +explicitly. This keeps temporal behavior in one design-owned implementation. ## Configuration hierarchy @@ -82,7 +91,7 @@ Contains module-owned inputs grouped by the shared adapter that consumes them: | `eqy/` | Golden and gate setup plus equivalence strategies | | `openroad/` | PDK-backed design configuration and timing constraints | | `sg_dft/` | Test clocks, modes, resets, and exclusions | -| `symbiyosys/` | Proof mode, engines, sources, and formal top | +| `symbiyosys/` | Proof and cover modes, engines, sources, and formal top | | `synthesis/` | Synthesis timing constraints | | `vc_lp/` | UPF power domains, supplies, states, isolation, and retention | | `verible/` | Style policy and reviewed style waivers | diff --git a/docs/verification-plan.md b/docs/verification-plan.md index e6be071..891ff29 100755 --- a/docs/verification-plan.md +++ b/docs/verification-plan.md @@ -13,32 +13,37 @@ The template verifies: - Asynchronous reset clears the output - An enabled rising edge captures input data - A disabled rising edge preserves output data +- The directed behavior passes through both SystemVerilog and PyUVM stimulus +- Shared assertions run under normal simulation, PyUVM, and formal proof +- Representative property antecedents are reachable in formal cover mode - RTL compiles and elaborates in independent frontends - RTL is generically synthesizable - Yosys synthesis preserves RTL behavior under the configured EQY strategy -The example does not claim protocol, performance, coverage, or parameter-space -closure for a production module. +The example does not claim protocol, performance, quantitative coverage, or +parameter-space closure for a production module. ## Verification environments | Environment | Top | Purpose | | --- | --- | --- | -| Verilator simulation | `mosaic_module_tb` | Directed stimulus, bound SVA, end-to-end smoke check | +| Verilator simulation | `mosaic_module_tb` | Directed SystemVerilog stimulus, bound SVA, and native coverage | +| PyUVM with Verilator | `mosaic_module` | Python-driven smoke test, the same bound SVA, native coverage, and functional coverage | | VCS simulation | `mosaic_module_tb` | Licensed simulation and SAIF generation path | -| SymbiYosys | `mosaic_module_formal` | Reset, update, and hold proofs | +| SymbiYosys proof | `mosaic_module_formal` | Reset, update, and hold proofs using the shared assertion wrapper | +| SymbiYosys cover | `mosaic_module_formal` | Reachability of representative reset, update, and hold scenarios | | EQY | `mosaic_module` | RTL-to-Yosys-netlist equivalence | | Static frontends | `mosaic_module` | Style, lint, compile, hierarchy, and synthesizability checks | ## Requirements traceability -| ID | Requirement | Simulation | Assertion or formal evidence | -| --- | --- | --- | --- | -| `REQ-RST-001` | Active reset clears `data_o` | Reset sequence in `mosaic_module_tb` | Combinational reset assertion in formal harness | -| `REQ-DATA-001` | Enabled edge captures `data_i` | Directed `32'h1234_5678` transfer | `output_updates_when_enabled` and formal update assertion | -| `REQ-HOLD-001` | Disabled edge preserves `data_o` | Disable after directed transfer | `output_holds_when_disabled` and formal hold assertion | -| `REQ-SYN-001` | RTL is synthesizable | Not applicable | Yosys synthesis and structural checks | -| `REQ-EQY-001` | Generic netlist matches RTL | Not applicable | EQY SAT strategy | +| ID | Requirement | SystemVerilog simulation | PyUVM | Assertion or formal evidence | +| --- | --- | --- | --- | --- | +| `REQ-RST-001` | Active reset clears `data_o` | Reset sequence in `mosaic_module_tb` | Reset phase in `MosaicModuleTest` | `reset_clears_output` | +| `REQ-DATA-001` | Enabled edge captures `data_i` | Directed `32'h1234_5678` transfer | Enabled-update phase and functional coverage | `output_updates_when_enabled` | +| `REQ-HOLD-001` | Disabled edge preserves `data_o` | Disable after directed transfer | Disabled-hold phase and functional coverage | `output_holds_when_disabled` | +| `REQ-SYN-001` | RTL is synthesizable | Not applicable | Not applicable | Yosys synthesis and structural checks | +| `REQ-EQY-001` | Generic netlist matches RTL | Not applicable | Not applicable | EQY SAT strategy | Replace this table with every production requirement. A requirement without an evidence mapping is not covered merely because the testbench passes. @@ -67,9 +72,12 @@ Production simulation must add as applicable: ## Assertion plan -Assertions are bound through `verif/assertions/mosaic_module_bind.sv` and are -compiled in the simulation file list. Verilator simulation enables assertions -with `--assert`. +Reusable sequences live in `verif/properties/mosaic_module_sequences.svh`, and +named properties live in `verif/properties/mosaic_module_properties.svh`. The +assertion checker includes those properties and is attached to the DUT through +`verif/assertions/mosaic_module_bind.sv` in normal simulation and PyUVM. +Verilator enables assertions with `--assert`. The formal harness explicitly +instantiates the same checker rather than relying on `bind`. For every assertion, document: @@ -83,11 +91,24 @@ For every assertion, document: An assertion that never reaches its antecedent is not useful evidence. Add cover properties or coverage points for important activation conditions. +## PyUVM plan + +`verif/pyuvm/test_mosaic_module.py` repeats reset, enabled-update, and +disabled-hold behavior through cocotb. PyUVM owns Python stimulus and checking. +It does not call SVA. The HDL simulator compiles the shared assertion and +coverage wrappers, then evaluates them concurrently while PyUVM drives the DUT. + +The flow must retain a clean JUnit result, native coverage, and the separate +`functional-coverage.json` summary under `reports/pyuvm_open_source/`. The +repository CI evidence check verifies that all files exist and that native +coverage names both the assertion and coverage source areas. + ## Formal plan -The formal harness treats reset, enable, and input data as symbolic. It proves -reset behavior plus enabled update and disabled hold behavior with an induction -depth of eight. +The formal harness treats reset, enable, and input data as symbolic. Proof mode +checks reset behavior plus enabled update and disabled hold behavior with an +induction depth of eight. Cover mode demonstrates that representative +antecedents and transfers are reachable. Before release, review: @@ -113,8 +134,10 @@ and any synthesis transformations that require matching rules. ## Coverage plan -The template does not yet collect functional or code coverage. A production -plan must define: +The template produces native Verilator coverage for normal simulation and +PyUVM, a separate JSON functional coverage summary from PyUVM, and formal cover +reachability results. These artifacts demonstrate the integration contract but +do not define production closure targets. A production plan must define: | Coverage type | Required content | | --- | --- | @@ -126,6 +149,10 @@ plan must define: State quantitative targets and the approval process for exclusions. +Review native and Python coverage independently. Python bins do not prove that +bound SVA or HDL cover properties executed, while native HDL coverage does not +replace transaction and scenario coverage sampled by the verification model. + ## Parameter and configuration matrix The smoke flow uses `DATA_WIDTH=32`. Add a reviewed matrix for all supported @@ -168,8 +195,9 @@ Do not retain injected faults in the release branch. - [ ] Enabled portable flows record `PASS`. - [ ] Disabled portable flows have an approved reason and record `SKIP`. - [ ] Simulation regressions pass with recorded tests and seed policy. +- [ ] PyUVM reports clean JUnit, native coverage, and functional coverage evidence. - [ ] Assertions have no failures and meaningful activation is demonstrated. -- [ ] Formal properties are proven or have reviewed bounded status. +- [ ] Formal properties are proven and required cover properties are reachable. - [ ] Equivalence passes for every required synthesis configuration. - [ ] Coverage goals are met and exclusions are approved. - [ ] All waivers are recorded in [Reviewed waivers](waivers.md). diff --git a/filelists/assertions.f b/filelists/assertions.f new file mode 100644 index 0000000..5578ad4 --- /dev/null +++ b/filelists/assertions.f @@ -0,0 +1,3 @@ +# Compile the checker before the wrapper that binds it to the DUT. +verif/assertions/mosaic_module_sva.sv +verif/assertions/mosaic_module_bind.sv diff --git a/filelists/coverage.f b/filelists/coverage.f new file mode 100644 index 0000000..d23beb6 --- /dev/null +++ b/filelists/coverage.f @@ -0,0 +1,3 @@ +# Compile the coverage model before the wrapper that binds it to the DUT. +verif/coverage/mosaic_module_coverage.sv +verif/coverage/mosaic_module_coverage_bind.sv diff --git a/filelists/formal.f b/filelists/formal.f index 37d74e3..c558b2a 100644 --- a/filelists/formal.f +++ b/filelists/formal.f @@ -1,3 +1,6 @@ -+incdir+rtl -rtl/mosaic_module.sv ++define+MOSAIC_FORMAL ++define+FORMAL_ASSERTIONS +-f filelists/rtl.f +-f filelists/properties.f +-f filelists/assertions.f verif/formal/mosaic_module_formal.sv diff --git a/filelists/properties.f b/filelists/properties.f new file mode 100644 index 0000000..a270914 --- /dev/null +++ b/filelists/properties.f @@ -0,0 +1,2 @@ +# Properties are included in wrapper scope, so this layer supplies their path. ++incdir+verif/properties diff --git a/filelists/tb.f b/filelists/tb.f index a24f1cc..204deb8 100755 --- a/filelists/tb.f +++ b/filelists/tb.f @@ -1,5 +1,3 @@ -f filelists/rtl.f +incdir+verif verif/tb/mosaic_module_tb.sv -verif/assertions/mosaic_module_sva.sv -verif/assertions/mosaic_module_bind.sv diff --git a/flows/symbiyosys/formal.sby b/flows/symbiyosys/formal.sby index 49125b7..6afcb94 100644 --- a/flows/symbiyosys/formal.sby +++ b/flows/symbiyosys/formal.sby @@ -6,9 +6,13 @@ depth 8 smtbmc bitwuzla [script] -read -formal -sv mosaic_module.sv mosaic_module_formal.sv +read -formal -D MOSAIC_FORMAL -D MOSAIC_YOSYS_FORMAL -D FORMAL_ASSERTIONS -sv mosaic_module.sv mosaic_module_sva.sv mosaic_module_bind.sv mosaic_module_formal.sv prep -top mosaic_module_formal [files] rtl/mosaic_module.sv +verif/properties/mosaic_module_sequences.svh +verif/properties/mosaic_module_properties.svh +verif/assertions/mosaic_module_sva.sv +verif/assertions/mosaic_module_bind.sv verif/formal/mosaic_module_formal.sv diff --git a/flows/symbiyosys/formal_cover.sby b/flows/symbiyosys/formal_cover.sby new file mode 100644 index 0000000..0549216 --- /dev/null +++ b/flows/symbiyosys/formal_cover.sby @@ -0,0 +1,18 @@ +[options] +mode cover +depth 8 + +[engines] +smtbmc bitwuzla + +[script] +read -formal -D MOSAIC_FORMAL -D MOSAIC_YOSYS_FORMAL -D FORMAL_COVERAGE -sv mosaic_module.sv mosaic_module_coverage.sv mosaic_module_coverage_bind.sv mosaic_module_formal.sv +prep -top mosaic_module_formal + +[files] +rtl/mosaic_module.sv +verif/properties/mosaic_module_sequences.svh +verif/properties/mosaic_module_properties.svh +verif/coverage/mosaic_module_coverage.sv +verif/coverage/mosaic_module_coverage_bind.sv +verif/formal/mosaic_module_formal.sv diff --git a/mosaic-flow b/mosaic-flow index 8fb2950..a3b54f6 160000 --- a/mosaic-flow +++ b/mosaic-flow @@ -1 +1 @@ -Subproject commit 8fb295058d4e569800383e7aa6f5af2c50b01b47 +Subproject commit a3b54f696c19784ea2aea7817dfcba4049ca60a1 diff --git a/verif/assertions/mosaic_module_bind.sv b/verif/assertions/mosaic_module_bind.sv index a588cb1..eb34ecb 100755 --- a/verif/assertions/mosaic_module_bind.sv +++ b/verif/assertions/mosaic_module_bind.sv @@ -1 +1,20 @@ -bind mosaic_module mosaic_module_sva #(.DATA_WIDTH(DATA_WIDTH)) i_mosaic_module_sva (.*); +// Stable wrapper boundary for attaching the assertion checker to the DUT. +module mosaic_module_bind #( + parameter int unsigned DATA_WIDTH = 32 +) ( + input logic clk_i, + input logic rst_ni, + input logic enable_i, + input logic [DATA_WIDTH-1:0] data_i, + input logic [DATA_WIDTH-1:0] data_o +); + + mosaic_module_sva #(.DATA_WIDTH(DATA_WIDTH)) i_mosaic_module_sva (.*); + +endmodule + +`ifndef MOSAIC_FORMAL +// Formal harnesses instantiate this wrapper explicitly because the Yosys +// frontend does not reliably apply simulation-oriented bind statements. +bind mosaic_module mosaic_module_bind #(.DATA_WIDTH(DATA_WIDTH)) i_mosaic_module_bind (.*); +`endif diff --git a/verif/assertions/mosaic_module_sva.sv b/verif/assertions/mosaic_module_sva.sv index 81d1d0e..44fe96d 100755 --- a/verif/assertions/mosaic_module_sva.sv +++ b/verif/assertions/mosaic_module_sva.sv @@ -1,3 +1,4 @@ +// Shared functional checker used by simulation, PyUVM, and formal verification. module mosaic_module_sva #( parameter int unsigned DATA_WIDTH = 32 ) ( @@ -8,10 +9,36 @@ module mosaic_module_sva #( input logic [DATA_WIDTH-1:0] data_o ); +`ifdef MOSAIC_YOSYS_FORMAL + // Yosys cannot parse the concurrent SVA library. This procedural form keeps + // the same reset, update, and hold semantics in the shared checker wrapper. + logic past_valid = 1'b0; + + always_ff @(posedge clk_i) begin + past_valid <= 1'b1; + + if (!rst_ni) begin + assert (data_o == '0); + end else if (past_valid && $past(rst_ni)) begin + if ($past(enable_i)) begin + assert (data_o == $past(data_i)); + end else begin + assert (data_o == $past(data_o)); + end + end + end +`else + // Simulation and SVA-capable formal tools consume the common properties. + `include "mosaic_module_properties.svh" + +reset_clears_output : + assert property (@(posedge clk_i) reset_clears_output_p); + output_updates_when_enabled : - assert property (@(posedge clk_i) disable iff (!rst_ni) enable_i |=> data_o == $past(data_i)); + assert property (@(posedge clk_i) output_updates_when_enabled_p); output_holds_when_disabled : - assert property (@(posedge clk_i) disable iff (!rst_ni) !enable_i |=> $stable(data_o)); + assert property (@(posedge clk_i) output_holds_when_disabled_p); +`endif endmodule diff --git a/verif/coverage/mosaic_module_coverage.sv b/verif/coverage/mosaic_module_coverage.sv new file mode 100644 index 0000000..3568d5b --- /dev/null +++ b/verif/coverage/mosaic_module_coverage.sv @@ -0,0 +1,50 @@ +// Shared coverage model used by simulation, PyUVM, and formal reachability. +module mosaic_module_coverage #( + parameter int unsigned DATA_WIDTH = 32 +) ( + input logic clk_i, + input logic rst_ni, + input logic enable_i, + input logic [DATA_WIDTH-1:0] data_i, + input logic [DATA_WIDTH-1:0] data_o +); + +`ifdef MOSAIC_YOSYS_FORMAL + // Procedural equivalents preserve cover intent in Yosys. The final cover + // checks the same one-cycle representative transfer as the shared property. + logic past_valid = 1'b0; + + always_ff @(posedge clk_i) begin + past_valid <= 1'b1; + + if (rst_ni) begin + cover (enable_i); + cover (!enable_i); + cover (enable_i && data_i == 32'h1234_5678); + cover (past_valid && $past( + rst_ni + ) && $past( + enable_i + ) && $past( + data_i + ) == 32'h1234_5678 && data_o == 32'h1234_5678); + end + end +`else + // Keep coverage directives separate while reusing the common properties. + `include "mosaic_module_properties.svh" + +enabled_operation : + cover property (@(posedge clk_i) disable iff (!rst_ni) enabled_operation_s); + + disabled_operation : + cover property (@(posedge clk_i) disable iff (!rst_ni) disabled_operation_s); + + representative_data : + cover property (@(posedge clk_i) disable iff (!rst_ni) representative_data_s); + + representative_output : + cover property (@(posedge clk_i) disable iff (!rst_ni) representative_output_p); +`endif + +endmodule diff --git a/verif/coverage/mosaic_module_coverage_bind.sv b/verif/coverage/mosaic_module_coverage_bind.sv new file mode 100644 index 0000000..5dd6c6a --- /dev/null +++ b/verif/coverage/mosaic_module_coverage_bind.sv @@ -0,0 +1,22 @@ +// Stable wrapper boundary for attaching the coverage model to the DUT. +module mosaic_module_coverage_bind #( + parameter int unsigned DATA_WIDTH = 32 +) ( + input logic clk_i, + input logic rst_ni, + input logic enable_i, + input logic [DATA_WIDTH-1:0] data_i, + input logic [DATA_WIDTH-1:0] data_o +); + + mosaic_module_coverage #(.DATA_WIDTH(DATA_WIDTH)) i_mosaic_module_coverage (.*); + +endmodule + +`ifndef MOSAIC_FORMAL +// Simulation attaches coverage automatically. Formal instantiates the wrapper +// in its harness to avoid relying on Yosys bind support. +bind mosaic_module mosaic_module_coverage_bind #( + .DATA_WIDTH(DATA_WIDTH) +) i_mosaic_module_coverage_bind (.*); +`endif diff --git a/verif/formal/mosaic_module_formal.sv b/verif/formal/mosaic_module_formal.sv index fa9f1d6..61fb7cf 100644 --- a/verif/formal/mosaic_module_formal.sv +++ b/verif/formal/mosaic_module_formal.sv @@ -1,3 +1,4 @@ +// Minimal unconstrained harness shared by proof and property-reachability tasks. module mosaic_module_formal; localparam int unsigned DATA_WIDTH = 32; @@ -6,26 +7,17 @@ module mosaic_module_formal; (* anyseq *)logic enable_i; (* anyseq *)logic [DATA_WIDTH-1:0] data_i; logic [DATA_WIDTH-1:0] data_o; - logic past_valid = 1'b0; mosaic_module #(.DATA_WIDTH(DATA_WIDTH)) dut (.*); - always_comb begin - if (!rst_ni) begin - assert (data_o == '0); - end - end + // Select one shared wrapper for each proof or reachability task. Keeping + // directives out of this harness prevents formal-only copies from diverging. +`ifdef FORMAL_ASSERTIONS + mosaic_module_bind #(.DATA_WIDTH(DATA_WIDTH)) i_mosaic_module_bind (.*); +`endif - always_ff @(posedge clk_i) begin - past_valid <= 1'b1; - - if (past_valid && rst_ni && $past(rst_ni)) begin - if ($past(enable_i)) begin - assert (data_o == $past(data_i)); - end else begin - assert (data_o == $past(data_o)); - end - end - end +`ifdef FORMAL_COVERAGE + mosaic_module_coverage_bind #(.DATA_WIDTH(DATA_WIDTH)) i_mosaic_module_coverage_bind (.*); +`endif endmodule diff --git a/verif/properties/mosaic_module_properties.svh b/verif/properties/mosaic_module_properties.svh new file mode 100644 index 0000000..8b61241 --- /dev/null +++ b/verif/properties/mosaic_module_properties.svh @@ -0,0 +1,23 @@ +// Included inside assertion and coverage module scopes. An include guard would +// incorrectly suppress declarations in the second wrapper within one compile. +`include "mosaic_module_sequences.svh" + +property representative_output_p; + (enable_i && data_i == 32'h1234_5678) ##1 data_o == 32'h1234_5678; +endproperty + +property reset_clears_output_p; + !rst_ni |-> data_o == '0; +endproperty + +property output_updates_when_enabled_p; + disable iff (!rst_ni) enable_i |=> data_o == $past( + data_i + ); +endproperty + +property output_holds_when_disabled_p; + disable iff (!rst_ni) !enable_i |=> $stable( + data_o + ); +endproperty diff --git a/verif/properties/mosaic_module_sequences.svh b/verif/properties/mosaic_module_sequences.svh new file mode 100644 index 0000000..6e0e41e --- /dev/null +++ b/verif/properties/mosaic_module_sequences.svh @@ -0,0 +1,8 @@ +// Interface-specific sequence vocabulary shared by assertions and coverage. +// This file intentionally has no include guard because each wrapper needs its +// own module-scoped declarations. +sequence enabled_operation_s; enable_i; endsequence + +sequence disabled_operation_s; !enable_i; endsequence + +sequence representative_data_s; enable_i && data_i == 32'h1234_5678; endsequence diff --git a/verif/pyuvm/test_mosaic_module.py b/verif/pyuvm/test_mosaic_module.py new file mode 100644 index 0000000..5f6b0fc --- /dev/null +++ b/verif/pyuvm/test_mosaic_module.py @@ -0,0 +1,53 @@ +"""PyUVM smoke test for the example MOSAIC module.""" + +from __future__ import annotations + +import json +import os +from pathlib import Path + +import cocotb +from cocotb.clock import Clock +from cocotb.triggers import FallingEdge, RisingEdge +from pyuvm import test, uvm_test + + +@test() +class MosaicModuleTest(uvm_test): + """Exercise reset, enabled updates, and disabled holds through PyUVM.""" + + async def run_phase(self) -> None: + """Drive representative operations and emit separate functional coverage.""" + self.raise_objection() + dut = cocotb.top + clock = Clock(dut.clk_i, 10, unit="ns") + cocotb.start_soon(clock.start()) + + # Python coverage complements simulator-native SVA and code coverage. + coverage = {"reset": 0, "enabled_update": 0, "disabled_hold": 0} + dut.rst_ni.value = 0 + dut.enable_i.value = 0 + dut.data_i.value = 0 + await RisingEdge(dut.clk_i) + await RisingEdge(dut.clk_i) + coverage["reset"] += 1 + + await FallingEdge(dut.clk_i) + dut.rst_ni.value = 1 + dut.enable_i.value = 1 + dut.data_i.value = 0x12345678 + await RisingEdge(dut.clk_i) + await FallingEdge(dut.clk_i) + assert int(dut.data_o.value) == 0x12345678 + coverage["enabled_update"] += 1 + + dut.enable_i.value = 0 + dut.data_i.value = 0xDEADBEEF + await RisingEdge(dut.clk_i) + await FallingEdge(dut.clk_i) + assert int(dut.data_o.value) == 0x12345678 + coverage["disabled_hold"] += 1 + + coverage_path = Path(os.environ["PYUVM_FUNCTIONAL_COVERAGE_FILE"]) + coverage_path.write_text(json.dumps(coverage, indent=2) + "\n", encoding="utf-8") + self.drop_objection()