diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index c9ea830..9644262 100644 --- a/.github/workflows/rtl-simulation.yml +++ b/.github/workflows/rtl-simulation.yml @@ -154,13 +154,15 @@ jobs: 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' + - name: Qualify representative functional and structural coverage + if: (matrix.module == 'write_gate' && matrix.profile == 'width_2') || (matrix.module == 'operand_isolation' && matrix.profile == 'width_16_pattern') 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 + module="${{ matrix.module }}" + profile="${{ matrix.profile }}" + make MODULE="${module}" PROFILE="${profile}" FORCE_FLOW=1 open-coverage \ + 2>&1 | tee "ci-artifacts/native-${module}-coverage.log" + coverage_dir="reports/${module}/${profile}/coverage_qualification" cp "${coverage_dir}/status.txt" "${coverage_dir}/forced-status.txt" printf 'SKIP\n' > "${coverage_dir}/status.txt" @@ -172,6 +174,8 @@ jobs: 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" + elif [[ "${{ matrix.module }}" == operand_isolation && "${{ matrix.profile }}" == width_16_pattern ]]; then + export RELEASE_ADDITIONAL_EVIDENCE="reports/operand_isolation/width_16_pattern/coverage_qualification/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 @@ -273,17 +277,19 @@ jobs: "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' + - name: Qualify representative functional and structural coverage in container + if: (matrix.module == 'write_gate' && matrix.profile == 'width_2') || (matrix.module == 'operand_isolation' && matrix.profile == 'width_16_pattern') run: | set -o pipefail + module="${{ matrix.module }}" + profile="${{ matrix.profile }}" 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 + "mosaic-module-ci:${GITHUB_SHA}-${{ matrix.module }}-${{ matrix.profile }}" MODULE="${module}" PROFILE="${profile}" FORCE_FLOW=1 open-coverage \ + 2>&1 | tee "ci-artifacts/container-${module}-coverage.log" + coverage_dir="reports/${module}/${profile}/coverage_qualification" cp "${coverage_dir}/status.txt" "${coverage_dir}/forced-status.txt" printf 'SKIP\n' > "${coverage_dir}/status.txt" @@ -293,6 +299,8 @@ jobs: additional_evidence="" if [[ "${{ matrix.module }}" == write_gate && "${{ matrix.profile }}" == width_2 ]]; then additional_evidence="reports/write_gate/width_2/coverage_qualification/forced-status.txt" + elif [[ "${{ matrix.module }}" == operand_isolation && "${{ matrix.profile }}" == width_16_pattern ]]; then + additional_evidence="reports/operand_isolation/width_16_pattern/coverage_qualification/forced-status.txt" fi docker run --rm \ --user "$(id -u):$(id -g)" \ diff --git a/README.md b/README.md index f51570e..a3f139b 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,7 @@ repository infrastructure and pinned [`mosaic-flow`](mosaic-flow) methodology. | `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/) | +| `operand_isolation` | Parameterizable architectural clamping of inactive datapath operands | [`docs/operand_isolation/`](docs/operand_isolation/) | 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/operand_isolation.json b/config/coverage-policies/operand_isolation.json new file mode 100644 index 0000000..21dd53e --- /dev/null +++ b/config/coverage-policies/operand_isolation.json @@ -0,0 +1,49 @@ +{ + "schema": "mosaic-coverage-policy-v1", + "scope": { + "include": [ + "rtl/operand_isolation.sv", + "verif/coverage/operand_isolation_coverage.sv", + "verif/coverage/operand_isolation_transition_coverage.sv", + "verif/coverage/operand_isolation_integration_coverage.sv" + ], + "exclude": [] + }, + "thresholds": { + "line": 95, + "branch": 80, + "toggle": 90, + "user": 100 + }, + "coverpoints": [ + {"name": "transparent_mode", "minimum_hits": 1}, + {"name": "isolation_mode", "minimum_hits": 1}, + {"name": "transparent_zero", "minimum_hits": 1}, + {"name": "transparent_ones", "minimum_hits": 1}, + {"name": "isolated_input_differs", "minimum_hits": 1}, + {"name": "isolated_input_matches", "minimum_hits": 1}, + {"name": "isolation_assert_data_stable", "minimum_hits": 1}, + {"name": "isolation_assert_data_changes", "minimum_hits": 1}, + {"name": "isolation_deassert_data_stable", "minimum_hits": 1}, + {"name": "isolation_deassert_data_changes", "minimum_hits": 1}, + {"name": "isolated_input_changes", "minimum_hits": 1}, + {"name": "transparent_input_changes", "minimum_hits": 1}, + {"name": "back_to_back_isolation", "minimum_hits": 1}, + {"name": "arithmetic_active", "minimum_hits": 1}, + {"name": "arithmetic_isolated", "minimum_hits": 1}, + {"name": "vector_active", "minimum_hits": 1}, + {"name": "vector_isolated", "minimum_hits": 1}, + {"name": "address_generation_active", "minimum_hits": 1}, + {"name": "address_generation_isolated", "minimum_hits": 1} + ], + "exclusions": [ + { + "source": "rtl/operand_isolation.sv", + "metric": "line", + "reason": "The default arm implements X/Z control propagation and cannot execute in Verilator's binary simulation. Dedicated Icarus X/Z campaigns qualify the arm.", + "owner": "module-maintainers", + "scope": {"line_start": 27} + } + ], + "formal": {"required": true} +} diff --git a/config/modules.json b/config/modules.json index 7ce29d4..e77b828 100644 --- a/config/modules.json +++ b/config/modules.json @@ -10,6 +10,7 @@ {"name": "level_shifter"}, {"name": "isolation_cell"}, {"name": "retention_register"}, - {"name": "write_gate"} + {"name": "write_gate"}, + {"name": "operand_isolation"} ] } diff --git a/config/modules/operand_isolation-flows.mk b/config/modules/operand_isolation-flows.mk new file mode 100644 index 0000000..5d61945 --- /dev/null +++ b/config/modules/operand_isolation-flows.mk @@ -0,0 +1,36 @@ +# Required portable checks for the technology-independent operand-isolation 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 + +# Destination timing, domains, scan, technology mapping, and activity belong to +# the first consuming datapath that uses the isolated operand. +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/operand_isolation.mk b/config/modules/operand_isolation.mk new file mode 100644 index 0000000..6507b67 --- /dev/null +++ b/config/modules/operand_isolation.mk @@ -0,0 +1,59 @@ +# Operand-isolation tops and design-owned flow inputs. +export DESIGN_TOP := operand_isolation +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/operand_isolation.sv \ + verif/properties/operand_isolation_predicates.svh \ + verif/assertions/operand_isolation_sva.sv \ + verif/assertions/operand_isolation_bind.sv \ + verif/coverage/operand_isolation_coverage.sv \ + verif/coverage/operand_isolation_transition_coverage.sv \ + verif/coverage/operand_isolation_integration_coverage.sv \ + verif/coverage/operand_isolation_coverage_bind.sv \ + verif/formal/operand_isolation_formal.sv \ + verif/mutations/operand_isolation_inverted_control_mutant.sv \ + verif/tb/operand_isolation_test_case.sv \ + verif/tb/operand_isolation_activity_test_case.sv \ + verif/tb/operand_isolation_tb.sv \ + verif/tb/operand_isolation_four_state_tb.sv \ + verif/tb/operand_isolation_invalid_width_tb.sv \ + verif/tb/operand_isolation_invalid_clamp_tb.sv +export FORMAL_CONFIG := $(call resolve_flow_config,symbiyosys,formal.sby) +export FORMAL_COVER_CONFIG := $(MODULE_ROOT)/flows/symbiyosys/operand_isolation.cover.sby +export EQUIVALENCE_CONFIG := $(call resolve_flow_config,eqy,equivalence.eqy) +export COVERAGE_QUALIFICATION_POLICY := $(MODULE_ROOT)/config/coverage-policies/operand_isolation.json +export COVERAGE_QUALIFICATION_SOURCE := verilator_sim +export SIM_COVERAGE := enabled +export QUALIFICATION_CAMPAIGN_MANIFEST := $(MODULE_ROOT)/config/qualification-campaigns/operand_isolation.json +export STATIC_INTENT_CONFIG := $(MODULE_ROOT)/config/static-intent/operand_isolation.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/operand_isolation.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/operand_isolation.json b/config/parameter-profiles/operand_isolation.json new file mode 100644 index 0000000..9d6474e --- /dev/null +++ b/config/parameter-profiles/operand_isolation.json @@ -0,0 +1,47 @@ +{ + "schema": "mosaic-parameter-profiles-v1", + "include": [ + { + "name": "width_1_zero", + "parameters": {"WIDTH": 1, "CLAMP_VALUE": "1'b0"}, + "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": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + }, + { + "name": "width_8_ones", + "parameters": {"WIDTH": 8, "CLAMP_VALUE": "8'hff"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + }, + { + "name": "width_16_pattern", + "parameters": {"WIDTH": 16, "CLAMP_VALUE": "16'ha55a"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + }, + { + "name": "width_32_zero", + "parameters": {"WIDTH": 32, "CLAMP_VALUE": "32'h00000000"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + }, + { + "name": "width_64_ones", + "parameters": {"WIDTH": 64, "CLAMP_VALUE": "64'hffffffffffffffff"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + }, + { + "name": "width_128_pattern", + "parameters": {"WIDTH": 128, "CLAMP_VALUE": "128'ha5a55a5af0f00f0fa5a55a5af0f00f0f"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + }, + { + "name": "width_256_pattern", + "parameters": {"WIDTH": 256, "CLAMP_VALUE": "256'ha5a55a5af0f00f0fa5a55a5af0f00f0f5a5aa5a50f0ff0f05a5aa5a50f0ff0f0"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "operand_isolation", "testbench": "operand_isolation_tb", "formal": "operand_isolation_formal"} + } + ] +} diff --git a/config/qualification-campaigns/operand_isolation.json b/config/qualification-campaigns/operand_isolation.json new file mode 100644 index 0000000..5391c58 --- /dev/null +++ b/config/qualification-campaigns/operand_isolation.json @@ -0,0 +1,123 @@ +{ + "schema": "mosaic-qualification-campaigns-v1", + "campaigns": { + "negative": { + "inputs": [ + "rtl/operand_isolation.sv", + "verif/mutations/operand_isolation_inverted_control_mutant.sv", + "verif/tb/operand_isolation_test_case.sv", + "verif/tb/operand_isolation_invalid_width_tb.sv", + "verif/tb/operand_isolation_invalid_clamp_tb.sv" + ], + "cases": [ + { + "id": "nominal_unit_regression", + "evidence": "nominal_unit_regression", + "role": "positive_control", + "kind": "simulation_control", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DOPERAND_ISOLATION_DISABLE_COVERAGE", "-s", "operand_isolation_test_case", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/tb/operand_isolation_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success"} + ] + }, + { + "id": "inverted_control_mutation", + "evidence": "inverted_control_mutation", + "role": "negative", + "kind": "simulation_mutation", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DOPERAND_ISOLATION_DISABLE_COVERAGE", "-s", "operand_isolation_test_case", "-o", "{case_work_dir}/simulation.vvp", "verif/mutations/operand_isolation_inverted_control_mutant.sv", "verif/tb/operand_isolation_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "actual=", "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", "operand_isolation_invalid_width_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/tb/operand_isolation_invalid_width_tb.sv"], "expected": "failure", "diagnostic": "operand_isolation_width_must_be_greater_than_zero", "failure_class": "elaboration"} + ] + }, + { + "id": "invalid_clamp_x_elaboration", + "evidence": "invalid_clamp_x_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "operand_isolation_invalid_clamp_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/tb/operand_isolation_invalid_clamp_tb.sv"], "expected": "failure", "diagnostic": "operand_isolation_clamp_value_must_be_known", "failure_class": "elaboration"} + ] + }, + { + "id": "invalid_clamp_z_elaboration", + "evidence": "invalid_clamp_z_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DOPERAND_ISOLATION_INVALID_CLAMP_Z", "-s", "operand_isolation_invalid_clamp_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/tb/operand_isolation_invalid_clamp_tb.sv"], "expected": "failure", "diagnostic": "operand_isolation_clamp_value_must_be_known", "failure_class": "elaboration"} + ] + } + ] + }, + "four_state": { + "simulator": "iverilog", + "inputs": [ + "rtl/operand_isolation.sv", + "verif/assertions/operand_isolation_sva.sv", + "verif/tb/operand_isolation_four_state_tb.sv" + ], + "cases": [ + { + "id": "disabled_unknown_control_x", + "evidence": "disabled_unknown_control_x", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_isolate", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DOPERAND_ISOLATION_DISABLE_UNKNOWN_MONITOR", "-s", "operand_isolation_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/assertions/operand_isolation_sva.sv", "verif/tb/operand_isolation_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "OPERAND_ISOLATION_UNKNOWN_CONTROL_STIMULUS_REACHED"} + ] + }, + { + "id": "unknown_control_x", + "evidence": "unknown_control_x", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_unknown_control_x", + "injections": [{"control": "i_isolate", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "operand_isolation_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/assertions/operand_isolation_sva.sv", "verif/tb/operand_isolation_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "operand_isolation isolation control is unknown", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_high_impedance_control_z", + "evidence": "disabled_high_impedance_control_z", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_isolate", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DOPERAND_ISOLATION_DISABLE_UNKNOWN_MONITOR", "-DOPERAND_ISOLATION_INJECT_Z", "-s", "operand_isolation_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/assertions/operand_isolation_sva.sv", "verif/tb/operand_isolation_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "OPERAND_ISOLATION_UNKNOWN_CONTROL_STIMULUS_REACHED"} + ] + }, + { + "id": "high_impedance_control_z", + "evidence": "high_impedance_control_z", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_high_impedance_control_z", + "injections": [{"control": "i_isolate", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DOPERAND_ISOLATION_INJECT_Z", "-s", "operand_isolation_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/operand_isolation.sv", "verif/assertions/operand_isolation_sva.sv", "verif/tb/operand_isolation_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "operand_isolation isolation control is unknown", "failure_class": "unknown_control"} + ] + } + ] + } + } +} diff --git a/config/static-intent/operand_isolation.json b/config/static-intent/operand_isolation.json new file mode 100644 index 0000000..e311c37 --- /dev/null +++ b/config/static-intent/operand_isolation.json @@ -0,0 +1,28 @@ +{ + "schema": "mosaic-static-intent-v1", + "sdc": { + "profiles": [ + {"name": "synthesis", "path": "flows/synthesis/operand_isolation.timing.sdc", "kind": "combinational"}, + {"name": "physical", "path": "flows/openroad/operand_isolation.timing.sdc", "kind": "combinational"} + ], + "consistency": [ + { + "profiles": ["synthesis", "physical"], + "commands": ["set_input_transition", "set_load", "set_max_delay"] + } + ] + }, + "upf": { + "path": "flows/vc_lp/operand_isolation.power.upf", + "top": "operand_isolation", + "mode": "always_on", + "required": { + "power_domains": ["PD_OPERAND_ISOLATION"], + "supply_ports": ["VDD", "VSS"], + "supply_nets": ["VDD", "VSS"], + "supply_connections": ["VDD", "VSS"], + "domain_supplies": ["PD_OPERAND_ISOLATION"] + }, + "forbidden_strategies": ["isolation", "level_shifting", "retention", "power_switch"] + } +} diff --git a/docs/README.md b/docs/README.md index 57b3d42..c91abe2 100644 --- a/docs/README.md +++ b/docs/README.md @@ -6,6 +6,7 @@ - [Parameterizable D flip-flop](dff/README.md) - [Parameterizable write gate](write_gate/README.md) +- [Parameterizable operand isolation](operand_isolation/README.md) ## Template documentation diff --git a/docs/operand_isolation/README.md b/docs/operand_isolation/README.md new file mode 100644 index 0000000..c05bcc4 --- /dev/null +++ b/docs/operand_isolation/README.md @@ -0,0 +1,30 @@ +# Operand Isolation Documentation + +`operand_isolation` clamps an inactive datapath operand to a compile-time +constant so downstream combinational logic does not follow irrelevant input +activity. It is a stateless architectural power primitive and is not a UPF +power-domain isolation cell. + +- [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=operand_isolation PROFILE=width_16_pattern clean open-source +``` + +Run the complete supported parameter matrix with: + +```sh +make MODULE=operand_isolation clean all-profiles PROFILE_JOBS=4 +``` + +The parameter-profile schema does not select `coverage_qualification`. Native +and container CI therefore force the representative `width_16_pattern` +coverage gate before release-manifest generation, retain its passing status as +additional evidence, and restore the profile-owned status to `SKIP`. diff --git a/docs/operand_isolation/interface.md b/docs/operand_isolation/interface.md new file mode 100644 index 0000000..05d9a19 --- /dev/null +++ b/docs/operand_isolation/interface.md @@ -0,0 +1,85 @@ +# Interface Specification + +[Return to the module documentation index](README.md). + +## Overview + +`operand_isolation` is a combinational, technology-independent datapath +primitive. It passes `i_data` while computation is active and drives +`CLAMP_VALUE` while isolation is requested. The clamp prevents irrelevant +upstream activity from propagating into an expensive downstream cone. + +This module implements architectural operand isolation. It does not implement +power-domain isolation, retention, level shifting, synchronization, state +holding, protocol cancellation, or glitch filtering. + +## Parameters + +| Parameter | Type | Default | Legal values | Description | +| --- | --- | --- | --- | --- | +| `WIDTH` | `int unsigned` | `32` | Integers greater than or equal to 1 | Operand width | +| `CLAMP_VALUE` | `logic [WIDTH-1:0]` | `'0` | Known zero and one bits | Constant driven while isolated | + +The declared parameter type sizes `CLAMP_VALUE` to exactly `WIDTH` bits. +`WIDTH=0` and a clamp containing X or Z are rejected during elaboration. + +## Ports + +| Port | Direction | Width | Description | +| --- | --- | --- | --- | +| `i_data` | Input | `WIDTH` | Upstream operand | +| `i_isolate` | Input | 1 | Active-high architectural isolation request | +| `o_data` | Output | `WIDTH` | Transparent or clamped operand | + +The module has no clock, reset, state, handshake, or backpressure interface. + +## Functional Behavior + +| `i_isolate` | `o_data` | +| --- | --- | +| `0` | `i_data` | +| `1` | `CLAMP_VALUE` | +| `X` or `Z` | All bits unknown and an assertion failure in verification | + +Pass-through mode preserves the complete four-state value of `i_data`. +Isolation mode prevents changes on `i_data` from changing `o_data`. + +## Timing Contract + +- Architectural latency is zero cycles. +- The initiation interval is one cycle when placed between registered stages. +- `i_data` to `o_data` and `i_isolate` to `o_data` are combinational paths. +- The integration must make `i_isolate` stable before downstream capture. +- This module does not make an asynchronous control metastability-safe. + +The control path can become timing-critical when it drives wide operands or +many instances. Buffering and replication are physical integration decisions. + +## Clamp Selection + +Zero is the preferred initial value because it often maps to simple gating. +Another value may be selected when it is legal for the downstream function and +reduces activity more effectively. The selected clamp must not trigger an +exception, illegal mode, memory operation, or control action when the +downstream result is inactive. + +## Integration Assumptions + +- The consumer asserts `i_isolate` only when the downstream result is unused. +- Valid, ready, stall, kill, predicate, lane-mask, and pipeline state remain + coordinated with the isolation decision. +- `i_data` and `i_isolate` are coherent in the consuming clock domain. +- An asynchronous isolation request is synchronized before reaching this leaf. +- Test mode can force transparent operation when downstream ATPG access needs it. +- UPF inserts approved isolation and level shifting at actual power crossings. + +Violating the first assumption can silently corrupt an accepted operation. +That protocol relationship must be verified at the consuming hierarchy. + +## Low-Power Scope + +The leaf is useful only when saved downstream switching exceeds its area, +delay, and control-generation cost. Unit verification demonstrates activity +suppression in representative combinational cones. Technology-specific energy +savings require a mapped baseline and consuming implementation under identical +activity, libraries, corners, and workloads. diff --git a/docs/operand_isolation/power-characterization.md b/docs/operand_isolation/power-characterization.md new file mode 100644 index 0000000..80c0c0f --- /dev/null +++ b/docs/operand_isolation/power-characterization.md @@ -0,0 +1,39 @@ +# Power Characterization + +[Return to the module documentation index](README.md). + +## Portable Activity Evidence + +The open-source regression compares equivalent downstream combinational cones +driven directly by `i_data` and through `operand_isolation`. It exercises three +representative classes: + +- Arithmetic preprocessing +- Vector bit manipulation +- Address-generation arithmetic + +The test alternates active and isolated intervals while input data continues to +change. It checks functional equality in every active interval and fails unless +the isolated cone records fewer output-bit transitions than its ungated +baseline. Results use the `OPERAND_ISOLATION_ACTIVITY` prefix in the simulation +report. + +These transition counts validate useful suppression and stimulus quality. They +are not a library-based power estimate and must not be reported as energy +savings. + +## Integration Signoff + +The consuming implementation must compare isolated and equivalent ungated +designs using the same workload and annotated activity. PrimePower or an +approved alternative must include: + +- Isolation logic internal power +- Isolation-control generation and distribution +- Downstream combinational internal and switching power +- Leakage and total power +- Activity annotation coverage + +PrimeTime must close both operand and isolation-control paths to the downstream +capture point. CDC, RDC, DFT, and VC LP must use the consuming hierarchy and +must not credit this block as a required power-domain isolation cell. diff --git a/docs/operand_isolation/project-configuration.md b/docs/operand_isolation/project-configuration.md new file mode 100644 index 0000000..8fa43aa --- /dev/null +++ b/docs/operand_isolation/project-configuration.md @@ -0,0 +1,35 @@ +# Project Configuration + +[Return to the module documentation index](README.md). + +`config/modules/operand_isolation.mk` owns the tops, layered filelists, flow +inputs, and report roots. `config/modules/operand_isolation-flows.mk` enables +the portable lint, formatting, elaboration, generic synthesis, formal, +equivalence, simulation, qualification, and static-intent checks. + +The qualified matrix contains widths 1, 8, 16, 32, 64, 128, and 256. It covers +zero, all-one, and nontrivial clamp classes. The width-one profile owns the +invalid-parameter, mutation, and four-state campaigns because their behavior +does not depend on datapath width. + +`PROPERTY_FILELIST`, `ASSERTION_FILELIST`, and `COVERAGE_FILELIST` keep shared +predicates, checking wrappers, and coverage wrappers separate. Simulation and +formal compile the same combinational assertion and coverage definitions. + +Both SDC files define matching input transition, output load, complete +input-to-output delay, operand-to-output, and control-to-output constraints. +Portable static-intent validation also checks an always-on UPF baseline that +forbids isolation, level-shifting, retention, and power-switch strategies at +this architectural leaf. + +Commercial lint, CDC, DFT, low-power, mapped synthesis, timing, power, and +physical signoff are disabled for standalone portable qualification. They +require the actual downstream datapath, clock and reset domains, test controls, +power states, target libraries, corners, and representative annotated activity. +Their expected leaf status is `SKIP`, not `PASS`. + +The pinned parameter-profile schema does not admit `coverage_qualification`. +GitHub Actions therefore reruns the representative width-16 simulation with +`FORCE_FLOW=1`, qualifies native HDL and formal coverage, preserves the passing +status as `forced-status.txt`, restores the profile-owned status to `SKIP`, and +indexes the forced status in the release manifest. diff --git a/docs/operand_isolation/release-checklist.md b/docs/operand_isolation/release-checklist.md new file mode 100644 index 0000000..5ad9fb5 --- /dev/null +++ b/docs/operand_isolation/release-checklist.md @@ -0,0 +1,291 @@ +# 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, + report paths, and CI matrix consistently use `operand_isolation` within + `mosaic-common`._ +- [x] Supported parameter values and configurations are listed. + _`WIDTH >= 1` and a fully known `WIDTH`-bit `CLAMP_VALUE` are legal. The + qualified matrix covers widths 1, 8, 16, 32, 64, 128, and 256 with zero, + all-one, and nontrivial pattern clamp classes._ +- [x] Unsupported modes and external assumptions are explicit. + _The leaf does not provide power-domain isolation, retention, level shifting, + synchronization, state holding, glitch filtering, or protocol cancellation. + The consumer owns isolation legality, control timing, and operation capture._ +- [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 policy requires portable lint, formatting, elaboration, generic + synthesis, formal, equivalence, simulation, and static-intent checks. The + remaining standalone adapters record reviewed policy `SKIP` results._ + +## Interface and architecture + +- [x] [Interface specification](interface.md) matches the RTL. + _The parameter types, active-high isolation control, transparent equation, + clamp equation, and X/Z behavior agree with `rtl/operand_isolation.sv`._ +- [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. + _Architectural latency is zero cycles. The leaf has no handshake, + backpressure, acknowledgement, or runtime error interface. An X/Z isolation + control propagates an unknown output and is reported by verification._ +- [x] Disabled, reset, test, and low-power behavior are documented. + _Asserting `i_isolate` drives `CLAMP_VALUE`. Reset is not applicable, test + integration must permit transparent operation, and this architectural clamp + is explicitly distinguished from UPF power-domain isolation._ +- [x] Integration assumptions and protocol dependencies are reviewed. + _The consumer must assert isolation only when the operand is unused, keep the + control stable before capture, synchronize asynchronous requests, and align + isolation with valid, ready, stall, kill, predicate, lane-mask, and pipeline + state._ + +## RTL quality + +- [x] Verible style lint records `PASS` or an approved policy `SKIP`. + _All seven supported parameter profiles record `PASS`._ +- [x] Verible formatting records the expected status. + _All module-owned SystemVerilog and property sources use four-space + indentation and record `PASS`._ +- [x] Slang elaboration records the expected status. + _Every supported width and clamp profile elaborates successfully._ +- [x] Verilator lint records the expected status. + _All seven profiles record `PASS` with assertions and coverage wrappers in + their layered filelists._ +- [x] Yosys generic synthesis records the expected status. + _Every profile synthesizes to combinational logic. The representative + `WIDTH=16` pattern clamp contains 16 generic gates and no state._ +- [x] No unresolved warning is hidden outside the reviewed waiver files. + _The retained portable lint, elaboration, synthesis, simulation, formal, and + equivalence logs contain no warning or error requiring a waiver._ + +## Functional verification + +- [x] The [verification plan](verification-plan.md) maps every requirement to a + test, assertion, formal property, or reviewed combination. + _The traceability table covers pass-through, clamping, input independence, + illegal control, parameter legality, combinational behavior, activity + reduction, synthesis structure, and equivalence._ +- [x] All supported parameter configurations have evidence. + _Native and container regressions pass for widths 1, 8, 16, 32, 64, 128, + and 256 across zero, all-one, and nontrivial pattern clamp classes._ +- [x] Positive, negative, reset, error, and boundary tests pass. + _Directed, per-bit, alternating, deterministic long-sequence, isolated-input + activity, inverted-control mutation, invalid-width, invalid-X/Z-clamp, and + X/Z-control campaigns pass. Reset is not applicable._ +- [x] Assertions run in simulation and reach meaningful antecedents. + _Bound assertions check transparent and isolated equations plus unknown + controls. All 19 required functional, transition, and integration coverpoints + are observed in the representative coverage run._ +- [x] Formal assumptions are reviewed for overconstraint. + _The formal harness has no assumptions and leaves both operands and the + isolation control symbolic._ +- [x] Formal proofs pass at justified depth or by complete proof. + _The combinational contract and twin-DUT input-independence properties pass + by complete induction at depth one for every supported profile._ +- [x] RTL-to-Yosys-netlist equivalence passes. + _EQY proves the `o_data` partition equivalent for all seven profiles._ +- [x] Functional and code coverage goals are met or deviations are approved. + _The representative profile reaches 100 percent effective line coverage, + 100 percent branch coverage, 99.5495 percent toggle coverage, 100 percent + user coverage, all 19 named points, and formal cover reachability. + `OI-COV-001` approves the exact X/Z default-arm line exclusion, which is + qualified separately by passing four-state simulation._ + +## Constraints and static checks + +- [x] Synthesis and physical clocks agree unless a difference is documented. + _Both constraint sets describe a combinational leaf and intentionally create + no clock._ +- [x] Input, output, uncertainty, exception, and asynchronous paths are reviewed. + _Matching SDC files constrain input transition, output load, every + input-to-output path, and explicit operand and isolation-control paths. Clock + uncertainty, timing exceptions, and asynchronous clock paths do not apply._ +- [x] CDC and reset-domain intent covers every domain and crossing. + _The leaf has no clock, reset, state, or internal crossing. The consumer must + provide coherent operands and controls and synchronize any asynchronous + isolation request before this module._ +- [x] CDC violations are resolved or narrowly waived. + _CDC and RDC are policy `SKIP` at this stateless leaf. No crossing is waived, + and destination-domain analysis remains an integration requirement._ +- [x] DFT test modes, controllability, observability, and exclusions are reviewed. + _The module has no state or internal test mode. Integration must make + `i_isolate` controllable so transparent mode exposes the downstream cone._ +- [x] UPF power domains, states, isolation, retention, and supplies match the + architecture. + _Portable static intent validates one always-on domain and forbids isolation, + level shifting, retention, and power-switch strategies at this architectural + leaf. Actual power crossings remain owned by the consumer._ +- [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 reviewed policy `SKIP` because the + required clock, reset, scan, power-state, and technology context exists only + in the consumer. No commercial result is represented as `PASS`._ + +## Synthesis, timing, and power + +- [x] Design Compiler completes with the intended libraries and operating corner. + _Approved policy `SKIP` for the technology-independent leaf. Technology-mapped + synthesis is mandatory in the first consuming datapath._ +- [x] Area, QoR, and synthesis timing reports are reviewed. + _Yosys generic synthesis passes for every profile and produces only + combinational logic. The representative `WIDTH=16` patterned implementation + contains 16 generic gates and no state._ +- [x] PrimeTime reports no release-blocking setup or hold violation. + _Approved policy `SKIP` until registered launch and capture boundaries, + libraries, and operating corners are selected by the consumer._ +- [x] Unconstrained paths and constraint coverage are reviewed. + _Portable static intent validates a complete input-to-output maximum-delay + budget and explicit `i_data` and `i_isolate` path budgets in both SDC files._ +- [x] PrimePower uses representative SAIF activity. + _Approved policy `SKIP` at leaf level. Mapped isolated and ungated consumers + must be compared with identical representative activity before claiming + technology-specific energy savings._ +- [x] SAIF hierarchy and activity annotation coverage are reviewed. + _Standalone SAIF is not applicable while PrimePower is disabled. The portable + regression instead records downstream transitions for three use cases and + explicitly documents that these counts are not power estimates._ +- [x] Power, performance, and area results meet the module targets. + _The portable target is functional correctness and demonstrably lower + downstream activity with unchanged active behavior. Numeric PPA targets are + deferred to a mapped consuming datapath._ +- [x] PDK, library, tool, constraint, and corner identities are recorded. + _Release manifests record the portable toolchain, constraints, source hashes, + module and methodology revisions, and technology-independent scope. PDK, + library, and corner identities are conditional integration evidence._ + +## Physical implementation + +- [x] OpenROAD or the selected implementation flow uses the intended platform. + _Approved policy `SKIP` for standalone qualification. The committed Nangate45 + configuration is exploratory collateral, not a qualified implementation._ +- [x] Floorplan, utilization, aspect ratio, and margins are justified. + _Not applicable to this portable leaf release. The clamp must be placed near + its downstream cone, and integration owns control fanout, buffering, + congestion, voltage areas, utilization, and margins._ +- [x] Placement, clocking, routing, timing, DRC, and LVS evidence is retained when + physical implementation belongs to this module's release scope. + _Physical implementation is outside the standalone release scope. The + consuming block owns placement, routing, extraction, control timing, DRC, and + LVS. Clocking is not applicable inside this leaf._ +- [x] Preliminary open-source physical results are not labeled as commercial + signoff evidence. + _No physical or foundry signoff result is claimed._ + +## Waivers + +- [x] Every accepted waiver is recorded in [Reviewed waivers](waivers.md). + _`OI-COV-001` records the only requested exclusion and points to its dedicated + four-state qualification evidence._ +- [x] Each waiver identifies the tool, rule, object, justification, owner, + reviewer, date, and removal condition. + _`OI-COV-001` records the affected line, technical justification, dedicated + evidence, owner, reviewer, creation and approval dates, and objective removal + condition._ +- [x] Generated waiver drafts are not treated as approved policy. + _The coverage-policy exclusion is manually scoped to one exact RTL line. No + generated draft has been promoted into project policy._ +- [x] Expired waivers have been removed or re-reviewed. + _No operand-isolation waiver is expired._ + +## Reproducibility and evidence + +- [x] Native `make clean open-source` passes. + _`make MODULE=operand_isolation clean all-profiles PROFILE_JOBS=4` passes all + seven profiles, including the width-one negative and four-state campaigns. + The complete repository matrix also passes all 30 module-profile + combinations natively._ +- [x] The pinned Docker image builds and its portable gate passes. + _Image `sha256:5d6dfaec931c37c2ea69c1103053e0c3eea34899f0692d09a2302ba5a2b426d9` + was built from the current Dockerfile and pinned `mosaic-flow` revision. Its + complete 30-entry repository matrix, representative coverage, and release + manifest validation pass._ +- [x] The GitHub Actions disposition is reviewed for the recorded revision. + _Push run `35545096382` and pull-request run `35545136959` for revision + `5c188f9` were rejected before their first step because of failed account + payments or the configured spending limit. No flow executed or failed. Under + approved exception `OI-CI-001`, the exact native and container workflow + commands pass locally and the hosted result is recorded as + `BLOCKED_EXTERNAL`, not `PASS`._ +- [x] Commercial gates pass in the authorized local or self-hosted environment. + _Commercial gates are reviewed policy `SKIP` for portable leaf qualification. + Their integration requirements remain mandatory and no commercial execution + is inferred._ +- [x] Reports identify module revision, methodology revision, tool versions, + constraints, technology, date, and configuration. + _All 30 native and all 30 container release manifests validate for module + revision `5c188f9` and pinned methodology revision `0bd222f`. They record + configuration and tool metadata and hash required inputs and evidence._ +- [x] The CI and release-evidence retention disposition is reviewed. + _GitHub could not create artifacts because both hosted runs were rejected + before execution. Under `OI-CI-001`, local native and container logs, reports, + work databases, coverage evidence, and release manifests are retained in the + repository's ignored evidence directories. The exception expires when hosted + execution can be repeated and artifact IDs and retention dates recorded._ +- [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, synchronizer, or + internal domain crossing. The consumer must analyze operand sources, + isolation-control generation, clock and reset domains, and reconvergence._ +- [x] The DFT disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the leaf has no state, scan element, generated clock, or + internal test mode. The consumer must make `i_isolate` controllable, force + transparent mode for ATPG, and preserve downstream observability._ +- [x] The VC LP disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: portable static intent validates one always-on domain and + forbids UPF isolation, retention, level shifting, and power switches at this + architectural clamp. The consumer must run VC LP on its real domains, + supplies, power states, crossings, and sequencing._ +- [x] The PrimeTime disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: meaningful timing requires registered launch and capture + boundaries, target libraries, operating corners, and final control fanout. + The consumer must close both operand-to-output and control-to-output paths._ +- [x] The PrimePower disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: a standalone clamp cannot demonstrate net power savings. + The consumer must compare mapped isolated and ungated downstream cones using + identical representative activity and annotation coverage._ +- [x] The physical-signoff disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: placement and routing are meaningful only with the actual + downstream cone, control distribution, voltage areas, target PDK, and loads. + The consumer owns extraction, timing, power integrity, DRC, and LVS._ + +These reviewed skips close the portable leaf checklist only. The transferred +requirements remain mandatory before a multiplier, MAC, ALU, vector lane, +address generator, or other consumer can claim integration signoff or silicon +power savings. + +## Known methodology limitation + +The pinned `mosaic-flow` parameter-profile schema does not admit +`coverage_qualification` in a profile flow list. Native and container CI force +coverage for `width_16_pattern`, preserve its passing status as +`forced-status.txt`, restore the profile-owned status to `SKIP`, and index the +passing supplemental evidence in the release manifest. + +## Final commands + +```sh +git submodule status +make MODULE=operand_isolation PROFILE=width_16_pattern flow-config-check +make MODULE=operand_isolation clean all-profiles PROFILE_JOBS=4 +make MODULE=operand_isolation PROFILE=width_16_pattern FORCE_FLOW=1 open-coverage +``` + +Run commercial commands only in the licensed consuming environment after the +datapath, libraries, corners, activity, test intent, and power intent exist. + +## 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 local `PASS` files. diff --git a/docs/operand_isolation/verification-plan.md b/docs/operand_isolation/verification-plan.md new file mode 100644 index 0000000..84a109d --- /dev/null +++ b/docs/operand_isolation/verification-plan.md @@ -0,0 +1,103 @@ +# Verification Plan + +[Return to the module documentation index](README.md). + +## Verification Objectives + +The environment verifies transparent operation, clamped operation, input +independence while isolated, explicit X/Z control handling, parameter legality, +activity reduction, generic synthesis, and RTL-to-netlist equivalence. + +## Verification Environments + +| Environment | Top | Purpose | +| --- | --- | --- | +| Verilator simulation | `operand_isolation_tb` | Directed, per-bit, transition, randomized, integration, assertion, and coverage checks | +| Icarus qualification | Dedicated fixtures | Mutation, invalid-parameter, and X/Z detection campaigns | +| SymbiYosys | `operand_isolation_formal` | Complete combinational proof and formal cover reachability | +| EQY | `operand_isolation` | RTL-to-Yosys-netlist equivalence | +| Static frontends | `operand_isolation` | Style, formatting, elaboration, lint, and synthesizability | +| Static intent | Policy manifest | Matching SDC semantics and always-on UPF baseline | + +## Requirements Traceability + +| ID | Requirement | Simulation evidence | Assertion or formal evidence | +| --- | --- | --- | --- | +| `REQ-PASS-001` | `i_isolate=0` preserves `i_data` | Directed, one-hot, alternating, and deterministic sequences | Transparent equation assertion and formal proof | +| `REQ-CLAMP-001` | `i_isolate=1` drives `CLAMP_VALUE` | Every directed class and changing isolated inputs | Clamp equation assertion and formal proof | +| `REQ-INDEP-001` | Input changes cannot affect an isolated output | Long isolated activity intervals | Twin-input formal independence proof | +| `REQ-XCTL-001` | X/Z control is detected and propagates unknown output | Four-state qualification campaign | Unknown-control assertion | +| `REQ-PARAM-001` | Illegal width and unknown clamp are rejected | Negative elaboration fixtures | Static generate checks | +| `REQ-COMB-001` | No state affects the output | Back-to-back mode and data changes | Complete depth-one formal proof | +| `REQ-ACT-001` | Isolation reduces representative downstream activity | Three integration activity models | Not applicable | +| `REQ-SYN-001` | RTL synthesizes to combinational logic | Structural Yosys result | Yosys and lint gates | +| `REQ-EQY-001` | Generic netlist matches the RTL | Not applicable | EQY SAT strategy | + +## Parameter Matrix + +| Profile | Width | Clamp class | Portable evidence | +| --- | ---: | --- | --- | +| `width_1_zero` | 1 | Zero | Full flow plus negative and X/Z campaigns | +| `width_8_ones` | 8 | All one | Full portable flow | +| `width_16_pattern` | 16 | Nontrivial pattern | Full portable flow and representative coverage | +| `width_32_zero` | 32 | Zero | Full portable flow | +| `width_64_ones` | 64 | All one | Full portable flow | +| `width_128_pattern` | 128 | Nontrivial pattern | Full portable flow | +| `width_256_pattern` | 256 | Nontrivial pattern | Full portable flow | + +## Simulation Plan + +Each profile checks zero, all-one, alternating, one-hot, inverse one-hot, clamp, +and deterministic long sequences in both modes. The transition monitor covers +isolation assertion and deassertion with stable and changing data, input changes +within each mode, and back-to-back isolated samples. + +The integration test drives arithmetic, vector, and address-generation models. +It verifies active functional equality and compares downstream transition counts +under continuing isolated input activity. + +## Assertion and Formal Plan + +Bound assertions check the transparent and clamped equations and reject an +unknown isolation control. The formal harness instantiates two copies with +independent operands to prove that their outputs are equal whenever isolation is +asserted. The proof has no assumptions and completes at combinational depth one. + +Formal cover reuses the functional coverage wrapper to demonstrate reachability +of transparent, isolated, matching-clamp, and differing-clamp scenarios. + +## Negative and Four-State Qualification + +- A positive control proves the unit fixture can pass with nominal RTL. +- An inverted-control mutant must be detected by the same checker. +- `WIDTH=0` must fail elaboration. +- A clamp containing X or Z must fail elaboration. +- X and Z controls must reach the stimulus control when monitoring is disabled. +- The assertion monitor must fail for the same X and Z injections when enabled. + +## Coverage Goals + +- At least 95 percent scoped line coverage +- At least 80 percent scoped branch coverage +- At least 90 percent scoped toggle coverage +- 100 percent scoped user coverage +- Every named functional and integration coverpoint observed +- Formal cover reachability passes + +The reviewed line exclusion covers only the RTL default arm that propagates an +X/Z isolation control. Verilator cannot execute that arm in binary simulation, +so dedicated Icarus four-state campaigns provide its positive and negative +evidence. Any additional exclusion must identify an exact source counter, +technical reason, owner, and removal condition. + +## Exit Criteria + +- [ ] Every traced requirement has passing evidence. +- [ ] Every declared parameter profile passes its required flows. +- [ ] Mutation, invalid-parameter, and X/Z campaigns pass. +- [ ] Assertions and formal proofs pass without unreviewed assumptions. +- [ ] RTL-to-netlist equivalence passes. +- [ ] Coverage goals are met or deviations are approved. +- [ ] Static-intent validation passes. +- [ ] All waivers are recorded in [Reviewed waivers](waivers.md). +- [ ] The [release checklist](release-checklist.md) is complete. diff --git a/docs/operand_isolation/waivers.md b/docs/operand_isolation/waivers.md new file mode 100644 index 0000000..24577d1 --- /dev/null +++ b/docs/operand_isolation/waivers.md @@ -0,0 +1,44 @@ +# Reviewed Waivers + +[Return to the module documentation index](README.md). + +Each accepted waiver must identify the tool, rule, affected object, technical +justification, evidence, owner, reviewer, creation date, and expiration or +removal condition. + +## Accepted Waivers + +```text +ID: OI-COV-001 +Tool and rule: mosaic-flow coverage qualification, RTL line coverage +Affected file and object: rtl/operand_isolation.sv line 27, unknown-control default arm +Technical justification: Verilator coverage runs in binary simulation and cannot execute an X/Z control arm. Dedicated Icarus campaigns prove X and Z output propagation and assertion detection. +Evidence: reports/operand_isolation/width_1_zero/four_state_qualification and config/qualification-campaigns/operand_isolation.json +Owner: module-maintainers +Reviewer: Erick Andres Obregon Fonseca +Created: 2026-09-20 +Approved: 2026-09-20 +Expires or removal condition: Remove when the qualified coverage source records four-state RTL line execution. +``` + +```text +ID: OI-CI-001 +Tool and rule: GitHub Actions hosted execution and release-artifact retention +Affected file and object: Open-source RTL quality gate runs 35545096382 and 35545136959 for module revision 5c188f974296c2ca60f348a31ac305c1ec8bc5fb +Technical justification: GitHub rejected both runs before their first step because recent account payments failed or the spending limit must be increased. No module, profile, tool, or workflow command executed or failed. The exact 30-entry native and container module-profile matrix, module-specific OpenROAD and coverage steps, and all native and container release-manifest validations pass locally with the pinned methodology and Docker image. +Evidence: GitHub check-run annotations 106169472290 and 106169577949, ci-artifacts/local-native, ci-artifacts/local-native-special, ci-artifacts/local-container, ci-artifacts/local-container-special, reports, and work +Owner: module-maintainers and repository infrastructure owner +Reviewer: Erick Andres Obregon Fonseca +Created: 2026-09-20 +Approved: 2026-09-20 +Expires or removal condition: Re-run the complete hosted workflow and record its artifact IDs and retention dates when GitHub Actions billing or spending capacity is restored. +``` + +## Integration Deferrals + +Standalone CDC, RDC, DFT, VC LP, Design Compiler, PrimeTime, PrimePower, and +physical signoff are not represented as passing leaf checks. They require the +consuming datapath and its technology, clock, reset, test, power-state, and +activity context. Their leaf policy status is `SKIP`, and the transferred +requirements remain mandatory before an integration can claim signoff or power +savings. diff --git a/filelists/operand_isolation.assertions.f b/filelists/operand_isolation.assertions.f new file mode 100644 index 0000000..2a9cb43 --- /dev/null +++ b/filelists/operand_isolation.assertions.f @@ -0,0 +1,2 @@ +verif/assertions/operand_isolation_sva.sv +verif/assertions/operand_isolation_bind.sv diff --git a/filelists/operand_isolation.coverage.f b/filelists/operand_isolation.coverage.f new file mode 100644 index 0000000..a0ab9bf --- /dev/null +++ b/filelists/operand_isolation.coverage.f @@ -0,0 +1,4 @@ +verif/coverage/operand_isolation_coverage.sv +verif/coverage/operand_isolation_transition_coverage.sv +verif/coverage/operand_isolation_integration_coverage.sv +verif/coverage/operand_isolation_coverage_bind.sv diff --git a/filelists/operand_isolation.formal.f b/filelists/operand_isolation.formal.f new file mode 100644 index 0000000..66a9182 --- /dev/null +++ b/filelists/operand_isolation.formal.f @@ -0,0 +1,3 @@ +-f filelists/operand_isolation.rtl.f ++incdir+verif/properties +verif/formal/operand_isolation_formal.sv diff --git a/filelists/operand_isolation.properties.f b/filelists/operand_isolation.properties.f new file mode 100644 index 0000000..2dfc6d9 --- /dev/null +++ b/filelists/operand_isolation.properties.f @@ -0,0 +1 @@ ++incdir+verif/properties diff --git a/filelists/operand_isolation.rtl.f b/filelists/operand_isolation.rtl.f new file mode 100644 index 0000000..cae6988 --- /dev/null +++ b/filelists/operand_isolation.rtl.f @@ -0,0 +1,2 @@ ++incdir+rtl +rtl/operand_isolation.sv diff --git a/filelists/operand_isolation.tb.f b/filelists/operand_isolation.tb.f new file mode 100644 index 0000000..ec95abb --- /dev/null +++ b/filelists/operand_isolation.tb.f @@ -0,0 +1,5 @@ +-f filelists/operand_isolation.rtl.f ++incdir+verif +verif/tb/operand_isolation_test_case.sv +verif/tb/operand_isolation_activity_test_case.sv +verif/tb/operand_isolation_tb.sv diff --git a/flows/cdc/operand_isolation.constraints.tcl b/flows/cdc/operand_isolation.constraints.tcl new file mode 100644 index 0000000..856ab36 --- /dev/null +++ b/flows/cdc/operand_isolation.constraints.tcl @@ -0,0 +1,2 @@ +# operand_isolation has no clock, reset, state, or synchronization element. +# CDC remains an integration check for i_data and i_isolate at the consumer. diff --git a/flows/eqy/operand_isolation.equivalence.eqy b/flows/eqy/operand_isolation.equivalence.eqy new file mode 100644 index 0000000..e3615e4 --- /dev/null +++ b/flows/eqy/operand_isolation.equivalence.eqy @@ -0,0 +1,11 @@ +[gold] +read_verilog -sv rtl/operand_isolation.sv +prep -top operand_isolation + +[gate] +read_verilog work/operand_isolation/yosys_synthesis/operand_isolation_netlist.v +prep -top operand_isolation + +[strategy sat] +use sat +depth 1 diff --git a/flows/openroad/operand_isolation.config.mk b/flows/openroad/operand_isolation.config.mk new file mode 100644 index 0000000..74313af --- /dev/null +++ b/flows/openroad/operand_isolation.config.mk @@ -0,0 +1,11 @@ +# Exploratory physical setup for a representative WIDTH=16 pattern clamp. +export DESIGN_NAME = operand_isolation +export PLATFORM = $(OPENROAD_PLATFORM) +export VERILOG_FILES = $(REPO_ROOT)/rtl/operand_isolation.sv +export VERILOG_TOP_PARAMS = WIDTH 16 CLAMP_VALUE 16'ha55a +export SDC_FILE = $(OPENROAD_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/operand_isolation.timing.sdc b/flows/openroad/operand_isolation.timing.sdc new file mode 100644 index 0000000..11775c5 --- /dev/null +++ b/flows/openroad/operand_isolation.timing.sdc @@ -0,0 +1,11 @@ +# Match the synthesis 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_data*] \ + -to [get_ports o_data*] +set_max_delay 10.000 \ + -from [get_ports i_isolate] \ + -to [get_ports o_data*] diff --git a/flows/sg_dft/operand_isolation.constraints.tcl b/flows/sg_dft/operand_isolation.constraints.tcl new file mode 100644 index 0000000..ddc9b48 --- /dev/null +++ b/flows/sg_dft/operand_isolation.constraints.tcl @@ -0,0 +1,2 @@ +# operand_isolation has no state or test clock. Integration must make +# i_isolate controllable so transparent mode exposes the downstream datapath. diff --git a/flows/symbiyosys/operand_isolation.cover.sby b/flows/symbiyosys/operand_isolation.cover.sby new file mode 100644 index 0000000..473fa2b --- /dev/null +++ b/flows/symbiyosys/operand_isolation.cover.sby @@ -0,0 +1,16 @@ +[options] +mode cover +depth 2 + +[engines] +smtbmc bitwuzla + +[script] +read -formal -D MOSAIC_FORMAL -D MOSAIC_YOSYS_FORMAL -D FORMAL_COVERAGE -sv operand_isolation.sv operand_isolation_coverage.sv operand_isolation_coverage_bind.sv operand_isolation_formal.sv +prep -top operand_isolation_formal + +[files] +rtl/operand_isolation.sv +verif/coverage/operand_isolation_coverage.sv +verif/coverage/operand_isolation_coverage_bind.sv +verif/formal/operand_isolation_formal.sv diff --git a/flows/symbiyosys/operand_isolation.formal.sby b/flows/symbiyosys/operand_isolation.formal.sby new file mode 100644 index 0000000..f35dba8 --- /dev/null +++ b/flows/symbiyosys/operand_isolation.formal.sby @@ -0,0 +1,17 @@ +[options] +mode prove +depth 1 + +[engines] +smtbmc bitwuzla + +[script] +read -formal -D MOSAIC_FORMAL -D MOSAIC_YOSYS_FORMAL -D FORMAL_ASSERTIONS -sv operand_isolation.sv operand_isolation_sva.sv operand_isolation_bind.sv operand_isolation_formal.sv +prep -top operand_isolation_formal + +[files] +rtl/operand_isolation.sv +verif/properties/operand_isolation_predicates.svh +verif/assertions/operand_isolation_sva.sv +verif/assertions/operand_isolation_bind.sv +verif/formal/operand_isolation_formal.sv diff --git a/flows/synthesis/operand_isolation.timing.sdc b/flows/synthesis/operand_isolation.timing.sdc new file mode 100644 index 0000000..9afada9 --- /dev/null +++ b/flows/synthesis/operand_isolation.timing.sdc @@ -0,0 +1,14 @@ +# 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 both the operand and isolation-control paths visible in timing reports. +set_max_delay 10.000 \ + -from [get_ports i_data*] \ + -to [get_ports o_data*] +set_max_delay 10.000 \ + -from [get_ports i_isolate] \ + -to [get_ports o_data*] diff --git a/flows/vc_lp/operand_isolation.power.upf b/flows/vc_lp/operand_isolation.power.upf new file mode 100644 index 0000000..28d96ed --- /dev/null +++ b/flows/vc_lp/operand_isolation.power.upf @@ -0,0 +1,15 @@ +# Baseline always-on domain for the architectural operand-isolation leaf. +set_design_top operand_isolation +create_power_domain PD_OPERAND_ISOLATION -include_scope +create_supply_port VDD -domain PD_OPERAND_ISOLATION +create_supply_port VSS -domain PD_OPERAND_ISOLATION +create_supply_net VDD -domain PD_OPERAND_ISOLATION +create_supply_net VSS -domain PD_OPERAND_ISOLATION +connect_supply_net VDD -ports VDD +connect_supply_net VSS -ports VSS +set_domain_supply_net PD_OPERAND_ISOLATION \ + -primary_power_net VDD \ + -primary_ground_net VSS + +# This architectural clamp must not be credited as UPF isolation. Physical +# domain crossings and their strategies belong to the consuming hierarchy. diff --git a/rtl/operand_isolation.sv b/rtl/operand_isolation.sv new file mode 100644 index 0000000..d55f8ff --- /dev/null +++ b/rtl/operand_isolation.sv @@ -0,0 +1,31 @@ +/// Parameterizable architectural operand-isolation primitive. +/// +/// This module clamps an inactive operand before an expensive combinational +/// cone. It is not a replacement for UPF isolation at a power-domain boundary. +module operand_isolation #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + input logic [WIDTH-1:0] i_data, + input logic i_isolate, + output logic [WIDTH-1:0] o_data +); + + generate + if (WIDTH < 1) begin : g_invalid_width + operand_isolation_width_must_be_greater_than_zero invalid_width (); + end + if (^CLAMP_VALUE === 1'bx) begin : g_invalid_clamp_value + operand_isolation_clamp_value_must_be_known invalid_clamp_value (); + end + endgenerate + + always_comb begin + case (i_isolate) + 1'b0: o_data = i_data; + 1'b1: o_data = CLAMP_VALUE; + default: o_data = 'x; + endcase + end + +endmodule diff --git a/scripts/verible-format b/scripts/verible-format index 006f65a..ffb76cd 100755 --- a/scripts/verible-format +++ b/scripts/verible-format @@ -2,13 +2,13 @@ set -euo pipefail # Counter, reset synchronizer, lane mask, priority encoder, level shifter, -# isolation cell, retention register, and write gate sources use four-space -# indentation. +# isolation cell, retention register, write gate, and operand isolation 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 || "${source_file}" == *write_gate*.sv || "${source_file}" == *write_gate*.svh ]]; 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 || "${source_file}" == *operand_isolation*.sv || "${source_file}" == *operand_isolation*.svh ]]; then args=(--indentation_spaces=4 "${args[@]}") fi diff --git a/verif/assertions/operand_isolation_bind.sv b/verif/assertions/operand_isolation_bind.sv new file mode 100644 index 0000000..7f00d13 --- /dev/null +++ b/verif/assertions/operand_isolation_bind.sv @@ -0,0 +1,25 @@ +/// Stable boundary used to bind checks to every operand-isolation instance. +module operand_isolation_bind #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + input logic [WIDTH-1:0] i_data, + input logic i_isolate, + input logic [WIDTH-1:0] o_data +); + + operand_isolation_sva #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) i_operand_isolation_sva ( + .* + ); + +endmodule + +`ifndef MOSAIC_FORMAL +bind operand_isolation operand_isolation_bind #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) +) i_operand_isolation_bind (.*); +`endif diff --git a/verif/assertions/operand_isolation_sva.sv b/verif/assertions/operand_isolation_sva.sv new file mode 100644 index 0000000..702f09f --- /dev/null +++ b/verif/assertions/operand_isolation_sva.sv @@ -0,0 +1,42 @@ +/// Combinational operand-isolation checks shared by simulation and formal proof. +module operand_isolation_sva #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + input logic [WIDTH-1:0] i_data, + input logic i_isolate, + input logic [WIDTH-1:0] o_data +); + +`ifdef MOSAIC_YOSYS_FORMAL + always_comb begin + if (i_isolate) begin + assert (o_data == CLAMP_VALUE); + end else begin + assert (o_data == i_data); + end + end +`else + `include "operand_isolation_predicates.svh" + + always_comb begin + if (operand_isolation_control_known_f(i_isolate)) begin + assert (o_data === operand_isolation_expected_f(i_data, i_isolate, CLAMP_VALUE)) + else $fatal(1, "operand_isolation output equation failed"); + if (i_isolate) begin + assert (operand_isolation_clamped_f(o_data, CLAMP_VALUE)) + else $fatal(1, "operand_isolation failed to clamp an inactive operand"); + end else begin + assert (operand_isolation_transparent_f(i_data, o_data)) + else $fatal(1, "operand_isolation changed an active operand"); + end + end + +`ifndef OPERAND_ISOLATION_DISABLE_UNKNOWN_MONITOR + assert (!$isunknown(i_isolate)) + else $fatal(1, "operand_isolation isolation control is unknown"); +`endif + end +`endif + +endmodule diff --git a/verif/coverage/operand_isolation_coverage.sv b/verif/coverage/operand_isolation_coverage.sv new file mode 100644 index 0000000..e80c6b1 --- /dev/null +++ b/verif/coverage/operand_isolation_coverage.sv @@ -0,0 +1,22 @@ +/// Functional coverage for the operand-isolation combinational contract. +module operand_isolation_coverage #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + input logic [WIDTH-1:0] i_data, + input logic i_isolate, + input logic [WIDTH-1:0] o_data +); + + always_comb begin + transparent_mode : cover (!i_isolate && o_data == i_data); + isolation_mode : cover (i_isolate && o_data == CLAMP_VALUE); + transparent_zero : cover (!i_isolate && i_data == '0 && o_data == '0); + transparent_ones : cover (!i_isolate && i_data == '1 && o_data == '1); + isolated_input_differs : + cover (i_isolate && i_data != CLAMP_VALUE && o_data == CLAMP_VALUE); + isolated_input_matches : + cover (i_isolate && i_data == CLAMP_VALUE && o_data == CLAMP_VALUE); + end + +endmodule diff --git a/verif/coverage/operand_isolation_coverage_bind.sv b/verif/coverage/operand_isolation_coverage_bind.sv new file mode 100644 index 0000000..c37056c --- /dev/null +++ b/verif/coverage/operand_isolation_coverage_bind.sv @@ -0,0 +1,25 @@ +/// Stable boundary used to bind functional coverage to every DUT instance. +module operand_isolation_coverage_bind #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + input logic [WIDTH-1:0] i_data, + input logic i_isolate, + input logic [WIDTH-1:0] o_data +); + + operand_isolation_coverage #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) i_operand_isolation_coverage ( + .* + ); + +endmodule + +`ifndef MOSAIC_FORMAL +bind operand_isolation operand_isolation_coverage_bind #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) +) i_operand_isolation_coverage_bind (.*); +`endif diff --git a/verif/coverage/operand_isolation_integration_coverage.sv b/verif/coverage/operand_isolation_integration_coverage.sv new file mode 100644 index 0000000..7020993 --- /dev/null +++ b/verif/coverage/operand_isolation_integration_coverage.sv @@ -0,0 +1,27 @@ +/// Covers isolation state for representative downstream datapath classes. +module operand_isolation_integration_coverage #( + parameter int unsigned USE_CASE = 0 +) ( + input logic i_sample, + input logic i_isolate, + input logic i_input_changes +); + + if (USE_CASE == 0) begin : g_arithmetic + always @(posedge i_sample) begin + arithmetic_active : cover (!i_isolate); + arithmetic_isolated : cover (i_isolate && i_input_changes); + end + end else if (USE_CASE == 1) begin : g_vector + always @(posedge i_sample) begin + vector_active : cover (!i_isolate); + vector_isolated : cover (i_isolate && i_input_changes); + end + end else begin : g_address_generation + always @(posedge i_sample) begin + address_generation_active : cover (!i_isolate); + address_generation_isolated : cover (i_isolate && i_input_changes); + end + end + +endmodule diff --git a/verif/coverage/operand_isolation_transition_coverage.sv b/verif/coverage/operand_isolation_transition_coverage.sv new file mode 100644 index 0000000..9dd1502 --- /dev/null +++ b/verif/coverage/operand_isolation_transition_coverage.sv @@ -0,0 +1,41 @@ +/// Samples isolation transitions and concurrent operand activity. +module operand_isolation_transition_coverage #( + parameter int unsigned WIDTH = 32 +) ( + input logic i_sample, + input logic [WIDTH-1:0] i_data, + input logic i_isolate +); + + logic previous_valid; + logic previous_isolate; + logic [WIDTH-1:0] previous_data; + + initial begin + previous_valid = 1'b0; + previous_isolate = 1'b0; + previous_data = '0; + end + + always @(posedge i_sample) begin + if (previous_valid) begin + isolation_assert_data_stable : + cover (!previous_isolate && i_isolate && previous_data == i_data); + isolation_assert_data_changes : + cover (!previous_isolate && i_isolate && previous_data != i_data); + isolation_deassert_data_stable : + cover (previous_isolate && !i_isolate && previous_data == i_data); + isolation_deassert_data_changes : + cover (previous_isolate && !i_isolate && previous_data != i_data); + isolated_input_changes : + cover (previous_isolate && i_isolate && previous_data != i_data); + transparent_input_changes : + cover (!previous_isolate && !i_isolate && previous_data != i_data); + back_to_back_isolation : cover (previous_isolate && i_isolate); + end + previous_isolate = i_isolate; + previous_data = i_data; + previous_valid = 1'b1; + end + +endmodule diff --git a/verif/formal/operand_isolation_formal.sv b/verif/formal/operand_isolation_formal.sv new file mode 100644 index 0000000..788481a --- /dev/null +++ b/verif/formal/operand_isolation_formal.sv @@ -0,0 +1,60 @@ +/// Unconstrained harness proving the operand-isolation contract and input independence. +module operand_isolation_formal #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +); + + (* anyseq *)logic [WIDTH-1:0] i_data; + (* anyseq *)logic [WIDTH-1:0] independent_data; + (* anyseq *)logic i_isolate; + logic [WIDTH-1:0] o_data; + logic [WIDTH-1:0] independent_output; + + operand_isolation #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) dut ( + .i_data(i_data), + .i_isolate(i_isolate), + .o_data(o_data) + ); + + operand_isolation #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) independent_dut ( + .i_data(independent_data), + .i_isolate(i_isolate), + .o_data(independent_output) + ); + +`ifdef FORMAL_ASSERTIONS + operand_isolation_bind #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) i_operand_isolation_bind ( + .* + ); +`endif + +`ifdef FORMAL_COVERAGE + operand_isolation_coverage_bind #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) i_operand_isolation_coverage_bind ( + .* + ); +`endif + + always_comb begin + if (i_isolate) begin + assert (o_data == CLAMP_VALUE); + assert (independent_output == CLAMP_VALUE); + assert (o_data == independent_output); + end else begin + assert (o_data == i_data); + assert (independent_output == independent_data); + end + end + +endmodule diff --git a/verif/mutations/operand_isolation_inverted_control_mutant.sv b/verif/mutations/operand_isolation_inverted_control_mutant.sv new file mode 100644 index 0000000..1f1899f --- /dev/null +++ b/verif/mutations/operand_isolation_inverted_control_mutant.sv @@ -0,0 +1,19 @@ +// Verification-only mutation: isolation-control behavior is deliberately inverted. +module operand_isolation #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + input logic [WIDTH-1:0] i_data, + input logic i_isolate, + output logic [WIDTH-1:0] o_data +); + + always_comb begin + case (i_isolate) + 1'b0: o_data = CLAMP_VALUE; + 1'b1: o_data = i_data; + default: o_data = 'x; + endcase + end + +endmodule diff --git a/verif/properties/operand_isolation_predicates.svh b/verif/properties/operand_isolation_predicates.svh new file mode 100644 index 0000000..f19ce02 --- /dev/null +++ b/verif/properties/operand_isolation_predicates.svh @@ -0,0 +1,25 @@ +// Module-scoped predicates shared by operand-isolation checkers. +// This file has no include guard because each wrapper owns its declarations. + +function automatic logic [WIDTH-1:0] operand_isolation_expected_f( + input logic [WIDTH-1:0] data, input logic isolate, input logic [WIDTH-1:0] clamp_value); + case (isolate) + 1'b0: operand_isolation_expected_f = data; + 1'b1: operand_isolation_expected_f = clamp_value; + default: operand_isolation_expected_f = 'x; + endcase +endfunction + +function automatic logic operand_isolation_control_known_f(input logic isolate); + operand_isolation_control_known_f = !$isunknown(isolate); +endfunction + +function automatic logic operand_isolation_clamped_f(input logic [WIDTH-1:0] output_data, + input logic [WIDTH-1:0] clamp_value); + operand_isolation_clamped_f = (output_data === clamp_value); +endfunction + +function automatic logic operand_isolation_transparent_f(input logic [WIDTH-1:0] input_data, + input logic [WIDTH-1:0] output_data); + operand_isolation_transparent_f = (output_data === input_data); +endfunction diff --git a/verif/tb/operand_isolation_activity_test_case.sv b/verif/tb/operand_isolation_activity_test_case.sv new file mode 100644 index 0000000..74ad0d1 --- /dev/null +++ b/verif/tb/operand_isolation_activity_test_case.sv @@ -0,0 +1,122 @@ +/// Compares downstream combinational activity with and without operand isolation. +module operand_isolation_activity_test_case #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0, + parameter int unsigned USE_CASE = 0 +) ( + output logic o_done +); + + logic [WIDTH-1:0] i_data; + logic i_isolate; + logic [WIDTH-1:0] o_data; + logic [WIDTH-1:0] baseline_cone; + logic [WIDTH-1:0] isolated_cone; + logic [WIDTH-1:0] previous_data; + logic [WIDTH-1:0] previous_baseline_cone; + logic [WIDTH-1:0] previous_isolated_cone; + logic coverage_sample; + logic previous_valid; + longint unsigned baseline_toggles; + longint unsigned isolated_toggles; + + operand_isolation #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) dut ( + .* + ); + + function automatic logic [WIDTH-1:0] datapath_model(input logic [WIDTH-1:0] data); + case (USE_CASE) + 0: datapath_model = ~data; + 1: datapath_model = data ^ (data << 1); + default: datapath_model = data + WIDTH'(1); + endcase + 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 + + assign baseline_cone = datapath_model(i_data); + assign isolated_cone = datapath_model(o_data); + +`ifndef OPERAND_ISOLATION_DISABLE_COVERAGE + operand_isolation_integration_coverage #( + .USE_CASE(USE_CASE) + ) i_integration_coverage ( + .i_sample(coverage_sample), + .i_isolate(i_isolate), + .i_input_changes(previous_valid && previous_data != i_data) + ); +`endif + + task automatic apply_operand(input logic [WIDTH-1:0] data, input logic isolate); + i_data = data; + i_isolate = isolate; + #1ns; + + if (isolate) begin + assert (o_data == CLAMP_VALUE) + else $fatal(1, "USE_CASE=%0d isolated operand did not clamp", USE_CASE); + end else begin + assert (isolated_cone == baseline_cone) + else $fatal(1, "USE_CASE=%0d active datapath changed", USE_CASE); + end + + if (previous_valid) begin + baseline_toggles += count_set_bits(baseline_cone ^ previous_baseline_cone); + isolated_toggles += count_set_bits(isolated_cone ^ previous_isolated_cone); + end + coverage_sample = 1'b1; + #1ps; + coverage_sample = 1'b0; + previous_data = i_data; + previous_baseline_cone = baseline_cone; + previous_isolated_cone = isolated_cone; + previous_valid = 1'b1; + endtask + + initial begin + o_done = 1'b0; + i_data = '0; + i_isolate = 1'b0; + previous_data = '0; + previous_baseline_cone = '0; + previous_isolated_cone = '0; + coverage_sample = 1'b0; + previous_valid = 1'b0; + baseline_toggles = 0; + isolated_toggles = 0; + + apply_operand('0, 1'b0); + apply_operand('1, 1'b0); + apply_operand(CLAMP_VALUE, 1'b1); + repeat (32) begin + apply_operand('0, 1'b1); + apply_operand('1, 1'b1); + end + apply_operand('1, 1'b0); + apply_operand('0, 1'b0); + + assert (isolated_toggles < baseline_toggles) + else + $fatal( + 1, + "USE_CASE=%0d isolation did not reduce downstream activity: baseline=%0d isolated=%0d", + USE_CASE, + baseline_toggles, + isolated_toggles + ); + + $display( + "OPERAND_ISOLATION_ACTIVITY use_case=%0d width=%0d baseline_toggles=%0d isolated_toggles=%0d", + USE_CASE, WIDTH, baseline_toggles, isolated_toggles); + o_done = 1'b1; + end + +endmodule diff --git a/verif/tb/operand_isolation_four_state_tb.sv b/verif/tb/operand_isolation_four_state_tb.sv new file mode 100644 index 0000000..a94bcae --- /dev/null +++ b/verif/tb/operand_isolation_four_state_tb.sv @@ -0,0 +1,42 @@ +/// Four-state qualification fixture for an illegal isolation control. +module operand_isolation_four_state_tb; + + logic [3:0] i_data = 4'ha; + logic i_isolate = 1'b0; + logic [3:0] o_data; + + operand_isolation #( + .WIDTH(4), + .CLAMP_VALUE(4'h5) + ) dut ( + .* + ); + + operand_isolation_sva #( + .WIDTH(4), + .CLAMP_VALUE(4'h5) + ) i_operand_isolation_sva ( + .* + ); + + initial begin + #1ns; +`ifdef OPERAND_ISOLATION_INJECT_Z + i_isolate = 1'bz; +`else + i_isolate = 1'bx; +`endif + #1ns; + +`ifdef OPERAND_ISOLATION_DISABLE_UNKNOWN_MONITOR + if (o_data !== 'x) begin + $fatal(1, "OPERAND_ISOLATION_UNKNOWN_OUTPUT_NOT_PROPAGATED"); + end + $display("OPERAND_ISOLATION_UNKNOWN_CONTROL_STIMULUS_REACHED"); + $finish; +`else + $fatal(1, "OPERAND_ISOLATION_UNKNOWN_CONTROL_MONITOR_DID_NOT_FIRE"); +`endif + end + +endmodule diff --git a/verif/tb/operand_isolation_invalid_clamp_tb.sv b/verif/tb/operand_isolation_invalid_clamp_tb.sv new file mode 100644 index 0000000..95e44ab --- /dev/null +++ b/verif/tb/operand_isolation_invalid_clamp_tb.sv @@ -0,0 +1,13 @@ +/// Elaboration-negative fixture for a clamp containing an unknown bit. +module operand_isolation_invalid_clamp_tb; + + operand_isolation #( + .WIDTH(4), +`ifdef OPERAND_ISOLATION_INVALID_CLAMP_Z + .CLAMP_VALUE(4'b0z01) +`else + .CLAMP_VALUE(4'b0x01) +`endif + ) dut (); + +endmodule diff --git a/verif/tb/operand_isolation_invalid_width_tb.sv b/verif/tb/operand_isolation_invalid_width_tb.sv new file mode 100644 index 0000000..c8c2543 --- /dev/null +++ b/verif/tb/operand_isolation_invalid_width_tb.sv @@ -0,0 +1,6 @@ +/// Elaboration-negative fixture for the unsupported WIDTH=0 configuration. +module operand_isolation_invalid_width_tb; + + operand_isolation #(.WIDTH(0)) dut (); + +endmodule diff --git a/verif/tb/operand_isolation_tb.sv b/verif/tb/operand_isolation_tb.sv new file mode 100644 index 0000000..b01b5f7 --- /dev/null +++ b/verif/tb/operand_isolation_tb.sv @@ -0,0 +1,38 @@ +/// Top-level regression for one profile-selected operand-isolation configuration. +module operand_isolation_tb #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +); + + logic [3:0] done; + + operand_isolation_test_case #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) u_unit ( + .o_done(done[0]) + ); + + for (genvar use_case = 0; use_case < 3; use_case++) begin : g_activity + operand_isolation_activity_test_case #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE), + .USE_CASE(use_case) + ) u_activity ( + .o_done(done[use_case+1]) + ); + end + + initial begin + wait (&done); + $display("PASS: operand_isolation WIDTH=%0d CLAMP_VALUE=%h regression completed", WIDTH, + CLAMP_VALUE); + $finish; + end + + initial begin + #20us; + $fatal(1, "operand_isolation WIDTH=%0d regression timed out", WIDTH); + end + +endmodule diff --git a/verif/tb/operand_isolation_test_case.sv b/verif/tb/operand_isolation_test_case.sv new file mode 100644 index 0000000..f5f3c7f --- /dev/null +++ b/verif/tb/operand_isolation_test_case.sv @@ -0,0 +1,115 @@ +/// Reusable self-checking unit test for one operand-isolation configuration. +module operand_isolation_test_case #( + parameter int unsigned WIDTH = 32, + parameter logic [WIDTH-1:0] CLAMP_VALUE = '0 +) ( + output logic o_done +); + + logic [WIDTH-1:0] i_data; + logic i_isolate; + logic [WIDTH-1:0] o_data; + logic coverage_sample; + + operand_isolation #( + .WIDTH(WIDTH), + .CLAMP_VALUE(CLAMP_VALUE) + ) dut ( + .* + ); + +`ifndef OPERAND_ISOLATION_DISABLE_COVERAGE + operand_isolation_transition_coverage #( + .WIDTH(WIDTH) + ) i_transition_coverage ( + .i_sample(coverage_sample), + .i_data(i_data), + .i_isolate(i_isolate) + ); +`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] deterministic_vector(input int unsigned index); + for (int unsigned bit_index = 0; bit_index < WIDTH; bit_index++) begin + deterministic_vector[bit_index] = index[(bit_index+(bit_index/7))%32] ^ bit_index[0]; + end + endfunction + + task automatic check_case(input logic [WIDTH-1:0] data, input logic isolate); + logic [WIDTH-1:0] expected; + + i_data = data; + i_isolate = isolate; + #1ns; + expected = isolate ? CLAMP_VALUE : data; + assert (o_data === expected) + else + $fatal( + 1, + "WIDTH=%0d CLAMP=%h data=%h isolate=%b expected=%h actual=%h", + WIDTH, + CLAMP_VALUE, + data, + isolate, + expected, + o_data + ); + 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, 1'b0); + check_case('1, 1'b0); + check_case('0, 1'b1); + check_case('1, 1'b1); + check_case(CLAMP_VALUE, 1'b1); + check_case(alternating_zero, 1'b0); + check_case(alternating_one, 1'b0); + check_case(alternating_zero, 1'b1); + check_case(alternating_one, 1'b1); + + 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, 1'b0); + check_case(~one_hot, 1'b0); + check_case(one_hot, 1'b1); + check_case(~one_hot, 1'b1); + end + + // Exercise control transitions with both stable and changing operands. + check_case(alternating_zero, 1'b0); + check_case(alternating_zero, 1'b1); + check_case(alternating_one, 1'b0); + check_case(alternating_zero, 1'b1); + check_case(alternating_one, 1'b1); + check_case(alternating_one, 1'b0); + + repeat (4) begin + check_case(CLAMP_VALUE, 1'b1); + end + for (int unsigned iteration = 0; iteration < 128; iteration++) begin + check_case(deterministic_vector(iteration), iteration[0]); + end + + o_done = 1'b1; + end + +endmodule