What is SVA?
SystemVerilog Assertions(SVA)는 특정 동작이나 시간 규칙을 검증하기 위해 설계 또는 테스트벤치에 포함된 명령문입니다.
Think of them as "Active Comments":
Passive: comments explain what code should do.
Active: SVA checks if the code actually does it, continuously, every clock cycle.
Types of Assertions
1. Immediate Assertions
Checked at a single point in time, like an if statement. Used in procedural code (always blocks, tasks, functions).
always @(posedge clk) begin
// Simple immediate assertion
assert (data != 'x)
else $error("Data is unknown!");
// With pass action
assert (valid && ready)
$display("Handshake successful!")
else
$error("Handshake failed: valid=%b, ready=%b", valid, ready);
// Assert with severity levels
assert (count <= MAX_COUNT)
else begin
$fatal(1, "Counter overflow! count=%0d, max=%0d", count, MAX_COUNT);
end
endImmediate assertions have three forms:
1. Simple Assert
// Basic form
assert (expression);
// With messages
assert (address[1:0] == 2'b00)
else $error("Address must be word-aligned!");2. Assert with Pass/Fail Actions
assert (expression) pass_action else fail_action;
// Example
assert (fifo_full && write_en == 0)
$display("PASS: No write when full")
else
$error("FAIL: Attempted write to full FIFO");3. Deferred Assertions (SystemVerilog 2012)
Deferred assertions handle glitches by evaluating at the end of the time step:
// #0 - Observed region (after all NBA updates)
assert #0 (data === expected_data)
else $error("Data mismatch in observed region");
// final - Final region (very end of time step)
assert final (done || (count < MAX))
else $error("Failed at end of time step");2. Concurrent Assertions
Checked continuously over time, can span multiple clock cycles. Used for protocol checking and temporal relationships.
// Property: After req goes high, ack must follow within 1-5 cycles
property req_ack_protocol;
@(posedge clk) disable iff (rst)
req |-> ##[1:5] ack;
endproperty
// Assert the property
assert property (req_ack_protocol)
else $error("Protocol violation: ack not received within 5 cycles of req");
// Cover the property (for verification)
cover property (req_ack_protocol)
$display("req->ack handshake observed");Concurrent assertions are the heart of SVA. They describe temporal relationships and protocols using sequences and properties.
// Level 1: SEQUENCE - Defines a pattern of events
sequence burst_start;
valid && ready && burst_type != 0;
endsequence
// Level 2: PROPERTY - Adds temporal logic
property burst_completes;
@(posedge clk) disable iff (reset)
burst_start |-> ##[1:10] burst_done;
endproperty
// Level 3: ASSERTION - Checks the property
assert property (burst_completes)
else $error("Burst did not complete within 10 cycles");
SVA는 항상 두 단계로 나뉩니다.
-
property (법안 발의): "이런 타이밍 규칙이 있어~"라고 조건을 정의만 해두는 곳입니다.
-
assert (경찰 투입): 방금 만든 property를 들고 시뮬레이션 내내 감시하다가, 어기면 $error로 체포하는 역할입니다.
1. Reset Checks (리셋 구간 감시)
property p_reset_awvalid;
@(posedge clk) (!rst_n) |-> (awvalid == 1'b0);
endproperty- 핵심 연산자: |-> (Overlapping Implication)
- 의미: "조건이 맞으면, 같은 클럭(Right now)에 결과를 확인해라."
- 해석: 클럭이 뛸 때 리셋(!rst_n)이 0이라면? 미루지 말고 바로 지금 당장(|->) awvalid도 0인지 확인해라!
2. Handshake Hold Rules (VALID 유지 규칙)
property p_awvalid_hold;
@(posedge clk) disable iff (!rst_n)
(awvalid && !awready) |=> (awvalid);
endproperty- 핵심 연산자: |=> (Non-overlapping Implication)
- 의미: "조건이 맞으면, 다음 클럭(Next clock)에 결과를 확인해라."
- 해석: 리셋 중이 아닐 때(disable iff), 만약 이번 클럭에 마스터가 valid를 띄웠는데 슬레이브가 아직 ready를 안 줬다면(awvalid && !awready)? ➔ 마스터 너, 다음 클럭(|=>)에도 무조건 valid 계속 띄우고 있어! (내 마음대로 내리면 에러!)
diable iff(!rst_n)
만약 리셋(rst_n)이 0으로 떨어지면, 지금 감시하고 있던 SVA 룰을 전부 무시하고 당장 CCTV의 전원을 꺼버려라!"라는 뜻입니다.
- disable: 작동을 멈춰라! (Kill the assertion)
- iff (if and only if): 오직 이 괄호 안의 조건이 참(True)일 때만!
3. Payload Stability Rules (데이터 변경 금지 규칙)
property p_awaddr_stable;
@(posedge clk) disable iff (!rst_n)
(awvalid && !awready) |=> $stable(awaddr);
endproperty- 핵심 연산자: $stable (Stability Check)
- 의미: "이전 클럭이랑 값이 똑같은지(안 변했는지) 확인해라."
- 해석: 이번 클럭에 valid를 줬는데 ready를 못 받아서 대기 중이라면(awvalid && !awready)? ➔ 너 다음 클럭(|=>)에 주소값 바꾸지 말고 그대로 유지해($stable(awaddr))! 기다리는 도중에 주소나 데이터를 몰래 딴 걸로 바꾸면 에러!
AXI4-Lite Assertions
// 1. Reset Checks (Reset 구간에서 VALID 신호들은 0이어야 함)
property p_reset_awvalid; @(posedge clk) (!rst_n) |-> (awvalid == 1'b0); endproperty
property p_reset_wvalid; @(posedge clk) (!rst_n) |-> (wvalid == 1'b0); endproperty
property p_reset_arvalid; @(posedge clk) (!rst_n) |-> (arvalid == 1'b0); endproperty
assert_reset_awvalid: assert property(p_reset_awvalid) else $error("SVA FATAL: AWVALID is not 0 during reset!");
assert_reset_wvalid: assert property(p_reset_wvalid) else $error("SVA FATAL: WVALID is not 0 during reset!");
assert_reset_arvalid: assert property(p_reset_arvalid) else $error("SVA FATAL: ARVALID is not 0 during reset!");
// 2. Handshake Hold Rules (VALID가 뜨면 READY가 뜰 때까지 유지되어야 함)
property p_awvalid_hold; @(posedge clk) disable iff (!rst_n) (awvalid && !awready) |=> (awvalid); endproperty
property p_wvalid_hold; @(posedge clk) disable iff (!rst_n) (wvalid && !wready) |=> (wvalid); endproperty
property p_arvalid_hold; @(posedge clk) disable iff (!rst_n) (arvalid && !arready) |=> (arvalid); endproperty
assert_awvalid_hold: assert property(p_awvalid_hold) else $error("SVA FATAL: AWVALID dropped before AWREADY!");
assert_wvalid_hold: assert property(p_wvalid_hold) else $error("SVA FATAL: WVALID dropped before WREADY!");
assert_arvalid_hold: assert property(p_arvalid_hold) else $error("SVA FATAL: ARVALID dropped before ARREADY!");
// 3. Payload Stability Rules (READY를 기다리는 동안 주소/데이터는 변하면 안 됨)
property p_awaddr_stable; @(posedge clk) disable iff (!rst_n) (awvalid && !awready) |=> $stable(awaddr); endproperty
property p_wdata_stable; @(posedge clk) disable iff (!rst_n) (wvalid && !wready) |=> $stable(wdata); endproperty
property p_araddr_stable; @(posedge clk) disable iff (!rst_n) (arvalid && !arready) |=> $stable(araddr); endproperty
assert_awaddr_stable: assert property(p_awaddr_stable) else $error("SVA FATAL: AWADDR changed while waiting!");
assert_wdata_stable: assert property(p_wdata_stable) else $error("SVA FATAL: WDATA changed while waiting!");
assert_araddr_stable: assert property(p_araddr_stable) else $error("SVA FATAL: ARADDR changed while waiting!");
Design Verification engineer