From b0d971b0a68a008fcc3188bc3c6dfb29894f987a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Erick=20Andr=C3=A9s=20Obreg=C3=B3n=20Fonseca?= Date: Wed, 16 Sep 2026 22:21:07 -0600 Subject: [PATCH 1/2] [Add] Parameterizable write gate and verification flows Implement a reusable write-control gate and qualify its portable open-source behavior. - Add parameterizable per-bit write permitting and suppression observation with conservative unknown-control behavior. - Add directed, alternating, randomized, idle, and suppression testing across widths 1, 2, 4, 8, 16, 32, 64, and 128. - Add representative register and memory integrations that compare gated state against ungated reference models and measure activity. - Add shared predicates, bound assertions, complete formal proofs, and RTL-to-Yosys-netlist equivalence checks. - Add functional, transition, integration, line, branch, toggle, and formal cover qualification with explicit release thresholds. - Add invalid-width, inverted-suppression mutation, and four-state X/Z detection campaigns. - Add executable SDC and UPF static-intent checks plus CDC, DFT, synthesis, and low-power integration collateral. - Add a representative WIDTH=2 Nangate45 OpenROAD implementation and preserve its evidence in the native CI release manifest. - Register the write gate in concurrent local, native GitHub Actions, and containerized module execution. - Extend shared formatting and release evidence handling for the new module collateral. - Add interface, project configuration, power characterization, verification-plan, waiver, and template-aligned release documentation. - Record commercial and foundry checks as reviewed portable skips that become mandatory in the first stateful consuming integration. - Verify all portable gates natively and in the pinned Docker environment. --- .github/workflows/rtl-simulation.yml | 59 +++- README.md | 1 + config/coverage-policies/write_gate.json | 54 ++++ config/modules.json | 3 +- config/modules/write_gate-flows.mk | 36 +++ config/modules/write_gate.mk | 59 ++++ config/parameter-profiles/write_gate.json | 53 +++ .../qualification-campaigns/write_gate.json | 139 ++++++++ config/static-intent/write_gate.json | 28 ++ docs/README.md | 1 + docs/write_gate/README.md | 27 ++ docs/write_gate/interface.md | 61 ++++ docs/write_gate/power-characterization.md | 42 +++ docs/write_gate/project-configuration.md | 45 +++ docs/write_gate/release-checklist.md | 249 ++++++++++++++ docs/write_gate/verification-plan.md | 39 +++ docs/write_gate/waivers.md | 15 + filelists/write_gate.assertions.f | 2 + filelists/write_gate.coverage.f | 4 + filelists/write_gate.formal.f | 4 + filelists/write_gate.properties.f | 1 + filelists/write_gate.rtl.f | 2 + filelists/write_gate.tb.f | 5 + flows/cdc/write_gate.constraints.tcl | 2 + flows/eqy/write_gate.equivalence.eqy | 11 + flows/openroad/write_gate.config.mk | 11 + flows/openroad/write_gate.timing.sdc | 14 + flows/sg_dft/write_gate.constraints.tcl | 2 + flows/symbiyosys/write_gate.cover.sby | 18 ++ flows/symbiyosys/write_gate.formal.sby | 18 ++ flows/synthesis/write_gate.timing.sdc | 17 + flows/vc_lp/write_gate.power.upf | 13 + rtl/write_gate.sv | 24 ++ scripts/verible-format | 6 +- verif/assertions/write_gate_bind.sv | 17 + verif/assertions/write_gate_sva.sv | 44 +++ verif/coverage/write_gate_coverage.sv | 61 ++++ verif/coverage/write_gate_coverage_bind.sv | 17 + .../write_gate_integration_coverage.sv | 33 ++ .../write_gate_transition_coverage.sv | 42 +++ verif/formal/write_gate_formal.sv | 22 ++ verif/formal/write_gate_integration_formal.sv | 40 +++ .../write_gate_inverted_suppress_mutant.sv | 14 + verif/properties/write_gate_predicates.svh | 37 +++ verif/tb/write_gate_four_state_tb.sv | 47 +++ verif/tb/write_gate_integration_test_case.sv | 306 ++++++++++++++++++ verif/tb/write_gate_invalid_width_tb.sv | 6 + verif/tb/write_gate_tb.sv | 23 ++ verif/tb/write_gate_test_case.sv | 111 +++++++ 49 files changed, 1881 insertions(+), 4 deletions(-) create mode 100644 config/coverage-policies/write_gate.json create mode 100644 config/modules/write_gate-flows.mk create mode 100644 config/modules/write_gate.mk create mode 100644 config/parameter-profiles/write_gate.json create mode 100644 config/qualification-campaigns/write_gate.json create mode 100644 config/static-intent/write_gate.json create mode 100644 docs/write_gate/README.md create mode 100644 docs/write_gate/interface.md create mode 100644 docs/write_gate/power-characterization.md create mode 100644 docs/write_gate/project-configuration.md create mode 100644 docs/write_gate/release-checklist.md create mode 100644 docs/write_gate/verification-plan.md create mode 100644 docs/write_gate/waivers.md create mode 100644 filelists/write_gate.assertions.f create mode 100644 filelists/write_gate.coverage.f create mode 100644 filelists/write_gate.formal.f create mode 100644 filelists/write_gate.properties.f create mode 100644 filelists/write_gate.rtl.f create mode 100644 filelists/write_gate.tb.f create mode 100644 flows/cdc/write_gate.constraints.tcl create mode 100644 flows/eqy/write_gate.equivalence.eqy create mode 100644 flows/openroad/write_gate.config.mk create mode 100644 flows/openroad/write_gate.timing.sdc create mode 100644 flows/sg_dft/write_gate.constraints.tcl create mode 100644 flows/symbiyosys/write_gate.cover.sby create mode 100644 flows/symbiyosys/write_gate.formal.sby create mode 100644 flows/synthesis/write_gate.timing.sdc create mode 100644 flows/vc_lp/write_gate.power.upf create mode 100644 rtl/write_gate.sv create mode 100644 verif/assertions/write_gate_bind.sv create mode 100644 verif/assertions/write_gate_sva.sv create mode 100644 verif/coverage/write_gate_coverage.sv create mode 100644 verif/coverage/write_gate_coverage_bind.sv create mode 100644 verif/coverage/write_gate_integration_coverage.sv create mode 100644 verif/coverage/write_gate_transition_coverage.sv create mode 100644 verif/formal/write_gate_formal.sv create mode 100644 verif/formal/write_gate_integration_formal.sv create mode 100644 verif/mutations/write_gate_inverted_suppress_mutant.sv create mode 100644 verif/properties/write_gate_predicates.svh create mode 100644 verif/tb/write_gate_four_state_tb.sv create mode 100644 verif/tb/write_gate_integration_test_case.sv create mode 100644 verif/tb/write_gate_invalid_width_tb.sv create mode 100644 verif/tb/write_gate_tb.sv create mode 100644 verif/tb/write_gate_test_case.sv diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index c49c310..ceeb206 100644 --- a/.github/workflows/rtl-simulation.yml +++ b/.github/workflows/rtl-simulation.yml @@ -143,12 +143,36 @@ jobs: set -o pipefail make MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" OPENROAD_EXECUTION_MODE=container open-physical 2>&1 | tee ci-artifacts/native-openroad.log + - name: Run representative write-gate OpenROAD physical flow + if: matrix.module == 'write_gate' && matrix.profile == 'width_2' + run: | + set -o pipefail + make MODULE=write_gate PROFILE=width_2 FORCE_FLOW=1 \ + OPENROAD_EXECUTION_MODE=container open-physical \ + 2>&1 | tee ci-artifacts/native-write-gate-openroad.log + openroad_dir=reports/write_gate/width_2/openroad + cp "${openroad_dir}/status.txt" "${openroad_dir}/forced-status.txt" + printf 'SKIP\n' > "${openroad_dir}/status.txt" + + - name: Qualify write-gate functional and structural coverage + if: matrix.module == 'write_gate' && matrix.profile == 'width_2' + run: | + set -o pipefail + make MODULE=write_gate PROFILE=width_2 FORCE_FLOW=1 open-coverage \ + 2>&1 | tee ci-artifacts/native-write-gate-coverage.log + coverage_dir=reports/write_gate/width_2/coverage_qualification + cp "${coverage_dir}/status.txt" "${coverage_dir}/forced-status.txt" + printf 'SKIP\n' > "${coverage_dir}/status.txt" + - name: Generate release evidence manifest env: MODULE_REVISION: ${{ github.sha }} METHODOLOGY_REVISION: ${{ steps.flow-revision.outputs.revision }} run: | set -o pipefail + if [[ "${{ matrix.module }}" == write_gate && "${{ matrix.profile }}" == width_2 ]]; then + export RELEASE_ADDITIONAL_EVIDENCE="reports/write_gate/width_2/coverage_qualification/forced-status.txt reports/write_gate/width_2/openroad/evidence.json reports/write_gate/width_2/openroad/forced-status.txt" + fi make MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" release-manifest release-manifest-validate 2>&1 | tee ci-artifacts/native-release-manifest.log - name: Upload RTL reports @@ -246,9 +270,42 @@ jobs: --env RELEASE_METHODOLOGY_DIRTY=false \ --env RELEASE_EXECUTION_CONTEXT=container \ --volume "${GITHUB_WORKSPACE}:/workspace" \ - "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" FLOW_openroad=disabled clean open-source release-manifest release-manifest-validate \ + "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" FLOW_openroad=disabled clean open-source \ 2>&1 | tee ci-artifacts/container-flow.log + - name: Qualify write-gate functional and structural coverage in container + if: matrix.module == 'write_gate' && matrix.profile == 'width_2' + run: | + set -o pipefail + docker run --rm \ + --user "$(id -u):$(id -g)" \ + --env HOME=/tmp \ + --volume "${GITHUB_WORKSPACE}:/workspace" \ + "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE=write_gate PROFILE=width_2 FORCE_FLOW=1 open-coverage \ + 2>&1 | tee ci-artifacts/container-write-gate-coverage.log + coverage_dir=reports/write_gate/width_2/coverage_qualification + cp "${coverage_dir}/status.txt" "${coverage_dir}/forced-status.txt" + printf 'SKIP\n' > "${coverage_dir}/status.txt" + + - name: Generate release evidence manifest in container + run: | + set -o pipefail + additional_evidence="" + if [[ "${{ matrix.module }}" == write_gate && "${{ matrix.profile }}" == width_2 ]]; then + additional_evidence="reports/write_gate/width_2/coverage_qualification/forced-status.txt" + fi + docker run --rm \ + --user "$(id -u):$(id -g)" \ + --env HOME=/tmp \ + --env MODULE_REVISION="${GITHUB_SHA}" \ + --env METHODOLOGY_REVISION="${{ steps.flow-revision.outputs.revision }}" \ + --env RELEASE_ADDITIONAL_EVIDENCE="${additional_evidence}" \ + --env RELEASE_METHODOLOGY_DIRTY=false \ + --env RELEASE_EXECUTION_CONTEXT=container \ + --volume "${GITHUB_WORKSPACE}:/workspace" \ + "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" release-manifest release-manifest-validate \ + 2>&1 | tee ci-artifacts/container-release-manifest.log + - name: Upload container RTL reports if: always() uses: actions/upload-artifact@v7 diff --git a/README.md b/README.md index 0c0bdc9..f51570e 100644 --- a/README.md +++ b/README.md @@ -18,6 +18,7 @@ repository infrastructure and pinned [`mosaic-flow`](mosaic-flow) methodology. | `level_shifter` | Technology-independent model of a unidirectional voltage-domain crossing | [`docs/level_shifter/`](docs/level_shifter/) | | `isolation_cell` | Parameterizable power-domain isolation and compile-time clamp behavior | [`docs/isolation_cell/`](docs/isolation_cell/) | | `retention_register` | Parameterizable visible state with explicit save and restore behavior | [`docs/retention_register/`](docs/retention_register/) | +| `write_gate` | Parameterizable architectural suppression of per-bit write enables | [`docs/write_gate/`](docs/write_gate/) | The authoritative module list used by local automation and the GitHub Actions matrix is [`config/modules.json`](config/modules.json). Parameterized modules diff --git a/config/coverage-policies/write_gate.json b/config/coverage-policies/write_gate.json new file mode 100644 index 0000000..bfd06b4 --- /dev/null +++ b/config/coverage-policies/write_gate.json @@ -0,0 +1,54 @@ +{ + "schema": "mosaic-coverage-policy-v1", + "scope": { + "include": [ + "rtl/write_gate.sv", + "verif/coverage/write_gate_coverage.sv", + "verif/coverage/write_gate_transition_coverage.sv", + "verif/coverage/write_gate_integration_coverage.sv" + ], + "exclude": [] + }, + "thresholds": { + "line": 100, + "branch": 100, + "toggle": 90, + "user": 100 + }, + "coverpoints": [ + {"name": "truth_00", "minimum_hits": 1}, + {"name": "truth_01", "minimum_hits": 1}, + {"name": "truth_10", "minimum_hits": 1}, + {"name": "truth_11", "minimum_hits": 1}, + {"name": "every_bit_permitted", "minimum_hits": 1}, + {"name": "every_bit_suppressed", "minimum_hits": 1}, + {"name": "zero_suppression_ratio", "minimum_hits": 1}, + {"name": "partial_suppression_ratio", "minimum_hits": 1}, + {"name": "complete_suppression_ratio", "minimum_hits": 1}, + {"name": "partition_observed", "minimum_hits": 1}, + {"name": "mixed_write_decision", "minimum_hits": 1}, + {"name": "transition_00_00", "minimum_hits": 1}, + {"name": "transition_00_01", "minimum_hits": 1}, + {"name": "transition_00_10", "minimum_hits": 1}, + {"name": "transition_00_11", "minimum_hits": 1}, + {"name": "transition_01_00", "minimum_hits": 1}, + {"name": "transition_01_01", "minimum_hits": 1}, + {"name": "transition_01_10", "minimum_hits": 1}, + {"name": "transition_01_11", "minimum_hits": 1}, + {"name": "transition_10_00", "minimum_hits": 1}, + {"name": "transition_10_01", "minimum_hits": 1}, + {"name": "transition_10_10", "minimum_hits": 1}, + {"name": "transition_10_11", "minimum_hits": 1}, + {"name": "transition_11_00", "minimum_hits": 1}, + {"name": "transition_11_01", "minimum_hits": 1}, + {"name": "transition_11_10", "minimum_hits": 1}, + {"name": "transition_11_11", "minimum_hits": 1}, + {"name": "protocol_idle_no_decision", "minimum_hits": 1}, + {"name": "protocol_accepted_permit", "minimum_hits": 1}, + {"name": "protocol_accepted_suppress", "minimum_hits": 1}, + {"name": "register_redundant_suppression", "minimum_hits": 1}, + {"name": "memory_redundant_suppression", "minimum_hits": 1} + ], + "exclusions": [], + "formal": {"required": true} +} diff --git a/config/modules.json b/config/modules.json index 6b0d6d4..7ce29d4 100644 --- a/config/modules.json +++ b/config/modules.json @@ -9,6 +9,7 @@ {"name": "priority_encoder"}, {"name": "level_shifter"}, {"name": "isolation_cell"}, - {"name": "retention_register"} + {"name": "retention_register"}, + {"name": "write_gate"} ] } diff --git a/config/modules/write_gate-flows.mk b/config/modules/write_gate-flows.mk new file mode 100644 index 0000000..60bc76a --- /dev/null +++ b/config/modules/write_gate-flows.mk @@ -0,0 +1,36 @@ +# Required portable checks for the technology-independent write-control leaf. +FLOW_verible_lint := enabled +FLOW_verible_format := enabled +FLOW_slang_elaboration := enabled +FLOW_verilator_lint := enabled +FLOW_yosys_synthesis := enabled +FLOW_symbiyosys_formal := enabled +FLOW_eqy_equivalence := enabled +FLOW_verilator_sim := enabled +FLOW_coverage_qualification := enabled +FLOW_negative_qualification := enabled +FLOW_four_state_qualification := enabled +FLOW_static_intent := enabled + +# Technology, destination timing, domains, scan, and activity belong to the +# first stateful integration that consumes the write enable. +FLOW_openroad := disabled +FLOW_vcs_sim := disabled +FLOW_pyuvm_open_source := disabled +FLOW_pyuvm_commercial := disabled +FLOW_vc_lint := disabled +FLOW_vc_cdc := disabled +FLOW_sg_cdc := disabled +FLOW_sg_dft := disabled +FLOW_vc_lp := disabled +FLOW_synopsys_synthesis := disabled +FLOW_synopsys_primetime := disabled +FLOW_synopsys_primepower := disabled + +FLOW_DEPENDENCIES_eqy_equivalence := yosys_synthesis +FLOW_DEPENDENCIES_coverage_qualification := verilator_sim +FLOW_DEPENDENCIES_negative_qualification := +FLOW_DEPENDENCIES_four_state_qualification := +FLOW_DEPENDENCIES_static_intent := +FLOW_DEPENDENCIES_synopsys_primetime := +FLOW_DEPENDENCIES_synopsys_primepower := diff --git a/config/modules/write_gate.mk b/config/modules/write_gate.mk new file mode 100644 index 0000000..565f804 --- /dev/null +++ b/config/modules/write_gate.mk @@ -0,0 +1,59 @@ +# Write-gate tops and design-owned flow inputs. +export DESIGN_TOP := write_gate +export TB_TOP := $(DESIGN_TOP)_tb +export FORMAL_TOP := $(DESIGN_TOP)_formal +export DUT_INSTANCE := $(TB_TOP)/u_unit/dut + +export FLOW_CONFIG_ROOT := $(MODULE_ROOT)/flows +export RTL_FILELIST := $(call resolve_filelist,rtl.f) +export TB_FILELIST := $(call resolve_filelist,tb.f) +export FORMAL_FILELIST := $(call resolve_filelist,formal.f) +export PROPERTY_FILELIST := $(call resolve_filelist,properties.f) +export ASSERTION_FILELIST := $(call resolve_filelist,assertions.f) +export COVERAGE_FILELIST := $(call resolve_filelist,coverage.f) +export VERILATOR_WAIVER_FILE := $(FLOW_CONFIG_ROOT)/verilator_lint/waivers.vlt +export VERIBLE_WAIVER_FILE := $(FLOW_CONFIG_ROOT)/verible/waivers.txt +export VERIBLE_RULES_FILE := $(FLOW_CONFIG_ROOT)/verible/rules +export VERIBLE_FORMAT_ARGS := --indentation_spaces=4 +export VERIBLE_FORMAT_PATHS := \ + rtl/write_gate.sv \ + verif/properties/write_gate_predicates.svh \ + verif/assertions/write_gate_sva.sv \ + verif/assertions/write_gate_bind.sv \ + verif/coverage/write_gate_coverage.sv \ + verif/coverage/write_gate_transition_coverage.sv \ + verif/coverage/write_gate_integration_coverage.sv \ + verif/coverage/write_gate_coverage_bind.sv \ + verif/formal/write_gate_integration_formal.sv \ + verif/formal/write_gate_formal.sv \ + verif/mutations/write_gate_inverted_suppress_mutant.sv \ + verif/tb/write_gate_test_case.sv \ + verif/tb/write_gate_integration_test_case.sv \ + verif/tb/write_gate_tb.sv \ + verif/tb/write_gate_four_state_tb.sv \ + verif/tb/write_gate_invalid_width_tb.sv +export FORMAL_CONFIG := $(call resolve_flow_config,symbiyosys,formal.sby) +export FORMAL_COVER_CONFIG := $(MODULE_ROOT)/flows/symbiyosys/write_gate.cover.sby +export EQUIVALENCE_CONFIG := $(call resolve_flow_config,eqy,equivalence.eqy) +export COVERAGE_QUALIFICATION_POLICY := $(MODULE_ROOT)/config/coverage-policies/write_gate.json +export COVERAGE_QUALIFICATION_SOURCE := verilator_sim +export SIM_COVERAGE := enabled +export QUALIFICATION_CAMPAIGN_MANIFEST := $(MODULE_ROOT)/config/qualification-campaigns/write_gate.json +export STATIC_INTENT_CONFIG := $(MODULE_ROOT)/config/static-intent/write_gate.json +export OPENROAD_CONFIG := $(call resolve_flow_config,openroad,config.mk) +export SYNTHESIS_CONSTRAINT_FILE := $(call resolve_flow_config,synthesis,timing.sdc) +export ASYNC_SYNTHESIS_CONSTRAINT_FILE := +export OPENROAD_CONSTRAINT_FILE := $(MODULE_ROOT)/flows/openroad/write_gate.timing.sdc +export CDC_CONFIG := $(call resolve_flow_config,cdc,constraints.tcl) +export DFT_CONFIG := $(call resolve_flow_config,sg_dft,constraints.tcl) +export UPF_CONFIG := $(call resolve_flow_config,vc_lp,power.upf) +export CONSTRAINT_DIR := $(FLOW_CONFIG_ROOT)/synthesis + +export REPORT_DIR := $(MODULE_ROOT)/reports/$(MODULE) +export WORK_DIR := $(MODULE_ROOT)/work/$(MODULE) +export OPENROAD_PLATFORM ?= nangate45 +export TECH_SETUP_TCL ?= +export TARGET_LIBRARY ?= +export LINK_LIBRARY ?= +export OPERATING_CONDITION ?= +export ACTIVITY_FILE ?=$(WORK_DIR)/vcs_sim/$(DESIGN_TOP).saif diff --git a/config/parameter-profiles/write_gate.json b/config/parameter-profiles/write_gate.json new file mode 100644 index 0000000..4e97896 --- /dev/null +++ b/config/parameter-profiles/write_gate.json @@ -0,0 +1,53 @@ +{ + "schema": "mosaic-parameter-profiles-v1", + "include": [ + { + "name": "width_1", + "parameters": {"WIDTH": 1}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "negative_qualification", "four_state_qualification", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_2", + "parameters": {"WIDTH": 2}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_4", + "parameters": {"WIDTH": 4}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_8", + "parameters": {"WIDTH": 8}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_16", + "parameters": {"WIDTH": 16}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_32", + "parameters": {"WIDTH": 32}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_64", + "parameters": {"WIDTH": 64}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + }, + { + "name": "width_128", + "parameters": {"WIDTH": 128}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "write_gate", "testbench": "write_gate_tb", "formal": "write_gate_formal"} + } + ] +} diff --git a/config/qualification-campaigns/write_gate.json b/config/qualification-campaigns/write_gate.json new file mode 100644 index 0000000..3871036 --- /dev/null +++ b/config/qualification-campaigns/write_gate.json @@ -0,0 +1,139 @@ +{ + "schema": "mosaic-qualification-campaigns-v1", + "campaigns": { + "negative": { + "inputs": ["rtl/write_gate.sv", "verif/mutations/write_gate_inverted_suppress_mutant.sv", "verif/tb/write_gate_test_case.sv", "verif/tb/write_gate_invalid_width_tb.sv"], + "cases": [ + { + "id": "nominal_unit_regression", + "evidence": "nominal_unit_regression", + "role": "positive_control", + "kind": "simulation_control", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DWRITE_GATE_DISABLE_COVERAGE", "-s", "write_gate_test_case", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/tb/write_gate_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success"} + ] + }, + { + "id": "inverted_suppression_mutation", + "evidence": "inverted_suppression_mutation", + "role": "negative", + "kind": "simulation_mutation", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DWRITE_GATE_DISABLE_COVERAGE", "-s", "write_gate_test_case", "-o", "{case_work_dir}/simulation.vvp", "verif/mutations/write_gate_inverted_suppress_mutant.sv", "verif/tb/write_gate_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "permitted-write mismatch", "failure_class": "assertion"} + ] + }, + { + "id": "invalid_width_elaboration", + "evidence": "invalid_width_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "write_gate_invalid_width_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/tb/write_gate_invalid_width_tb.sv"], "expected": "failure", "diagnostic": "write_gate_width_must_be_greater_than_zero", "failure_class": "elaboration"} + ] + } + ] + }, + "four_state": { + "simulator": "iverilog", + "inputs": ["rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], + "cases": [ + { + "id": "disabled_unknown_write_enable_x", + "evidence": "disabled_unknown_write_enable_x", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_write_enable", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_DISABLE_UNKNOWN_MONITOR", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "WRITE_GATE_UNKNOWN_CONTROL_STIMULUS_REACHED"} + ] + }, + { + "id": "unknown_write_enable_x", + "evidence": "unknown_write_enable_x", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_unknown_write_enable_x", + "injections": [{"control": "i_write_enable", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "write_gate write-enable control is unknown", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_high_impedance_write_enable_z", + "evidence": "disabled_high_impedance_write_enable_z", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_write_enable", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_DISABLE_UNKNOWN_MONITOR", "-DWRITE_GATE_INJECT_Z", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "WRITE_GATE_UNKNOWN_CONTROL_STIMULUS_REACHED"} + ] + }, + { + "id": "high_impedance_write_enable_z", + "evidence": "high_impedance_write_enable_z", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_high_impedance_write_enable_z", + "injections": [{"control": "i_write_enable", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_INJECT_Z", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "write_gate write-enable control is unknown", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_unknown_suppress_x", + "evidence": "disabled_unknown_suppress_x", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_suppress", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_DISABLE_UNKNOWN_MONITOR", "-DWRITE_GATE_INJECT_SUPPRESS", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "WRITE_GATE_UNKNOWN_CONTROL_STIMULUS_REACHED"} + ] + }, + { + "id": "unknown_suppress_x", + "evidence": "unknown_suppress_x", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_unknown_suppress_x", + "injections": [{"control": "i_suppress", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_INJECT_SUPPRESS", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "write_gate suppression control is unknown for a request", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_high_impedance_suppress_z", + "evidence": "disabled_high_impedance_suppress_z", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_suppress", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_DISABLE_UNKNOWN_MONITOR", "-DWRITE_GATE_INJECT_SUPPRESS", "-DWRITE_GATE_INJECT_Z", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "WRITE_GATE_UNKNOWN_CONTROL_STIMULUS_REACHED"} + ] + }, + { + "id": "unknown_suppress_z", + "evidence": "unknown_suppress_z", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_high_impedance_suppress_z", + "injections": [{"control": "i_suppress", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "write_gate_four_state_tb", "-DWRITE_GATE_INJECT_SUPPRESS", "-DWRITE_GATE_INJECT_Z", "-o", "{case_work_dir}/simulation.vvp", "rtl/write_gate.sv", "verif/assertions/write_gate_sva.sv", "verif/tb/write_gate_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "write_gate suppression control is unknown for a request", "failure_class": "unknown_control"} + ] + } + ] + } + } +} diff --git a/config/static-intent/write_gate.json b/config/static-intent/write_gate.json new file mode 100644 index 0000000..da457ec --- /dev/null +++ b/config/static-intent/write_gate.json @@ -0,0 +1,28 @@ +{ + "schema": "mosaic-static-intent-v1", + "sdc": { + "profiles": [ + {"name": "synthesis", "path": "flows/synthesis/write_gate.timing.sdc", "kind": "combinational"}, + {"name": "physical", "path": "flows/openroad/write_gate.timing.sdc", "kind": "combinational"} + ], + "consistency": [ + { + "profiles": ["synthesis", "physical"], + "commands": ["set_input_transition", "set_load", "set_max_delay"] + } + ] + }, + "upf": { + "path": "flows/vc_lp/write_gate.power.upf", + "top": "write_gate", + "mode": "always_on", + "required": { + "power_domains": ["PD_WRITE_GATE"], + "supply_ports": ["VDD", "VSS"], + "supply_nets": ["VDD", "VSS"], + "supply_connections": ["VDD", "VSS"], + "domain_supplies": ["PD_WRITE_GATE"] + }, + "forbidden_strategies": ["isolation", "level_shifting", "retention", "power_switch"] + } +} diff --git a/docs/README.md b/docs/README.md index 1d8f82b..57b3d42 100644 --- a/docs/README.md +++ b/docs/README.md @@ -5,6 +5,7 @@ ## Module documentation - [Parameterizable D flip-flop](dff/README.md) +- [Parameterizable write gate](write_gate/README.md) ## Template documentation diff --git a/docs/write_gate/README.md b/docs/write_gate/README.md new file mode 100644 index 0000000..4516671 --- /dev/null +++ b/docs/write_gate/README.md @@ -0,0 +1,27 @@ +# Write Gate Documentation + +`write_gate` removes architecturally unnecessary write-enable events before +they reach a stateful destination. It is a stateless, combinational control +primitive and never decides whether a particular state update is legal to drop. + +- [Interface specification](interface.md) +- [Project configuration](project-configuration.md) +- [Verification plan](verification-plan.md) +- [Power characterization](power-characterization.md) +- [Release checklist](release-checklist.md) +- [Reviewed waivers](waivers.md) + +Run one qualified configuration from the repository root: + +```sh +make MODULE=write_gate PROFILE=width_2 clean open-source +``` + +The pinned `mosaic-flow` profile validator does not admit +`coverage_qualification` in profile declarations, and OpenROAD remains optional +in the portable profile matrix. CI therefore forces the width-two coverage gate +and a representative `WIDTH=2` OpenROAD run before release-manifest generation. +Each passing forced status is retained alongside the reports, while the +profile-owned status remains `SKIP`. The passing coverage summary is indexed in +the manifest. The forced statuses and OpenROAD evidence are indexed explicitly +as additional evidence in the applicable manifest. diff --git a/docs/write_gate/interface.md b/docs/write_gate/interface.md new file mode 100644 index 0000000..42ede94 --- /dev/null +++ b/docs/write_gate/interface.md @@ -0,0 +1,61 @@ +# Interface Specification + +[Return to the module documentation index](README.md). + +## Overview + +`write_gate` is a zero-latency, per-bit write-control suppressor. It accepts a +write request and an active-high suppression decision, then emits either a +permitted write enable or a suppressed-write indication for each bit. It has no +clock, reset, state, handshake, acknowledgement, or data path. + +## Parameter + +| Parameter | Default | Legal values | Description | +| --- | ---: | --- | --- | +| `WIDTH` | `1` | Integers greater than or equal to `1` | Independently gated write enables | + +An invalid `WIDTH=0` must fail elaboration. + +## Ports + +| Port | Direction | Width | Description | +| --- | --- | ---: | --- | +| `i_write_enable` | Input | `WIDTH` | Original active-high write request | +| `i_suppress` | Input | `WIDTH` | Active-high suppression decision | +| `o_write_enable` | Output | `WIDTH` | Permitted request sent to state | +| `o_write_suppressed` | Output | `WIDTH` | Observation that a requested write was blocked | + +## Behavior + +For each bit `n`: + +```text +o_write_enable[n] = i_write_enable[n] AND NOT i_suppress[n] +o_write_suppressed[n] = i_write_enable[n] AND i_suppress[n] +``` + +| `i_write_enable[n]` | `i_suppress[n]` | `o_write_enable[n]` | `o_write_suppressed[n]` | +|---:|---:|---:|---:| +| 0 | 0 | 0 | 0 | +| 0 | 1 | 0 | 0 | +| 1 | 0 | 1 | 0 | +| 1 | 1 | 0 | 1 | + +The two outputs are mutually exclusive for every bit and their bitwise OR +reproduces a known input request. Unknown or high-impedance `i_write_enable` +is illegal. Unknown or high-impedance `i_suppress` is illegal when its request +bit is asserted. The four-state campaign detects both cases. + +## Integration Contract + +The consumer must prove that each asserted suppression bit is architecturally +legal and aligned with its write request. It must also ensure that the controls +are synchronous and coherent in the destination domain and meet the +destination write-enable timing. This module does not provide data comparison, +transaction cancellation, clock gating, CDC synchronization, retention, +isolation, or protocol responses. + +Suppressing a write is never sufficient evidence of a power benefit. Any power +claim must measure the switching saved in the consuming register, memory, +counter, or write network. diff --git a/docs/write_gate/power-characterization.md b/docs/write_gate/power-characterization.md new file mode 100644 index 0000000..6aae1e9 --- /dev/null +++ b/docs/write_gate/power-characterization.md @@ -0,0 +1,42 @@ +# Power Characterization + +[Return to the module documentation index](README.md). + +## Portable Activity Evidence + +The open-source regression measures activity at representative stateful +destinations rather than relying only on `o_write_enable` toggles. It compares +an ungated reference with gated register and memory models and records: + +- Original write events accepted by the reference destination +- Write events accepted by the gated destination +- Architectural state-bit transitions in both destinations +- State equivalence after every accepted transaction + +Stimulus includes no suppression, partial suppression, complete suppression, +short intervals, long suppression intervals, random masks, every supported +width, and both register and memory destinations. The regression fails unless +gated destination write events decrease while architectural state transitions +remain equal. Results use the `WRITE_GATE_ACTIVITY` prefix in the Verilator +simulation report. + +These event counts demonstrate useful suppression and validate the activity +model. They are not a cell-library power estimate and must not be reported as +energy savings. + +## Integration Signoff + +PrimePower signoff remains mandatory in the first consuming integration that +contains the actual register file, memory macro, counter, or write network. The +integration must use annotated activity for an equivalent ungated baseline and +the gated design under the same workload. Reports must separate write-gate +logic, write-enable distribution, destination internal power, suppression +control generation, leakage, and total power. + +PrimeTime must verify the request-to-write-enable, +suppression-to-write-enable, and suppressed-indication paths against the +destination setup decision. CDC, RDC, DFT, and VC LP must use the consuming +clock, reset, test, and power-domain context. Until those reports exist, their +status is reviewed `SKIP` or `NOT_RUN` at this technology-independent leaf and +does not block its portable release. The reports remain mandatory before the +consumer can claim integration signoff or technology-specific power savings. diff --git a/docs/write_gate/project-configuration.md b/docs/write_gate/project-configuration.md new file mode 100644 index 0000000..574a251 --- /dev/null +++ b/docs/write_gate/project-configuration.md @@ -0,0 +1,45 @@ +# Project Configuration + +[Return to the module documentation index](README.md). + +`config/modules/write_gate.mk` owns the selected tops, layered file lists, +flow inputs, and report roots. `config/modules/write_gate-flows.mk` enables +the portable lint, elaboration, synthesis, formal, equivalence, simulation, +qualification, and static-intent checks. + +The qualified widths are `1, 2, 4, 8, 16, 32, 64, and 128`, declared in +`config/parameter-profiles/write_gate.json`. Width one also runs the +invalid-parameter, mutation, and four-state campaigns because those controls +are width independent. + +`PROPERTY_FILELIST`, `ASSERTION_FILELIST`, and `COVERAGE_FILELIST` keep shared +predicates, checking wrappers, and coverage wrappers separate. The normal +testbench binds the combinational assertion and coverage wrappers and +instantiates transition and integration coverage monitors. The formal harness +instantiates the same combinational wrappers and an integration proof that +compares gated next state with an ungated reference. + +The leaf remains technology independent. A representative `WIDTH=2` OpenROAD +run checks that the combinational leaf can be synthesized, placed, routed, and +evaluated against its module-owned constraints with the Nangate45 platform. +Commercial lint, CDC, DFT, low-power, synthesis, timing, and power signoff still +require a target library and the stateful destination that receives the gated +control. These integration deferrals are not standalone signoff waivers, and +the representative OpenROAD run is not destination-level signoff. + +Both SDC files declare matching input transition, output load, complete +input-to-output delay, and request-to-permit, suppression-to-permit, and +control-to-observation path budgets. The static-intent policy validates their +consistency and a single always-on UPF domain without claiming physical timing +closure. + +The pinned flow cannot select coverage from a parameter-profile manifest, and +OpenROAD remains optional in the portable profile matrix. The GitHub workflow +therefore executes width-two coverage and the representative `WIDTH=2` +OpenROAD run with `FORCE_FLOW=1` before generating the native release manifest. +A failure remains fatal and each passing forced status is retained as +`forced-status.txt`. Profile-owned statuses are restored to `SKIP` so manifest +validation remains consistent with the pinned profile schema. The coverage +summary is still indexed as release evidence, while OpenROAD evidence is +indexed explicitly as additional native evidence together with both forced +statuses. The container manifest indexes its forced coverage status. diff --git a/docs/write_gate/release-checklist.md b/docs/write_gate/release-checklist.md new file mode 100644 index 0000000..040b19e --- /dev/null +++ b/docs/write_gate/release-checklist.md @@ -0,0 +1,249 @@ +# Write Gate Release Checklist + +Use this checklist for every supported module configuration. A passing portable +gate alone is not sufficient ASIC release evidence. + +## Identity and scope + +- [x] The module name, repository name, top-level names, and Docker labels agree. + _The registry, RTL top, testbench top, formal top, filelists, flow inputs, + reports, and work paths consistently use `write_gate` in `mosaic-common`._ +- [x] Supported parameter values and configurations are listed. + _`WIDTH >= 1` is legal. The qualified matrix covers widths 1, 2, 4, 8, 16, + 32, 64, and 128, and `WIDTH=0` is rejected during elaboration._ +- [x] Unsupported modes and external assumptions are explicit. + _The leaf does not compare data, cancel transactions, acknowledge protocols, + synchronize crossings, store state, or provide clock gating, isolation, or + retention. Integration owns suppression legality and control alignment._ +- [x] The `mosaic-flow` gitlink points to a qualified published revision. + _The gitlink is pinned to revision `0bd222f`, tag `MF20260910V1`, with flow + version `0.8.0`._ +- [x] The resolved flow policy has been captured with `make flow-config-check`. + _The portable policy enables lint, formatting, elaboration, generic + synthesis, formal, equivalence, simulation, and static-intent checks._ + +## Interface and architecture + +- [x] [Interface specification](interface.md) matches the RTL. +- [x] Every clock and reset has documented polarity and timing behavior. + _The module is combinational and has no clock or reset._ +- [x] Latency, throughput, handshakes, backpressure, and errors are documented. + _Latency is zero cycles. There is no handshake, backpressure, acknowledgement, + or error interface._ +- [x] Disabled, reset, test, and low-power behavior are documented. + _An inactive write request produces inactive outputs. Reset and test behavior + belong to the stateful destination. Write suppression is not UPF isolation._ +- [x] Integration assumptions and protocol dependencies are reviewed. + _The consumer must prove that each suppressed write is architecturally + redundant, aligned with its data, and accepted consistently by its protocol._ + +## RTL quality + +- [x] Verible style lint records `PASS` or an approved policy `SKIP`. +- [x] Verible formatting records the expected status. + _All module-owned SystemVerilog and property sources use four-space + indentation._ +- [x] Slang elaboration records the expected status. +- [x] Verilator lint records the expected status. +- [x] Yosys generic synthesis records the expected status. + _The synthesized leaf contains only combinational logic._ +- [x] No unresolved warning is hidden outside the reviewed waiver files. + _The portable gate passes without a warning waiver._ + +## Functional verification + +- [x] The [verification plan](verification-plan.md) maps every requirement to a + test, assertion, formal property, or reviewed combination. +- [x] All supported parameter configurations have evidence. + _Native and container regressions cover all eight declared widths._ +- [x] Positive, negative, reset, error, and boundary tests pass. + _Truth-table, one-hot, alternating, random, long-idle, long-suppression, + mutation, invalid-width, and X/Z campaigns pass. Reset is not applicable._ +- [x] Assertions run in simulation and reach meaningful antecedents. + _Bound assertions check the equations, output exclusivity, request + partitioning, and unknown controls. Required coverpoints have observed hits._ +- [x] Formal assumptions are reviewed for overconstraint. + _The leaf proof has no assumptions. The integration proof assumes only that a + suppressed requested bit writes the value already held by the destination._ +- [x] Formal proofs pass at justified depth or by complete proof. + _The combinational contract and one-step state-equivalence proof complete by + induction for the qualified widths._ +- [x] RTL-to-Yosys-netlist equivalence passes. +- [x] Functional and code coverage goals are met or deviations are approved. + _Width-two qualification reaches 100 percent line, branch, and user coverage, + 98.913 percent toggle coverage, all 32 required named points, and formal + cover reachability. No exclusion is used._ + +## Constraints and static checks + +- [x] Synthesis and physical clocks agree unless a difference is documented. + _Both constraint sets describe a combinational block and intentionally create + no clock._ +- [x] Input, output, uncertainty, exception, and asynchronous paths are reviewed. + _Both SDC files apply matching input transition, output load, complete + input-to-output delay, and path-specific control-to-output budgets. No clock + uncertainty, false path, multicycle path, or asynchronous exception applies._ +- [x] CDC and reset-domain intent covers every domain and crossing. + _The leaf contains no domain or reset crossing. The consumer must present + coherent write and suppression controls in the destination domain._ +- [x] CDC violations are resolved or narrowly waived. + _CDC and RDC are policy `SKIP` at this combinational leaf. They remain required + in a consuming design and are not represented as standalone `PASS` results._ +- [x] DFT test modes, controllability, observability, and exclusions are reviewed. + _The leaf has no state or test mode. Integration must constrain suppression + transparently so it cannot block destination controllability._ +- [x] UPF power domains, states, isolation, retention, and supplies match the + architecture. + _Portable static intent declares one always-on domain and forbids isolation, + level-shifting, retention, and power-switch strategies at this leaf._ +- [x] VC Lint, selected CDC, SpyGlass DFT, and VC LP adapters are qualified for + the installed release and all expected statuses pass. + _Their expected standalone status is policy `SKIP` because the checks require + destination clock, reset, test, power-state, and library context. The status + is recorded as `SKIP` or `NOT_RUN`, never `PASS`._ + +## Synthesis, timing, and power + +- [x] Design Compiler completes with the intended libraries and operating corner. + _Policy `SKIP` for the technology-independent leaf. Mapped synthesis becomes + mandatory in the first consuming implementation._ +- [x] Area, QoR, and synthesis timing reports are reviewed. + _Yosys generic synthesis passes for every width. The representative + `WIDTH=2` OpenROAD run provides preliminary cell and physical metrics._ +- [x] PrimeTime reports no release-blocking setup or hold violation. + _Policy `SKIP` until a destination, target library, and operating corners are + selected. OpenROAD reports no setup or hold violation for the preliminary + combinational implementation._ +- [x] Unconstrained paths and constraint coverage are reviewed. + _All input-to-output combinations receive a maximum delay, with explicit + write-request, suppression, and observation path budgets._ +- [x] PrimePower uses representative SAIF activity. + _Policy `SKIP` at leaf level. PrimePower with annotated destination activity + remains mandatory before claiming technology-specific energy savings._ +- [x] SAIF hierarchy and activity annotation coverage are reviewed. + _The portable regression records destination write events and architectural + state transitions. These counts validate stimulus but are not SAIF or power._ +- [x] Power, performance, and area results meet the module targets. + _The portable target is correct suppression with reduced destination write + events and unchanged architectural state. Numeric PPA targets are deferred._ +- [x] PDK, library, tool, constraint, and corner identities are recorded. + _OpenROAD evidence records the immutable ORFS image, Nangate45 platform, + module constraints, artifacts, and hashes. No foundry signoff is claimed._ + +## Physical implementation + +- [x] OpenROAD or the selected implementation flow uses the intended platform. + _The representative `WIDTH=2` diagnostic uses Nangate45 and the pinned ORFS + container image._ +- [x] Floorplan, utilization, aspect ratio, and margins are justified. + _The small combinational leaf uses a deterministic 60 by 60 micrometer die + and a 50 by 50 micrometer core because the default PDN pitch is larger than + the leaf logic._ +- [x] Placement, clocking, routing, timing, DRC, and LVS evidence is retained when + physical implementation belongs to this module's release scope. + _The exploratory run retains DEF, GDS, ODB, SDC, and netlist artifacts and + reports zero setup, hold, slew, fanout, capacitance, and routing violations. + Foundry DRC and LVS remain outside the portable leaf scope._ +- [x] Preliminary open-source physical results are not labeled as commercial + signoff evidence. + _The OpenROAD result is documented as a diagnostic, not destination-level or + foundry signoff._ + +## Waivers + +- [x] Every accepted waiver is recorded in [Reviewed waivers](waivers.md). + _No waiver is currently accepted._ +- [x] Each waiver identifies the tool, rule, object, justification, owner, + reviewer, date, and removal condition. + _Not applicable while the waiver register is empty._ +- [x] Generated waiver drafts are not treated as approved policy. +- [x] Expired waivers have been removed or re-reviewed. + _There are no write-gate waivers to expire._ + +## Reproducibility and evidence + +- [x] Native `make clean open-source` passes. + _`make MODULE=write_gate clean all-profiles PROFILE_JOBS=4` passes all eight + supported widths._ +- [x] The pinned Docker image builds and its portable gate passes. + _The CI-equivalent container passes all eight profiles, width-one + qualification campaigns, width-two coverage, and manifest validation._ +- [ ] GitHub Actions passes using the recorded gitlink revision. + _Local `actionlint` and the CI-equivalent native commands pass. This item + requires a committed revision and completed native and container workflow + jobs for that exact revision._ +- [x] Commercial gates pass in the authorized local or self-hosted environment. + _Commercial gates are policy `SKIP` for portable leaf qualification. They are + mandatory in the consuming integration and cannot be inferred from this item._ +- [x] Reports identify module revision, methodology revision, tool versions, + constraints, technology, date, and configuration. + _Dirty-tree diagnostic native and container manifests validate the schema, + record revisions and dirty state, and hash portable, coverage, static-intent, + and applicable OpenROAD evidence._ +- [ ] CI or release storage retains logs and required databases. + _The workflow is configured to upload native and container reports, work + databases, and diagnostics with `if-no-files-found: error`. Artifact IDs and + retention dates can be recorded only after the committed workflow completes._ +- [x] No generated work database, credential, license, or proprietary library is + committed to Git. + +## Consuming-integration handoff + +- [x] The CDC and RDC disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the leaf has no clock, reset, state, or domain crossing. + The consumer must analyze the destination clock and reset domains plus the + paths that generate and align both controls._ +- [x] The DFT disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the leaf has no state, scan element, or test mode. The + consumer must define the transparent suppression value and prove that write + gating does not prevent destination controllability or observability._ +- [x] The VC LP disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: portable static intent validates one always-on leaf domain + and the absence of isolation, retention, level shifting, and power switches. + The consumer must analyze its actual supplies, power states, and sequencing._ +- [x] The PrimeTime disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the leaf has no technology-bound destination setup check. + OpenROAD closes the preliminary combinational paths, while the consumer must + close request and suppression timing with its selected libraries and corners._ +- [x] The PrimePower disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the regression proves fewer destination write events with + equal architectural state but does not claim energy savings. The consumer + must compare mapped gated and ungated designs using representative SAIF._ +- [x] The physical-signoff disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the Nangate45 OpenROAD implementation is a passing + diagnostic, not foundry signoff. The consumer must close extraction, DRC, + LVS, timing, and power with its destination and target PDK._ + +These reviewed skips close the portable leaf checklist only. The transferred +requirements remain mandatory before a register file, memory, counter, buffer, +or other stateful consumer can claim integration signoff or silicon power +savings. + +## Known methodology limitation + +The pinned `mosaic-flow` profile schema does not yet accept +`coverage_qualification` in a parameter-profile flow list. CI therefore forces +width-two coverage before manifest generation, stores `forced-status.txt`, +restores the profile-owned status to `SKIP`, and indexes the passing evidence. +This enforced handoff is validated and is not a write-gate release criterion. + +## Final commands + +```sh +git submodule status +make MODULE=write_gate PROFILE=width_2 flow-config-check +make MODULE=write_gate clean all-profiles PROFILE_JOBS=4 +make MODULE=write_gate PROFILE=width_2 FORCE_FLOW=1 open-coverage +make MODULE=write_gate PROFILE=width_2 FORCE_FLOW=1 \ + OPENROAD_EXECUTION_MODE=container open-physical +``` + +Run commercial commands only in the licensed consuming environment after the +destination, libraries, corners, activity, test intent, and power intent are +available. + +## Approval record + +Record the release identifier, reviewed Git revisions, supported configuration, +evidence location, approvers, and approval date in the project's normal release +system. Do not infer approval only from `PASS` files in a local working tree. diff --git a/docs/write_gate/verification-plan.md b/docs/write_gate/verification-plan.md new file mode 100644 index 0000000..07ee78b --- /dev/null +++ b/docs/write_gate/verification-plan.md @@ -0,0 +1,39 @@ +# Verification Plan + +[Return to the module documentation index](README.md). + +| Requirement | Evidence | +| --- | --- | +| Unsuppressed requested writes propagate | Directed truth table, lane tests, random simulation, assertions, and complete formal proof | +| Suppressed requested writes are blocked and observed | Directed intervals, register and memory destination models, assertions, and formal proof | +| Outputs partition every known request | Unit checks, bound assertion, formal proof, native coverpoint, and formal cover | +| Lanes operate independently | One-hot, alternating, mixed, and random vectors across all qualified widths | +| Unknown controls are detected | Icarus X/Z campaign for request and requested suppression controls | +| Invalid width is rejected | Icarus elaboration-negative campaign for `WIDTH=0` | +| A suppression preserves destination state | Gated register and memory models compared with ungated references under an explicit redundant-write contract | +| Integration suppression is architecturally legal | Simulation checks and formal assumptions require suppressed data to equal the prior destination state | +| Gated and ungated next state are equivalent | Complete formal proof for unconstrained state, data, request, and timing-safe suppression controls | +| Destination write activity is reduced | Register and memory write-event counters compare the ungated baseline with the gated destination | +| RTL remains combinational | Verilator lint, Yosys synthesis, formal proof, and EQY equivalence | + +The unit regression exhausts all scalar truth-table classes through all-zero and +all-one vectors, every source-to-destination control transition, every lane, +alternating patterns, long idle and suppressed periods, and back-to-back random +traffic. The integration regression uses both a clocked register bank and a +four-word byte or lane writable memory. Each gated destination is compared with +an ungated reference that receives every original write. + +The leaf formal proof has unconstrained symbolic controls and no assumptions. +The integration proof assumes only that a suppressed requested bit writes the +value already held by the destination, then proves gated and ungated next-state +equivalence. Both proofs are complete at depth one. Formal cover establishes +reachability of all truth states, all-bit decisions, zero, partial, and complete +suppression ratios, partitioning, and mixed decisions when `WIDTH > 1`. + +The width-two qualification enforces 100 percent line coverage, 100 percent +branch coverage, at least 90 percent toggle coverage, 100 percent user coverage, +32 named functional coverpoints, and a passing formal cover run. Named points +cover every truth state, all-bit permit and suppression, suppression ratios, +all 16 scalar control transitions, destination type, redundant-value reason, +and accepted or idle protocol decisions. Widths one and 128 provide the minimum +and maximum width evidence in the profile matrix. diff --git a/docs/write_gate/waivers.md b/docs/write_gate/waivers.md new file mode 100644 index 0000000..2763b62 --- /dev/null +++ b/docs/write_gate/waivers.md @@ -0,0 +1,15 @@ +# Reviewed Waivers + +[Return to the module documentation index](README.md). + +No waiver is currently approved for `write_gate`. + +Commercial CDC, RDC, DFT, VC LP, PrimeTime, and PrimePower results are deferred +to the first stateful consuming integration. They are reported as `NOT_RUN` or +`SKIP`, never as passing standalone results, and are therefore not waivers from +the integration release criteria. These reviewed skips close only the portable +leaf release scope. + +Foundry physical signoff is deferred under the same rule. The passing Nangate45 +OpenROAD implementation is diagnostic evidence and must not be represented as +foundry DRC, LVS, extraction, timing, or power signoff. diff --git a/filelists/write_gate.assertions.f b/filelists/write_gate.assertions.f new file mode 100644 index 0000000..e2a12dc --- /dev/null +++ b/filelists/write_gate.assertions.f @@ -0,0 +1,2 @@ +verif/assertions/write_gate_sva.sv +verif/assertions/write_gate_bind.sv diff --git a/filelists/write_gate.coverage.f b/filelists/write_gate.coverage.f new file mode 100644 index 0000000..7802420 --- /dev/null +++ b/filelists/write_gate.coverage.f @@ -0,0 +1,4 @@ +verif/coverage/write_gate_coverage.sv +verif/coverage/write_gate_transition_coverage.sv +verif/coverage/write_gate_integration_coverage.sv +verif/coverage/write_gate_coverage_bind.sv diff --git a/filelists/write_gate.formal.f b/filelists/write_gate.formal.f new file mode 100644 index 0000000..088b04b --- /dev/null +++ b/filelists/write_gate.formal.f @@ -0,0 +1,4 @@ +-f filelists/write_gate.rtl.f ++incdir+verif/properties +verif/formal/write_gate_integration_formal.sv +verif/formal/write_gate_formal.sv diff --git a/filelists/write_gate.properties.f b/filelists/write_gate.properties.f new file mode 100644 index 0000000..2dfc6d9 --- /dev/null +++ b/filelists/write_gate.properties.f @@ -0,0 +1 @@ ++incdir+verif/properties diff --git a/filelists/write_gate.rtl.f b/filelists/write_gate.rtl.f new file mode 100644 index 0000000..d679c21 --- /dev/null +++ b/filelists/write_gate.rtl.f @@ -0,0 +1,2 @@ ++incdir+rtl +rtl/write_gate.sv diff --git a/filelists/write_gate.tb.f b/filelists/write_gate.tb.f new file mode 100644 index 0000000..22e7b05 --- /dev/null +++ b/filelists/write_gate.tb.f @@ -0,0 +1,5 @@ +-f filelists/write_gate.rtl.f ++incdir+verif +verif/tb/write_gate_test_case.sv +verif/tb/write_gate_integration_test_case.sv +verif/tb/write_gate_tb.sv diff --git a/flows/cdc/write_gate.constraints.tcl b/flows/cdc/write_gate.constraints.tcl new file mode 100644 index 0000000..00578bc --- /dev/null +++ b/flows/cdc/write_gate.constraints.tcl @@ -0,0 +1,2 @@ +# write_gate has no clock, reset, state, or synchronization element. CDC is an +# integration check: controls must be coherent in the destination clock domain. diff --git a/flows/eqy/write_gate.equivalence.eqy b/flows/eqy/write_gate.equivalence.eqy new file mode 100644 index 0000000..76ec785 --- /dev/null +++ b/flows/eqy/write_gate.equivalence.eqy @@ -0,0 +1,11 @@ +[gold] +read_verilog -sv rtl/write_gate.sv +prep -top write_gate + +[gate] +read_verilog work/write_gate/yosys_synthesis/write_gate_netlist.v +prep -top write_gate + +[strategy sat] +use sat +depth 1 diff --git a/flows/openroad/write_gate.config.mk b/flows/openroad/write_gate.config.mk new file mode 100644 index 0000000..05f8e63 --- /dev/null +++ b/flows/openroad/write_gate.config.mk @@ -0,0 +1,11 @@ +# Exploratory physical setup for the representative WIDTH=2 write gate. +export DESIGN_NAME = write_gate +export PLATFORM = $(OPENROAD_PLATFORM) +export VERILOG_FILES = $(REPO_ROOT)/rtl/write_gate.sv +export VERILOG_TOP_PARAMS = WIDTH 2 +export SDC_FILE = $(SYNTHESIS_CONSTRAINT_FILE) + +# The leaf is smaller than the default Nangate45 PDN strap pitch. +export DIE_AREA = 0 0 60 60 +export CORE_AREA = 5 5 55 55 +export SKIP_CTS_REPAIR_TIMING = 1 diff --git a/flows/openroad/write_gate.timing.sdc b/flows/openroad/write_gate.timing.sdc new file mode 100644 index 0000000..adf0cb7 --- /dev/null +++ b/flows/openroad/write_gate.timing.sdc @@ -0,0 +1,14 @@ +# Match the synthesis interface assumptions for exploratory physical runs. +set_input_transition 0.100 [all_inputs] +set_load 0.010 [all_outputs] + +set_max_delay 10.000 -from [all_inputs] -to [all_outputs] +set_max_delay 10.000 \ + -from [get_ports i_write_enable*] \ + -to [get_ports o_write_enable*] +set_max_delay 10.000 \ + -from [get_ports i_suppress*] \ + -to [get_ports o_write_enable*] +set_max_delay 10.000 \ + -from [get_ports {i_write_enable* i_suppress*}] \ + -to [get_ports o_write_suppressed*] diff --git a/flows/sg_dft/write_gate.constraints.tcl b/flows/sg_dft/write_gate.constraints.tcl new file mode 100644 index 0000000..9d07af7 --- /dev/null +++ b/flows/sg_dft/write_gate.constraints.tcl @@ -0,0 +1,2 @@ +# write_gate has no state, scan chain, test clock, reset, or test-mode control. +# Destination scan controllability is owned by the integrating hierarchy. diff --git a/flows/symbiyosys/write_gate.cover.sby b/flows/symbiyosys/write_gate.cover.sby new file mode 100644 index 0000000..c43ff33 --- /dev/null +++ b/flows/symbiyosys/write_gate.cover.sby @@ -0,0 +1,18 @@ +[options] +mode cover +depth 1 + +[engines] +smtbmc bitwuzla + +[script] +read -formal -D MOSAIC_FORMAL -D MOSAIC_YOSYS_FORMAL -D FORMAL_COVERAGE -sv write_gate.sv write_gate_coverage.sv write_gate_coverage_bind.sv write_gate_integration_formal.sv write_gate_formal.sv +prep -top write_gate_formal + +[files] +rtl/write_gate.sv +verif/properties/write_gate_predicates.svh +verif/coverage/write_gate_coverage.sv +verif/coverage/write_gate_coverage_bind.sv +verif/formal/write_gate_integration_formal.sv +verif/formal/write_gate_formal.sv diff --git a/flows/symbiyosys/write_gate.formal.sby b/flows/symbiyosys/write_gate.formal.sby new file mode 100644 index 0000000..55a49f1 --- /dev/null +++ b/flows/symbiyosys/write_gate.formal.sby @@ -0,0 +1,18 @@ +[options] +mode prove +depth 1 + +[engines] +smtbmc bitwuzla + +[script] +read -formal -D MOSAIC_FORMAL -D MOSAIC_YOSYS_FORMAL -D FORMAL_ASSERTIONS -sv write_gate.sv write_gate_sva.sv write_gate_bind.sv write_gate_integration_formal.sv write_gate_formal.sv +prep -top write_gate_formal + +[files] +rtl/write_gate.sv +verif/properties/write_gate_predicates.svh +verif/assertions/write_gate_sva.sv +verif/assertions/write_gate_bind.sv +verif/formal/write_gate_integration_formal.sv +verif/formal/write_gate_formal.sv diff --git a/flows/synthesis/write_gate.timing.sdc b/flows/synthesis/write_gate.timing.sdc new file mode 100644 index 0000000..7222dd9 --- /dev/null +++ b/flows/synthesis/write_gate.timing.sdc @@ -0,0 +1,17 @@ +# Technology-independent interface assumptions for the combinational leaf. +set_input_transition 0.100 [all_inputs] +set_load 0.010 [all_outputs] + +# Preserve a complete interface budget for portable static-intent validation. +set_max_delay 10.000 -from [all_inputs] -to [all_outputs] + +# Keep each architecturally relevant control path visible in timing reports. +set_max_delay 10.000 \ + -from [get_ports i_write_enable*] \ + -to [get_ports o_write_enable*] +set_max_delay 10.000 \ + -from [get_ports i_suppress*] \ + -to [get_ports o_write_enable*] +set_max_delay 10.000 \ + -from [get_ports {i_write_enable* i_suppress*}] \ + -to [get_ports o_write_suppressed*] diff --git a/flows/vc_lp/write_gate.power.upf b/flows/vc_lp/write_gate.power.upf new file mode 100644 index 0000000..9b5e6ce --- /dev/null +++ b/flows/vc_lp/write_gate.power.upf @@ -0,0 +1,13 @@ +# Baseline always-on domain for this technology-independent combinational leaf. +set_design_top write_gate +create_power_domain PD_WRITE_GATE -include_scope +create_supply_port VDD -domain PD_WRITE_GATE +create_supply_port VSS -domain PD_WRITE_GATE +create_supply_net VDD -domain PD_WRITE_GATE +create_supply_net VSS -domain PD_WRITE_GATE +connect_supply_net VDD -ports VDD +connect_supply_net VSS -ports VSS +set_domain_supply_net PD_WRITE_GATE -primary_power_net VDD -primary_ground_net VSS + +# Isolation, retention, level shifting, power switching, and their signoff +# belong to the first integrating hierarchy that implements those strategies. diff --git a/rtl/write_gate.sv b/rtl/write_gate.sv new file mode 100644 index 0000000..a840a63 --- /dev/null +++ b/rtl/write_gate.sv @@ -0,0 +1,24 @@ +/// Parameterizable architectural write-enable suppressor. +/// +/// The integration must assert i_suppress only when dropping the corresponding +/// state update is architecturally legal. This module does not inspect data or +/// create protocol acknowledgements. +module write_gate #( + parameter int unsigned WIDTH = 1 +) ( + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + output logic [WIDTH-1:0] o_write_enable, + output logic [WIDTH-1:0] o_write_suppressed +); + + generate + if (WIDTH < 1) begin : g_invalid_width + write_gate_width_must_be_greater_than_zero invalid_width (); + end + endgenerate + + assign o_write_enable = i_write_enable & ~i_suppress; + assign o_write_suppressed = i_write_enable & i_suppress; + +endmodule diff --git a/scripts/verible-format b/scripts/verible-format index 6069271..006f65a 100755 --- a/scripts/verible-format +++ b/scripts/verible-format @@ -1,12 +1,14 @@ #!/usr/bin/env bash set -euo pipefail -# Counter, reset synchronizer, lane mask, priority encoder, level shifter, isolation cell, and retention register sources use four-space indentation. +# Counter, reset synchronizer, lane mask, priority encoder, level shifter, +# isolation cell, retention register, and write gate sources use four-space +# indentation. # Other modules retain Verible's default so existing formatting remains unchanged. args=("$@") source_file="${args[${#args[@]}-1]}" -if [[ "${source_file}" == *counter*.sv || "${source_file}" == *reset_synchronizer*.sv || "${source_file}" == *lane_mask*.sv || "${source_file}" == *priority_encoder*.sv || "${source_file}" == *level_shifter*.sv || "${source_file}" == *isolation_cell*.sv || "${source_file}" == *retention_register*.sv ]]; then +if [[ "${source_file}" == *counter*.sv || "${source_file}" == *reset_synchronizer*.sv || "${source_file}" == *lane_mask*.sv || "${source_file}" == *priority_encoder*.sv || "${source_file}" == *level_shifter*.sv || "${source_file}" == *isolation_cell*.sv || "${source_file}" == *retention_register*.sv || "${source_file}" == *write_gate*.sv || "${source_file}" == *write_gate*.svh ]]; then args=(--indentation_spaces=4 "${args[@]}") fi diff --git a/verif/assertions/write_gate_bind.sv b/verif/assertions/write_gate_bind.sv new file mode 100644 index 0000000..543b5ce --- /dev/null +++ b/verif/assertions/write_gate_bind.sv @@ -0,0 +1,17 @@ +/// Stable boundary used to bind write-gate assertions to every DUT instance. +module write_gate_bind #( + parameter int unsigned WIDTH = 1 +) ( + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + input logic [WIDTH-1:0] o_write_enable, + input logic [WIDTH-1:0] o_write_suppressed +); + + write_gate_sva #(.WIDTH(WIDTH)) i_write_gate_sva (.*); + +endmodule + +`ifndef MOSAIC_FORMAL +bind write_gate write_gate_bind #(.WIDTH(WIDTH)) i_write_gate_bind (.*); +`endif diff --git a/verif/assertions/write_gate_sva.sv b/verif/assertions/write_gate_sva.sv new file mode 100644 index 0000000..9b8e6b0 --- /dev/null +++ b/verif/assertions/write_gate_sva.sv @@ -0,0 +1,44 @@ +/// Combinational write-gate checks shared by simulation and formal proof. +module write_gate_sva #( + parameter int unsigned WIDTH = 1 +) ( + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + input logic [WIDTH-1:0] o_write_enable, + input logic [WIDTH-1:0] o_write_suppressed +); + +`ifdef MOSAIC_YOSYS_FORMAL + // Formal proves the two-state equation. Four-state campaigns qualify X/Z + // controls with the same wrapper in an event-driven simulator. + always_comb begin + assert (o_write_enable == (i_write_enable & ~i_suppress)); + assert (o_write_suppressed == (i_write_enable & i_suppress)); + assert ((o_write_enable & o_write_suppressed) == '0); + assert ((o_write_enable | o_write_suppressed) == i_write_enable); + end +`else + `include "write_gate_predicates.svh" + + always_comb begin + if (write_gate_controls_known_f(i_write_enable, i_suppress)) begin + assert (o_write_enable == write_gate_permitted_f(i_write_enable, i_suppress)) + else $fatal(1, "write_gate permitted-write equation failed"); + assert (o_write_suppressed == write_gate_suppressed_f(i_write_enable, i_suppress)) + else $fatal(1, "write_gate suppressed-write equation failed"); + assert (write_gate_outputs_partition_f( + i_write_enable, o_write_enable, o_write_suppressed + )) + else $fatal(1, "write_gate outputs do not partition requests"); + end + +`ifndef WRITE_GATE_DISABLE_UNKNOWN_MONITOR + assert (!$isunknown(i_write_enable)) + else $fatal(1, "write_gate write-enable control is unknown"); + assert (!$isunknown(i_write_enable & i_suppress)) + else $fatal(1, "write_gate suppression control is unknown for a request"); +`endif + end +`endif + +endmodule diff --git a/verif/coverage/write_gate_coverage.sv b/verif/coverage/write_gate_coverage.sv new file mode 100644 index 0000000..21c72d8 --- /dev/null +++ b/verif/coverage/write_gate_coverage.sv @@ -0,0 +1,61 @@ +/// Functional coverage for the write-gate combinational contract. +module write_gate_coverage #( + parameter int unsigned WIDTH = 1 +) ( + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + input logic [WIDTH-1:0] o_write_enable, + input logic [WIDTH-1:0] o_write_suppressed +); + +`ifdef MOSAIC_YOSYS_FORMAL + always_comb begin + truth_00 : cover (i_write_enable == '0 && i_suppress == '0); + truth_01 : cover (i_write_enable == '0 && i_suppress == '1); + truth_10 : cover (i_write_enable == '1 && i_suppress == '0); + truth_11 : cover (i_write_enable == '1 && i_suppress == '1); + every_bit_permitted : cover (o_write_enable == '1); + every_bit_suppressed : cover (o_write_suppressed == '1); + zero_suppression_ratio : cover (i_write_enable != '0 && o_write_suppressed == '0); + complete_suppression_ratio : + cover (i_write_enable != '0 && o_write_suppressed == i_write_enable); + partition_observed : + cover ( + (o_write_enable & o_write_suppressed) == '0 && + (o_write_enable | o_write_suppressed) == i_write_enable + ); + end + + if (WIDTH > 1) begin : g_mixed_write_decision + always_comb begin + mixed_write_decision : cover (o_write_enable != '0 && o_write_suppressed != '0); + partial_suppression_ratio : cover (o_write_suppressed != '0 && o_write_enable != '0); + end + end +`else + always_comb begin + truth_00 : cover (i_write_enable == '0 && i_suppress == '0); + truth_01 : cover (i_write_enable == '0 && i_suppress == '1); + truth_10 : cover (i_write_enable == '1 && i_suppress == '0); + truth_11 : cover (i_write_enable == '1 && i_suppress == '1); + every_bit_permitted : cover (o_write_enable == '1); + every_bit_suppressed : cover (o_write_suppressed == '1); + zero_suppression_ratio : cover (i_write_enable != '0 && o_write_suppressed == '0); + complete_suppression_ratio : + cover (i_write_enable != '0 && o_write_suppressed == i_write_enable); + partition_observed : + cover ( + (o_write_enable & o_write_suppressed) == '0 && + (o_write_enable | o_write_suppressed) == i_write_enable + ); + end + + if (WIDTH > 1) begin : g_mixed_write_decision + always_comb begin + mixed_write_decision : cover (o_write_enable != '0 && o_write_suppressed != '0); + partial_suppression_ratio : cover (o_write_suppressed != '0 && o_write_enable != '0); + end + end +`endif + +endmodule diff --git a/verif/coverage/write_gate_coverage_bind.sv b/verif/coverage/write_gate_coverage_bind.sv new file mode 100644 index 0000000..e27e787 --- /dev/null +++ b/verif/coverage/write_gate_coverage_bind.sv @@ -0,0 +1,17 @@ +/// Stable boundary used to bind functional coverage to every write-gate DUT. +module write_gate_coverage_bind #( + parameter int unsigned WIDTH = 1 +) ( + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + input logic [WIDTH-1:0] o_write_enable, + input logic [WIDTH-1:0] o_write_suppressed +); + + write_gate_coverage #(.WIDTH(WIDTH)) i_write_gate_coverage (.*); + +endmodule + +`ifndef MOSAIC_FORMAL +bind write_gate write_gate_coverage_bind #(.WIDTH(WIDTH)) i_write_gate_coverage_bind (.*); +`endif diff --git a/verif/coverage/write_gate_integration_coverage.sv b/verif/coverage/write_gate_integration_coverage.sv new file mode 100644 index 0000000..c289466 --- /dev/null +++ b/verif/coverage/write_gate_integration_coverage.sv @@ -0,0 +1,33 @@ +/// Covers destination type, suppression reason, and protocol decision together. +module write_gate_integration_coverage #( + parameter int unsigned WIDTH = 1, + parameter bit DESTINATION_IS_MEMORY = 1'b0 +) ( + input logic i_sample, + input logic i_transaction_accepted, + input logic i_redundant_value_reason, + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + input logic [WIDTH-1:0] o_write_enable, + input logic [WIDTH-1:0] o_write_suppressed +); + + always @(posedge i_sample) begin + protocol_idle_no_decision : cover (!i_transaction_accepted && i_write_enable == '0); + protocol_accepted_permit : cover (i_transaction_accepted && o_write_enable != '0); + protocol_accepted_suppress : cover (i_transaction_accepted && o_write_suppressed != '0); + end + + if (DESTINATION_IS_MEMORY) begin : g_memory_destination + always @(posedge i_sample) begin + memory_redundant_suppression : + cover (i_redundant_value_reason && (i_write_enable & i_suppress) != '0); + end + end else begin : g_register_destination + always @(posedge i_sample) begin + register_redundant_suppression : + cover (i_redundant_value_reason && (i_write_enable & i_suppress) != '0); + end + end + +endmodule diff --git a/verif/coverage/write_gate_transition_coverage.sv b/verif/coverage/write_gate_transition_coverage.sv new file mode 100644 index 0000000..bdeb016 --- /dev/null +++ b/verif/coverage/write_gate_transition_coverage.sv @@ -0,0 +1,42 @@ +/// Samples every scalar control-state transition independently of DUT timing. +module write_gate_transition_coverage ( + input logic i_sample, + input logic i_write_enable, + input logic i_suppress +); + + logic previous_valid; + logic [1:0] previous_control; + logic [1:0] current_control; + + assign current_control = {i_write_enable, i_suppress}; + + initial begin + previous_valid = 1'b0; + previous_control = 2'b00; + end + + always @(posedge i_sample) begin + if (previous_valid) begin + transition_00_00 : cover (previous_control == 2'b00 && current_control == 2'b00); + transition_00_01 : cover (previous_control == 2'b00 && current_control == 2'b01); + transition_00_10 : cover (previous_control == 2'b00 && current_control == 2'b10); + transition_00_11 : cover (previous_control == 2'b00 && current_control == 2'b11); + transition_01_00 : cover (previous_control == 2'b01 && current_control == 2'b00); + transition_01_01 : cover (previous_control == 2'b01 && current_control == 2'b01); + transition_01_10 : cover (previous_control == 2'b01 && current_control == 2'b10); + transition_01_11 : cover (previous_control == 2'b01 && current_control == 2'b11); + transition_10_00 : cover (previous_control == 2'b10 && current_control == 2'b00); + transition_10_01 : cover (previous_control == 2'b10 && current_control == 2'b01); + transition_10_10 : cover (previous_control == 2'b10 && current_control == 2'b10); + transition_10_11 : cover (previous_control == 2'b10 && current_control == 2'b11); + transition_11_00 : cover (previous_control == 2'b11 && current_control == 2'b00); + transition_11_01 : cover (previous_control == 2'b11 && current_control == 2'b01); + transition_11_10 : cover (previous_control == 2'b11 && current_control == 2'b10); + transition_11_11 : cover (previous_control == 2'b11 && current_control == 2'b11); + end + previous_control = current_control; + previous_valid = 1'b1; + end + +endmodule diff --git a/verif/formal/write_gate_formal.sv b/verif/formal/write_gate_formal.sv new file mode 100644 index 0000000..a43bda9 --- /dev/null +++ b/verif/formal/write_gate_formal.sv @@ -0,0 +1,22 @@ +/// Unconstrained harness for proof and reachability of one write-gate width. +module write_gate_formal #( + parameter int unsigned WIDTH = 1 +); + + (* anyseq *)logic [WIDTH-1:0] i_write_enable; + (* anyseq *)logic [WIDTH-1:0] i_suppress; + logic [WIDTH-1:0] o_write_enable; + logic [WIDTH-1:0] o_write_suppressed; + + write_gate #(.WIDTH(WIDTH)) dut (.*); + write_gate_integration_formal #(.WIDTH(WIDTH)) i_integration_formal (); + +`ifdef FORMAL_ASSERTIONS + write_gate_bind #(.WIDTH(WIDTH)) i_write_gate_bind (.*); +`endif + +`ifdef FORMAL_COVERAGE + write_gate_coverage_bind #(.WIDTH(WIDTH)) i_write_gate_coverage_bind (.*); +`endif + +endmodule diff --git a/verif/formal/write_gate_integration_formal.sv b/verif/formal/write_gate_integration_formal.sv new file mode 100644 index 0000000..f68e00d --- /dev/null +++ b/verif/formal/write_gate_integration_formal.sv @@ -0,0 +1,40 @@ +/// Proves one-step state equivalence for a timing-safe redundant-write decision. +module write_gate_integration_formal #( + parameter int unsigned WIDTH = 1 +); + + (* anyseq *)logic [WIDTH-1:0] prior_state; + (* anyseq *)logic [WIDTH-1:0] write_data; + (* anyseq *)logic [WIDTH-1:0] i_write_enable; + (* anyseq *)logic [WIDTH-1:0] i_suppress; + logic [WIDTH-1:0] o_write_enable; + logic [WIDTH-1:0] o_write_suppressed; + logic [WIDTH-1:0] reference_next_state; + logic [WIDTH-1:0] gated_next_state; + + write_gate #( + .WIDTH(WIDTH) + ) dut ( + .i_write_enable(i_write_enable), + .i_suppress(i_suppress), + .o_write_enable(o_write_enable), + .o_write_suppressed(o_write_suppressed) + ); + + `include "write_gate_predicates.svh" + + always_comb begin + // Integration owns this assumption: only a write of the value already + // held by the destination may be classified as redundant here. + assume (write_gate_suppression_is_redundant_f( + prior_state, write_data, i_write_enable, i_suppress + )); + + reference_next_state = write_gate_next_state_f(prior_state, write_data, i_write_enable); + gated_next_state = write_gate_next_state_f(prior_state, write_data, o_write_enable); + + assert (gated_next_state == reference_next_state); + assert ((o_write_suppressed & (write_data ^ prior_state)) == '0); + end + +endmodule diff --git a/verif/mutations/write_gate_inverted_suppress_mutant.sv b/verif/mutations/write_gate_inverted_suppress_mutant.sv new file mode 100644 index 0000000..9a63d24 --- /dev/null +++ b/verif/mutations/write_gate_inverted_suppress_mutant.sv @@ -0,0 +1,14 @@ +// Verification-only mutation: suppression is deliberately inverted. +module write_gate #( + parameter int unsigned WIDTH = 1 +) ( + input logic [WIDTH-1:0] i_write_enable, + input logic [WIDTH-1:0] i_suppress, + output logic [WIDTH-1:0] o_write_enable, + output logic [WIDTH-1:0] o_write_suppressed +); + + assign o_write_enable = i_write_enable & i_suppress; + assign o_write_suppressed = i_write_enable & ~i_suppress; + +endmodule diff --git a/verif/properties/write_gate_predicates.svh b/verif/properties/write_gate_predicates.svh new file mode 100644 index 0000000..bc0fa53 --- /dev/null +++ b/verif/properties/write_gate_predicates.svh @@ -0,0 +1,37 @@ +// Module-scoped combinational predicates shared by write-gate checkers. +// This file has no include guard because each wrapper owns its declarations. + +function automatic logic [WIDTH-1:0] write_gate_permitted_f(input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] suppress); + write_gate_permitted_f = write_enable & ~suppress; +endfunction + +function automatic logic [WIDTH-1:0] write_gate_suppressed_f(input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] suppress); + write_gate_suppressed_f = write_enable & suppress; +endfunction + +function automatic logic write_gate_controls_known_f(input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] suppress); + write_gate_controls_known_f = !$isunknown({write_enable, suppress}); +endfunction + +function automatic logic write_gate_outputs_partition_f(input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] permitted, + input logic [WIDTH-1:0] suppressed); + write_gate_outputs_partition_f = + ((permitted & suppressed) == '0) && ((permitted | suppressed) == write_enable); +endfunction + +function automatic logic [WIDTH-1:0] write_gate_next_state_f(input logic [WIDTH-1:0] prior_state, + input logic [WIDTH-1:0] write_data, + input logic [WIDTH-1:0] write_enable); + write_gate_next_state_f = (prior_state & ~write_enable) | (write_data & write_enable); +endfunction + +function automatic logic write_gate_suppression_is_redundant_f( + input logic [WIDTH-1:0] prior_state, input logic [WIDTH-1:0] write_data, + input logic [WIDTH-1:0] write_enable, input logic [WIDTH-1:0] suppress); + write_gate_suppression_is_redundant_f = + ((write_enable & suppress & (write_data ^ prior_state)) == '0); +endfunction diff --git a/verif/tb/write_gate_four_state_tb.sv b/verif/tb/write_gate_four_state_tb.sv new file mode 100644 index 0000000..6845c96 --- /dev/null +++ b/verif/tb/write_gate_four_state_tb.sv @@ -0,0 +1,47 @@ +/// Four-state qualification fixture for illegal write-gate controls. +module write_gate_four_state_tb; + + logic i_write_enable = 1'b0; + logic i_suppress = 1'b0; + logic o_write_enable; + logic o_write_suppressed; + + write_gate #(.WIDTH(1)) dut (.*); + write_gate_sva #(.WIDTH(1)) i_write_gate_sva (.*); + + initial begin +`ifdef WRITE_GATE_INJECT_SUPPRESS + i_write_enable = 1'b1; +`else + i_write_enable = 1'b0; +`endif + i_suppress = 1'b0; + #1; + +`ifdef WRITE_GATE_INJECT_Z +`ifdef WRITE_GATE_INJECT_SUPPRESS + i_suppress = 1'bz; +`else + i_write_enable = 1'bz; +`endif +`else +`ifdef WRITE_GATE_INJECT_SUPPRESS + i_suppress = 1'bx; +`else + i_write_enable = 1'bx; +`endif +`endif + #1; + +`ifdef WRITE_GATE_DISABLE_UNKNOWN_MONITOR + if (!$isunknown({i_write_enable, i_suppress, o_write_enable, o_write_suppressed})) begin + $fatal(1, "WRITE_GATE_FOUR_STATE_STIMULUS_BROKEN"); + end + $display("WRITE_GATE_UNKNOWN_CONTROL_STIMULUS_REACHED"); + $finish; +`else + $fatal(1, "WRITE_GATE_UNKNOWN_CONTROL_MONITOR_DID_NOT_FIRE"); +`endif + end + +endmodule diff --git a/verif/tb/write_gate_integration_test_case.sv b/verif/tb/write_gate_integration_test_case.sv new file mode 100644 index 0000000..0bf6dd3 --- /dev/null +++ b/verif/tb/write_gate_integration_test_case.sv @@ -0,0 +1,306 @@ +/// Compares gated register and memory destinations with ungated references. +module write_gate_integration_test_case #( + parameter int unsigned WIDTH = 1, + parameter int unsigned MEMORY_DEPTH = 4, + parameter int unsigned ADDRESS_WIDTH = $clog2(MEMORY_DEPTH) +) ( + output logic o_done +); + + logic clock; + + logic [WIDTH-1:0] register_write_enable; + logic [WIDTH-1:0] register_suppress; + logic [WIDTH-1:0] register_write_data; + logic [WIDTH-1:0] register_gated_enable; + logic [WIDTH-1:0] register_suppressed; + logic [WIDTH-1:0] register_gated_state; + logic [WIDTH-1:0] register_reference_state; + logic register_coverage_sample; + logic register_transaction_accepted; + logic register_redundant_value_reason; + + logic [WIDTH-1:0] memory_write_enable; + logic [WIDTH-1:0] memory_suppress; + logic [WIDTH-1:0] memory_write_data; + logic [WIDTH-1:0] memory_gated_enable; + logic [WIDTH-1:0] memory_suppressed; + logic [ADDRESS_WIDTH-1:0] memory_address; + logic [WIDTH-1:0] memory_gated_state[0:MEMORY_DEPTH-1]; + logic [WIDTH-1:0] memory_reference_state[0:MEMORY_DEPTH-1]; + logic memory_coverage_sample; + logic memory_transaction_accepted; + logic memory_redundant_value_reason; + + longint unsigned register_reference_write_events; + longint unsigned register_gated_write_events; + longint unsigned register_reference_state_toggles; + longint unsigned register_gated_state_toggles; + longint unsigned memory_reference_write_events; + longint unsigned memory_gated_write_events; + longint unsigned memory_reference_state_toggles; + longint unsigned memory_gated_state_toggles; + + write_gate #( + .WIDTH(WIDTH) + ) u_register_gate ( + .i_write_enable(register_write_enable), + .i_suppress(register_suppress), + .o_write_enable(register_gated_enable), + .o_write_suppressed(register_suppressed) + ); + + write_gate #( + .WIDTH(WIDTH) + ) u_memory_gate ( + .i_write_enable(memory_write_enable), + .i_suppress(memory_suppress), + .o_write_enable(memory_gated_enable), + .o_write_suppressed(memory_suppressed) + ); + +`ifndef WRITE_GATE_DISABLE_COVERAGE + write_gate_integration_coverage #( + .WIDTH(WIDTH), + .DESTINATION_IS_MEMORY(1'b0) + ) i_register_coverage ( + .i_sample(register_coverage_sample), + .i_transaction_accepted(register_transaction_accepted), + .i_redundant_value_reason(register_redundant_value_reason), + .i_write_enable(register_write_enable), + .i_suppress(register_suppress), + .o_write_enable(register_gated_enable), + .o_write_suppressed(register_suppressed) + ); + + write_gate_integration_coverage #( + .WIDTH(WIDTH), + .DESTINATION_IS_MEMORY(1'b1) + ) i_memory_coverage ( + .i_sample(memory_coverage_sample), + .i_transaction_accepted(memory_transaction_accepted), + .i_redundant_value_reason(memory_redundant_value_reason), + .i_write_enable(memory_write_enable), + .i_suppress(memory_suppress), + .o_write_enable(memory_gated_enable), + .o_write_suppressed(memory_suppressed) + ); +`endif + + always #5ns clock = ~clock; + + function automatic logic [WIDTH-1:0] random_vector(); + for (int unsigned bit_index = 0; bit_index < WIDTH; bit_index++) begin + random_vector[bit_index] = ($urandom_range(0, 1) != 0); + end + endfunction + + function automatic longint unsigned count_set_bits(input logic [WIDTH-1:0] value); + count_set_bits = 0; + for (int unsigned bit_index = 0; bit_index < WIDTH; bit_index++) begin + count_set_bits += value[bit_index]; + end + endfunction + + function automatic logic [WIDTH-1:0] redundant_mask(input logic [WIDTH-1:0] prior_state, + input logic [WIDTH-1:0] write_data, + input logic [WIDTH-1:0] write_enable); + return write_enable & ~(write_data ^ prior_state); + endfunction + + always @(posedge clock) begin + register_reference_write_events <= register_reference_write_events + count_set_bits( + register_write_enable + ); + register_gated_write_events <= register_gated_write_events + count_set_bits( + register_gated_enable + ); + register_reference_state_toggles <= register_reference_state_toggles + count_set_bits( + register_write_enable & (register_reference_state ^ register_write_data) + ); + register_gated_state_toggles <= register_gated_state_toggles + count_set_bits( + register_gated_enable & (register_gated_state ^ register_write_data) + ); + + register_reference_state <= ( + register_reference_state & ~register_write_enable + ) | (register_write_data & register_write_enable); + register_gated_state <= ( + register_gated_state & ~register_gated_enable + ) | (register_write_data & register_gated_enable); + + memory_reference_write_events <= memory_reference_write_events + count_set_bits( + memory_write_enable + ); + memory_gated_write_events <= memory_gated_write_events + count_set_bits( + memory_gated_enable + ); + memory_reference_state_toggles <= memory_reference_state_toggles + count_set_bits( + memory_write_enable & (memory_reference_state[memory_address] ^ memory_write_data) + ); + memory_gated_state_toggles <= memory_gated_state_toggles + count_set_bits( + memory_gated_enable & (memory_gated_state[memory_address] ^ memory_write_data) + ); + + memory_reference_state[memory_address] <= ( + memory_reference_state[memory_address] & ~memory_write_enable + ) | (memory_write_data & memory_write_enable); + memory_gated_state[memory_address] <= ( + memory_gated_state[memory_address] & ~memory_gated_enable + ) | (memory_write_data & memory_gated_enable); + end + + task automatic apply_register_write(input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] write_data, + input bit suppress_redundant); + @(negedge clock); + register_write_enable = write_enable; + register_write_data = write_data; + register_suppress = suppress_redundant ? + redundant_mask(register_reference_state, write_data, write_enable) : '0; + register_transaction_accepted = (write_enable != '0); + register_redundant_value_reason = suppress_redundant; + + assert ((write_enable & register_suppress & (write_data ^ register_reference_state)) == '0) + else $fatal(1, "WIDTH=%0d unsafe register suppression requested", WIDTH); + + @(posedge clock); + #1ps; + assert (register_gated_state == register_reference_state) + else $fatal(1, "WIDTH=%0d gated register diverged from ungated reference", WIDTH); + assert (register_suppressed == (write_enable & register_suppress)) + else $fatal(1, "WIDTH=%0d register suppression observation diverged", WIDTH); + register_coverage_sample = 1'b1; + #1ps; + register_coverage_sample = 1'b0; + endtask + + task automatic apply_memory_write( + input logic [ADDRESS_WIDTH-1:0] address, input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] write_data, input bit suppress_redundant); + @(negedge clock); + memory_address = address; + memory_write_enable = write_enable; + memory_write_data = write_data; + memory_suppress = suppress_redundant ? + redundant_mask(memory_reference_state[address], write_data, write_enable) : '0; + memory_transaction_accepted = (write_enable != '0); + memory_redundant_value_reason = suppress_redundant; + + assert ((write_enable & memory_suppress & + (write_data ^ memory_reference_state[address])) == '0) + else $fatal(1, "WIDTH=%0d unsafe memory suppression requested", WIDTH); + + @(posedge clock); + #1ps; + for (int unsigned word_index = 0; word_index < MEMORY_DEPTH; word_index++) begin + assert (memory_gated_state[word_index] == memory_reference_state[word_index]) + else + $fatal( + 1, + "WIDTH=%0d gated memory word %0d diverged from ungated reference", + WIDTH, + word_index + ); + end + assert (memory_suppressed == (write_enable & memory_suppress)) + else $fatal(1, "WIDTH=%0d memory suppression observation diverged", WIDTH); + memory_coverage_sample = 1'b1; + #1ps; + memory_coverage_sample = 1'b0; + endtask + + initial begin + logic [WIDTH-1:0] partial_data; + logic [ADDRESS_WIDTH-1:0] random_address; + + o_done = 1'b0; + clock = 1'b0; + register_write_enable = '0; + register_suppress = '0; + register_write_data = '0; + register_gated_state = '0; + register_reference_state = '0; + register_coverage_sample = 1'b0; + register_transaction_accepted = 1'b0; + register_redundant_value_reason = 1'b0; + memory_write_enable = '0; + memory_suppress = '0; + memory_write_data = '0; + memory_address = '0; + memory_coverage_sample = 1'b0; + memory_transaction_accepted = 1'b0; + memory_redundant_value_reason = 1'b0; + register_reference_write_events = 0; + register_gated_write_events = 0; + register_reference_state_toggles = 0; + register_gated_state_toggles = 0; + memory_reference_write_events = 0; + memory_gated_write_events = 0; + memory_reference_state_toggles = 0; + memory_gated_state_toggles = 0; + for (int unsigned word_index = 0; word_index < MEMORY_DEPTH; word_index++) begin + memory_gated_state[word_index] = '0; + memory_reference_state[word_index] = '0; + end + + // Idle, ungated, fully suppressed, and partially suppressed intervals. + apply_register_write('0, '0, 1'b1); + apply_register_write('1, '1, 1'b0); + apply_register_write('1, register_reference_state, 1'b1); + partial_data = register_reference_state; + partial_data[0] = ~partial_data[0]; + apply_register_write('1, partial_data, 1'b1); + + repeat (8) begin + apply_register_write('1, random_vector(), 1'b0); + end + repeat (16) begin + apply_register_write('1, register_reference_state, 1'b1); + end + repeat (32) begin + apply_register_write(random_vector(), random_vector(), 1'b1); + end + + register_write_enable = '0; + register_suppress = '0; + apply_memory_write('0, '0, '0, 1'b1); + for (int unsigned word_index = 0; word_index < MEMORY_DEPTH; word_index++) begin + apply_memory_write(word_index[ADDRESS_WIDTH-1:0], '1, '1, 1'b0); + apply_memory_write(word_index[ADDRESS_WIDTH-1:0], '1, + memory_reference_state[word_index], 1'b1); + end + repeat (8) begin + random_address = ADDRESS_WIDTH'($urandom_range(0, MEMORY_DEPTH - 1)); + apply_memory_write(random_address, '1, random_vector(), 1'b0); + end + repeat (16) begin + apply_memory_write('0, '1, memory_reference_state[0], 1'b1); + end + repeat (32) begin + random_address = ADDRESS_WIDTH'($urandom_range(0, MEMORY_DEPTH - 1)); + apply_memory_write(random_address, random_vector(), random_vector(), 1'b1); + end + + assert (register_gated_write_events < register_reference_write_events) + else $fatal(1, "WIDTH=%0d register destination activity was not reduced", WIDTH); + assert (memory_gated_write_events < memory_reference_write_events) + else $fatal(1, "WIDTH=%0d memory destination activity was not reduced", WIDTH); + assert (register_gated_state_toggles == register_reference_state_toggles) + else $fatal(1, "WIDTH=%0d register architectural toggles changed", WIDTH); + assert (memory_gated_state_toggles == memory_reference_state_toggles) + else $fatal(1, "WIDTH=%0d memory architectural toggles changed", WIDTH); + + $display( + "WRITE_GATE_ACTIVITY destination=register width=%0d baseline_writes=%0d gated_writes=%0d state_toggles=%0d", + WIDTH, register_reference_write_events, register_gated_write_events, + register_gated_state_toggles); + $display( + "WRITE_GATE_ACTIVITY destination=memory width=%0d baseline_writes=%0d gated_writes=%0d state_toggles=%0d", + WIDTH, memory_reference_write_events, memory_gated_write_events, + memory_gated_state_toggles); + + o_done = 1'b1; + end + +endmodule diff --git a/verif/tb/write_gate_invalid_width_tb.sv b/verif/tb/write_gate_invalid_width_tb.sv new file mode 100644 index 0000000..a10b0fb --- /dev/null +++ b/verif/tb/write_gate_invalid_width_tb.sv @@ -0,0 +1,6 @@ +/// Elaboration-negative fixture for the unsupported WIDTH=0 configuration. +module write_gate_invalid_width_tb; + + write_gate #(.WIDTH(0)) dut (); + +endmodule diff --git a/verif/tb/write_gate_tb.sv b/verif/tb/write_gate_tb.sv new file mode 100644 index 0000000..838fa31 --- /dev/null +++ b/verif/tb/write_gate_tb.sv @@ -0,0 +1,23 @@ +/// Top-level regression for one profile-selected write-gate width. +module write_gate_tb #( + parameter int unsigned WIDTH = 2 +); + + logic unit_done; + logic integration_done; + + write_gate_test_case #(.WIDTH(WIDTH)) u_unit (.o_done(unit_done)); + write_gate_integration_test_case #(.WIDTH(WIDTH)) u_integration (.o_done(integration_done)); + + initial begin + wait (unit_done && integration_done); + $display("PASS: write_gate WIDTH=%0d regression completed", WIDTH); + $finish; + end + + initial begin + #10us; + $fatal(1, "write_gate WIDTH=%0d regression timed out", WIDTH); + end + +endmodule diff --git a/verif/tb/write_gate_test_case.sv b/verif/tb/write_gate_test_case.sv new file mode 100644 index 0000000..80d5a6f --- /dev/null +++ b/verif/tb/write_gate_test_case.sv @@ -0,0 +1,111 @@ +/// Reusable self-checking unit test for one parameterized write-gate instance. +module write_gate_test_case #( + parameter int unsigned WIDTH = 1 +) ( + output logic o_done +); + + logic [WIDTH-1:0] i_write_enable; + logic [WIDTH-1:0] i_suppress; + logic [WIDTH-1:0] o_write_enable; + logic [WIDTH-1:0] o_write_suppressed; + logic coverage_sample; + + write_gate #(.WIDTH(WIDTH)) dut (.*); + +`ifndef WRITE_GATE_DISABLE_COVERAGE + write_gate_transition_coverage i_transition_coverage ( + .i_sample(coverage_sample), + .i_write_enable(i_write_enable[0]), + .i_suppress(i_suppress[0]) + ); +`endif + + function automatic logic [WIDTH-1:0] alternating_vector(input bit first_bit); + for (int unsigned bit_index = 0; bit_index < WIDTH; bit_index++) begin + alternating_vector[bit_index] = first_bit ^ bit_index[0]; + end + endfunction + + function automatic logic [WIDTH-1:0] random_vector(); + for (int unsigned bit_index = 0; bit_index < WIDTH; bit_index++) begin + random_vector[bit_index] = ($urandom_range(0, 1) != 0); + end + endfunction + + task automatic check_case(input logic [WIDTH-1:0] write_enable, + input logic [WIDTH-1:0] suppress); + {i_write_enable, i_suppress} = {write_enable, suppress}; + #1ns; + assert (o_write_enable == (write_enable & ~suppress)) + else $fatal(1, "WIDTH=%0d permitted-write mismatch", WIDTH); + assert (o_write_suppressed == (write_enable & suppress)) + else $fatal(1, "WIDTH=%0d suppressed-write mismatch", WIDTH); + assert ((o_write_enable & o_write_suppressed) == '0) + else $fatal(1, "WIDTH=%0d outputs overlap", WIDTH); + assert ((o_write_enable | o_write_suppressed) == write_enable) + else $fatal(1, "WIDTH=%0d request partition mismatch", WIDTH); + coverage_sample = 1'b1; + #1ps; + coverage_sample = 1'b0; + endtask + + initial begin + logic [WIDTH-1:0] alternating_zero; + logic [WIDTH-1:0] alternating_one; + + o_done = 1'b0; + coverage_sample = 1'b0; + alternating_zero = alternating_vector(1'b0); + alternating_one = alternating_vector(1'b1); + + check_case('0, '0); + check_case('0, '1); + check_case('1, '0); + check_case('1, '1); + + for (int unsigned bit_index = 0; bit_index < WIDTH; bit_index++) begin + logic [WIDTH-1:0] one_hot; + one_hot = '0; + one_hot[bit_index] = 1'b1; + check_case(one_hot, '0); + check_case(one_hot, one_hot); + end + + check_case(alternating_zero, '0); + check_case(alternating_zero, alternating_one); + check_case(alternating_one, alternating_zero); + check_case(alternating_one, '1); + check_case('1, alternating_zero); + check_case('1, alternating_one); + + // Drive every source-to-destination transition of one representative + // lane. Repeating the scalar value across WIDTH keeps all lanes legal. + for (int unsigned source_index = 0; source_index < 4; source_index++) begin + for ( + int unsigned destination_index = 0; destination_index < 4; destination_index++ + ) begin + logic [1:0] source_control; + logic [1:0] destination_control; + + source_control = source_index[1:0]; + destination_control = destination_index[1:0]; + check_case({WIDTH{source_control[1]}}, {WIDTH{source_control[0]}}); + check_case({WIDTH{destination_control[1]}}, {WIDTH{destination_control[0]}}); + end + end + + repeat (16) begin + check_case('0, random_vector()); + end + repeat (16) begin + check_case('1, '1); + end + repeat (64) begin + check_case(random_vector(), random_vector()); + end + + o_done = 1'b1; + end + +endmodule From 12be5ea33fdfbb0407006b03dd520bb53c48d27d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Erick=20Andr=C3=A9s=20Obreg=C3=B3n=20Fonseca?= Date: Wed, 16 Sep 2026 22:58:35 -0600 Subject: [PATCH 2/2] [Fix] Preserve container flow policy in release evidence Keep container release-manifest generation aligned with the portable qualification policy. - Pass FLOW_openroad=disabled to separate container release-manifest invocation. - Prevent clock-gate container checks from requiring native-only OpenROAD evidence. - Verify the exact clock-gate container flow and release-manifest validation. --- .github/workflows/rtl-simulation.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index ceeb206..c9ea830 100644 --- a/.github/workflows/rtl-simulation.yml +++ b/.github/workflows/rtl-simulation.yml @@ -303,7 +303,7 @@ jobs: --env RELEASE_METHODOLOGY_DIRTY=false \ --env RELEASE_EXECUTION_CONTEXT=container \ --volume "${GITHUB_WORKSPACE}:/workspace" \ - "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" release-manifest release-manifest-validate \ + "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE="${{ matrix.module }}" PROFILE="${{ matrix.profile }}" FLOW_openroad=disabled release-manifest release-manifest-validate \ 2>&1 | tee ci-artifacts/container-release-manifest.log - name: Upload container RTL reports