[Verilog 문법] 검증의 기본 Assertion 살펴보기

 

 

제목을 검증의 기본 Assertion이라고 했지만, 설계에 있어서도 Assertion은 필수적인 요소일까? 인터페이스나 버스, 프로토콜이 중요한 IP에는 조기 검증에 큰 도움이 된다고 본다. 하지만 Assertion을 쓰지 않는다고 해서 부족한 설계라고 할 수 없으며, 본인이 추구하는 방법대로 검증하는 실력 있는 설계자들도 많다. 

 

Assertion을 알고 제대로 사용한다면 불필요한 검증 리소스를 줄일 수 있고 내 설계의 어떤 부분이 수정되어야 하는지 빠르게 알 수 있다. 두 말 할 것 없이 검증 엔지니어라면 필수로 알아야만 하는 System Verilog 문법이며, IP의 입력이나 출력이 잘못되었는지 확인하기엔 이만한 방법이 없다.

 

설계 엔지니어일 때, Assertion은 내게 가깝고도 먼 이름이었다. 긴박한 TAT(Turn Around Time)에 쫓기며 설계를 하고 있으면 Assertion을 넣어야겠다는 생각만 했지, 현실적으로 검증 엔지니어가 넣어 준 부분만 확인하고 넘어가곤 했다. 직접 작성해보면 별 게 없는데, 막상 내 RTL 코드에 넣자니 찝찝한 알 수 없는 느낌적인 느낌.

 

 

미안... 뭔가 찜찜하단 말이야...

 

 

관련 강좌를 여러 번 듣고, 여러 웹페이지들을 방문하여 사용법을 읽어봐도, 내가 직접 코드를 작성하지 않으면 진짜 내 것이 되지 않는다. 일명

 

 

백 문 이 불 여 일 타 (百 聞 以 不 如 一 打)

백 번 듣는 것보다 한 번 쳐보는게 낫다.

 

 

제대로 사용할 줄 아는데 전략적으로 빼는 것과 잘 몰라서 쓰지 않는 것은 다르다. 오늘 포스팅에서는 검증의 묘를 더해주는 Assertion에 대해 살펴보고자 한다.

 

 

 

---

 

 

 

 

Assertion의 정의

 

Assertion의 사전적 정의는 다음과 같다.

 

Cambridge 사전에서 찾은 사전적 정의

 

 

SW testing 기법에서 유래된 것으로, 개발자가 반드시 참이어야만 하는 주장/명제를 코드로 구현하여 이를 위반하는 경우를 찾아 버그나 기타 문제를 발견하는 것이다. 보통은 Design spcification에 따라서 꼭 지켜져야 하는 부분을 코드에 심어둔다. 

 

예를 들어, Hand shaking을 통해 데이터를 전송하는 프로토콜에서 아래와 같은 스펙이 있다고 하자.

 

REQ가 발생한 후, 3 clock cycle 안에 ACK를 받아야 한다

 

이를 Assertion으로 명시하여 검증할 수 있다. 3 clock cycle 이후에 ACK가 발생하거나 아예 ACK가 발생하지 않는다면, Assertion failure로 간주하고 에러를 발생시킨다.

 

 

3 clock 안에 ACK가 발생하지 않으면 실패

 

 

Assertion의 장점은 합성할 때, Design compiler에서 해당 내용을 자동으로 무시하고 넘어간다는 것이다. 즉, 별도의 Embedded checker code가 필요하지 않다. 또한, Simulation 시, Assertion을 on/off 할 수 있기 때문에 Test code를 직접 RTL에 넣는 것보다 유연한 컨트롤이 가능하다. 

 

 

Assertion을 쓰지 않으면 조금 복잡해진다.

 

 

 

---

 

 

 

 

 

Assertion의 두 가지 종류

 

두 가지 타입의 Assertion이 있다. 

 

• Immediate assertion
• Concurrent assertion

처음에는 어떤 차이가 있는지 명확히 알지 못해서 사용할 때마다 혼동한 적이 많았다. 알고나면 굉장히 단순한데, 현재 시간에서 참/거짓을 판단하는지 아니면, clock과 동기화되어 순차적인 이벤트를 검사하는지에 따라 나뉜다. 

 

 

두 가지 타입의 Assertion 비교

 

Immediate assertion은 조건에 따라, 참/거짓만 판별하면 되므로 비교적 간단하지만 Concurrent assertion은 시간 정보를 담아야 하기 때문에 사용되는 문법이나 시스템 함수 등이 조금 많고 복잡하다. 이 포스팅에서 모든 것을 담기에는 양이 너무 방대해지므로, 맛보기 형식으로 간단히 다루고 넘어가려 한다. 각각의 문법을 자세하게 설명하는 것은 나중으로 미뤄두고, assertion 관련해서 유용한 링크 두 개를 글 후미에 남기도록 하겠다. (어물쩍 넘어가기...?)

 

Immediate assertion은 if...else 조건문과 유사하다고 했는데, 정말 그런지 아래 예시 코드를 살펴보자.

 

 

▼ Immediate assertion 예시 코드

 

 

State machine에서 각 state를 onehot형태로 구현했다고 치자. state가 4bit이라 했을 때, 0001, 0010, 0100, 1000 외에 어떠한 값도 올 수 없다. 만약 정해진 state를 벗어난 값이 입력되면, spec out이므로, error를 출력하고 simulation을 종료한다. 이러한 명제에는 시간 정보가 포함되어 있지 않다. 즉, 시간에 상관없이 값이 잘못된 순간 바로 Assertion failure가 된다. 

 

