异步 FIFO：Packet 与累计进度交互演示

通用教学模型：7 个 slot；3-bit Gray 进度；3 级同步。时间统一以 Rx 时钟周期计；1 Tx 周期 = 4/7 Rx 周期。全部参数仅用于演示，不对应工程实现；不模拟亚稳态。

仿真时间: 0.00 Rx 周期

✅ 模型状态断言状态：全部 8 项运行时 Invariants 成立

占用: 0/7 写/读指针: W0/R0 计数器: W0/R0 FIFO 保序: 严格一致 满空互斥: 正常

时间轴步进: |

流量与握手:

Tx 发送域 · 1 周期 = 4/7 Rx 周期

#0 拍

下次: 0.57 Rx 周期

Rx 接收域 · 基准周期

#0 拍

下次: 1.00 Rx 周期

通道 ① Data 与 Metadata 准静态直连总线 (Tx ➔ Rx) — 稳定后由 Rx 捕获

Tx 物理触发器 (Data + Metadata slots): WrPtr = Slot-0

Data + Metadata ➔

Rx 接收端捕获触发器 (Rx capture):

None (空闲)

选通读取槽位:

Slot-0 (RdPtr)

通道 ② RdPtr[2:0] 异步反向回环选通通道 (Rx ➔ Tx 7:1 MUX.Sel) — Tx 零采样！以 RxClk 为基准闭环 | 纯组合回环

Tx 7:1 组合 MUX (selected Data):

MUX.Sel = RdPtr[000]b ➔ Slot-0

Tx 无触发器

◄ 反向回环 RdPtr

Rx 物理读指针 (RdPtr):

RdPtr = 0 (模 ${DEPTH}: 000b)

RxClk 驱动

通道 ③ WrCnt[2:0] 前向模 8 格雷码同步通道 (Tx ➔ Rx 3-DFF 同步器)

Tx 发射寄存器 (WrCnt):

WrCnt = 000 (Gray) | Bin = 0

发射源 Launch

跨域 WrCnt ➔

Rx 域 3-DFF 同步器: WrCntSync = 000

Stage 1

000

Stage 2

000

Stage 3 (同步输出)

000

通道 ④ RdCnt[2:0] 反向信用模 8 格雷码同步通道 (Rx ➔ Tx 3-DFF 同步器)

Tx 域 3-DFF 同步器: RdCntSync = 000

Stage 3 (同步输出)

000

Stage 2

000

Stage 1

000

◄ 跨域 RdCnt

Rx 信用发射寄存器 (RdCnt):

RdCnt = 000 (Gray) | Bin = 0

消费源 Launch

通道 ⑤ Sideband 实时背压警报侧带同步通道 (Tx ➔ Rx 1-bit 3-DFF) — 非 FIFO 队列！

Tx 发射寄存器 (实时状态输入): 0b

输入激励: 当前Rx_Sideband: 0b

实时 Sideband 由独立输入控制，不随 slot 排队。

1-bit Sideband ➔

Rx 1-bit 3-DFF 同步器 (同步状态输出): 0b

Stage 1

Stage 2

Stage 3 (同步输出)

Tx 满产生逻辑 (WrFull) WrFull = 0 (Tx.Rdy = 1)

数学意义: 写端可见占用达到 D 时为 Full；D 按延时覆盖需求选择

当前: WrCntBin=0, RdCntBin=0 实际占用: 0 / 7

Rx 空产生逻辑 (RdEmpty) RdEmpty = 1 (Rx.Vld = 0)

数学意义: 格雷码同构单射，Gray(A) == Gray(B) 恒等价于 A == B (零转换门延迟)

当前: RdCnt=000, WrCntSync=000 状态: 完全相同 ➔ FIFO 为空

模型时延多层次规范度量 (4 Decoupled Model Latency Metrics) 严格区分：计数器进度 CDC vs 握手完成 vs 满空边沿释放

① WrCnt CDC 可见时延

WrCnt Launch ➔ WrCntSync 可见:

-- Rx 周期

标称: φ + 2*Trx

② EMPTY ➔ Rx.Vld 拉高

空 ➔ 首包变非空置位 Vld:

-- Rx 周期

仅在 Empty 变非空触发，后续包=N/A

③ 报文端到端传输时延

Tx Accepted ➔ Rx Consumed:

-- Rx 周期

含 CDC 启动 + 排队 + 下游反压

④ FULL ➔ Tx.Rdy 满释放

满 ➔ 消费释放信用 Rdy 拉高:

N/A

标称: φ' + 2*Ttx，未满时=N/A

📦 视图 A：报文生命周期 (Packet Lifecycle)

选择报文:

💡 重要架构解耦提示：Packet 与 Gray counter transition 并非 1:1 CDC token。目的域可能跳过中间 counter state；FIFO 正确性依赖 progress 语义，而不是逐 packet counter event 被采样。

注入报文后，在此查看该报文的真实存储、产生计数事件、捕获与端到端完成时延。

⚡ 视图 B：计数器状态跳变 CDC 追踪 (Counter CDC History) 支持检测目的端采样跳步 (Skip)

暂无计数器跳变事件。步进仿真后查看 WrCnt / RdCnt 各事件的 Stage 1/2/3 采样或跳过状态。

🧪 6 大模型基准回归测试套件 (Model Check Regression Suite)

离散时钟边沿事件与时延统计追踪 (Strict NBA Event Log)

完成事务: 0

[0.00 Rx 周期] 仿真引擎就绪。解耦模型已加载，支持 Counter State Skip 与精确多级时延度量。