dreamqin68 opened a new pull request, #41:
URL: https://github.com/apache/tvm-vta/pull/41
## Summary
`TensorStoreNarrowVME` advances its sub-block select register `tag` back to
`0` on `tag === (numMemBlock - 1).U` **without gating that wrap on the write
handshake** `io.vme_wr.data.fire`. When the AXI slave legally de-asserts
`WREADY` at the high-half beat of a 128-bit output element, the engine rolls
`tag` back to the low half while the high-half beat is still unaccepted. This
has two consequences:
1. It changes `WDATA` while `WVALID` is held high and the beat has not been
accepted — an **AXI4 write-data channel stability violation** (per the AMBA AXI
handshake-process rule, ARM IHI 0022 §A3.2.1: once a source asserts `VALID` it
must keep `VALID` asserted and hold the payload — `WDATA`/`WSTRB`/`WLAST` —
stable until the `READY` handshake completes).
2. It re-presents and re-accepts the **low half** in the slot that owed the
high half, injecting a duplicate beat that **shifts the accepted write stream
by one 64-bit beat**, so the beat the `AW` burst committed to its last slot is
displaced off the end. When the burst is packed with real data that displaced
beat is a real block (silent data loss); the witness below proves the
beat-sequence shift itself but does not exhibit a real-data drop (see the scope
note).
The bug only fires when `WREADY` de-asserts at the high-half (last
sub-block) beat; a stall at the low-half beat is benign. It is contingent on
the AXI slave / interconnect de-asserting `WREADY` mid-burst, which AXI4
explicitly permits, so designs whose memory subsystem happens to hold `WREADY`
high across a burst never observe it — but it is a latent correctness bug, not
a protocol-legal behavior.
Scope of the "corruption" claim: the witness below proves the
**module-level** effect — the accepted-beat sequence shifts by one 64-bit beat
and re-accepts the low half — which is a genuine AXI-protocol violation on the
write channel. The **end-to-end** numerical impact on a stored tensor (which
DRAM bytes end up wrong, and whether a tail block is dropped) additionally
depends on the `AW`-committed burst length and the memory subsystem's tail
handling, and is not reproduced here. So "corruption" here means a proven
write-stream desynchronization, not a demonstrated end-to-end wrong-value
workload.
## Root cause
In `hardware/chisel/src/main/scala/core/TensorStoreNarrowVME.scala`:
```scala
when(state === sWriteCmd || tag === (numMemBlock - 1).U) { // <-- wrap
ungated by fire
tag := 0.U
}.elsewhen(io.vme_wr.data.fire) {
tag := tag + 1.U
}
```
`io.vme_wr.data.bits.data := mdata(tag)` and `io.vme_wr.data.valid := state
=== sWriteData`. On a `WREADY`-low cycle the FSM stays in `sWriteData` (its
transition out is guarded by `io.vme_wr.data.ready`), so `WVALID` stays high
while `tag` wraps underneath it.
The inconsistency is visible inside the same block: the sibling pointers for
the same write stream are already handshake-gated —
```scala
}.elsewhen(io.vme_wr.data.fire && tag === (numMemBlock - 1).U) { set := set
+ 1.U }
...
}.elsewhen(io.vme_wr.data.fire && set === (tensorLength - 1).U && tag ===
(numMemBlock - 1).U) { raddr_cur := raddr_cur + 1.U }
```
Only `tag`'s wrap is left ungated.
## The fix
Gate both the wrap and the increment on `io.vme_wr.data.fire`, matching how
`set` and `raddr_cur` already advance:
```scala
when(state === sWriteCmd) {
tag := 0.U
}.elsewhen(io.vme_wr.data.fire) {
tag := Mux(tag === (numMemBlock - 1).U, 0.U, tag + 1.U)
}
```
On entry (`sWriteCmd`) `tag` resets to 0; on each accepted beat it wraps if
at the last sub-block, else increments. During a `WREADY` stall there is no
fire, so `tag` holds and the high-half beat stays presented and stable.
### Why this is behavior-preserving off the stall path
The one place the FSM leaves `sWriteData` between sub-block groups is the
`sReadMem` re-read cycle. A maintainer will reasonably ask what `tag` does
across the `sWriteData -> sReadMem -> sWriteData` round-trip, since the
original code reset `tag` unconditionally at the wrap moment while this patch
folds the reset into the fire branch. Tracing the FSM (`sWriteData` block and
`is(sReadMem){ state := sWriteData }`):
- `sReadMem` is entered **only** on `io.vme_wr.data.ready` (= fire, since
`WVALID` is high in `sWriteData`) with `tag === (numMemBlock - 1).U` and `xcnt
=/= xlen`. So the high-half beat has already been **accepted** before the FSM
moves to `sReadMem`.
- On that accepting cycle the patched code takes the
`.elsewhen(io.vme_wr.data.fire)` branch and computes `Mux(tag === last, 0.U,
...)` = `0.U` — identical to the original unconditional reset for the fire case.
- On the `sReadMem` cycle itself, `state === sWriteCmd` is false and
`io.vme_wr.data.valid` (`state === sWriteData`) is false, so `fire` is false;
neither branch executes and `tag` holds `0`.
- Back in `sWriteData`, `tag = 0` selects the low half of the next element.
So on the no-stall path the patched `tag` sequence is bit-for-bit identical
to the original; the only behavioral change is under back-pressure (high-half
beat not yet fired), where `tag` now holds instead of wrapping early. This is
confirmed empirically: the CONTROL run of the witness below stores two 128-bit
elements and its accepted-beat sequence (the four real beats `LOW0, HIGH0,
LOW1, HIGH1` followed by two `ZERO` pad beats) — which crosses the `sReadMem`
round-trip between elements 0 and 1 — is identical before and after the patch.
## Reproduction and verification (Verilator)
A self-contained directed Verilator witness drives the elaborated module
directly and runs the **same stimulus twice**: a CONTROL run that never
de-asserts `WREADY`, and a STALL run that de-asserts `WREADY` for 3 cycles
exactly at the high-half beat. It machine-checks two properties and is written
to FAIL if the DUT holds `WDATA` stable and accepts the same beat sequence as
the control, so it can refute, not only confirm. The two loaded elements give
the symbol names used below: `LOW0 = 0x1716151413121110`, `HIGH0 =
0x1f1e1d1c1b1a1918`, `LOW1 = 0x4746454443424140`, `HIGH1 = 0x4f4e4d4c4b4a4948`,
and `ZERO = 0x0000000000000000` (the burst over-reads past the two loaded
elements, so its tail beats are zero).
The FIXED `.sv` was re-elaborated from the patched Chisel via `sbt runMain
vta.DefaultPynqConfig` inside docker `tlcpack/ci-cpu:20220630` at the
repo-pinned Chisel 3.5.0 / Scala 2.12.15, with no hand-edited Verilog; the
witness itself simulates on host Verilator 5.048.
Before the fix:
```
STALL run:
cyc 1: WVALID=1 WREADY=1 WDATA=LOW0 <= ACCEPTED
cyc 2: WVALID=1 WREADY=0 WDATA=HIGH0 (high-half beat, not
accepted)
cyc 3: WVALID=1 WREADY=0 WDATA=LOW0 (!! WDATA changed under
WVALID && !WREADY)
cyc 4: WVALID=1 WREADY=0 WDATA=LOW0 (still stalled)
cyc 5: WVALID=1 WREADY=1 WDATA=LOW0 <= ACCEPTED (low half accepted a
SECOND time)
CONTROL accepted beats: LOW0, HIGH0, LOW1, HIGH1, ZERO, ZERO (0 stability
violations)
STALL accepted beats: LOW0, LOW0, HIGH0, LOW1, HIGH1, ZERO (1 stability
violation)
P1 (AXI W-stability violated): CONFIRMED
P2 (low half accepted twice): CONFIRMED
```
The full accepted sequences (verbatim from the log) show the stutter
precisely: the STALL run inserts a second `LOW0` and shifts every later beat
one slot right, so `HIGH1` is still accepted — what falls off the end of the
burst is one of the two trailing `ZERO` pad beats, not real data. In this
stimulus the burst over-reads two zero-pad beats (only two elements were
loaded), which absorb the one-beat shift; see the scope note above for why a
real-data drop is inferred but not exhibited here.
After the fix, re-elaborated from the patched Chisel and re-run with the
identical witness:
```
STALL run:
cyc 2..4: WVALID=1 WREADY=0 WDATA=HIGH0 held stable across the whole stall
cyc 5: WVALID=1 WREADY=1 WDATA=HIGH0 <= ACCEPTED
CONTROL accepted beats: LOW0, HIGH0, LOW1, HIGH1, ZERO, ZERO (0 stability
violations)
STALL accepted beats: LOW0, HIGH0, LOW1, HIGH1, ZERO, ZERO (0 stability
violations)
P1: REFUTED
P2: REFUTED
```
The fix restores `WDATA` stability under back-pressure and makes the
accepted-beat sequence under a stall identical to the no-stall sequence.
Diffing the elaborated Verilog before vs after the patch shows the only logic
change is the `tag` next-state block (everything else is net renumbering from
the added `Mux`); the fix is surgical.
### Bounded-exhaustive stall sweep (invariant held to bound)
To move from "one counterexample" to "the invariant holds under every
bounded stall", a second witness injects a `WREADY`-low stall of length `len`
on the beat at position `pos`, for every `pos` in `[0, 4)` (the two 128-bit
elements = beats `low0, high0, low1, high1`, which crosses the `sReadMem`
round-trip) and every `len` in `[1, 8]`, and checks P1 (0 W-stability
violations) and P2 (accepted sequence == the no-stall CONTROL sequence) for
each of the 32 combinations. The same sweep runs on both DUTs, with a
non-vacuity guard requiring CONTROL itself to accept the four real beats with 0
violations:
- Pre-fix: 16 of 32 fail — **exactly** the 16 high-half positions (`pos` 1
and 3, all 8 lengths); every low-half stall is clean. This confirms the defect
is specific to the high-half beat and that low-half back-pressure is benign,
and shows the check has teeth.
- Fixed: **0 of 32 fail** — the invariant `WVALID && !WREADY |=>
$stable(WDATA)`, together with the accepted-beat sequence, holds under every
bounded stall position and length.
Scope of the bound: this is exhaustive over stall position and length (to
length 8) for the shipping `DefaultPynqConfig` (`numMemBlock = 2`, so the
sub-block phases are exactly {low, high}). It is a bounded simulation proof,
not an unbounded formal one, and does not re-elaborate `numMemBlock > 2`
configs.
`numMemBlock` is **derived, not a literal**: `numMemBlock = (tensorWidth *
tensorElemBits) / memBlockBits` (`TensorUtil.scala:62`). For the store's `out`
tensor (`TensorStore(tensorType = "out")`, `Store.scala:52`) under
`DefaultPynqConfig`, the three inputs are `tensorWidth = blockOut = 16`,
`tensorElemBits = outBits = 8`, and `memBlockBits = memParams.dataBits = 64`
(note: the mem bus, not `hostParams.dataBits = 32`), so `numMemBlock = (16 * 8)
/ 64 = 128 / 64 = 2` — a 128-bit output element streamed as two 64-bit
sub-blocks. A different tensor type or a config with different
`blockOut`/`outBits`/`memBlockBits` changes this count, so the two-phase {low,
high} structure the sweep exhausts is config-specific; the fix itself (gating
the wrap on `fire`) is not — it is correct for any `numMemBlock`.
## Precedent (same defect class, load side)
The same class of defect — a DRAM-transfer pointer advancing while the data
handshake is de-asserted — was fixed once before, on the load path, in commit
`164f3e0dc71b17121b9750c75aa9582fdafbbf57` ("[VTA][Chisel] LoadUop FSM bug
fix", inside `[VTA][Chisel,de10nano] Chisel fixes and de10nano support`,
Pasquale Cocchini, 2020-03-09). That fix's own words: "The LoadUop FSM
incorrectly advances the address of the next uop to read from DRAM when the
DRAM data valid bit is deasserted"; it folded the address advance into the
handshake-guarded section of the FSM — exactly the shape of this store-side
fix. The store-side `tag` wrap was not covered then and is still ungated now.
(This commit is reachable on the `master` branch and originated as `apache/tvm`
monorepo PR #4986; its hash was preserved across the split into
`apache/tvm-vta`.)
## Reproduction artifacts
The only code change in this PR is the one-line `tag` next-state fix shown
above. The two Verilator witnesses (directed + bounded sweep), their build
scripts, run logs, and the pre-/post-fix elaborated `.sv` are a standalone
verification harness kept outside this repository; happy to attach them or open
a follow-up if a reviewer would like to run them.
---
<details>
<summary>Related / out of scope (not part of this PR)</summary>
- **Legacy monolithic store on the separate `master` branch.** The `master`
branch (not the default `main`) still ships the pre-refactor monolithic
`TensorStore.scala` (256 lines), whose `tag` wrap at lines 182-186 is the
identical ungated `when(state === sWriteCmd || tag === (numMemBlock - 1).U) {
tag := 0.U }.elsewhen(io.vme_wr.data.fire()) { tag := tag + 1.U }`. On `main`,
`TensorStore.scala` is only a 62-line dispatcher with no `tag` logic (the
datapath was split into `TensorStoreNarrowVME` / `TensorStoreWideVME`), so a
`main` grep of `TensorStore.scala` will not show the bug — it lives in
`TensorStoreNarrowVME.scala`, which this PR fixes. If `master` is still
maintained, the same one-line handshake-gating applies there.
- **`TensorLoadSimple.scala` dead-code look-alike.** It has a structurally
similar ungated `tag` wrap on the read side (`state === sIdle || state ===
sReadCmd || tag === (numMemBlock-1).U -> tag := 0`), but it is dead code:
`TensorLoad.scala` selects it only under `val forceSimpleTensorLoad = false`, a
hardcoded flag, so no shipped config instantiates it. Not touched by this PR.
- **Live load path is unaffected.** `TensorLoadNarrowVME` /
`TensorLoadWideVME` have no `tag` sub-block counter; their destination-index
and SRAM-write advances are gated on `io.vme_rd.data.fire`. Checked at the same
strength as the store bug: a directed Verilator witness on `TensorLoadWideVME`
(the live uop loader) inserting a mid-burst `RVALID` stall found the SRAM
read-back identical to a no-stall control, with both the load and the stall
shown non-vacuous.
</details>
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
To unsubscribe, e-mail: [email protected]
For queries about this service, please contact Infrastructure at:
[email protected]