이와 반대로 Concurrent assertion은 시간 정보가 담겨 있다. 만약 동기화된 clock이 인가되지 않으면, 값이 잘못되더라도 Assertion code는 판단을 하지 않는다. 앞서 살펴봤던 Hand shaking case가 3 clock cycle이라는 시간 정보를 담고 있으므로, Concurrent assertion 케이스이며 코드는 다음과 같다.

 

 

▼ Concurrent assertion 예시 코드

 

data_clk의 rising edge에서 req가 입력되어야만 다음 구문의 진위를 판단한다. 

|->는 implication operator로 조건이 참일 때, 다음 sequence(순서)를 판단하라는 문법이다. 다음과 같이 두 가지 종류가 있으며, 경우에 따라 골라서 사용하면 된다. 

 

• |-> 현재 cycle을 포함한다. (overlapping)
• |=> 현재 cycle을 포함하지 않는다. (non-overlapping)

시간 정보를 나타내는 문법에는 여러 가지가 있지만, ##[min_count:max_count]는 조건이 참일 때, 다음 sequence를 판별하기까지의 clock cycle의 범위를 나타낸다. 

 

즉, 예시에서의 Assertion code는 data_clk에 동기화되어 req가 참일 때, 현재 cycle을 포함해서 1~3 cycle 안에 ack를 받아야 명제를 만족한다. 이를 지키지 않는 케이스는 spec out이며, error를 출력하고 종료한다.

 

 

 

---

 

 

 

 

 

이전 포스팅이었던 SRAM model 만들기에 몇 가지 assertion code를 넣어 무작정 따라 해 봤다. assertion은 심각도(severity)에 따라 $info, $warning, $error, $fatal의 4가지 로그를 출력할 수 있다. 앞의 두 가지는 simulation이 바로 종료되지 않는 반면, 뒤의 두 가지는 바로 종료된다.

 

 

▼ SRAM model에 포함된 assertion code

// Assertion
property WEnCheck;
  @(posedge clock) !WEn |-> !CSn;
endproperty
assert property (WEnCheck)
else $warning("[WEnCheck] Assertion failed!");
 
property AddrCheck;
    @(posedge clock) (addr <= AMAX);
endproperty
assert property (AddrCheck)
else $error("[AddrCheck] Assertion failed!");
 
property RdataCheck;
    @(posedge clock) (!CSn && !WEn) |=> !$isunknown(rdata);
endproperty
assert property(RdataCheck)
else $error("[RdataCheck] Assertion failed!");
 
 

(1) [WEnCheck] WEn이 low일 때, CSn이 high로 가도록 testbench를 수정하여, assertion fail test 진행

(2) [AddrCheck] sram의 max address를 넘는 값을 인가하여 assertion fail test 진행

(3) [RdataCheck] max address를 넘는 값을 인가하여 read 된 출력이 unknown이 나오도록 하여 assertion fail test 진행

 

 

▼ 임의로 testbench를 수정하여 assertion code 결과 확인

// case 1 result
xmsim: *W,ASRTST (./design.sv,38): (time 112500 PS) Assertion tb.sram.WEnCheck has failed      
[WEnCheck] Assertion failed!
 
// case 2 result
xmsim: *E,ASRTST (./design.sv,44): (time 142500 PS) Assertion tb.sram.AddrCheck has failed
[AddrCheck] Assertion failed!
 
// case 3 result
xmsim: *E,ASRTST (./design.sv,50): (time 147500 PS) Assertion tb.sram.RdataCheck has failed
[RdataCheck] Assertion failed!
 

 

 

맺음말

 

완성도를 높이기 위한 방법은 사람마다 다를 수 있다. 그러나 선택 옵션이 하나 더 있다고 해서 나쁠 것 없다. 선택적으로 필요할 때마다 꺼내 쓸 수 있는 무기는 많을수록 좋다고 생각한다.

 

법사라고 주문만 쓰라는 법 없다.

 

설계 엔지니어는 직접 본인의 design에 Assertion 코드를 삽입하여 사용하는 것이 좋고, 검증 엔지니어는 외부에 Assertion module을 만들고 binding 하여 사용하는 것을 추천한다고 한다. Assertion은 과도하게 사용하면 simulation time을 증가시키는 요인이 되기도 하지만, 적절하게 쓰기만 하면 설계 완성도를 높이는 효과적인 방법이 된다. 

 

망설이고 있는 설계자가 있다면 일단 해보는 것을 추천한다. 확실한건 Assertion을 사용하면서 실보다 득이 많다는 것이다. 이 글을 통해 Assertion으로 설계 검증에 날개를 다는 엔지니어들이 더욱 많아지길 빌며...

 

앞에서 설명한 assertion 관련 두 사이트를 남기며 이만 글을 줄인다. 

(좋은 내용이 많다. 본 포스팅의 예시도 해당 사이트의 글을 상당수 참조하였다.)

 

http://videos.accellera.org/systemverilog2016/sv16hm597gr9/index.html

Technical Tutorial: SVA Advanced Topics: SVAUnit and Assertions for Formal

http://staging.doulos.com/knowhow/systemverilog/systemverilog-tutorials/systemverilog-assertions-tutorial/

Doulos