Skid Buffer¶

Skid buffer¶

Skid buffer 指的就是，对于 valid + ready 的握手信号，用空间（更多的逻辑）来换取时间（更好的时序）的一个硬件模块。

简单来说，背景就是，为了解决 valid 和 ready 信号在数据流水线上一路经过组合逻辑导致的时序问题，在中途加上一些寄存器来阻隔。当然了，代价就是延迟和面积，不过吞吐量还是需要保持的。

由于需求的不同，Skid buffer 也有不同的实现。目前，找到了四个实现，实现上有所不同，特性也不大一样。

统一约定¶

由于我在 SpinalHDL 语言中重新实现了下面的这些 Skid buffer，所以按照 SpinalHDL 的 Stream 定义接口：

class SkidBufferCommon[T <: Data](
    gen: => T
) extends Component {
  val io = new Bundle {
    val s = slave(Stream(gen))
    val m = master(Stream(gen))
  }
}

在这里，io.s 表示从上游取的数据，io.m 表示传递给下游的数据。

输出信号共有：io.s.ready、io.m.valid 和 io.m.payload。

ZipCPU 版本¶

第一个版本来自 ZipCPU：

博客地址：Building a Skid Buffer for AXI processing 代码地址：skidbuffer.v

它有两个参数，一个表示是否有额外的输出寄存器（outputReg），一个表示是否低功耗（lowPower）。

FPGACPU 版本¶

第二个版本来自 FPGACPU：

文章地址：Pipeline Skid Buffer

SpinalHDL S2M 版本¶

第三个版本来自 SpinalHDL Library 的 s2mPipe：

代码地址：Stream.scala L348

SpinalHDL M2S 版本¶

第四个版本来自 SpinalHDL Library 的 m2sPipe：

代码地址：Stream.scala L327

四个版本的对比¶

在研究了代码以后，可以看到这四个版本的区别：

版本	ZipCPU w/ outputReg	ZipCPU w/o outputReg	FPGACPU	S2M	M2S
io.s.ready	Reg	Reg	Reg	Reg	Comb
io.m.valid	Reg	Comb	Reg	Comb	Reg
io.m.payload	Reg	Comb	Reg	Comb	Reg
latency	1	0	1	0	1
buffer 数量	1	1	2	1	1

注：

Reg 表示从寄存器输出，Comb 表示从组合逻辑输出
Latency 表示从 io.s.fire 到 io.m.fire 的延迟
Buffer 表示缓冲的 payload 个数
ZipCPU w/o outputReg 和 S2M 实现的逻辑是一样的

形式化验证¶

为了确认上面这些类型的 Skid Buffer 都可以正常工作，按照 ZipCPU Skid Buffer 的文章，也照着写了几个 property：

1: 在 valid && ~ready 的时候，valid 需要继续保持为高，并且 payload 不变：

// When valid goes high, data is stable and valid stays high before ready
when(past(stream.valid && ~stream.ready && ~outerReset)) {
    slaveAssume(stream.valid);
    if (dataStable) {
        slaveAssume(stable(stream.payload.asBits));
    }
}

2: 在 reset 释放的第一个周期里，valid 不能为高：

参考 AXI 标准 (IHI0022E Page 38 A3.1.2) 原文：

The earliest point after reset that a master is permitted to begin driving ARVALID, AWVALID, or WVALID HIGH is at a rising ACLK edge after ARESETn is HIGH.

// Valid is low in the first cycle after reset falls
when(pastValid && past(outerReset) && ~outerReset) {
    slaveAssume(~stream.valid);
}

3: 添加 cover property，要求 io.s 和 io.m 可以连续若干个周期 valid && ready，保证吞吐率：

cover(
    pastValid && genPast(pastValid, null, cycles) && genPast(
        ~outerReset,
        null,
        cycles
    ) && genPast(stream.fire, payload, cycles)
)

采用 yosys-smtbmc 工具验证了以上四种 Skid buffer 都满足这些属性。