From 4ef4f34f7df1e81b1e6e400cb86152488f1d60e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Erick=20Andr=C3=A9s=20Obreg=C3=B3n=20Fonseca?= Date: Tue, 29 Sep 2026 01:37:56 -0600 Subject: [PATCH 1/3] [Add] Parameterizable multiplexer and verification flows Implement a reusable N-to-1 data selector and qualify its portable open-source behavior. - Add parameterizable input count, data width, default output, validity reporting, fail-closed X/Z behavior, and elaboration-time parameter guards. - Add six qualified profiles covering one through eight inputs and one through 128 data bits, including non-power-of-two configurations. - Add legal, invalid, transition, randomized, and unknown-selection verification with selected and unselected input activity. - Add shared predicates, bound assertions, assumption-free formal proofs, reusable coverage, and RTL-to-Yosys-netlist equivalence checks. - Add functional, transition, line, branch, toggle, and formal coverage qualification with explicit release thresholds. - Add invalid-parameter, invalid-valid mutation, and four-state X/Z detection campaigns. - Add executable SDC and UPF static-intent checks plus CDC, DFT, synthesis, low-power, and exploratory physical collateral. - Register the mux in concurrent local, native GitHub Actions, and containerized module-profile execution. - Preserve representative coverage evidence in native and containerized release manifests. - Add interface, project configuration, power characterization, verification-plan, waiver, and template-aligned release documentation. - Record commercial and physical checks as reviewed portable skips that remain mandatory in the first consuming integration. - Verify all six profiles natively and in the pinned Docker environment, including coverage and release-manifest validation. --- .github/workflows/rtl-simulation.yml | 8 +- README.md | 1 + config/coverage-policies/mux.json | 35 +++ config/modules.json | 3 +- config/modules/mux-flows.mk | 36 +++ config/modules/mux.mk | 59 +++++ config/parameter-profiles/mux.json | 41 ++++ config/qualification-campaigns/mux.json | 135 +++++++++++ config/static-intent/mux.json | 28 +++ docs/README.md | 1 + docs/mux/README.md | 32 +++ docs/mux/interface.md | 75 ++++++ docs/mux/power-characterization.md | 41 ++++ docs/mux/project-configuration.md | 47 ++++ docs/mux/release-checklist.md | 252 ++++++++++++++++++++ docs/mux/verification-plan.md | 95 ++++++++ docs/mux/waivers.md | 12 + filelists/mux.assertions.f | 2 + filelists/mux.coverage.f | 3 + filelists/mux.formal.f | 3 + filelists/mux.properties.f | 1 + filelists/mux.rtl.f | 2 + filelists/mux.tb.f | 4 + flows/cdc/mux.constraints.tcl | 1 + flows/eqy/mux.equivalence.eqy | 14 ++ flows/openroad/mux.config.mk | 8 + flows/openroad/mux.timing.sdc | 6 + flows/sg_dft/mux.constraints.tcl | 1 + flows/symbiyosys/mux.cover.sby | 16 ++ flows/symbiyosys/mux.formal.sby | 17 ++ flows/synthesis/mux.timing.sdc | 6 + flows/vc_lp/mux.power.upf | 9 + rtl/mux.sv | 45 ++++ verif/assertions/mux_bind.sv | 34 +++ verif/assertions/mux_sva.sv | 47 ++++ verif/coverage/mux_coverage.sv | 41 ++++ verif/coverage/mux_coverage_bind.sv | 34 +++ verif/coverage/mux_transition_coverage.sv | 96 ++++++++ verif/formal/mux_formal.sv | 57 +++++ verif/mutations/mux_invalid_valid_mutant.sv | 25 ++ verif/properties/mux_predicates.svh | 18 ++ verif/tb/mux_four_state_tb.sv | 48 ++++ verif/tb/mux_invalid_data_width_tb.sv | 16 ++ verif/tb/mux_invalid_default_value_tb.sv | 17 ++ verif/tb/mux_invalid_num_inputs_tb.sv | 16 ++ verif/tb/mux_invalid_sel_width_tb.sv | 17 ++ verif/tb/mux_tb.sv | 34 +++ verif/tb/mux_test_case.sv | 152 ++++++++++++ 48 files changed, 1688 insertions(+), 3 deletions(-) create mode 100644 config/coverage-policies/mux.json create mode 100644 config/modules/mux-flows.mk create mode 100644 config/modules/mux.mk create mode 100644 config/parameter-profiles/mux.json create mode 100644 config/qualification-campaigns/mux.json create mode 100644 config/static-intent/mux.json create mode 100644 docs/mux/README.md create mode 100644 docs/mux/interface.md create mode 100644 docs/mux/power-characterization.md create mode 100644 docs/mux/project-configuration.md create mode 100644 docs/mux/release-checklist.md create mode 100644 docs/mux/verification-plan.md create mode 100644 docs/mux/waivers.md create mode 100644 filelists/mux.assertions.f create mode 100644 filelists/mux.coverage.f create mode 100644 filelists/mux.formal.f create mode 100644 filelists/mux.properties.f create mode 100644 filelists/mux.rtl.f create mode 100644 filelists/mux.tb.f create mode 100644 flows/cdc/mux.constraints.tcl create mode 100644 flows/eqy/mux.equivalence.eqy create mode 100644 flows/openroad/mux.config.mk create mode 100644 flows/openroad/mux.timing.sdc create mode 100644 flows/sg_dft/mux.constraints.tcl create mode 100644 flows/symbiyosys/mux.cover.sby create mode 100644 flows/symbiyosys/mux.formal.sby create mode 100644 flows/synthesis/mux.timing.sdc create mode 100644 flows/vc_lp/mux.power.upf create mode 100644 rtl/mux.sv create mode 100644 verif/assertions/mux_bind.sv create mode 100644 verif/assertions/mux_sva.sv create mode 100644 verif/coverage/mux_coverage.sv create mode 100644 verif/coverage/mux_coverage_bind.sv create mode 100644 verif/coverage/mux_transition_coverage.sv create mode 100644 verif/formal/mux_formal.sv create mode 100644 verif/mutations/mux_invalid_valid_mutant.sv create mode 100644 verif/properties/mux_predicates.svh create mode 100644 verif/tb/mux_four_state_tb.sv create mode 100644 verif/tb/mux_invalid_data_width_tb.sv create mode 100644 verif/tb/mux_invalid_default_value_tb.sv create mode 100644 verif/tb/mux_invalid_num_inputs_tb.sv create mode 100644 verif/tb/mux_invalid_sel_width_tb.sv create mode 100644 verif/tb/mux_tb.sv create mode 100644 verif/tb/mux_test_case.sv diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index bf011a8..e93471a 100644 --- a/.github/workflows/rtl-simulation.yml +++ b/.github/workflows/rtl-simulation.yml @@ -155,7 +155,7 @@ jobs: printf 'SKIP\n' > "${openroad_dir}/status.txt" - 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') || (matrix.module == 'decoder' && matrix.profile == 'outputs_3') + if: (matrix.module == 'write_gate' && matrix.profile == 'width_2') || (matrix.module == 'operand_isolation' && matrix.profile == 'width_16_pattern') || (matrix.module == 'decoder' && matrix.profile == 'outputs_3') || (matrix.module == 'mux' && matrix.profile == 'inputs_3_width_16') run: | set -o pipefail module="${{ matrix.module }}" @@ -178,6 +178,8 @@ jobs: export RELEASE_ADDITIONAL_EVIDENCE="reports/operand_isolation/width_16_pattern/coverage_qualification/forced-status.txt" elif [[ "${{ matrix.module }}" == decoder && "${{ matrix.profile }}" == outputs_3 ]]; then export RELEASE_ADDITIONAL_EVIDENCE="reports/decoder/outputs_3/coverage_qualification/forced-status.txt" + elif [[ "${{ matrix.module }}" == mux && "${{ matrix.profile }}" == inputs_3_width_16 ]]; then + export RELEASE_ADDITIONAL_EVIDENCE="reports/mux/inputs_3_width_16/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 @@ -280,7 +282,7 @@ jobs: 2>&1 | tee ci-artifacts/container-flow.log - 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') || (matrix.module == 'decoder' && matrix.profile == 'outputs_3') + if: (matrix.module == 'write_gate' && matrix.profile == 'width_2') || (matrix.module == 'operand_isolation' && matrix.profile == 'width_16_pattern') || (matrix.module == 'decoder' && matrix.profile == 'outputs_3') || (matrix.module == 'mux' && matrix.profile == 'inputs_3_width_16') run: | set -o pipefail module="${{ matrix.module }}" @@ -305,6 +307,8 @@ jobs: additional_evidence="reports/operand_isolation/width_16_pattern/coverage_qualification/forced-status.txt" elif [[ "${{ matrix.module }}" == decoder && "${{ matrix.profile }}" == outputs_3 ]]; then additional_evidence="reports/decoder/outputs_3/coverage_qualification/forced-status.txt" + elif [[ "${{ matrix.module }}" == mux && "${{ matrix.profile }}" == inputs_3_width_16 ]]; then + additional_evidence="reports/mux/inputs_3_width_16/coverage_qualification/forced-status.txt" fi docker run --rm \ --user "$(id -u):$(id -g)" \ diff --git a/README.md b/README.md index 8b35442..a7babf7 100644 --- a/README.md +++ b/README.md @@ -21,6 +21,7 @@ repository infrastructure and pinned [`mosaic-flow`](mosaic-flow) methodology. | `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/) | | `decoder` | Parameterizable binary-to-one-hot decoder with validity reporting | [`docs/decoder/`](docs/decoder/) | +| `mux` | Parameterizable N-to-1 data selector with validity reporting | [`docs/mux/`](docs/mux/) | 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/mux.json b/config/coverage-policies/mux.json new file mode 100644 index 0000000..b5180ba --- /dev/null +++ b/config/coverage-policies/mux.json @@ -0,0 +1,35 @@ +{ + "schema": "mosaic-coverage-policy-v1", + "scope": { + "include": [ + "rtl/mux.sv", + "verif/coverage/mux_coverage.sv", + "verif/coverage/mux_transition_coverage.sv" + ], + "exclude": [] + }, + "thresholds": { + "line": 95, + "branch": 90, + "toggle": 90, + "user": 100 + }, + "coverpoints": [ + {"name": "legal_selection", "minimum_hits": 1}, + {"name": "first_selection", "minimum_hits": 1}, + {"name": "last_selection", "minimum_hits": 1}, + {"name": "selected_zero", "minimum_hits": 1}, + {"name": "selected_all_ones", "minimum_hits": 1}, + {"name": "distinct_input_values", "minimum_hits": 1}, + {"name": "invalid_selection", "minimum_hits": 1}, + {"name": "legal_selection_changed", "minimum_hits": 1}, + {"name": "selected_input_changed", "minimum_hits": 1}, + {"name": "unselected_input_changed", "minimum_hits": 1}, + {"name": "legal_to_invalid", "minimum_hits": 1}, + {"name": "invalid_to_legal", "minimum_hits": 1}, + {"name": "all_selection_encodings", "minimum_hits": 1}, + {"name": "all_legal_selection_pairs", "minimum_hits": 1} + ], + "exclusions": [], + "formal": {"required": true} +} diff --git a/config/modules.json b/config/modules.json index 17425d7..a6816ec 100644 --- a/config/modules.json +++ b/config/modules.json @@ -12,6 +12,7 @@ {"name": "retention_register"}, {"name": "write_gate"}, {"name": "operand_isolation"}, - {"name": "decoder"} + {"name": "decoder"}, + {"name": "mux"} ] } diff --git a/config/modules/mux-flows.mk b/config/modules/mux-flows.mk new file mode 100644 index 0000000..a77c524 --- /dev/null +++ b/config/modules/mux-flows.mk @@ -0,0 +1,36 @@ +# Required portable checks for the technology-independent mux 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 + +# Clock-domain, scan, power-domain, mapped timing, power, and placement context +# belong to the first consuming block that uses the selected datapath. +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/mux.mk b/config/modules/mux.mk new file mode 100644 index 0000000..5aca036 --- /dev/null +++ b/config/modules/mux.mk @@ -0,0 +1,59 @@ +# Mux tops and design-owned flow inputs. +export DESIGN_TOP := mux +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/mux.sv \ + verif/properties/mux_predicates.svh \ + verif/assertions/mux_sva.sv \ + verif/assertions/mux_bind.sv \ + verif/coverage/mux_coverage.sv \ + verif/coverage/mux_transition_coverage.sv \ + verif/coverage/mux_coverage_bind.sv \ + verif/formal/mux_formal.sv \ + verif/mutations/mux_invalid_valid_mutant.sv \ + verif/tb/mux_test_case.sv \ + verif/tb/mux_tb.sv \ + verif/tb/mux_four_state_tb.sv \ + verif/tb/mux_invalid_num_inputs_tb.sv \ + verif/tb/mux_invalid_data_width_tb.sv \ + verif/tb/mux_invalid_sel_width_tb.sv \ + verif/tb/mux_invalid_default_value_tb.sv +export FORMAL_CONFIG := $(call resolve_flow_config,symbiyosys,formal.sby) +export FORMAL_COVER_CONFIG := $(MODULE_ROOT)/flows/symbiyosys/mux.cover.sby +export EQUIVALENCE_CONFIG := $(call resolve_flow_config,eqy,equivalence.eqy) +export COVERAGE_QUALIFICATION_POLICY := $(MODULE_ROOT)/config/coverage-policies/mux.json +export COVERAGE_QUALIFICATION_SOURCE := verilator_sim +export SIM_COVERAGE := enabled +export QUALIFICATION_CAMPAIGN_MANIFEST := $(MODULE_ROOT)/config/qualification-campaigns/mux.json +export STATIC_INTENT_CONFIG := $(MODULE_ROOT)/config/static-intent/mux.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/mux.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/mux.json b/config/parameter-profiles/mux.json new file mode 100644 index 0000000..4e90517 --- /dev/null +++ b/config/parameter-profiles/mux.json @@ -0,0 +1,41 @@ +{ + "schema": "mosaic-parameter-profiles-v1", + "include": [ + { + "name": "inputs_1_width_1", + "parameters": {"NUM_INPUTS": 1, "DATA_WIDTH": 1, "DEFAULT_VALUE": "1'b1"}, + "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": "mux", "testbench": "mux_tb", "formal": "mux_formal"} + }, + { + "name": "inputs_2_width_8", + "parameters": {"NUM_INPUTS": 2, "DATA_WIDTH": 8, "DEFAULT_VALUE": "8'ha5"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "mux", "testbench": "mux_tb", "formal": "mux_formal"} + }, + { + "name": "inputs_3_width_16", + "parameters": {"NUM_INPUTS": 3, "DATA_WIDTH": 16, "DEFAULT_VALUE": "16'hbeef"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "mux", "testbench": "mux_tb", "formal": "mux_formal"} + }, + { + "name": "inputs_4_width_32", + "parameters": {"NUM_INPUTS": 4, "DATA_WIDTH": 32, "DEFAULT_VALUE": "32'h00000000"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "mux", "testbench": "mux_tb", "formal": "mux_formal"} + }, + { + "name": "inputs_5_width_64", + "parameters": {"NUM_INPUTS": 5, "DATA_WIDTH": 64, "DEFAULT_VALUE": "64'ha5a55a5af0f00f0f"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "mux", "testbench": "mux_tb", "formal": "mux_formal"} + }, + { + "name": "inputs_8_width_128", + "parameters": {"NUM_INPUTS": 8, "DATA_WIDTH": 128, "DEFAULT_VALUE": "128'ha5a55a5af0f00f0f5a5aa5a50f0ff0f0"}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "mux", "testbench": "mux_tb", "formal": "mux_formal"} + } + ] +} diff --git a/config/qualification-campaigns/mux.json b/config/qualification-campaigns/mux.json new file mode 100644 index 0000000..af2b2bd --- /dev/null +++ b/config/qualification-campaigns/mux.json @@ -0,0 +1,135 @@ +{ + "schema": "mosaic-qualification-campaigns-v1", + "campaigns": { + "negative": { + "inputs": [ + "rtl/mux.sv", + "verif/mutations/mux_invalid_valid_mutant.sv", + "verif/tb/mux_test_case.sv", + "verif/tb/mux_invalid_num_inputs_tb.sv", + "verif/tb/mux_invalid_data_width_tb.sv", + "verif/tb/mux_invalid_sel_width_tb.sv", + "verif/tb/mux_invalid_default_value_tb.sv" + ], + "cases": [ + { + "id": "nominal_unit_regression", + "evidence": "nominal_unit_regression", + "role": "positive_control", + "kind": "simulation_control", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DMUX_DISABLE_COVERAGE", "-s", "mux_test_case", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/tb/mux_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success"} + ] + }, + { + "id": "invalid_valid_mutation", + "evidence": "invalid_valid_mutation", + "role": "negative", + "kind": "simulation_mutation", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DMUX_DISABLE_COVERAGE", "-s", "mux_test_case", "-o", "{case_work_dir}/simulation.vvp", "verif/mutations/mux_invalid_valid_mutant.sv", "verif/tb/mux_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "actual=", "failure_class": "assertion"} + ] + }, + { + "id": "invalid_num_inputs_elaboration", + "evidence": "invalid_num_inputs_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "mux_invalid_num_inputs_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/tb/mux_invalid_num_inputs_tb.sv"], "expected": "failure", "diagnostic": "mux_num_inputs_must_be_greater_than_zero", "failure_class": "elaboration"} + ] + }, + { + "id": "invalid_data_width_elaboration", + "evidence": "invalid_data_width_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "mux_invalid_data_width_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/tb/mux_invalid_data_width_tb.sv"], "expected": "failure", "diagnostic": "mux_data_width_must_be_greater_than_zero", "failure_class": "elaboration"} + ] + }, + { + "id": "invalid_sel_width_elaboration", + "evidence": "invalid_sel_width_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "mux_invalid_sel_width_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/tb/mux_invalid_sel_width_tb.sv"], "expected": "failure", "diagnostic": "mux_sel_width_must_match_num_inputs", "failure_class": "elaboration"} + ] + }, + { + "id": "invalid_default_value_elaboration", + "evidence": "invalid_default_value_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "mux_invalid_default_value_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/tb/mux_invalid_default_value_tb.sv"], "expected": "failure", "diagnostic": "mux_default_value_must_be_known", "failure_class": "elaboration"} + ] + } + ] + }, + "four_state": { + "simulator": "iverilog", + "inputs": [ + "rtl/mux.sv", + "verif/assertions/mux_sva.sv", + "verif/tb/mux_four_state_tb.sv" + ], + "cases": [ + { + "id": "disabled_unknown_select_x", + "evidence": "disabled_unknown_select_x", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_select", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DMUX_DISABLE_UNKNOWN_MONITOR", "-s", "mux_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/assertions/mux_sva.sv", "verif/tb/mux_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "MUX_UNKNOWN_SELECTION_FAIL_CLOSED_CONFIRMED"} + ] + }, + { + "id": "unknown_select_x", + "evidence": "unknown_select_x", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_unknown_select_x", + "injections": [{"control": "i_select", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-s", "mux_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/assertions/mux_sva.sv", "verif/tb/mux_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "mux selection contains an unknown value", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_high_impedance_select_z", + "evidence": "disabled_high_impedance_select_z", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_select", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DMUX_DISABLE_UNKNOWN_MONITOR", "-DMUX_INJECT_Z", "-s", "mux_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/assertions/mux_sva.sv", "verif/tb/mux_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "MUX_UNKNOWN_SELECTION_FAIL_CLOSED_CONFIRMED"} + ] + }, + { + "id": "high_impedance_select_z", + "evidence": "high_impedance_select_z", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_high_impedance_select_z", + "injections": [{"control": "i_select", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DMUX_INJECT_Z", "-s", "mux_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/mux.sv", "verif/assertions/mux_sva.sv", "verif/tb/mux_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "mux selection contains an unknown value", "failure_class": "unknown_control"} + ] + } + ] + } + } +} diff --git a/config/static-intent/mux.json b/config/static-intent/mux.json new file mode 100644 index 0000000..515e472 --- /dev/null +++ b/config/static-intent/mux.json @@ -0,0 +1,28 @@ +{ + "schema": "mosaic-static-intent-v1", + "sdc": { + "profiles": [ + {"name": "synthesis", "path": "flows/synthesis/mux.timing.sdc", "kind": "combinational"}, + {"name": "physical", "path": "flows/openroad/mux.timing.sdc", "kind": "combinational"} + ], + "consistency": [ + { + "profiles": ["synthesis", "physical"], + "commands": ["set_input_transition", "set_load", "set_max_delay"] + } + ] + }, + "upf": { + "path": "flows/vc_lp/mux.power.upf", + "top": "mux", + "mode": "always_on", + "required": { + "power_domains": ["PD_MUX"], + "supply_ports": ["VDD", "VSS"], + "supply_nets": ["VDD", "VSS"], + "supply_connections": ["VDD", "VSS"], + "domain_supplies": ["PD_MUX"] + }, + "forbidden_strategies": ["isolation", "level_shifting", "retention", "power_switch"] + } +} diff --git a/docs/README.md b/docs/README.md index e3fe4fa..8556653 100644 --- a/docs/README.md +++ b/docs/README.md @@ -8,6 +8,7 @@ - [Parameterizable write gate](write_gate/README.md) - [Parameterizable operand isolation](operand_isolation/README.md) - [Parameterizable decoder](decoder/README.md) +- [Parameterizable multiplexer](mux/README.md) ## Template documentation diff --git a/docs/mux/README.md b/docs/mux/README.md new file mode 100644 index 0000000..5bc70c7 --- /dev/null +++ b/docs/mux/README.md @@ -0,0 +1,32 @@ +# Parameterizable Multiplexer + +`mux` is a zero-latency, combinational N-to-1 selector for datapath operands, +results, bypass paths, configuration words, predicates, and routing data. Legal +selections forward exactly one input. Invalid or unknown selections return the +configured default and deassert `o_select_valid`. + +## Documentation + +- [Interface specification](interface.md) +- [Verification plan](verification-plan.md) +- [Project configuration](project-configuration.md) +- [Power characterization](power-characterization.md) +- [Release checklist](release-checklist.md) +- [Reviewed waivers](waivers.md) + +## Qualified configurations + +The parameter matrix covers one, two, three, four, five, and eight inputs with +data widths from one to 128 bits. It includes power-of-two and non-power-of-two +input counts, nonzero default values, and the `NUM_INPUTS=1` boundary. + +## Run locally + +```sh +make MODULE=mux PROFILE=inputs_3_width_16 flow-config-check +make MODULE=mux clean all-profiles PROFILE_JOBS=4 +make MODULE=mux PROFILE=inputs_3_width_16 FORCE_FLOW=1 open-coverage +``` + +Generated reports and work products are isolated below `reports/mux/` and +`work/mux/`. diff --git a/docs/mux/interface.md b/docs/mux/interface.md new file mode 100644 index 0000000..5987051 --- /dev/null +++ b/docs/mux/interface.md @@ -0,0 +1,75 @@ +# Interface Specification + +[Return to the module documentation index](README.md). + +## Overview + +`mux` selects one fixed-width input word using a binary index. The leaf is +purely combinational and has no clock, reset, state, handshake, or backpressure. + +The primitive does not validate opcodes, routes, datatypes, contexts, source +domains, or protocol legality. Those policies remain with the consumer. + +## Parameters + +| Parameter | Default | Legal values | Description | +| --- | ---: | --- | --- | +| `NUM_INPUTS` | `2` | Integers greater than or equal to `1` | Number of selectable words | +| `DATA_WIDTH` | `32` | Integers greater than or equal to `1` | Width of each input and `o_data` | +| `DEFAULT_VALUE` | `'0` | Known zero and one bits fitting `DATA_WIDTH` | Value returned for an invalid or unknown selection | +| `SEL_WIDTH` | Derived | `(NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1` | Binary selection width | + +Overriding `SEL_WIDTH` with a value other than the derived width is illegal. +Unknown or high-impedance bits in `DEFAULT_VALUE` are illegal because they +would violate the deterministic fail-closed contract. + +## Ports + +| Port | Direction | Width | Description | +| --- | --- | ---: | --- | +| `i_data` | Input | `NUM_INPUTS x DATA_WIDTH` | Packed collection of selectable words | +| `i_select` | Input | `SEL_WIDTH` | Binary selection index | +| `o_data` | Output | `DATA_WIDTH` | Selected word or `DEFAULT_VALUE` | +| `o_select_valid` | Output | `1` | Indicates that `i_select` is known and in range | + +The declaration order is +`logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data`. Selection zero maps to +`i_data[0]`. Selection `N` maps to `i_data[N]`. + +## Behavior + +| Condition | `o_data` | `o_select_valid` | +| --- | --- | ---: | +| Known `i_select < NUM_INPUTS` | `i_data[i_select]` | `1` | +| Out-of-range binary selection | `DEFAULT_VALUE` | `0` | +| Selection contains X or Z | `DEFAULT_VALUE` | `0` | + +For `NUM_INPUTS=1`, `SEL_WIDTH` remains one bit. Selection zero is legal and +selection one is invalid. + +Changes on unselected inputs do not change the functional value of `o_data`. +They can still consume dynamic power in upstream logic or physical routing. + +## Timing Contract + +- Architectural latency is zero cycles. +- Initiation interval is one cycle between surrounding registered stages. +- Timing paths exist from every data input to `o_data`. +- Timing paths exist from `i_select` to `o_data` and `o_select_valid`. +- No false path, multicycle path, asynchronous exception, clock uncertainty, or + reset exception applies inside the leaf. + +Large fan-in or width values can exceed a consuming block's timing target. A +pipelined or hierarchical selector changes the latency contract and must use a +different module. + +## Integration Contract + +- Data and selection must be coherent in the consuming clock-domain context. +- Asynchronous inputs must be synchronized or protected before this leaf. +- Unrelated clock or voltage domains must not be combined without integration + analysis and the required crossing cells. +- `o_select_valid` may be left unconnected only when configuration validation + proves every runtime selection legal. +- Operand isolation belongs before high-capacitance sources when the system + needs to suppress upstream switching. diff --git a/docs/mux/power-characterization.md b/docs/mux/power-characterization.md new file mode 100644 index 0000000..061033f --- /dev/null +++ b/docs/mux/power-characterization.md @@ -0,0 +1,41 @@ +# Power Characterization + +[Return to the module documentation index](README.md). + +## Standalone Scope + +The mux has no clock or sequential state, so clock gating, retention, and +state-save energy do not apply. Portable verification proves only functional +selection behavior and switching coverage. It does not claim a technology- +specific power result. + +## Relevant Activity + +Dynamic power depends on: + +- Toggle rates and correlation of every `i_data` word +- Selection transition rate and transition distance +- Input count and data width +- Logic structure chosen by synthesis +- Fanout and physical routing of `o_data` and `o_select_valid` +- Glitch propagation from data and selection paths + +Unselected input changes do not change the functional output, but they may +still toggle upstream logic and internal implementation nodes. Operand +isolation is an integration technique and is intentionally not embedded here. + +## Required Integration Evidence + +Before a consumer claims an energy benefit, it must use mapped libraries and +representative annotated activity to review: + +- Dynamic and leakage power +- SAIF hierarchy and annotation coverage +- Data-to-output and selection-to-output delay +- Area and logic depth +- Glitch activity after implementation +- Isolation and level-shifting for actual voltage-domain crossings + +PrimePower or an equivalent signoff flow belongs to the consuming physical +implementation because the standalone leaf has no selected PDK, corner, +placement, routing, or workload activity model. diff --git a/docs/mux/project-configuration.md b/docs/mux/project-configuration.md new file mode 100644 index 0000000..57f5c74 --- /dev/null +++ b/docs/mux/project-configuration.md @@ -0,0 +1,47 @@ +# Project Configuration + +[Return to the module documentation index](README.md). + +The module is registered as `mux` in `config/modules.json`. Its tops, filelists, +flow inputs, and output paths are defined by `config/modules/mux.mk`. Required +and disabled adapters are defined by `config/modules/mux-flows.mk`. + +## Portable Release Policy + +The standalone leaf requires: + +- Verible lint and formatting +- Slang elaboration +- Verilator lint and self-checking simulation +- Yosys generic synthesis +- SymbiYosys proof and cover reachability +- EQY RTL-to-netlist equivalence +- Negative and four-state qualification campaigns +- Portable SDC and UPF static-intent validation +- Representative code, toggle, user, and formal coverage qualification + +The six supported elaborations are declared in +`config/parameter-profiles/mux.json`. The representative coverage profile is +`inputs_3_width_16`. + +## Integration-Owned Checks + +Standalone policy disables VC Lint, CDC, SpyGlass DFT, VC LP, Design Compiler, +PrimeTime, PrimePower, and OpenROAD. The leaf has no state, clock, reset, scan +element, internal domain crossing, or independent physical boundary. + +Those checks remain required where the consuming design selects libraries, +operating corners, source and destination domains, test intent, power states, +loads, placement, routing, and representative activity. A disabled adapter is +a reviewed `SKIP`, never a `PASS`. + +## Evidence Paths + +```text +reports/mux// +work/mux// +``` + +Use `make MODULE=mux PROFILE= flow-config-check` before interpreting +results. Release manifests must identify the module revision, pinned +`mosaic-flow` revision, selected parameters, tools, constraints, and evidence. diff --git a/docs/mux/release-checklist.md b/docs/mux/release-checklist.md new file mode 100644 index 0000000..cb6ef8a --- /dev/null +++ b/docs/mux/release-checklist.md @@ -0,0 +1,252 @@ +# Multiplexer Release Checklist + +Use this checklist for every supported mux 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 `mux` in `mosaic-common`. The Docker + image remains the common-module CI environment._ +- [x] Supported parameter values and configurations are listed. + _`NUM_INPUTS >= 1` and `DATA_WIDTH >= 1` are legal. `SEL_WIDTH` must retain + its derived value and `DEFAULT_VALUE` must contain only known bits. Six + profiles cover one through eight inputs and one through 128 data bits._ +- [x] Unsupported modes and external assumptions are explicit. + _The leaf does not validate routes, opcodes, datatypes, domains, contexts, or + protocols. Integration owns source coherence, architectural legality, and + crossing protection._ +- [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`. + _Portable policy enables lint, formatting, elaboration, generic synthesis, + formal, equivalence, simulation, qualification campaigns, coverage, and + static-intent checks._ + +## Interface and Architecture + +- [x] [Interface specification](interface.md) matches the RTL. + _The documented parameters, packed input ordering, output equation, validity + output, fail-closed behavior, and bit ordering match `rtl/mux.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. + _Latency is zero cycles. There is no handshake or backpressure. Invalid and + unknown selections return `DEFAULT_VALUE` and deassert `o_select_valid`._ +- [x] Disabled, reset, test, and low-power behavior are documented. + _There is no enable, reset, or test mode. Functional output stability for + unselected input changes does not imply zero internal or upstream activity._ +- [x] Integration assumptions and protocol dependencies are reviewed. + _The consumer must provide coherent data and selection, validate higher-level + legality, and protect asynchronous or voltage-domain crossings._ + +## RTL Quality + +- [x] Verible style lint records `PASS` or an approved policy `SKIP`. +- [x] Verible formatting records the expected status. + _All mux-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. + _Every qualified profile synthesizes to combinational logic without a latch, + flip-flop, memory, loop, or unresolved reference._ +- [x] No unresolved warning is hidden outside the reviewed waiver files. + _The portable gate passes without a mux 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 regressions pass for all six declared profiles._ +- [x] Positive, negative, reset, error, and boundary tests pass. + _The regression exhausts all selection encodings with zero, one, and distinct + data, every ordered legal transition, selected and unselected data changes, + randomized activity, invalid parameters, a validity mutant, and X/Z controls. + Reset is not applicable._ +- [x] Assertions run in simulation and reach meaningful antecedents. + _Bound assertions check exact data and validity equations. Directed stimulus + reaches legal, invalid, boundary, data-change, and unknown-control cases._ +- [x] Formal assumptions are reviewed for overconstraint. + _The combinational proof leaves every data bit and selection bit unconstrained + and uses no assumptions._ +- [x] Formal proofs pass at justified depth or by complete proof. + _Depth-one complete combinational proofs pass for all six profiles._ +- [x] RTL-to-Yosys-netlist equivalence passes. +- [x] Functional and code coverage goals are met or deviations are approved. + _The representative three-input, 16-bit profile reaches 100 percent line, + branch, and user coverage, 95.4392 percent toggle coverage, all 14 required + sampled points, and all seven formal cover statements without exclusions._ + +## Constraints and Static Checks + +- [x] Synthesis and physical clocks agree unless a difference is documented. + _Both SDC files 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 data and selection 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 clock, reset, domain, or crossing. The consumer must + synchronize asynchronous controls and prove data-selection coherence._ +- [x] CDC violations are resolved or narrowly waived. + _CDC and RDC are policy `SKIP` at this combinational leaf. They remain required + in the 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, test mode, or internally generated clock. Integration + owns controllability and observability of the selected data paths._ +- [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`. Open-source lint and + portable static intent pass. Domain, test, and library-dependent checks move + to the consumer and no commercial `PASS` is claimed._ + +## 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 input-count and width profile. The + representative three-input, 16-bit profile maps to 66 generic combinational + cells and no state._ +- [x] PrimeTime reports no release-blocking setup or hold violation. + _Policy `SKIP` until launch and capture boundaries, target libraries, loads, + and operating corners are selected. No PrimeTime `PASS` is claimed._ +- [x] Unconstrained paths and constraint coverage are reviewed. + _Every input-to-output combination receives a maximum delay, with explicit + data-to-output and selection-to-output budgets._ +- [x] PrimePower uses representative SAIF activity. + _Policy `SKIP` at leaf level. PrimePower remains mandatory before a consumer + claims technology-specific energy savings._ +- [x] SAIF hierarchy and activity annotation coverage are reviewed. + _Portable regression measures functional and toggle coverage but does not + relabel those results as SAIF or power evidence._ +- [x] Power, performance, and area results meet the module targets. + _The portable target is correct combinational selection and functional output + stability for unselected data changes. Numeric PPA targets are deferred._ +- [x] PDK, library, tool, constraint, and corner identities are recorded. + _Portable evidence records tool and constraint identity. No PDK, mapped + library, operating corner, or signoff target is selected for this leaf._ + +## Physical Implementation + +- [x] OpenROAD or the selected implementation flow uses the intended platform. + _OpenROAD is a reviewed policy `SKIP` because physical implementation is not + part of the standalone mux release. Checked-in configuration is preliminary + integration collateral._ +- [x] Floorplan, utilization, aspect ratio, and margins are justified. + _Not applicable to the technology-independent leaf. These values depend on + placement with the register file, route network, or datapath it selects._ +- [x] Placement, clocking, routing, timing, DRC, and LVS evidence is retained when + physical implementation belongs to this module's release scope. + _Physical implementation does not belong to this leaf's release scope. The + consuming block must retain implementation and signoff evidence._ +- [x] Preliminary open-source physical results are not labeled as commercial + signoff evidence. + _No standalone physical result or foundry-signoff claim is made._ + +## 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 mux waivers to expire._ + +## Reproducibility and Evidence + +- [x] Native `make clean open-source` passes. + _`make MODULE=mux clean all-profiles PROFILE_JOBS=4` passes all six supported + profiles. Representative forced coverage qualification also passes._ +- [x] The pinned Docker image builds and its portable gate passes. + _Image `sha256:5d6dfaec931c37c2ea69c1103053e0c3eea34899f0692d09a2302ba5a2b426d9` + was built from pinned methodology revision `0bd222f` (`MF20260910V1`). All + six mux profiles, representative forced coverage, and the six container + manifest validations pass with the CI-equivalent commands._ +- [ ] GitHub Actions passes using the recorded gitlink revision. + _This requires a committed revision and completed native and container jobs + for that exact revision._ +- [x] Commercial gates pass in the authorized local or self-hosted environment. + _Commercial gates are reviewed policy `SKIP` for portable leaf qualification. + They remain mandatory where identified in consuming integration._ +- [x] Reports identify module revision, methodology revision, tool versions, + constraints, technology, date, and configuration. + _All six native and all six container diagnostic manifests validate. They + record base module revision `d907c79`, dirty-tree state, pinned methodology + revision `0bd222f`, profile parameters, technology context, input and evidence + hashes, generation date, and open-source tool versions. A clean committed + revision remains necessary for final GitHub release evidence._ +- [ ] CI or release storage retains logs and required databases. + _The workflow uploads native and container reports, work databases, and + diagnostics. Artifact IDs and retention dates require a committed run._ +- [x] No generated work database, credential, license, or proprietary library is + committed to Git. + +## Consuming-Integration Handoff + +- [x] The VC Lint disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: Verible, Verilator, Slang, Yosys, and formal checks cover the + standalone RTL. The consuming project may require VC Lint under its policy._ +- [x] The CDC and RDC disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the leaf has no clock, reset, state, or crossing. The + consumer must analyze domains that generate data and selection._ +- [x] The DFT disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: the leaf has no state, scan element, generated clock, or test + mode. The consumer must prove path controllability and observability._ +- [x] The VC LP disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: portable static intent validates one always-on leaf domain. + The consumer must analyze supplies, states, crossings, and required cells._ +- [x] The mapped synthesis and PrimeTime disposition is reviewed. + _Reviewed `SKIP`: generic synthesis proves a combinational implementation. + The consumer must map and close data and selection paths with chosen libraries, + loads, boundaries, and corners._ +- [x] The PrimePower disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: functional activity behavior is verified but no energy saving + is claimed. The consumer must use representative annotated activity._ +- [x] The physical-signoff disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: placement-dependent delay, fanout, congestion, glitches, + extraction, DRC, and LVS belong to the consuming implementation._ + +These reviewed skips close only their standalone policy decisions. Transferred +requirements remain mandatory before a tile, NoC router, register file, context +memory, functional unit, or other consumer can claim integration or silicon +signoff. + +## Known Methodology Limitation + +The pinned `mosaic-flow` profile schema does not accept +`coverage_qualification` in a parameter-profile flow list. CI therefore forces +coverage for `inputs_3_width_16`, preserves `forced-status.txt`, restores the +profile-owned status to `SKIP`, and indexes the passing evidence in the release +manifest. This enforced handoff is not a mux release deviation. + +## Final Commands + +```sh +git submodule status +make MODULE=mux PROFILE=inputs_3_width_16 flow-config-check +make MODULE=mux clean all-profiles PROFILE_JOBS=4 +make MODULE=mux PROFILE=inputs_3_width_16 FORCE_FLOW=1 open-coverage +make MODULE=mux PROFILE=inputs_3_width_16 release-manifest release-manifest-validate +``` + +Run commercial commands only in the licensed consuming environment after the +source and destination domains, 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/mux/verification-plan.md b/docs/mux/verification-plan.md new file mode 100644 index 0000000..8971620 --- /dev/null +++ b/docs/mux/verification-plan.md @@ -0,0 +1,95 @@ +# Verification Plan + +[Return to the module documentation index](README.md). + +## Objectives + +Verification establishes exact input selection, validity reporting, +deterministic invalid behavior, deterministic X/Z handling, non-power-of-two +support, parameter enforcement, and absence of retained state. + +## Requirements Traceability + +| ID | Requirement | Evidence | +| --- | --- | --- | +| `REQ-MUX-001` | Every legal selection forwards exactly the corresponding input | Exhaustive simulation, bound assertions, formal proof | +| `REQ-MUX-002` | Every invalid binary encoding returns `DEFAULT_VALUE` and invalid status | Non-power-of-two profiles, assertions, formal proof | +| `REQ-MUX-003` | Unknown or high-impedance selection fails closed and is detected | Icarus X/Z qualification campaign | +| `REQ-MUX-004` | Changes to selected data propagate | Directed and randomized simulation, assertions | +| `REQ-MUX-005` | Changes only to unselected data preserve the functional output | Directed transition test, exact output assertion | +| `REQ-MUX-006` | Minimum, wide, power-of-two, and non-power-of-two configurations work | Six parameter profiles | +| `REQ-MUX-007` | Illegal structural parameters fail elaboration | Negative qualification campaign | +| `REQ-MUX-008` | Synthesized logic preserves RTL behavior | Yosys synthesis and EQY | +| `REQ-MUX-009` | The leaf has no state, clock, reset, or broad timing exception | Static intent validation | + +## Parameter Matrix + +| Profile | `NUM_INPUTS` | `DATA_WIDTH` | Purpose | +| --- | ---: | ---: | --- | +| `inputs_1_width_1` | 1 | 1 | Minimum boundary and invalid selection one | +| `inputs_2_width_8` | 2 | 8 | Small power-of-two selector | +| `inputs_3_width_16` | 3 | 16 | Representative non-power-of-two coverage profile | +| `inputs_4_width_32` | 4 | 32 | Scalar datapath selector | +| `inputs_5_width_64` | 5 | 64 | Wider non-power-of-two selector | +| `inputs_8_width_128` | 8 | 128 | Vector datapath selector | + +Each profile uses a declared `DEFAULT_VALUE` and runs formatting, lint, +elaboration, generic synthesis, formal proof, equivalence, simulation, and +static-intent checks. The minimum profile also owns parameter-negative and +four-state qualification campaigns. + +## Simulation Plan + +For each profile, the self-checking test exhausts every selection encoding with +zero, one, and distinct input words. It exercises every ordered pair of legal +selections, selected-data changes, unselected-data changes, both invalid-region +boundaries when present, and deterministic randomized data and selection. + +The `NUM_INPUTS=1` profile proves that the derived selection width never becomes +zero. Non-power-of-two profiles prove that unused binary encodings do not wrap +or select an unintended input. + +## Assertion and Coverage Plan + +Assertions are bound to every `mux` instance and check the exact output and +validity equations. They also prove fail-closed output behavior for an unknown +selection and report unknown controls in four-state simulation. + +Coverage observes every legal input selection, first and last inputs, invalid +encodings, zero and all-one selected words, distinct input words, every ordered +legal transition, selected and unselected data changes, and legal-invalid +boundary transitions. Cumulative completion bins require all binary selection +encodings and all ordered legal selection pairs to occur. The representative +three-input profile qualifies code, toggle, user, and formal cover evidence. + +## Formal Plan + +The harness leaves every data bit and the selection unconstrained. A depth-one +complete combinational proof establishes exact selection and default behavior +without assumptions. Formal cover proves reachability of legal, boundary, +pattern, distinct-data, and invalid-selection scenarios. + +Selection-set and transition-matrix completion are sampled in simulation because +they require history. The formal model independently proves exact behavior for +every unconstrained data and selection value. + +## Negative and Four-State Qualification + +The negative campaign proves that the self-checking test rejects a mutant that +never asserts `o_select_valid`. It also confirms that zero input count, zero +data width, inconsistent `SEL_WIDTH`, and unknown `DEFAULT_VALUE` fail +elaboration with module-specific diagnostics. + +Pinned Icarus campaigns inject X and Z into `i_select`. Disabled-monitor cases +prove the RTL returns the configured default. Paired monitor cases prove the +verification layer detects the unknown selection. + +## Exit Criteria + +- [x] All six profiles pass their declared portable flow matrix. +- [x] Negative and four-state campaigns pass. +- [x] Assertions execute without unexpected failures. +- [x] Formal proof and RTL-to-netlist equivalence pass. +- [x] Coverage goals are met or narrowly reviewed. +- [x] Static timing and power intent validation passes. +- [ ] The release checklist is complete. diff --git a/docs/mux/waivers.md b/docs/mux/waivers.md new file mode 100644 index 0000000..aa67fa7 --- /dev/null +++ b/docs/mux/waivers.md @@ -0,0 +1,12 @@ +# Reviewed Waivers + +[Return to the module documentation index](README.md). + +Each waiver must record the tool and rule, affected object, technical +justification, evidence, owner, reviewer, creation date, and removal condition. + +## Accepted Waivers + +No mux waiver is currently accepted. + +Generated waiver drafts are diagnostic suggestions and are not approved policy. diff --git a/filelists/mux.assertions.f b/filelists/mux.assertions.f new file mode 100644 index 0000000..8c4c1a2 --- /dev/null +++ b/filelists/mux.assertions.f @@ -0,0 +1,2 @@ +verif/assertions/mux_sva.sv +verif/assertions/mux_bind.sv diff --git a/filelists/mux.coverage.f b/filelists/mux.coverage.f new file mode 100644 index 0000000..7d45d6b --- /dev/null +++ b/filelists/mux.coverage.f @@ -0,0 +1,3 @@ +verif/coverage/mux_coverage.sv +verif/coverage/mux_transition_coverage.sv +verif/coverage/mux_coverage_bind.sv diff --git a/filelists/mux.formal.f b/filelists/mux.formal.f new file mode 100644 index 0000000..d2851f9 --- /dev/null +++ b/filelists/mux.formal.f @@ -0,0 +1,3 @@ +-f filelists/mux.rtl.f ++incdir+verif/properties +verif/formal/mux_formal.sv diff --git a/filelists/mux.properties.f b/filelists/mux.properties.f new file mode 100644 index 0000000..2dfc6d9 --- /dev/null +++ b/filelists/mux.properties.f @@ -0,0 +1 @@ ++incdir+verif/properties diff --git a/filelists/mux.rtl.f b/filelists/mux.rtl.f new file mode 100644 index 0000000..5dba3b3 --- /dev/null +++ b/filelists/mux.rtl.f @@ -0,0 +1,2 @@ ++incdir+rtl +rtl/mux.sv diff --git a/filelists/mux.tb.f b/filelists/mux.tb.f new file mode 100644 index 0000000..4f44f4e --- /dev/null +++ b/filelists/mux.tb.f @@ -0,0 +1,4 @@ +-f filelists/mux.rtl.f ++incdir+verif +verif/tb/mux_test_case.sv +verif/tb/mux_tb.sv diff --git a/flows/cdc/mux.constraints.tcl b/flows/cdc/mux.constraints.tcl new file mode 100644 index 0000000..57a323b --- /dev/null +++ b/flows/cdc/mux.constraints.tcl @@ -0,0 +1 @@ +# Stateless combinational leaf with no internal clock, reset, or crossing. diff --git a/flows/eqy/mux.equivalence.eqy b/flows/eqy/mux.equivalence.eqy new file mode 100644 index 0000000..5084e9d --- /dev/null +++ b/flows/eqy/mux.equivalence.eqy @@ -0,0 +1,14 @@ +[gold] +read_verilog -sv rtl/mux.sv +prep -top mux + +[gate] +read_verilog work/mux/yosys_synthesis/mux_netlist.v +prep -top mux + +[collect mux] +group o_* + +[strategy sat] +use sat +depth 1 diff --git a/flows/openroad/mux.config.mk b/flows/openroad/mux.config.mk new file mode 100644 index 0000000..8da75e3 --- /dev/null +++ b/flows/openroad/mux.config.mk @@ -0,0 +1,8 @@ +export DESIGN_NAME := mux +export PLATFORM := nangate45 +export SDC_FILE := $(MODULE_ROOT)/flows/openroad/mux.timing.sdc +export CORE_UTILIZATION := 20 +export CORE_ASPECT_RATIO := 1 +export CORE_MARGIN := 5 +export DIE_AREA := 0 0 80 80 +export CORE_AREA := 5 5 75 75 diff --git a/flows/openroad/mux.timing.sdc b/flows/openroad/mux.timing.sdc new file mode 100644 index 0000000..221030d --- /dev/null +++ b/flows/openroad/mux.timing.sdc @@ -0,0 +1,6 @@ +# Preliminary combinational mux timing intent for OpenROAD. +set_input_transition 0.1 [all_inputs] +set_load 0.01 [all_outputs] +set_max_delay 5.0 -from [all_inputs] -to [all_outputs] +set_max_delay 4.0 -from [get_ports i_select*] -to [all_outputs] +set_max_delay 5.0 -from [get_ports i_data*] -to [get_ports o_data*] diff --git a/flows/sg_dft/mux.constraints.tcl b/flows/sg_dft/mux.constraints.tcl new file mode 100644 index 0000000..fe35326 --- /dev/null +++ b/flows/sg_dft/mux.constraints.tcl @@ -0,0 +1 @@ +# Stateless combinational leaf with no scan element or internal test mode. diff --git a/flows/symbiyosys/mux.cover.sby b/flows/symbiyosys/mux.cover.sby new file mode 100644 index 0000000..cacfe12 --- /dev/null +++ b/flows/symbiyosys/mux.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 mux.sv mux_coverage.sv mux_coverage_bind.sv mux_formal.sv +prep -top mux_formal + +[files] +rtl/mux.sv +verif/coverage/mux_coverage.sv +verif/coverage/mux_coverage_bind.sv +verif/formal/mux_formal.sv diff --git a/flows/symbiyosys/mux.formal.sby b/flows/symbiyosys/mux.formal.sby new file mode 100644 index 0000000..7b3c8b7 --- /dev/null +++ b/flows/symbiyosys/mux.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 mux.sv mux_sva.sv mux_bind.sv mux_formal.sv +prep -top mux_formal + +[files] +rtl/mux.sv +verif/properties/mux_predicates.svh +verif/assertions/mux_sva.sv +verif/assertions/mux_bind.sv +verif/formal/mux_formal.sv diff --git a/flows/synthesis/mux.timing.sdc b/flows/synthesis/mux.timing.sdc new file mode 100644 index 0000000..5555b68 --- /dev/null +++ b/flows/synthesis/mux.timing.sdc @@ -0,0 +1,6 @@ +# Combinational mux timing intent. +set_input_transition 0.1 [all_inputs] +set_load 0.01 [all_outputs] +set_max_delay 5.0 -from [all_inputs] -to [all_outputs] +set_max_delay 4.0 -from [get_ports i_select*] -to [all_outputs] +set_max_delay 5.0 -from [get_ports i_data*] -to [get_ports o_data*] diff --git a/flows/vc_lp/mux.power.upf b/flows/vc_lp/mux.power.upf new file mode 100644 index 0000000..9a08f92 --- /dev/null +++ b/flows/vc_lp/mux.power.upf @@ -0,0 +1,9 @@ +set_design_top mux +create_power_domain PD_MUX -include_scope +create_supply_port VDD -domain PD_MUX +create_supply_port VSS -domain PD_MUX +create_supply_net VDD -domain PD_MUX +create_supply_net VSS -domain PD_MUX +connect_supply_net VDD -ports VDD +connect_supply_net VSS -ports VSS +set_domain_supply_net PD_MUX -primary_power_net VDD -primary_ground_net VSS diff --git a/rtl/mux.sv b/rtl/mux.sv new file mode 100644 index 0000000..48c73c9 --- /dev/null +++ b/rtl/mux.sv @@ -0,0 +1,45 @@ +`timescale 1ns / 1ps + +/// Parameterizable N-to-1 multiplexer with fail-closed invalid handling. +module mux #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + output logic [DATA_WIDTH-1:0] o_data, + output logic o_select_valid +); + + localparam int unsigned ExpectedSelWidth = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1; + + generate + if (NUM_INPUTS < 1) begin : g_invalid_num_inputs + mux_num_inputs_must_be_greater_than_zero invalid_num_inputs (); + end + if (DATA_WIDTH < 1) begin : g_invalid_data_width + mux_data_width_must_be_greater_than_zero invalid_data_width (); + end + if (SEL_WIDTH != ExpectedSelWidth) begin : g_invalid_sel_width + mux_sel_width_must_match_num_inputs invalid_sel_width (); + end + if (^DEFAULT_VALUE === 1'bx) begin : g_invalid_default_value + mux_default_value_must_be_known invalid_default_value (); + end + endgenerate + + always_comb begin + o_data = DEFAULT_VALUE; + o_select_valid = 1'b0; + + // A four-state condition executes only for a known, legal selection. + // Unknown and out-of-range encodings therefore fail closed. + if ({1'b0, i_select} < (SEL_WIDTH + 1)'(NUM_INPUTS)) begin + o_data = i_data[i_select]; + o_select_valid = 1'b1; + end + end + +endmodule diff --git a/verif/assertions/mux_bind.sv b/verif/assertions/mux_bind.sv new file mode 100644 index 0000000..3e80f00 --- /dev/null +++ b/verif/assertions/mux_bind.sv @@ -0,0 +1,34 @@ +`timescale 1ns / 1ps + +/// Stable boundary used to bind checks to every mux instance. +module mux_bind #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + input logic [DATA_WIDTH-1:0] o_data, + input logic o_select_valid +); + + mux_sva #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) i_mux_sva ( + .* + ); + +endmodule + +`ifndef MOSAIC_FORMAL +bind mux mux_bind #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) +) i_mux_bind (.*); +`endif diff --git a/verif/assertions/mux_sva.sv b/verif/assertions/mux_sva.sv new file mode 100644 index 0000000..8264a70 --- /dev/null +++ b/verif/assertions/mux_sva.sv @@ -0,0 +1,47 @@ +`timescale 1ns / 1ps + +/// Combinational mux checks shared by simulation and formal proof. +module mux_sva #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + input logic [DATA_WIDTH-1:0] o_data, + input logic o_select_valid +); + +`ifdef MOSAIC_YOSYS_FORMAL + always_comb begin + if ({1'b0, i_select} < (SEL_WIDTH + 1)'(NUM_INPUTS)) begin + assert (o_data == i_data[i_select]); + assert (o_select_valid); + end else begin + assert (o_data == DEFAULT_VALUE); + assert (!o_select_valid); + end + end +`else + `include "mux_predicates.svh" + + always @(i_data, i_select, o_data, o_select_valid) begin + #1ps; + assert (o_data === mux_expected_f(i_data, i_select)) + else $fatal(1, "mux output equation failed"); + assert (o_select_valid === mux_selection_legal_f(i_select)) + else $fatal(1, "mux validity equation failed"); + + if (!mux_select_known_f(i_select)) begin + assert ((o_data === DEFAULT_VALUE) && (o_select_valid === 1'b0)) + else $fatal(1, "mux did not fail closed for an unknown selection"); + end +`ifndef MUX_DISABLE_UNKNOWN_MONITOR + assert (mux_select_known_f(i_select)) + else $fatal(1, "mux selection contains an unknown value"); +`endif + end +`endif + +endmodule diff --git a/verif/coverage/mux_coverage.sv b/verif/coverage/mux_coverage.sv new file mode 100644 index 0000000..1536003 --- /dev/null +++ b/verif/coverage/mux_coverage.sv @@ -0,0 +1,41 @@ +`timescale 1ns / 1ps + +/// Functional coverage for the mux's combinational contract. +module mux_coverage #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + input logic [DATA_WIDTH-1:0] o_data, + input logic o_select_valid +); + + always_comb begin + legal_selection : + cover (({1'b0, i_select} < (SEL_WIDTH + 1)'(NUM_INPUTS)) && o_select_valid); + first_selection : cover ((i_select == '0) && o_select_valid && (o_data == i_data[0])); + last_selection : + cover ((i_select == SEL_WIDTH'(NUM_INPUTS - 1)) && o_select_valid && + (o_data == i_data[NUM_INPUTS-1])); + selected_zero : cover (o_select_valid && (i_data[i_select] == '0) && (o_data == '0)); + selected_all_ones : cover (o_select_valid && (i_data[i_select] == '1) && (o_data == '1)); + end + + if (NUM_INPUTS > 1) begin : g_distinct_inputs + always_comb begin + distinct_input_values : cover (o_select_valid && (i_data[0] != i_data[NUM_INPUTS-1])); + end + end + + if ((64'(1) << SEL_WIDTH) > longint'(NUM_INPUTS)) begin : g_invalid_encoding + always_comb begin + invalid_selection : + cover (({1'b0, i_select} >= (SEL_WIDTH + 1)'(NUM_INPUTS)) && + (o_data == DEFAULT_VALUE) && !o_select_valid); + end + end + +endmodule diff --git a/verif/coverage/mux_coverage_bind.sv b/verif/coverage/mux_coverage_bind.sv new file mode 100644 index 0000000..deb35ed --- /dev/null +++ b/verif/coverage/mux_coverage_bind.sv @@ -0,0 +1,34 @@ +`timescale 1ns / 1ps + +/// Stable boundary used to bind functional coverage to every mux instance. +module mux_coverage_bind #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + input logic [DATA_WIDTH-1:0] o_data, + input logic o_select_valid +); + + mux_coverage #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) i_mux_coverage ( + .* + ); + +endmodule + +`ifndef MOSAIC_FORMAL +bind mux mux_coverage_bind #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) +) i_mux_coverage_bind (.*); +`endif diff --git a/verif/coverage/mux_transition_coverage.sv b/verif/coverage/mux_transition_coverage.sv new file mode 100644 index 0000000..871f236 --- /dev/null +++ b/verif/coverage/mux_transition_coverage.sv @@ -0,0 +1,96 @@ +`timescale 1ns / 1ps + +/// Sampled transition coverage driven by the self-checking mux test. +module mux_transition_coverage #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic i_sample, + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + input logic [DATA_WIDTH-1:0] o_data, + input logic o_select_valid +); + + localparam int unsigned NumEncodings = 1 << SEL_WIDTH; + localparam int unsigned NumLegalTransitions = NUM_INPUTS * NUM_INPUTS; + + logic previous_sample_valid; + logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] previous_data; + logic [SEL_WIDTH-1:0] previous_select; + logic [DATA_WIDTH-1:0] previous_output; + logic previous_select_valid; + logic [NumEncodings-1:0] observed_encodings; + logic [NumEncodings-1:0] encodings_with_current; + logic [NumLegalTransitions-1:0] observed_legal_transitions; + logic [NumLegalTransitions-1:0] legal_transitions_with_current; + + function automatic logic selection_legal(input logic [SEL_WIDTH-1:0] select); + selection_legal = {1'b0, select} < (SEL_WIDTH + 1)'(NUM_INPUTS); + endfunction + + initial begin + previous_sample_valid = 1'b0; + previous_data = '0; + previous_select = '0; + previous_output = '0; + previous_select_valid = 1'b0; + observed_encodings = '0; + observed_legal_transitions = '0; + end + + always_comb begin + encodings_with_current = observed_encodings; + encodings_with_current[i_select] = 1'b1; + + legal_transitions_with_current = observed_legal_transitions; + if (previous_sample_valid && previous_select_valid && o_select_valid) begin + legal_transitions_with_current[ + (int'(previous_select) * NUM_INPUTS) + int'(i_select) + ] = 1'b1; + end + end + + always @(posedge i_sample) begin + all_selection_encodings : cover (&encodings_with_current); + all_legal_selection_pairs : cover (&legal_transitions_with_current); + + if (previous_sample_valid) begin + legal_selection_changed : + cover (previous_select_valid && o_select_valid && (previous_select != i_select)); + selected_input_changed : + cover (previous_select_valid && o_select_valid && + (previous_select == i_select) && + (previous_data[i_select] != i_data[i_select]) && + (previous_output != o_data)); + unselected_input_changed : + cover (previous_select_valid && o_select_valid && + (previous_select == i_select) && + (previous_data[i_select] == i_data[i_select]) && + (previous_data != i_data) && (previous_output == o_data)); + end + + previous_sample_valid <= 1'b1; + previous_data <= i_data; + previous_select <= i_select; + previous_output <= o_data; + previous_select_valid <= o_select_valid; + observed_encodings <= encodings_with_current; + observed_legal_transitions <= legal_transitions_with_current; + end + + if ((64'(1) << SEL_WIDTH) > longint'(NUM_INPUTS)) begin : g_invalid_transitions + always @(posedge i_sample) begin + if (previous_sample_valid) begin + legal_to_invalid : + cover (previous_select_valid && !o_select_valid && !selection_legal(i_select)); + invalid_to_legal : + cover (!previous_select_valid && !selection_legal( + previous_select + ) && o_select_valid); + end + end + end + +endmodule diff --git a/verif/formal/mux_formal.sv b/verif/formal/mux_formal.sv new file mode 100644 index 0000000..9e3697c --- /dev/null +++ b/verif/formal/mux_formal.sv @@ -0,0 +1,57 @@ +`timescale 1ns / 1ps + +/// Unconstrained harness proving the N-to-1 mux contract. +module mux_formal #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +); + + (* anyseq *)logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data; + (* anyseq *)logic [ SEL_WIDTH-1:0] i_select; + logic [DATA_WIDTH-1:0] o_data; + logic o_select_valid; + + mux #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) dut ( + .* + ); + +`ifdef FORMAL_ASSERTIONS + mux_bind #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) i_mux_bind ( + .* + ); +`endif + +`ifdef FORMAL_COVERAGE + mux_coverage_bind #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) i_mux_coverage_bind ( + .* + ); +`endif + + always_comb begin + if ({1'b0, i_select} < (SEL_WIDTH + 1)'(NUM_INPUTS)) begin + assert (o_select_valid); + assert (o_data == i_data[i_select]); + end else begin + assert (!o_select_valid); + assert (o_data == DEFAULT_VALUE); + end + end + +endmodule diff --git a/verif/mutations/mux_invalid_valid_mutant.sv b/verif/mutations/mux_invalid_valid_mutant.sv new file mode 100644 index 0000000..331fea3 --- /dev/null +++ b/verif/mutations/mux_invalid_valid_mutant.sv @@ -0,0 +1,25 @@ +`timescale 1ns / 1ps + +/// Deliberately faulty mux used only to qualify the regression. +module mux #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data, + input logic [ SEL_WIDTH-1:0] i_select, + output logic [DATA_WIDTH-1:0] o_data, + output logic o_select_valid +); + + always_comb begin + o_data = DEFAULT_VALUE; + o_select_valid = 1'b0; + if ({1'b0, i_select} < (SEL_WIDTH + 1)'(NUM_INPUTS)) begin + o_data = i_data[i_select]; + o_select_valid = 1'b0; + end + end + +endmodule diff --git a/verif/properties/mux_predicates.svh b/verif/properties/mux_predicates.svh new file mode 100644 index 0000000..06c44ed --- /dev/null +++ b/verif/properties/mux_predicates.svh @@ -0,0 +1,18 @@ +// Module-scoped predicates shared by mux checkers. +// This file has no include guard because each wrapper owns its declarations. + +function automatic logic mux_select_known_f(input logic [SEL_WIDTH-1:0] select); + mux_select_known_f = !$isunknown(select); +endfunction + +function automatic logic mux_selection_legal_f(input logic [SEL_WIDTH-1:0] select); + mux_selection_legal_f = !$isunknown(select) && ({1'b0, select} < (SEL_WIDTH + 1)'(NUM_INPUTS)); +endfunction + +function automatic logic [DATA_WIDTH-1:0] mux_expected_f( + input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] data, input logic [SEL_WIDTH-1:0] select); + mux_expected_f = DEFAULT_VALUE; + if (mux_selection_legal_f(select)) begin + mux_expected_f = data[select]; + end +endfunction diff --git a/verif/tb/mux_four_state_tb.sv b/verif/tb/mux_four_state_tb.sv new file mode 100644 index 0000000..7d55de2 --- /dev/null +++ b/verif/tb/mux_four_state_tb.sv @@ -0,0 +1,48 @@ +`timescale 1ns / 1ps + +/// Four-state qualification for deterministic unknown-selection behavior. +module mux_four_state_tb; + + localparam logic [15:0] DefaultValue = 16'ha55a; + + logic [ 2:0][15:0] i_data = {16'h3333, 16'h2222, 16'h1111}; + logic [ 1:0] i_select = 2'b01; + logic [15:0] o_data; + logic o_select_valid; + + mux #( + .NUM_INPUTS (3), + .DATA_WIDTH (16), + .DEFAULT_VALUE(DefaultValue) + ) dut ( + .* + ); + + mux_sva #( + .NUM_INPUTS (3), + .DATA_WIDTH (16), + .DEFAULT_VALUE(DefaultValue) + ) i_mux_sva ( + .* + ); + + initial begin + #1ns; +`ifdef MUX_INJECT_Z + i_select = 'z; +`else + i_select = 'x; +`endif + #1ns; + + assert ((o_data === DefaultValue) && (o_select_valid === 1'b0)) + else $fatal(1, "MUX_UNKNOWN_SELECTION_DID_NOT_FAIL_CLOSED"); +`ifdef MUX_DISABLE_UNKNOWN_MONITOR + $display("MUX_UNKNOWN_SELECTION_FAIL_CLOSED_CONFIRMED"); + $finish; +`else + $fatal(1, "MUX_UNKNOWN_SELECTION_MONITOR_DID_NOT_FIRE"); +`endif + end + +endmodule diff --git a/verif/tb/mux_invalid_data_width_tb.sv b/verif/tb/mux_invalid_data_width_tb.sv new file mode 100644 index 0000000..5644064 --- /dev/null +++ b/verif/tb/mux_invalid_data_width_tb.sv @@ -0,0 +1,16 @@ +`timescale 1ns / 1ps + +/// Negative elaboration fixture for DATA_WIDTH=0. +module mux_invalid_data_width_tb; + logic [1:0] i_data; + logic i_select; + logic [1:0] o_data; + logic o_select_valid; + + mux #( + .NUM_INPUTS(2), + .DATA_WIDTH(0) + ) dut ( + .* + ); +endmodule diff --git a/verif/tb/mux_invalid_default_value_tb.sv b/verif/tb/mux_invalid_default_value_tb.sv new file mode 100644 index 0000000..a19a931 --- /dev/null +++ b/verif/tb/mux_invalid_default_value_tb.sv @@ -0,0 +1,17 @@ +`timescale 1ns / 1ps + +/// Negative elaboration fixture for an unknown DEFAULT_VALUE bit. +module mux_invalid_default_value_tb; + logic [2:0][3:0] i_data; + logic [1:0] i_select; + logic [3:0] o_data; + logic o_select_valid; + + mux #( + .NUM_INPUTS (3), + .DATA_WIDTH (4), + .DEFAULT_VALUE(4'b0x01) + ) dut ( + .* + ); +endmodule diff --git a/verif/tb/mux_invalid_num_inputs_tb.sv b/verif/tb/mux_invalid_num_inputs_tb.sv new file mode 100644 index 0000000..8c02cca --- /dev/null +++ b/verif/tb/mux_invalid_num_inputs_tb.sv @@ -0,0 +1,16 @@ +`timescale 1ns / 1ps + +/// Negative elaboration fixture for NUM_INPUTS=0. +module mux_invalid_num_inputs_tb; + logic [1:0][7:0] i_data; + logic i_select; + logic [7:0] o_data; + logic o_select_valid; + + mux #( + .NUM_INPUTS(0), + .DATA_WIDTH(8) + ) dut ( + .* + ); +endmodule diff --git a/verif/tb/mux_invalid_sel_width_tb.sv b/verif/tb/mux_invalid_sel_width_tb.sv new file mode 100644 index 0000000..5bc229e --- /dev/null +++ b/verif/tb/mux_invalid_sel_width_tb.sv @@ -0,0 +1,17 @@ +`timescale 1ns / 1ps + +/// Negative elaboration fixture for an overridden, inconsistent select width. +module mux_invalid_sel_width_tb; + logic [3:0][7:0] i_data; + logic [2:0] i_select; + logic [7:0] o_data; + logic o_select_valid; + + mux #( + .NUM_INPUTS(4), + .DATA_WIDTH(8), + .SEL_WIDTH (3) + ) dut ( + .* + ); +endmodule diff --git a/verif/tb/mux_tb.sv b/verif/tb/mux_tb.sv new file mode 100644 index 0000000..5652593 --- /dev/null +++ b/verif/tb/mux_tb.sv @@ -0,0 +1,34 @@ +`timescale 1ns / 1ps + +/// Top-level regression for one profile-selected mux configuration. +module mux_tb #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +); + + logic done; + + mux_test_case #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) u_unit ( + .o_done(done) + ); + + initial begin + wait (done); + $display("PASS: mux NUM_INPUTS=%0d DATA_WIDTH=%0d DEFAULT_VALUE=%h regression completed", + NUM_INPUTS, DATA_WIDTH, DEFAULT_VALUE); + $finish; + end + + initial begin + #100us; + $fatal(1, "mux NUM_INPUTS=%0d DATA_WIDTH=%0d regression timed out", NUM_INPUTS, DATA_WIDTH); + end + +endmodule diff --git a/verif/tb/mux_test_case.sv b/verif/tb/mux_test_case.sv new file mode 100644 index 0000000..2cf9702 --- /dev/null +++ b/verif/tb/mux_test_case.sv @@ -0,0 +1,152 @@ +`timescale 1ns / 1ps + +/// Reusable self-checking test for one mux parameter configuration. +module mux_test_case #( + parameter int unsigned NUM_INPUTS = 2, + parameter int unsigned DATA_WIDTH = 32, + parameter logic [DATA_WIDTH-1:0] DEFAULT_VALUE = '0, + parameter int unsigned SEL_WIDTH = (NUM_INPUTS > 1) ? $clog2(NUM_INPUTS) : 1 +) ( + output logic o_done +); + + localparam longint unsigned NumEncodings = 64'(1) << SEL_WIDTH; + + logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] i_data; + logic [ SEL_WIDTH-1:0] i_select; + logic [DATA_WIDTH-1:0] o_data; + logic o_select_valid; + logic coverage_sample; + integer random_seed; + + mux #( + .NUM_INPUTS (NUM_INPUTS), + .DATA_WIDTH (DATA_WIDTH), + .DEFAULT_VALUE(DEFAULT_VALUE), + .SEL_WIDTH (SEL_WIDTH) + ) dut ( + .* + ); + +`ifndef MUX_DISABLE_COVERAGE + mux_transition_coverage #( + .NUM_INPUTS(NUM_INPUTS), + .DATA_WIDTH(DATA_WIDTH), + .SEL_WIDTH (SEL_WIDTH) + ) i_transition_coverage ( + .i_sample(coverage_sample), + .* + ); +`endif + + function automatic logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] distinct_data_f(); + logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] value; + + value = '0; + for (int unsigned input_index = 0; input_index < NUM_INPUTS; input_index++) begin + value[input_index] = DATA_WIDTH'(input_index + 1); + end + return value; + endfunction + + function automatic logic [DATA_WIDTH-1:0] random_data_f(); + logic [DATA_WIDTH-1:0] value; + + for (int unsigned bit_index = 0; bit_index < DATA_WIDTH; bit_index++) begin + value[bit_index] = 1'($urandom_range(0, 1)); + end + return value; + endfunction + + task automatic check_case(input logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] data, + input longint unsigned selection); + logic [DATA_WIDTH-1:0] expected_data; + logic expected_valid; + + i_data = data; + i_select = SEL_WIDTH'(selection); + #1ns; + + expected_valid = selection < longint'(NUM_INPUTS); + expected_data = DEFAULT_VALUE; + if (expected_valid) begin + expected_data = data[SEL_WIDTH'(selection)]; + end + + assert ({o_select_valid, o_data} === {expected_valid, expected_data}) + else + $fatal( + 1, + "NUM_INPUTS=%0d DATA_WIDTH=%0d select=%0d expected=%b_%h actual=%b_%h", + NUM_INPUTS, + DATA_WIDTH, + selection, + expected_valid, + expected_data, + o_select_valid, + o_data + ); + coverage_sample = 1'b1; + #1ps; + coverage_sample = 1'b0; + endtask + + initial begin + logic [NUM_INPUTS-1:0][DATA_WIDTH-1:0] test_data; + logic [SEL_WIDTH-1:0] unselected_index; + + o_done = 1'b0; + i_data = '0; + i_select = '0; + coverage_sample = 1'b0; + + // Exhaust every selection encoding with zero, one, and distinct data. + for (longint unsigned selection = 0; selection < NumEncodings; selection++) begin + check_case('0, selection); + check_case('1, selection); + check_case(distinct_data_f(), selection); + end + + // Exercise every ordered transition between legal selections. + test_data = distinct_data_f(); + for (longint unsigned previous = 0; previous < longint'(NUM_INPUTS); previous++) begin + for (longint unsigned current = 0; current < longint'(NUM_INPUTS); current++) begin + check_case(test_data, previous); + check_case(test_data, current); + end + end + + // Prove selected data changes propagate and unselected changes do not. + test_data = distinct_data_f(); + check_case(test_data, 0); + test_data[0] = '1; + check_case(test_data, 0); + if (NUM_INPUTS > 1) begin + unselected_index = SEL_WIDTH'(1); + test_data = distinct_data_f(); + check_case(test_data, 0); + test_data[unselected_index] = ~test_data[unselected_index]; + check_case(test_data, 0); + end + + // Directly exercise both boundaries of the invalid-encoding region. + if (NumEncodings > longint'(NUM_INPUTS)) begin + check_case(test_data, longint'(NUM_INPUTS) - 1); + check_case(test_data, longint'(NUM_INPUTS)); + check_case(test_data, 0); + end + + // Exercise simultaneous data and selection changes with a fixed seed. + random_seed = 32'h4d55_5801 ^ NUM_INPUTS ^ DATA_WIDTH; + void'($urandom(random_seed)); + for (int unsigned iteration = 0; iteration < 128; iteration++) begin + for (int unsigned input_index = 0; input_index < NUM_INPUTS; input_index++) begin + test_data[input_index] = random_data_f(); + end + check_case(test_data, 64'($urandom()) % NumEncodings); + end + + o_done = 1'b1; + end + +endmodule From 894632882c53efd755657e51811a2d334c508b57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Erick=20Andr=C3=A9s=20Obreg=C3=B3n=20Fonseca?= Date: Tue, 29 Sep 2026 02:12:50 -0600 Subject: [PATCH 2/3] [Fix] Apply mux indentation policy in shared checks Keep repository-wide Verible checks aligned with the four-space mux source policy. - Recognize mux SystemVerilog sources in the shared formatting adapter. - Prevent unrelated module jobs from formatting mux files with Verible default two-space indentation. - Verify affected native and container format gates for counter, clock gate, reset synchronizer, retention register, and mux. --- scripts/verible-format | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/verible-format b/scripts/verible-format index 7bc81b6..94b762d 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, write gate, operand isolation, and decoder -# sources use four-space indentation. +# isolation cell, retention register, write gate, operand isolation, decoder, +# and mux 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 || "${source_file}" == *operand_isolation*.sv || "${source_file}" == *operand_isolation*.svh || "${source_file}" == *decoder*.sv || "${source_file}" == *decoder*.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 || "${source_file}" == *decoder*.sv || "${source_file}" == *decoder*.svh || "${source_file}" == *mux*.sv || "${source_file}" == *mux*.svh ]]; then args=(--indentation_spaces=4 "${args[@]}") fi From 1d2ad590f27134ba3476b313c658094d1ac8e17a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Erick=20Andr=C3=A9s=20Obreg=C3=B3n=20Fonseca?= Date: Tue, 29 Sep 2026 18:34:20 -0600 Subject: [PATCH 3/3] [Update] Complete multiplexer release checklist Close the final portable release requirements with successful hosted qualification evidence. - Reference push run 36541363113 and pull-request run 36541367519 for qualified branch revision 8946328 and pinned methodology revision 0bd222f. - Record clean native and container manifests, retained artifact IDs, and the December 28, 2026 retention date. - Complete the verification exit criteria and release checklist with no remaining open items. --- docs/mux/release-checklist.md | 27 ++++++++++++++++----------- docs/mux/verification-plan.md | 2 +- 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/docs/mux/release-checklist.md b/docs/mux/release-checklist.md index cb6ef8a..ec86dc4 100644 --- a/docs/mux/release-checklist.md +++ b/docs/mux/release-checklist.md @@ -174,22 +174,27 @@ gate alone is not sufficient ASIC release evidence. was built from pinned methodology revision `0bd222f` (`MF20260910V1`). All six mux profiles, representative forced coverage, and the six container manifest validations pass with the CI-equivalent commands._ -- [ ] GitHub Actions passes using the recorded gitlink revision. - _This requires a committed revision and completed native and container jobs - for that exact revision._ +- [x] GitHub Actions passes using the recorded gitlink revision. + _Push run `36541363113` and pull-request run `36541367519` each pass all + 89 jobs for branch revision `8946328` with pinned methodology revision + `0bd222f`. The pull request records 178 successful checks._ - [x] Commercial gates pass in the authorized local or self-hosted environment. _Commercial gates are reviewed policy `SKIP` for portable leaf qualification. They remain mandatory where identified in consuming integration._ - [x] Reports identify module revision, methodology revision, tool versions, constraints, technology, date, and configuration. - _All six native and all six container diagnostic manifests validate. They - record base module revision `d907c79`, dirty-tree state, pinned methodology - revision `0bd222f`, profile parameters, technology context, input and evidence - hashes, generation date, and open-source tool versions. A clean committed - revision remains necessary for final GitHub release evidence._ -- [ ] CI or release storage retains logs and required databases. - _The workflow uploads native and container reports, work databases, and - diagnostics. Artifact IDs and retention dates require a committed run._ + _All six native and all six container manifests from the successful push run + validate for clean module revision `8946328` and methodology revision + `0bd222f`. They record profile parameters, technology context, input and + evidence hashes, generation date, and open-source tool versions. The + pull-request manifests also validate for synthetic merge revision `7e06fc5`._ +- [x] CI or release storage retains logs and required databases. + _Each successful run retains 12 mux artifacts through December 28, 2026. + Native artifact `11021014669` and container artifact `11021033913` are the + representative `inputs_3_width_16` evidence from push run `36541363113`. + The native artifacts include reports, diagnostics, and work databases. The + container artifacts include reports, diagnostics, coverage, and validated + release manifests. The run pages record all artifact IDs._ - [x] No generated work database, credential, license, or proprietary library is committed to Git. diff --git a/docs/mux/verification-plan.md b/docs/mux/verification-plan.md index 8971620..5be91c7 100644 --- a/docs/mux/verification-plan.md +++ b/docs/mux/verification-plan.md @@ -92,4 +92,4 @@ verification layer detects the unknown selection. - [x] Formal proof and RTL-to-netlist equivalence pass. - [x] Coverage goals are met or narrowly reviewed. - [x] Static timing and power intent validation passes. -- [ ] The release checklist is complete. +- [x] The release checklist is complete.