From b41fe539df0949ec10e5cf35064b8b3c69cd4089 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Erick=20Andr=C3=A9s=20Obreg=C3=B3n=20Fonseca?= Date: Thu, 10 Sep 2026 23:02:46 -0600 Subject: [PATCH] [Update] Consume MF20260910V1 qualification flows Update the module template to consume mosaic-flow MF20260910V1 and demonstrate its reusable qualification contracts for parameterized RTL modules. - Pin the mosaic-flow submodule to the MF20260910V1 release revision. - Import the project Make API while preserving the simple single-module flow. - Enable portable coverage, negative, four-state, and static-intent qualification. - Add versioned coverage, compaign, static-intent, profile, and OpenROAD policies. - Qualify minimum, nominal, and wide DATA_WIDTH profiles with isolated evidence. - Add expected-failure controls for coverage, campaign, monitor, and intent gates. - Reuse parameter-aware RTL verification across simulation, PyUVM, and formal. - Add a pinned containerized Nangate45 OpenROAD CI job and physical evidence checks. - Record native, container, and physical evidence through release manifests. - Validate exact methodology revision, cache inputs, clean source state, and output ownership. - Update module creation, multi-module, configuration, verification, waiver, release, and qualification documentation for the MF20260910V1 contracts. - Verify the portable gate, qualification controls, concurrent parameter profiles, static intent, and containerized Nangate45 implementation locally. --- .github/scripts/check-profile-evidence.sh | 73 +++ .../scripts/check-qualification-controls.sh | 259 ++++++++ .github/workflows/rtl-simulation.yml | 170 +++++- Makefile | 4 +- README.md | 33 +- config/coverage-policy.json | 25 + config/design.mk | 12 + config/examples/parameter-profiles.json | 53 ++ config/flows.mk | 21 +- config/qualification-campaigns.json | 220 +++++++ config/qualification-equivalent.eqy | 12 + config/qualification-inequivalent.eqy | 12 + config/static-intent.json | 64 ++ docs/README.md | 14 +- docs/creating-a-module.md | 98 ++- .../examples/multi-module/config/modules.json | 7 + .../config/modules/counter-flows.mk | 2 + .../multi-module/config/modules/counter.mk | 2 + .../multi-module/config/modules/fifo-flows.mk | 2 + .../multi-module/config/modules/fifo.mk | 2 + docs/interface.md | 14 +- docs/multi-module-repositories.md | 568 +++++++----------- docs/project-configuration.md | 77 ++- docs/qualification.md | 170 ++++++ docs/release-checklist.md | 49 +- docs/repository-structure.md | 32 +- docs/verification-plan.md | 87 ++- docs/waivers.md | 17 + flows/openroad/config.mk | 11 +- flows/openroad/evidence-policy.json | 55 ++ flows/openroad/timing.sdc | 2 +- flows/synthesis/timing.sdc | 2 +- mosaic-flow | 2 +- verif/coverage/mosaic_module_coverage.sv | 4 +- verif/formal/mosaic_module_formal.sv | 5 +- verif/mutations/mosaic_module_bad_netlist.v | 15 + verif/properties/mosaic_module_properties.svh | 2 +- verif/properties/mosaic_module_sequences.svh | 2 +- verif/pyuvm/test_mosaic_module.py | 19 +- verif/tb/mosaic_module_four_state_tb.sv | 31 + verif/tb/mosaic_module_tb.sv | 29 +- 41 files changed, 1802 insertions(+), 476 deletions(-) create mode 100755 .github/scripts/check-profile-evidence.sh create mode 100755 .github/scripts/check-qualification-controls.sh create mode 100644 config/coverage-policy.json create mode 100644 config/examples/parameter-profiles.json create mode 100644 config/qualification-campaigns.json create mode 100644 config/qualification-equivalent.eqy create mode 100644 config/qualification-inequivalent.eqy create mode 100644 config/static-intent.json create mode 100644 docs/examples/multi-module/config/modules.json create mode 100644 docs/examples/multi-module/config/modules/counter-flows.mk create mode 100644 docs/examples/multi-module/config/modules/counter.mk create mode 100644 docs/examples/multi-module/config/modules/fifo-flows.mk create mode 100644 docs/examples/multi-module/config/modules/fifo.mk create mode 100644 docs/qualification.md create mode 100644 flows/openroad/evidence-policy.json create mode 100644 verif/mutations/mosaic_module_bad_netlist.v create mode 100644 verif/tb/mosaic_module_four_state_tb.sv diff --git a/.github/scripts/check-profile-evidence.sh b/.github/scripts/check-profile-evidence.sh new file mode 100755 index 0000000..78a2aca --- /dev/null +++ b/.github/scripts/check-profile-evidence.sh @@ -0,0 +1,73 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Validate the project examples and qualify the module parameter profiles with +# bounded concurrency while preserving the ordinary no-profile entry point. +module_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +flow_root="${FLOW_ROOT:-${module_root}/mosaic-flow}" +module_manifest="${module_root}/docs/examples/multi-module/config/modules.json" +profile_manifest="${module_root}/config/examples/parameter-profiles.json" + +python3 "${flow_root}/ci/module_manifest.py" validate \ + --manifest "${module_manifest}" \ + --module-root "${module_root}/docs/examples/multi-module" +module_matrix_a="$(python3 "${flow_root}/ci/module_manifest.py" matrix \ + --manifest "${module_manifest}" \ + --module-root "${module_root}/docs/examples/multi-module")" +module_matrix_b="$(python3 "${flow_root}/ci/module_manifest.py" matrix \ + --manifest "${module_manifest}" \ + --module-root "${module_root}/docs/examples/multi-module")" +test "${module_matrix_a}" = "${module_matrix_b}" + +python3 "${flow_root}/ci/parameter_profiles.py" validate \ + --manifest "${profile_manifest}" +profile_matrix_a="$(python3 "${flow_root}/ci/parameter_profiles.py" matrix \ + --manifest "${profile_manifest}" --module mosaic_module)" +profile_matrix_b="$(python3 "${flow_root}/ci/parameter_profiles.py" matrix \ + --manifest "${profile_manifest}" --module mosaic_module)" +test "${profile_matrix_a}" = "${profile_matrix_b}" + +mkdir -p "${module_root}/ci-artifacts" +printf '%s\n' "${module_matrix_a}" \ + >"${module_root}/ci-artifacts/module-matrix.json" +printf '%s\n' "${profile_matrix_a}" \ + >"${module_root}/ci-artifacts/parameter-profile-matrix.json" + +make -C "${module_root}" \ + PARAMETER_PROFILE_MANIFEST="${profile_manifest}" \ + PROFILE_JOBS="${PROFILE_JOBS:-3}" \ + all-profiles + +python3 - "${module_root}" <<'PY' +import json +import sys +from pathlib import Path + +module_root = Path(sys.argv[1]) +expected = {"width_min": 1, "nominal": 32, "width_wide": 64} +summary = json.loads( + (module_root / "reports/parameter-profile-summary.json").read_text( + encoding="utf-8" + ) +) +assert summary["aggregate_status"] == "PASS", summary +assert {entry["profile"] for entry in summary["profiles"]} == set(expected), summary + +for profile, width in expected.items(): + evidence = json.loads( + (module_root / "reports" / profile / "parameter-profile.json").read_text( + encoding="utf-8" + ) + ) + assert evidence["parameters"]["DATA_WIDTH"] == width, evidence + netlist = ( + module_root + / "work" + / profile + / "yosys_synthesis" + / "mosaic_module_netlist.v" + ) + assert netlist.stat().st_size > 0, netlist +PY + +echo "Module manifest and concurrent parameter-profile checks passed" diff --git a/.github/scripts/check-qualification-controls.sh b/.github/scripts/check-qualification-controls.sh new file mode 100755 index 0000000..7fa142f --- /dev/null +++ b/.github/scripts/check-qualification-controls.sh @@ -0,0 +1,259 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Prove that each portable qualification gate fails closed on a representative +# broken policy, escaped fault, unavailable tool, or disabled monitor. +module_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +flow_root="${FLOW_ROOT:-${module_root}/mosaic-flow}" +control_root="${module_root}/work/qualification-controls" +mkdir -p "${control_root}" + +# Resolve the same pinned tool path exported to normal flow adapters. This also +# makes the controls usable inside the packaged methodology container. +# shellcheck disable=SC2016 +resolved_tool_path="$(make --no-print-directory --silent \ + --eval='mosaic-print-tool-path: ; @printf "%s\n" "$$PATH"' \ + mosaic-print-tool-path)" +export PATH="${resolved_tool_path}" + +expect_failure() { + local name="$1" + shift + if "$@" >"${control_root}/${name}.log" 2>&1; then + echo "Expected ${name} control to fail" >&2 + exit 1 + fi +} + +python3 - "${module_root}" "${control_root}" <<'PY' +import json +import sys +from pathlib import Path + +module_root = Path(sys.argv[1]) +control_root = Path(sys.argv[2]) + +coverage = json.loads( + (module_root / "config/coverage-policy.json").read_text(encoding="utf-8") +) +coverage["coverpoints"][0]["minimum_hits"] = 1_000_000 +(control_root / "deficient-coverage.json").write_text( + json.dumps(coverage, indent=2) + "\n", encoding="utf-8" +) + +negative = { + "schema": "mosaic-qualification-campaigns-v1", + "campaigns": { + "negative": { + "infrastructure_diagnostics": ["MOSAIC_MISSING_TOOL"], + "cases": [ + { + "id": "working_control", + "evidence": "working_control", + "role": "positive_control", + "kind": "positive_control", + "phases": [ + { + "name": "run", + "command": [ + "{python}", + "-c", + "print(\"WORKING_CONTROL_PASS\")", + ], + "expected": "success", + "diagnostic": "WORKING_CONTROL_PASS", + } + ], + }, + { + "id": "missing_tool_control", + "evidence": "missing_tool_control", + "role": "positive_control", + "kind": "infrastructure_control", + "phases": [ + { + "name": "run", + "command": ["MOSAIC_MISSING_TOOL"], + "expected": "success", + } + ], + }, + { + "id": "escaped_mutation", + "evidence": "escaped_mutation", + "role": "negative", + "kind": "simulation_mutation", + "positive_control": "working_control", + "phases": [ + { + "name": "run", + "command": [ + "{python}", + "-c", + "print(\"MUTATION_SHOULD_HAVE_FAILED\")", + ], + "expected": "failure", + "diagnostic": "MUTATION_SHOULD_HAVE_FAILED", + "failure_class": "mutation", + } + ], + }, + ] + } + }, +} +(control_root / "broken-negative-campaign.json").write_text( + json.dumps(negative, indent=2) + "\n", encoding="utf-8" +) + +four_state = json.loads( + (module_root / "config/qualification-campaigns.json").read_text(encoding="utf-8") +) +four_state["campaigns"] = {"four_state": four_state["campaigns"]["four_state"]} +detection = four_state["campaigns"]["four_state"]["cases"][1] +detection["phases"][0]["command"].insert( + 4, "-DMOSAIC_MODULE_DISABLE_UNKNOWN_MONITOR" +) +(control_root / "disabled-monitor-campaign.json").write_text( + json.dumps(four_state, indent=2) + "\n", encoding="utf-8" +) + +static_intent = json.loads( + (module_root / "config/static-intent.json").read_text(encoding="utf-8") +) +base_sdc = (module_root / "flows/synthesis/timing.sdc").read_text( + encoding="utf-8" +) + +static_sdc_cases = { + "missing": base_sdc.replace( + "set_output_delay 0.500 -clock clk_i [all_outputs]\n", "" + ), + "duplicate": base_sdc.replace( + "set_clock_uncertainty 0.100 [get_clocks clk_i]\n", + "set_clock_uncertainty 0.100 [get_clocks clk_i]\n" * 2, + ), + "conflicting": base_sdc.replace( + "create_clock -name clk_i -period 10.000 [get_ports clk_i]\n", + "create_clock -name clk_i -period 10.000 [get_ports clk_i]\n" + "create_clock -name clk_i -period 8.0 [get_ports clk_i]\n", + ), + "broad": base_sdc + "set_false_path -from [all_inputs]\n", + "unsupported": base_sdc + "set_operating_conditions typical\n", +} + +for name, contents in static_sdc_cases.items(): + path = control_root / f"{name}.sdc" + path.write_text(contents, encoding="utf-8") + policy = json.loads(json.dumps(static_intent)) + policy["sdc"]["profiles"] = [policy["sdc"]["profiles"][0]] + policy["sdc"].pop("consistency", None) + policy["sdc"]["profiles"][0]["path"] = ( + f"work/qualification-controls/{name}.sdc" + ) + policy.pop("upf", None) + (control_root / f"{name}-static-intent.json").write_text( + json.dumps(policy, indent=2) + "\n", encoding="utf-8" + ) + +incomplete_policy = { + "schema": "mosaic-static-intent-v1", + "sdc": { + "profiles": [ + { + "name": "incomplete", + "path": "work/qualification-controls/incomplete.sdc", + "kind": "combinational", + } + ] + }, +} +(control_root / "incomplete.sdc").write_text( + "set_max_delay 5.0 -from [get_ports data_i] -to [all_outputs]\n", + encoding="utf-8", +) +(control_root / "incomplete-static-intent.json").write_text( + json.dumps(incomplete_policy, indent=2) + "\n", encoding="utf-8" +) + +forbidden_policy = json.loads(json.dumps(static_intent)) +forbidden_policy.pop("sdc", None) +forbidden_policy["upf"]["path"] = ( + "work/qualification-controls/forbidden.upf" +) +forbidden_policy["upf"]["forbidden_strategies"] = ["isolation"] +base_upf = (module_root / "flows/vc_lp/power.upf").read_text(encoding="utf-8") +(control_root / "forbidden.upf").write_text( + base_upf + + "set_isolation ISO_UNEXPECTED -domain PD_MOSAIC_MODULE " + "-applies_to outputs -clamp_value 0\n", + encoding="utf-8", +) +(control_root / "forbidden-static-intent.json").write_text( + json.dumps(forbidden_policy, indent=2) + "\n", encoding="utf-8" +) +PY + +expect_failure deficient-coverage \ + python3 "${flow_root}/ci/coverage_qualification.py" qualify \ + --policy "${control_root}/deficient-coverage.json" \ + --module-root "${module_root}" \ + --native "${module_root}/reports/verilator_sim/coverage.dat" \ + --lcov "${module_root}/reports/verilator_sim/coverage.info" \ + --source verilator_sim \ + --formal-result PASS \ + --formal-reached 4 \ + --output "${control_root}/deficient-coverage-summary.json" +grep -Fq '"status": "FAIL"' \ + "${control_root}/deficient-coverage-summary.json" + +expect_failure broken-negative-campaign \ + python3 "${flow_root}/ci/qualification_campaign.py" \ + --campaign negative \ + --manifest "${control_root}/broken-negative-campaign.json" \ + --module-root "${module_root}" \ + --flow-root "${flow_root}" \ + --report-dir "${control_root}/negative-reports" \ + --work-dir "${control_root}/negative-work" +grep -Fq '"classification": "escaped_fault"' \ + "${control_root}/negative-reports/summary.json" +grep -Fq '"classification": "infrastructure_failure"' \ + "${control_root}/negative-reports/summary.json" + +expect_failure disabled-monitor \ + python3 "${flow_root}/ci/qualification_campaign.py" \ + --campaign four_state \ + --manifest "${control_root}/disabled-monitor-campaign.json" \ + --module-root "${module_root}" \ + --flow-root "${flow_root}" \ + --report-dir "${control_root}/four-state-reports" \ + --work-dir "${control_root}/four-state-work" +grep -Fq '"classification": "escaped_fault"' \ + "${control_root}/four-state-reports/summary.json" + +test "$(<"${module_root}/reports/static_intent/status.txt")" = PASS + +static_intent_failure() { + local name="$1" + local report="$2" + local code="$3" + expect_failure "${name}-static-intent" \ + python3 "${flow_root}/ci/static_intent.py" \ + --config "${control_root}/${name}-static-intent.json" \ + --module-root "${module_root}" \ + --output-dir "${control_root}/${name}-static-intent-reports" + grep -Fq '"status": "FAIL"' \ + "${control_root}/${name}-static-intent-reports/summary.json" + grep -Fq "\"code\": \"${code}\"" \ + "${control_root}/${name}-static-intent-reports/${report}-findings.json" +} + +static_intent_failure missing sdc missing_command +static_intent_failure duplicate sdc duplicate_command +static_intent_failure conflicting sdc conflicting_command +static_intent_failure broad sdc broad_exception +static_intent_failure incomplete sdc incomplete_max_delay +static_intent_failure forbidden upf forbidden_strategy +static_intent_failure unsupported sdc invalid_sdc_intent + +echo "Portable qualification failure controls passed" diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index e9f2eb0..66e8b25 100644 --- a/.github/workflows/rtl-simulation.yml +++ b/.github/workflows/rtl-simulation.yml @@ -10,12 +10,14 @@ permissions: env: FLOW_ROOT: ${{ github.workspace }}/mosaic-flow + MOSAIC_FLOW_RELEASE: MF20260910V1 + MOSAIC_FLOW_RELEASE_REVISION: 0bd222f827afd802944d5f7e6ebc2ccc3a96f7ea jobs: rtl-checks: name: Open-source RTL checks runs-on: ubuntu-24.04 - timeout-minutes: 15 + timeout-minutes: 30 steps: - name: Check out module repository @@ -40,6 +42,10 @@ jobs: echo "mosaic-flow must be a pinned Git submodule" >&2 exit 1 fi + if [[ "${revision}" != "${MOSAIC_FLOW_RELEASE_REVISION}" ]]; then + echo "mosaic-flow gitlink must resolve to ${MOSAIC_FLOW_RELEASE}" >&2 + exit 1 + fi echo "mosaic_flow_revision=${revision}" >> ci-artifacts/native-context.txt echo "revision=${revision}" >> "${GITHUB_OUTPUT}" @@ -59,6 +65,7 @@ jobs: echo "mosaic-flow checkout ${checked_out_revision} does not match gitlink ${expected_revision}" >&2 exit 1 fi + test -z "$(git -C mosaic-flow status --porcelain)" - name: Validate project flow selection run: make flow-config-check @@ -67,7 +74,7 @@ jobs: uses: actions/cache@v5 with: path: ~/.cache/mosaic - key: mosaic-tools-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('mosaic-flow/config/tool-versions.env', 'mosaic-flow/config/pyuvm-requirements.txt') }} + key: mosaic-tools-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('mosaic-flow/VERSION', 'mosaic-flow/config/tool-versions.env', 'mosaic-flow/config/pyuvm-requirements.txt') }} - name: Set up pinned open-source tools run: make setup-open-source @@ -102,6 +109,25 @@ jobs: - name: Validate native PyUVM evidence run: ./.github/scripts/check-pyuvm-evidence.sh + - name: Validate portable qualification failure controls + run: ./.github/scripts/check-qualification-controls.sh + + - name: Validate manifests and parameter profiles + run: ./.github/scripts/check-profile-evidence.sh + + - name: Generate native release evidence + run: | + make \ + MODULE_REVISION="${GITHUB_SHA}" \ + METHODOLOGY_REVISION="${{ steps.flow-revision.outputs.revision }}" \ + RELEASE_EXECUTION_CONTEXT=native \ + release-manifest release-manifest-validate + + - name: Verify native source cleanliness + run: | + test -z "$(git status --porcelain --untracked-files=normal)" + test -z "$(git -C mosaic-flow status --porcelain)" + - name: Upload RTL reports if: always() uses: actions/upload-artifact@v7 @@ -140,6 +166,10 @@ jobs: echo "mosaic-flow must be a pinned Git submodule" >&2 exit 1 fi + if [[ "${revision}" != "${MOSAIC_FLOW_RELEASE_REVISION}" ]]; then + echo "mosaic-flow gitlink must resolve to ${MOSAIC_FLOW_RELEASE}" >&2 + exit 1 + fi echo "mosaic_flow_revision=${revision}" >> ci-artifacts/container-context.txt echo "revision=${revision}" >> "${GITHUB_OUTPUT}" @@ -159,6 +189,7 @@ jobs: echo "mosaic-flow checkout ${checked_out_revision} does not match gitlink ${expected_revision}" >&2 exit 1 fi + test -z "$(git -C mosaic-flow status --porcelain)" - name: Validate project flow selection run: make flow-config-check @@ -194,6 +225,32 @@ jobs: - name: Validate container PyUVM evidence run: ./.github/scripts/check-pyuvm-evidence.sh + - name: Validate container qualification controls and release evidence + run: | + docker run --rm \ + --user "$(id -u):$(id -g)" \ + --env HOME=/tmp \ + --env MODULE_REVISION="${GITHUB_SHA}" \ + --env METHODOLOGY_REVISION="${{ steps.flow-revision.outputs.revision }}" \ + --volume "${GITHUB_WORKSPACE}:/workspace" \ + --entrypoint bash \ + "mosaic-module-ci:${GITHUB_SHA}" \ + -lc './.github/scripts/check-qualification-controls.sh && \ + make MODULE_REVISION="${MODULE_REVISION}" \ + METHODOLOGY_REVISION="${METHODOLOGY_REVISION}" \ + RELEASE_METHODOLOGY_DIRTY=false \ + RELEASE_EXECUTION_CONTEXT=container \ + release-manifest release-manifest-validate' + + - name: Verify container source cleanliness and ownership + run: | + test -z "$(git status --porcelain --untracked-files=normal)" + test -z "$(git -C mosaic-flow status --porcelain)" + if find reports work -not -user "$(id -un)" -print -quit | grep -q .; then + echo "Containerized checks produced files owned by another user" >&2 + exit 1 + fi + - name: Upload container RTL reports if: always() uses: actions/upload-artifact@v7 @@ -203,3 +260,112 @@ jobs: reports/ ci-artifacts/ if-no-files-found: error + + openroad-checks: + name: Containerized Nangate45 implementation + runs-on: ubuntu-24.04 + timeout-minutes: 30 + + steps: + - name: Check out module repository + uses: actions/checkout@v7 + with: + persist-credentials: false + + - name: Read pinned mosaic-flow submodule revision + id: flow-revision + run: | + revision="$(git ls-files --stage mosaic-flow | awk '$1 == "160000" {print $2}')" + test "${revision}" = "${MOSAIC_FLOW_RELEASE_REVISION}" + echo "revision=${revision}" >> "${GITHUB_OUTPUT}" + + - name: Check out pinned mosaic-flow + uses: actions/checkout@v7 + with: + repository: ECASLab/mosaic-flow + ref: ${{ steps.flow-revision.outputs.revision }} + path: mosaic-flow + persist-credentials: false + + - name: Verify mosaic-flow checkout + run: | + test "$(git -C mosaic-flow rev-parse HEAD)" = \ + "${{ steps.flow-revision.outputs.revision }}" + test -z "$(git -C mosaic-flow status --porcelain)" + + - name: Cache pinned OpenROAD image + uses: actions/cache@v5 + with: + path: ~/.cache/mosaic/openroad-images + key: openroad-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('mosaic-flow/config/tool-versions.env') }} + + - name: Prepare pinned OpenROAD image + run: mosaic-flow/ci/cache_openroad_image.sh + + - name: Run Nangate45 implementation + run: | + make \ + FLOW_openroad=enabled \ + OPENROAD_EXECUTION_MODE=container \ + open-physical + + - name: Validate physical evidence and ownership + run: | + python3 - <<'PY' + import json + from pathlib import Path + + evidence = json.loads( + Path("reports/openroad/evidence.json").read_text(encoding="utf-8") + ) + assert evidence["status"] == "PASS", evidence + assert evidence["design"]["platform"] == "nangate45", evidence + assert evidence["execution"]["mode"] == "container", evidence + image = evidence["execution"]["image"] + assert image["reference"].endswith("@" + image["digest"]), image + assert {item["name"] for item in evidence["artifacts"]} == { + "final_def", + "final_gds", + "final_netlist", + "final_odb", + "final_sdc", + } + assert all(item["bytes"] > 0 for item in evidence["artifacts"]) + assert all(item["passed"] for item in evidence["metrics"]) + PY + if find reports/openroad work/openroad \ + -not -user "$(id -un)" -print -quit | grep -q .; then + echo "OpenROAD produced files owned by another user" >&2 + exit 1 + fi + + - name: Index physical release evidence + run: | + make \ + FLOW_openroad=enabled \ + DISABLED_FLOWS="verible_lint verible_format slang_elaboration verilator_lint yosys_synthesis symbiyosys_formal eqy_equivalence verilator_sim pyuvm_open_source coverage_qualification negative_qualification four_state_qualification static_intent vcs_sim pyuvm_commercial vc_lint vc_cdc sg_cdc sg_dft vc_lp synopsys_synthesis synopsys_primetime synopsys_primepower" \ + MODULE_REVISION="${GITHUB_SHA}" \ + METHODOLOGY_REVISION="${{ steps.flow-revision.outputs.revision }}" \ + RELEASE_EXECUTION_CONTEXT=openroad_container \ + RELEASE_TECHNOLOGY=nangate45 \ + release-manifest release-manifest-validate + grep -Fq 'reports/openroad/evidence.json' \ + reports/release_manifest/openroad_container/manifest.json + + - name: Verify physical source cleanliness + run: | + test -z "$(git status --porcelain --untracked-files=normal)" + test -z "$(git -C mosaic-flow status --porcelain)" + + - name: Upload physical implementation evidence + if: always() + uses: actions/upload-artifact@v7 + with: + name: openroad-nangate45-reports + path: | + reports/openroad/ + reports/release_manifest/openroad_container/ + work/openroad/results/ + work/openroad/reports/ + work/openroad/logs/ + if-no-files-found: error diff --git a/Makefile b/Makefile index f2f7d4b..799c7db 100644 --- a/Makefile +++ b/Makefile @@ -3,6 +3,4 @@ SHELL := /usr/bin/env bash export MODULE_ROOT := $(CURDIR) export FLOW_ROOT ?= $(abspath $(MODULE_ROOT)/mosaic-flow) -include config/design.mk -include $(FLOW_ROOT)/config/tools.mk -include $(FLOW_ROOT)/mk/module.mk +include $(FLOW_ROOT)/mk/project.mk diff --git a/README.md b/README.md index 355d881..3d571eb 100644 --- a/README.md +++ b/README.md @@ -62,7 +62,10 @@ retains an independent project root, flow policy, regression, and report tree. ## Configuration -The root `Makefile` is a thin consumer of `mosaic-flow/mk/module.mk`. +The root `Makefile` is a thin consumer of `mosaic-flow/mk/project.mk`. The +project API preserves the ordinary single-module commands and also activates +validated module and parameter-profile manifests when a repository declares +them. Module identity and paths belong in `config/design.mk`. Flow states and dependencies belong in `config/flows.mk`. Tool-specific project inputs mirror the shared hierarchy under `flows//`. @@ -78,15 +81,20 @@ Start from [Creating a module](docs/creating-a-module.md). At minimum: 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. -7. Run native, containerized, and applicable commercial qualification. +5. Replace the example coverage, campaign, static-intent, and physical-evidence + policies. +6. Declare representative parameter profiles and required evidence. +7. Review flow states and dependencies. +8. Replace template documentation with module-specific records. +9. Run native, containerized, physical, and applicable commercial + qualification. ## Continuous integration -`.github/workflows/rtl-simulation.yml` runs the complete open-source gate on -pushes and pull requests using both native and containerized execution. It does -not invoke licensed Synopsys tools. +`.github/workflows/rtl-simulation.yml` runs the portable gate using both native +and pinned-container execution. It also qualifies the representative parameter +profiles and runs a dedicated containerized Nangate45 OpenROAD job. It does not +invoke licensed commercial tools. `ECASLab/mosaic-flow` is public, so CI does not require an additional repository secret. It checks out the exact submodule revision recorded here rather than a @@ -119,7 +127,12 @@ keep all accepted exceptions in [Reviewed waivers](docs/waivers.md). The open-source gate covers style, formatting, elaboration, lint, generic synthesis, formal proof and cover reachability, RTL-to-netlist equivalence, -SystemVerilog simulation, PyUVM, and native HDL coverage. PyUVM functional +SystemVerilog simulation, PyUVM, quantitative native HDL coverage, negative and +four-state campaigns, and portable SDC and UPF intent checks. 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. +coverage. The public Nangate45 job is exploratory implementation evidence. +Technology-mapped signoff, timing, power, CDC, DFT, low-power, and physical +verification use the configured authorized implementation environment. + +The module-owned qualification contracts and release-manifest commands are +summarized in [Qualification and release evidence](docs/qualification.md). diff --git a/config/coverage-policy.json b/config/coverage-policy.json new file mode 100644 index 0000000..ece7c54 --- /dev/null +++ b/config/coverage-policy.json @@ -0,0 +1,25 @@ +{ + "schema": "mosaic-coverage-policy-v1", + "scope": { + "include": [ + "rtl/*.sv", + "verif/coverage/*.sv" + ] + }, + "thresholds": { + "line": 90, + "branch": 90, + "toggle": 90, + "user": 100 + }, + "coverpoints": [ + {"name": "enabled_operation", "minimum_hits": 1}, + {"name": "disabled_operation", "minimum_hits": 1}, + {"name": "representative_data", "minimum_hits": 1}, + {"name": "representative_output", "minimum_hits": 1} + ], + "exclusions": [], + "formal": { + "required": true + } +} diff --git a/config/design.mk b/config/design.mk index de3b059..b05e20a 100755 --- a/config/design.mk +++ b/config/design.mk @@ -24,8 +24,16 @@ 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 COVERAGE_QUALIFICATION_POLICY := $(MODULE_ROOT)/config/coverage-policy.json +export COVERAGE_QUALIFICATION_SOURCE := verilator_sim +export QUALIFICATION_CAMPAIGN_MANIFEST := $(MODULE_ROOT)/config/qualification-campaigns.json +export STATIC_INTENT_CONFIG := $(MODULE_ROOT)/config/static-intent.json export EQUIVALENCE_CONFIG := $(FLOW_CONFIG_ROOT)/eqy/equivalence.eqy export OPENROAD_CONFIG := $(FLOW_CONFIG_ROOT)/openroad/config.mk +export OPENROAD_CONSTRAINT_FILE := $(FLOW_CONFIG_ROOT)/openroad/timing.sdc +export OPENROAD_EVIDENCE_POLICY := $(FLOW_CONFIG_ROOT)/openroad/evidence-policy.json +export OPENROAD_DESIGN_NAME := $(DESIGN_TOP) +export OPENROAD_FLOW_VARIANT := template_release export SYNTHESIS_CONSTRAINT_FILE := $(FLOW_CONFIG_ROOT)/synthesis/timing.sdc export CDC_CONFIG := $(FLOW_CONFIG_ROOT)/cdc/constraints.tcl export DFT_CONFIG := $(FLOW_CONFIG_ROOT)/sg_dft/constraints.tcl @@ -35,6 +43,10 @@ export REPORT_DIR := $(MODULE_ROOT)/reports export WORK_DIR := $(MODULE_ROOT)/work export OPENROAD_PLATFORM ?= nangate45 +# Release evidence defaults to the portable, technology-independent context. +export RELEASE_MODULE_NAME := mosaic_module +export RELEASE_TECHNOLOGY := technology-independent + # Override in CI or a site-local, untracked environment file. export TECH_SETUP_TCL ?= export TARGET_LIBRARY ?= diff --git a/config/examples/parameter-profiles.json b/config/examples/parameter-profiles.json new file mode 100644 index 0000000..ae3f435 --- /dev/null +++ b/config/examples/parameter-profiles.json @@ -0,0 +1,53 @@ +{ + "schema": "mosaic-parameter-profiles-v1", + "include": [ + { + "name": "width_min", + "parameters": {"DATA_WIDTH": 1}, + "flows": [ + "verible_lint", + "verible_format", + "slang_elaboration", + "verilator_lint", + "yosys_synthesis", + "symbiyosys_formal", + "eqy_equivalence", + "verilator_sim", + "pyuvm_open_source", + "static_intent" + ] + }, + { + "name": "nominal", + "parameters": {"DATA_WIDTH": 32}, + "flows": [ + "verible_lint", + "verible_format", + "slang_elaboration", + "verilator_lint", + "yosys_synthesis", + "symbiyosys_formal", + "eqy_equivalence", + "verilator_sim", + "pyuvm_open_source", + "static_intent" + ] + }, + { + "name": "width_wide", + "parameters": {"DATA_WIDTH": 64}, + "flows": [ + "verible_lint", + "verible_format", + "slang_elaboration", + "verilator_lint", + "yosys_synthesis", + "symbiyosys_formal", + "eqy_equivalence", + "verilator_sim", + "pyuvm_open_source", + "static_intent" + ] + } + ] +} diff --git a/config/flows.mk b/config/flows.mk index 77b15a7..f28914c 100644 --- a/config/flows.mk +++ b/config/flows.mk @@ -8,20 +8,25 @@ FLOW_symbiyosys_formal := enabled FLOW_eqy_equivalence := enabled FLOW_verilator_sim := enabled FLOW_pyuvm_open_source := enabled +FLOW_coverage_qualification := enabled +FLOW_negative_qualification := enabled +FLOW_four_state_qualification := enabled +FLOW_static_intent := enabled FLOW_openroad := disabled -FLOW_vcs_sim := enabled +FLOW_vcs_sim := disabled FLOW_pyuvm_commercial := disabled -FLOW_vc_lint := enabled -FLOW_vc_cdc := enabled +FLOW_vc_lint := disabled +FLOW_vc_cdc := disabled FLOW_sg_cdc := disabled -FLOW_sg_dft := enabled -FLOW_vc_lp := enabled -FLOW_synopsys_synthesis := enabled -FLOW_synopsys_primetime := enabled -FLOW_synopsys_primepower := enabled +FLOW_sg_dft := disabled +FLOW_vc_lp := disabled +FLOW_synopsys_synthesis := disabled +FLOW_synopsys_primetime := disabled +FLOW_synopsys_primepower := disabled # Project dependency overrides. Dependencies must use canonical flow IDs. FLOW_DEPENDENCIES_eqy_equivalence := yosys_synthesis +FLOW_DEPENDENCIES_coverage_qualification := verilator_sim FLOW_DEPENDENCIES_synopsys_primetime := synopsys_synthesis FLOW_DEPENDENCIES_synopsys_primepower := vcs_sim synopsys_synthesis diff --git a/config/qualification-campaigns.json b/config/qualification-campaigns.json new file mode 100644 index 0000000..f32037b --- /dev/null +++ b/config/qualification-campaigns.json @@ -0,0 +1,220 @@ +{ + "schema": "mosaic-qualification-campaigns-v1", + "campaigns": { + "negative": { + "inputs": [ + "config/qualification-equivalent.eqy", + "config/qualification-inequivalent.eqy", + "rtl/mosaic_module.sv", + "verif/mutations/mosaic_module_bad_netlist.v", + "verif/tb/mosaic_module_tb.sv" + ], + "cases": [ + { + "id": "simulation_positive_control", + "evidence": "simulation_positive_control", + "role": "positive_control", + "kind": "positive_control", + "phases": [ + { + "name": "compile", + "command": [ + "{verilator}", + "--binary", + "--timing", + "--assert", + "-Wall", + "-Wno-BLKSEQ", + "-Wno-SYNCASYNCNET", + "--top-module", + "mosaic_module_tb", + "--Mdir", + "{case_work_dir}/obj_dir", + "rtl/mosaic_module.sv", + "verif/tb/mosaic_module_tb.sv" + ], + "expected": "success" + }, + { + "name": "run", + "command": ["{case_work_dir}/obj_dir/Vmosaic_module_tb"], + "expected": "success", + "diagnostic": "MOSAIC_MODULE_TEST_PASS" + } + ] + }, + { + "id": "equivalence_positive_control", + "evidence": "equivalence_positive_control", + "role": "positive_control", + "kind": "equivalence_control", + "phases": [ + { + "name": "run", + "command": [ + "{eqy}", + "-f", + "-d", + "{case_work_dir}/eqy", + "config/qualification-equivalent.eqy" + ], + "expected": "success", + "diagnostic": "Successfully proved designs equivalent" + } + ] + }, + { + "id": "detected_capture_mutation", + "evidence": "detected_capture_mutation", + "role": "negative", + "kind": "simulation_mutation", + "positive_control": "simulation_positive_control", + "phases": [ + { + "name": "compile", + "command": [ + "{verilator}", + "--binary", + "--timing", + "--assert", + "-Wall", + "-Wno-BLKSEQ", + "-Wno-DECLFILENAME", + "-Wno-SYNCASYNCNET", + "--top-module", + "mosaic_module_tb", + "--Mdir", + "{case_work_dir}/obj_dir", + "verif/mutations/mosaic_module_bad_netlist.v", + "verif/tb/mosaic_module_tb.sv" + ], + "expected": "success" + }, + { + "name": "run", + "command": ["{case_work_dir}/obj_dir/Vmosaic_module_tb"], + "expected": "failure", + "diagnostic": "Unexpected output", + "failure_class": "assertion" + } + ] + }, + { + "id": "invalid_width_elaboration", + "evidence": "invalid_width_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "simulation_positive_control", + "phases": [ + { + "name": "compile", + "command": [ + "{verilator}", + "--lint-only", + "-Wall", + "-GDATA_WIDTH=0", + "--top-module", + "mosaic_module", + "rtl/mosaic_module.sv" + ], + "expected": "failure", + "diagnostic": "ASCRANGE|Ascending bit range vector", + "failure_class": "elaboration" + } + ] + }, + { + "id": "expected_equivalence_mismatch", + "evidence": "expected_equivalence_mismatch", + "role": "negative", + "kind": "equivalence_mismatch", + "positive_control": "equivalence_positive_control", + "phases": [ + { + "name": "run", + "command": [ + "{eqy}", + "-f", + "-d", + "{case_work_dir}/eqy", + "config/qualification-inequivalent.eqy" + ], + "expected": "failure", + "diagnostic": "Successfully proved designs inequivalent|Failed to prove equivalence", + "failure_class": "equivalence" + } + ] + } + ] + }, + "four_state": { + "simulator": "iverilog", + "inputs": ["verif/tb/mosaic_module_four_state_tb.sv"], + "cases": [ + { + "id": "disabled_monitor_control", + "evidence": "disabled_monitor_control", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [ + {"control": "enable_i", "values": ["X", "Z"]} + ], + "phases": [ + { + "name": "compile", + "command": [ + "{iverilog}", + "-g2012", + "-s", + "mosaic_module_four_state_tb", + "-DMOSAIC_MODULE_DISABLE_UNKNOWN_MONITOR", + "-o", + "{case_work_dir}/simulation.vvp", + "verif/tb/mosaic_module_four_state_tb.sv" + ], + "expected": "success" + }, + { + "name": "run", + "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], + "expected": "success", + "diagnostic": "UNKNOWN_ENABLE_STIMULUS_REACHED" + } + ] + }, + { + "id": "unknown_enable_detection", + "evidence": "unknown_enable_detection", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_monitor_control", + "injections": [ + {"control": "enable_i", "values": ["X", "Z"]} + ], + "phases": [ + { + "name": "compile", + "command": [ + "{iverilog}", + "-g2012", + "-s", + "mosaic_module_four_state_tb", + "-o", + "{case_work_dir}/simulation.vvp", + "verif/tb/mosaic_module_four_state_tb.sv" + ], + "expected": "success" + }, + { + "name": "run", + "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], + "expected": "failure", + "diagnostic": "UNKNOWN_ENABLE_XZ_DETECTED", + "failure_class": "unknown_control" + } + ] + } + ] + } + } +} diff --git a/config/qualification-equivalent.eqy b/config/qualification-equivalent.eqy new file mode 100644 index 0000000..1fa9cc8 --- /dev/null +++ b/config/qualification-equivalent.eqy @@ -0,0 +1,12 @@ +[gold] +read_verilog -sv rtl/mosaic_module.sv +prep -top mosaic_module + +[gate] +read_verilog -sv rtl/mosaic_module.sv +prep -top mosaic_module + +[strategy sby] +use sby +depth 8 +engine smtbmc bitwuzla diff --git a/config/qualification-inequivalent.eqy b/config/qualification-inequivalent.eqy new file mode 100644 index 0000000..33d9a7b --- /dev/null +++ b/config/qualification-inequivalent.eqy @@ -0,0 +1,12 @@ +[gold] +read_verilog -sv rtl/mosaic_module.sv +prep -top mosaic_module + +[gate] +read_verilog -sv verif/mutations/mosaic_module_bad_netlist.v +prep -top mosaic_module + +[strategy sby] +use sby +depth 8 +engine smtbmc bitwuzla diff --git a/config/static-intent.json b/config/static-intent.json new file mode 100644 index 0000000..7b36c52 --- /dev/null +++ b/config/static-intent.json @@ -0,0 +1,64 @@ +{ + "schema": "mosaic-static-intent-v1", + "sdc": { + "profiles": [ + { + "name": "synthesis", + "path": "flows/synthesis/timing.sdc", + "kind": "sequential", + "expected_ports": { + "clock": ["clk_i"], + "input_delay": ["enable_i", "data_i"], + "output_delay": ["data_o"] + }, + "clocks": [ + {"name": "clk_i", "period": 10.0, "port": "clk_i"} + ], + "intentional_exceptions": [ + {"command": "set_false_path", "from_ports": ["rst_ni"], "to_ports": []} + ] + }, + { + "name": "physical", + "path": "flows/openroad/timing.sdc", + "kind": "sequential", + "expected_ports": { + "clock": ["clk_i"], + "input_delay": ["enable_i", "data_i"], + "output_delay": ["data_o"] + }, + "clocks": [ + {"name": "clk_i", "period": 10.0, "port": "clk_i"} + ], + "intentional_exceptions": [ + {"command": "set_false_path", "from_ports": ["rst_ni"], "to_ports": []} + ] + } + ], + "consistency": [ + { + "profiles": ["synthesis", "physical"], + "commands": [ + "create_clock", + "set_clock_uncertainty", + "set_input_delay", + "set_output_delay", + "set_false_path" + ] + } + ] + }, + "upf": { + "path": "flows/vc_lp/power.upf", + "top": "mosaic_module", + "mode": "always_on", + "required": { + "power_domains": ["PD_MOSAIC_MODULE"], + "supply_ports": ["VDD", "VSS"], + "supply_nets": ["VDD", "VSS"], + "supply_connections": ["VDD", "VSS"], + "domain_supplies": ["PD_MOSAIC_MODULE"] + }, + "forbidden_strategies": [] + } +} diff --git a/docs/README.md b/docs/README.md index e70a96f..2f7e3b5 100644 --- a/docs/README.md +++ b/docs/README.md @@ -43,8 +43,10 @@ keep module-specific decisions here. consumers may rely on. 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 +7. [Qualification and release evidence](qualification.md) explains parameter + profiles, coverage, campaigns, static intent, OpenROAD, and manifests. +8. [Reviewed waivers](waivers.md) records every accepted tool exception. +9. [Release checklist](release-checklist.md) defines the evidence required before publishing a module revision. ## Quick reference @@ -66,8 +68,16 @@ keep module-specific decisions here. | Define CDC intent | `flows/cdc/constraints.tcl` | | Define DFT intent | `flows/sg_dft/constraints.tcl` | | Define power intent | `flows/vc_lp/power.upf` | +| Define coverage policy | `config/coverage-policy.json` | +| Define negative and four-state campaigns | `config/qualification-campaigns.json` | +| Define portable SDC and UPF expectations | `config/static-intent.json` | +| Declare parameter profiles | `config/parameter-profiles.json` | +| Define physical evidence policy | `flows/openroad/evidence-policy.json` | | Validate project policy | `make flow-config-check` | | Run portable acceptance | `make clean open-source` | +| Run all parameter profiles | `make all-profiles PROFILE_JOBS=4` | +| Run containerized OpenROAD | `make FLOW_openroad=enabled OPENROAD_EXECUTION_MODE=container open-physical` | +| Build a release manifest | `make release-manifest release-manifest-validate` | | Validate PyUVM evidence | `./.github/scripts/check-pyuvm-evidence.sh` | | Inspect results | `reports//` | diff --git a/docs/creating-a-module.md b/docs/creating-a-module.md index d7fc563..784c232 100644 --- a/docs/creating-a-module.md +++ b/docs/creating-a-module.md @@ -37,12 +37,20 @@ At minimum, rename and update: - `verif/assertions/mosaic_module_bind.sv` - Both files under `verif/coverage/` - `verif/formal/mosaic_module_formal.sv` +- `verif/tb/mosaic_module_four_state_tb.sv` +- `verif/mutations/mosaic_module_bad_netlist.v` - Every file under `filelists/` - `config/design.mk` +- `config/coverage-policy.json` +- `config/qualification-campaigns.json` +- `config/static-intent.json` +- `config/examples/parameter-profiles.json` +- Both `config/qualification-*.eqy` files - `flows/symbiyosys/formal.sby` - `flows/symbiyosys/formal_cover.sby` - `flows/eqy/equivalence.eqy` - `flows/openroad/config.mk` +- `flows/openroad/evidence-policy.json` - `flows/vc_lp/power.upf` - This repository's title and documentation @@ -130,24 +138,32 @@ and toggle coverage. See ### Parameterized modules -The current portable flow synthesizes and compares one `DESIGN_TOP` using its -default parameter values. A simulation or formal harness may instantiate several -parameter combinations, but that does not create synthesis or equivalence -evidence for each combination. +Use a versioned `config/parameter-profiles.json` manifest when a production +module has several representative elaborations. The template demonstration +manifest remains under `config/examples/` so it can exercise the API without +making profile selection mandatory for ordinary single-module use. For every parameter value that changes generated structure: 1. Exercise it in the self-checking simulation regression. 2. Include it in formal verification when practical. 3. Record whether synthesis and equivalence are required for that profile. -4. Use a reviewed wrapper top or a separate configured verification target when - persistent per-profile synthesis evidence is required. -5. Do not report a manual diagnostic command as release evidence unless its +4. Declare the parameter map and required flows in the profile manifest. +5. Ensure the simulation and formal tops expose and propagate the parameter. +6. Run the bounded aggregate and retain its profile-local evidence. +7. Do not report a manual diagnostic command as release evidence unless its configuration, output, and status are retained reproducibly. -Do not add module-specific orchestration to the thin Makefile. A general -parameter-matrix runner belongs in `mosaic-flow` and must be versioned as a -shared methodology feature. +```sh +make profile-manifest-check +make profile-list +make profile-matrix +make all-profiles PROFILE_JOBS=4 +``` + +The shared runner translates parameters to supported backends and isolates +results below `reports//` and `work//`. Do not add +module-specific profile orchestration to the thin Makefile. ## Configure design intent @@ -182,8 +198,42 @@ to compare the intended golden RTL with the netlist generated by Yosys. ### Physical implementation Set the design name, RTL sources, platform, SDC, utilization, aspect ratio, and -margin in `flows/openroad/config.mk`. Keep `FLOW_openroad` disabled until a -qualified OpenROAD Flow Scripts checkout and PDK are available. +margin in `flows/openroad/config.mk`. Replace +`flows/openroad/evidence-policy.json` with required artifact paths and metric +thresholds for the selected platform. Keep `FLOW_openroad` out of the portable +default when its runtime is too heavy, then enable it explicitly in a dedicated +CI job or qualified local target. + +The pinned container path is reproducible and requires no local ORFS checkout: + +```sh +make FLOW_openroad=enabled \ + OPENROAD_EXECUTION_MODE=container \ + open-physical +``` + +Use `OPENROAD_EXECUTION_MODE=local` with `OPENROAD_FLOW_ROOT=` for an +approved local ORFS tree. Public Nangate45 output is exploratory evidence and +must not be described as foundry signoff. + +## Configure qualification policies + +Replace the template policy values with module-owned requirements: + +- `config/coverage-policy.json` defines quantitative native HDL, named + coverpoint, and formal-cover closure. +- `config/qualification-campaigns.json` defines positive controls, mutations, + expected failure signatures, and four-state cases. +- `config/static-intent.json` defines the timing-intent kind, SDC port coverage, + intentional exceptions, cross-profile consistency, and required or forbidden + UPF structures. +- `flows/openroad/evidence-policy.json` defines physical artifacts and metric + thresholds. + +Keep production RTL out of mutation cases and keep every command as a JSON +argument array. Add positive controls before negative cases so a broken tool or +always-failing monitor cannot masquerade as fault detection. Use a true +four-state simulator for X and Z controls. ## Select flows and dependencies @@ -228,6 +278,8 @@ Prepare tools and run from a clean generated state: make setup-open-source make clean open-source ./.github/scripts/check-pyuvm-evidence.sh +./.github/scripts/check-qualification-controls.sh +./.github/scripts/check-profile-evidence.sh ``` Build and validate the container path: @@ -249,6 +301,28 @@ docker run --rm \ ./.github/scripts/check-pyuvm-evidence.sh ``` +Run exploratory physical acceptance separately: + +```sh +make FLOW_openroad=enabled \ + OPENROAD_EXECUTION_MODE=container \ + open-physical +``` + +After all policy-required flows pass, generate and validate the indexed release +record from a clean tree: + +```sh +make \ + MODULE_REVISION="$(git rev-parse HEAD)" \ + METHODOLOGY_REVISION="$(git -C mosaic-flow rev-parse HEAD)" \ + RELEASE_EXECUTION_CONTEXT=native \ + release-manifest release-manifest-validate +``` + +`RELEASE_ALLOW_DIRTY=enabled` is only a local diagnostic override. The manifest +records the dirty state and is not publishable release evidence. + In the licensed environment, qualify all enabled Synopsys adapters and run the commercial gate. The placeholder VC Lint, CDC, SpyGlass DFT, and VC LP adapters must not be mistaken for completed signoff. diff --git a/docs/examples/multi-module/config/modules.json b/docs/examples/multi-module/config/modules.json new file mode 100644 index 0000000..c7f8717 --- /dev/null +++ b/docs/examples/multi-module/config/modules.json @@ -0,0 +1,7 @@ +{ + "schema": "mosaic-modules-v1", + "include": [ + {"name": "counter", "artifact_suffix": "native"}, + {"name": "fifo", "artifact_suffix": "native"} + ] +} diff --git a/docs/examples/multi-module/config/modules/counter-flows.mk b/docs/examples/multi-module/config/modules/counter-flows.mk new file mode 100644 index 0000000..f51f293 --- /dev/null +++ b/docs/examples/multi-module/config/modules/counter-flows.mk @@ -0,0 +1,2 @@ +# Example module-owned flow policy for a multi-module repository. +FLOW_verilator_lint := enabled diff --git a/docs/examples/multi-module/config/modules/counter.mk b/docs/examples/multi-module/config/modules/counter.mk new file mode 100644 index 0000000..348dd58 --- /dev/null +++ b/docs/examples/multi-module/config/modules/counter.mk @@ -0,0 +1,2 @@ +# Example module-owned design configuration for a multi-module repository. +export DESIGN_TOP := counter diff --git a/docs/examples/multi-module/config/modules/fifo-flows.mk b/docs/examples/multi-module/config/modules/fifo-flows.mk new file mode 100644 index 0000000..f51f293 --- /dev/null +++ b/docs/examples/multi-module/config/modules/fifo-flows.mk @@ -0,0 +1,2 @@ +# Example module-owned flow policy for a multi-module repository. +FLOW_verilator_lint := enabled diff --git a/docs/examples/multi-module/config/modules/fifo.mk b/docs/examples/multi-module/config/modules/fifo.mk new file mode 100644 index 0000000..8647262 --- /dev/null +++ b/docs/examples/multi-module/config/modules/fifo.mk @@ -0,0 +1,2 @@ +# Example module-owned design configuration for a multi-module repository. +export DESIGN_TOP := fifo diff --git a/docs/interface.md b/docs/interface.md index bc60e43..e25ab31 100755 --- a/docs/interface.md +++ b/docs/interface.md @@ -22,8 +22,10 @@ MOSAIC architectural block. | --- | --- | --- | --- | --- | | `DATA_WIDTH` | `int unsigned` | `32` | Positive integers | Width of `data_i` and `data_o` | -The template does not currently assert that `DATA_WIDTH` is greater than zero. -A production module should add static parameter checks for every illegal value. +The normal template elaboration uses 32 bits. The qualification example also +uses 1 and 64 bits. A negative campaign confirms that `DATA_WIDTH=0` is rejected +by elaboration. A production module should add explicit static parameter checks +when its supported frontend set provides a portable mechanism. ## Clocks and resets @@ -74,9 +76,11 @@ replaced or justified for a production module. ## Errors and illegal use The template has no error output and performs no runtime protocol checking. -Unknown input values follow SystemVerilog simulation and synthesis semantics. -Production modules must define illegal transactions, error reporting, and -recovery behavior explicitly. +Unknown data values follow SystemVerilog simulation and synthesis semantics. +An X or Z value on `enable_i` is illegal verification stimulus and the dedicated +four-state monitor rejects it. This monitor is verification collateral rather +than a hardware error output. Production modules must define illegal +transactions, error reporting, and recovery behavior explicitly. ## Low-power behavior diff --git a/docs/multi-module-repositories.md b/docs/multi-module-repositories.md index 67d72ec..0b918eb 100644 --- a/docs/multi-module-repositories.md +++ b/docs/multi-module-repositories.md @@ -2,439 +2,287 @@ ## Scope -The base template represents one independently releasable RTL module. A -repository that intentionally owns several closely related or commonly reused -modules can still use the same methodology by treating each module directory as -an independent `MODULE_ROOT`. - -The shared `mosaic-flow` contract remains unchanged: - -- One design top per module root -- One simulation top per module root -- One formal top per module root -- One set of flow states, constraints, waivers, reports, and work products per - module root - -Do not combine unrelated design tops into one `config/design.mk`. Isolation is -what allows failures, waivers, constraints, and release evidence to remain -attributable to one module. - -## When to use this mode - -Use a multi-module repository when the modules share ownership, release cadence, -and a meaningful common purpose. Examples include a library of small primitive -blocks or a tightly coupled protocol subsystem. - -Keep independently evolving specialized units in separate repositories. A -repository boundary is preferable when a unit has its own release schedule, -technology requirements, access policy, or verification environment. - -## Converting the template - -Convert the stock single-module layout deliberately: - -1. Create `modules//` for the example module. -2. Move its `rtl/`, `verif/`, `filelists/`, `config/`, and `flows/` directories - below that module root. -3. Give the module its own thin Makefile and design-owned documentation. -4. Keep `.github/`, `Dockerfile`, and `mosaic-flow/` at the repository root. -5. Change the generated-artifact entries in `.gitignore` to recursive patterns - so every module's `work/`, `reports/`, and `ci-artifacts/` trees remain - untracked. -6. Add every verification target to `.github/modules.json`. -7. Replace the stock single-module jobs in - `.github/workflows/rtl-simulation.yml` with the matrix jobs. -8. Add integration roots only after the corresponding unit targets pass - independently. -9. Run every manifest entry locally before enabling the new workflow. - -Do not leave the original single-module workflow active beside the matrix -unless duplicate execution is intentional. The matrix becomes the -repository-level open-source acceptance gate. +The base template remains one independently releasable RTL module. A repository +that owns several closely related modules can use the same root hierarchy and +one pinned `mosaic-flow` checkout while qualifying each selected top +independently. + +Use this mode when modules share ownership, release cadence, and a meaningful +common purpose, such as a library of small primitive blocks. Keep independently +evolving specialized units in separate repositories when they need their own +release schedule, technology requirements, access policy, or verification +environment. + +Every selected module retains its own design profile, flow policy, parameter +profiles, reports, work products, constraints, waivers, and release evidence. +Do not combine unrelated tops into one configuration merely to shorten CI. + +## Project API + +The repository keeps one thin root Makefile: + +```make +SHELL := /usr/bin/env bash + +export MODULE_ROOT := $(CURDIR) +export FLOW_ROOT ?= $(abspath $(MODULE_ROOT)/mosaic-flow) + +include $(FLOW_ROOT)/mk/project.mk +``` + +`project.mk` preserves the simple single-module path when no manifest exists. +When `config/modules.json` exists, normal flow targets require a selected +`MODULE` and load its matching design and flow configuration. ## Repository hierarchy -Keep the methodology submodule and repository-level automation at the root. -Place a complete project instance under `modules/` for every verification -target: +Keep shared source categories at the root. Use top-qualified file names only +where modules need different inputs: ```text rtl-library/ -|-- .github/ +|-- config/ | |-- modules.json -| `-- workflows/ -| `-- rtl-quality.yml -|-- modules/ -| |-- fifo/ -| | |-- config/ -| | |-- docs/ -| | |-- filelists/ -| | |-- flows/ -| | |-- rtl/ -| | |-- verif/ -| | `-- Makefile -| |-- alu/ -| `-- multiplier/ -|-- integration/ -| `-- datapath/ +| |-- modules/ +| | |-- counter.mk +| | |-- counter-flows.mk +| | |-- fifo.mk +| | `-- fifo-flows.mk +| `-- parameter-profiles/ +| |-- counter.json +| `-- fifo.json +|-- docs/ +| |-- counter/ +| `-- fifo/ +|-- filelists/ +| |-- counter.rtl.f +| |-- counter.tb.f +| |-- fifo.rtl.f +| `-- fifo.tb.f +|-- flows/ +| |-- synthesis/ +| | |-- counter.timing.sdc +| | `-- fifo.timing.sdc +| `-- symbiyosys/ +| |-- counter.formal.sby +| `-- fifo.formal.sby +|-- rtl/ +|-- verif/ |-- mosaic-flow/ -|-- Dockerfile +|-- Makefile `-- README.md ``` -Each directory under `modules/` follows the normal module hierarchy documented -in [Repository structure](repository-structure.md). An integration target uses -the same hierarchy but may compile several released module sources together. - -## Generated-artifact policy +The standard resolver functions search a top-qualified input first and then the +shared fallback: -The stock single-module ignore patterns must also cover nested module roots. Use -recursive patterns in the repository-level `.gitignore`: +```text +filelists/. +filelists/ -```gitignore -**/work/ -**/reports/ -**/ci-artifacts/ +flows//. +flows// ``` -Do not add separate ignore entries every time a module is created. Confirm the -policy before review: +This supports a shared `rtl.f`, `timing.sdc`, or waiver file when the content is +genuinely common. A module-specific file wins when present. Do not duplicate a +shared file only to satisfy the naming pattern. -```sh -git check-ignore modules//work/probe -git check-ignore modules//reports/probe -git check-ignore modules//ci-artifacts/probe +## Module manifest + +`config/modules.json` is the versioned registry. The `mosaic-modules-v1` schema +requires a nonempty `include` array and unique lowercase names: + +```json +{ + "schema": "mosaic-modules-v1", + "include": [ + {"name": "counter", "artifact_suffix": "native"}, + {"name": "fifo", "artifact_suffix": "native"} + ] +} ``` -Every command must print the tested path. A missing result means the nested -artifact tree is not ignored. +For every entry, the validator requires: + +```text +config/modules/.mk +config/modules/-flows.mk +``` -## Per-module Makefile +Additional fields are retained in the generated CI matrix. Names must begin +with a letter and contain only lowercase letters, digits, and underscores. +Unknown selections, malformed JSON, duplicates, and missing profile files fail +before a tool starts. -Every module keeps a thin Makefile. `MODULE_ROOT` resolves to that module -directory, while CI supplies the repository-level `mosaic-flow` path: +The design profile exports the same variables as `config/design.mk`. Use shared +resolver functions for inputs that support top-qualified fallback: ```make -SHELL := /usr/bin/env bash +export DESIGN_TOP := counter +export TB_TOP := $(DESIGN_TOP)_tb +export FORMAL_TOP := $(DESIGN_TOP)_formal +export DUT_INSTANCE := $(TB_TOP)/dut + +export RTL_FILELIST := $(call mosaic_resolve_filelist,rtl.f) +export TB_FILELIST := $(call mosaic_resolve_filelist,tb.f) +export FORMAL_CONFIG := \ + $(call mosaic_resolve_flow_config,symbiyosys,formal.sby) +``` -export MODULE_ROOT := $(CURDIR) -export FLOW_ROOT ?= $(abspath $(MODULE_ROOT)/../../mosaic-flow) +The matching `-flows.mk` declares that module's complete `FLOW_` +policy and dependency overrides. Standard `REPORT_DIR` and `WORK_DIR` values +are already module-qualified and normally need no override. + +## Selection and matrices -include config/design.mk -include $(FLOW_ROOT)/config/tools.mk -include $(FLOW_ROOT)/mk/module.mk +Validate and inspect the registry before running tools: + +```sh +make module-manifest-check +make module-list +make module-matrix +make module-profile-matrix ``` -Do not add module-specific orchestration to this Makefile. Put module identity -and paths in `config/design.mk`, policy in `config/flows.mk`, and tool intent -under `flows/`. +Run one selected module with the normal API: -## Module manifest +```sh +make MODULE=counter flow-config-check +make MODULE=counter clean open-source +``` -Use `.github/modules.json` as the repository-level source of truth for CI -discovery. Keep names stable because they become job labels and artifact names: +Run every module with bounded concurrency: -```json -{ - "include": [ - { - "name": "fifo", - "path": "modules/fifo" - }, - { - "name": "alu", - "path": "modules/alu" - }, - { - "name": "multiplier", - "path": "modules/multiplier" - } - ] -} +```sh +make all-modules +make all-modules TARGET=open-formal MODULE_JOBS=4 ``` -Every entry must satisfy these rules: +`MODULE_JOBS=0` uses all available processors. The aggregate waits for every +child, preserves completed evidence, and returns nonzero if any module fails or +lacks required status. -- `name` is unique and contains only lowercase letters, numbers, `_`, or `-`. -- `path` is a unique repository-relative directory. -- The directory contains a Makefile and complete module configuration. -- Report and work roots remain below that directory. -- The entry represents a verification target, not merely one SystemVerilog - source file. +Each selected module defaults to: -Validate the manifest during review: +```text +reports/// +work/// +``` -```sh -python3 -m json.tool .github/modules.json >/dev/null +If `config/parameter-profiles/.json` exists, the profile name is inserted +before the flow ID. `module-profile-matrix` combines every registered module +with its own profiles, while a module without a profile manifest contributes a +single `default` entry: + +```text +reports//// +work//// ``` +`make MODULE= clean` removes only that module's generated state. A root +`make clean` without selection removes the complete project report and work +trees. + ## GitHub Actions matrix -The workflow first reads the committed manifest. Every matrix child then checks -out the same module revision and exact methodology gitlink, but runs the flow -from its own module root. The stock workflow does not discover module roots, so -replace its single-module jobs or create a new matrix workflow and disable the -old one. +Generate the matrix through the validated methodology API rather than parsing +the JSON directly: ```yaml jobs: - module-matrix: - name: Read module matrix + qualification-matrix: runs-on: ubuntu-24.04 outputs: - matrix: ${{ steps.modules.outputs.matrix }} + matrix: ${{ steps.matrix.outputs.value }} + flow_revision: ${{ steps.flow.outputs.revision }} steps: - - name: Check out repository - uses: actions/checkout@v7 - - - name: Read module manifest - id: modules - run: | - matrix="$(python3 -c \ - $'import json\nprint(json.dumps(json.load(open(".github/modules.json")))))')" - echo "matrix=${matrix}" >> "${GITHUB_OUTPUT}" - - module-checks: - name: ${{ matrix.name }} RTL checks - needs: module-matrix - runs-on: ubuntu-24.04 - strategy: - fail-fast: false - matrix: ${{ fromJSON(needs.module-matrix.outputs.matrix) }} - - steps: - - name: Check out repository - uses: actions/checkout@v7 + - uses: actions/checkout@v7 with: persist-credentials: false - - - name: Read methodology revision - id: flow-revision + - name: Read pinned mosaic-flow revision + id: flow run: | revision="$(git ls-files --stage mosaic-flow | awk '$1 == "160000" {print $2}')" - if [[ ! "${revision}" =~ ^[0-9a-f]{40}$ ]] - then - echo "mosaic-flow must be a pinned Git submodule" >&2 - exit 1 - fi + test "${#revision}" -eq 40 echo "revision=${revision}" >> "${GITHUB_OUTPUT}" - - - name: Check out pinned methodology - uses: actions/checkout@v7 + - uses: actions/checkout@v7 with: repository: ECASLab/mosaic-flow - ref: ${{ steps.flow-revision.outputs.revision }} + ref: ${{ steps.flow.outputs.revision }} path: mosaic-flow persist-credentials: false + - name: Generate module and profile matrix + id: matrix + run: echo "value=$(make module-profile-matrix)" >> "${GITHUB_OUTPUT}" - - name: Cache open-source tools - uses: actions/cache@v5 + rtl-checks: + name: ${{ matrix.job_name }} / native + needs: qualification-matrix + runs-on: ubuntu-24.04 + strategy: + fail-fast: false + matrix: ${{ fromJSON(needs.qualification-matrix.outputs.matrix) }} + steps: + - uses: actions/checkout@v7 with: - path: ~/.cache/mosaic - 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: | - make -C "${{ matrix.path }}" \ - FLOW_ROOT="${GITHUB_WORKSPACE}/mosaic-flow" \ - flow-config-check - - - name: Run module quality gate + persist-credentials: false + - uses: actions/checkout@v7 + with: + repository: ECASLab/mosaic-flow + ref: ${{ needs.qualification-matrix.outputs.flow_revision }} + path: mosaic-flow + persist-credentials: false + - name: Run selected qualification run: | - make -C "${{ matrix.path }}" \ - FLOW_ROOT="${GITHUB_WORKSPACE}/mosaic-flow" \ + make MODULE="${{ matrix.module }}" \ + PROFILE="${{ matrix.profile }}" \ 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 + - uses: actions/upload-artifact@v7 if: always() - uses: actions/upload-artifact@v7 with: - name: ${{ matrix.name }}-open-source-reports - path: ${{ matrix.path }}/reports/ + name: ${{ matrix.job_name }}-reports + path: reports/${{ matrix.module }}/ if-no-files-found: error ``` -`fail-fast: false` allows every module to finish and report its own result. The -matrix job still fails when any child fails, so an integration or release job -that declares `needs: module-checks` cannot start prematurely. +Use the same validated matrix for native and pinned-container jobs. Verify the +exact methodology gitlink in every child. Qualify cache scopes, image tags, +artifact names, report paths, and diagnostics by module and profile. Run +containers as the invoking UID and GID and verify output ownership. -The production workflow should retain the template's tool-version reporting and -diagnostic artifact behavior. Use module-qualified diagnostic paths and artifact -names so parallel jobs cannot be confused during review. +`fail-fast: false` lets every module report its result. The matrix job still +fails when any child fails, so integration jobs with `needs: rtl-checks` cannot +start prematurely. -Do not reduce the matrix workflow to only the abbreviated native job above. The -repository-level conversion must preserve these behaviors from the stock -workflow for every manifest entry: +## Verification and integration -- 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. -- Diagnostic artifacts are uploaded even when the flow fails. +Every module job independently runs its enabled style, elaboration, lint, +synthesis, formal, equivalence, simulation, PyUVM, coverage, campaign, and +static-intent flows. Its source lists must include any packages or instantiated +dependencies needed for a clean build. A unit job must not consume another +module job's generated output. -The container execution step must select the matrix module explicitly: - -```yaml -- name: Run containerized module flow - run: | - docker run --rm \ - --user "$(id -u):$(id -g)" \ - --env HOME=/tmp \ - --volume "${GITHUB_WORKSPACE}:/workspace" \ - --workdir "/workspace/${{ matrix.path }}" \ - "mosaic-module-ci:${GITHUB_SHA}" clean open-source -``` - -Use distinct artifact names such as -`${{ matrix.name }}-native-reports` and -`${{ matrix.name }}-container-reports`. Reusing one artifact name across matrix -children can overwrite or combine evidence from unrelated module roots. - -## RTL checks per module - -`make clean open-source` runs the enabled portable flow graph against only the -current module root. Consequently, each matrix child independently performs: - -- Verible style lint and formatting -- Slang compilation and elaboration -- Strict Verilator lint -- Yosys generic synthesis -- 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 -are resolved within that module only. Reports are naturally isolated under -`modules//reports//` because `MODULE_ROOT` differs for every -matrix child. - -## Regression configuration - -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. 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. -6. Record the test inventory and expected native plus functional coverage in - `docs/verification-plan.md`. -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 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 - -The container image embeds the shared methodology. Mount the repository root -and select the module with Docker's working directory: - -```sh -docker run --rm \ - --user "$(id -u):$(id -g)" \ - --env HOME=/tmp \ - --volume "$PWD:/workspace" \ - --workdir /workspace/modules/fifo \ - mosaic-module-ci:local clean open-source -``` - -A container matrix may use -`--workdir "/workspace/${{ matrix.path }}"`. Building the same image in every -matrix child is correct but expensive. Prefer one cached image build per -workflow, then distribute or publish that immutable image for the module jobs. -Keep the embedded `mosaic-flow` revision equal to the parent gitlink. - -## Commercial flows - -Run licensed flows from each module root in the authorized environment: - -```sh -make -C modules/fifo FLOW_ROOT="$PWD/mosaic-flow" synopsys-check-env -make -C modules/fifo FLOW_ROOT="$PWD/mosaic-flow" synopsys-all -``` - -Commercial reports and constraints remain module-specific. Do not combine -waivers or signoff evidence from different tops into one status. - -## Dependencies and integration - -Source dependencies do not normally create GitHub job dependencies. A FIFO that -uses a shared package must compile the package in its own file list rather than -waiting for a package job. - -Use `needs: module-checks` for an integration target that should run only after -every unit target passes: - -```yaml - integration-checks: - needs: module-checks - runs-on: ubuntu-24.04 - steps: - - name: Run integrated datapath verification - run: | - make -C integration/datapath \ - FLOW_ROOT="${GITHUB_WORKSPACE}/mosaic-flow" \ - clean open-source -``` - -The integration directory owns its top, assertions, constraints, waivers, and -reports. Unit-level waivers do not automatically authorize an integration-level -violation. - -## Local execution - -Run the same commands used by one matrix child: - -```sh -make -C modules/fifo FLOW_ROOT="$PWD/mosaic-flow" flow-config-check -make -C modules/fifo FLOW_ROOT="$PWD/mosaic-flow" clean open-source - -make -C modules/alu FLOW_ROOT="$PWD/mosaic-flow" flow-config-check -make -C modules/alu FLOW_ROOT="$PWD/mosaic-flow" clean open-source -``` +An integration target owns its own top, file lists, assertions, constraints, +waivers, and reports. Run it only after all required unit qualifications pass. +Unit waivers do not automatically authorize an integration-level violation. -The repository may provide a root convenience target that iterates the committed -manifest, but it must delegate to these module-local Makefiles. The module-local -commands remain the release contract. +Commercial flows remain module-selected and run only in the authorized +environment. Physical implementation may be selected per module or profile. +Public Nangate45 results remain exploratory evidence. ## Release requirements -A multi-module repository release requires: +A multi-module release requires: -- Every manifest entry to complete its enabled unit flows -- Every module regression to pass +- A valid deterministic registry and combined module-profile matrix +- Every selected unit flow and parameter profile to complete +- Separate reports, work products, release manifests, and waiver records - Every required integration target to pass after unit checks -- Separate artifacts and waiver records for every verification target - The same module revision and methodology gitlink in every job - Documented compatibility between modules released together +- No output collision during bounded concurrent execution -Do not infer repository success from one passing module. The matrix aggregate -and required integration jobs define the repository-level result. +Do not infer repository success from one passing module. The aggregate matrix +and required integration jobs define repository-level acceptance. diff --git a/docs/project-configuration.md b/docs/project-configuration.md index 195672d..4a0e55a 100644 --- a/docs/project-configuration.md +++ b/docs/project-configuration.md @@ -4,12 +4,15 @@ The module consumes shared defaults and then applies design-owned policy: -1. `config/design.mk` defines module identity, paths, and technology inputs. -2. `mosaic-flow/config/tools.mk` defines pinned tool locations and command +1. `mosaic-flow/mk/project.mk` selects the single-module or manifest-backed + project mode. +2. `config/design.mk` defines module identity, paths, and technology inputs. +3. `mosaic-flow/config/tools.mk` defines pinned tool locations and command defaults. -3. `mosaic-flow/config/flows.mk` defines canonical flow states and dependencies. -4. Module `config/flows.mk` replaces shared states or dependencies. -5. Make command-line assignments provide temporary diagnostic overrides. +4. `mosaic-flow/config/flows.mk` defines canonical flow states and dependencies. +5. Module `config/flows.mk` replaces shared states or dependencies. +6. A selected parameter profile narrows flows and overrides parameters or tops. +7. Make command-line assignments provide temporary diagnostic overrides. The root Makefile establishes this order. Keep it free of design-specific flow logic. @@ -51,6 +54,12 @@ The current Design Compiler adapter reads `$(CONSTRAINT_DIR)/timing.sdc`. Keep `SYNTHESIS_CONSTRAINT_FILE` consistent with that file. +Qualification paths include `COVERAGE_QUALIFICATION_POLICY`, +`QUALIFICATION_CAMPAIGN_MANIFEST`, `STATIC_INTENT_CONFIG`, +`OPENROAD_EVIDENCE_POLICY`, and the optional +`PARAMETER_PROFILE_MANIFEST`. Keep these files versioned and below +`MODULE_ROOT` so release evidence can hash them. + ## Flow states Every canonical flow has an explicit module policy: @@ -65,10 +74,11 @@ 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 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. +The template enables normal Verilator simulation, open-source PyUVM, coverage +qualification, negative testing, four-state testing, and static-intent checks +in the portable gate. OpenROAD is enabled only by the dedicated physical job. +All commercial flows are disabled by default and must be enabled deliberately +in a qualified licensed environment. Run: @@ -78,6 +88,55 @@ make flow-config-check Review the output after every state or dependency change. +Coverage qualification depends on the normal Verilator simulation artifact: + +```make +FLOW_DEPENDENCIES_coverage_qualification := verilator_sim +``` + +The validator rejects an enabled flow whose dependency is disabled, as well as +unknown IDs, cycles, and contradictory aggregate policy. + +## Parameter profiles + +The example `config/examples/parameter-profiles.json` qualifies `DATA_WIDTH` +values 1, 32, and 64 without making profile selection mandatory for the normal +single-module command. Validate and run it with: + +```sh +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + profile-manifest-check +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + profile-list +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + profile-matrix +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + all-profiles PROFILE_JOBS=3 +``` + +Production modules should move their reviewed manifest to +`config/parameter-profiles.json`. Once that default exists, ordinary flow +targets require `PROFILE=`. Each profile receives isolated +`reports//` and `work//` trees. `all-profiles` uses bounded +parallel execution and fails when any child fails or lacks required evidence. + +## Qualification and release inputs + +The module-owned policy files use versioned schemas supplied by the pinned +methodology: + +| Input | Purpose | +| --- | --- | +| `config/coverage-policy.json` | Independent line, branch, toggle, user, named coverpoint, and formal-cover requirements | +| `config/qualification-campaigns.json` | Positive controls, expected failures, mutations, and Icarus X/Z detection | +| `config/static-intent.json` | Expected timing kind, SDC commands and ports, profile consistency, and UPF structure | +| `flows/openroad/evidence-policy.json` | Required physical artifacts, report patterns, and metric thresholds | + +Run the gates independently with `make open-coverage`, +`make open-negative`, `make open-four-state`, and +`make open-static-intent`. See [Qualification and release +evidence](qualification.md) for their evidence and signoff boundaries. + ## PyUVM and shared verification PyUVM does not import or invoke SystemVerilog assertions. The Python test drives diff --git a/docs/qualification.md b/docs/qualification.md new file mode 100644 index 0000000..ed86650 --- /dev/null +++ b/docs/qualification.md @@ -0,0 +1,170 @@ +# Qualification and release evidence + +[Return to the module documentation index](README.md). + +This template consumes `mosaic-flow` release `MF20260910V1`, resolved by the +gitlink to commit `0bd222f827afd802944d5f7e6ebc2ccc3a96f7ea`. The module owns +the policies and design fixtures below. The pinned methodology owns schema +validation, execution, status semantics, and release indexing. + +## Evidence classes + +| Class | Template use | Signoff boundary | +| --- | --- | --- | +| Portable | Lint, elaboration, generic synthesis, formal, equivalence, simulation, PyUVM, coverage, campaigns, and static intent | Required public CI evidence, not technology signoff | +| Optional physical | Containerized ORFS on public Nangate45 | Exploratory place-and-route evidence, not foundry signoff | +| Commercial | VCS, VC Lint, CDC, DFT, VC LP, Design Compiler, PrimeTime, and PrimePower | Disabled until a licensed site qualifies the adapter and project inputs | +| Signoff | Project-selected PDK, libraries, corners, extraction, STA, power, CDC, DFT, low-power, DRC, and LVS | Must run in the authorized implementation environment | + +Every canonical enabled flow must write `PASS`. A disabled flow is an approved +policy `SKIP`. `FAIL`, `BLOCKED`, missing evidence, an unauthorized skip, or +stale evidence rejects release-manifest generation. + +## Coverage policy + +`config/coverage-policy.json` declares independent minimum line, branch, +toggle, and user coverage, required named coverpoints, and formal cover +reachability. The template reuses native coverage generated by normal Verilator +simulation through `COVERAGE_QUALIFICATION_SOURCE=verilator_sim`. It does not +duplicate SVA or the HDL coverage wrapper. + +PyUVM functional coverage remains a separate JSON artifact. It describes +transactions and scenarios observed by the Python verification environment and +must not be combined numerically with structural HDL coverage. + +```sh +make open-sim +make open-formal +make open-coverage +``` + +The CI control script raises a named-coverpoint requirement beyond the collected +result and proves that deficient evidence fails qualification. + +## Negative and four-state campaigns + +`config/qualification-campaigns.json` declares commands as arrays, expected +results, required diagnostic expressions, and failure classes. The negative +campaign contains successful simulation and equivalence controls before testing +an injected capture fault, an illegal width, and a deliberately inequivalent +netlist. Mutations stay under `verif/mutations/` and are never compiled by the +normal file lists. + +The four-state campaign compiles +`verif/tb/mosaic_module_four_state_tb.sv` with pinned Icarus. One control proves +that X and Z stimulus reaches `enable_i` with the monitor disabled. The paired +case requires the monitor to reject both values with the expected diagnostic. + +```sh +make open-negative +make open-four-state +``` + +Evidence is isolated below `reports///` and +`work///`. Profile and module names are inserted before the flow +ID when selected. `.github/scripts/check-qualification-controls.sh` also proves +that escaped mutations, unavailable tools, and disabled unknown-value monitors +cannot qualify. + +## Portable static intent + +`config/static-intent.json` identifies this example as a sequential design. It +requires `clk_i`, uncertainty, input and output delays, the reviewed asynchronous +reset false path, agreement between synthesis and physical SDC, and an +always-on UPF domain. Isolation, retention, level shifting, and power switches +are not required by this example. + +```sh +make open-static-intent +``` + +The CI controls reject missing, duplicate, conflicting, broad, incomplete, +forbidden, and unsupported SDC or UPF intent. This parser-backed gate has no +timing graph, voltage model, cell library, or CDC analysis. It is not STA, CDC, +IEEE 1801, VC LP, or physical signoff. + +## Parameter profiles + +The non-default example at `config/examples/parameter-profiles.json` exercises +minimum, nominal, and wide `DATA_WIDTH` values. Testbench and formal tops expose +the same parameter and propagate it to the DUT. Supported adapters receive the +profile override through their native parameter mechanism. + +```sh +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + profile-manifest-check +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + profile-matrix +make PARAMETER_PROFILE_MANIFEST=config/examples/parameter-profiles.json \ + all-profiles PROFILE_JOBS=3 +``` + +`PROFILE_JOBS` bounds parallel execution. The aggregate result is +`reports/parameter-profile-summary.json`. Each child receives isolated +`reports//` and `work//` trees and the aggregate fails when a +child fails or lacks evidence. + +## Multi-module example + +`docs/examples/multi-module/config/modules.json` demonstrates the versioned +`mosaic-modules-v1` registry without turning this single-module repository into +a multi-module project. The selected `counter` and `fifo` entries resolve their +matching files under `config/modules/`. + +```sh +python3 mosaic-flow/ci/module_manifest.py validate \ + --manifest docs/examples/multi-module/config/modules.json \ + --module-root docs/examples/multi-module +python3 mosaic-flow/ci/module_manifest.py matrix \ + --manifest docs/examples/multi-module/config/modules.json \ + --module-root docs/examples/multi-module +``` + +The CI script emits the module and parameter-profile matrices twice and compares +them byte for byte before running the bounded profile regression. + +## OpenROAD evidence + +The physical job enables `openroad` explicitly and uses the immutable ORFS +image recorded by the methodology release. The module supplies +`flows/openroad/config.mk`, `timing.sdc`, and `evidence-policy.json`. + +```sh +make FLOW_openroad=enabled \ + OPENROAD_EXECUTION_MODE=container \ + open-physical +``` + +The policy requires nonempty final DEF, GDS, ODB, SDC, and netlist artifacts. +It also requires zero setup, hold, slew, fanout, capacitance, and routing +violations for the representative fixture. `reports/openroad/evidence.json` +records the image reference and digest, platform, flow variant, input and +artifact hashes, sizes, and parsed metrics. The container runs as the invoking +UID and GID. + +For a qualified local ORFS checkout, set `OPENROAD_EXECUTION_MODE=local` and +`OPENROAD_FLOW_ROOT=`. Do not replace the CI image with a floating tag. + +## Release manifest + +Run every flow required by the selected policy before generating a manifest: + +```sh +make \ + MODULE_REVISION="$(git rev-parse HEAD)" \ + METHODOLOGY_REVISION="$(git -C mosaic-flow rev-parse HEAD)" \ + RELEASE_EXECUTION_CONTEXT=native \ + release-manifest release-manifest-validate +``` + +The manifest hashes declared RTL, verification layers, file lists, constraints, +waivers, policies, and configuration. It indexes canonical status, normalized +coverage, PyUVM functional coverage, static-intent findings, campaign summaries, +and physical evidence when enabled. It records the selected module, profile, +technology, execution context, revisions, and exact tool identities. + +A dirty module or methodology tree fails by default. During local development, +`RELEASE_ALLOW_DIRTY=enabled` permits generation while recording the dirty +state. Such a manifest is diagnostic only and must not be published as release +evidence. CI always supplies explicit revisions and validates clean source and +the pinned methodology checkout. diff --git a/docs/release-checklist.md b/docs/release-checklist.md index ed9399c..fd2b3f1 100644 --- a/docs/release-checklist.md +++ b/docs/release-checklist.md @@ -7,6 +7,7 @@ gate alone is not sufficient ASIC release evidence. - [ ] The module name, repository name, top-level names, and Docker labels agree. - [ ] Supported parameter values and configurations are listed. +- [ ] The parameter-profile manifest validates and its matrix is deterministic. - [ ] Unsupported modes and external assumptions are explicit. - [ ] The `mosaic-flow` gitlink points to a qualified published revision. - [ ] The resolved flow policy has been captured with `make flow-config-check`. @@ -44,6 +45,16 @@ gate alone is not sufficient ASIC release evidence. - [ ] 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. +- [ ] The versioned coverage policy passes for line, branch, toggle, user, + required named coverpoints, and formal reachability. +- [ ] A deficient-coverage control proves that threshold enforcement fails + closed. +- [ ] Negative campaigns include successful controls and detect assertion, + elaboration, equivalence, and mutation failures as applicable. +- [ ] Four-state cases use a pinned four-state simulator and prove both X/Z + stimulus reachability and monitor detection. +- [ ] Escaped-fault, unavailable-tool, and disabled-monitor controls are rejected + with the expected classifications. - [ ] VCS or Xcelium PyUVM evidence passes when commercial PyUVM belongs to the module's release scope. @@ -56,6 +67,13 @@ gate alone is not sufficient ASIC release evidence. - [ ] DFT test modes, controllability, observability, and exclusions are reviewed. - [ ] UPF power domains, states, isolation, retention, and supplies match the architecture. +- [ ] The versioned static-intent policy names the applicable timing kind and + required or forbidden power strategies. +- [ ] Portable SDC and UPF validation passes its positive policy and rejects + missing, duplicate, conflicting, broad, incomplete, forbidden, and unsupported + controls. +- [ ] Reviewers understand that portable static intent does not replace STA, + CDC, IEEE 1801, or commercial low-power signoff. - [ ] VC Lint, selected CDC, SpyGlass DFT, and VC LP adapters are qualified for the installed release and all expected statuses pass. @@ -78,6 +96,12 @@ gate alone is not sufficient ASIC release evidence. physical implementation belongs to this module's release scope. - [ ] Preliminary open-source physical results are not labeled as commercial signoff evidence. +- [ ] The physical-evidence policy requires nonempty DEF, GDS, ODB, SDC, and + netlist artifacts plus reviewed metric thresholds. +- [ ] OpenROAD evidence records an immutable image digest or exact local ORFS + revision, platform, variant, input hashes, artifact hashes, and metrics. +- [ ] Containerized physical output is owned by the invoking user and isolated + by selected module and parameter profile. ## Waivers @@ -90,16 +114,27 @@ gate alone is not sufficient ASIC release evidence. ## Reproducibility and evidence - [ ] Native `make clean open-source` passes. +- [ ] Every representative profile passes with bounded concurrency and isolated + reports, work products, formal artifacts, and netlists. - [ ] 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. +- [ ] Commercial gates pass in the authorized local or self-hosted environment + when they belong to release scope. Otherwise their policy is an approved + `SKIP`. - [ ] Reports identify module revision, methodology revision, tool versions, constraints, technology, date, and configuration. - [ ] CI or release storage retains logs and required databases. - [ ] No generated work database, credential, license, or proprietary library is committed to Git. +- [ ] Native, container, and applicable physical release manifests validate with + explicit module and methodology revisions. +- [ ] Release manifests hash declared RTL, verification layers, constraints, + policies, waivers, and configuration inputs and index every enabled compact + evidence summary. +- [ ] No dirty-tree override is present in publishable release evidence. +- [ ] The source tree and `mosaic-flow` submodule remain clean after validation. ## Final commands @@ -107,13 +142,19 @@ gate alone is not sufficient ASIC release evidence. git submodule status make flow-config-check make clean open-source +./.github/scripts/check-qualification-controls.sh +./.github/scripts/check-profile-evidence.sh +make FLOW_openroad=enabled OPENROAD_EXECUTION_MODE=container open-physical +make release-manifest release-manifest-validate make synopsys-check-env make synopsys-all CDC_TOOL=vc ``` -Run the Synopsys commands only in the licensed environment after all -release-specific adapters are qualified. Select `CDC_TOOL=sg` instead when that -engine is the approved project policy. +Pass full revision IDs and a distinct `RELEASE_EXECUTION_CONTEXT` when creating +publishable manifests. Run the Synopsys commands only in the licensed +environment after all release-specific adapters are qualified and when those +flows belong to release scope. Select `CDC_TOOL=sg` instead when that engine is +the approved project policy. ## Approval record diff --git a/docs/repository-structure.md b/docs/repository-structure.md index f8fa7fd..177cd58 100644 --- a/docs/repository-structure.md +++ b/docs/repository-structure.md @@ -11,7 +11,8 @@ module-repository/ |-- .github/ Portable module CI and evidence checks | |-- scripts/ CI-owned release-evidence validators | `-- workflows/ Native and containerized quality gates -|-- config/ Cross-flow module configuration +|-- config/ Cross-flow configuration and qualification policy +| `-- examples/ Non-default manifest examples and fixtures |-- docs/ Design contract and engineering records |-- filelists/ Ordered source manifests |-- flows/ Module-owned inputs for shared flow adapters @@ -43,6 +44,7 @@ verif/ |-- assertions/ Assertion checker and simulation bind wrapper |-- coverage/ HDL coverage model and simulation bind wrapper |-- formal/ Formal harnesses and assumptions +|-- mutations/ Deliberately incorrect qualification fixtures |-- pyuvm/ Python tests, agents, monitors, and scoreboards |-- tb/ Unit-level SystemVerilog testbench and tests `-- models/ Optional reference models @@ -81,6 +83,14 @@ flows. Defines project policy. Every canonical flow is explicitly enabled or disabled, and project-specific dependencies may replace shared defaults. +Versioned JSON policies beside these Make fragments define machine-readable +qualification intent. `coverage-policy.json` sets HDL and formal coverage +requirements, `qualification-campaigns.json` defines expected-failure and +four-state controls, and `static-intent.json` describes the SDC and UPF subset +that must be present. A production parameter matrix normally belongs in +`config/parameter-profiles.json`. The template keeps its demonstration matrix +under `config/examples/` so the no-profile single-module command remains valid. + ### `flows/` Contains module-owned inputs grouped by the shared adapter that consumes them: @@ -107,14 +117,14 @@ therefore improve a tool adapter without silently replacing module constraints. root Makefile imports: ```make -include config/design.mk -include $(FLOW_ROOT)/config/tools.mk -include $(FLOW_ROOT)/mk/module.mk +include $(FLOW_ROOT)/mk/project.mk ``` -Keep this Makefile thin. New reusable targets belong in `mosaic-flow`. New -module inputs belong in `config/design.mk` or the matching module-owned flow -directory. +`project.mk` loads the normal single-module configuration when no module +manifest exists. It activates validated project selection when +`config/modules.json` is present. Keep this Makefile thin. New reusable targets +belong in `mosaic-flow`. New module inputs belong in `config/design.mk`, a +selected module configuration, or the matching module-owned flow directory. The complete shared hierarchy is documented in [`mosaic-flow/docs/architecture.md`](../mosaic-flow/docs/architecture.md). @@ -125,7 +135,9 @@ The complete shared hierarchy is documented in Contains statuses, logs, and compact summaries intended for review or CI retention. The first file to inspect is usually -`reports//status.txt`. +`reports//status.txt`. Parameter profiles and selected +modules insert their names before the flow ID. Release manifests are separated +again by execution context under `reports/release_manifest//`. ### `work/` @@ -138,7 +150,9 @@ flow reports while preserving the report root placeholder. ## Container and CI ownership The GitHub workflow validates the module with the exact `mosaic-flow` revision -recorded by the gitlink. It runs both native and containerized portable checks. +recorded by the gitlink. It runs native and containerized portable checks plus a +dedicated containerized Nangate45 physical fixture. Generated ownership and +submodule cleanliness are checked before evidence is uploaded. The Dockerfile copies only the executable shared methodology into the image. The module repository is mounted at runtime, which keeps RTL and generated diff --git a/docs/verification-plan.md b/docs/verification-plan.md index 891ff29..02819e4 100755 --- a/docs/verification-plan.md +++ b/docs/verification-plan.md @@ -19,9 +19,17 @@ The template verifies: - 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, quantitative coverage, or -parameter-space closure for a production module. +- Minimum, nominal, and wide parameter profiles propagate consistently through + elaboration, lint, synthesis, formal, equivalence, simulation, and PyUVM +- Quantitative HDL and formal coverage policy passes +- Negative controls prove assertion, elaboration, equivalence, and monitor + failures are detected +- A pinned four-state simulator detects X and Z on the example control input +- Portable SDC and UPF intent matches the module-owned expectation + +The example demonstrates the qualification mechanisms. It does not claim that +the three representative widths close the parameter space of a replacement +production module. ## Verification environments @@ -34,13 +42,18 @@ parameter-space closure for a production module. | 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 | +| Coverage qualification | Collected Verilator and SymbiYosys evidence | Enforce line, branch, toggle, user, named coverpoint, and formal-cover policy | +| Negative campaign | Module-owned controls and mutations | Prove expected failures are attributable and do not escape | +| Icarus four-state campaign | `mosaic_module_four_state_tb` | Prove X and Z control detection with a disabled-monitor control | +| Static-intent validator | Module SDC and UPF | Check the supported portable timing and power-intent subset | +| Containerized ORFS | `mosaic_module` | Produce exploratory Nangate45 physical evidence | ## Requirements traceability | 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-DATA-001` | Enabled edge captures `data_i` | Width-aware all-ones 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 | @@ -54,9 +67,11 @@ The current directed test: 1. Holds asynchronous reset active for two rising edges. 2. Releases reset on a falling edge. -3. Applies one enabled input value. -4. Disables updates and checks the registered output. -5. Waits long enough for one-cycle implication assertions to complete. +3. Captures an all-ones input value. +4. Changes the input to zero while disabled and checks that the output holds. +5. Re-enables capture and checks the zero transition. +6. Reasserts asynchronous reset and checks that the output clears. +7. Waits long enough for one-cycle implication assertions to complete. Production simulation must add as applicable: @@ -136,8 +151,10 @@ and any synthesis transformations that require matching rules. 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: +reachability results. `config/coverage-policy.json` currently requires 90 +percent line, branch, and toggle coverage, 100 percent user coverage, hits on +four named coverpoints, and passing formal cover reachability. A production +plan must review and replace these example targets as appropriate: | Coverage type | Required content | | --- | --- | @@ -155,38 +172,42 @@ 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 -values. At minimum, test boundary widths and values that change generated -structure. +The versioned demonstration manifest is +`config/examples/parameter-profiles.json`. It stays outside the default path so +the repository remains usable with the simple no-profile command. | Configuration | Simulation | Formal | Synthesis | Equivalence | Status | | --- | --- | --- | --- | --- | --- | -| `DATA_WIDTH=32` | Required | Required | Required | Required | Template smoke | +| `DATA_WIDTH=1` | Required | Required | Required | Required | Boundary profile | +| `DATA_WIDTH=32` | Required | Required | Required | Required | Nominal profile | +| `DATA_WIDTH=64` | Required | Required | Required | Required | Wide profile | -The current Yosys and EQY adapters qualify only `DESIGN_TOP` with its default -parameter values. Listing another profile in this table does not make synthesis -or equivalence evidence exist for it. Use a reviewed wrapper top or separate -configured verification target for every profile that requires persistent -synthesis and EQY reports until `mosaic-flow` provides a shared parameter-matrix -contract. +The manifest also selects elaboration, lint, PyUVM, and static-intent evidence +for every profile. The shared runner translates `DATA_WIDTH` for each backend, +renders profile-local formal and EQY configuration, and isolates every report, +work product, and synthesized netlist below the profile name. The bounded +aggregate preserves completed evidence and fails if any child fails or is +missing. -Simulation and formal harnesses may instantiate multiple profiles in one top. -Record those instances explicitly and distinguish structural elaboration from -per-profile synthesis, timing, power, and equivalence evidence. +This representative matrix is infrastructure evidence, not automatic proof of +every legal positive integer. A production module must select its legal +boundaries and both sides of every structural feature toggle. ## Negative testing -Qualification must prove that checking fails when behavior is wrong. Introduce -temporary faults or dedicated negative fixtures to confirm detection of: +`config/qualification-campaigns.json` proves that checking fails when behavior +is wrong. It contains successful simulation and equivalence controls plus +dedicated negative fixtures for: -- Incorrect reset value -- Update while disabled -- Failure to capture while enabled -- Assertion failure -- RTL and synthesized netlist mismatch -- Lint or formatting violation +- A mutation that violates enabled capture behavior +- An illegal zero width rejected during elaboration +- A deliberately inequivalent candidate netlist +- X and Z control values detected by a four-state monitor -Do not retain injected faults in the release branch. +The CI acceptance script additionally proves that deficient coverage, an +escaped mutation, an unavailable tool, a disabled X/Z monitor, and malformed +static intent all fail closed. Deliberately incorrect RTL remains isolated under +`verif/mutations/` and is not included in normal file lists. ## Exit criteria @@ -200,5 +221,9 @@ Do not retain injected faults in the release branch. - [ ] 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. +- [ ] Negative and four-state campaigns pass with their positive controls. +- [ ] Portable static intent passes and its limitations are understood. +- [ ] Every selected parameter profile has isolated complete evidence. +- [ ] Release manifests validate for each required execution context. - [ ] All waivers are recorded in [Reviewed waivers](waivers.md). - [ ] The release checklist is complete. diff --git a/docs/waivers.md b/docs/waivers.md index 541ddce..c531469 100755 --- a/docs/waivers.md +++ b/docs/waivers.md @@ -38,3 +38,20 @@ Expires or removal condition: ## Accepted waivers None. + +## Qualification exclusions + +Coverage exclusions belong in `config/coverage-policy.json` with an attributable +reason and review record. They are not tool waivers and must not be used to hide +unreachable requirements or untested legal behavior. + +The negative mutation command suppresses Verilator `DECLFILENAME` only for the +deliberately misnamed candidate file under `verif/mutations/`. This command-local +diagnostic control is not applied to production RTL and is not an accepted +release waiver. Normal lint remains governed by the reviewed Verilator waiver +file above. + +Portable static-intent validation limitations and the public Nangate45 signoff +boundary are methodology scope statements, not waivers. A required commercial +or signoff flow must be enabled and pass once it belongs to the module release +scope. diff --git a/flows/openroad/config.mk b/flows/openroad/config.mk index c5c529f..6dbce65 100644 --- a/flows/openroad/config.mk +++ b/flows/openroad/config.mk @@ -2,6 +2,11 @@ export DESIGN_NAME = mosaic_module export PLATFORM = $(OPENROAD_PLATFORM) export VERILOG_FILES = $(REPO_ROOT)/rtl/mosaic_module.sv export SDC_FILE = $(REPO_ROOT)/flows/openroad/timing.sdc -export CORE_UTILIZATION = 35 -export CORE_ASPECT_RATIO = 1 -export CORE_MARGIN = 2 +# RTL-to-netlist equivalence is qualified by the module's EQY flow. Disable the +# optional ORFS Kepler LEC helper so the pinned physical container remains +# portable across GitHub-hosted and local x86_64 runners. +export LEC_CHECK = 0 +# Keep the tiny template design large enough for the platform's default PDN +# straps. Production modules must replace these representative dimensions. +export DIE_AREA = 0 0 60 60 +export CORE_AREA = 5 5 55 55 diff --git a/flows/openroad/evidence-policy.json b/flows/openroad/evidence-policy.json new file mode 100644 index 0000000..49b8b21 --- /dev/null +++ b/flows/openroad/evidence-policy.json @@ -0,0 +1,55 @@ +{ + "schema": "mosaic-openroad-evidence-policy-v1", + "artifacts": [ + {"name": "final_def", "directory": "results", "path": "6_final.def"}, + {"name": "final_gds", "directory": "results", "path": "6_final.gds"}, + {"name": "final_odb", "directory": "results", "path": "6_final.odb"}, + {"name": "final_sdc", "directory": "results", "path": "6_final.sdc"}, + {"name": "final_netlist", "directory": "results", "path": "6_final.v"} + ], + "metrics": [ + { + "name": "setup_violations", + "directory": "reports", + "path": "6_finish.rpt", + "pattern": "^setup violation count[ \\t]+(?P[0-9]+)$", + "maximum": 0 + }, + { + "name": "hold_violations", + "directory": "reports", + "path": "6_finish.rpt", + "pattern": "^hold violation count[ \\t]+(?P[0-9]+)$", + "maximum": 0 + }, + { + "name": "slew_violations", + "directory": "reports", + "path": "6_finish.rpt", + "pattern": "^max slew violation count[ \\t]+(?P[0-9]+)$", + "maximum": 0 + }, + { + "name": "fanout_violations", + "directory": "reports", + "path": "6_finish.rpt", + "pattern": "^max fanout violation count[ \\t]+(?P[0-9]+)$", + "maximum": 0 + }, + { + "name": "capacitance_violations", + "directory": "reports", + "path": "6_finish.rpt", + "pattern": "^max cap violation count[ \\t]+(?P[0-9]+)$", + "maximum": 0 + }, + { + "name": "routing_violations", + "directory": "logs", + "path": "5_2_route.log", + "pattern": "Number of violations = (?P[0-9]+)", + "match": "last", + "maximum": 0 + } + ] +} diff --git a/flows/openroad/timing.sdc b/flows/openroad/timing.sdc index 3ca8d0a..65b08fa 100644 --- a/flows/openroad/timing.sdc +++ b/flows/openroad/timing.sdc @@ -1,5 +1,5 @@ create_clock -name clk_i -period 10.000 [get_ports clk_i] set_clock_uncertainty 0.100 [get_clocks clk_i] -set_input_delay 0.500 -clock clk_i [remove_from_collection [all_inputs] [get_ports {clk_i rst_ni}]] +set_input_delay 0.500 -clock clk_i [get_ports {enable_i data_i}] set_output_delay 0.500 -clock clk_i [all_outputs] set_false_path -from [get_ports rst_ni] diff --git a/flows/synthesis/timing.sdc b/flows/synthesis/timing.sdc index 3ca8d0a..65b08fa 100644 --- a/flows/synthesis/timing.sdc +++ b/flows/synthesis/timing.sdc @@ -1,5 +1,5 @@ create_clock -name clk_i -period 10.000 [get_ports clk_i] set_clock_uncertainty 0.100 [get_clocks clk_i] -set_input_delay 0.500 -clock clk_i [remove_from_collection [all_inputs] [get_ports {clk_i rst_ni}]] +set_input_delay 0.500 -clock clk_i [get_ports {enable_i data_i}] set_output_delay 0.500 -clock clk_i [all_outputs] set_false_path -from [get_ports rst_ni] diff --git a/mosaic-flow b/mosaic-flow index a3b54f6..0bd222f 160000 --- a/mosaic-flow +++ b/mosaic-flow @@ -1 +1 @@ -Subproject commit a3b54f696c19784ea2aea7817dfcba4049ca60a1 +Subproject commit 0bd222f827afd802944d5f7e6ebc2ccc3a96f7ea diff --git a/verif/coverage/mosaic_module_coverage.sv b/verif/coverage/mosaic_module_coverage.sv index 3568d5b..4729bb1 100644 --- a/verif/coverage/mosaic_module_coverage.sv +++ b/verif/coverage/mosaic_module_coverage.sv @@ -20,14 +20,14 @@ module mosaic_module_coverage #( if (rst_ni) begin cover (enable_i); cover (!enable_i); - cover (enable_i && data_i == 32'h1234_5678); + cover (enable_i && data_i == {DATA_WIDTH{1'b1}}); cover (past_valid && $past( rst_ni ) && $past( enable_i ) && $past( data_i - ) == 32'h1234_5678 && data_o == 32'h1234_5678); + ) == {DATA_WIDTH{1'b1}} && data_o == {DATA_WIDTH{1'b1}}); end end `else diff --git a/verif/formal/mosaic_module_formal.sv b/verif/formal/mosaic_module_formal.sv index 61fb7cf..722814e 100644 --- a/verif/formal/mosaic_module_formal.sv +++ b/verif/formal/mosaic_module_formal.sv @@ -1,6 +1,7 @@ // Minimal unconstrained harness shared by proof and property-reachability tasks. -module mosaic_module_formal; - localparam int unsigned DATA_WIDTH = 32; +module mosaic_module_formal #( + parameter int unsigned DATA_WIDTH = 32 +); (* gclk *)logic clk_i; (* anyseq *)logic rst_ni; diff --git a/verif/mutations/mosaic_module_bad_netlist.v b/verif/mutations/mosaic_module_bad_netlist.v new file mode 100644 index 0000000..94a9b3f --- /dev/null +++ b/verif/mutations/mosaic_module_bad_netlist.v @@ -0,0 +1,15 @@ +// Verification-only candidate with deliberately incorrect combinational data. +module mosaic_module #( + parameter DATA_WIDTH = 32 +) ( + input wire clk_i, + input wire rst_ni, + input wire enable_i, + input wire [DATA_WIDTH-1:0] data_i, + output wire [DATA_WIDTH-1:0] data_o +); + wire unused_controls = clk_i | rst_ni | enable_i; + + assign data_o = ~data_i ^ {DATA_WIDTH{unused_controls & 1'b0}}; + +endmodule diff --git a/verif/properties/mosaic_module_properties.svh b/verif/properties/mosaic_module_properties.svh index 8b61241..adb2ac5 100644 --- a/verif/properties/mosaic_module_properties.svh +++ b/verif/properties/mosaic_module_properties.svh @@ -3,7 +3,7 @@ `include "mosaic_module_sequences.svh" property representative_output_p; - (enable_i && data_i == 32'h1234_5678) ##1 data_o == 32'h1234_5678; + (enable_i && data_i == {DATA_WIDTH{1'b1}}) ##1 data_o == {DATA_WIDTH{1'b1}}; endproperty property reset_clears_output_p; diff --git a/verif/properties/mosaic_module_sequences.svh b/verif/properties/mosaic_module_sequences.svh index 6e0e41e..948b56b 100644 --- a/verif/properties/mosaic_module_sequences.svh +++ b/verif/properties/mosaic_module_sequences.svh @@ -5,4 +5,4 @@ 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 +sequence representative_data_s; enable_i && data_i == {DATA_WIDTH{1'b1}}; endsequence diff --git a/verif/pyuvm/test_mosaic_module.py b/verif/pyuvm/test_mosaic_module.py index 5f6b0fc..543378c 100644 --- a/verif/pyuvm/test_mosaic_module.py +++ b/verif/pyuvm/test_mosaic_module.py @@ -20,6 +20,8 @@ async def run_phase(self) -> None: """Drive representative operations and emit separate functional coverage.""" self.raise_objection() dut = cocotb.top + data_width = len(dut.data_i) + all_ones = (1 << data_width) - 1 clock = Clock(dut.clk_i, 10, unit="ns") cocotb.start_soon(clock.start()) @@ -35,19 +37,28 @@ async def run_phase(self) -> None: await FallingEdge(dut.clk_i) dut.rst_ni.value = 1 dut.enable_i.value = 1 - dut.data_i.value = 0x12345678 + dut.data_i.value = all_ones await RisingEdge(dut.clk_i) await FallingEdge(dut.clk_i) - assert int(dut.data_o.value) == 0x12345678 + assert int(dut.data_o.value) == all_ones coverage["enabled_update"] += 1 dut.enable_i.value = 0 - dut.data_i.value = 0xDEADBEEF + dut.data_i.value = 0 await RisingEdge(dut.clk_i) await FallingEdge(dut.clk_i) - assert int(dut.data_o.value) == 0x12345678 + assert int(dut.data_o.value) == all_ones coverage["disabled_hold"] += 1 + dut.enable_i.value = 1 + await RisingEdge(dut.clk_i) + await FallingEdge(dut.clk_i) + assert int(dut.data_o.value) == 0 + + dut.rst_ni.value = 0 + await FallingEdge(dut.clk_i) + dut.rst_ni.value = 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() diff --git a/verif/tb/mosaic_module_four_state_tb.sv b/verif/tb/mosaic_module_four_state_tb.sv new file mode 100644 index 0000000..96e95bb --- /dev/null +++ b/verif/tb/mosaic_module_four_state_tb.sv @@ -0,0 +1,31 @@ +module mosaic_module_four_state_tb; + logic enable_i; + logic saw_x; + logic saw_z; + + initial begin + saw_x = 1'b0; + saw_z = 1'b0; + + enable_i = 1'bx; + #1; + saw_x = $isunknown(enable_i); + + enable_i = 1'bz; + #1; + saw_z = $isunknown(enable_i); + +`ifdef MOSAIC_MODULE_DISABLE_UNKNOWN_MONITOR + if (saw_x && saw_z) begin + $display("UNKNOWN_ENABLE_STIMULUS_REACHED"); + $finish; + end + $fatal(1, "FOUR_STATE_STIMULUS_BROKEN"); +`else + if (saw_x && saw_z) begin + $fatal(1, "UNKNOWN_ENABLE_XZ_DETECTED"); + end + $finish; +`endif + end +endmodule diff --git a/verif/tb/mosaic_module_tb.sv b/verif/tb/mosaic_module_tb.sv index 53f55b7..68980a9 100755 --- a/verif/tb/mosaic_module_tb.sv +++ b/verif/tb/mosaic_module_tb.sv @@ -1,5 +1,6 @@ -module mosaic_module_tb; - localparam int unsigned DATA_WIDTH = 32; +module mosaic_module_tb #( + parameter int unsigned DATA_WIDTH = 32 +); logic clk_i; logic rst_ni; @@ -20,19 +21,37 @@ module mosaic_module_tb; repeat (2) @(posedge clk_i); @(negedge clk_i); rst_ni = 1'b1; - data_i = 32'h1234_5678; + data_i = '1; enable_i = 1'b1; @(posedge clk_i); @(negedge clk_i); enable_i = 1'b0; - assert (data_o == 32'h1234_5678) + assert (data_o == '1) else $fatal(1, "Unexpected output: %h", data_o); - // Allow both one-cycle SVA implications to reach their consequents. + // Exercise both transition directions before checking the hold path. + data_i = '0; + @(posedge clk_i); + @(negedge clk_i); + assert (data_o == '1) + else $fatal(1, "Disabled output changed unexpectedly: %h", data_o); + + enable_i = 1'b1; + @(posedge clk_i); + @(negedge clk_i); + enable_i = 1'b0; + assert (data_o == '0) + else $fatal(1, "Unexpected cleared output: %h", data_o); + + // Reassert reset to exercise the asynchronous control in both directions. + rst_ni = 1'b0; + #1ns; + rst_ni = 1'b1; repeat (2) @(posedge clk_i); @(negedge clk_i); + $display("MOSAIC_MODULE_TEST_PASS"); $finish; end endmodule