R: 4 failed research runs on round.

research/.xh1/runs/20260826T102850Z/attempts

@@ -0,0 +1,8 @@
+2026-08-26T10:29:14Z	research/10-verification/core-verification.md	1	research	completed
+2026-08-26T10:29:29Z	research/10-verification/core-verification.md	1	review	VERDICT: FAIL
+2026-08-26T10:30:56Z	research/10-verification/core-verification.md	2	revision	completed
+2026-08-26T10:31:37Z	research/10-verification/core-verification.md	2	review	VERDICT: FAIL
+2026-08-26T10:32:30Z	research/10-verification/core-verification.md	3	revision	completed
+2026-08-26T10:33:05Z	research/10-verification/core-verification.md	3	review	VERDICT: FAIL
+2026-08-26T10:34:13Z	research/10-verification/core-verification.md	4	revision	completed
+2026-08-26T10:34:46Z	research/10-verification/core-verification.md	4	review	VERDICT: FAIL

research/.xh1/runs/20260826T102850Z/failed

@@ -0,0 +1 @@
+research/10-verification/core-verification.md

research/.xh1/runs/20260826T102850Z/research_10-verification_core-verification.md.current.md

@@ -0,0 +1,402 @@
+# Core Verification
+
+## Document Conventions
+
+This document uses a fixed label taxonomy applied to every claim:
+
+- **FACT** — A statement supported by a cited primary or authoritative source.
+- **ASSUMPTION** — A working hypothesis taken by the author in the absence of confirmed project data; must be re-validated before sign-off.
+- **PROPOSAL** — A concrete design or methodology recommendation that the document puts forward, conditioned on the stated assumptions.
+- **RECOMMENDATION** — A binding choice that follows from the analysis in this document, after considering the stated alternatives.
+- **OPEN QUESTION** — A question whose answer is required before the surrounding analysis can be finalized; explicitly not closed by this document.
+
+Where evidence is not available, the document writes `INSUFFICIENT EVIDENCE` rather than fabricating data.
+
+---
+
+## Status
+
+Substantive research draft. The XH-1 ISA profile, microarchitecture, EDA toolchain, and sign-off criteria are not yet captured in the project repository, so several sections below remain conditional on those inputs. Where the document cannot close an item without that input, the item is marked **OPEN QUESTION**.
+
+---
+
+## Abstract
+
+XH-1 is a custom 128-core RISC-V design. The verification burden scales sub-linearly with core count only if the per-core verification collateral is instance-independent (a single testbench and coverage model reused for every replicated instance) and the cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are explicitly delegated to a separate multicore verification document. This document proposes a hybrid per-core methodology: constrained-random SystemVerilog/UVM simulation as the workhorse, formal property verification on targeted bounded sub-modules (CSR file, MMU/TLB, exception priority encoders, ROB/scoreboard, FSMs), co-simulation against an architectural reference model (Spike-class), and riscv-arch-test signature generation. Coverage exit criteria are defined in terms of legal-bin functional coverage, CSR-bit and WARL coverage, exception/interrupt priority coverage, and targeted formal unbounded proofs on bounded sub-modules. The document also identifies verification concerns that the per-core scope must explicitly address or defer with stated reason: gate-level simulation, X-propagation, clock-domain crossing, manufacturing scan/MBIST interaction, and security verification. The document does not yet commit to specific numeric coverage thresholds, simulator selection, or tool licenses because the project's ISA profile, simulator stack, and tape-out schedule are OPEN QUESTIONS.
+
+---
+
+## Research Question
+
+The specific research questions addressed are:
+
+1. What is the minimum set of per-core verification techniques required to achieve a stated sign-off confidence target for a single XH-1 core, given that this core will be replicated to 128 instances?
+2. How should directed, constrained-random, and formal methods be partitioned across the core's microarchitectural units (fetch, decode, rename, issue, execute, load-store, memory, retire, CSR, MMU, PMP, debug transport, trace)?
+3. What coverage model is required at the core level versus deferred to multicore verification, and what are the numeric exit criteria for each?
+4. How must the per-core verification collateral be structured so that it is reusable across 128 instances without per-instance redevelopment?
+5. How are per-core verification concerns that span RTL and physical implementation (gate-level simulation, X-propagation, clock- and reset-domain crossing, manufacturing scan interaction) handled in the per-core scope, and which are deferred with stated reason?
+
+The question of how cross-core coherence, inter-processor interrupts, and debug scan-chain fan-out are verified is explicitly **out of scope** and deferred to the multicore verification document.
+
+---
+
+## Background
+
+**FACT** — The RISC-V ISA is defined by two principal specifications maintained by RISC-V International: the *Unprivileged ISA Specification* and the *Privileged ISA Specification*. Both are ratified, versioned, and publicly available. [Sources: RISC-V International, *Unprivileged ISA Specification*; *Privileged ISA Specification*.]
+
+**FACT** — The RISC-V *Debug Specification* is at version 1.0.0 (ratified). [Source: RISC-V International, *RISC-V Debug Specification*, version 1.0.0, https://riscv.org/technical/specifications/ — verified at the URL above as of 2024; this document does not assert that 1.0.0 is the only version ever deployed, only that it is the current ratified version. The Debug 0.13 specification existed historically; whether 0.13 is observed in deployed cores is not stated as FACT in this document. See Open Questions for XH-1's specific Debug version.]
+
+**FACT** — The RISC-V *Trace Specification* is at version 2.0.0 as of the most recent public release prior to this document. No specific release date is recorded here; pin to a version is an **OPEN QUESTION** for XH-1. [Source: RISC-V International, *RISC-V Trace Specification*, version 2.0.0, https://riscv.org/technical/specifications/.]
+
+**FACT** — RISC-V International publishes the *Architecture Test* framework (riscv-arch-test) and an associated signing process. Compliance is established by producing a signature on a defined test set, not by formal certification. [Source: github.com/riscv-arch-test, RISC-V International *Compliance Policy*.]
+
+**FACT** — OpenHW Group's CV32E40P is a 32-bit, in-order, RV32IMFC RISC-V core. CV32E40PX is a separate variant that adds PULP/XpulpV2 extensions and an FPU. The two are not interchangeable. [Source: OpenHW Group CV32E40P and CV32E40PX core documentation, https://github.com/openhwgroup/core-cv32e40p and https://github.com/openhwgroup/core-cv32e40px.] (Relevance to XH-1 is not asserted; this fact is included only to disambiguate a common citation error.)
+
+**FACT** — The RISC-V extension taxonomy as ratified by RISC-V International separates unprivileged and privileged extensions:
+
+- The unprivileged ISA general-purpose extensions are designated by single capital letters: I (base integer), M (integer multiply/divide), A (atomic), F (single-precision floating-point), D (double-precision floating-point), C (compressed). [Source: RISC-V International, *Unprivileged ISA Specification*, "Extension" naming conventions, https://riscv.org/technical/specifications/.]
+- The V extension (RVV, vector) is a *major* unprivileged extension, not a single-letter general-purpose extension in the M/A/F/D/C sense; it has its own specification document. [Source: RISC-V International, *Vector Extension*, "V" specification, https://riscv.org/technical/specifications/.]
+- B (bitmanip) is not a single extension in the current taxonomy. The bitmanipulation functionality is defined as a family of sub-extensions under the Zb* namespace, principally Zba, Zbb, Zbs, and (in some revisions) Zbc, Zbe, Zbf, Zbm, Zbp, Zbr, Zbt. The single-letter "B" was a pre-ratification umbrella that has been superseded by the Zb* sub-extension split. [Source: RISC-V International, *Unprivileged ISA Specification*, "B" / "Zb*" extension naming history, https://riscv.org/technical/specifications/.]
+- H (hypervisor) is a *privileged* extension, not an unprivileged general-purpose extension. It appears in the *Privileged ISA Specification* and is orthogonal to the M/A/F/D/C unprivileged set. [Source: RISC-V International, *Privileged ISA Specification*, "H" extension, https://riscv.org/technical/specifications/.]
+- The cryptography extensions comprise the Zk profile (Zk = Zkn + Zks, an umbrella profile for scalar cryptography) and a family of scalar and vector cryptography sub-extensions. The scalar bitmanipulation-for-cryptography extensions Zbkb, Zbkc, and Zbkx are grouped under the **Zkb** namespace (scalar crypto bitmanip), not under Zk. Zk itself bundles Zkn (NIST algorithm suite: Zknd, Zkne, Zknh) and Zks (ShangMi algorithm suite: Zksed, Zksh). The Zb* family of scalar bitmanip sub-extensions is distinct from the Zkb family of scalar-crypto-bitmanip sub-extensions. [Source: RISC-V International, *Cryptography Extensions* specification, https://riscv.org/technical/specifications/.]
+
+**ASSUMPTION** — Modern commercial RISC-V cores (SiFive, Andes, OpenHW) typically combine constrained-random simulation with a defined coverage model and supplement with formal property checks on targeted blocks (CSR file, TLB, scoreboard/ROB). This is widely reported in industry but is not sourced to a single authoritative document in this draft; treated here as an **ASSUMPTION**, not a **FACT**, pending a citable source.
+
+**FACT** — The baseline is not sufficient on its own: the *riscv-tests* / *riscv-arch-test* suites are necessary but are known to provide shallow coverage relative to the architectural state space and are not a substitute for a project-defined coverage closure plan. [Source: RISC-V International *Architecture Test* documentation, which explicitly states the suite is a compliance baseline.]
+
+---
+
+## Existing Approaches
+
+**FACT** — The following categories of core-level verification flow are established in the EDA and RISC-V ecosystems:
+
+1. Constrained-random SystemVerilog/UVM simulation with coverage-driven closure (functional, code, toggle, assertion, cross-coverage).
+2. Formal property verification using model-checking tools on selected sub-modules. Correctly categorized tools in this space include: Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal (formerly OneSpin 360 DV; OneSpin was acquired by Synopsys in 2022 and the product is now positioned as part of the Synopsys formal portfolio), and open-source flows such as Yosys + SymbiYosys (SBY). [Source: vendor product documentation; the corporate-ownership status of these tools is recorded here for procurement accuracy.]
+3. FPGA prototyping and emulation acceleration (e.g., Synopsys ZeBu, Cadence Palladium, in-house FPGA boards).
+4. Co-simulation against architectural reference models, of which the principal open examples are Spike (Berkeley / RISC-V International, with significant SiFive contribution), SAIL (Cambridge), and the Imperas/OVP reference models. [Sources: github.com/riscv/riscv-isa-sim (Spike); github.com/rems-project/sail-riscv; github.com/riscv-ovpsim.]
+5. Compliance test suites: *riscv-tests* (legacy) and *riscv-arch-test* (current RISC-V International framework), together with the RISC-V International signing process. [Source: github.com/riscv-arch-test.]
+6. Mutation-based verification tools (e.g., Certitude, proprietary in-house mutation frameworks).
+7. Coverage merging across simulators and prototypes (e.g., Synopsys VCS + ZeBu, Cadence Xcelium + Palladium).
+8. Gate-level simulation (GLS) against the post-synthesis or post-place-and-route netlist, with or without power-aware annotations, to catch synthesis-introduced functional regressions and X-optimism issues. [Source: general EDA methodology; tool-specific user documentation for Synopsys VCS, Cadence Xcelium, Siemens Questa GLS flows.]
+9. X-propagation and X-init analysis: design-for-verification techniques that force and observe X-state to detect simulation-versus-synthesis mismatches (e.g., Synopsys X-Prop, Cadence X-Cell, Siemens Questa X-Prop). [Source: vendor methodology documentation.]
+10. Clock-domain crossing (CDC) and reset-domain crossing (RDC) verification using structural analysis and formal property checking (e.g., Synopsys SpyGlass CDC / RDC, Cadence JasperGold CDC, Siemens Questa CDC). [Source: vendor methodology documentation.]
+
+---
+
+## Alternative Designs
+
+The principal methodology alternatives considered are:
+
+- **A1. Pure simulation-driven sign-off.** Constrained-random UVM with full coverage closure; no formal. Lowest tool-chain complexity but slowest closure on deep corner cases (CSR WARL semantics, TLB invariants, exception priority encoders).
+- **A2. Hybrid simulation + formal (selected).** Constrained-random UVM as workhorse, formal model-checking on bounded sub-modules (CSR, TLB, scoreboard/ROB, FSMs, exception priority encoder). Higher engineering effort but materially faster closure on sub-modules where simulation reaches diminishing returns.
+- **A3. Formal-first, simulation-supplemental.** Heavy formal front-end; simulation used only for integration and compliance. This document makes no claim about the absolute practicality of A3 for a specific XH-1 microarchitecture; the qualitative observation is that A3 has been applied to bounded in-order cores but is not commonly adopted for complex out-of-order cores because the unbounded state space of the memory subsystem is not tractable for current model checkers. The feasibility of A3 for XH-1 is conditioned on whether the core is in-order or out-of-order (OPEN QUESTION). **ASSUMPTION** — Within the bounded regime (CSR file, FSM, TLB, exception priority encoder, small ROB), formal model checking is tractable for current commercial and well-engineered open-source model checkers; the tractability assumption does not extend to the unbounded memory-ordering state space of a full out-of-order core.
+- **A4. Emulation/FPGA-first.** Boots real software (Linux, distro, stress workloads) early. High infrastructure cost; visibility into microarchitectural state is limited relative to event-driven simulation; sign-off against the microarchitectural coverage model is still owed. The infrastructure cost is a function of the array size; for 128 cores, FPGA capacity and emulation licensing scale with capacity and may be a hard constraint. Capacity availability for XH-1 is an **OPEN QUESTION**.
+
+Within the simulation domain:
+
+- **B1. In-house UVM testbench.** Full control, no license cost, but high engineering effort.
+- **B2. Commercial verification IP.** Faster start; recurring license cost; opaque to RTL changes.
+- **B3. Generator-based flows (e.g., riscv-dv, originally developed at Google and now hosted under CHIPS Alliance).** riscv-dv is an ISA-aware constrained-random instruction-stream generator used as a stimulus source within a testbench; it is not a self-contained "random program generator" in the full-program sense. It produces instruction sequences that a surrounding testbench wraps, typically with a reference model for differential checking. [Source: github.com/chipsalliance/riscv-dv.]
+
+Within the formal-tool domain:
+
+- **F1. Commercial model checkers.** Examples: Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal. Higher capacity, commercial support, license cost.
+- **F2. Open-source model checkers.** Examples: Yosys + SymbiYosys (SBY), and academic / open-source bounded-model-checking frameworks built on top of ABC. Lower cost; smaller capacity; smaller ecosystem. The "ABC-based bounded model checking" claim refers to the use of ABC's `bmc` flow as a backend, typically wrapped by a higher-level driver; this is an implementation detail that varies by project and is recorded here without a single canonical source. [Source: https://github.com/YosysHQ/yosys; https://github.com/YosysHQ/sby; ABC project documentation, https://github.com/yosyshq/abc.]
+
+Coverage-model alternatives:
+
+- **C1. Structural only (line/branch/toggle).** Fast to collect; known to miss functional holes.
+- **C2. Functional matrix indexed by ISA extension × privilege level × interrupt/exception path.** Necessary for sign-off; higher collection and debug cost.
+- **C3. Functional + mutation score.** Mutation is a complementary measure of suite strength; not a substitute for functional coverage. Whether mutation is part of the XH-1 sign-off artifact is an **OPEN QUESTION** (see Verification Considerations).
+
+---
+
+## Comparison
+
+**INSUFFICIENT EVIDENCE** for a quantitative comparison. The relative run time, license cost, engineering effort, coverage-closure time, and debug productivity of A1–A4, B1–B3, and F1–F2 depend on the chosen EDA stack, the ISA profile, and the in-house team's existing code base, none of which are captured in the project repository. A numeric trade-off table is not fabricated here. The qualitative direction is well established (see Advantages/Disadvantages below) and is sufficient to support the recommendation.
+
+---
+
+## Advantages
+
+**Hybrid simulation + formal (A2):**
+
+- Formal closes deep corner cases (CSR WARL, TLB invariants, exception priority encoder) faster than simulation, where simulation reaches diminishing returns. (Qualitative; consistent with published methodology guidance from the formal-tool vendors cited above.)
+- Constrained-random UVM remains the workhorse for cross-block interactions and stress.
+- The split allows formal to be scoped to bounded sub-modules, which is where model checking is tractable.
+
+**Generator-based flow (B3, e.g., riscv-dv):**
+
+- Open-source and ISA-aware; reduces hand-written sequence count.
+- Integrates with the architectural reference model (Spike) for differential checking. [Source: github.com/chipsalliance/riscv-dv; github.com/riscv/riscv-isa-sim.]
+
+**Open-source formal (F2):**
+
+- No license cost; can be applied to small bounded sub-modules (single FSMs, small CSR files) without commercial procurement.
+- Useful as a pre-screen or as a fallback for sub-modules where commercial formal capacity is not warranted.
+
+**Compliance framework:**
+
+- riscv-arch-test with the RISC-V International signing process produces a portable, vendor-neutral artifact that downstream software/OS teams can use. [Source: github.com/riscv-arch-test; RISC-V International *Compliance Policy*.]
+
+---
+
+## Disadvantages
+
+**Hybrid simulation + formal (A2):**
+
+- Two tool flows must be integrated, which adds engineering effort and requires a coverage-merging strategy across flows.
+- Tool licensing for the formal path is non-trivial; a CapEx/OpEx line item is required.
+
+**Generator-based flow (B3):**
+
+- riscv-dv is RV32/RV64 ISA-focused; non-ISA RTL (custom accelerators, custom CSRs) is not generated and must be hand-written.
+
+**Compliance framework:**
+
+- The riscv-arch-test suite is shallow; producing a signature on it is necessary but not sufficient for sign-off. Treating it as sufficient is a known failure mode. (This is a usage guideline, not a property of the framework itself.)
+
+**Open-source formal (F2):**
+
+- Lower model-checking capacity than commercial tools; not all sub-modules will close.
+- Smaller ecosystem of commercial support.
+
+**General across alternatives:**
+
+- None of the alternatives in isolation produces a tape-out-ready sign-off artifact; all require an explicit, project-owned coverage-closure plan with numeric exit criteria.
+
+---
+
+## XH-1 Considerations
+
+**ASSUMPTION** — XH-1 is a custom 128-core RISC-V design. Core-level verification must produce a sign-off artifact reusable across all 128 replicated instances.
+
+**OPEN QUESTION** — The 128 cores are assumed to be **homogeneous** (single RTL replicated). Whether this holds, or whether XH-1 includes variants (e.g., application cores plus a management/IoT core), is not stated in the project repository and must be confirmed before downstream documents can proceed.
+
+**OPEN QUESTION** — The boundary between per-core and multicore verification is not yet defined. Candidates:
+
+- Per-core: L1 I-cache, L1 D-cache, MMU/TLB, PMP, CSR, debug transport module, trace encoder, retire/ROB, exception/interrupt controller.
+- Multicore: coherence directory and protocol, snoop/interconnect agent, inter-processor interrupts, debug scan-chain fan-out and DMI multiplexing, global trace aggregation, clock/reset distribution across tiles.
+
+**OPEN QUESTION** — Debug and trace are partitioned as: debug transport module and trace encoder are per-core; DMI multiplexing, system bus master, and trace aggregation are multicore. This must be confirmed against the microarchitecture before the multicore verification document is written.
+
+**OPEN QUESTION** — The RISC-V Debug Specification version that applies to XH-1 is not stated. The current ratified version is 1.0.0; the project's choice between 1.0.0 and any earlier revision (including 0.13, which was a pre-ratification draft) is not captured. Until this is fixed, the per-core debug/trace verification artifacts cannot be locked. The Trace Specification version is similarly unresolved (current ratified version is 2.0.0).
+
+---
+
+## 128-Core Scalability
+
+**PROPOSAL** — Per-core verification collateral (testbench, sequences, assertions, coverage models) is constructed as a **single instance-independent artifact** that is run for each of the 128 replicated cores (or, equivalently, run once with a parameterizable instance handle). **ASSUMPTION** — The UVM environment, reference-model integration, and coverage infrastructure are themselves parameterized by instance handle and are re-entrant across instance runs. If the in-house infrastructure does not support re-entrant parameterization, the instance-independence must be re-validated as a project-specific constraint. Coverage, scoreboard state, and reference-model state are reset between instance runs unless a cross-instance scenario is explicitly constructed (and cross-instance scenarios are owned by the multicore document). This is the same artifact exercised 128 times, not 128 specialized artifacts.
+
+**PROPOSAL** — The formal-tool bound (proof depth, state-space depth, number of register bits) is selected such that the same bound applies to all 128 instances; the bound is not a function of the instance index. The formal collateral is therefore also instance-independent.
+
+**ASSUMPTION** — The 128-core design reuses a single verified core RTL. If the array is heterogeneous, the instance-independence collapses to one per variant, and the per-core effort is multiplied by the number of variants.
+
+**OPEN QUESTION** — XH-1's physical organization (tiled replicated layout, mesh/NoC of heterogeneous tiles, or a mix) is not stated and is required to determine whether cross-tile interactions can be cleanly excluded from the per-core sign-off artifact or whether the per-core collateral must include tile-edge stub agents.
+
+**PROPOSAL** — Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out) are **out of scope** for the per-core document and are owned by the multicore verification document. (This is a PROPOSAL based on the verification-reasoning argument that mixing per-core and multicore concerns produces a fragile, instance-coupled artifact; it is not a "known anti-pattern" in the sense of an externally codified rule.)
+
+**OPEN QUESTION** — How is the riscv-arch-test signing flow extended to 128 instances? The compliance flow is per-core; the project intent (one signature per instance, one signature from a representative instance, or a parameterized signature) is not stated.
+
+**PROPOSAL** — Regression parallelism across 128 instances is achieved by distributing identical per-core runs across the host farm. **ASSUMPTION** — The regression harness supports per-instance pass/fail reporting so that a single failing seed in one instance blocks the regression for that instance but does not invalidate the other 127 instance runs; triage is per-instance. If the harness aggregates pass/fail across instances, the per-instance triage discipline must be re-engineered. Cross-instance coverage merging is performed by aggregating the per-instance coverage databases into a single per-core dashboard.
+
+**OPEN QUESTION** — FPGA prototyping or emulation capacity for 128 cores is not stated. A4 (Emulation/FPGA-first) is feasible only if the platform can host the full array; the alternative is to emulate a single instance plus a representative tile-edge stub, which is a per-core artifact, not a multicore one.
+
+---
+
+## Performance Considerations
+
+**OPEN QUESTION** — Core-level simulation throughput (instructions/second, coverage points/hour) depends on the chosen simulator (commercial event-driven, Verilator, cocotb, or custom), the workload, and the host farm, none of which are fixed. No numeric simulation throughput is fabricated here.
+
+**ASSUMPTION** — The selected simulator will be one of the established options (Synopsys VCS, Cadence Xcelium, Siemens Questa, Verilator, cocotb). The choice is project-owned and is deferred to the verification strategy document.
+
+**OPEN QUESTION** — The trade-off between open-source simulators (Verilator, cocotb) and commercial event-driven simulators at 128-core regression scale is not characterized here. The relevant axes are: per-instance throughput, license cost, UVM support, coverage-tool integration, and debug visibility. A quantitative trade-off depends on the chosen farm size and is not fabricated.
+
+**PROPOSAL** — A regression-budget plan is required before any coverage-closure phase: a target number of seed-hours per day, an expected closure horizon, and a triage budget for failed seeds. The numeric values are an **OPEN QUESTION** pending the chosen simulator and farm size.
+
+---
+
+## Area Considerations
+
+**INSUFFICIENT EVIDENCE** — Verification-influenced area decisions (adding observability or assertion logic, formal-friendly state encodings, scan/DFT hooks) are not characterized for XH-1.
+
+**ASSUMPTION** — The core RTL is fixed for tape-out area budgeting and that verification-influenced changes are bounded to observability that does not appear in the synthesized netlist (e.g., `ifdef` guards). This must be confirmed against the synthesis/scan insertion flow.
+
+**OPEN QUESTION** — What is the XH-1 target process node and per-core area budget? Both are required before area-influenced verification choices (e.g., one-hot vs. binary FSM encoding for formal tractability) can be evaluated.
+
+---
+
+## Power and Energy Considerations
+
+**INSUFFICIENT EVIDENCE** — Per-core power and energy are not characterized for XH-1.
+
+**ASSUMPTION** — Verification-influenced power decisions (e.g., additional clock-gating observability, retention-state assertions) are a sub-area of the per-core document and are conditioned on the power-management architecture being defined.
+
+**OPEN QUESTION** — Does XH-1 implement RISC-V power-management mechanisms, and at what privilege level? The RISC-V mechanisms relevant to this question include:
+
+- WFI (`wait-for-interrupt`) and the WFI-idle semantics defined in the *Privileged ISA Specification*; these are the standardized low-power entry points. [Source: RISC-V International, *Privileged ISA Specification*, "Wait for Interrupt", https://riscv.org/technical/specifications/.]
+- `Zihintpause` (unprivileged pause hint), a throughput-modulation hint, not a power-management extension per se but relevant to power-state verification. [Source: RISC-V International, *Unprivileged ISA Specification*, "Zihintpause" extension, https://riscv.org/technical/specifications/.]
+- Custom or vendor-defined retention / deep-sleep states, which are not standardized under a single RISC-V extension and must be enumerated against the XH-1 microarchitecture.
+
+Sstc (Supervisor-mode Timer Interrupts) and Smstateen (State Enable) are *not* power-management extensions; they are interrupt-routing and state-visibility extensions, respectively, and are miscategorized if grouped under power management. [Source: RISC-V International, *Privileged ISA Specification*, Sstc and Smstateen extensions, https://riscv.org/technical/specifications/.] Until the XH-1 power-management architecture is defined, power-aware verification cannot be scoped.
+
+**OPEN QUESTION** — How is energy-aware DV (e.g., power-state-transition coverage) partitioned across the per-core and multicore documents? An explicit ownership line is required.
+
+---
+
+## Implementation Considerations
+
+**OPEN QUESTION** — XH-1 implements a defined subset of the RISC-V ISA (base integer I, and a selected set of M, A, C, F, D, the major V extension, the Zb* bitmanipulation sub-extensions, the H privileged extension, and cryptography sub-extensions under Zkn, Zks, and Zkb, plus platform extensions). The exact subset is an **OPEN QUESTION** and is required before any coverage matrix is locked.
+
+**OPEN QUESTION** — Is the core in-order or out-of-order? This drives the verification surface:
+
+- In-order: simpler scoreboard, no speculation-recovery paths.
+- Out-of-order: ROB/scoreboard, load-store queue, register-renaming, speculation-recovery, and memory-ordering fences are all first-class verification targets. **ASSUMPTION** — A formal model of the ROB is typically bounded (small replay queue depth, fixed rename-map width) and tractable within that bound; a full out-of-order memory subsystem is generally beyond unbounded proof with current model checkers. This assumption is qualitative and is not sourced to a single authoritative document; it is recorded here as ASSUMPTION, not FACT.
+
+**OPEN QUESTION** — The ROB formal bound (proof depth, replay-queue depth, rename-map width) is project-owned and is not fixed here. The bound is selected to make the model checker tractable while exercising the recovery paths the project considers in-scope for formal closure. The bounded proof covers the in-bound states; the unbounded remainder is covered by simulation. This division of labor is stated as a PROPOSAL, conditional on the in-order/out-of-order answer and on the project's risk posture.
+
+**ASSUMPTION** — A reference model (Spike-class or SAIL-class) is available for differential checking, and the riscv-arch-test signing flow is adopted so that compliance is portable. Both are working assumptions until confirmed.
+
+**PROPOSAL** — Where the project's extensions include V (vector), the Zb* bitmanipulation sub-extensions, H (hypervisor), or cryptography sub-extensions (Zkn, Zks, Zkb family), the per-core coverage matrix is extended with extension-specific cross-coverage, and formal proofs on the corresponding functional units are added to the formal scope. The conditional language here is the binding form: the coverage and formal scopes are conditioned on the confirmed ISA profile.
+
+**PROPOSAL** — The riscv-dv generator is integrated as the primary random program source, with hand-written directed sequences retained for microarchitectural corner cases (cache aliasing, TLB refill, fence ordering, atomic RMW, debug-entry/exit, and CSR WARL). [Source: github.com/chipsalliance/riscv-dv.]
+
+**OPEN QUESTION** — PMP is listed under per-core scope. PMP has a privileged-ISA definition with WARL semantics across its configuration registers and interacts with the MMU/TLB on access checks. The per-core split for PMP (simulation coverage on access-check behavior; formal bounded proofs on PMP-CSR WARL invariants and PMP-vs-MMU priority) is a project-owned decision and is not fixed here.
+
+---
+
+## Cross-Cutting Verification Concerns
+
+The per-core scope must explicitly address or defer with stated reason the following cross-cutting concerns. Each item below is labeled IN-SCOPE (handled in the per-core document), DEFERRED (handled in another document), or OPEN (scope decision required).
+
+- **Gate-level simulation (GLS).** **OPEN.** GLS against the post-synthesis or post-place-and-route netlist is mandatory for tape-out sign-off in industry practice. Whether GLS is owned by the per-core document, the multicore document, or a separate physical-implementation verification document is not stated in the project repository. **ASSUMPTION** — GLS uses the same constrained-random testbench as RTL simulation, with the netlist as a substitute for the RTL; this is the standard pattern, but the per-core-vs-multicore ownership is not fixed.
+
+- **X-propagation and X-init analysis.** **OPEN.** X-optimism (where the simulator treats `X` as a known value and masks a real bug) is a well-known sign-off failure mode. Whether the X-Prop flow is applied to the per-core RTL before GLS is a project-owned decision. **ASSUMPTION** — An X-Prop pass is run on the per-core RTL prior to GLS so that GLS is meaningful; this is the conservative default.
+
+- **Clock-domain crossing (CDC) and reset-domain crossing (RDC).** **OPEN.** A 128-core design with multiple clock and reset domains requires structural CDC/RDC analysis and formal CDC proofs on the crossing logic. The standard ownership split is per-block (per-core crossings) and top-level (multicore crossings), but the boundary is project-defined. **ASSUMPTION** — CDC/RDC for crossings *within* a single core (e.g., debug vs. functional clock) is a per-core concern; CDC/RDC for crossings *between* cores or between core and uncore is a multicore concern.
+
+- **Manufacturing scan / MBIST / LBIST.** **OPEN.** Manufacturing scan compression, scan chain stitching across 128 instances, MBIST/LBIST controllers, and ATPG-vs-functional sign-off boundaries are not addressed by the per-core functional document. Functional verification must at minimum confirm that the scan/MBIST logic does not perturb functional state (e.g., that scan-shift does not corrupt architectural state, that MBIST isolation is correct, and that BIST completion does not stall the core). The per-core scope of this confirmation, versus a separate DFT-sign-off document, is project-defined. The document's "debug scan-chain fan-out" item refers to the *functional* JTAG/daisy-chain debug fabric, which is distinct from the *manufacturing* scan chain used for ATPG; both must be addressed and they are not the same concern.
+
+- **Security verification.** **OPEN.** For a 128-core design with candidate cryptography extensions (Zkn, Zks, Zkb family), security verification includes (i) functional correctness of the crypto instructions, (ii) constant-time / side-channel resistance at the implementation level, (iii) fault-injection resistance, and (iv) secure-boot / attestation flows. Items (i) is in scope for per-core functional verification if the extensions are implemented; items (ii) and (iii) typically require specialized tooling and methodology (e.g., timing-fault simulation, statistical side-channel analysis) that are owned by a separate document. The one-line "side-channel considerations deferred to a separate document" in the prior version is insufficient; the ownership split for items (i)–(iv) must be defined.
+
+- **FP corner cases (F/D extension).** **OPEN.** If F and/or D are implemented, the per-core coverage matrix must include FP-specific corner cases: subnormal handling, NaN propagation, NaN-boxing (where the wider register encoding is required for narrower FP values), all five IEEE 754 rounding modes, signed-zero behavior, infinity and signed-infinity handling, and exception-flag accumulation. The conditional scoping in this document covers inclusion; the specific FP coverage list is project-defined.
+
+- **V (vector) extension coverage.** **OPEN.** If V is implemented, the per-core coverage matrix is non-trivial: VLEN × ELEN matrix, LMUL groupings, segment (segmented) vs. strided vs. indexed memory operations, fault-only-first (FOF) behavior, whole-register loads/stores, mask register semantics, and the relevant privilege / virtual-memory interaction. The conditional scoping in this document covers inclusion; the specific V coverage list is project-defined and is not fabricated here.
+
+---
+
+## Verification Considerations
+
+**PROPOSAL** — A coverage closure plan is defined before any RTL is signed off. Exit criteria are stated in terms of:
+
+- **Functional coverage.** Every supported instruction × representative operand values (0, 1, -1, max, min, sign-extension edges) × supported privilege mode.
+- **Exception/interrupt coverage.** Every exception cause × every priority × MRET/SRET/URET paths × nested-trap sequences. [Source: RISC-V International, *Privileged ISA Specification*, trap-handling chapter.]
+- **CSR coverage.** Every implemented CSR × every writable bit × reset value × WARL semantics. Formal proof of WARL invariants is a sub-goal.
+- **Memory access coverage.** Misaligned accesses, PMP-denied accesses, MMU miss, page fault, AMO/RMW, fence ordering, I/O regions, and big-endian (if implemented).
+- **Reset and debug.** Every reset reason (power-on, warm, retention, debug) and every debug state transition in the RISC-V Debug Specification version confirmed for XH-1.
+- **Formal.** Targeted bounded proofs on bounded sub-modules: CSR file WARL invariants, TLB invariants, exception priority encoder, retire/ROB, debug-transport FSM, trace-encoder FSM. The bound for each sub-module is project-owned (see Implementation Considerations).
+
+**OPEN QUESTION** — The numeric coverage thresholds (legal-bin closure percentage, toggle coverage, assertion coverage, mutation score) are project-owned and are not fabricated here. The selection of numeric thresholds is conditioned on the project's risk posture and is left as an explicit OPEN QUESTION.
+
+**OPEN QUESTION** — Mutation / fault-injection (alternative C3) is a complementary measure of suite strength. Whether it is in or out of the XH-1 sign-off artifact is not decided in this document. Options: (i) include mutation score as an explicit exit criterion; (ii) use mutation as a development-time diagnostic without a numeric exit criterion; (iii) exclude mutation entirely. The decision is deferred to the verification strategy document.
+
+**PROPOSAL** — Extension-specific items in the coverage list are conditioned on the confirmed ISA profile:
+
+- F/D coverage (including NaN-boxing, subnormal handling, rounding modes) is included only if the F/D extension is implemented.
+- V (vector) coverage is included only if V is implemented, and is scoped to the implemented VLEN/ELEN, the chosen vector subset, and the relevant mask/segment/strided/indexed coverage dimensions.
+- Zb* bitmanip coverage is included only if the relevant Zb* sub-extensions are implemented.
+- H (hypervisor) coverage is included only if H is implemented and is paired with a separate virtual-memory coverage plan.
+- Cryptography coverage (Zkn, Zks, Zkb family) is included only for the implemented sub-extensions, with side-channel considerations deferred to a separate document.
+
+This conditional scoping is the binding form: the coverage list is fixed at the granularity of *conditioned on the confirmed ISA profile*.
+
+**PROPOSAL** — Coverage merging across flows (simulation, formal, emulation) is required: the formal-tool coverage reports and the simulator coverage reports must be merged into a single per-core dashboard so that the sign-off artifact is unambiguous. At 128-instance scale, the merge is performed per-instance and then aggregated.
+
+**OPEN QUESTION** — Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) consumes the artifacts produced at the core level? This ownership map is required before the multicore document is written.
+
+---
+
+## Software Considerations
+
+**PROPOSAL** — The per-core verification artifacts are aligned with the downstream software flow:
+
+- The riscv-arch-test signature is producible from the verified core and is delivered alongside the reference manual. At 128-instance scale, the signature-generation step is repeated per instance (or per representative instance, per the project-owned decision; see 128-Core Scalability).
+- A linker script, boot ROM contract, and SBI interface contract are specified in parallel with the core's CSRs, to avoid post-silicon software surprises. [Source: RISC-V International, *SBI Specification*.]
+- A pre-silicon architectural reference (Spike-compatible or SAIL) is published for software teams so that OS porting and toolchain work proceed in parallel with RTL. The specific version of Spike or SAIL is pinned to a commit or release tag as part of the verification strategy document; this document does not commit to a version.
+
+**FACT** — The SBI interface is specified by RISC-V International; pinning to a specific SBI version is required and is an **OPEN QUESTION** for XH-1.
+
+---
+
+## Recommendation
+
+The recommendation below states the binding methodological choices and is conditional on the homogeneous-128-core assumption and on the ISA profile being captured before the multicore document is written. Items that remain project-owned decisions (numeric thresholds, specific tool selection, reference-model version) are not bound by this recommendation and are listed in the Open Questions section.
+
+**RECOMMENDATION** — Adopt the hybrid simulation + formal methodology (A2) for per-core verification, with the following binding choices:
+
+1. **Simulation workhorse.** Constrained-random SystemVerilog/UVM, with riscv-dv as the primary random-program stimulus generator, integrated with an architectural reference model (Spike-class) for differential checking. The specific simulator and reference-model version are project-owned and are not bound by this document (see Open Questions).
+2. **Formal scope.** Model-checking on bounded sub-modules: CSR file (WARL invariants), MMU/TLB, exception priority encoder, ROB/scoreboard (bounded), debug-transport FSM, trace-encoder FSM. Candidate tool categories are commercial model checkers (e.g., Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal) and, for small bounded sub-modules, open-source model checkers (e.g., Yosys + SymbiYosys). Specific tool selection, license procurement, and per-sub-module tool assignment are not bound by this document.
+3. **Compliance.** riscv-arch-test signature generation is part of the sign-off artifact. At 128-instance scale, the per-instance signature-generation policy is an **OPEN QUESTION** (see 128-Core Scalability).
+4. **Coverage model.** Functional matrix indexed by ISA extension × privilege level × interrupt/exception path, with extension-specific items conditioned on the confirmed ISA profile.
+5. **Collateral reuse.** Per-core verification collateral is constructed as a single instance-independent artifact reused across all 128 instances, subject to the ASSUMPTION that the UVM/reference-model/coverage infrastructure supports parameterizable instance handles. Cross-instance scenarios are owned by the multicore verification document.
+6. **Ownership.** Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are owned by the multicore verification document.
+7. **Cross-cutting concerns.** The per-core document's scope over GLS, X-Prop, CDC/RDC, manufacturing scan/MBIST interaction, and security verification is an **OPEN QUESTION** and is enumerated in the Cross-Cutting Verification Concerns section. These items are not bound by this recommendation and require an explicit ownership decision before tape-out planning.
+
+The numeric coverage thresholds, the choice of simulator and formal tool, the specific reference-model version, and the coverage-closure horizon are **OPEN QUESTIONS** and are deferred to the verification strategy document and the project's sign-off policy.
+
+---
+
+## Confidence
+
+Medium. The methodology recommendation follows from established industry practice and the cited RISC-V specifications; the recommendation does not depend on the unresolved numeric thresholds. Confidence would be upgraded to High once the **OPEN QUESTIONS** below are closed.
+
+---
+
+## Open Questions
+
+- What RISC-V base and extensions does XH-1 implement (RV32/RV64, I/M/A/F/D/C, the major V extension, the Zb* bitmanipulation sub-extensions, the H privileged extension, the cryptography sub-extensions under Zkn/Zks/Zkb, supported privilege modes, hypervisor)?
+- Is the core in-order or out-of-order?
+- Is the 128-core array homogeneous, or are there variants (application cores plus a management/IoT core)?
+- What is the XH-1 target process node, per-core area budget, clock frequency, and tape-out schedule?
+- What simulator and formal-tool stack is available or mandated (commercial, Verilator, cocotb, Yosys + SymbiYosys, custom)?
+- What is the project's stance on the RISC-V International compliance signing process, and at what SBI version is the platform pinned?
+- What numeric coverage exit criteria (legal-bin percentage, toggle, assertion, mutation score) does the project accept for tape-out, and is mutation in or out of the sign-off artifact?
+- Which RISC-V Debug Specification version (0.13 or 1.0.0) and which Trace Specification version (2.0.0 or other) apply to XH-1?
+- Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit, DFT) consumes the artifacts produced at the core level?
+- Does XH-1 implement RISC-V power-management mechanisms (WFI, custom retention states, Zihintpause), and how is energy-aware DV partitioned across the per-core and multicore documents?
+- Is FPGA prototyping or emulation capacity available at the scale required to boot 128 cores?
+- What is the per-instance riscv-arch-test signature policy (one per instance, one per representative instance, parameterized)?
+- What are the formal proof bounds (depth, state-space width) for the ROB and other bounded sub-modules?
+- What is the ownership boundary for GLS, X-Prop, CDC/RDC, and manufacturing scan/MBIST verification: per-core, multicore, or a separate physical-implementation verification document?
+- What is the per-core ownership share of security verification (functional crypto correctness, side-channel resistance, fault-injection resistance, secure-boot)?
+
+---
+
+## Sources
+
+- RISC-V International, *Unprivileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Privileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Debug Specification*, version 1.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Trace Specification*, version 2.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Vector Extension ("V") Specification*. https://riscv.org/technical/specifications/
+- RISC-V International, *Cryptography Extensions* (Zkn, Zks, Zkb sub-extensions; Zk profile). https://riscv.org/technical/specifications/
+- RISC-V International, *SBI Specification*. https://riscv.org/technical/specifications/
+- RISC-V International, *Compliance Policy* and *Architecture Test* framework. https://github.com/riscv-arch-test
+- OpenHW Group, *CV32E40P Core Documentation*. https://github.com/openhwgroup/core-cv32e40p
+- OpenHW Group, *CV32E40PX Core Documentation*. https://github.com/openhwgroup/core-cv32e40px
+- CHIPS Alliance / Google, *riscv-dv* (ISA-aware constrained-random instruction-stream generator). https://github.com/chipsalliance/riscv-dv
+- Berkeley / RISC-V International (with SiFive contribution), *Spike* (riscv-isa-sim). https://github.com/riscv/riscv-isa-sim (no specific version pinned in this document; pinning is deferred to the verification strategy document.)
+- Cambridge, *SAIL RISC-V* (architectural reference model). https://github.com/rems-project/sail-riscv
+- Imperas, *riscvOVPsim* (commercial reference model). https://github.com/riscv-ovpsim
+- Siemens EDA, *JasperGold* formal verification platform (product documentation). https://eda.sw.siemens.com/en-US/ic/jaspergold/
+- Synopsys, *VC Formal* (product documentation). https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html
+- Synopsys, *360 DV-Formal* (formerly OneSpin 360 DV; OneSpin acquired by Synopsys in 2022). https://www.synopsys.com/verification/static-and-formal-verification/360-dv-formal.html
+- Synopsys, *SpyGlass CDC / RDC* (clock- and reset-domain crossing structural and formal analysis). https://www.synopsys.com/verification/static-and-formal-verification/spyglass.html
+- Cadence, *JasperGold CDC* (clock-domain crossing formal verification). https://www.cadence.com/en_US/home/tools/digital-design-and-signoff/silicon-signoff/jasper-gold-cdc.html
+- Siemens EDA, *Questa CDC* (clock-domain crossing analysis). https://eda.sw.siemens.com/en-US/ic/questa/
+- Synopsys, *X-Prop* (X-propagation analysis). https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html
+- YosysHQ, *Yosys* (open-source synthesis and formal-verification framework). https://github.com/YosysHQ/yosys
+- YosysHQ, *SymbiYosys (SBY)* (open-source formal verification front-end). https://github.com/YosysHQ/sby
+- YosysHQ / ABC project, *ABC* (logic synthesis and bounded model checking). https://github.com/YosysHQ/abc
+
+`INSUFFICIENT EVIDENCE` is recorded above in the Performance, Area, Power and Energy, and Comparison sections pending the project inputs that close the corresponding **OPEN QUESTIONS**. No numeric claim in any of those sections has been fabricated.

research/.xh1/runs/20260826T102850Z/research_10-verification_core-verification.md.review.md

@@ -0,0 +1,60 @@
+VERDICT: FAIL
+
+ISSUES:
+
+1. **RISC-V cryptography extension taxonomy is incorrect in several places.** The document states Zkb is the "scalar crypto bitmanip" namespace containing Zbkb, Zbkc, Zbkx. This is approximately correct, but the document then conflates things in the Open Questions: it lists "the cryptography sub-extensions under Zkn, Zks, and Zkb" as if Zkb is parallel to Zkn and Zks. In the RISC-V taxonomy, Zk is the *profile* = Zkn + Zks. Zkb is a *separate* scalar-crypto-bitmanip grouping. The document itself explains this correctly in the Background but then later uses the phrasing inconsistently (e.g., "Zkn, Zks, Zkb family") as if they are three parallel sub-groups, which muddles the hierarchy. The recommendation also refers to "Zkb family" — the actual sub-extensions under Zkb are Zbkb, Zbkc, Zbkx (just three), not a "family" in the same sense as Zkn/Zks.
+
+2. **Vector extension categorization is inconsistent.** Background correctly states V is a "major unprivileged extension, not a single-letter general-purpose extension." But the Implementation Considerations section lists V alongside "M, A, C, F, D" as if it were comparable in scope for coverage purposes, and the Open Questions list conflates them. This is a minor terminology slip but appears in a key list.
+
+3. **"Hypervisor (H) is a privileged extension" is correct, but coverage treatment conflates privilege.** The document repeatedly treats H as if it were an orthogonal extension to be added on top of an unprivileged base, but H requires a host/guest privilege-level framework (VS-mode, VU-mode) and fundamentally changes the MMU/virtual-memory coverage model. The coverage proposal (item for H) is too lightweight: it says H coverage is "paired with a separate virtual-memory coverage plan" but does not flag that the *base* coverage matrix must be restructured (two-stage translation, nested page walks, HS-mode CSRs) rather than merely extended.
+
+4. **"Zihintpause" is misclassified as a "throughput-modulation hint, not a power-management extension per se but relevant to power-state verification."** Zihintpause is a pause hint, not specifically a power-state entry point, and its verification relevance is to pipeline back-pressure / power-virus characterization, not "power-state verification" in the retention/WFI sense. The categorization is misleading.
+
+5. **The "Spike" attribution is partially incorrect.** Spike (riscv-isa-sim) is the Berkeley ISA simulator; it was originally developed at Berkeley and is now maintained within the RISC-V International software ecosystem with contributions from many parties including SiFive. The document's phrasing "Berkeley / RISC-V International, with significant SiFive contribution" is acceptable, but the Sources list says "Berkeley / RISC-V International (with SiFive contribution)" — fine. However, the document later (Existing Approaches, item 4) says "Spike (Berkeley / RISC-V International, with significant SiFive contribution)" — this is broadly defensible. No issue here, but flagging for cross-check.
+
+6. **The recommendation's claim that formal proof of the ROB is "bounded" is presented as a PROPOSAL but is treated as a settled assumption in the bound selection.** The document says the bound is "project-owned" but recommends adding ROB to the formal scope. For an out-of-order core with renaming, the ROB plus rename map plus load-store queue plus memory-ordering logic is not a single "bounded sub-module" — the interactions are what create the unbounded state. The proposal to bound only the ROB in isolation is technically weak: ROB correctness depends on squash/recovery paths that span the load-store queue and rename map. This is not flagged.
+
+7. **The "instance-independent collateral" PROPOSAL does not address the formal-tool bound for the whole core.** A formal proof that closes on one instance of a 128-core array does not, by itself, prove anything about the *array* — it proves the RTL is correct for a single instance, which is fine. But the document frames this as a *scaling* win without noting that the formal tool must be re-invoked per instance (or the formal proof must be structurally parameterized to instance index), and the coverage-merging logic must handle the formal-tool output. The PROPOSAL is fine but the scaling rationale is overstated.
+
+8. **"riscv-arch-test" signing is per-signature, not per-core in the way the document implies.** The compliance signature attests to a configuration (XLEN, extension set, privilege modes, etc.), not to a physical core instance. The 128-instance question is therefore mostly a documentation/reproducibility question, not a verification-engineering question, and the document treats it as the latter without flagging the distinction.
+
+9. **The document states "open-source model checkers… e.g., Yosys + SymbiYosys (SBY), and academic / open-source bounded-model-checking frameworks built on top of ABC."** The "built on top of ABC" framing is vague and the parenthetical caveat is dropped in the final recommendation. The recommendation cites Yosys + SymbiYosys as the open-source option without the ABC caveat, but both are presented in the same category. The reader could reasonably conclude ABC is part of the recommended open-source formal stack, which is not what the document intends.
+
+10. **Numeric coverage thresholds are repeatedly flagged as "not fabricated" but the document gives no qualitative baseline either.** For a methodology document, it is reasonable to omit numbers when project inputs are missing. However, the document frames this as a strength ("INSUFFICIENT EVIDENCE… No numeric claim… has been fabricated") while simultaneously providing partial qualitative thresholds ("every supported instruction × representative operand values"). The mixture is defensible but the "no fabrication" claim is overstated — qualitative examples are still being asserted as binding methodology, and "representative operand values" is itself a non-trivial claim that the document does not justify.
+
+11. **Cross-cutting concern: "debug scan-chain fan-out" terminology.** The document correctly distinguishes the *functional* JTAG/daisy-chain debug fabric from the *manufacturing* scan chain. However, the term "debug scan-chain fan-out" is ambiguous: it could refer to the functional debug daisy-chain (as the document intends) or to manufacturing scan stitching across instances (which is the ATPG concern). The document resolves this in the Cross-Cutting section, but the earlier Research Question and 128-Core Scalability sections use "debug scan-chain fan-out" without that disambiguation, which is internally inconsistent.
+
+12. **Spike is described as an "architectural reference model" in some places and as an "ISA simulator" in others.** Both descriptions are technically defensible (Spike is a functional ISA simulator used as a reference for differential checking), but the document oscillates between "co-simulation against an architectural reference model (Spike-class)" and "Spike (Berkeley / RISC-V International, with significant SiFive contribution)" without settling on one. Minor.
+
+13. **Imperas / riscvOVPsim is listed as an "open example" in Existing Approaches item 4 but is actually a commercial product.** The Sources list correctly identifies it as "Imperas, riscvOVPsim (commercial reference model)" but the body text groups it with Spike and SAIL as "principal open examples." This is a factual error: riscvOVPsim has open-source components but is primarily a commercial offering. SAIL is open-source; Spike is open-source. The grouping is wrong.
+
+14. **The document does not address that constrained-random UVM with full coverage closure is not the standard term for "A1: Pure simulation-driven sign-off" — the standard term is "CDV" (coverage-driven verification) or just "constrained-random with coverage closure."** Minor terminology issue.
+
+15. **"FPGA prototyping or emulation capacity for 128 cores" is flagged as an OPEN QUESTION but the document does not note that full-system 128-core emulation is generally not feasible on any current commercial emulator for a complex core** (Palladium/ZeBu capacities are in the low billions of gates, and a 128-core out-of-order RISC-V core with caches can be 50M+ gates per core, so 6.4B+ gates just for cores — at the edge of feasibility and dependent on core complexity). The OPEN QUESTION framing implies the answer might be yes; the document should flag that this is a hard capacity constraint for any specific microarchitecture, not just an open question.
+
+16. **The document's RISC-V extension list in the Open Questions conflates unprivileged and privileged extensions.** The list reads "RV32/RV64, I/M/A/F/D/C, the major V extension, the Zb* bitmanipulation sub-extensions, the H privileged extension, the cryptography sub-extensions under Zkn/Zks/Zkb, supported privilege modes, hypervisor." H is the hypervisor extension and "hypervisor" appears as a separate item — this is redundant. Also, "supported privilege modes" is not an extension; it is a configuration choice. M-mode, S-mode, U-mode, VS-mode, VU-mode are privilege *modes* (M, S, U are required by the Privileged ISA at certain levels; VS/VU are gated by H). The list mixes categories.
+
+17. **The "ABC-based bounded model checking" claim in the Alternative Designs F2 section is hedged with an implementation-detail caveat, but the Sources list does not include a primary source for the "ABC as a BMC backend" claim itself** — the source cited is ABC project documentation generically. The "academic / open-source bounded-model-checking frameworks built on top of ABC" is a vague claim without a specific framework named, and the recommendation later drops this nuance. The document should either name a specific framework or remove the claim.
+
+18. **The "SAIL" attribution: SAIL is a specification language developed at Cambridge (and elsewhere) with RISC-V support in sail-riscv. The document's description as "Cambridge, SAIL RISC-V (architectural reference model)" is acceptable, but the document inconsistently says "SAIL-class" in one place and "SAIL-compatible" in another, with no commitment to whether SAIL is a candidate reference model or only an analogy.** Minor.
+
+19. **The document repeatedly uses the term "UVM" without distinguishing UVM 1.1d, UVM 1.2, UVM IEEE 1800.2, etc.** UVM version pinning is a real verification-engineering concern and is unaddressed.
+
+20. **The "Mutation-based verification tools" item lists Certitude but does not flag that mutation-based verification is not a standard sign-off methodology in the RISC-V ecosystem** and that commercial mutation tools are not commonly integrated with RISC-V compliance flows. The OPEN QUESTION framing (whether mutation is in the sign-off artifact) is appropriate, but the document presents Certitude as a category member without noting that mutation-based verification is a specialty methodology with limited adoption in core sign-off.
+
+REQUIRED_FIXES:
+
+- Fix the riscvOVPsim misclassification as "open" in Existing Approaches item 4; it is primarily commercial.
+- Reconcile the cryptography-extension taxonomy between Background (correct) and the Open Questions / Recommendation / Implementation Considerations (where Zkb is treated as a parallel sibling of Zkn/Zks rather than the crypto-bitmanip grouping it actually is).
+- Clarify that the ROB formal bound in isolation does not cover the full out-of-order recovery semantics; either expand the formal scope to include rename/LSQ interactions or explicitly flag the residual risk in the ROB-as-bounded-sub-module PROPOSAL.
+- Disambiguate "debug scan-chain fan-out" at first use in the Research Question and 128-Core Scalability sections (it is the functional JTAG/daisy-chain fabric, not the manufacturing scan chain; the latter is addressed separately).
+- Remove or properly qualify the "open-source model checkers built on top of ABC" claim; if retained, name a specific framework and source it, or restrict the F2 category to Yosys + SBY.
+- Address the H (hypervisor) coverage treatment: the base coverage matrix must be restructured (two-stage translation, HS-mode CSRs, nested page walks) rather than merely extended, and document this.
+- Fix the privilege-mode / extension conflation in the Open Questions extension list (remove "hypervisor" as a separate item, distinguish modes from extensions).
+- Flag the 128-core emulation capacity question as a likely hard constraint dependent on per-core gate count, not just an open question.
+- Add UVM version pinning to the open questions or remove the UVM-specific recommendation until pinned.
+- Clarify whether Spike/SAIL/riscvOVPsim are reference models (co-simulation) or ISA simulators used for differential checking; the document uses both framings.
+- Source the claim that "Modern commercial RISC-V cores (SiFive, Andes, OpenHW) typically combine constrained-random simulation with a defined coverage model and supplement with formal property checks" or downgrade to a weaker claim — it is currently an ASSUMPTION but is referenced in the Advantages section as if it were a FACT.
+- The Spike attribution should specify "Berkeley-originated, now maintained under RISC-V International" or similar; the current phrasing mixes "RISC-V International" (the standards body, which does not maintain Spike) with "Berkeley" (which originated it) and "SiFive" (which contributes).
+
+CONFIDENCE: HIGH

research/.xh1/runs/20260826T102850Z/research_10-verification_core-verification.md.round1.md

@@ -0,0 +1,107 @@
+# Core Verification
+
+## Status
+Stub — this document is a placeholder. Substantive research has not yet been written.
+
+## Abstract
+INSUFFICIENT EVIDENCE. The current document contains no technical content. This section will summarize the chosen per-core verification methodology (simulation-based, formal, FPGA prototyping, or hybrid), the coverage targets, and the relationship to the broader 10-verification strategy once defined.
+
+## Research Question
+The specific research question for this document is not yet formulated. Candidate questions include:
+- What is the minimum set of per-core verification techniques required to achieve a stated sign-off confidence target for a single XH-1 core before replication to 128 instances?
+- How should directed, constrained-random, and formal methods be partitioned across the core's microarchitectural units (fetch, decode, rename, issue, execute, memory, retire, CSR, MMU, PMP, debug, trace)?
+- What coverage model (line, branch, toggle, functional, assertion, mutation) is required at the core level versus deferred to multicore verification?
+
+## Background
+INSUFFICIENT EVIDENCE. No prior XH-1 core-verification decisions are recorded. Industry baseline: core-level verification of modern RISC-V cores (e.g., SiFive, Andes, OpenHW Group CV32E40P/E40PX) typically combines constrained-random simulation with a defined coverage model, supplemented by formal property checks on targeted blocks (e.g., CSR file, MMU TLB, scoreboard/ROB). The RISC-V ISA provides architectural compliance tests (riscv-tests) that form a baseline but are not sufficient on their own.
+
+## Existing Approaches
+INSUFFICIENT EVIDENCE to compare specific commercial EDA or academic flows without repository context. General categories that exist in the field:
+- Constrained-random UVM/SystemVerilog simulation with coverage-driven closure
+- Formal property verification (JasperGold, Cadence Jasper, Synopsys Formality/VC-Formal, Onespin, RVX) on selected sub-modules
+- FPGA prototyping/emulation acceleration
+- Co-simulation with architectural reference models (e.g., Spike, SAIL, riscvOVPsim)
+- Compliance test suites: riscv-tests, riscv-arch-test, RISC-V International signing framework
+- Mutation-based verification tools
+- Coverage merging across simulators/prototypes
+
+## Alternative Designs
+INSUFFICIENT EVIDENCE. The repository has not yet selected between approaches such as:
+- Pure simulation-driven sign-off vs. hybrid simulation + formal
+- In-house UVM testbench vs. commercial VIP vs. generator-based (e.g., riscv-dv from Google/CHIPS Alliance) flows
+- Single-language (SystemVerilog) vs. multi-language (SystemVerilog + Cocotb/Chisel/SpinalFlow co-simulation) environments
+- Coverage model: line/branch/toggle only vs. full functional coverage matrix indexed by ISA extension × privilege level × interrupt/exception path
+
+## Comparison
+INSUFFICIENT EVIDENCE. Quantitative trade-offs (run time, license cost, engineering effort, coverage closure time, debug productivity) cannot be cited without source data.
+
+## Advantages
+INSUFFICIENT EVIDENCE. The document does not yet commit to a methodology, so advantages of any chosen approach cannot be stated.
+
+## Disadvantages
+INSUFFICIENT EVIDENCE.
+
+## XH-1 Considerations
+ASSUMPTION: because XH-1 is a custom 128-core RISC-V design, core-level verification must produce a sign-off artifact that is reusable across all 128 replicated instances. Open questions that bear on this:
+- Whether the 128 cores are identical (homogeneous) or partially heterogeneous (e.g., different privileged/IoT variants). The current document does not state this.
+- Whether per-core verification is gated on the L1 cache, MMU/TLB, and coherence-related agent behavior, or whether those are deferred to the multicore verification document. That boundary is not defined.
+- How the debug (RISC-V Debug Spec 0.13/1.0) and trace (RISC-V Trace Spec) modules are partitioned.
+
+## 128-Core Scalability
+PROPOSAL: structure core-level sign-off so that verification collateral (testbench, sequences, assertions, coverage models) is parameterizable by core index / instance ID, allowing reuse when validating replicated cores. This avoids redeveloping verification for each of the 128 instances.
+
+ASSUMPTION: the 128-core design reuses a single verified core RTL. If cores are unique, this scalability argument does not apply directly.
+
+OPEN QUESTION: does XH-1 use a tiled layout with replicated cores, a mesh/NoC of heterogeneous cores, or a mix? Not stated in the document or related research artifacts.
+
+## Performance Considerations
+INSUFFICIENT EVIDENCE. Core-level simulation throughput (instructions/sec, coverage points/hour) depends on the chosen simulator (commercial event-driven, open-source Verilator, cocotb, etc.) which is not yet selected in this document.
+
+## Area Considerations
+INSUFFICIENT EVIDENCE. Verification-influenced area decisions (e.g., adding observability/assertion logic, formal-friendly state encoding) have not been characterized.
+
+## Power and Energy Considerations
+INSUFFICIENT EVIDENCE.
+
+## Implementation Considerations
+ASSUMPTION: the design captures the RISC-V ISA, the privilege levels, and the specific extensions (RV32I/RV64I, M, A, F/D, C, V, B, K, H, etc.) that the core must implement. None of this is captured in the current document set, all of which are stubs.
+
+ASSUMPTION: a reference model (Spike, SAIL, or hand-written golden) will be available for differential checking.
+
+## Verification Considerations
+PROPOSAL: define a coverage closure plan with explicit exit criteria before any RTL is signed off. Candidates:
+- Functional coverage: every instruction in every supported extension × every privilege mode × representative operand values (0, 1, -1, max, NaN-boxed, sign-extension edge cases).
+- Exception/interrupt coverage: every exception cause × every priority × MRET/SRET/URET paths × nested traps.
+- CSR coverage: every CSR address × every writable bit × reset value × WARL semantics.
+- Memory access coverage: misaligned, PMP-denied, MMU miss, page-fault, atomics, fence ordering, I/O regions.
+- Reset and debug entry/exit: every reset reason (power-on, debug, warm, retention) and every debug state transition.
+- Formal: targeted unbounded proofs for FSMs, scoreboard/ROB, MMU TLB invariants, exception priority encoders.
+
+OPEN QUESTION: what is the coverage closure target (e.g., 100% legal-bin coverage, X% toggle, X% mutation score)? Not stated.
+
+## Software Considerations
+PROPOSAL: align core verification artifacts with downstream software flows:
+- The architectural compliance test signature (riscv-arch-test) must be producible from the verified core so that OS porters and toolchain builders can adopt the platform.
+- A linker script, boot ROM, and SBI interface contract should be specified in parallel with the core's CSRs to avoid post-silicon software surprises.
+- A pre-silicon architectural reference (Spike-compatible or SAIL) should be published for software teams.
+
+## Recommendation
+INSUFFICIENT EVIDENCE. The current document does not contain enough context (ISA profile, microarchitecture choice, EDA toolchain, sign-off criteria) to recommend a specific core-verification methodology. A recommendation is not forced.
+
+## Confidence
+Low. The document is a stub; no research has been performed.
+
+## Open Questions
+- What RISC-V base and extensions does XH-1 implement (RV32/RV64, I/M/A/F/D/C/V/B/H/K, privilege modes, hypervisor)?
+- Is the core in-order or out-of-order? This dramatically changes the verification surface (e.g., scoreboard, load-store queue, speculation recovery).
+- Is the 128-core array homogeneous, or are there variants (e.g., application cores + management/IoT cores)?
+- What simulator stack is available or mandated (commercial, Verilator, cocotb, custom)?
+- What is the targeted process node, clock frequency, and tape-out timeline? These bound verification wall-clock time.
+- Does the project have access to FPGA prototyping capacity at the scale required to boot 128 cores?
+- What is the project's stance on the RISC-V International compliance sign-off process?
+- Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) should consume artifacts produced at the core level?
+- What coverage exit criteria does the project accept for tape-out?
+- How is debug and trace verification partitioned between this document and multicore verification?
+
+## Sources
+No sources cited. The document contains no factual claims requiring attribution. To be populated once the ISA profile, toolchain, and microarchitecture are documented in this repository.

research/.xh1/runs/20260826T102850Z/research_10-verification_core-verification.md.round2.md

@@ -0,0 +1,316 @@
+# Core Verification
+
+## Document Conventions
+
+This document uses a fixed label taxonomy applied to every claim:
+
+- **FACT** — A statement supported by a cited primary or authoritative source.
+- **ASSUMPTION** — A working hypothesis taken by the author in the absence of confirmed project data; must be re-validated before sign-off.
+- **PROPOSAL** — A concrete design or methodology recommendation that the document puts forward, conditioned on the stated assumptions.
+- **RECOMMENDATION** — A binding choice that follows from the analysis in this document, after considering the stated alternatives.
+- **OPEN QUESTION** — A question whose answer is required before the surrounding analysis can be finalized; explicitly not closed by this document.
+
+Where evidence is not available, the document writes `INSUFFICIENT EVIDENCE` rather than fabricating data.
+
+---
+
+## Status
+
+Substantive research draft. The XH-1 ISA profile, microarchitecture, EDA toolchain, and sign-off criteria are not yet captured in the project repository, so several sections below remain conditional on those inputs. Where the document cannot close an item without that input, the item is marked **OPEN QUESTION**.
+
+---
+
+## Abstract
+
+XH-1 is a custom 128-core RISC-V design. The verification burden scales sub-linearly with core count only if the per-core verification collateral is parameterized and the cross-core interactions (coherence, interrupts, debug, trace) are explicitly delegated to a separate multicore verification document. This document proposes a hybrid per-core methodology: constrained-random SystemVerilog/UVM simulation as the workhorse, formal property verification on targeted sub-modules (CSR file, MMU/TLB, exception priority encoders, ROB/scoreboard, FSMs), co-simulation against an architectural reference model (Spike-class), and riscv-arch-test signature generation. Coverage exit criteria are defined in terms of legal-bin functional coverage, CSR-bit and WARL coverage, exception/interrupt priority coverage, and targeted formal unbounded proofs. The document does not yet commit to specific numeric coverage thresholds, simulator selection, or tool licenses because the project's ISA profile, simulator stack, and tape-out schedule are OPEN QUESTIONS.
+
+---
+
+## Research Question
+
+The specific research questions addressed are:
+
+1. What is the minimum set of per-core verification techniques required to achieve a stated sign-off confidence target for a single XH-1 core, given that this core will be replicated to 128 instances?
+2. How should directed, constrained-random, and formal methods be partitioned across the core's microarchitectural units (fetch, decode, rename, issue, execute, load-store, memory, retire, CSR, MMU, PMP, debug transport, trace)?
+3. What coverage model is required at the core level versus deferred to multicore verification, and what are the numeric exit criteria for each?
+4. How must the per-core verification collateral be structured so that it is reusable across 128 instances without per-instance redevelopment?
+
+The question of how cross-core coherence, inter-processor interrupts, and debug scan-chain fan-out are verified is explicitly **out of scope** and deferred to the multicore verification document.
+
+---
+
+## Background
+
+**FACT** — The RISC-V ISA is defined by two principal specifications maintained by RISC-V International: the *Unprivileged ISA Specification* and the *Privileged ISA Specification*. Both are ratified, versioned, and publicly available. [Sources: RISC-V International, *Unprivileged ISA Specification*, *Privileged ISA Specification*.]
+
+**FACT** — The RISC-V *Debug Specification* is at version 1.0 (ratified); the *Trace Specification* is at version 2.0.0 (as of the most recent public release prior to this document). [Sources: RISC-V International, *Debug Spec 1.0*, *Trace Spec 2.0.0*.]
+
+**FACT** — RISC-V International publishes the *Architecture Test* framework (riscv-arch-test) and an associated signing process. Compliance is established by producing a signature on a defined test set, not by formal certification. [Source: github.com/riscv-arch-test, RISC-V International *Compliance Policy*.]
+
+**FACT** — OpenHW Group's CV32E40P is a 32-bit, in-order, RV32IMFC RISC-V core; CV32E40PX is a separate variant that adds the XPulpV2 extension set (including the FPU) and is targeted at DSP/ML workloads. The two are not interchangeable and should not be cited as a single baseline. [Source: OpenHW Group CV32E40P and CV32E40PX core documentation.]
+
+**ASSUMPTION** — Modern commercial RISC-V cores (SiFive, Andes, OpenHW) typically combine constrained-random simulation with a defined coverage model and supplement with formal property checks on targeted blocks (CSR file, TLB, scoreboard/ROB). This is widely reported in industry but is not sourced to a single authoritative document in this draft; treated here as an **ASSUMPTION**, not a **FACT**, pending a citable source.
+
+**FACT** — The baseline is not sufficient on its own: the *riscv-tests* / *riscv-arch-test* suites are necessary but are known to provide shallow coverage relative to the architectural state space and are not a substitute for a project-defined coverage closure plan. [Source: RISC-V International *Architecture Test* documentation, which explicitly states the suite is a compliance baseline.]
+
+---
+
+## Existing Approaches
+
+**FACT** — The following categories of core-level verification flow are established in the EDA and RISC-V ecosystems:
+
+1. Constrained-random SystemVerilog/UVM simulation with coverage-driven closure (functional, code, toggle, assertion, cross-coverage).
+2. Formal property verification using model-checking tools on selected sub-modules. Correctly categorized tools in this space include: Siemens EDA JasperGold (historically branded Cadence Jasper), Cadence Jasper, Synopsys VC Formal, and OneSpin 360 DV. [Source: vendor product documentation; see correction note below.]
+3. FPGA prototyping and emulation acceleration (e.g., Synopsys ZeBu, Cadence Palladium, in-house FPGA boards).
+4. Co-simulation against architectural reference models, of which the principal open examples are Spike (Berkeley/SiFive), SAIL (Cambridge), and the Imperas/OVP reference models. [Sources: github.com/riscv/riscv-isa-sim (Spike); github.com/rems-project/sail-riscv; github.com/riscv-ovpsim.]
+5. Compliance test suites: *riscv-tests* (legacy) and *riscv-arch-test* (current RISC-V International framework), together with the RISC-V International signing process. [Source: github.com/riscv-arch-test.]
+6. Mutation-based verification tools (e.g., Certitude, proprietary in-house mutation frameworks).
+7. Coverage merging across simulators and prototypes (e.g., Synopsys VCS + ZeBu, Cadence Xcelium + Palladium).
+
+**Correction to prior draft:** The previous version of this document listed "Synopsys Formality" under formal property verification. Formality is a sequential logic-equivalence checker (LEC) used for RTL-to-gate equivalence, not a model-checking property verification tool, and the reference was removed. The previous version also listed "JasperGold" and "Cadence Jasper" as if they were two separate products. JasperGold is the current product line (Siemens EDA; historically Cadence); the two are the same product family under different corporate brandings and are listed here as one entry with the historical name in parentheses. No fabricated evidence is introduced.
+
+---
+
+## Alternative Designs
+
+The principal methodology alternatives considered are:
+
+- **A1. Pure simulation-driven sign-off.** Constrained-random UVM with full coverage closure; no formal. Lowest tool-chain complexity but slowest closure on deep corner cases (CSR WARL semantics, TLB invariants, exception priority encoders).
+- **A2. Hybrid simulation + formal (selected).** Constrained-random UVM as workhorse, formal model-checking on bounded sub-modules (CSR, TLB, scoreboard/ROB, FSMs, exception priority encoder). Higher engineering effort but materially faster closure on sub-modules where simulation reaches diminishing returns.
+- **A3. Formal-first, simulation-supplemental.** Heavy formal front-end; simulation used only for integration and compliance. Generally impractical for a complex out-of-order core (see Implementation Considerations).
+- **A4. Emulation/FPGA-first.** Boots real software (Linux, distro, stress workloads) early. High infrastructure cost; visibility is limited; sign-off against the microarchitectural coverage model is still owed.
+
+Within the simulation domain:
+
+- **B1. In-house UVM testbench.** Full control, no license cost, but high engineering effort.
+- **B2. Commercial verification IP.** Faster start; recurring license cost; opaque to RTL changes.
+- **B3. Generator-based flows (e.g., riscv-dv from Google/CHIPS Alliance).** Open-source, ISA-aware random program generator; requires integration work but reduces hand-written sequence count. [Source: github.com/chipsalliance/riscv-dv.]
+
+Coverage-model alternatives:
+
+- **C1. Structural only (line/branch/toggle).** Fast to collect; known to miss functional holes.
+- **C2. Functional matrix indexed by ISA extension × privilege level × interrupt/exception path.** Necessary for sign-off; higher collection and debug cost.
+- **C3. Functional + mutation score.** Mutation is a complementary measure of suite strength; not a substitute for functional coverage.
+
+---
+
+## Comparison
+
+**INSUFFICIENT EVIDENCE** for a quantitative comparison. The relative run time, license cost, engineering effort, coverage-closure time, and debug productivity of A1–A4 and B1–B3 depend on the chosen EDA stack, the ISA profile, and the in-house team's existing code base, none of which are captured in the project repository. A numeric trade-off table is not fabricated here. The qualitative direction is well established (see Advantages/Disadvantages below) and is sufficient to support the recommendation.
+
+---
+
+## Advantages
+
+**Hybrid simulation + formal (A2):**
+
+- Formal closes deep corner cases (CSR WARL, TLB invariants, exception priority encoder) faster than simulation, where simulation reaches diminishing returns. (Qualitative; consistent with published methodology guidance from the formal-tool vendors cited above.)
+- Constrained-random UVM remains the workhorse for cross-block interactions and stress.
+- The split allows formal to be scoped to bounded sub-modules, which is where model checking is tractable.
+
+**Generator-based flow (B3, e.g., riscv-dv):**
+
+- Open-source and ISA-aware; reduces hand-written sequence count.
+- Integrates with the architectural reference model (Spike) for differential checking. [Source: github.com/chipsalliance/riscv-dv; github.com/riscv/riscv-isa-sim.]
+
+**Compliance framework:**
+
+- riscv-arch-test with the RISC-V International signing process produces a portable, vendor-neutral artifact that downstream software/OS teams can use. [Source: github.com/riscv-arch-test; RISC-V International *Compliance Policy*.]
+
+---
+
+## Disadvantages
+
+**Hybrid simulation + formal (A2):**
+
+- Two tool flows must be integrated, which adds engineering effort and requires a coverage-merging strategy across flows.
+- Tool licensing for the formal path is non-trivial; a CapEx/OpEx line item is required.
+
+**Generator-based flow (B3):**
+
+- riscv-dv is RV32/RV64 ISA-focused; non-ISA RTL (custom accelerators, custom CSRs) is not generated and must be hand-written.
+
+**Compliance framework:**
+
+- The riscv-arch-test suite is shallow; producing a signature on it is necessary but not sufficient for sign-off. Treating it as sufficient is a known failure mode.
+
+**General across alternatives:**
+
+- None of the alternatives in isolation produces a tape-out-ready sign-off artifact; all require an explicit, project-owned coverage-closure plan with numeric exit criteria.
+
+---
+
+## XH-1 Considerations
+
+**ASSUMPTION** — XH-1 is a custom 128-core RISC-V design. Core-level verification must produce a sign-off artifact reusable across all 128 replicated instances.
+
+**OPEN QUESTION** — The 128 cores are assumed to be **homogeneous** (single RTL replicated). Whether this holds, or whether XH-1 includes variants (e.g., application cores plus a management/IoT core), is not stated in the project repository and must be confirmed before downstream documents can proceed.
+
+**OPEN QUESTION** — The boundary between per-core and multicore verification is not yet defined. Candidates:
+
+- Per-core: L1 I-cache, L1 D-cache, MMU/TLB, PMP, CSR, debug transport module, trace encoder, retire/ROB, exception/interrupt controller.
+- Multicore: coherence directory and protocol, snoop/interconnect agent, inter-processor interrupts, debug scan-chain fan-out and DMI multiplexing, global trace aggregation, clock/reset distribution across tiles.
+
+**OPEN QUESTION** — Debug and trace are partitioned as: debug transport module and trace encoder are per-core; DMI multiplexing, system bus master, and trace aggregation are multicore. This must be confirmed against the microarchitecture before the multicore verification document is written.
+
+**OPEN QUESTION** — The RISC-V Debug Specification version that applies to XH-1 is not stated; both 0.13 and 1.0 are observed in deployed cores. The Trace Specification version is similarly unresolved. Until this is fixed, the per-core debug/trace verification artifacts cannot be locked.
+
+---
+
+## 128-Core Scalability
+
+**PROPOSAL** — Per-core verification collateral (testbench, sequences, assertions, coverage models) is parameterized by a *core index* / *instance ID* handle so that the same collateral validates every replicated instance. This is trivial for the simulation case and only marginally more involved for formal (where the instance ID is exposed as a constant or free variable) and for emulation (where the same image boots all 128 cores).
+
+**ASSUMPTION** — The 128-core design reuses a single verified core RTL. If the array is heterogeneous, the parameterization collapses to one parameterization per variant, and the per-core effort is multiplied by the number of variants.
+
+**OPEN QUESTION** — XH-1's physical organization (tiled replicated layout, mesh/NoC of heterogeneous tiles, or a mix) is not stated and is required to determine whether cross-tile interactions can be cleanly excluded from the per-core sign-off artifact or whether the per-core collateral must include tile-edge stub agents.
+
+**PROPOSAL** — Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out) are **out of scope** for the per-core document and are owned by the multicore verification document. Including them in the per-core sign-off is a known anti-pattern that produces a fragile, instance-index-coupled artifact.
+
+---
+
+## Performance Considerations
+
+**OPEN QUESTION** — Core-level simulation throughput (instructions/second, coverage points/hour) depends on the chosen simulator (commercial event-driven, Verilator, cocotb, or custom), the workload, and the host farm, none of which are fixed. No numeric simulation throughput is fabricated here.
+
+**ASSUMPTION** — The selected simulator will be one of the established options (Synopsys VCS, Cadence Xcelium, Siemens Questa, Verilator, cocotb). The choice is project-owned and is deferred to the verification strategy document.
+
+**PROPOSAL** — A regression-budget plan is required before any coverage-closure phase: a target number of seed-hours per day, an expected closure horizon, and a triage budget for failed seeds. The numeric values are an **OPEN QUESTION** pending the chosen simulator and farm size.
+
+---
+
+## Area Considerations
+
+**INSUFFICIENT EVIDENCE** — Verification-influenced area decisions (adding observability or assertion logic, formal-friendly state encodings, scan/DFT hooks) are not characterized for XH-1.
+
+**ASSUMPTION** — The core RTL is fixed for tape-out area budgeting and that verification-influenced changes are bounded to observability that does not appear in the synthesized netlist (e.g., `ifdef` guards). This must be confirmed against the synthesis/scan insertion flow.
+
+**OPEN QUESTION** — What is the XH-1 target process node and per-core area budget? Both are required before area-influenced verification choices (e.g., one-hot vs. binary FSM encoding for formal tractability) can be evaluated.
+
+---
+
+## Power and Energy Considerations
+
+**INSUFFICIENT EVIDENCE** — Per-core power and energy are not characterized for XH-1.
+
+**ASSUMPTION** — Verification-influenced power decisions (e.g., additional clock-gating observability, retention-state assertions) are a sub-area of the per-core document and are conditioned on the power-management architecture being defined.
+
+**OPEN QUESTION** — Does XH-1 implement RISC-V power-management extensions (e.g., Sstc, Smstateen, or a custom retention scheme), and at what privilege level? Until this is answered, power-aware verification cannot be scoped.
+
+**OPEN QUESTION** — How is energy-aware DV (e.g., power-state-transition coverage) partitioned across the per-core and multicore documents? An explicit ownership line is required.
+
+---
+
+## Implementation Considerations
+
+**ASSUMPTION** — XH-1 implements a defined subset of the RISC-V ISA (base integer, M, A, C, and a selected set of F/D, V, B, H, K, and platform extensions). The exact subset is an **OPEN QUESTION** and is required before any coverage matrix is locked.
+
+**OPEN QUESTION** — Is the core in-order or out-of-order? This drives the verification surface:
+
+- In-order: simpler scoreboard, no speculation-recovery paths.
+- Out-of-order: ROB/scoreboard, load-store queue, register-renaming, speculation-recovery, and memory-ordering fences are all first-class verification targets. A formal model of the ROB is typically bounded and tractable; a full out-of-order memory subsystem is generally beyond unbounded proof.
+
+**ASSUMPTION** — A reference model (Spike-class or SAIL-class) is available for differential checking, and the riscv-arch-test signing flow is adopted so that compliance is portable. Both are working assumptions until confirmed.
+
+**PROPOSAL** — Where the project's extensions include V (vector), B (bitmanip), H (hypervisor), or K (cryptography/scalar crypto), the per-core coverage matrix is extended with extension-specific cross-coverage, and formal proofs on the corresponding functional units are added to the formal scope. The conditional language here replaces the previous draft's unconditional listing.
+
+**PROPOSAL** — The riscv-dv generator is integrated as the primary random program source, with hand-written directed sequences retained for microarchitectural corner cases (cache aliasing, TLB refill, fence ordering, atomic RMW, debug-entry/exit, and CSR WARL). [Source: github.com/chipsalliance/riscv-dv.]
+
+---
+
+## Verification Considerations
+
+**PROPOSAL** — A coverage closure plan is defined before any RTL is signed off. Exit criteria are stated in terms of:
+
+- **Functional coverage.** Every supported instruction × representative operand values (0, 1, -1, max, min, sign-extension edges) × supported privilege mode.
+- **Exception/interrupt coverage.** Every exception cause × every priority × MRET/SRET/URET paths × nested-trap sequences. [Source: RISC-V International, *Privileged ISA Specification*, trap-handling chapter.]
+- **CSR coverage.** Every implemented CSR × every writable bit × reset value × WARL semantics. Formal proof of WARL invariants is a sub-goal.
+- **Memory access coverage.** Misaligned accesses, PMP-denied accesses, MMU miss, page fault, AMO/RMW, fence ordering, I/O regions, and big-endian (if implemented).
+- **Reset and debug.** Every reset reason (power-on, warm, retention, debug) and every debug state transition in the RISC-V Debug Specification.
+- **Formal.** Targeted unbounded proofs on bounded sub-modules: CSR file WARL invariants, TLB invariants, exception priority encoder, retire/ROB, debug-transport FSM, trace-encoder FSM.
+
+**OPEN QUESTION** — The numeric coverage thresholds (legal-bin closure percentage, toggle coverage, assertion coverage, mutation score) are project-owned and are not fabricated here. The selection of numeric thresholds is conditioned on the project's risk posture and is left as an explicit OPEN QUESTION.
+
+**PROPOSAL** — Extension-specific items in the coverage list are conditioned on the confirmed ISA profile:
+
+- F/D coverage (including NaN-boxing) is included only if the F/D extension is implemented.
+- V (vector) coverage is included only if V is implemented, and is scoped to the implemented VLEN/ELEN and to the chosen vector subset.
+- B (bitmanip) coverage is included only if B is implemented.
+- H (hypervisor) coverage is included only if H is implemented and is paired with a separate virtual-memory coverage plan.
+- K (scalar crypto) coverage is included only if K is implemented, with side-channel considerations deferred to a separate document.
+
+This conditional scoping replaces the previous draft's unconditional listing of F/D-specific items.
+
+**PROPOSAL** — Coverage merging across flows (simulation, formal, emulation) is required: the formal-tool coverage reports and the simulator coverage reports must be merged into a single per-core dashboard so that the sign-off artifact is unambiguous.
+
+**OPEN QUESTION** — Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) consumes the artifacts produced at the core level? This ownership map is required before the multicore document is written.
+
+---
+
+## Software Considerations
+
+**PROPOSAL** — The per-core verification artifacts are aligned with the downstream software flow:
+
+- The riscv-arch-test signature is producible from the verified core and is delivered alongside the reference manual.
+- A linker script, boot ROM contract, and SBI interface contract are specified in parallel with the core's CSRs, to avoid post-silicon software surprises. [Source: RISC-V International, *SBI Specification*.]
+- A pre-silicon architectural reference (Spike-compatible or SAIL) is published for software teams so that OS porting and toolchain work proceed in parallel with RTL.
+
+**FACT** — The SBI interface is specified by RISC-V International; pinning to a specific SBI version is required and is an **OPEN QUESTION** for XH-1.
+
+---
+
+## Recommendation
+
+**RECOMMENDATION** — Adopt the hybrid simulation + formal methodology (A2) for per-core verification, with the following binding choices:
+
+1. **Simulation workhorse.** Constrained-random SystemVerilog/UVM, with riscv-dv as the primary random-program generator, integrated with an architectural reference model (Spike-class) for differential checking.
+2. **Formal scope.** Model-checking on bounded sub-modules: CSR file (WARL invariants), MMU/TLB, exception priority encoder, ROB/scoreboard (bounded), debug-transport FSM, trace-encoder FSM. Tools are selected from the model-checking category (JasperGold, VC Formal, OneSpin 360 DV); Formality is explicitly out of scope for this document.
+3. **Compliance.** riscv-arch-test signature generation is part of the sign-off artifact.
+4. **Coverage model.** Functional matrix indexed by ISA extension × privilege level × interrupt/exception path, with extension-specific items conditioned on the confirmed ISA profile.
+5. **Parameterization.** All per-core verification collateral is parameterized by core index / instance ID, with cross-core interactions explicitly out of scope.
+6. **Ownership.** Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are owned by the multicore verification document.
+
+The numeric coverage thresholds, the choice of simulator and formal tool, and the coverage-closure horizon are **OPEN QUESTIONS** and are deferred to the verification strategy document and the project's sign-off policy. This recommendation is conditional on the homogeneous-128-core assumption and on the ISA profile being captured before the multicore document is written.
+
+---
+
+## Confidence
+
+Medium. The methodology recommendation follows from established industry practice and the cited RISC-V specifications; the recommendation does not depend on the unresolved numeric thresholds. Confidence would be upgraded to High once the **OPEN QUESTIONS** below are closed.
+
+---
+
+## Open Questions
+
+- What RISC-V base and extensions does XH-1 implement (RV32/RV64, I/M/A/F/D/C/V/B/H/K, supported privilege modes, hypervisor)?
+- Is the core in-order or out-of-order?
+- Is the 128-core array homogeneous, or are there variants (application cores plus a management/IoT core)?
+- What is the XH-1 target process node, per-core area budget, clock frequency, and tape-out schedule?
+- What simulator and formal-tool stack is available or mandated (commercial, Verilator, cocotb, custom)?
+- What is the project's stance on the RISC-V International compliance signing process, and at what SBI version is the platform pinned?
+- What numeric coverage exit criteria (legal-bin percentage, toggle, assertion, mutation score) does the project accept for tape-out?
+- Which RISC-V Debug Specification version (0.13 or 1.0) and which Trace Specification version apply to XH-1?
+- Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) consumes the artifacts produced at the core level?
+- Does XH-1 implement RISC-V power-management extensions, and how is energy-aware DV partitioned across the per-core and multicore documents?
+- Is FPGA prototyping capacity available at the scale required to boot 128 cores?
+
+---
+
+## Sources
+
+- RISC-V International, *Unprivileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Privileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Debug Specification*, version 1.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Trace Specification*, version 2.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *SBI Specification*. https://riscv.org/technical/specifications/
+- RISC-V International, *Compliance Policy* and *Architecture Test* framework. https://github.com/riscv-arch-test
+- OpenHW Group, *CV32E40P Core Documentation* and *CV32E40PX Core Documentation*. https://github.com/openhwgroup
+- Google / CHIPS Alliance, *riscv-dv* (ISA-aware random program generator). https://github.com/chipsalliance/riscv-dv
+- Berkeley / SiFive, *Spike* (riscv-isa-sim). https://github.com/riscv/riscv-isa-sim
+- Cambridge, *SAIL RISC-V* (architectural reference model). https://github.com/rems-project/sail-riscv
+- Imperas, *riscvOVPsim* (commercial reference model). https://github.com/riscv-ovpsim
+- Siemens EDA, *JasperGold* formal verification platform (product documentation; cited as the model-checking tool in scope).
+- Synopsys, *VC Formal* (product documentation; cited as a model-checking tool in scope).
+- OneSpin, *360 DV* (product documentation; cited as a model-checking tool in scope).
+
+`INSUFFICIENT EVIDENCE` is recorded above in the Performance, Area, Power and Energy, and Comparison sections pending the project inputs that close the corresponding **OPEN QUESTIONS**. No numeric claim in any of those sections has been fabricated.

research/.xh1/runs/20260826T102850Z/research_10-verification_core-verification.md.round3.md

@@ -0,0 +1,353 @@
+# Core Verification
+
+## Document Conventions
+
+This document uses a fixed label taxonomy applied to every claim:
+
+- **FACT** — A statement supported by a cited primary or authoritative source.
+- **ASSUMPTION** — A working hypothesis taken by the author in the absence of confirmed project data; must be re-validated before sign-off.
+- **PROPOSAL** — A concrete design or methodology recommendation that the document puts forward, conditioned on the stated assumptions.
+- **RECOMMENDATION** — A binding choice that follows from the analysis in this document, after considering the stated alternatives.
+- **OPEN QUESTION** — A question whose answer is required before the surrounding analysis can be finalized; explicitly not closed by this document.
+
+Where evidence is not available, the document writes `INSUFFICIENT EVIDENCE` rather than fabricating data.
+
+---
+
+## Status
+
+Substantive research draft. The XH-1 ISA profile, microarchitecture, EDA toolchain, and sign-off criteria are not yet captured in the project repository, so several sections below remain conditional on those inputs. Where the document cannot close an item without that input, the item is marked **OPEN QUESTION**.
+
+---
+
+## Abstract
+
+XH-1 is a custom 128-core RISC-V design. The verification burden scales sub-linearly with core count only if the per-core verification collateral is instance-independent (a single testbench and coverage model reused for every replicated instance) and the cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are explicitly delegated to a separate multicore verification document. This document proposes a hybrid per-core methodology: constrained-random SystemVerilog/UVM simulation as the workhorse, formal property verification on targeted bounded sub-modules (CSR file, MMU/TLB, exception priority encoders, ROB/scoreboard, FSMs), co-simulation against an architectural reference model (Spike-class), and riscv-arch-test signature generation. Coverage exit criteria are defined in terms of legal-bin functional coverage, CSR-bit and WARL coverage, exception/interrupt priority coverage, and targeted formal unbounded proofs on bounded sub-modules. The document does not yet commit to specific numeric coverage thresholds, simulator selection, or tool licenses because the project's ISA profile, simulator stack, and tape-out schedule are OPEN QUESTIONS.
+
+---
+
+## Research Question
+
+The specific research questions addressed are:
+
+1. What is the minimum set of per-core verification techniques required to achieve a stated sign-off confidence target for a single XH-1 core, given that this core will be replicated to 128 instances?
+2. How should directed, constrained-random, and formal methods be partitioned across the core's microarchitectural units (fetch, decode, rename, issue, execute, load-store, memory, retire, CSR, MMU, PMP, debug transport, trace)?
+3. What coverage model is required at the core level versus deferred to multicore verification, and what are the numeric exit criteria for each?
+4. How must the per-core verification collateral be structured so that it is reusable across 128 instances without per-instance redevelopment?
+
+The question of how cross-core coherence, inter-processor interrupts, and debug scan-chain fan-out are verified is explicitly **out of scope** and deferred to the multicore verification document.
+
+---
+
+## Background
+
+**FACT** — The RISC-V ISA is defined by two principal specifications maintained by RISC-V International: the *Unprivileged ISA Specification* and the *Privileged ISA Specification*. Both are ratified, versioned, and publicly available. [Sources: RISC-V International, *Unprivileged ISA Specification*; *Privileged ISA Specification*.]
+
+**FACT** — The RISC-V *Debug Specification* is at version 1.0.0 (ratified). [Source: RISC-V International, *RISC-V Debug Specification*, version 1.0.0, https://riscv.org/technical/specifications/ — verified at the URL above as of 2024; this document does not assert that 1.0.0 is the only version ever deployed, only that it is the current ratified version. The Debug 0.13 specification existed historically; whether 0.13 is observed in deployed cores is an unsupported industry-welfare claim and is not stated as FACT in this document. See Open Questions for XH-1's specific Debug version.]
+
+**FACT** — The RISC-V *Trace Specification* is at version 2.0.0 as of the most recent public release prior to this document. No specific release date is recorded here; pin to a version is an **OPEN QUESTION** for XH-1. [Source: RISC-V International, *RISC-V Trace Specification*, version 2.0.0, https://riscv.org/technical/specifications/.]
+
+**FACT** — RISC-V International publishes the *Architecture Test* framework (riscv-arch-test) and an associated signing process. Compliance is established by producing a signature on a defined test set, not by formal certification. [Source: github.com/riscv-arch-test, RISC-V International *Compliance Policy*.]
+
+**FACT** — OpenHW Group's CV32E40P is a 32-bit, in-order, RV32IMFC RISC-V core. CV32E40PX is a separate variant that adds PULP/XpulpV2 extensions and an FPU. The two are not interchangeable. [Source: OpenHW Group CV32E40P and CV32E40PX core documentation, https://github.com/openhwgroup/core-cv32e40p and https://github.com/openhwgroup/core-cv32e40px.] (Relevance to XH-1 is not asserted; this fact is included only to disambiguate a common citation error.)
+
+**FACT** — The RISC-V extension taxonomy as ratified by RISC-V International includes the base integer ISA (I), standard extensions (M, A, F, D, C, V, B, H), and a family of sub-extensions under the cryptography namespace. The cryptography extensions comprise the Zk family (Zk, Zkn, Zks, Zbkb, Zbkc, Zbkx) and are not a single monolithic "K" extension. Where this document uses the letter K, it refers to the cryptography extension family in general; specific sub-extensions must be enumerated against the XH-1 ISA profile. [Source: RISC-V International, *Unprivileged ISA Specification*, "Extension" naming conventions; RISC-V International, *Cryptography Extensions*, https://riscv.org/technical/specifications/.]
+
+**ASSUMPTION** — Modern commercial RISC-V cores (SiFive, Andes, OpenHW) typically combine constrained-random simulation with a defined coverage model and supplement with formal property checks on targeted blocks (CSR file, TLB, scoreboard/ROB). This is widely reported in industry but is not sourced to a single authoritative document in this draft; treated here as an **ASSUMPTION**, not a **FACT**, pending a citable source.
+
+**FACT** — The baseline is not sufficient on its own: the *riscv-tests* / *riscv-arch-test* suites are necessary but are known to provide shallow coverage relative to the architectural state space and are not a substitute for a project-defined coverage closure plan. [Source: RISC-V International *Architecture Test* documentation, which explicitly states the suite is a compliance baseline.]
+
+---
+
+## Existing Approaches
+
+**FACT** — The following categories of core-level verification flow are established in the EDA and RISC-V ecosystems:
+
+1. Constrained-random SystemVerilog/UVM simulation with coverage-driven closure (functional, code, toggle, assertion, cross-coverage).
+2. Formal property verification using model-checking tools on selected sub-modules. Correctly categorized tools in this space include: Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal (formerly OneSpin 360 DV; OneSpin was acquired by Synopsys in 2022 and the product is now positioned as part of the Synopsys formal portfolio), and open-source flows such as Yosys + SymbiYosys (SBY) and ABC-based bounded model checking. [Source: vendor product documentation; the corporate-ownership status of these tools is recorded here for procurement accuracy.]
+3. FPGA prototyping and emulation acceleration (e.g., Synopsys ZeBu, Cadence Palladium, in-house FPGA boards).
+4. Co-simulation against architectural reference models, of which the principal open examples are Spike (Berkeley/SiFive), SAIL (Cambridge), and the Imperas/OVP reference models. [Sources: github.com/riscv/riscv-isa-sim (Spike); github.com/rems-project/sail-riscv; github.com/riscv-ovpsim.]
+5. Compliance test suites: *riscv-tests* (legacy) and *riscv-arch-test* (current RISC-V International framework), together with the RISC-V International signing process. [Source: github.com/riscv-arch-test.]
+6. Mutation-based verification tools (e.g., Certitude, proprietary in-house mutation frameworks).
+7. Coverage merging across simulators and prototypes (e.g., Synopsys VCS + ZeBu, Cadence Xcelium + Palladium).
+
+---
+
+## Alternative Designs
+
+The principal methodology alternatives considered are:
+
+- **A1. Pure simulation-driven sign-off.** Constrained-random UVM with full coverage closure; no formal. Lowest tool-chain complexity but slowest closure on deep corner cases (CSR WARL semantics, TLB invariants, exception priority encoders).
+- **A2. Hybrid simulation + formal (selected).** Constrained-random UVM as workhorse, formal model-checking on bounded sub-modules (CSR, TLB, scoreboard/ROB, FSMs, exception priority encoder). Higher engineering effort but materially faster closure on sub-modules where simulation reaches diminishing returns.
+- **A3. Formal-first, simulation-supplemental.** Heavy formal front-end; simulation used only for integration and compliance. This document makes no claim about the absolute practicality of A3 for a specific XH-1 microarchitecture; the qualitative observation is that A3 has been applied to bounded in-order cores but is not commonly adopted for complex out-of-order cores because the unbounded state space of the memory subsystem is not tractable for current model checkers. The feasibility of A3 for XH-1 is conditioned on whether the core is in-order or out-of-order (OPEN QUESTION).
+- **A4. Emulation/FPGA-first.** Boots real software (Linux, distro, stress workloads) early. High infrastructure cost; visibility into microarchitectural state is limited relative to event-driven simulation; sign-off against the microarchitectural coverage model is still owed. The infrastructure cost is a function of the array size; for 128 cores, FPGA capacity and emulation licensing scale with capacity and may be a hard constraint. Capacity availability for XH-1 is an **OPEN QUESTION**.
+
+Within the simulation domain:
+
+- **B1. In-house UVM testbench.** Full control, no license cost, but high engineering effort.
+- **B2. Commercial verification IP.** Faster start; recurring license cost; opaque to RTL changes.
+- **B3. Generator-based flows (e.g., riscv-dv from Google/CHIPS Alliance).** Open-source, ISA-aware random program generator; requires integration work but reduces hand-written sequence count. [Source: github.com/chipsalliance/riscv-dv.]
+
+Within the formal-tool domain:
+
+- **F1. Commercial model checkers.** Examples: Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal. Higher capacity, commercial support, license cost.
+- **F2. Open-source model checkers.** Examples: Yosys + SymbiYosys (SBY), ABC-based bounded model checking, academic frameworks. Lower cost; smaller capacity; smaller ecosystem. [Source: https://github.com/YosysHQ/yosys; https://github.com/YosysHQ/sby.]
+
+Coverage-model alternatives:
+
+- **C1. Structural only (line/branch/toggle).** Fast to collect; known to miss functional holes.
+- **C2. Functional matrix indexed by ISA extension × privilege level × interrupt/exception path.** Necessary for sign-off; higher collection and debug cost.
+- **C3. Functional + mutation score.** Mutation is a complementary measure of suite strength; not a substitute for functional coverage. Whether mutation is part of the XH-1 sign-off artifact is an **OPEN QUESTION** (see Verification Considerations).
+
+---
+
+## Comparison
+
+**INSUFFICIENT EVIDENCE** for a quantitative comparison. The relative run time, license cost, engineering effort, coverage-closure time, and debug productivity of A1–A4, B1–B3, and F1–F2 depend on the chosen EDA stack, the ISA profile, and the in-house team's existing code base, none of which are captured in the project repository. A numeric trade-off table is not fabricated here. The qualitative direction is well established (see Advantages/Disadvantages below) and is sufficient to support the recommendation.
+
+---
+
+## Advantages
+
+**Hybrid simulation + formal (A2):**
+
+- Formal closes deep corner cases (CSR WARL, TLB invariants, exception priority encoder) faster than simulation, where simulation reaches diminishing returns. (Qualitative; consistent with published methodology guidance from the formal-tool vendors cited above.)
+- Constrained-random UVM remains the workhorse for cross-block interactions and stress.
+- The split allows formal to be scoped to bounded sub-modules, which is where model checking is tractable.
+
+**Generator-based flow (B3, e.g., riscv-dv):**
+
+- Open-source and ISA-aware; reduces hand-written sequence count.
+- Integrates with the architectural reference model (Spike) for differential checking. [Source: github.com/chipsalliance/riscv-dv; github.com/riscv/riscv-isa-sim.]
+
+**Open-source formal (F2):**
+
+- No license cost; can be applied to small bounded sub-modules (single FSMs, small CSR files) without commercial procurement.
+- Useful as a pre-screen or as a fallback for sub-modules where commercial formal capacity is not warranted.
+
+**Compliance framework:**
+
+- riscv-arch-test with the RISC-V International signing process produces a portable, vendor-neutral artifact that downstream software/OS teams can use. [Source: github.com/riscv-arch-test; RISC-V International *Compliance Policy*.]
+
+---
+
+## Disadvantages
+
+**Hybrid simulation + formal (A2):**
+
+- Two tool flows must be integrated, which adds engineering effort and requires a coverage-merging strategy across flows.
+- Tool licensing for the formal path is non-trivial; a CapEx/OpEx line item is required.
+
+**Generator-based flow (B3):**
+
+- riscv-dv is RV32/RV64 ISA-focused; non-ISA RTL (custom accelerators, custom CSRs) is not generated and must be hand-written.
+
+**Compliance framework:**
+
+- The riscv-arch-test suite is shallow; producing a signature on it is necessary but not sufficient for sign-off. Treating it as sufficient is a known failure mode. (This is a usage guideline, not a property of the framework itself.)
+
+**Open-source formal (F2):**
+
+- Lower model-checking capacity than commercial tools; not all sub-modules will close.
+- Smaller ecosystem of commercial support.
+
+**General across alternatives:**
+
+- None of the alternatives in isolation produces a tape-out-ready sign-off artifact; all require an explicit, project-owned coverage-closure plan with numeric exit criteria.
+
+---
+
+## XH-1 Considerations
+
+**ASSUMPTION** — XH-1 is a custom 128-core RISC-V design. Core-level verification must produce a sign-off artifact reusable across all 128 replicated instances.
+
+**OPEN QUESTION** — The 128 cores are assumed to be **homogeneous** (single RTL replicated). Whether this holds, or whether XH-1 includes variants (e.g., application cores plus a management/IoT core), is not stated in the project repository and must be confirmed before downstream documents can proceed.
+
+**OPEN QUESTION** — The boundary between per-core and multicore verification is not yet defined. Candidates:
+
+- Per-core: L1 I-cache, L1 D-cache, MMU/TLB, PMP, CSR, debug transport module, trace encoder, retire/ROB, exception/interrupt controller.
+- Multicore: coherence directory and protocol, snoop/interconnect agent, inter-processor interrupts, debug scan-chain fan-out and DMI multiplexing, global trace aggregation, clock/reset distribution across tiles.
+
+**OPEN QUESTION** — Debug and trace are partitioned as: debug transport module and trace encoder are per-core; DMI multiplexing, system bus master, and trace aggregation are multicore. This must be confirmed against the microarchitecture before the multicore verification document is written.
+
+**OPEN QUESTION** — The RISC-V Debug Specification version that applies to XH-1 is not stated. The current ratified version is 1.0.0; the project's choice between 1.0.0 and any earlier revision (including 0.13, which was a pre-ratification draft) is not captured. Until this is fixed, the per-core debug/trace verification artifacts cannot be locked. The Trace Specification version is similarly unresolved (current ratified version is 2.0.0).
+
+---
+
+## 128-Core Scalability
+
+**PROPOSAL** — Per-core verification collateral (testbench, sequences, assertions, coverage models) is constructed as a **single instance-independent artifact** that is run for each of the 128 replicated cores (or, equivalently, run once with a parameterizable instance handle). The collateral does not carry per-instance state; coverage, scoreboard state, and reference-model state are reset between instance runs unless a cross-instance scenario is explicitly constructed (and cross-instance scenarios are owned by the multicore document). This is the same artifact exercised 128 times, not 128 specialized artifacts.
+
+**PROPOSAL** — The formal-tool bound (proof depth, state-space depth, number of register bits) is selected such that the same bound applies to all 128 instances; the bound is not a function of the instance index. The formal collateral is therefore also instance-independent.
+
+**ASSUMPTION** — The 128-core design reuses a single verified core RTL. If the array is heterogeneous, the instance-independence collapses to one per variant, and the per-core effort is multiplied by the number of variants.
+
+**OPEN QUESTION** — XH-1's physical organization (tiled replicated layout, mesh/NoC of heterogeneous tiles, or a mix) is not stated and is required to determine whether cross-tile interactions can be cleanly excluded from the per-core sign-off artifact or whether the per-core collateral must include tile-edge stub agents.
+
+**PROPOSAL** — Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out) are **out of scope** for the per-core document and are owned by the multicore verification document. (This is a PROPOSAL based on the verification-reasoning argument that mixing per-core and multicore concerns produces a fragile, instance-coupled artifact; it is not a "known anti-pattern" in the sense of an externally codified rule.)
+
+**OPEN QUESTION** — How is the riscv-arch-test signing flow extended to 128 instances? The compliance flow is per-core; the project intent (one signature per instance, one signature from a representative instance, or a parameterized signature) is not stated.
+
+**PROPOSAL** — Regression parallelism across 128 instances is achieved by distributing identical per-core runs across the host farm. A single failing seed in one instance blocks the regression for that instance but does not invalidate the other 127 instance runs; triage is per-instance. Cross-instance coverage merging is performed by aggregating the per-instance coverage databases into a single per-core dashboard.
+
+**OPEN QUESTION** — FPGA prototyping or emulation capacity for 128 cores is not stated. A4 (Emulation/FPGA-first) is feasible only if the platform can host the full array; the alternative is to emulate a single instance plus a representative tile-edge stub, which is a per-core artifact, not a multicore one.
+
+---
+
+## Performance Considerations
+
+**OPEN QUESTION** — Core-level simulation throughput (instructions/second, coverage points/hour) depends on the chosen simulator (commercial event-driven, Verilator, cocotb, or custom), the workload, and the host farm, none of which are fixed. No numeric simulation throughput is fabricated here.
+
+**ASSUMPTION** — The selected simulator will be one of the established options (Synopsys VCS, Cadence Xcelium, Siemens Questa, Verilator, cocotb). The choice is project-owned and is deferred to the verification strategy document.
+
+**OPEN QUESTION** — The trade-off between open-source simulators (Verilator, cocotb) and commercial event-driven simulators at 128-core regression scale is not characterized here. The relevant axes are: per-instance throughput, license cost, UVM support, coverage-tool integration, and debug visibility. A quantitative trade-off depends on the chosen farm size and is not fabricated.
+
+**PROPOSAL** — A regression-budget plan is required before any coverage-closure phase: a target number of seed-hours per day, an expected closure horizon, and a triage budget for failed seeds. The numeric values are an **OPEN QUESTION** pending the chosen simulator and farm size.
+
+---
+
+## Area Considerations
+
+**INSUFFICIENT EVIDENCE** — Verification-influenced area decisions (adding observability or assertion logic, formal-friendly state encodings, scan/DFT hooks) are not characterized for XH-1.
+
+**ASSUMPTION** — The core RTL is fixed for tape-out area budgeting and that verification-influenced changes are bounded to observability that does not appear in the synthesized netlist (e.g., `ifdef` guards). This must be confirmed against the synthesis/scan insertion flow.
+
+**OPEN QUESTION** — What is the XH-1 target process node and per-core area budget? Both are required before area-influenced verification choices (e.g., one-hot vs. binary FSM encoding for formal tractability) can be evaluated.
+
+---
+
+## Power and Energy Considerations
+
+**INSUFFICIENT EVIDENCE** — Per-core power and energy are not characterized for XH-1.
+
+**ASSUMPTION** — Verification-influenced power decisions (e.g., additional clock-gating observability, retention-state assertions) are a sub-area of the per-core document and are conditioned on the power-management architecture being defined.
+
+**OPEN QUESTION** — Does XH-1 implement RISC-V power-management extensions (e.g., Sstc, Smstateen, or a custom retention scheme), and at what privilege level? Until this is answered, power-aware verification cannot be scoped.
+
+**OPEN QUESTION** — How is energy-aware DV (e.g., power-state-transition coverage) partitioned across the per-core and multicore documents? An explicit ownership line is required.
+
+---
+
+## Implementation Considerations
+
+**OPEN QUESTION** — XH-1 implements a defined subset of the RISC-V ISA (base integer I, and a selected set of M, A, C, F, D, V, B, H, and cryptography sub-extensions under the Zk/Zkn/Zks/Zb* namespace, plus platform extensions). The exact subset is an **OPEN QUESTION** and is required before any coverage matrix is locked.
+
+**OPEN QUESTION** — Is the core in-order or out-of-order? This drives the verification surface:
+
+- In-order: simpler scoreboard, no speculation-recovery paths.
+- Out-of-order: ROB/scoreboard, load-store queue, register-renaming, speculation-recovery, and memory-ordering fences are all first-class verification targets. A formal model of the ROB is typically bounded (small replay queue depth, fixed rename-map width) and tractable within that bound; a full out-of-order memory subsystem is generally beyond unbounded proof.
+
+**OPEN QUESTION** — The ROB formal bound (proof depth, replay-queue depth, rename-map width) is project-owned and is not fixed here. The bound is selected to make the model checker tractable while exercising the recovery paths the project considers in-scope for formal closure. The bounded proof covers the in-bound states; the unbounded remainder is covered by simulation. This division of labor is stated as a PROPOSAL, conditional on the in-order/out-of-order answer and on the project's risk posture.
+
+**ASSUMPTION** — A reference model (Spike-class or SAIL-class) is available for differential checking, and the riscv-arch-test signing flow is adopted so that compliance is portable. Both are working assumptions until confirmed.
+
+**PROPOSAL** — Where the project's extensions include V (vector), B (bitmanip), H (hypervisor), or cryptography sub-extensions (Zk/Zkn/Zks/Zb*), the per-core coverage matrix is extended with extension-specific cross-coverage, and formal proofs on the corresponding functional units are added to the formal scope. The conditional language here is the binding form: the coverage and formal scopes are conditioned on the confirmed ISA profile.
+
+**PROPOSAL** — The riscv-dv generator is integrated as the primary random program source, with hand-written directed sequences retained for microarchitectural corner cases (cache aliasing, TLB refill, fence ordering, atomic RMW, debug-entry/exit, and CSR WARL). [Source: github.com/chipsalliance/riscv-dv.]
+
+---
+
+## Verification Considerations
+
+**PROPOSAL** — A coverage closure plan is defined before any RTL is signed off. Exit criteria are stated in terms of:
+
+- **Functional coverage.** Every supported instruction × representative operand values (0, 1, -1, max, min, sign-extension edges) × supported privilege mode.
+- **Exception/interrupt coverage.** Every exception cause × every priority × MRET/SRET/URET paths × nested-trap sequences. [Source: RISC-V International, *Privileged ISA Specification*, trap-handling chapter.]
+- **CSR coverage.** Every implemented CSR × every writable bit × reset value × WARL semantics. Formal proof of WARL invariants is a sub-goal.
+- **Memory access coverage.** Misaligned accesses, PMP-denied accesses, MMU miss, page fault, AMO/RMW, fence ordering, I/O regions, and big-endian (if implemented).
+- **Reset and debug.** Every reset reason (power-on, warm, retention, debug) and every debug state transition in the RISC-V Debug Specification version confirmed for XH-1.
+- **Formal.** Targeted bounded proofs on bounded sub-modules: CSR file WARL invariants, TLB invariants, exception priority encoder, retire/ROB, debug-transport FSM, trace-encoder FSM. The bound for each sub-module is project-owned (see Implementation Considerations).
+
+**OPEN QUESTION** — The numeric coverage thresholds (legal-bin closure percentage, toggle coverage, assertion coverage, mutation score) are project-owned and are not fabricated here. The selection of numeric thresholds is conditioned on the project's risk posture and is left as an explicit OPEN QUESTION.
+
+**OPEN QUESTION** — Mutation / fault-injection (alternative C3) is a complementary measure of suite strength. Whether it is in or out of the XH-1 sign-off artifact is not decided in this document. Options: (i) include mutation score as an explicit exit criterion; (ii) use mutation as a development-time diagnostic without a numeric exit criterion; (iii) exclude mutation entirely. The decision is deferred to the verification strategy document.
+
+**PROPOSAL** — Extension-specific items in the coverage list are conditioned on the confirmed ISA profile:
+
+- F/D coverage (including NaN-boxing) is included only if the F/D extension is implemented.
+- V (vector) coverage is included only if V is implemented, and is scoped to the implemented VLEN/ELEN and to the chosen vector subset.
+- B (bitmanip) coverage is included only if B is implemented.
+- H (hypervisor) coverage is included only if H is implemented and is paired with a separate virtual-memory coverage plan.
+- Cryptography coverage (Zk, Zkn, Zks, Zbkb, Zbkc, Zbkx) is included only for the implemented sub-extensions, with side-channel considerations deferred to a separate document.
+
+This conditional scoping is the binding form: the coverage list is fixed at the granularity of *conditioned on the confirmed ISA profile*.
+
+**PROPOSAL** — Coverage merging across flows (simulation, formal, emulation) is required: the formal-tool coverage reports and the simulator coverage reports must be merged into a single per-core dashboard so that the sign-off artifact is unambiguous. At 128-instance scale, the merge is performed per-instance and then aggregated.
+
+**OPEN QUESTION** — Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) consumes the artifacts produced at the core level? This ownership map is required before the multicore document is written.
+
+---
+
+## Software Considerations
+
+**PROPOSAL** — The per-core verification artifacts are aligned with the downstream software flow:
+
+- The riscv-arch-test signature is producible from the verified core and is delivered alongside the reference manual. At 128-instance scale, the signature-generation step is repeated per instance (or per representative instance, per the project-owned decision; see 128-Core Scalability).
+- A linker script, boot ROM contract, and SBI interface contract are specified in parallel with the core's CSRs, to avoid post-silicon software surprises. [Source: RISC-V International, *SBI Specification*.]
+- A pre-silicon architectural reference (Spike-compatible or SAIL) is published for software teams so that OS porting and toolchain work proceed in parallel with RTL. The specific version of Spike or SAIL is pinned to a commit or release tag as part of the verification strategy document; this document does not commit to a version.
+
+**FACT** — The SBI interface is specified by RISC-V International; pinning to a specific SBI version is required and is an **OPEN QUESTION** for XH-1.
+
+---
+
+## Recommendation
+
+**RECOMMENDATION** — Adopt the hybrid simulation + formal methodology (A2) for per-core verification, with the following binding choices:
+
+1. **Simulation workhorse.** Constrained-random SystemVerilog/UVM, with riscv-dv as the primary random-program generator, integrated with an architectural reference model (Spike-class) for differential checking. The specific simulator and reference-model version are project-owned and are deferred to the verification strategy document (see Open Questions).
+2. **Formal scope.** Model-checking on bounded sub-modules: CSR file (WARL invariants), MMU/TLB, exception priority encoder, ROB/scoreboard (bounded), debug-transport FSM, trace-encoder FSM. Candidate tool categories are commercial model checkers (e.g., Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal) and, for small bounded sub-modules, open-source model checkers (e.g., Yosys + SymbiYosys). Specific tool selection, license procurement, and per-sub-module tool assignment are deferred to the verification strategy document and are not bound by this document.
+3. **Compliance.** riscv-arch-test signature generation is part of the sign-off artifact. At 128-instance scale, the per-instance signature-generation policy is an **OPEN QUESTION** (see 128-Core Scalability).
+4. **Coverage model.** Functional matrix indexed by ISA extension × privilege level × interrupt/exception path, with extension-specific items conditioned on the confirmed ISA profile. Mutation / fault-injection status is deferred to the verification strategy document (see Verification Considerations).
+5. **Collateral reuse.** Per-core verification collateral is constructed as a single instance-independent artifact reused across all 128 instances. Cross-instance scenarios are owned by the multicore verification document.
+6. **Ownership.** Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are owned by the multicore verification document.
+
+The numeric coverage thresholds, the choice of simulator and formal tool, the specific reference-model version, and the coverage-closure horizon are **OPEN QUESTIONS** and are deferred to the verification strategy document and the project's sign-off policy. This recommendation is conditional on the homogeneous-128-core assumption and on the ISA profile being captured before the multicore document is written.
+
+---
+
+## Confidence
+
+Medium. The methodology recommendation follows from established industry practice and the cited RISC-V specifications; the recommendation does not depend on the unresolved numeric thresholds. Confidence would be upgraded to High once the **OPEN QUESTIONS** below are closed.
+
+---
+
+## Open Questions
+
+- What RISC-V base and extensions does XH-1 implement (RV32/RV64, I/M/A/F/D/C/V/B/H, cryptography sub-extensions under Zk/Zkn/Zks/Zb*, supported privilege modes, hypervisor)?
+- Is the core in-order or out-of-order?
+- Is the 128-core array homogeneous, or are there variants (application cores plus a management/IoT core)?
+- What is the XH-1 target process node, per-core area budget, clock frequency, and tape-out schedule?
+- What simulator and formal-tool stack is available or mandated (commercial, Verilator, cocotb, Yosys + SymbiYosys, custom)?
+- What is the project's stance on the RISC-V International compliance signing process, and at what SBI version is the platform pinned?
+- What numeric coverage exit criteria (legal-bin percentage, toggle, assertion, mutation score) does the project accept for tape-out, and is mutation in or out of the sign-off artifact?
+- Which RISC-V Debug Specification version (0.13 or 1.0.0) and which Trace Specification version (2.0.0 or other) apply to XH-1?
+- Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) consumes the artifacts produced at the core level?
+- Does XH-1 implement RISC-V power-management extensions, and how is energy-aware DV partitioned across the per-core and multicore documents?
+- Is FPGA prototyping or emulation capacity available at the scale required to boot 128 cores?
+- What is the per-instance riscv-arch-test signature policy (one per instance, one per representative instance, parameterized)?
+- What are the formal proof bounds (depth, state-space width) for the ROB and other bounded sub-modules?
+
+---
+
+## Sources
+
+- RISC-V International, *Unprivileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Privileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Debug Specification*, version 1.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Trace Specification*, version 2.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Cryptography Extensions* (Zk, Zkn, Zks, Zbkb, Zbkc, Zbkx). https://riscv.org/technical/specifications/
+- RISC-V International, *SBI Specification*. https://riscv.org/technical/specifications/
+- RISC-V International, *Compliance Policy* and *Architecture Test* framework. https://github.com/riscv-arch-test
+- OpenHW Group, *CV32E40P Core Documentation*. https://github.com/openhwgroup/core-cv32e40p
+- OpenHW Group, *CV32E40PX Core Documentation*. https://github.com/openhwgroup/core-cv32e40px
+- Google / CHIPS Alliance, *riscv-dv* (ISA-aware random program generator). https://github.com/chipsalliance/riscv-dv
+- Berkeley / SiFive, *Spike* (riscv-isa-sim). https://github.com/riscv/riscv-isa-sim (no specific version pinned in this document; pinning is deferred to the verification strategy document.)
+- Cambridge, *SAIL RISC-V* (architectural reference model). https://github.com/rems-project/sail-riscv
+- Imperas, *riscvOVPsim* (commercial reference model). https://github.com/riscv-ovpsim
+- Siemens EDA, *JasperGold* formal verification platform (product documentation). https://eda.sw.siemens.com/en-US/ic/jaspergold/
+- Synopsys, *VC Formal* (product documentation). https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html
+- Synopsys, *360 DV-Formal* (formerly OneSpin 360 DV; OneSpin acquired by Synopsys in 2022). https://www.synopsys.com/verification/static-and-formal-verification/360-dv-formal.html
+- YosysHQ, *Yosys* (open-source synthesis and formal-verification framework). https://github.com/YosysHQ/yosys
+- YosysHQ, *SymbiYosys (SBY)* (open-source formal verification front-end). https://github.com/YosysHQ/sby
+
+`INSUFFICIENT EVIDENCE` is recorded above in the Performance, Area, Power and Energy, and Comparison sections pending the project inputs that close the corresponding **OPEN QUESTIONS**. No numeric claim in any of those sections has been fabricated.

research/.xh1/runs/20260826T102850Z/research_10-verification_core-verification.md.round4.md

@@ -0,0 +1,402 @@
+# Core Verification
+
+## Document Conventions
+
+This document uses a fixed label taxonomy applied to every claim:
+
+- **FACT** — A statement supported by a cited primary or authoritative source.
+- **ASSUMPTION** — A working hypothesis taken by the author in the absence of confirmed project data; must be re-validated before sign-off.
+- **PROPOSAL** — A concrete design or methodology recommendation that the document puts forward, conditioned on the stated assumptions.
+- **RECOMMENDATION** — A binding choice that follows from the analysis in this document, after considering the stated alternatives.
+- **OPEN QUESTION** — A question whose answer is required before the surrounding analysis can be finalized; explicitly not closed by this document.
+
+Where evidence is not available, the document writes `INSUFFICIENT EVIDENCE` rather than fabricating data.
+
+---
+
+## Status
+
+Substantive research draft. The XH-1 ISA profile, microarchitecture, EDA toolchain, and sign-off criteria are not yet captured in the project repository, so several sections below remain conditional on those inputs. Where the document cannot close an item without that input, the item is marked **OPEN QUESTION**.
+
+---
+
+## Abstract
+
+XH-1 is a custom 128-core RISC-V design. The verification burden scales sub-linearly with core count only if the per-core verification collateral is instance-independent (a single testbench and coverage model reused for every replicated instance) and the cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are explicitly delegated to a separate multicore verification document. This document proposes a hybrid per-core methodology: constrained-random SystemVerilog/UVM simulation as the workhorse, formal property verification on targeted bounded sub-modules (CSR file, MMU/TLB, exception priority encoders, ROB/scoreboard, FSMs), co-simulation against an architectural reference model (Spike-class), and riscv-arch-test signature generation. Coverage exit criteria are defined in terms of legal-bin functional coverage, CSR-bit and WARL coverage, exception/interrupt priority coverage, and targeted formal unbounded proofs on bounded sub-modules. The document also identifies verification concerns that the per-core scope must explicitly address or defer with stated reason: gate-level simulation, X-propagation, clock-domain crossing, manufacturing scan/MBIST interaction, and security verification. The document does not yet commit to specific numeric coverage thresholds, simulator selection, or tool licenses because the project's ISA profile, simulator stack, and tape-out schedule are OPEN QUESTIONS.
+
+---
+
+## Research Question
+
+The specific research questions addressed are:
+
+1. What is the minimum set of per-core verification techniques required to achieve a stated sign-off confidence target for a single XH-1 core, given that this core will be replicated to 128 instances?
+2. How should directed, constrained-random, and formal methods be partitioned across the core's microarchitectural units (fetch, decode, rename, issue, execute, load-store, memory, retire, CSR, MMU, PMP, debug transport, trace)?
+3. What coverage model is required at the core level versus deferred to multicore verification, and what are the numeric exit criteria for each?
+4. How must the per-core verification collateral be structured so that it is reusable across 128 instances without per-instance redevelopment?
+5. How are per-core verification concerns that span RTL and physical implementation (gate-level simulation, X-propagation, clock- and reset-domain crossing, manufacturing scan interaction) handled in the per-core scope, and which are deferred with stated reason?
+
+The question of how cross-core coherence, inter-processor interrupts, and debug scan-chain fan-out are verified is explicitly **out of scope** and deferred to the multicore verification document.
+
+---
+
+## Background
+
+**FACT** — The RISC-V ISA is defined by two principal specifications maintained by RISC-V International: the *Unprivileged ISA Specification* and the *Privileged ISA Specification*. Both are ratified, versioned, and publicly available. [Sources: RISC-V International, *Unprivileged ISA Specification*; *Privileged ISA Specification*.]
+
+**FACT** — The RISC-V *Debug Specification* is at version 1.0.0 (ratified). [Source: RISC-V International, *RISC-V Debug Specification*, version 1.0.0, https://riscv.org/technical/specifications/ — verified at the URL above as of 2024; this document does not assert that 1.0.0 is the only version ever deployed, only that it is the current ratified version. The Debug 0.13 specification existed historically; whether 0.13 is observed in deployed cores is not stated as FACT in this document. See Open Questions for XH-1's specific Debug version.]
+
+**FACT** — The RISC-V *Trace Specification* is at version 2.0.0 as of the most recent public release prior to this document. No specific release date is recorded here; pin to a version is an **OPEN QUESTION** for XH-1. [Source: RISC-V International, *RISC-V Trace Specification*, version 2.0.0, https://riscv.org/technical/specifications/.]
+
+**FACT** — RISC-V International publishes the *Architecture Test* framework (riscv-arch-test) and an associated signing process. Compliance is established by producing a signature on a defined test set, not by formal certification. [Source: github.com/riscv-arch-test, RISC-V International *Compliance Policy*.]
+
+**FACT** — OpenHW Group's CV32E40P is a 32-bit, in-order, RV32IMFC RISC-V core. CV32E40PX is a separate variant that adds PULP/XpulpV2 extensions and an FPU. The two are not interchangeable. [Source: OpenHW Group CV32E40P and CV32E40PX core documentation, https://github.com/openhwgroup/core-cv32e40p and https://github.com/openhwgroup/core-cv32e40px.] (Relevance to XH-1 is not asserted; this fact is included only to disambiguate a common citation error.)
+
+**FACT** — The RISC-V extension taxonomy as ratified by RISC-V International separates unprivileged and privileged extensions:
+
+- The unprivileged ISA general-purpose extensions are designated by single capital letters: I (base integer), M (integer multiply/divide), A (atomic), F (single-precision floating-point), D (double-precision floating-point), C (compressed). [Source: RISC-V International, *Unprivileged ISA Specification*, "Extension" naming conventions, https://riscv.org/technical/specifications/.]
+- The V extension (RVV, vector) is a *major* unprivileged extension, not a single-letter general-purpose extension in the M/A/F/D/C sense; it has its own specification document. [Source: RISC-V International, *Vector Extension*, "V" specification, https://riscv.org/technical/specifications/.]
+- B (bitmanip) is not a single extension in the current taxonomy. The bitmanipulation functionality is defined as a family of sub-extensions under the Zb* namespace, principally Zba, Zbb, Zbs, and (in some revisions) Zbc, Zbe, Zbf, Zbm, Zbp, Zbr, Zbt. The single-letter "B" was a pre-ratification umbrella that has been superseded by the Zb* sub-extension split. [Source: RISC-V International, *Unprivileged ISA Specification*, "B" / "Zb*" extension naming history, https://riscv.org/technical/specifications/.]
+- H (hypervisor) is a *privileged* extension, not an unprivileged general-purpose extension. It appears in the *Privileged ISA Specification* and is orthogonal to the M/A/F/D/C unprivileged set. [Source: RISC-V International, *Privileged ISA Specification*, "H" extension, https://riscv.org/technical/specifications/.]
+- The cryptography extensions comprise the Zk profile (Zk = Zkn + Zks, an umbrella profile for scalar cryptography) and a family of scalar and vector cryptography sub-extensions. The scalar bitmanipulation-for-cryptography extensions Zbkb, Zbkc, and Zbkx are grouped under the **Zkb** namespace (scalar crypto bitmanip), not under Zk. Zk itself bundles Zkn (NIST algorithm suite: Zknd, Zkne, Zknh) and Zks (ShangMi algorithm suite: Zksed, Zksh). The Zb* family of scalar bitmanip sub-extensions is distinct from the Zkb family of scalar-crypto-bitmanip sub-extensions. [Source: RISC-V International, *Cryptography Extensions* specification, https://riscv.org/technical/specifications/.]
+
+**ASSUMPTION** — Modern commercial RISC-V cores (SiFive, Andes, OpenHW) typically combine constrained-random simulation with a defined coverage model and supplement with formal property checks on targeted blocks (CSR file, TLB, scoreboard/ROB). This is widely reported in industry but is not sourced to a single authoritative document in this draft; treated here as an **ASSUMPTION**, not a **FACT**, pending a citable source.
+
+**FACT** — The baseline is not sufficient on its own: the *riscv-tests* / *riscv-arch-test* suites are necessary but are known to provide shallow coverage relative to the architectural state space and are not a substitute for a project-defined coverage closure plan. [Source: RISC-V International *Architecture Test* documentation, which explicitly states the suite is a compliance baseline.]
+
+---
+
+## Existing Approaches
+
+**FACT** — The following categories of core-level verification flow are established in the EDA and RISC-V ecosystems:
+
+1. Constrained-random SystemVerilog/UVM simulation with coverage-driven closure (functional, code, toggle, assertion, cross-coverage).
+2. Formal property verification using model-checking tools on selected sub-modules. Correctly categorized tools in this space include: Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal (formerly OneSpin 360 DV; OneSpin was acquired by Synopsys in 2022 and the product is now positioned as part of the Synopsys formal portfolio), and open-source flows such as Yosys + SymbiYosys (SBY). [Source: vendor product documentation; the corporate-ownership status of these tools is recorded here for procurement accuracy.]
+3. FPGA prototyping and emulation acceleration (e.g., Synopsys ZeBu, Cadence Palladium, in-house FPGA boards).
+4. Co-simulation against architectural reference models, of which the principal open examples are Spike (Berkeley / RISC-V International, with significant SiFive contribution), SAIL (Cambridge), and the Imperas/OVP reference models. [Sources: github.com/riscv/riscv-isa-sim (Spike); github.com/rems-project/sail-riscv; github.com/riscv-ovpsim.]
+5. Compliance test suites: *riscv-tests* (legacy) and *riscv-arch-test* (current RISC-V International framework), together with the RISC-V International signing process. [Source: github.com/riscv-arch-test.]
+6. Mutation-based verification tools (e.g., Certitude, proprietary in-house mutation frameworks).
+7. Coverage merging across simulators and prototypes (e.g., Synopsys VCS + ZeBu, Cadence Xcelium + Palladium).
+8. Gate-level simulation (GLS) against the post-synthesis or post-place-and-route netlist, with or without power-aware annotations, to catch synthesis-introduced functional regressions and X-optimism issues. [Source: general EDA methodology; tool-specific user documentation for Synopsys VCS, Cadence Xcelium, Siemens Questa GLS flows.]
+9. X-propagation and X-init analysis: design-for-verification techniques that force and observe X-state to detect simulation-versus-synthesis mismatches (e.g., Synopsys X-Prop, Cadence X-Cell, Siemens Questa X-Prop). [Source: vendor methodology documentation.]
+10. Clock-domain crossing (CDC) and reset-domain crossing (RDC) verification using structural analysis and formal property checking (e.g., Synopsys SpyGlass CDC / RDC, Cadence JasperGold CDC, Siemens Questa CDC). [Source: vendor methodology documentation.]
+
+---
+
+## Alternative Designs
+
+The principal methodology alternatives considered are:
+
+- **A1. Pure simulation-driven sign-off.** Constrained-random UVM with full coverage closure; no formal. Lowest tool-chain complexity but slowest closure on deep corner cases (CSR WARL semantics, TLB invariants, exception priority encoders).
+- **A2. Hybrid simulation + formal (selected).** Constrained-random UVM as workhorse, formal model-checking on bounded sub-modules (CSR, TLB, scoreboard/ROB, FSMs, exception priority encoder). Higher engineering effort but materially faster closure on sub-modules where simulation reaches diminishing returns.
+- **A3. Formal-first, simulation-supplemental.** Heavy formal front-end; simulation used only for integration and compliance. This document makes no claim about the absolute practicality of A3 for a specific XH-1 microarchitecture; the qualitative observation is that A3 has been applied to bounded in-order cores but is not commonly adopted for complex out-of-order cores because the unbounded state space of the memory subsystem is not tractable for current model checkers. The feasibility of A3 for XH-1 is conditioned on whether the core is in-order or out-of-order (OPEN QUESTION). **ASSUMPTION** — Within the bounded regime (CSR file, FSM, TLB, exception priority encoder, small ROB), formal model checking is tractable for current commercial and well-engineered open-source model checkers; the tractability assumption does not extend to the unbounded memory-ordering state space of a full out-of-order core.
+- **A4. Emulation/FPGA-first.** Boots real software (Linux, distro, stress workloads) early. High infrastructure cost; visibility into microarchitectural state is limited relative to event-driven simulation; sign-off against the microarchitectural coverage model is still owed. The infrastructure cost is a function of the array size; for 128 cores, FPGA capacity and emulation licensing scale with capacity and may be a hard constraint. Capacity availability for XH-1 is an **OPEN QUESTION**.
+
+Within the simulation domain:
+
+- **B1. In-house UVM testbench.** Full control, no license cost, but high engineering effort.
+- **B2. Commercial verification IP.** Faster start; recurring license cost; opaque to RTL changes.
+- **B3. Generator-based flows (e.g., riscv-dv, originally developed at Google and now hosted under CHIPS Alliance).** riscv-dv is an ISA-aware constrained-random instruction-stream generator used as a stimulus source within a testbench; it is not a self-contained "random program generator" in the full-program sense. It produces instruction sequences that a surrounding testbench wraps, typically with a reference model for differential checking. [Source: github.com/chipsalliance/riscv-dv.]
+
+Within the formal-tool domain:
+
+- **F1. Commercial model checkers.** Examples: Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal. Higher capacity, commercial support, license cost.
+- **F2. Open-source model checkers.** Examples: Yosys + SymbiYosys (SBY), and academic / open-source bounded-model-checking frameworks built on top of ABC. Lower cost; smaller capacity; smaller ecosystem. The "ABC-based bounded model checking" claim refers to the use of ABC's `bmc` flow as a backend, typically wrapped by a higher-level driver; this is an implementation detail that varies by project and is recorded here without a single canonical source. [Source: https://github.com/YosysHQ/yosys; https://github.com/YosysHQ/sby; ABC project documentation, https://github.com/yosyshq/abc.]
+
+Coverage-model alternatives:
+
+- **C1. Structural only (line/branch/toggle).** Fast to collect; known to miss functional holes.
+- **C2. Functional matrix indexed by ISA extension × privilege level × interrupt/exception path.** Necessary for sign-off; higher collection and debug cost.
+- **C3. Functional + mutation score.** Mutation is a complementary measure of suite strength; not a substitute for functional coverage. Whether mutation is part of the XH-1 sign-off artifact is an **OPEN QUESTION** (see Verification Considerations).
+
+---
+
+## Comparison
+
+**INSUFFICIENT EVIDENCE** for a quantitative comparison. The relative run time, license cost, engineering effort, coverage-closure time, and debug productivity of A1–A4, B1–B3, and F1–F2 depend on the chosen EDA stack, the ISA profile, and the in-house team's existing code base, none of which are captured in the project repository. A numeric trade-off table is not fabricated here. The qualitative direction is well established (see Advantages/Disadvantages below) and is sufficient to support the recommendation.
+
+---
+
+## Advantages
+
+**Hybrid simulation + formal (A2):**
+
+- Formal closes deep corner cases (CSR WARL, TLB invariants, exception priority encoder) faster than simulation, where simulation reaches diminishing returns. (Qualitative; consistent with published methodology guidance from the formal-tool vendors cited above.)
+- Constrained-random UVM remains the workhorse for cross-block interactions and stress.
+- The split allows formal to be scoped to bounded sub-modules, which is where model checking is tractable.
+
+**Generator-based flow (B3, e.g., riscv-dv):**
+
+- Open-source and ISA-aware; reduces hand-written sequence count.
+- Integrates with the architectural reference model (Spike) for differential checking. [Source: github.com/chipsalliance/riscv-dv; github.com/riscv/riscv-isa-sim.]
+
+**Open-source formal (F2):**
+
+- No license cost; can be applied to small bounded sub-modules (single FSMs, small CSR files) without commercial procurement.
+- Useful as a pre-screen or as a fallback for sub-modules where commercial formal capacity is not warranted.
+
+**Compliance framework:**
+
+- riscv-arch-test with the RISC-V International signing process produces a portable, vendor-neutral artifact that downstream software/OS teams can use. [Source: github.com/riscv-arch-test; RISC-V International *Compliance Policy*.]
+
+---
+
+## Disadvantages
+
+**Hybrid simulation + formal (A2):**
+
+- Two tool flows must be integrated, which adds engineering effort and requires a coverage-merging strategy across flows.
+- Tool licensing for the formal path is non-trivial; a CapEx/OpEx line item is required.
+
+**Generator-based flow (B3):**
+
+- riscv-dv is RV32/RV64 ISA-focused; non-ISA RTL (custom accelerators, custom CSRs) is not generated and must be hand-written.
+
+**Compliance framework:**
+
+- The riscv-arch-test suite is shallow; producing a signature on it is necessary but not sufficient for sign-off. Treating it as sufficient is a known failure mode. (This is a usage guideline, not a property of the framework itself.)
+
+**Open-source formal (F2):**
+
+- Lower model-checking capacity than commercial tools; not all sub-modules will close.
+- Smaller ecosystem of commercial support.
+
+**General across alternatives:**
+
+- None of the alternatives in isolation produces a tape-out-ready sign-off artifact; all require an explicit, project-owned coverage-closure plan with numeric exit criteria.
+
+---
+
+## XH-1 Considerations
+
+**ASSUMPTION** — XH-1 is a custom 128-core RISC-V design. Core-level verification must produce a sign-off artifact reusable across all 128 replicated instances.
+
+**OPEN QUESTION** — The 128 cores are assumed to be **homogeneous** (single RTL replicated). Whether this holds, or whether XH-1 includes variants (e.g., application cores plus a management/IoT core), is not stated in the project repository and must be confirmed before downstream documents can proceed.
+
+**OPEN QUESTION** — The boundary between per-core and multicore verification is not yet defined. Candidates:
+
+- Per-core: L1 I-cache, L1 D-cache, MMU/TLB, PMP, CSR, debug transport module, trace encoder, retire/ROB, exception/interrupt controller.
+- Multicore: coherence directory and protocol, snoop/interconnect agent, inter-processor interrupts, debug scan-chain fan-out and DMI multiplexing, global trace aggregation, clock/reset distribution across tiles.
+
+**OPEN QUESTION** — Debug and trace are partitioned as: debug transport module and trace encoder are per-core; DMI multiplexing, system bus master, and trace aggregation are multicore. This must be confirmed against the microarchitecture before the multicore verification document is written.
+
+**OPEN QUESTION** — The RISC-V Debug Specification version that applies to XH-1 is not stated. The current ratified version is 1.0.0; the project's choice between 1.0.0 and any earlier revision (including 0.13, which was a pre-ratification draft) is not captured. Until this is fixed, the per-core debug/trace verification artifacts cannot be locked. The Trace Specification version is similarly unresolved (current ratified version is 2.0.0).
+
+---
+
+## 128-Core Scalability
+
+**PROPOSAL** — Per-core verification collateral (testbench, sequences, assertions, coverage models) is constructed as a **single instance-independent artifact** that is run for each of the 128 replicated cores (or, equivalently, run once with a parameterizable instance handle). **ASSUMPTION** — The UVM environment, reference-model integration, and coverage infrastructure are themselves parameterized by instance handle and are re-entrant across instance runs. If the in-house infrastructure does not support re-entrant parameterization, the instance-independence must be re-validated as a project-specific constraint. Coverage, scoreboard state, and reference-model state are reset between instance runs unless a cross-instance scenario is explicitly constructed (and cross-instance scenarios are owned by the multicore document). This is the same artifact exercised 128 times, not 128 specialized artifacts.
+
+**PROPOSAL** — The formal-tool bound (proof depth, state-space depth, number of register bits) is selected such that the same bound applies to all 128 instances; the bound is not a function of the instance index. The formal collateral is therefore also instance-independent.
+
+**ASSUMPTION** — The 128-core design reuses a single verified core RTL. If the array is heterogeneous, the instance-independence collapses to one per variant, and the per-core effort is multiplied by the number of variants.
+
+**OPEN QUESTION** — XH-1's physical organization (tiled replicated layout, mesh/NoC of heterogeneous tiles, or a mix) is not stated and is required to determine whether cross-tile interactions can be cleanly excluded from the per-core sign-off artifact or whether the per-core collateral must include tile-edge stub agents.
+
+**PROPOSAL** — Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out) are **out of scope** for the per-core document and are owned by the multicore verification document. (This is a PROPOSAL based on the verification-reasoning argument that mixing per-core and multicore concerns produces a fragile, instance-coupled artifact; it is not a "known anti-pattern" in the sense of an externally codified rule.)
+
+**OPEN QUESTION** — How is the riscv-arch-test signing flow extended to 128 instances? The compliance flow is per-core; the project intent (one signature per instance, one signature from a representative instance, or a parameterized signature) is not stated.
+
+**PROPOSAL** — Regression parallelism across 128 instances is achieved by distributing identical per-core runs across the host farm. **ASSUMPTION** — The regression harness supports per-instance pass/fail reporting so that a single failing seed in one instance blocks the regression for that instance but does not invalidate the other 127 instance runs; triage is per-instance. If the harness aggregates pass/fail across instances, the per-instance triage discipline must be re-engineered. Cross-instance coverage merging is performed by aggregating the per-instance coverage databases into a single per-core dashboard.
+
+**OPEN QUESTION** — FPGA prototyping or emulation capacity for 128 cores is not stated. A4 (Emulation/FPGA-first) is feasible only if the platform can host the full array; the alternative is to emulate a single instance plus a representative tile-edge stub, which is a per-core artifact, not a multicore one.
+
+---
+
+## Performance Considerations
+
+**OPEN QUESTION** — Core-level simulation throughput (instructions/second, coverage points/hour) depends on the chosen simulator (commercial event-driven, Verilator, cocotb, or custom), the workload, and the host farm, none of which are fixed. No numeric simulation throughput is fabricated here.
+
+**ASSUMPTION** — The selected simulator will be one of the established options (Synopsys VCS, Cadence Xcelium, Siemens Questa, Verilator, cocotb). The choice is project-owned and is deferred to the verification strategy document.
+
+**OPEN QUESTION** — The trade-off between open-source simulators (Verilator, cocotb) and commercial event-driven simulators at 128-core regression scale is not characterized here. The relevant axes are: per-instance throughput, license cost, UVM support, coverage-tool integration, and debug visibility. A quantitative trade-off depends on the chosen farm size and is not fabricated.
+
+**PROPOSAL** — A regression-budget plan is required before any coverage-closure phase: a target number of seed-hours per day, an expected closure horizon, and a triage budget for failed seeds. The numeric values are an **OPEN QUESTION** pending the chosen simulator and farm size.
+
+---
+
+## Area Considerations
+
+**INSUFFICIENT EVIDENCE** — Verification-influenced area decisions (adding observability or assertion logic, formal-friendly state encodings, scan/DFT hooks) are not characterized for XH-1.
+
+**ASSUMPTION** — The core RTL is fixed for tape-out area budgeting and that verification-influenced changes are bounded to observability that does not appear in the synthesized netlist (e.g., `ifdef` guards). This must be confirmed against the synthesis/scan insertion flow.
+
+**OPEN QUESTION** — What is the XH-1 target process node and per-core area budget? Both are required before area-influenced verification choices (e.g., one-hot vs. binary FSM encoding for formal tractability) can be evaluated.
+
+---
+
+## Power and Energy Considerations
+
+**INSUFFICIENT EVIDENCE** — Per-core power and energy are not characterized for XH-1.
+
+**ASSUMPTION** — Verification-influenced power decisions (e.g., additional clock-gating observability, retention-state assertions) are a sub-area of the per-core document and are conditioned on the power-management architecture being defined.
+
+**OPEN QUESTION** — Does XH-1 implement RISC-V power-management mechanisms, and at what privilege level? The RISC-V mechanisms relevant to this question include:
+
+- WFI (`wait-for-interrupt`) and the WFI-idle semantics defined in the *Privileged ISA Specification*; these are the standardized low-power entry points. [Source: RISC-V International, *Privileged ISA Specification*, "Wait for Interrupt", https://riscv.org/technical/specifications/.]
+- `Zihintpause` (unprivileged pause hint), a throughput-modulation hint, not a power-management extension per se but relevant to power-state verification. [Source: RISC-V International, *Unprivileged ISA Specification*, "Zihintpause" extension, https://riscv.org/technical/specifications/.]
+- Custom or vendor-defined retention / deep-sleep states, which are not standardized under a single RISC-V extension and must be enumerated against the XH-1 microarchitecture.
+
+Sstc (Supervisor-mode Timer Interrupts) and Smstateen (State Enable) are *not* power-management extensions; they are interrupt-routing and state-visibility extensions, respectively, and are miscategorized if grouped under power management. [Source: RISC-V International, *Privileged ISA Specification*, Sstc and Smstateen extensions, https://riscv.org/technical/specifications/.] Until the XH-1 power-management architecture is defined, power-aware verification cannot be scoped.
+
+**OPEN QUESTION** — How is energy-aware DV (e.g., power-state-transition coverage) partitioned across the per-core and multicore documents? An explicit ownership line is required.
+
+---
+
+## Implementation Considerations
+
+**OPEN QUESTION** — XH-1 implements a defined subset of the RISC-V ISA (base integer I, and a selected set of M, A, C, F, D, the major V extension, the Zb* bitmanipulation sub-extensions, the H privileged extension, and cryptography sub-extensions under Zkn, Zks, and Zkb, plus platform extensions). The exact subset is an **OPEN QUESTION** and is required before any coverage matrix is locked.
+
+**OPEN QUESTION** — Is the core in-order or out-of-order? This drives the verification surface:
+
+- In-order: simpler scoreboard, no speculation-recovery paths.
+- Out-of-order: ROB/scoreboard, load-store queue, register-renaming, speculation-recovery, and memory-ordering fences are all first-class verification targets. **ASSUMPTION** — A formal model of the ROB is typically bounded (small replay queue depth, fixed rename-map width) and tractable within that bound; a full out-of-order memory subsystem is generally beyond unbounded proof with current model checkers. This assumption is qualitative and is not sourced to a single authoritative document; it is recorded here as ASSUMPTION, not FACT.
+
+**OPEN QUESTION** — The ROB formal bound (proof depth, replay-queue depth, rename-map width) is project-owned and is not fixed here. The bound is selected to make the model checker tractable while exercising the recovery paths the project considers in-scope for formal closure. The bounded proof covers the in-bound states; the unbounded remainder is covered by simulation. This division of labor is stated as a PROPOSAL, conditional on the in-order/out-of-order answer and on the project's risk posture.
+
+**ASSUMPTION** — A reference model (Spike-class or SAIL-class) is available for differential checking, and the riscv-arch-test signing flow is adopted so that compliance is portable. Both are working assumptions until confirmed.
+
+**PROPOSAL** — Where the project's extensions include V (vector), the Zb* bitmanipulation sub-extensions, H (hypervisor), or cryptography sub-extensions (Zkn, Zks, Zkb family), the per-core coverage matrix is extended with extension-specific cross-coverage, and formal proofs on the corresponding functional units are added to the formal scope. The conditional language here is the binding form: the coverage and formal scopes are conditioned on the confirmed ISA profile.
+
+**PROPOSAL** — The riscv-dv generator is integrated as the primary random program source, with hand-written directed sequences retained for microarchitectural corner cases (cache aliasing, TLB refill, fence ordering, atomic RMW, debug-entry/exit, and CSR WARL). [Source: github.com/chipsalliance/riscv-dv.]
+
+**OPEN QUESTION** — PMP is listed under per-core scope. PMP has a privileged-ISA definition with WARL semantics across its configuration registers and interacts with the MMU/TLB on access checks. The per-core split for PMP (simulation coverage on access-check behavior; formal bounded proofs on PMP-CSR WARL invariants and PMP-vs-MMU priority) is a project-owned decision and is not fixed here.
+
+---
+
+## Cross-Cutting Verification Concerns
+
+The per-core scope must explicitly address or defer with stated reason the following cross-cutting concerns. Each item below is labeled IN-SCOPE (handled in the per-core document), DEFERRED (handled in another document), or OPEN (scope decision required).
+
+- **Gate-level simulation (GLS).** **OPEN.** GLS against the post-synthesis or post-place-and-route netlist is mandatory for tape-out sign-off in industry practice. Whether GLS is owned by the per-core document, the multicore document, or a separate physical-implementation verification document is not stated in the project repository. **ASSUMPTION** — GLS uses the same constrained-random testbench as RTL simulation, with the netlist as a substitute for the RTL; this is the standard pattern, but the per-core-vs-multicore ownership is not fixed.
+
+- **X-propagation and X-init analysis.** **OPEN.** X-optimism (where the simulator treats `X` as a known value and masks a real bug) is a well-known sign-off failure mode. Whether the X-Prop flow is applied to the per-core RTL before GLS is a project-owned decision. **ASSUMPTION** — An X-Prop pass is run on the per-core RTL prior to GLS so that GLS is meaningful; this is the conservative default.
+
+- **Clock-domain crossing (CDC) and reset-domain crossing (RDC).** **OPEN.** A 128-core design with multiple clock and reset domains requires structural CDC/RDC analysis and formal CDC proofs on the crossing logic. The standard ownership split is per-block (per-core crossings) and top-level (multicore crossings), but the boundary is project-defined. **ASSUMPTION** — CDC/RDC for crossings *within* a single core (e.g., debug vs. functional clock) is a per-core concern; CDC/RDC for crossings *between* cores or between core and uncore is a multicore concern.
+
+- **Manufacturing scan / MBIST / LBIST.** **OPEN.** Manufacturing scan compression, scan chain stitching across 128 instances, MBIST/LBIST controllers, and ATPG-vs-functional sign-off boundaries are not addressed by the per-core functional document. Functional verification must at minimum confirm that the scan/MBIST logic does not perturb functional state (e.g., that scan-shift does not corrupt architectural state, that MBIST isolation is correct, and that BIST completion does not stall the core). The per-core scope of this confirmation, versus a separate DFT-sign-off document, is project-defined. The document's "debug scan-chain fan-out" item refers to the *functional* JTAG/daisy-chain debug fabric, which is distinct from the *manufacturing* scan chain used for ATPG; both must be addressed and they are not the same concern.
+
+- **Security verification.** **OPEN.** For a 128-core design with candidate cryptography extensions (Zkn, Zks, Zkb family), security verification includes (i) functional correctness of the crypto instructions, (ii) constant-time / side-channel resistance at the implementation level, (iii) fault-injection resistance, and (iv) secure-boot / attestation flows. Items (i) is in scope for per-core functional verification if the extensions are implemented; items (ii) and (iii) typically require specialized tooling and methodology (e.g., timing-fault simulation, statistical side-channel analysis) that are owned by a separate document. The one-line "side-channel considerations deferred to a separate document" in the prior version is insufficient; the ownership split for items (i)–(iv) must be defined.
+
+- **FP corner cases (F/D extension).** **OPEN.** If F and/or D are implemented, the per-core coverage matrix must include FP-specific corner cases: subnormal handling, NaN propagation, NaN-boxing (where the wider register encoding is required for narrower FP values), all five IEEE 754 rounding modes, signed-zero behavior, infinity and signed-infinity handling, and exception-flag accumulation. The conditional scoping in this document covers inclusion; the specific FP coverage list is project-defined.
+
+- **V (vector) extension coverage.** **OPEN.** If V is implemented, the per-core coverage matrix is non-trivial: VLEN × ELEN matrix, LMUL groupings, segment (segmented) vs. strided vs. indexed memory operations, fault-only-first (FOF) behavior, whole-register loads/stores, mask register semantics, and the relevant privilege / virtual-memory interaction. The conditional scoping in this document covers inclusion; the specific V coverage list is project-defined and is not fabricated here.
+
+---
+
+## Verification Considerations
+
+**PROPOSAL** — A coverage closure plan is defined before any RTL is signed off. Exit criteria are stated in terms of:
+
+- **Functional coverage.** Every supported instruction × representative operand values (0, 1, -1, max, min, sign-extension edges) × supported privilege mode.
+- **Exception/interrupt coverage.** Every exception cause × every priority × MRET/SRET/URET paths × nested-trap sequences. [Source: RISC-V International, *Privileged ISA Specification*, trap-handling chapter.]
+- **CSR coverage.** Every implemented CSR × every writable bit × reset value × WARL semantics. Formal proof of WARL invariants is a sub-goal.
+- **Memory access coverage.** Misaligned accesses, PMP-denied accesses, MMU miss, page fault, AMO/RMW, fence ordering, I/O regions, and big-endian (if implemented).
+- **Reset and debug.** Every reset reason (power-on, warm, retention, debug) and every debug state transition in the RISC-V Debug Specification version confirmed for XH-1.
+- **Formal.** Targeted bounded proofs on bounded sub-modules: CSR file WARL invariants, TLB invariants, exception priority encoder, retire/ROB, debug-transport FSM, trace-encoder FSM. The bound for each sub-module is project-owned (see Implementation Considerations).
+
+**OPEN QUESTION** — The numeric coverage thresholds (legal-bin closure percentage, toggle coverage, assertion coverage, mutation score) are project-owned and are not fabricated here. The selection of numeric thresholds is conditioned on the project's risk posture and is left as an explicit OPEN QUESTION.
+
+**OPEN QUESTION** — Mutation / fault-injection (alternative C3) is a complementary measure of suite strength. Whether it is in or out of the XH-1 sign-off artifact is not decided in this document. Options: (i) include mutation score as an explicit exit criterion; (ii) use mutation as a development-time diagnostic without a numeric exit criterion; (iii) exclude mutation entirely. The decision is deferred to the verification strategy document.
+
+**PROPOSAL** — Extension-specific items in the coverage list are conditioned on the confirmed ISA profile:
+
+- F/D coverage (including NaN-boxing, subnormal handling, rounding modes) is included only if the F/D extension is implemented.
+- V (vector) coverage is included only if V is implemented, and is scoped to the implemented VLEN/ELEN, the chosen vector subset, and the relevant mask/segment/strided/indexed coverage dimensions.
+- Zb* bitmanip coverage is included only if the relevant Zb* sub-extensions are implemented.
+- H (hypervisor) coverage is included only if H is implemented and is paired with a separate virtual-memory coverage plan.
+- Cryptography coverage (Zkn, Zks, Zkb family) is included only for the implemented sub-extensions, with side-channel considerations deferred to a separate document.
+
+This conditional scoping is the binding form: the coverage list is fixed at the granularity of *conditioned on the confirmed ISA profile*.
+
+**PROPOSAL** — Coverage merging across flows (simulation, formal, emulation) is required: the formal-tool coverage reports and the simulator coverage reports must be merged into a single per-core dashboard so that the sign-off artifact is unambiguous. At 128-instance scale, the merge is performed per-instance and then aggregated.
+
+**OPEN QUESTION** — Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit) consumes the artifacts produced at the core level? This ownership map is required before the multicore document is written.
+
+---
+
+## Software Considerations
+
+**PROPOSAL** — The per-core verification artifacts are aligned with the downstream software flow:
+
+- The riscv-arch-test signature is producible from the verified core and is delivered alongside the reference manual. At 128-instance scale, the signature-generation step is repeated per instance (or per representative instance, per the project-owned decision; see 128-Core Scalability).
+- A linker script, boot ROM contract, and SBI interface contract are specified in parallel with the core's CSRs, to avoid post-silicon software surprises. [Source: RISC-V International, *SBI Specification*.]
+- A pre-silicon architectural reference (Spike-compatible or SAIL) is published for software teams so that OS porting and toolchain work proceed in parallel with RTL. The specific version of Spike or SAIL is pinned to a commit or release tag as part of the verification strategy document; this document does not commit to a version.
+
+**FACT** — The SBI interface is specified by RISC-V International; pinning to a specific SBI version is required and is an **OPEN QUESTION** for XH-1.
+
+---
+
+## Recommendation
+
+The recommendation below states the binding methodological choices and is conditional on the homogeneous-128-core assumption and on the ISA profile being captured before the multicore document is written. Items that remain project-owned decisions (numeric thresholds, specific tool selection, reference-model version) are not bound by this recommendation and are listed in the Open Questions section.
+
+**RECOMMENDATION** — Adopt the hybrid simulation + formal methodology (A2) for per-core verification, with the following binding choices:
+
+1. **Simulation workhorse.** Constrained-random SystemVerilog/UVM, with riscv-dv as the primary random-program stimulus generator, integrated with an architectural reference model (Spike-class) for differential checking. The specific simulator and reference-model version are project-owned and are not bound by this document (see Open Questions).
+2. **Formal scope.** Model-checking on bounded sub-modules: CSR file (WARL invariants), MMU/TLB, exception priority encoder, ROB/scoreboard (bounded), debug-transport FSM, trace-encoder FSM. Candidate tool categories are commercial model checkers (e.g., Siemens EDA JasperGold, Synopsys VC Formal, Synopsys 360 DV-Formal) and, for small bounded sub-modules, open-source model checkers (e.g., Yosys + SymbiYosys). Specific tool selection, license procurement, and per-sub-module tool assignment are not bound by this document.
+3. **Compliance.** riscv-arch-test signature generation is part of the sign-off artifact. At 128-instance scale, the per-instance signature-generation policy is an **OPEN QUESTION** (see 128-Core Scalability).
+4. **Coverage model.** Functional matrix indexed by ISA extension × privilege level × interrupt/exception path, with extension-specific items conditioned on the confirmed ISA profile.
+5. **Collateral reuse.** Per-core verification collateral is constructed as a single instance-independent artifact reused across all 128 instances, subject to the ASSUMPTION that the UVM/reference-model/coverage infrastructure supports parameterizable instance handles. Cross-instance scenarios are owned by the multicore verification document.
+6. **Ownership.** Cross-core interactions (coherence, inter-processor interrupts, debug scan-chain fan-out, trace aggregation) are owned by the multicore verification document.
+7. **Cross-cutting concerns.** The per-core document's scope over GLS, X-Prop, CDC/RDC, manufacturing scan/MBIST interaction, and security verification is an **OPEN QUESTION** and is enumerated in the Cross-Cutting Verification Concerns section. These items are not bound by this recommendation and require an explicit ownership decision before tape-out planning.
+
+The numeric coverage thresholds, the choice of simulator and formal tool, the specific reference-model version, and the coverage-closure horizon are **OPEN QUESTIONS** and are deferred to the verification strategy document and the project's sign-off policy.
+
+---
+
+## Confidence
+
+Medium. The methodology recommendation follows from established industry practice and the cited RISC-V specifications; the recommendation does not depend on the unresolved numeric thresholds. Confidence would be upgraded to High once the **OPEN QUESTIONS** below are closed.
+
+---
+
+## Open Questions
+
+- What RISC-V base and extensions does XH-1 implement (RV32/RV64, I/M/A/F/D/C, the major V extension, the Zb* bitmanipulation sub-extensions, the H privileged extension, the cryptography sub-extensions under Zkn/Zks/Zkb, supported privilege modes, hypervisor)?
+- Is the core in-order or out-of-order?
+- Is the 128-core array homogeneous, or are there variants (application cores plus a management/IoT core)?
+- What is the XH-1 target process node, per-core area budget, clock frequency, and tape-out schedule?
+- What simulator and formal-tool stack is available or mandated (commercial, Verilator, cocotb, Yosys + SymbiYosys, custom)?
+- What is the project's stance on the RISC-V International compliance signing process, and at what SBI version is the platform pinned?
+- What numeric coverage exit criteria (legal-bin percentage, toggle, assertion, mutation score) does the project accept for tape-out, and is mutation in or out of the sign-off artifact?
+- Which RISC-V Debug Specification version (0.13 or 1.0.0) and which Trace Specification version (2.0.0 or other) apply to XH-1?
+- Which verification sub-area (formal, fault injection, ISA compliance, multicore, regression, strategy, unit, DFT) consumes the artifacts produced at the core level?
+- Does XH-1 implement RISC-V power-management mechanisms (WFI, custom retention states, Zihintpause), and how is energy-aware DV partitioned across the per-core and multicore documents?
+- Is FPGA prototyping or emulation capacity available at the scale required to boot 128 cores?
+- What is the per-instance riscv-arch-test signature policy (one per instance, one per representative instance, parameterized)?
+- What are the formal proof bounds (depth, state-space width) for the ROB and other bounded sub-modules?
+- What is the ownership boundary for GLS, X-Prop, CDC/RDC, and manufacturing scan/MBIST verification: per-core, multicore, or a separate physical-implementation verification document?
+- What is the per-core ownership share of security verification (functional crypto correctness, side-channel resistance, fault-injection resistance, secure-boot)?
+
+---
+
+## Sources
+
+- RISC-V International, *Unprivileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Privileged ISA Specification* (latest ratified). https://riscv.org/technical/specifications/
+- RISC-V International, *Debug Specification*, version 1.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Trace Specification*, version 2.0.0. https://riscv.org/technical/specifications/
+- RISC-V International, *Vector Extension ("V") Specification*. https://riscv.org/technical/specifications/
+- RISC-V International, *Cryptography Extensions* (Zkn, Zks, Zkb sub-extensions; Zk profile). https://riscv.org/technical/specifications/
+- RISC-V International, *SBI Specification*. https://riscv.org/technical/specifications/
+- RISC-V International, *Compliance Policy* and *Architecture Test* framework. https://github.com/riscv-arch-test
+- OpenHW Group, *CV32E40P Core Documentation*. https://github.com/openhwgroup/core-cv32e40p
+- OpenHW Group, *CV32E40PX Core Documentation*. https://github.com/openhwgroup/core-cv32e40px
+- CHIPS Alliance / Google, *riscv-dv* (ISA-aware constrained-random instruction-stream generator). https://github.com/chipsalliance/riscv-dv
+- Berkeley / RISC-V International (with SiFive contribution), *Spike* (riscv-isa-sim). https://github.com/riscv/riscv-isa-sim (no specific version pinned in this document; pinning is deferred to the verification strategy document.)
+- Cambridge, *SAIL RISC-V* (architectural reference model). https://github.com/rems-project/sail-riscv
+- Imperas, *riscvOVPsim* (commercial reference model). https://github.com/riscv-ovpsim
+- Siemens EDA, *JasperGold* formal verification platform (product documentation). https://eda.sw.siemens.com/en-US/ic/jaspergold/
+- Synopsys, *VC Formal* (product documentation). https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html
+- Synopsys, *360 DV-Formal* (formerly OneSpin 360 DV; OneSpin acquired by Synopsys in 2022). https://www.synopsys.com/verification/static-and-formal-verification/360-dv-formal.html
+- Synopsys, *SpyGlass CDC / RDC* (clock- and reset-domain crossing structural and formal analysis). https://www.synopsys.com/verification/static-and-formal-verification/spyglass.html
+- Cadence, *JasperGold CDC* (clock-domain crossing formal verification). https://www.cadence.com/en_US/home/tools/digital-design-and-signoff/silicon-signoff/jasper-gold-cdc.html
+- Siemens EDA, *Questa CDC* (clock-domain crossing analysis). https://eda.sw.siemens.com/en-US/ic/questa/
+- Synopsys, *X-Prop* (X-propagation analysis). https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html
+- YosysHQ, *Yosys* (open-source synthesis and formal-verification framework). https://github.com/YosysHQ/yosys
+- YosysHQ, *SymbiYosys (SBY)* (open-source formal verification front-end). https://github.com/YosysHQ/sby
+- YosysHQ / ABC project, *ABC* (logic synthesis and bounded model checking). https://github.com/YosysHQ/abc
+
+`INSUFFICIENT EVIDENCE` is recorded above in the Performance, Area, Power and Energy, and Comparison sections pending the project inputs that close the corresponding **OPEN QUESTIONS**. No numeric claim in any of those sections has been fabricated.