시리즈: ... · sequences · coverage · SVA
SVA란
SVA = SystemVerilog Assertions
= "프로토콜 규칙을 매 사이클 자동으로 감시하는 감시자"
스코어보드/커버리지가 "완성된 버스트"를 사후 검사한다면,
SVA는 "매 클록마다" 프로토콜 위반을 실시간 감시앞서 배운 VALID/READY 골든 룰을 코드로 자동 감시하는 게 이 파일이다. 이력서의 "~25 bind-based SVA protocol assertions"의 실제 구현.
스코어보드/커버리지와 다른 위치
스코어보드: "완성된 버스트가 맞나?" (트랜잭션 단위, 사후)
커버리지: "이 조합을 봤나?" (트랜잭션 단위, 사후)
SVA: "지금 이 클록에 프로토콜 위반했나?" (사이클 단위, 실시간)
예: VALID를 올렸다가 READY 전에 내리면
→ 스코어보드는 모름 (데이터만 봄)
→ SVA는 그 순간 즉시 에러! ✅flowchart LR
BUS["AXI 버스<br/>매 클록 신호"]
BUS -->|매 사이클 감시| SVA["SVA<br/>프로토콜 위반?<br/>(실시간)"]
BUS -->|완성된 버스트| SB["Scoreboard<br/>데이터 맞나?<br/>(사후)"]
BUS -->|완성된 버스트| COV["Coverage<br/>조합 봤나?<br/>(사후)"]bind — RTL을 안 건드리고 주입
// Written as a standalone module and `bind`-ed into tb_top, so the
// checks are injected without touching the interface, the testbench
// or the RTL.이게 SVA의 핵심 설계 패턴이다.
bind = 별도 모듈을 기존 모듈에 "붙이는" 문법
axi4_sva를 독립 모듈로 작성
→ bind로 tb_top에 주입
→ 인터페이스/테스트벤치/RTL 코드를 하나도 안 건드림!
장점 (실무 표준):
프로토콜 체커가 설계 밖에 존재
→ 자유롭게 붙였다 뗐다 가능
→ +define+AXI4_NO_SVA로 통째로 제거 가능왜 tb_top에 bind하나 (interface가 아니라)
// a module may not be instantiated inside an interface
// (XSim rejects that with VRFC 10-3535). Binding at tb_top gives one
// checker instance that works with either DUT.
interface 안에는 module을 못 넣음 (XSim 제약)
→ tb_top에 bind
→ 두 DUT(v1/v2) 다 같은 인터페이스에 연결되므로
체커 하나가 양쪽 다 커버bind tb_top axi4_sva u_axi4_sva (
.clk (clk),
.awid (axi.awid),
...
);"tb_top 안에 axi4_sva를 u_axi4_sva라는 이름으로 붙여라"
신호는 tb_top의 axi 인터페이스 신호에 연결⚠️ XSim 제약 — 이 파일의 숨은 고생
주석 곳곳에 XSim(Vivado 시뮬레이터)의 함정이 기록돼있다. 이게 이력서의 "validated assertion liveness via negative testing"의 배경이다.
함정 1 — untyped property argument가 조용히 무시됨
// properties with *untyped* formal arguments are silently ignored by
// Vivado XSim — "untyped port "valid" found ... It will be ignored."
// which makes the whole checker vacuous without any error.문제:
파라미터화된 property를 쓰면
XSim이 조용히 무시함 (에러도 없이!)
→ 체커가 아무것도 안 하는데 "통과"로 보임 (vacuous = 공허한)
이게 앞서 배운 blind pass criterion과 같은 위험!
→ 체커가 눈멀어있는데 아무도 모름
해결:
파라미터 property 대신 매크로로 인라인 확장
→ 각 assertion을 직접 펼침함정 2 — dynamic array가 assertion에서 무시됨
// XSim cannot evaluate dynamic arrays/queues inside a concurrent
// assertion ("Dynamic array inside concurrent assertion. It will be
// ignored." — silently vacuous!). So the outstanding-address tracker is
// a STATIC circular buffer.문제:
outstanding 추적에 queue를 쓰고 싶은데
XSim이 assertion 안의 dynamic array를 무시 → 또 vacuous
해결:
static circular buffer(고정 크기 원형 버퍼)로 구현
→ assertion은 거기서 뽑은 scalar만 참조그래서 negative testing으로 검증
// the checker was validated with a deliberately failing self-test assertion.
체커가 "진짜 동작하는지" 확인하려고
일부러 실패하는 assertion을 넣어봄
→ 정말 FAIL 나는지 확인
→ "vacuous가 아니라 실제로 감시 중"임을 증명
= assertion liveness 검증 (체커를 검증하는 것)매크로 — 인라인 확장
`define AXI_VALID_HELD(nm, vld, rdy) \
nm: assert property (@(posedge clk) disable iff (rst) \
((vld) && !(rdy)) |=> (vld)) \
else $error("AXI-SVA: %s - VALID de-asserted before READY", `"nm`");
`define AXI_STABLE(nm, vld, rdy, sig) \
nm: assert property (@(posedge clk) disable iff (rst) \
((vld) && !(rdy)) |=> $stable(sig)) \
else $error("AXI-SVA: %s - payload changed while stalled", `"nm`");매크로 = property를 파라미터화하는 대신 텍스트로 펼치기
(XSim의 untyped argument 함정 회피)
nm = assertion 이름
vld = VALID 신호
rdy = READY 신호
sig = 안정성 체크할 payload
`"nm`" = 매크로 인자를 문자열로 (에러 메시지용)assertion 종류별 정리
1. VALID 유지 (골든 룰 2)
`AXI_VALID_HELD(a_awvalid_held, awvalid, awready)
`AXI_VALID_HELD(a_wvalid_held, wvalid, wready)
`AXI_VALID_HELD(a_bvalid_held, bvalid, bready)
`AXI_VALID_HELD(a_arvalid_held, arvalid, arready)
`AXI_VALID_HELD(a_rvalid_held, rvalid, rready)규칙: VALID를 올렸으면 READY 올 때까지 못 내림
((vld) && !(rdy)) |=> (vld)
= "VALID인데 READY 아직 안 옴" → "다음 사이클에도 VALID"
|=> = "다음 클록에" (overlapping이 아닌 next-cycle implication)
5개 채널 전부 감시 → 앞서 배운 골든 룰 2의 자동화2. Payload 안정 (골든 룰)
`AXI_STABLE(a_awaddr_stable, awvalid, awready, awaddr)
`AXI_STABLE(a_awlen_stable, awvalid, awready, awlen)
...
`AXI_STABLE(a_wdata_stable, wvalid, wready, wdata)
...규칙: 전송이 stall된 동안 payload가 바뀌면 안 됨
((vld) && !(rdy)) |=> $stable(sig)
= "VALID인데 READY 안 옴" → "다음 사이클에 sig가 그대로"
$stable(sig) = 이전 값과 같은지 (안 바뀌었는지)
→ VALID 올려놓고 주소/데이터를 바꾸는 위반 감지
awaddr, awlen, awsize, awburst, awid,
wdata, wstrb, wlast, araddr..., bresp, rresp, rlast 전부3. 예약/불법 인코딩
a_awburst_legal: assert property (@(posedge clk) disable iff (rst)
awvalid |-> awburst != 2'b11)
else $error("AXI-SVA: AWBURST uses the reserved encoding 2'b11");
a_awsize_fits: assert property (@(posedge clk) disable iff (rst)
awvalid |-> ((1 << awsize) <= STRB_WIDTH))
else $error("AXI-SVA: AWSIZE exceeds the data bus width");burst 2'b11 = 예약값 (사용 금지) → 쓰면 위반
size가 버스 폭 초과 → 위반 (32비트 버스에 8B 전송 불가)
|-> = "즉시" implication (같은 사이클)
disable iff (rst) = 리셋 중엔 검사 안 함4. X/Z 감지
a_aw_known: assert property (@(posedge clk) disable iff (rst)
awvalid |-> !$isunknown({awaddr, awlen, awsize, awburst, awid}))
else $error("AXI-SVA: X/Z on the AW channel while AWVALID");VALID인데 payload에 X/Z가 있으면 위반
$isunknown(sig) = sig에 X나 Z가 있나?
!$isunknown(...) = X/Z가 없어야 함
{a, b, c} = 신호들을 이어붙여서 한 번에 검사
→ 앞서 배운 "X 전파" 문제를 프로토콜 레벨에서 감지
(VALID일 때는 값이 확정돼야 함)5. 리셋 중 응답 금지
a_no_resp_in_reset: assert property (@(posedge clk)
rst |-> (!bvalid && !rvalid))
else $error("AXI-SVA: BVALID/RVALID asserted during reset");리셋 중엔 BVALID/RVALID가 뜨면 안 됨
rst |-> (!bvalid && !rvalid)
= "리셋이면" → "bvalid도 rvalid도 0"
이건 disable iff (rst)가 없음! (리셋 중을 검사하는 게 목적이니까)이게 이력서의 "cycle-accurate SVA catching reset-phase violations"와 연결되는 부분이에요.
6. WLAST/RLAST 위치 (가장 복잡)
버스트 beat 개수와 LAST 위치가 맞는지 검사. outstanding까지 지원하려고 tracker를 쓴다.
localparam int SVA_QDEPTH = 16;
int unsigned aw_len_mem [SVA_QDEPTH]; // static 배열 (dynamic 금지)
int unsigned aw_wr, aw_rd, ar_wr, ar_rd;
int unsigned w_beats, r_beats;
wire aw_pending = (aw_wr != aw_rd); // 대기 중인 AW 있나
wire [31:0] aw_head = aw_len_mem[aw_rd]; // 가장 오래된 AWLENstatic circular buffer로 outstanding 주소 추적:
AW 수락되면 → awlen을 버퍼에 저장 (aw_wr++)
WLAST 오면 → 버퍼에서 제거 (aw_rd++)
w_beats = 현재 몇 번째 W beat인가 카운트
aw_head = 지금 처리 중인 버스트의 예상 길이(AWLEN)always @(posedge clk) begin
if (rst) begin ... 리셋 ... end
else begin
if (awvalid && awready) begin // AW 수락
aw_len_mem[aw_wr] <= awlen;
aw_wr <= (aw_wr + 1) % SVA_QDEPTH;
end
if (wvalid && wready) begin // W beat
if (wlast) begin
w_beats <= 0;
if (aw_wr != aw_rd) aw_rd <= (aw_rd + 1) % SVA_QDEPTH;
end
else w_beats <= w_beats + 1;
end
...
end
end% SVA_QDEPTH = 원형 버퍼 (16 넘으면 0으로 되돌아감)
WLAST 위치 검사:a_wlast_position: assert property (@(posedge clk) disable iff (rst)
(wvalid && wready && wlast && aw_pending) |-> (w_beats == aw_head))
else $error("AXI-SVA: WLAST on beat %0d but AWLEN implies beat %0d",
w_beats, aw_head);"WLAST가 떴을 때 → 현재 beat 번호가 AWLEN과 같아야"
w_beats == aw_head
= "지금까지 센 beat 수" == "예상 길이"
→ WLAST가 너무 일찍/늦게 뜨면 위반!
overrun 검사도 있음:
a_w_no_overrun: !wlast일 때 w_beats < aw_head
= "아직 마지막 아닌데 예상 길이 넘으면" 위반전체 어서션 지도
| 어서션 그룹 | 감시 내용 | 개수 |
|---|---|---|
| VALID 유지 | READY 전 VALID 못 내림 | 5 |
| Payload 안정 | stall 중 값 고정 | 16 |
| 불법 인코딩 | 예약값/크기 초과 | 4 |
| X/Z 감지 | VALID 시 값 확정 | 3 |
| 리셋 응답 금지 | 리셋 중 응답 없음 | 1 |
| LAST 위치/overrun | beat 개수 일치 | 4 |
합계 ~33개 (이력서의 "~25"는 대략치)
+define+AXI4_NO_SVA — 통째로 끄기
`ifndef AXI4_NO_SVA
// ... 모든 assertion ...
`endif+define+AXI4_NO_SVA로 컴파일하면
→ 모든 assertion이 사라짐
→ 체커 없이 순수 시뮬레이션
용도: 디버깅 시 체커 노이즈 제거, 성능 측정 등
bind 패턴 덕에 이런 on/off가 자유로움SVA vs Scoreboard vs Coverage — 검증의 3축
| SVA | Scoreboard | Coverage | |
|---|---|---|---|
| 질문 | 규칙 지켰나? | 맞았나? | 봤나? |
| 단위 | 사이클 | 트랜잭션 | 트랜잭션 |
| 시점 | 실시간 | 사후 | 사후 |
| 감시 대상 | VALID/READY, 인코딩 | 데이터 값 | 시나리오 조합 |
| 위반 시 | 즉시 $error | mismatch | 낮은 % |
세 개가 상호보완:
SVA → 프로토콜을 어겼는지 (핸드셰이크, 타이밍)
Scoreboard → 데이터가 틀렸는지 (값)
Coverage → 충분히 테스트했는지 (범위)
→ 셋 다 있어야 "규칙 지키고, 정확하고, 빠짐없이" 검증한 줄 요약
SVA = 프로토콜 규칙을 매 사이클 실시간 감시하는 어서션 체커
bind 패턴:
독립 모듈로 작성 → tb_top에 주입 → RTL/TB 안 건드림
+define+AXI4_NO_SVA로 통째로 on/off
감시 항목 (~25+):
VALID 유지, payload 안정, 불법 인코딩,
X/Z 감지, 리셋 중 응답 금지, WLAST/RLAST 위치
XSim 함정 (실무 교훈):
untyped property, dynamic array가 조용히 무시됨 (vacuous)
→ 매크로 인라인 + static buffer로 회피
→ negative testing으로 "진짜 감시 중"임을 증명
검증 3축:
SVA(규칙) + Scoreboard(정확성) + Coverage(완결성)시리즈 완결 — 검증의 3축 완성
이제 AXI4 UVM 환경의 정말 모든 파일을 다뤘습니다.
tb_top
│
test → sequence → seq_item
│
cfg/agent/env ─ driver ─ interface ─ DUT
│
monitor
┌─────────────┼─────────────┐
scoreboard coverage SVA
(맞았나?) (봤나?) (규칙 지켰나?)
│ │ │
ref_model covergroup assertions
└─────────────┼─────────────┘
검증의 3축 완성검증의 세 가지 질문에 모두 답합니다:
- 정확성: scoreboard가 데이터를 ref_model과 비교 → "맞았나?"
- 완결성: coverage가 시나리오를 추적 → "봤나?"
- 준수성: SVA가 프로토콜을 실시간 감시 → "규칙 지켰나?"
이 셋이 만나 "규칙을 지키며, 정확하고, 빠짐없이 검증했다"는 완전한 신뢰를 만듭니다. 이것으로 AXI4-Full UVM 검증 환경 시리즈를 마칩니다.
Design Verification engineer