diff --git a/.github/workflows/rtl-simulation.yml b/.github/workflows/rtl-simulation.yml index 9644262..bf011a8 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') + 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') run: | set -o pipefail module="${{ matrix.module }}" @@ -176,6 +176,8 @@ jobs: 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" + elif [[ "${{ matrix.module }}" == decoder && "${{ matrix.profile }}" == outputs_3 ]]; then + export RELEASE_ADDITIONAL_EVIDENCE="reports/decoder/outputs_3/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 @@ -278,7 +280,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') + 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') run: | set -o pipefail module="${{ matrix.module }}" @@ -301,6 +303,8 @@ jobs: 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" + elif [[ "${{ matrix.module }}" == decoder && "${{ matrix.profile }}" == outputs_3 ]]; then + additional_evidence="reports/decoder/outputs_3/coverage_qualification/forced-status.txt" fi docker run --rm \ --user "$(id -u):$(id -g)" \ diff --git a/README.md b/README.md index a3f139b..8b35442 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,7 @@ repository infrastructure and pinned [`mosaic-flow`](mosaic-flow) methodology. | `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/) | +| `decoder` | Parameterizable binary-to-one-hot decoder with validity reporting | [`docs/decoder/`](docs/decoder/) | 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/decoder.json b/config/coverage-policies/decoder.json new file mode 100644 index 0000000..b91ac33 --- /dev/null +++ b/config/coverage-policies/decoder.json @@ -0,0 +1,31 @@ +{ + "schema": "mosaic-coverage-policy-v1", + "scope": { + "include": [ + "rtl/decoder.sv", + "verif/coverage/decoder_coverage.sv", + "verif/coverage/decoder_transition_coverage.sv" + ], + "exclude": [] + }, + "thresholds": { + "line": 95, + "branch": 90, + "toggle": 90, + "user": 100 + }, + "coverpoints": [ + {"name": "disabled_operation", "minimum_hits": 1}, + {"name": "enabled_legal", "minimum_hits": 1}, + {"name": "first_selection", "minimum_hits": 1}, + {"name": "last_selection", "minimum_hits": 1}, + {"name": "any_output_selected", "minimum_hits": 1}, + {"name": "enable_asserted", "minimum_hits": 1}, + {"name": "enable_deasserted", "minimum_hits": 1}, + {"name": "legal_selection_changed", "minimum_hits": 1}, + {"name": "legal_to_invalid", "minimum_hits": 1}, + {"name": "invalid_to_legal", "minimum_hits": 1} + ], + "exclusions": [], + "formal": {"required": true} +} diff --git a/config/modules.json b/config/modules.json index e77b828..17425d7 100644 --- a/config/modules.json +++ b/config/modules.json @@ -11,6 +11,7 @@ {"name": "isolation_cell"}, {"name": "retention_register"}, {"name": "write_gate"}, - {"name": "operand_isolation"} + {"name": "operand_isolation"}, + {"name": "decoder"} ] } diff --git a/config/modules/decoder-flows.mk b/config/modules/decoder-flows.mk new file mode 100644 index 0000000..b044eee --- /dev/null +++ b/config/modules/decoder-flows.mk @@ -0,0 +1,36 @@ +# Required portable checks for the technology-independent decoder 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 decoded controls. +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/decoder.mk b/config/modules/decoder.mk new file mode 100644 index 0000000..a7b5f36 --- /dev/null +++ b/config/modules/decoder.mk @@ -0,0 +1,57 @@ +# Decoder tops and design-owned flow inputs. +export DESIGN_TOP := decoder +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/decoder.sv \ + verif/properties/decoder_predicates.svh \ + verif/assertions/decoder_sva.sv \ + verif/assertions/decoder_bind.sv \ + verif/coverage/decoder_coverage.sv \ + verif/coverage/decoder_transition_coverage.sv \ + verif/coverage/decoder_coverage_bind.sv \ + verif/formal/decoder_formal.sv \ + verif/mutations/decoder_inverted_enable_mutant.sv \ + verif/tb/decoder_test_case.sv \ + verif/tb/decoder_tb.sv \ + verif/tb/decoder_four_state_tb.sv \ + verif/tb/decoder_invalid_num_outputs_tb.sv \ + verif/tb/decoder_invalid_select_width_tb.sv +export FORMAL_CONFIG := $(call resolve_flow_config,symbiyosys,formal.sby) +export FORMAL_COVER_CONFIG := $(MODULE_ROOT)/flows/symbiyosys/decoder.cover.sby +export EQUIVALENCE_CONFIG := $(call resolve_flow_config,eqy,equivalence.eqy) +export COVERAGE_QUALIFICATION_POLICY := $(MODULE_ROOT)/config/coverage-policies/decoder.json +export COVERAGE_QUALIFICATION_SOURCE := verilator_sim +export SIM_COVERAGE := enabled +export QUALIFICATION_CAMPAIGN_MANIFEST := $(MODULE_ROOT)/config/qualification-campaigns/decoder.json +export STATIC_INTENT_CONFIG := $(MODULE_ROOT)/config/static-intent/decoder.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/decoder.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/decoder.json b/config/parameter-profiles/decoder.json new file mode 100644 index 0000000..5bc4496 --- /dev/null +++ b/config/parameter-profiles/decoder.json @@ -0,0 +1,53 @@ +{ + "schema": "mosaic-parameter-profiles-v1", + "include": [ + { + "name": "outputs_1", + "parameters": {"NUM_OUTPUTS": 1}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "negative_qualification", "four_state_qualification", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_2", + "parameters": {"NUM_OUTPUTS": 2}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_3", + "parameters": {"NUM_OUTPUTS": 3}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_4", + "parameters": {"NUM_OUTPUTS": 4}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_5", + "parameters": {"NUM_OUTPUTS": 5}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_8", + "parameters": {"NUM_OUTPUTS": 8}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_16", + "parameters": {"NUM_OUTPUTS": 16}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + }, + { + "name": "outputs_32", + "parameters": {"NUM_OUTPUTS": 32}, + "flows": ["verible_lint", "verible_format", "slang_elaboration", "verilator_lint", "yosys_synthesis", "symbiyosys_formal", "eqy_equivalence", "verilator_sim", "static_intent"], + "tops": {"design": "decoder", "testbench": "decoder_tb", "formal": "decoder_formal"} + } + ] +} diff --git a/config/qualification-campaigns/decoder.json b/config/qualification-campaigns/decoder.json new file mode 100644 index 0000000..fbcce3d --- /dev/null +++ b/config/qualification-campaigns/decoder.json @@ -0,0 +1,159 @@ +{ + "schema": "mosaic-qualification-campaigns-v1", + "campaigns": { + "negative": { + "inputs": [ + "rtl/decoder.sv", + "verif/mutations/decoder_inverted_enable_mutant.sv", + "verif/tb/decoder_test_case.sv", + "verif/tb/decoder_invalid_num_outputs_tb.sv", + "verif/tb/decoder_invalid_select_width_tb.sv" + ], + "cases": [ + { + "id": "nominal_unit_regression", + "evidence": "nominal_unit_regression", + "role": "positive_control", + "kind": "simulation_control", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DDECODER_DISABLE_COVERAGE", "-s", "decoder_test_case", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/tb/decoder_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success"} + ] + }, + { + "id": "inverted_enable_mutation", + "evidence": "inverted_enable_mutation", + "role": "negative", + "kind": "simulation_mutation", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-DDECODER_DISABLE_COVERAGE", "-s", "decoder_test_case", "-o", "{case_work_dir}/simulation.vvp", "verif/mutations/decoder_inverted_enable_mutant.sv", "verif/tb/decoder_test_case.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "actual=", "failure_class": "assertion"} + ] + }, + { + "id": "invalid_num_outputs_elaboration", + "evidence": "invalid_num_outputs_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "decoder_invalid_num_outputs_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/tb/decoder_invalid_num_outputs_tb.sv"], "expected": "failure", "diagnostic": "decoder_num_outputs_must_be_greater_than_zero", "failure_class": "elaboration"} + ] + }, + { + "id": "invalid_select_width_elaboration", + "evidence": "invalid_select_width_elaboration", + "role": "negative", + "kind": "invalid_parameter", + "positive_control": "nominal_unit_regression", + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-s", "decoder_invalid_select_width_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/tb/decoder_invalid_select_width_tb.sv"], "expected": "failure", "diagnostic": "decoder_select_width_must_match_num_outputs", "failure_class": "elaboration"} + ] + } + ] + }, + "four_state": { + "simulator": "iverilog", + "inputs": [ + "rtl/decoder.sv", + "verif/assertions/decoder_sva.sv", + "verif/tb/decoder_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", "-DDECODER_DISABLE_UNKNOWN_MONITOR", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "DECODER_UNKNOWN_CONTROL_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", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "decoder control 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", "-DDECODER_DISABLE_UNKNOWN_MONITOR", "-DDECODER_INJECT_Z", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "DECODER_UNKNOWN_CONTROL_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", "-DDECODER_INJECT_Z", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "decoder control contains an unknown value", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_unknown_enable_x", + "evidence": "disabled_unknown_enable_x", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_enable", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DDECODER_DISABLE_UNKNOWN_MONITOR", "-DDECODER_INJECT_ENABLE", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "DECODER_UNKNOWN_CONTROL_FAIL_CLOSED_CONFIRMED"} + ] + }, + { + "id": "unknown_enable_x", + "evidence": "unknown_enable_x", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_unknown_enable_x", + "injections": [{"control": "i_enable", "values": ["X"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DDECODER_INJECT_ENABLE", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "decoder control contains an unknown value", "failure_class": "unknown_control"} + ] + }, + { + "id": "disabled_high_impedance_enable_z", + "evidence": "disabled_high_impedance_enable_z", + "role": "disabled_monitor_control", + "kind": "stimulus_control", + "injections": [{"control": "i_enable", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DDECODER_DISABLE_UNKNOWN_MONITOR", "-DDECODER_INJECT_ENABLE", "-DDECODER_INJECT_Z", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "success", "diagnostic": "DECODER_UNKNOWN_CONTROL_FAIL_CLOSED_CONFIRMED"} + ] + }, + { + "id": "high_impedance_enable_z", + "evidence": "high_impedance_enable_z", + "role": "unknown_detection", + "kind": "control_unknown", + "monitor_control": "disabled_high_impedance_enable_z", + "injections": [{"control": "i_enable", "values": ["Z"]}], + "phases": [ + {"name": "compile", "command": ["{iverilog}", "-g2012", "-I", "verif/properties", "-DDECODER_INJECT_ENABLE", "-DDECODER_INJECT_Z", "-s", "decoder_four_state_tb", "-o", "{case_work_dir}/simulation.vvp", "rtl/decoder.sv", "verif/assertions/decoder_sva.sv", "verif/tb/decoder_four_state_tb.sv"], "expected": "success"}, + {"name": "run", "command": ["{vvp}", "{case_work_dir}/simulation.vvp"], "expected": "failure", "diagnostic": "decoder control contains an unknown value", "failure_class": "unknown_control"} + ] + } + ] + } + } +} diff --git a/config/static-intent/decoder.json b/config/static-intent/decoder.json new file mode 100644 index 0000000..c8dc5f4 --- /dev/null +++ b/config/static-intent/decoder.json @@ -0,0 +1,28 @@ +{ + "schema": "mosaic-static-intent-v1", + "sdc": { + "profiles": [ + {"name": "synthesis", "path": "flows/synthesis/decoder.timing.sdc", "kind": "combinational"}, + {"name": "physical", "path": "flows/openroad/decoder.timing.sdc", "kind": "combinational"} + ], + "consistency": [ + { + "profiles": ["synthesis", "physical"], + "commands": ["set_input_transition", "set_load", "set_max_delay"] + } + ] + }, + "upf": { + "path": "flows/vc_lp/decoder.power.upf", + "top": "decoder", + "mode": "always_on", + "required": { + "power_domains": ["PD_DECODER"], + "supply_ports": ["VDD", "VSS"], + "supply_nets": ["VDD", "VSS"], + "supply_connections": ["VDD", "VSS"], + "domain_supplies": ["PD_DECODER"] + }, + "forbidden_strategies": ["isolation", "level_shifting", "retention", "power_switch"] + } +} diff --git a/docs/README.md b/docs/README.md index c91abe2..e3fe4fa 100644 --- a/docs/README.md +++ b/docs/README.md @@ -7,6 +7,7 @@ - [Parameterizable D flip-flop](dff/README.md) - [Parameterizable write gate](write_gate/README.md) - [Parameterizable operand isolation](operand_isolation/README.md) +- [Parameterizable decoder](decoder/README.md) ## Template documentation diff --git a/docs/decoder/README.md b/docs/decoder/README.md new file mode 100644 index 0000000..961d6e4 --- /dev/null +++ b/docs/decoder/README.md @@ -0,0 +1,29 @@ +# Parameterizable decoder + +[Return to the repository README](../../README.md). + +`decoder` converts an enabled binary selection into one active-high output. It +supports non-power-of-two output counts, reports whether a selection is legal, +and fails closed for disabled, invalid, or unknown controls. + +## 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) + +## Quick start + +```sh +make MODULE=decoder PROFILE=outputs_3 flow-config-check +make MODULE=decoder PROFILE=outputs_3 clean open-source +``` + +Run all qualified parameter profiles with: + +```sh +make MODULE=decoder clean all-profiles PROFILE_JOBS=4 +``` diff --git a/docs/decoder/interface.md b/docs/decoder/interface.md new file mode 100644 index 0000000..b69b19a --- /dev/null +++ b/docs/decoder/interface.md @@ -0,0 +1,74 @@ +# Interface specification + +[Return to the module documentation index](README.md). + +## Overview + +`decoder` is a zero-latency, combinational binary-to-one-hot decoder. It is +intended for routing controls, write enables, register selection, context +selection, functional-unit activation, and similar control paths. + +The primitive does not define opcodes, instruction formats, datatype legality, +context transitions, or tile-specific behavior. Higher-level logic remains +responsible for those policies. + +## Parameters + +| Parameter | Default | Legal values | Description | +| --- | ---: | --- | --- | +| `NUM_OUTPUTS` | `4` | Integers greater than or equal to `1` | Number of decoded outputs | +| `SELECT_WIDTH` | Derived | `(NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1` | Binary selection width | + +Overriding `SELECT_WIDTH` with a value other than the derived width is illegal. +Non-power-of-two values of `NUM_OUTPUTS` are supported. + +## Ports + +| Port | Direction | Width | Description | +| --- | --- | ---: | --- | +| `i_enable` | Input | `1` | Active-high decode enable | +| `i_select` | Input | `SELECT_WIDTH` | Binary selection | +| `o_decoded` | Output | `NUM_OUTPUTS` | Active-high one-hot result | +| `o_select_valid` | Output | `1` | Legal enabled selection indicator | + +`o_decoded[0]` corresponds to selection zero. In general, +`o_decoded[N]` corresponds to `i_select == N`. + +## Behavior + +| Condition | `o_decoded` | `o_select_valid` | +| --- | --- | ---: | +| Enabled and legal selection | Only `o_decoded[i_select]` is high | `1` | +| Disabled | All zero | `0` | +| Enabled and out-of-range selection | All zero | `0` | +| Unknown or high-impedance enable | All zero | `0` | +| Unknown or high-impedance selection | All zero | `0` | + +The output is always one-hot or zero. Invalid inputs never wrap, retain an old +value, or activate an unintended output. Four-state verification also flags +unknown controls so integration errors remain visible despite fail-closed RTL. + +## Timing contract + +- Architectural latency is zero cycles. +- Initiation interval is one cycle between surrounding registered stages. +- The module has no internal state, clock, reset, or backpressure. +- Timing paths exist from `i_enable` and `i_select` to both outputs. + +A registered or hierarchical decoder changes the latency contract and must use +a separate module. + +## Integration contract + +- `i_enable` and `i_select` must be coherent in the consuming clock domain. +- Asynchronous sources must be synchronized before reaching this leaf. +- Decoded outputs may drive enables but must not directly gate clocks. +- Physical clock control must use an approved integrated clock-gating cell. +- Operation, route, datatype, and destination legality remain external. +- Voltage and power-domain crossings require integration-level protection. + +## Low-power intent + +When disabled, selection changes do not propagate to `o_decoded` or +`o_select_valid`. This suppresses downstream activity. The behavior is logical +activity control and is not UPF isolation, retention, or power gating. diff --git a/docs/decoder/power-characterization.md b/docs/decoder/power-characterization.md new file mode 100644 index 0000000..80b28ee --- /dev/null +++ b/docs/decoder/power-characterization.md @@ -0,0 +1,29 @@ +# Power characterization + +[Return to the module documentation index](README.md). + +## Portable claim + +The decoder suppresses output activity while `i_enable` is low. Functional +verification proves that selection changes cannot activate a decoded output in +that state. + +No standalone energy-saving number is claimed. Dynamic power depends on output +count, selection distribution, fanout, glitches, physical mapping, voltage, +frequency, and downstream capacitance. + +## Integration measurements + +A consuming project that claims power savings must compare enabled and disabled +activity with representative workloads and retain: + +- Mapped technology and operating corner +- Input and output loads +- Selection and enable activity distributions +- SAIF hierarchy and annotation coverage +- Internal, switching, leakage, and total power +- Timing and area effects of the enable path + +PrimePower is an integration-level requirement once these inputs exist. The +portable leaf release must not relabel generic synthesis or toggle coverage as +technology-specific power evidence. diff --git a/docs/decoder/project-configuration.md b/docs/decoder/project-configuration.md new file mode 100644 index 0000000..222acdf --- /dev/null +++ b/docs/decoder/project-configuration.md @@ -0,0 +1,43 @@ +# Project configuration + +[Return to the module documentation index](README.md). + +## Registered tops + +| Purpose | Top | +| --- | --- | +| RTL | `decoder` | +| Simulation | `decoder_tb` | +| Formal | `decoder_formal` | + +The module is registered in `config/modules.json`. Module-owned variables and +flow policy live in `config/modules/decoder.mk` and +`config/modules/decoder-flows.mk`. + +## Source composition + +Properties, assertions, and coverage use separate filelists. The simulation +and formal adapters compose those reusable sources according to their selected +flow without embedding them in the RTL filelist. + +## Flow policy + +Portable lint, formatting, elaboration, Yosys synthesis, SymbiYosys proof, EQY, +Verilator simulation, qualification campaigns, and static-intent validation are +required. + +OpenROAD and commercial adapters are disabled for the standalone leaf. CDC, +DFT, low-power signoff, technology-mapped timing, activity-based power, and +physical implementation are transferred to the first consuming design that +provides real domains, libraries, loads, activity, and placement context. + +## Generated output isolation + +All generated reports and work databases are profile-scoped under: + +```text +reports/decoder// +work/decoder// +``` + +This permits concurrent execution of decoder profiles and other modules. diff --git a/docs/decoder/release-checklist.md b/docs/decoder/release-checklist.md new file mode 100644 index 0000000..7d829b3 --- /dev/null +++ b/docs/decoder/release-checklist.md @@ -0,0 +1,267 @@ +# Decoder Release Checklist + +Use this checklist for every supported decoder 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 `decoder` in `mosaic-common`. The + Docker image is labeled as the common-module CI environment._ +- [x] Supported parameter values and configurations are listed. + _`NUM_OUTPUTS >= 1` is legal and `SELECT_WIDTH` must retain its derived value. + The qualified matrix covers output counts 1, 2, 3, 4, 5, 8, 16, and 32._ +- [x] Unsupported modes and external assumptions are explicit. + _The leaf does not validate opcodes, datatypes, routes, contexts, domains, or + protocols. Integration owns source coherence, architectural legality, and + any synchronization or voltage-domain 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`. + _The portable policy enables lint, formatting, elaboration, generic + synthesis, formal, equivalence, simulation, qualification campaigns, and + static-intent checks._ + +## Interface and architecture + +- [x] [Interface specification](interface.md) matches the RTL. + _The documented parameters, ports, active-high encoding, validity output, + fail-closed behavior, and bit ordering match `rtl/decoder.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. An invalid + enabled selection is reported by deasserting `o_select_valid`._ +- [x] Disabled, reset, test, and low-power behavior are documented. + _Disabled, invalid, and unknown controls produce zero outputs. Reset and test + behavior are not applicable. Output suppression is logical activity control, + not UPF isolation._ +- [x] Integration assumptions and protocol dependencies are reviewed. + _The consumer must provide coherent controls in one domain, validate the + higher-level operation, and never use decoded outputs as physical clocks._ + +## RTL quality + +- [x] Verible style lint records `PASS` or an approved policy `SKIP`. +- [x] Verible formatting records the expected status. + _All decoder-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 decoder warning waiver._ + +## Functional verification + +- [x] The [verification plan](verification-plan.md) maps every requirement to a + test, assertion, formal property, or reviewed combination. +- [x] All supported parameter configurations have evidence. + _Native and CI-equivalent container regressions pass for all eight declared + output counts._ +- [x] Positive, negative, reset, error, and boundary tests pass. + _Exhaustive legal and invalid selections, disabled operation, ordered legal + transitions, random controls, the one-output boundary, invalid parameters, + an inverted-enable mutant, and X/Z controls pass. Reset is not applicable._ +- [x] Assertions run in simulation and reach meaningful antecedents. + _Bound assertions check the exact equations, one-hot-or-zero encoding, + disabled and invalid behavior, and unknown controls. Directed stimulus reaches + each applicable condition._ +- [x] Formal assumptions are reviewed for overconstraint. + _The combinational proof leaves enable and selection unconstrained and uses no + assumptions._ +- [x] Formal proofs pass at justified depth or by complete proof. + _The depth-one combinational proofs complete for every qualified profile._ +- [x] RTL-to-Yosys-netlist equivalence passes. +- [x] Functional and code coverage goals are met or deviations are approved. + _The representative `NUM_OUTPUTS=3` profile reaches 100 percent line, branch, + and user coverage, 97.7273 percent toggle coverage, all ten required sampled + points, and all six formal cover statements. No exclusion is used._ + +## 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 enable and select 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 sources and prove enable and 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 the controllability and observability of the selected destinations._ +- [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 output count. The representative + three-output decoder maps to six 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 + select-to-output, select-to-valid, enable-to-output, and enable-to-valid + budgets._ +- [x] PrimePower uses representative SAIF activity. + _Policy `SKIP` at leaf level. PrimePower remains mandatory before a consuming + design claims technology-specific energy savings._ +- [x] SAIF hierarchy and activity annotation coverage are reviewed. + _The portable regression measures functional and toggle coverage but does not + relabel those results as SAIF or power evidence. Annotation review transfers + to the mapped consuming design._ +- [x] Power, performance, and area results meet the module targets. + _The portable target is correct combinational decoding and zero output + activity while disabled. Numeric PPA targets are deferred to integration._ +- [x] PDK, library, tool, constraint, and corner identities are recorded. + _Validated manifests identify the technology-independent scope, tool versions, + methodology revision, constraints, and hashes. No PDK or signoff corner is + selected for the standalone 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 decoder release. The checked-in configuration is + preliminary integration collateral, not release evidence._ +- [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, bank, route, or control block it drives._ +- [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). + _`DEC-CI-001` records the external hosted-execution and artifact-retention + block for the qualified decoder revision._ +- [x] Each waiver identifies the tool, rule, object, justification, owner, + reviewer, date, and removal condition. + _`DEC-CI-001` records both run and check-run IDs, exact revisions, local + replacement evidence, owner, reviewer, approval date, and removal condition._ +- [x] Generated waiver drafts are not treated as approved policy. +- [x] Expired waivers have been removed or re-reviewed. + _`DEC-CI-001` remains active only while GitHub rejects jobs before execution._ + +## Reproducibility and evidence + +- [x] Native `make clean open-source` passes. + _`make MODULE=decoder clean all-profiles PROFILE_JOBS=4` passes all eight + supported output counts. The exact 38-entry repository module-profile matrix + also passes natively, including three representative coverage gates and the + required clock-gate and write-gate OpenROAD runs._ +- [x] The pinned Docker image builds and its portable gate passes. + _Image `sha256:5d6dfaec931c37c2ea69c1103053e0c3eea34899f0692d09a2302ba5a2b426d9` + was built from the pinned `MF20260910V1` methodology. Its complete 38-entry + matrix, representative coverage gates, and manifest validations pass._ +- [x] The GitHub Actions disposition is reviewed for the recorded revision. + _Push run `35551308160` and pull-request run `35551684468` for revision + `0ace813` were rejected before their first step because of failed account + payments or the configured spending limit. No flow executed or failed. Under + approved exception `DEC-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. + They are mandatory where identified in the consuming integration and are not + reported as `PASS` here._ +- [x] Reports identify module revision, methodology revision, tool versions, + constraints, technology, date, and configuration. + _All 38 native and all 38 container manifests validate for module revision + `0ace813` 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 `DEC-CI-001`, local native and container logs, + reports, coverage evidence, physical evidence, and release manifests are + retained in 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 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 signoff + 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 the domains that generate the controls and receive the + decoded enables._ +- [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 destination 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 actual supplies, power states, crossings, and + isolation or level-shifting requirements._ +- [x] The mapped synthesis and PrimeTime disposition is reviewed. + _Reviewed `SKIP`: generic synthesis proves a combinational implementation. + The consumer must map and close every select and enable path with its selected + libraries, loads, boundaries, and corners._ +- [x] The PrimePower disposition is reviewed for portable leaf release. + _Reviewed `SKIP`: output suppression is functionally proven 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, congestion, fanout, glitches, + extraction, DRC, and LVS belong to the consuming implementation._ + +These reviewed skips close the portable leaf checklist only. The transferred +requirements remain mandatory before a register file, context memory, tile, +NoC router, or other consumer can claim integration or silicon signoff. + +## Known methodology limitation + +The pinned `mosaic-flow` profile schema does not yet accept +`coverage_qualification` in a parameter-profile flow list. CI therefore forces +three-output coverage before manifest generation, stores `forced-status.txt`, +restores the profile-owned status to `SKIP`, and indexes the passing evidence. +This enforced handoff is validated and is not a decoder release deviation. + +## Final commands + +```sh +git submodule status +make MODULE=decoder PROFILE=outputs_3 flow-config-check +make MODULE=decoder clean all-profiles PROFILE_JOBS=4 +make MODULE=decoder PROFILE=outputs_3 FORCE_FLOW=1 open-coverage +make MODULE=decoder PROFILE=outputs_3 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/decoder/verification-plan.md b/docs/decoder/verification-plan.md new file mode 100644 index 0000000..a23d9a3 --- /dev/null +++ b/docs/decoder/verification-plan.md @@ -0,0 +1,95 @@ +# Verification plan + +[Return to the module documentation index](README.md). + +## Objectives + +Verification establishes exact binary-to-one-hot mapping, validity reporting, +disabled activity suppression, invalid-code rejection, deterministic X/Z +behavior, non-power-of-two support, derived parameter enforcement, and absence +of retained state. + +## Requirements traceability + +| ID | Requirement | Evidence | +| --- | --- | --- | +| `REQ-DEC-001` | Every enabled legal selection activates exactly its corresponding bit | Exhaustive simulation, bound assertions, formal proof | +| `REQ-DEC-002` | Disabled operation produces zero and is invalid | Exhaustive simulation, assertions, formal proof | +| `REQ-DEC-003` | Out-of-range encodings produce zero and are invalid | Exhaustive non-power-of-two profiles, assertions, formal proof | +| `REQ-DEC-004` | Output is always one-hot or zero | Assertion and exhaustive formal proof | +| `REQ-DEC-005` | Unknown enable or selection fails closed and is detected | Icarus X/Z qualification campaign | +| `REQ-DEC-006` | `NUM_OUTPUTS=1` and non-power-of-two counts work | Profiles 1, 3, and 5 plus formal proof | +| `REQ-DEC-007` | Invalid parameter values fail elaboration | Negative qualification campaign | +| `REQ-DEC-008` | Synthesized logic preserves RTL behavior | Yosys synthesis and EQY | +| `REQ-DEC-009` | The leaf has no state, clock, reset, or broad timing exception | Static intent validation | + +## Parameter matrix + +| Profile | `NUM_OUTPUTS` | Purpose | +| --- | ---: | --- | +| `outputs_1` | 1 | Minimum configuration and one-bit derived select width | +| `outputs_2` | 2 | Small power-of-two decode | +| `outputs_3` | 3 | Small non-power-of-two decode with one invalid encoding | +| `outputs_4` | 4 | Directional-port use case | +| `outputs_5` | 5 | Extended non-power-of-two decode | +| `outputs_8` | 8 | Register or bank selection | +| `outputs_16` | 16 | Context selection | +| `outputs_32` | 32 | Large flat decode | + +Each profile runs lint, formatting, elaboration, generic synthesis, formal +proof, equivalence, simulation, and static-intent checks. The minimum profile +also owns parameter-negative and four-state campaigns because those campaigns +compile dedicated fixtures independently from the selected profile. + +## Simulation plan + +For each profile, the self-checking test exhausts every binary selection with +enable low and high. It then exercises every ordered pair of legal selections +and a deterministic randomized sequence with simultaneous control changes. + +The checks cover every legal selection and every invalid encoding. Power-of-two +profiles have no invalid binary encoding, so that requirement is vacuous there. + +## Assertion and coverage plan + +Assertions are bound to every `decoder` instance and check: + +- Exact output and validity equations +- One-hot-or-zero output encoding +- Zero output for disabled or invalid operation +- Fail-closed behavior for unknown controls +- Detection of unknown controls in four-state simulation + +Functional cover statements observe disabled operation, legal operation, first +and last selections, invalid selections where representable, and activation of +each generated output. Code and user coverage use the module-owned policy. + +## Formal plan + +The harness leaves enable and selection unconstrained. A depth-one complete +combinational proof establishes output encoding, legal selection behavior, +invalid selection handling, and absence of state without assumptions. + +Formal cover mode checks reachability of the reusable coverage model. An +invalid-selection cover is unreachable by construction for power-of-two output +counts and is reviewed as a vacuous configuration-specific goal. + +## Negative and four-state qualification + +The negative campaign proves that the self-checking test rejects an +enable-inverted mutant. It also confirms that zero outputs and an inconsistent +`SELECT_WIDTH` fail elaboration with module-specific diagnostics. + +Pinned Icarus campaigns inject X and Z independently into `i_enable` and +`i_select`. Each disabled-monitor control proves that the RTL produces zero. +The paired monitor case proves that verification detects the unknown control. + +## Exit criteria + +- [x] All eight 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. +- [x] The release checklist is complete under reviewed exception `DEC-CI-001`. diff --git a/docs/decoder/waivers.md b/docs/decoder/waivers.md new file mode 100644 index 0000000..841e67a --- /dev/null +++ b/docs/decoder/waivers.md @@ -0,0 +1,23 @@ +# 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 + +```text +ID: DEC-CI-001 +Tool and rule: GitHub Actions hosted execution and release-artifact retention +Affected file and object: Open-source RTL quality gate runs 35551308160 and 35551684468 for module revision 0ace8134770d8d22d824a0f4bd46b14500e9f6d7 +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 38-entry native and container module-profile matrix, representative coverage steps, required OpenROAD steps, and all native and container release-manifest validations pass locally with the pinned methodology and Docker image. +Evidence: GitHub check-run annotations 106186451597 and 106187468422, 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. +``` + +Generated waiver drafts are diagnostic suggestions and are not approved policy. diff --git a/filelists/decoder.assertions.f b/filelists/decoder.assertions.f new file mode 100644 index 0000000..29a28f4 --- /dev/null +++ b/filelists/decoder.assertions.f @@ -0,0 +1,2 @@ +verif/assertions/decoder_sva.sv +verif/assertions/decoder_bind.sv diff --git a/filelists/decoder.coverage.f b/filelists/decoder.coverage.f new file mode 100644 index 0000000..852ee08 --- /dev/null +++ b/filelists/decoder.coverage.f @@ -0,0 +1,3 @@ +verif/coverage/decoder_coverage.sv +verif/coverage/decoder_transition_coverage.sv +verif/coverage/decoder_coverage_bind.sv diff --git a/filelists/decoder.formal.f b/filelists/decoder.formal.f new file mode 100644 index 0000000..1f72c8b --- /dev/null +++ b/filelists/decoder.formal.f @@ -0,0 +1,3 @@ +-f filelists/decoder.rtl.f ++incdir+verif/properties +verif/formal/decoder_formal.sv diff --git a/filelists/decoder.properties.f b/filelists/decoder.properties.f new file mode 100644 index 0000000..2dfc6d9 --- /dev/null +++ b/filelists/decoder.properties.f @@ -0,0 +1 @@ ++incdir+verif/properties diff --git a/filelists/decoder.rtl.f b/filelists/decoder.rtl.f new file mode 100644 index 0000000..6c2d1e9 --- /dev/null +++ b/filelists/decoder.rtl.f @@ -0,0 +1,2 @@ ++incdir+rtl +rtl/decoder.sv diff --git a/filelists/decoder.tb.f b/filelists/decoder.tb.f new file mode 100644 index 0000000..9937f9e --- /dev/null +++ b/filelists/decoder.tb.f @@ -0,0 +1,4 @@ +-f filelists/decoder.rtl.f ++incdir+verif +verif/tb/decoder_test_case.sv +verif/tb/decoder_tb.sv diff --git a/flows/cdc/decoder.constraints.tcl b/flows/cdc/decoder.constraints.tcl new file mode 100644 index 0000000..57a323b --- /dev/null +++ b/flows/cdc/decoder.constraints.tcl @@ -0,0 +1 @@ +# Stateless combinational leaf with no internal clock, reset, or crossing. diff --git a/flows/eqy/decoder.equivalence.eqy b/flows/eqy/decoder.equivalence.eqy new file mode 100644 index 0000000..3257614 --- /dev/null +++ b/flows/eqy/decoder.equivalence.eqy @@ -0,0 +1,14 @@ +[gold] +read_verilog -sv rtl/decoder.sv +prep -top decoder + +[gate] +read_verilog work/decoder/yosys_synthesis/decoder_netlist.v +prep -top decoder + +[collect decoder] +group o_* + +[strategy sat] +use sat +depth 1 diff --git a/flows/openroad/decoder.config.mk b/flows/openroad/decoder.config.mk new file mode 100644 index 0000000..9ae3f15 --- /dev/null +++ b/flows/openroad/decoder.config.mk @@ -0,0 +1,8 @@ +export DESIGN_NAME := decoder +export PLATFORM := nangate45 +export SDC_FILE := $(MODULE_ROOT)/flows/openroad/decoder.timing.sdc +export CORE_UTILIZATION := 20 +export CORE_ASPECT_RATIO := 1 +export CORE_MARGIN := 5 +export DIE_AREA := 0 0 60 60 +export CORE_AREA := 5 5 55 55 diff --git a/flows/openroad/decoder.timing.sdc b/flows/openroad/decoder.timing.sdc new file mode 100644 index 0000000..76957ef --- /dev/null +++ b/flows/openroad/decoder.timing.sdc @@ -0,0 +1,6 @@ +# Preliminary combinational decoder 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 3.0 -from [get_ports i_enable] -to [all_outputs] +set_max_delay 4.0 -from [get_ports i_select*] -to [all_outputs] diff --git a/flows/sg_dft/decoder.constraints.tcl b/flows/sg_dft/decoder.constraints.tcl new file mode 100644 index 0000000..fe35326 --- /dev/null +++ b/flows/sg_dft/decoder.constraints.tcl @@ -0,0 +1 @@ +# Stateless combinational leaf with no scan element or internal test mode. diff --git a/flows/symbiyosys/decoder.cover.sby b/flows/symbiyosys/decoder.cover.sby new file mode 100644 index 0000000..e72e03f --- /dev/null +++ b/flows/symbiyosys/decoder.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 decoder.sv decoder_coverage.sv decoder_coverage_bind.sv decoder_formal.sv +prep -top decoder_formal + +[files] +rtl/decoder.sv +verif/coverage/decoder_coverage.sv +verif/coverage/decoder_coverage_bind.sv +verif/formal/decoder_formal.sv diff --git a/flows/symbiyosys/decoder.formal.sby b/flows/symbiyosys/decoder.formal.sby new file mode 100644 index 0000000..a53d057 --- /dev/null +++ b/flows/symbiyosys/decoder.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 decoder.sv decoder_sva.sv decoder_bind.sv decoder_formal.sv +prep -top decoder_formal + +[files] +rtl/decoder.sv +verif/properties/decoder_predicates.svh +verif/assertions/decoder_sva.sv +verif/assertions/decoder_bind.sv +verif/formal/decoder_formal.sv diff --git a/flows/synthesis/decoder.timing.sdc b/flows/synthesis/decoder.timing.sdc new file mode 100644 index 0000000..62086d9 --- /dev/null +++ b/flows/synthesis/decoder.timing.sdc @@ -0,0 +1,6 @@ +# Combinational decoder 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 3.0 -from [get_ports i_enable] -to [all_outputs] +set_max_delay 4.0 -from [get_ports i_select*] -to [all_outputs] diff --git a/flows/vc_lp/decoder.power.upf b/flows/vc_lp/decoder.power.upf new file mode 100644 index 0000000..988ec84 --- /dev/null +++ b/flows/vc_lp/decoder.power.upf @@ -0,0 +1,9 @@ +set_design_top decoder +create_power_domain PD_DECODER -include_scope +create_supply_port VDD -domain PD_DECODER +create_supply_port VSS -domain PD_DECODER +create_supply_net VDD -domain PD_DECODER +create_supply_net VSS -domain PD_DECODER +connect_supply_net VDD -ports VDD +connect_supply_net VSS -ports VSS +set_domain_supply_net PD_DECODER -primary_power_net VDD -primary_ground_net VSS diff --git a/rtl/decoder.sv b/rtl/decoder.sv new file mode 100644 index 0000000..ad1d6bd --- /dev/null +++ b/rtl/decoder.sv @@ -0,0 +1,37 @@ +`timescale 1ns / 1ps + +/// Parameterizable binary-to-one-hot decoder with fail-closed invalid handling. +module decoder #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select, + output logic [ NUM_OUTPUTS-1:0] o_decoded, + output logic o_select_valid +); + + localparam int unsigned ExpectedSelectWidth = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1; + + generate + if (NUM_OUTPUTS < 1) begin : g_invalid_num_outputs + decoder_num_outputs_must_be_greater_than_zero invalid_num_outputs (); + end + if (SELECT_WIDTH != ExpectedSelectWidth) begin : g_invalid_select_width + decoder_select_width_must_match_num_outputs invalid_select_width (); + end + endgenerate + + always_comb begin + o_decoded = '0; + o_select_valid = 1'b0; + + // A four-state condition executes only when enable and selection are + // both known and legal. Unknown controls therefore fail closed. + if (i_enable && ({1'b0, i_select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS))) begin + o_decoded[i_select] = 1'b1; + o_select_valid = 1'b1; + end + end + +endmodule diff --git a/scripts/verible-format b/scripts/verible-format index ffb76cd..7bc81b6 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, and operand isolation sources -# use four-space indentation. +# isolation cell, retention register, write gate, operand isolation, and decoder +# 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 ]]; 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 ]]; then args=(--indentation_spaces=4 "${args[@]}") fi diff --git a/verif/assertions/decoder_bind.sv b/verif/assertions/decoder_bind.sv new file mode 100644 index 0000000..22ce5b1 --- /dev/null +++ b/verif/assertions/decoder_bind.sv @@ -0,0 +1,28 @@ +`timescale 1ns / 1ps + +/// Stable boundary used to bind checks to every decoder instance. +module decoder_bind #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select, + input logic [ NUM_OUTPUTS-1:0] o_decoded, + input logic o_select_valid +); + + decoder_sva #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) i_decoder_sva ( + .* + ); + +endmodule + +`ifndef MOSAIC_FORMAL +bind decoder decoder_bind #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) +) i_decoder_bind (.*); +`endif diff --git a/verif/assertions/decoder_sva.sv b/verif/assertions/decoder_sva.sv new file mode 100644 index 0000000..ede3b24 --- /dev/null +++ b/verif/assertions/decoder_sva.sv @@ -0,0 +1,48 @@ +`timescale 1ns / 1ps + +/// Combinational decoder checks shared by simulation and formal proof. +module decoder_sva #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select, + input logic [ NUM_OUTPUTS-1:0] o_decoded, + input logic o_select_valid +); + +`ifdef MOSAIC_YOSYS_FORMAL + always_comb begin + assert ($onehot0(o_decoded)); + if (i_enable && ({1'b0, i_select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS))) begin + assert (o_decoded == (NUM_OUTPUTS'(1'b1) << i_select)); + assert (o_select_valid); + end else begin + assert (o_decoded == '0); + assert (!o_select_valid); + end + end +`else + `include "decoder_predicates.svh" + + always @(i_enable, i_select, o_decoded, o_select_valid) begin + #1ps; + assert ($onehot0(o_decoded)) + else $fatal(1, "decoder produced a multi-hot output"); + assert (o_decoded === decoder_expected_f(i_enable, i_select)) + else $fatal(1, "decoder output equation failed"); + assert (o_select_valid === ((i_enable === 1'b1) && decoder_selection_legal_f(i_select))) + else $fatal(1, "decoder validity equation failed"); + + if (!decoder_controls_known_f(i_enable, i_select)) begin + assert ((o_decoded === '0) && (o_select_valid === 1'b0)) + else $fatal(1, "decoder did not fail closed for an unknown control"); + end +`ifndef DECODER_DISABLE_UNKNOWN_MONITOR + assert (decoder_controls_known_f(i_enable, i_select)) + else $fatal(1, "decoder control contains an unknown value"); +`endif + end +`endif + +endmodule diff --git a/verif/coverage/decoder_coverage.sv b/verif/coverage/decoder_coverage.sv new file mode 100644 index 0000000..7b70ae4 --- /dev/null +++ b/verif/coverage/decoder_coverage.sv @@ -0,0 +1,33 @@ +`timescale 1ns / 1ps + +/// Functional coverage for the decoder's combinational contract. +module decoder_coverage #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select, + input logic [ NUM_OUTPUTS-1:0] o_decoded, + input logic o_select_valid +); + + always_comb begin + disabled_operation : cover (!i_enable && (o_decoded == '0) && !o_select_valid); + enabled_legal : + cover (i_enable && ({1'b0, i_select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS)) && o_select_valid); + first_selection : cover (i_enable && (i_select == '0) && o_decoded[0]); + last_selection : + cover (i_enable && (i_select == SELECT_WIDTH'(NUM_OUTPUTS - 1)) && + o_decoded[NUM_OUTPUTS-1]); + any_output_selected : cover (o_select_valid && (|o_decoded)); + end + + if ((64'(1) << SELECT_WIDTH) > longint'(NUM_OUTPUTS)) begin : g_invalid_encoding + always_comb begin + invalid_selection : + cover (i_enable && ({1'b0, i_select} >= (SELECT_WIDTH + 1)'(NUM_OUTPUTS)) && + (o_decoded == '0) && !o_select_valid); + end + end + +endmodule diff --git a/verif/coverage/decoder_coverage_bind.sv b/verif/coverage/decoder_coverage_bind.sv new file mode 100644 index 0000000..00dd01f --- /dev/null +++ b/verif/coverage/decoder_coverage_bind.sv @@ -0,0 +1,28 @@ +`timescale 1ns / 1ps + +/// Stable boundary used to bind functional coverage to every decoder instance. +module decoder_coverage_bind #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select, + input logic [ NUM_OUTPUTS-1:0] o_decoded, + input logic o_select_valid +); + + decoder_coverage #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) i_decoder_coverage ( + .* + ); + +endmodule + +`ifndef MOSAIC_FORMAL +bind decoder decoder_coverage_bind #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) +) i_decoder_coverage_bind (.*); +`endif diff --git a/verif/coverage/decoder_transition_coverage.sv b/verif/coverage/decoder_transition_coverage.sv new file mode 100644 index 0000000..ee68988 --- /dev/null +++ b/verif/coverage/decoder_transition_coverage.sv @@ -0,0 +1,63 @@ +`timescale 1ns / 1ps + +/// Sampled transition coverage driven by the self-checking decoder test. +module decoder_transition_coverage #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_sample, + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select +); + + logic previous_sample_valid; + logic previous_enable; + logic [SELECT_WIDTH-1:0] previous_select; + + function automatic logic selection_legal(input logic [SELECT_WIDTH-1:0] select); + selection_legal = {1'b0, select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS); + endfunction + + initial begin + previous_sample_valid = 1'b0; + previous_enable = 1'b0; + previous_select = '0; + end + + always @(posedge i_sample) begin + if (previous_sample_valid) begin + enable_asserted : cover (!previous_enable && i_enable); + enable_deasserted : cover (previous_enable && !i_enable); + legal_selection_changed : + cover (previous_enable && selection_legal( + previous_select + ) && i_enable && selection_legal( + i_select + ) && (previous_select != i_select)); + end + + previous_sample_valid <= 1'b1; + previous_enable <= i_enable; + previous_select <= i_select; + end + + if ((64'(1) << SELECT_WIDTH) > longint'(NUM_OUTPUTS)) begin : g_invalid_transitions + always @(posedge i_sample) begin + if (previous_sample_valid) begin + legal_to_invalid : + cover (previous_enable && selection_legal( + previous_select + ) && i_enable && !selection_legal( + i_select + )); + invalid_to_legal : + cover (previous_enable && !selection_legal( + previous_select + ) && i_enable && selection_legal( + i_select + )); + end + end + end + +endmodule diff --git a/verif/formal/decoder_formal.sv b/verif/formal/decoder_formal.sv new file mode 100644 index 0000000..5797d37 --- /dev/null +++ b/verif/formal/decoder_formal.sv @@ -0,0 +1,51 @@ +`timescale 1ns / 1ps + +/// Unconstrained harness proving the binary-to-one-hot decoder contract. +module decoder_formal #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +); + + (* anyseq *)logic i_enable; + (* anyseq *)logic [SELECT_WIDTH-1:0] i_select; + logic [ NUM_OUTPUTS-1:0] o_decoded; + logic o_select_valid; + + decoder #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) dut ( + .* + ); + +`ifdef FORMAL_ASSERTIONS + decoder_bind #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) i_decoder_bind ( + .* + ); +`endif + +`ifdef FORMAL_COVERAGE + decoder_coverage_bind #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) i_decoder_coverage_bind ( + .* + ); +`endif + + always_comb begin + assert ($onehot0(o_decoded)); + if (i_enable && ({1'b0, i_select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS))) begin + assert (o_select_valid); + assert (o_decoded == (NUM_OUTPUTS'(1'b1) << i_select)); + assert (o_decoded[i_select]); + end else begin + assert (!o_select_valid); + assert (o_decoded == '0); + end + end + +endmodule diff --git a/verif/mutations/decoder_inverted_enable_mutant.sv b/verif/mutations/decoder_inverted_enable_mutant.sv new file mode 100644 index 0000000..648761f --- /dev/null +++ b/verif/mutations/decoder_inverted_enable_mutant.sv @@ -0,0 +1,23 @@ +`timescale 1ns / 1ps + +/// Deliberately faulty decoder used only to qualify the regression. +module decoder #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + input logic i_enable, + input logic [SELECT_WIDTH-1:0] i_select, + output logic [ NUM_OUTPUTS-1:0] o_decoded, + output logic o_select_valid +); + + always_comb begin + o_decoded = '0; + o_select_valid = 1'b0; + if (!i_enable && ({1'b0, i_select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS))) begin + o_decoded[i_select] = 1'b1; + o_select_valid = 1'b1; + end + end + +endmodule diff --git a/verif/properties/decoder_predicates.svh b/verif/properties/decoder_predicates.svh new file mode 100644 index 0000000..04cc670 --- /dev/null +++ b/verif/properties/decoder_predicates.svh @@ -0,0 +1,20 @@ +// Module-scoped predicates shared by decoder checkers. +// This file has no include guard because each wrapper owns its declarations. + +function automatic logic decoder_controls_known_f(input logic enable, + input logic [SELECT_WIDTH-1:0] select); + decoder_controls_known_f = !$isunknown(enable) && !$isunknown(select); +endfunction + +function automatic logic decoder_selection_legal_f(input logic [SELECT_WIDTH-1:0] select); + decoder_selection_legal_f = !$isunknown(select) && + ({1'b0, select} < (SELECT_WIDTH + 1)'(NUM_OUTPUTS)); +endfunction + +function automatic logic [NUM_OUTPUTS-1:0] decoder_expected_f( + input logic enable, input logic [SELECT_WIDTH-1:0] select); + decoder_expected_f = '0; + if ((enable === 1'b1) && decoder_selection_legal_f(select)) begin + decoder_expected_f[select] = 1'b1; + end +endfunction diff --git a/verif/tb/decoder_four_state_tb.sv b/verif/tb/decoder_four_state_tb.sv new file mode 100644 index 0000000..241a770 --- /dev/null +++ b/verif/tb/decoder_four_state_tb.sv @@ -0,0 +1,42 @@ +`timescale 1ns / 1ps + +/// Four-state qualification for deterministic unknown-control behavior. +module decoder_four_state_tb; + + logic i_enable = 1'b1; + logic [1:0] i_select = 2'b01; + logic [2:0] o_decoded; + logic o_select_valid; + + decoder #(.NUM_OUTPUTS(3)) dut (.*); + + decoder_sva #(.NUM_OUTPUTS(3)) i_decoder_sva (.*); + + initial begin + #1ns; +`ifdef DECODER_INJECT_ENABLE +`ifdef DECODER_INJECT_Z + i_enable = 1'bz; +`else + i_enable = 1'bx; +`endif +`else +`ifdef DECODER_INJECT_Z + i_select = 'z; +`else + i_select = 'x; +`endif +`endif + #1ns; + + assert ((o_decoded === '0) && (o_select_valid === 1'b0)) + else $fatal(1, "DECODER_UNKNOWN_CONTROL_DID_NOT_FAIL_CLOSED"); +`ifdef DECODER_DISABLE_UNKNOWN_MONITOR + $display("DECODER_UNKNOWN_CONTROL_FAIL_CLOSED_CONFIRMED"); + $finish; +`else + $fatal(1, "DECODER_UNKNOWN_CONTROL_MONITOR_DID_NOT_FIRE"); +`endif + end + +endmodule diff --git a/verif/tb/decoder_invalid_num_outputs_tb.sv b/verif/tb/decoder_invalid_num_outputs_tb.sv new file mode 100644 index 0000000..9edfa77 --- /dev/null +++ b/verif/tb/decoder_invalid_num_outputs_tb.sv @@ -0,0 +1,11 @@ +`timescale 1ns / 1ps + +/// Negative elaboration fixture for NUM_OUTPUTS=0. +module decoder_invalid_num_outputs_tb; + logic i_enable; + logic i_select; + logic [1:0] o_decoded; + logic o_select_valid; + + decoder #(.NUM_OUTPUTS(0)) dut (.*); +endmodule diff --git a/verif/tb/decoder_invalid_select_width_tb.sv b/verif/tb/decoder_invalid_select_width_tb.sv new file mode 100644 index 0000000..ff4ef09 --- /dev/null +++ b/verif/tb/decoder_invalid_select_width_tb.sv @@ -0,0 +1,16 @@ +`timescale 1ns / 1ps + +/// Negative elaboration fixture for an overridden, inconsistent select width. +module decoder_invalid_select_width_tb; + logic i_enable; + logic [2:0] i_select; + logic [3:0] o_decoded; + logic o_select_valid; + + decoder #( + .NUM_OUTPUTS (4), + .SELECT_WIDTH(3) + ) dut ( + .* + ); +endmodule diff --git a/verif/tb/decoder_tb.sv b/verif/tb/decoder_tb.sv new file mode 100644 index 0000000..1275b66 --- /dev/null +++ b/verif/tb/decoder_tb.sv @@ -0,0 +1,29 @@ +`timescale 1ns / 1ps + +/// Top-level regression for one profile-selected decoder configuration. +module decoder_tb #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +); + + logic done; + + decoder_test_case #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) u_unit ( + .o_done(done) + ); + + initial begin + wait (done); + $display("PASS: decoder NUM_OUTPUTS=%0d regression completed", NUM_OUTPUTS); + $finish; + end + + initial begin + #20us; + $fatal(1, "decoder NUM_OUTPUTS=%0d regression timed out", NUM_OUTPUTS); + end + +endmodule diff --git a/verif/tb/decoder_test_case.sv b/verif/tb/decoder_test_case.sv new file mode 100644 index 0000000..3514578 --- /dev/null +++ b/verif/tb/decoder_test_case.sv @@ -0,0 +1,107 @@ +`timescale 1ns / 1ps + +/// Reusable self-checking test for one decoder parameter configuration. +module decoder_test_case #( + parameter int unsigned NUM_OUTPUTS = 4, + parameter int unsigned SELECT_WIDTH = (NUM_OUTPUTS > 1) ? $clog2(NUM_OUTPUTS) : 1 +) ( + output logic o_done +); + + localparam longint unsigned NumEncodings = 64'(1) << SELECT_WIDTH; + + logic i_enable; + logic [SELECT_WIDTH-1:0] i_select; + logic [ NUM_OUTPUTS-1:0] o_decoded; + logic o_select_valid; + logic coverage_sample; + integer random_seed; + + decoder #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) dut ( + .* + ); + +`ifndef DECODER_DISABLE_COVERAGE + decoder_transition_coverage #( + .NUM_OUTPUTS (NUM_OUTPUTS), + .SELECT_WIDTH(SELECT_WIDTH) + ) i_transition_coverage ( + .i_sample(coverage_sample), + .i_enable(i_enable), + .i_select(i_select) + ); +`endif + + task automatic check_case(input logic enable, input longint unsigned selection); + logic [NUM_OUTPUTS-1:0] expected_decoded; + logic expected_valid; + + i_enable = enable; + i_select = SELECT_WIDTH'(selection); + #1ns; + + expected_decoded = '0; + expected_valid = enable && (selection < longint'(NUM_OUTPUTS)); + if (expected_valid) begin + expected_decoded[SELECT_WIDTH'(selection)] = 1'b1; + end + + assert ({o_select_valid, o_decoded} === {expected_valid, expected_decoded}) + else + $fatal( + 1, + "NUM_OUTPUTS=%0d enable=%b select=%0d expected=%b_%b actual=%b_%b", + NUM_OUTPUTS, + enable, + selection, + expected_valid, + expected_decoded, + o_select_valid, + o_decoded + ); + coverage_sample = 1'b1; + #1ps; + coverage_sample = 1'b0; + endtask + + initial begin + o_done = 1'b0; + i_enable = 1'b0; + i_select = '0; + coverage_sample = 1'b0; + + // Exhaust every binary encoding in both enabled and disabled modes. + for (longint unsigned selection = 0; selection < NumEncodings; selection++) begin + check_case(1'b0, selection); + check_case(1'b1, selection); + end + + // Exercise every ordered transition between legal selections. + for (longint unsigned previous = 0; previous < longint'(NUM_OUTPUTS); previous++) begin + for (longint unsigned current = 0; current < longint'(NUM_OUTPUTS); current++) begin + check_case(1'b1, previous); + check_case(1'b1, current); + end + end + + // Directly exercise both boundaries of the invalid-encoding region. + if (NumEncodings > longint'(NUM_OUTPUTS)) begin + check_case(1'b1, longint'(NUM_OUTPUTS) - 1); + check_case(1'b1, longint'(NUM_OUTPUTS)); + check_case(1'b1, 0); + end + + // Exercise simultaneous enable and selection changes with a fixed seed. + random_seed = 32'hdec0_de01 ^ NUM_OUTPUTS; + void'($urandom(random_seed)); + for (int unsigned iteration = 0; iteration < 128; iteration++) begin + check_case(iteration[0], 64'($urandom()) % NumEncodings); + end + + o_done = 1'b1; + end + +endmodule