𝗦𝗩𝗔 │ READY가 낮을 때 VALID와 data를 어떻게 검사할까?
SVA stall-hold property for a READY/VALID channel: next-edge VALID and payload stability
버스가 바쁠 때만 가끔 데이터가 사라진다고 해봅시다. 파형을 보니 VALID가 올라온 뒤 READY가 두 cycle 동안 0인데, 그 사이 VALID가 내려가거나 data가 바뀝니다. 평소에는 READY가 바로 1이라 지나쳤던 오류입니다.
READY/VALID 인터페이스에서 전송은 clock edge에 VALID와 READY가 모두 1일 때 성립합니다. VALID=1, READY=0인 edge는 아직 수락되지 않은 상태입니다. 따라서 source는 다음 edge에도 VALID와 그 전송의 payload를 유지해야 합니다. READY가 다음 edge에 1로 바뀌더라도, 바로 그 edge까지 같은 payload가 남아 있어야 합니다.
이 계약은 SystemVerilog assertion으로 짧게 쓸 수 있습니다. 여기서 rst_n은 active-low reset이고, payload는 해당 channel의 data와 sideband를 함께 묶은 신호입니다.
ap_hold_on_stall: assert property (
@(posedge clk) disable iff (!rst_n)
valid && !ready |=> valid && $stable(payload)
);
예를 들어 edge N에서 VALID=1, READY=0, payload=A라면 edge N+1에도 VALID=1과 payload=A를 검사합니다. N+1에도 READY=0이면 같은 의무가 N+2까지 이어집니다. N+2에서 READY=1로 전송이 끝난 뒤에는 다음 전송의 payload로 바꿀 수 있습니다.
여기서 |=>가 중요합니다. 조건이 맞은 다음 clock edge를 검사하기 때문입니다. |->로 바꾸면 같은 edge를 검사해 버립니다. 특히 첫 stall edge에서 data가 이전 전송 값에서 새 값으로 바뀐 것은 합법인데, 그 변화를 잘못 잡고 정작 다음 edge의 유지 의무는 놓칠 수 있습니다.
리뷰할 때는 payload에 byte enable, last, ID 같은 sideband까지 포함됐는지 확인하세요. 이 property는 stall 중 값 보존을 검증합니다. READY가 언젠가 올라와 전송이 끝난다는 liveness는 별도의 계약과 검증이 필요합니다. reset 구간과 X 값 처리도 환경에 맞춰 따로 점검해야 합니다.
근거: Arm, AMBA AXI and ACE Protocol Specification, IHI 0022H, §A3.2.1
https://developer.arm.com/-/media/Arm%20Developer%20Community/PDF/IHI0022H_amba_axi_protocol_spec.pdf
IEEE Std 1800-2023, SystemVerilog Language Reference Manual, §16
https://ieeexplore.ieee.org/document/10458102