From 4b3553faa7dfeb2603d717904a2c1fbf79f168f9 Mon Sep 17 00:00:00 2001 From: maksyuki Date: Mon, 19 Oct 2026 13:53:32 +0800 Subject: [PATCH] docs(spi): record SPI-P1 validation and review closure Document the standalone interfaces, timing checker, FIFO pressure cases, tool-component identity and exact execution commands. Update subsystem guides and the verification ledger with the matching ICS55/IHP130 evidence. Keep historical failures and producer identities separate from the new results. Record the optional PDF-test skip, unconstrained IO boundaries, deferred full-product regressions and the human phase-acceptance gate. Validation: 21 local links and the documentation-only post-test delta checked; git diff --check passed. No generated evidence is committed. --- docs/ip/spi-p1.md | 285 ++++++++++++++++++++++++++++++++++++ docs/ip/spi-verification.md | 156 +++++++++++++++++++- rtl/ip/README.md | 3 + scripts/README.md | 6 + tests/README.md | 13 ++ 5 files changed, 460 insertions(+), 3 deletions(-) create mode 100644 docs/ip/spi-p1.md diff --git a/docs/ip/spi-p1.md b/docs/ip/spi-p1.md new file mode 100644 index 00000000..71d73470 --- /dev/null +++ b/docs/ip/spi-p1.md @@ -0,0 +1,285 @@ +# SPI-P1 Standalone Core + +This implementation follows [SPI APB 1.0](spi.md) from +`dev@e62ccdad87e1fd412eff70cc2527ad3090f16a55`. It is a standalone block; +Tiny and Mini product filelists, address/IRQ/RCU routing, GPIO, DMA and SDK +runtime interfaces are unchanged. DMA capability is zero. Qualification and +phase acceptance belong to the [ledger](spi-verification.md). + +The 2026-10-19 review-closure change affects test/evidence sources only. It +adds independent PCLK-counted waveform checks, complete-core FIFO pressure +cases and tool-input schema 2. Production RTL, profiles, ABI and dependencies +remain byte-identical to the reviewed implementation. The final campaign uses +`BUILD_TIMESTAMP=2026-10-19-07-00`; all planned gates passed below the new +ICS55/IHP130 variants, including one full Pytest run (2085 passed, one optional +PDF-test skip). The ledger records the measured results and remaining gates. + +## Structure and interfaces + +```mermaid +flowchart LR + APB[APB4 and private origin] --> REG[spi_reg] + REG --> CORE[spi_master_core] + GPIO[Read-only GPIO state] --> GUARD[spi_gpio_guard] + GUARD --> CORE + CORE --> PACK[spi_word_packer: TX/RX 8x32] + CORE --> PHASE[spi_phase_ctrl] + PACK --> PHASE + PHASE --> PINS[SCK MOSI CS and raw MISO] +``` + +All state uses PCLK and Common registers. The two Common FIFOs have explicit +pre-edge push/pop qualification: full plus pop does not authorize a push. +Payload arrays are not reset; validity and packing state hide stale data. +The APB response is registered, and each access performs its side effect once. +Full/empty FIFO and invalid source accesses error without waiting for SCK. + +The private origin encoding is CPU=0, central DMA=1, other=2/3. Request and +channel qualification, per-direction reserved credit, credit retirement, +complete job/response status and pending START are external integration inputs. +They must remain attached to the admitted request. A credit commit is a FIFO +event, not terminal AXI retirement. The wrapper rejects reuse until retirement. +P1 test environments provide those inputs; no DMA allocator, TCD lifecycle, +fabric origin capture or CDC path is implemented here. PPROT is not an origin. + +The GPIO guard receives USER_SELECT, handoff, ALT selection, software OE, +open-drain and readiness. It checks prospective and retained session pins, +permits mutable D/C level, and disables only SPI's own OE on route loss. +Actual GPIO/RCU gating veto and software handback are P3 obligations. + +```mermaid +stateDiagram-v2 + DISABLED --> GAP: ENABLE + GAP --> IDLE: inactive delay + IDLE --> ARMED: ARM + HELD --> ARMED: ARM after complete cleanup + ARMED --> SETUP: START + SETUP --> SHIFT: setup delay + SHIFT --> HOLD: final trailing edge + HOLD --> HELD: HOLD_CS + HOLD --> GAP: release CS + HELD --> GAP: END after complete cleanup + IDLE --> DISABLED: DISABLE, keep reservation + SHIFT --> CLOSING: ABORT or fault + CLOSING --> DISABLED: drained RECOVER, keep reservation +``` + +ABORT applies to every acquired state, not only SHIFT. It does not count a +partial frame or report successful completion. Emergency guard loss permits +truncation; RECOVER disables monitoring before DISABLED handback even if the +external guard remains invalid. RELEASE alone relinquishes the reservation. +Wire completion and pending RX/transport cleanup remain separate conditions. + +## Validation entrypoints + +Activate `.cache/retrosoc/development/tiny-r2-p1/activate.sh`, choose one fresh +`BUILD_TIMESTAMP` and an explicit Tiny profile/PDK. The new targets are +`spi-p1-lint`, `spi-p1-rtl`, `spi-p1-formal`, `spi-p1-synth`, +`spi-p1-netsim`, `spi-p1-sta` and `spi-p1-report`. +`SIMU=VERILATOR` or `SIMU=IVERILOG` selects standalone behavioral execution. +Both backends use balanced mapping and PCLK SAFE24. Existing attempt roots +are never overwritten. A changed source requires a new timestamp. + +For example, after approval: + +```sh +make CONFIG=configs/ci/ics55-tiny.mk SOC=TINY PDK=ICS55 HAVE_SVA=YES \ + JOBS=4 spi-p1-lint spi-p1-rtl +``` + +All simulation commands require zero exit, exactly one fixture-specific +`SPI_P1_PASS` marker and no forbidden failure marker. The independent pin +model observes SCK/CS/MOSI and supplies deterministic MISO data without +accessing DUT internals. Unit markers do not replace Tiny TEST_STATUS for +future integrated firmware. The full product's long Icarus regression remains +deferred under the existing maintainer decision; P10 remains pending closure. + +The pin oracle counts half-periods in PCLK cycles, checks CPHA=0 first-bit +setup, complete final trailing edges and CS setup/hold/inactive intervals, +and permits stretching only between complete frames at CPOL. Normal ABORT +does not disable the checker: only the remaining trailing edge is allowed. +The synthetic checker fixture includes 16 valid mode/width/order cases, one +valid partial-frame abort, and eleven rejected traces (short/long half-period, +setup, frame termination, hold/inactive, post-abort edge, pause polarity and +payload errors). Each rejected trace must produce exactly its expected fault +mask. DUT fixtures fail on any nonzero mask; no general failure-marker waiver +is introduced for expected-negative tests. + +Results and immutable attempts are below the selected variant's +`meta/spi-p1//`, including sources, model/netlist, tools' logs and JSON +results. The original campaign completed on 2026-10-19 with 2068 passed / +1 optional PDF-test skip. That historical result predates the review fixes; +the ledger separates it from the new campaign. +Human phase acceptance remains pending. No qualified frequency, PDF +publication, commit or push is implied. + +The block SDC defines only PCLK. MISO/serial Pad/board round-trip timing is +uncharacterized; no blanket reset or MISO false path suppresses that gap. +Negative setup/hold and unconstrained boundaries remain observational records, +not a completed product timing analysis. Final combined qualification must +use the actual SPI/PIO-lite/PPALite-inclusive Tiny design. + +## Coverage and formal boundaries + +The core fixture exercises all 48 mode/width/order/direction combinations, +DIV=65535, and 256 additional segments using seed `0x53504931`, including +non-default RX-only dummy values. Pin decoding is independent of the DUT. +The APB fixture covers the frozen constant map, invalid accesses, 64-bit +round-up rejection in both widths, maximum legal quotas, full/empty FIFO, +watermark versus sticky IRQ behavior and source-qualified credit retirement. +The lifecycle fixture checks ABORT in all eight acquired states, additional +mid-frame abort offsets, held-CS width changes, maximum CS delays, asynchronous +reset, retained ownership and persistent GPIO faults during closing/recovery. +The packer fixture checks pre-edge full/empty behavior, including simultaneous +push/pop. The mapped-netlist fixture repeats the 48 pin cases and focused +APB rejection/abort/recover/release checks with actual standard-cell models. + +Both RTL simulators and both mapped netlists now execute 48 complete-core +pressure cases: modes0..3 x widths8/16 x both orders x three directions. +Counts37/19 require ten words and include a partial final transport word. +TX service starts with one word, deliberately waits at the next word boundary, +then replenishes the remaining words. RX service is withheld until eight +words fill the FIFO, then interleaved with deterministic 23..25-cycle delays. +Each observed wait is held for at least31 PCLKs; pins/edge count remain stable +at CPOL with CS active, and the corresponding stall counter must advance. +The pin and packed-data oracles check all resumed frames, quotas and tails. +Sixteen additional cases abort under TX starvation or RX-full pressure, and +112 cases sweep14 abort offsets at DIV7 across all modes and widths. Abort +checks retain the frozen `2*DIV + CS_HOLD + CS_INACTIVE + 2` bound and verify +event/frame accounting and retained session ownership after recovery. + +Output enable is independent of retained session ownership. ABORT from a +disabled-but-owned session cannot re-enable pins. A guard loss latches the +clamp until explicit recovery; restoring routing does not restore SPI OE. +Reserved or consumed credits remain transport-busy until retirement, and +registered FIFO responses remain pending through APB completion. The current +CPU control access is excluded from the transport-idle predicate. + +Formal evidence is compositional. The phase engine and register shell have +separate 32-step induction tasks. The session-core BMC retains the 192-step +bound, symbolic commands, legal register-update boundaries, independent +transport/readiness/fault inputs and accepted FIFO service. It uses DIV1..4, +CS delays1..3 and frame counts0..5; full numerical boundary cases are directed +simulations. It does not model DMA V2.2 allocation, descriptor execution, +Tiny source capture, CDC or physical MISO timing. +The independent phase-engine proof also limits DIV to 1..4; DIV65535 is +checked by both directed simulators, not claimed as an exhaustive formal range. + +The 320-step cover task must reach serial activity, completion and closing, +and produce a witness spanning the complete 192-cycle BMC window. The BMC +uses `--nopresat`: this explicit long witness checks satisfiable assumptions +without repeating that query before every assertion query. Conversion uses +`sv2v -E Assert`; model-level assertion/cover counts and witness length are +checked, so a successful empty proof cannot qualify. Full arbitrary-APB +monolithic BMC experiments that timed out remain separate historical attempts, +not complete-system proofs or waived current checks. + +The BMC task has a 1200-second execution allowance: the original 600-second +attempts reached approximately step178 without a counterexample and timed out. +The bound remains 192 and all properties remain enabled. Induction and cover +tasks retain 600 seconds. This execution-budget adjustment does not change +the frozen hardware contract, proof assumptions or global quality policy. + +The deep cover disables optional VCD export (`vcd off`) and retains the +Yosys witness, SMT constraints and Verilog testbench. The 23:25 cover reached +all goals, including step194, but timed out exporting its VCD; that attempt +is not a passed cover. `SPI_P1_FORMAL_REUSE_ROOT` can identify an earlier +formal stage for reuse of successful induction/BMC subtasks only. Reuse +requires identical regenerated and actually consumed models, equivalent SBY +configuration (only the model path is normalized), unchanged proof inputs +and tools, intact original artifacts, a successful command/status and active +properties. Original producer identities, commands and timestamps are retained. +Failure of any check stops reuse; the cover task always executes afresh. + +Tool-input schema2 additionally hashes actual `yosys-smtbmc`/`yosys-abc`, +the installed Yosys bin/data tree, SBY Python modules, SMT/witness helpers and +the Python interpreter/venv configuration. Missing components, mixed Yosys +installations and script-directory module shadowing fail closed. Formal +invocations select absolute SBY/Yosys/SMTBMC/ABC paths and clear user +PYTHONPATH/site overrides. Python bytecode caches are not proof inputs. +Revalidation compares the full inventory as well as individual hashes, so +added/removed files cannot evade detection. Original schema-less records +remain historical and cannot be reused under the stronger rule. The new +campaign therefore executes one fresh induction/BMC/cover sequence, shared +only as cell-free evidence by the IHP130 report. + +For the original recorded campaign, use `BUILD_TIMESTAMP=2026-10-18-23-58`, +`HAVE_SVA=YES` and `JOBS=4` with explicit TINY/PDK selection. The common logic +evidence is under the ICS55 variant. IHP130 report assembly supplies +`SPI_P1_COMMON_ROOT=build/ics55-tiny-2026-10-18-23-58-bbe722dc382e`; only +cell-free RTL/formal evidence is shared. Each PDK has its own synthesized +netlist, mapped simulation, Liberty inputs and STA reports. + +The exact invocation records and quality/JUnit results are retained under +the ICS55 variant's `meta/spi-p1/validation/`. Product firmware compilation +is compatibility evidence only; the SPI core is absent from product filelists. +The firmware, protocol and evidence-tool checks run before one full Pytest +execution. Repeated successful P7/VGA full-system simulations are not part +of this campaign. + +Original standalone commands (historical; these roots must not be overwritten): + +```sh +source .cache/retrosoc/development/tiny-r2-p1/activate.sh +make CONFIG=configs/ci/ics55-tiny.mk SOC=TINY PDK=ICS55 HAVE_SVA=YES \ + SIMU=VERILATOR SYNTH=YOSYS STA=OPENSTA JOBS=4 BUILD_TIMESTAMP=2026-10-18-23-58 \ + SPI_P1_FORMAL_REUSE_ROOT=build/ics55-tiny-2026-10-18-23-25-bbe722dc382e/meta/spi-p1/formal \ + spi-p1-lint spi-p1-rtl spi-p1-formal spi-p1-synth spi-p1-netsim spi-p1-sta +make CONFIG=configs/ci/ics55-tiny.mk SOC=TINY PDK=ICS55 HAVE_SVA=YES \ + SIMU=IVERILOG SYNTH=YOSYS STA=OPENSTA JOBS=4 BUILD_TIMESTAMP=2026-10-18-23-58 spi-p1-rtl +make CONFIG=configs/ci/ihp130-tiny.mk SOC=TINY PDK=IHP130 HAVE_SVA=YES \ + SIMU=IVERILOG SYNTH=YOSYS STA=OPENSTA JOBS=4 BUILD_TIMESTAMP=2026-10-18-23-58 \ + spi-p1-synth spi-p1-netsim spi-p1-sta +make CONFIG=configs/ci/ics55-tiny.mk SOC=TINY PDK=ICS55 HAVE_SVA=YES \ + SIMU=VERILATOR SYNTH=YOSYS STA=OPENSTA JOBS=4 BUILD_TIMESTAMP=2026-10-18-23-58 spi-p1-report +make CONFIG=configs/ci/ihp130-tiny.mk SOC=TINY PDK=IHP130 HAVE_SVA=YES \ + SIMU=IVERILOG SYNTH=YOSYS STA=OPENSTA JOBS=4 BUILD_TIMESTAMP=2026-10-18-23-58 \ + SPI_P1_COMMON_ROOT=build/ics55-tiny-2026-10-18-23-58-bbe722dc382e spi-p1-report +``` + +Compatibility firmware builds used `BUILD_TIMESTAMP=2026-10-18-23-25`, +`JOBS=4`, explicit `SOC`/`PDK` and `firmware`, respectively with +`configs/ci/ics55-tiny.mk` (TINY/ICS55), `configs/ci/ihp130-tiny.mk` +(TINY/IHP130), and `configs/ci/ihp130.mk` (MINI/IHP130). Their original +commands, source snapshots and results remain in the 23:25 ICS55 SPI +`validation/` directory; later changes affect standalone orchestration and +tests, not firmware inputs. No firmware simulation is claimed. + +Quality commands include `make CONFIG=configs/ci/ics55-tiny.mk SOC=TINY +PDK=ICS55 JOBS=4 format-check rtl-style-check-all rtl-readiness-check-all +sw-policy-check sw-host-test`, `ruff check .`, a standalone C11 header +compile, `git diff --check`, and PR/nightly dry-runs with explicit +TINY/ICS55, TINY/IHP130 and MINI/IHP130 selectors. Full Pytest uses +`python3 -m pytest -q --basetemp /pytest-all-tests +--junitxml /pytest-all.xml`; exact expanded commands and results +are retained under `validation/`. No new MISRA deviation is required for the +constant-only header; automated checks are not complete MISRA certification. + +The full Pytest run held all Git-owned source bytes stable. The final ledger +and this runbook were updated afterward to record the result; that documentation +delta is separate from the immutable test snapshot. Parallel Make invocations +can refresh the parent variant manifest's simulator selector. Per-stage +command/result logs and fixture names identify the simulator actually executed; +the parent manifest supplies the unchanged hardware profile, not a substitute +for those execution records. + +For the review-closure campaign, keep the same explicit profile/PDK, +`HAVE_SVA=YES`, simulator/backend and job selections, replace the timestamp +with `2026-10-19-07-00`, and leave `SPI_P1_FORMAL_REUSE_ROOT` empty. +IHP130 report assembly uses +`SPI_P1_COMMON_ROOT=build/ics55-tiny-2026-10-19-07-00-bbe722dc382e`. +Run the pure tool/parity tests and checker selftest first, then quality checks, +the two RTL simulators, fresh formal and separate block backends. Run one full +Pytest after these pass; retain exact commands and source snapshots in the +new ICS55 variant's `meta/spi-p1/validation/`. Firmware inputs did not change, +so existing firmware results retain their original producer identity. + +The retained campaign driver is +`build/ics55-tiny-2026-10-19-07-00-bbe722dc382e/meta/spi-p1/validation/run.py`. +It records exact expanded commands and source maps for `quick`, `rtl`, +`formal`, `backend-ics55`, `backend-ihp130`, `report` and `full`; completed +attempts reject overwriting. `audit.py` verifies the current-source records, +both PDK artifacts, all fixture case counts, fresh formal provenance and the +eight-file repair boundary. `docs-audit.json` records the two documentation +updates after full Pytest. These files are generated campaign evidence, not +project documentation or a new product build interface. diff --git a/docs/ip/spi-verification.md b/docs/ip/spi-verification.md index a13be4ea..af82a4e6 100644 --- a/docs/ip/spi-verification.md +++ b/docs/ip/spi-verification.md @@ -6,6 +6,155 @@ not existing hardware capability. At freeze, SPI RTL, DMA V2.2, native routing, HAL/display software and physical qualification are not delivered. Historical Tiny, SPI-SD, XPI, DMA and PIO evidence does not automatically cover this IP. +## SPI-P1 review-closure checkpoint (2026-10-19) + +The approved eight-file repair closes two missing verification obligations +(independent SCK timing and complete-core FIFO stall/resume) and strengthens +tool-component provenance. It does not modify production RTL, profiles, +register ABI, product integration or dependency versions. The existing +implementation remains based on `dev@e62ccdad87e1fd412eff70cc2527ad3090f16a55`. +See the [runbook](spi-p1.md) for the exact workload and checker contracts. + +The new campaign completed successfully. Matching evidence roots are: + +- `build/ics55-tiny-2026-10-19-07-00-bbe722dc382e/meta/spi-p1/`. +- `build/ihp130-tiny-2026-10-19-07-00-439583e27401/meta/spi-p1/`. + +Tool-input schema2 rejects older incomplete inventories rather than filling +them retrospectively. The fresh formal campaign retains depth192 BMC and +the complete-window cover witness; unchanged proof depth does not cover the +new large FIFO-pressure workloads, which are checked by RTL/netlist fixtures. +Original evidence below remains historical, including the old full-Pytest +count. No human SPI-P1 acceptance, P2 implementation or product qualification +is implied. Final combined-regression/physical obligations remain open. + +| Review-closure gate | Result / evidence boundary | +| --- | --- | +| Independent checker | Both simulators pass 28 synthetic traces: 17 legal cases and 11 exactly classified waveform/payload violations | +| Complete-core behavior | Both simulators pass all five fixtures; each core run retains 305 original segments plus 48 pressure completions, 16 pressure aborts and 112 phase-offset aborts | +| Mapped behavior | Both PDK netlists pass 48 original pin cases plus the same 48 pressure completions, 16 pressure aborts and 112 phase-offset aborts | +| Inventory/parity negatives | 44 pure tests pass; the focused run also includes both checker fixtures (46 passed, 8 deselected) | +| Formal, fresh execution | Phase/register induction pass; depth192 BMC passes in 769.397 s; cover passes in 193.824 s with 195 witness steps; no historical proof reuse | +| Quality / regression definitions | Ruff, formatting, owned RTL style/readiness and whitespace pass; TINY/ICS55 and TINY/IHP130 PR/nightly dry-runs pass | +| Full Pytest, one execution | 2085 passed, 1 skipped in 4980.22 s; the optional PDF retrieval test still lacks `pypdf` | +| Final integrity audit | All stage records match current implementation hashes and schema2 tool inventories; exactly the approved eight paths differ from the repair-start snapshot | + +Each RTL/netlist pressure campaign records 80 observed waits, with stable +CPOL/CS/edge counts and advancing stall counters. The standalone core runtime +is 0.996 s in Verilator and 18.812 s in Icarus (excluding compilation). These +host runtimes are not hardware performance measurements. + +Fresh mapping remains 7431 cells / Liberty area 19240.76 for ICS55 and 7949 / +126612.7254 for IHP130, with two 256-bit payload FIFOs and zero block SRAM +macros. Both STA executions report internal setup/hold WNS/TNS 0.00 and retain +319 missing input delays, 41 missing output delays and 42 unconstrained +endpoints. These are the same observational timing limitations, not closure. + +Exact commands, stdout/result JSON, before/after source maps, JUnit and +`final-audit.json` are in the new ICS55 root's `validation/`. All test-run +source snapshots were stable; only this ledger and the runbook were updated +after full Pytest to record final results. Producer records are immutable. +The repair-start source map is retained under +`build/ics55-tiny-2026-10-19-06-48-bbe722dc382e/meta/spi-p1/validation/start-source.json`. + +No firmware build was repeated: firmware inputs, product profiles and +interfaces are unchanged, and their original 23:25 results remain historical +compatibility evidence. Full product regressions, long firmware Icarus, +commercial/physical/Pad/board/silicon qualification remain unrun/deferred as +previously authorized. No warning baseline, metric policy, MISRA deviation, +dependency version, Git index or branch was changed. Independent read-only +review and explicit human acceptance remain required; readiness is still +`prototype` and all phase-acceptance flags remain false. + +## SPI-P1 implementation checkpoint (2026-10-18, historical) + +The approved standalone implementation starts from clean +`dev@e62ccdad87e1fd412eff70cc2527ad3090f16a55`. The +[SPI-P1 runbook](spi-p1.md) records the implementation, interface contracts, +coverage and commands. Default ICS55/PLL-present and explicit IHP130/no-PLL +compatibility remain SAFE24. Production product filelists, GPIO/RCU/address +maps, DMA V2.2, HAL/application integration and dependency versions are unchanged. +The standalone register header is additive; DMA capability remains clear. + +Standalone implementation validation completed on 2026-10-19; no SPI-P1 human +acceptance or later-phase approval is recorded. Tiny P10 remains pending +complete regression closure. Read the +dated implementation results separately from the original P0 freeze record. + +Evidence roots for the original candidate were: + +- `build/ics55-tiny-2026-10-18-23-58-bbe722dc382e/meta/spi-p1/`. +- `build/ihp130-tiny-2026-10-18-23-58-439583e27401/meta/spi-p1/`. + +Earlier attempts remain retained. In particular, initial formal tool PASS +results before `sv2v -E Assert` had no active properties and are invalid as +qualification evidence. Later induction/BMC timeouts, AIG preparation errors, +statistics-parser failures and the Icarus fixture timeout remain attributed +to their original sources. The Icarus timeout was caused by sv2v's lowering +of an early task return into millions of empty loop iterations; moving the +exit condition into the loop preserves its bound and every test case. +The 23:25 cover reached all goals but timed out during optional VCD export; +it remains failed. The 23:53 campaign disables that export, retains compact +witnesses and validates their length. Its induction and depth192 BMC reuse +the successful 23:25 subtasks only after exact model/configuration, proof +input/tool, artifact-integrity and nonvacuity checks. Original producer +identities remain in the reuse records; no historical failure is relabeled. +The 23:53 cover passed with a 195-step witness. The final 23:58 cohort follows +the repository formatter's Makefile EOF convention; its source snapshot is +distinct, and its focused gates are retained separately. + +### Completed standalone results (2026-10-19) + +The frozen `docs/ip/spi.md` SHA-256 is +`2c6b5c40d88973e34eb5e291c5cee40fa0128f7cc860727283e5b9c5ca32706c`. +The implementation remains an uncommitted worktree delta on the revision +above; each stage retains its actual source map, source archive, external +input hashes and commands. `report/record.json` combines checked stage records +without accepting the phase. `validation/final-audit.json` independently checks +current-source identity, retained artifact hashes, markers and result files. + +| Check | Result and boundary | +| --- | --- | +| Verilator and Icarus | All four standalone fixtures pass on each simulator; 305 core segments per simulator, including 48 exhaustive mode/width/order/direction cases, DIV65535 and 256 deterministic random segments | +| Formal | Phase and register induction pass; depth192 session-core BMC passes (original producer 773.96 s); final cover passes with a 195-step witness and active-property checks; compositional scope only | +| ABI/tool negative tests | 29 pass, including all 101 handwritten SVH/C constants and rejection of stale/failed/vacuous proof reuse | +| Quality | Formatting, owned RTL style/readiness, C policy/host tests, Ruff, standalone C header compilation and whitespace checks pass | +| Full Pytest | 2068 passed, 1 skipped in 4860.55 s; optional PDF retrieval test lacks `pypdf`; no dependency was installed or changed | +| Compatibility firmware | TINY/ICS55, TINY/IHP130 and MINI/IHP130 compile successfully in the retained 23:25 campaign; no product SPI or firmware-simulation claim | +| Regression definitions | PR/nightly dry-runs pass for TINY/ICS55, TINY/IHP130 and MINI/IHP130; these are not executed full regressions | + +| Block backend | ICS55 | IHP130 | +| --- | --- | --- | +| Balanced mapped cells | 7431 | 7949 | +| Liberty area | 19240.76 | 126612.7254 | +| FIFO payload / block SRAM macros | 2 x 256 bits / 0 | 2 x 256 bits / 0 | +| Standard-cell netlist fixture | PASS | PASS | +| Internal PCLK setup/hold WNS and TNS | all 0.00 | all 0.00 | + +Area is the selected library's synthesis statistic, not placed area or a +cross-PDK density claim. PCLK is 41.666666667 ns; synthesis uses rounded +41667 ps. STA uses one slow library per PDK and no external delay model: +each report has 319 inputs missing input delay, 41 outputs missing output +delay and 42 unconstrained endpoints. There is no blanket reset/MISO exception. +This does not qualify serial I/O, reset recovery/removal, board timing, all PVT +corners, higher SYS/PCLK operation or a complete Tiny netlist. + +Raw warnings remain retained: ABC reports combinational-network mapping in +both PDKs and six multi-output library cells in ICS55; formal lowering reports +FIFO memory expansion. Make records host/filesystem clock skew. Owned lint +passes with only the explicitly scoped managed-Common suppressions. No warning +baseline was regenerated, no metric was promoted, and no whole-product +warning/metric gate is claimed by these standalone targets. + +Unrun/deferred: long full-firmware Icarus and complete supported product +regressions remain deferred to the final combined campaign; no repeated P7/VGA +campaign, full-chip synthesis/netlist/STA, commercial flow, physical/Pad/board +or silicon qualification was run. Actual DMA V2.2, latched fabric origin, +GPIO/RCU integration, CDC/RDC and SDK/display qualification remain P2/P3 or +later obligations. No new MISRA deviation is required. Independent read-only +review and explicit human phase acceptance remain the next gate; the +readiness status stays `prototype` and `phase_accepted` stays false. + ## Configuration and Identity - Current normative default: TINY/ICS55, `HAVE_PLL=YES`, SAFE24 boot under the @@ -37,8 +186,9 @@ Tiny, SPI-SD, XPI, DMA and PIO evidence does not automatically cover this IP. ## Required Case Matrix -All cases currently have status **required, not run**. Later phase records -must add scoped evidence without deleting unmet conditions. +At P0 freeze all cases had status **required, not run**. The dated P1 record +above adds standalone evidence only; later integration and physical obligations +in this matrix remain required. | Case | Requirements | Required observation / phase | | --- | --- | --- | @@ -130,7 +280,7 @@ recovery. Tiny success requires exit 0, TEST_STATUS/`SIM_TEST_PASS` and no `SIM_TEST_TIMEOUT`. UART output is diagnostic only. Mini retains its own configured verdict; never substitute Mini coverage for missing Tiny support. -## Freeze Record and Gaps +## Freeze Record and Gaps (historical P0) | Phase | Evidence status | | --- | --- | diff --git a/rtl/ip/README.md b/rtl/ip/README.md index 1291cd07..04203cd5 100644 --- a/rtl/ip/README.md +++ b/rtl/ip/README.md @@ -22,6 +22,9 @@ Tiny block, distinct from SPI-SD and XPI. Its APB/packed FIFOs, native GPIO guard, source-qualified DMA V2.2 MMIO pacing and `SPI-P0..P5` gates are defined there, with [pending verification](../../docs/ip/spi-verification.md). A specification or reserved route does not add it to the current RTL/filelists. +The [SPI-P1 standalone implementation](../../docs/ip/spi-p1.md) is isolated +from product filelists. Its DMA capability remains clear; actual DMA V2.2, +Tiny routing, lifecycle and SDK integration belong to P2/P3. The [PPALite contract](../../docs/ip/ppalite.md) specifies a future camera-inline PCLK processor with RAW bypass, small FIFOs and existing DVP_RX11/DMA2 output. diff --git a/scripts/README.md b/scripts/README.md index 16e73a1d..97df6ecb 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -26,6 +26,12 @@ Scripts are part of the build contract. Prefer existing helpers over ad-hoc shell behavior, preserve structured JSON results, and keep setup/download behavior controlled by `dependencies/dependencies.lock.json`. +`spi_p1.py` runs the standalone SPI core through explicit `spi-p1-*` Make +entrypoints. It preserves attempt directories, source archives, command results +and simulation verdicts under the selected Tiny build variant. It does not +instantiate SPI in Tiny or implement central-DMA pacing. See the +[SPI-P1 runbook](../docs/ip/spi-p1.md) for scope and pending qualification. + `generate_apu_kws_rtl_constants.py` also emits the frozen APU-P9 APUC image and 15-bank layout manifest. `apu_kws_coeff.py` owns the independent APUC 1.0 schema and release validator; generated assets remain below the selected diff --git a/tests/README.md b/tests/README.md index 5edfefaf..2fac86d9 100644 --- a/tests/README.md +++ b/tests/README.md @@ -117,6 +117,19 @@ python3 -m pytest -q These tests complement, but do not replace, firmware builds, RTL simulation, synthesis, timing, or hardware validation. +`test_spi_register_parity.py` checks the handwritten SPI APB 1.0 mirror against +the independent frozen map and verifies that product filelists do not yet +advertise the block. `test_spi_p1.py` tests strict verdict and artifact identity +rejection and executes five standalone fixtures on both simulators. The +pin-checker selftest feeds valid and malformed synthetic waveforms to the +same oracle used by the DUT fixtures. Complete-core tests include 37-byte +and 19-halfword transfers, deliberate TX starvation/RX-full waits, delayed +service, tail checking and phase-safe ABORT. Tool inventory tests cover SBY +Python modules, Yosys SMT/witness helpers and ABC, including missing or changed +components and incompatible historical inventories. The +`spi-p1-rtl` and backend targets retain separate qualification artifacts; +they are not a Tiny SPI firmware integration result. + Historical Tiny publication fixtures also need the main repository history and dependency commit objects named by their archived locks. After ordinary dependency setup, run `python3 tests/publication_history.py prepare` before