새로운 홈플러그 브로드밴드(HomePlug Broadband) 전력선 네트워킹 SoC(System-on-a-chip)는 일반 전력선으로 네트워킹할 수 있도록 설계되어 무선 네트워크가 도달할 수 없는 장소까지 인터넷을 확장한다. 하지만 이 제품은 과도한 스케줄 및 고비용 문제가 일어날 수 있어 차별화된 성능 개발과 기성제품의 표준 IP 및 인터페이스, 수많은 주변장치의 이용 사이에 균형을 유지해야 한다. 이 글에서는 ‘최상의 도구들’을 이용하여 균형을 유지할 수 있었던 사례를 소개한다.

서론

무선 네트워킹은 편리하지만 작동할 때만 그 가치를 인정받는다. 누구나 한 번쯤 무선 네트워크 접속에 문제가 있어서 짜증이 났던 경험이 있을 것이다. 우리는 시야를 넓혀서 형식 분석 ‘앱’과 시뮬레이션 및 어셔션(assertion) 기반의 검증 IP를 혼합하여 더욱 완벽한 결과를 빠르고 효율적으로 달성하고자 했다. 다시 말해 검증 작업마다 알맞은 기술이 따로 있다고 본 것이다. 예를 들어 컨스트레인 랜덤 시뮬레이션(constrained random simulation)은 패킷 트래픽 구동 및 입력 ‘잡음(noise)’에 대한 강건성 인증에 적합하지만, 형식 분석(formal analysis)은 복잡한 로직과 IP 커넥티비티에 대한 철저한 분석(exhaustive analysis)에 적합하다. 
 

피검소자

홈플러그(HomePlug) 플랫폼은 유연한 전력선 네트워킹 SoC로 홈플러그 AV, 1.0, GP PHY, MAC 레이어를 구현하는 고성능 프로그래머블 전력선 모뎀과 완전통합형 아날로그 프론트엔드 및 광범위한 온칩 주변장치 세트를 갖춘 ARM9 CPU가 결합되어 있다. 그 다양한 기능들은 검증 엔지니어에게 큰 부담을 줄 수 있다. 이유는 고객들이 정교하게 수위를 다양화한 39개의 주변장치를 수천 개의 운용 사례에 적용할 수 있기 때문이다.  그림1은 부품 데이터 시트의 일부이다.

IP 커넥티비티 검증

첫 번째 과제는 부품 구성의 IP와 주변장치들 간의 기본적인 커넥티비티를 검증하는 것이다. 어렵지 않아 보일 수 있지만, SoC에는 여러 가지 저전력, BIST 및 기타 구성 모드가 존재하여 고객의 요청에 의한 맞춤화 작업이 포함되기도 전에 제어 신호와 데이터 경로에 영향을 미치거나 다중화한다. 이러한 요소들을 고려한다면 백 퍼센트 정확도로 검증해야 하는 연결들이 수만 개에 달하며 이는 아무리 체계적인 사람이라도 수작업으로는 검사할 수 없다.

우리도 처음에는 세부적인 수작업 검사와 C 기반의 시뮬레이션 테스트벤치 및 파형 분석에 의존해 이러한 커넥티비티를 간접적으로 검증했다. 이 방식은 우리의 테스트 계획상에서 본다면 다른 각본 및 사례들에서 얻은 부산물을 적용하는 것이었다. 하지만 얼마 지나지 않아 이 방법이 과거에는 통했지만, 주변장치 수가 매우 많은 차세대 설계에는 더욱 철저한 방법이 필요하다는 결론을 내렸다.

자연히 형식 분석을 검토하게 됐고 우리의 형식 분석 툴에서 구동되는 ‘SoC 커넥티비티 앱’ 형태의 솔루션(Cadenceⓡ Incisiveⓡ Formal Verifier)을 찾을 수 있었다. 더욱 구체적으로 이 앱은 평문 형식의 액셀 스프레드시트를 이용하여 커넥티비티 사양을 캡처한다. 그다음에는 상응하는 어서션을 자동 생성하고 형식 분석 툴을 실행하여 어서션 패일(failure)의 반례(counter examples)를 통해 모든 오류를 명확하게 집어낼 수 있다.

예전에는 시뮬레이션 기반의 프로세서를 통해 수 주일이나 걸렸다면 이제는 이 Soc 커넥티비티 앱을 이용함으로써 IP의 새로운 구성을 몇 시간 만에 신속하게 검증할 수 있게 됐다. 검증을 통해 UART 블록의 TX 및 RX 라인에 잘못된 연결이 있음을 발견했다. 하나는 TX에, 다른 하나는 RX에 연결되어야 할 포트들이 같은 GPIO에 잘못 연결되어 있었던 것이다. 이러한 버그는 UART가 루프백으로 연결되어 있던 펑셔널 시뮬레이션(functional simulation)에서는 발견되지 않았던 것이다.

AMBA 프로토콜 검증

ARM AMBA 버스는 우리 칩의 중심 동맥과 같다. 주변장치의 수가 증가하면 AMBA 구현 시의 복잡성도 함께 증가했다. 더구나 내부 버스에 연결하던 IP 중 일부는 고객에게 애플리케이션 옵션을 다양하게 제공하기 위해 구동 모드와 저전력 모드를 다수 갖춰 그 자체가 매우 복잡했다. 프로젝트를 관리하는 측면에서 본다면 표준형, 차별화되지 않은 버스와 부품에 드는 시간을 줄인다는 것은 고품질의 차별화된 IP 개발에 더 많은 시간을 투자할 수 있다는 것을 의미했다.

이 때문에 SoC 커넥티비티 앱을 통한 철저한 형식 분석에서 얻은 긍정적인 경험을 토대로 AMBA 프로토콜에 어서션 기반의 검증 IP(ABVIP)를 사용해 보기로 했다. 요약하면 AMBA 프로토콜 룰을 SVA/PSL 어서션의 라이브러리가 캡처하기 때문에 형식/동적 시뮬레이션 툴이 AMBA 버스 상의 우리 IP 앞부분에서 발생하는 모든 오류를 검증할 수 있는 것이다.

또한 가지 분명히 해 둘 것은 AHB 마스터 인터페이스 검증을 위해 형식 분석을 사용한 것은 마스터 포트 검증에서 형식 분석 방식이 잘 알려졌고 확실한 강점 분야이기 때문이다. 이를 설명하기 위한 특정 예시를 들어본다.

우리 칩의 일부 주변장치는 공통의 슬레이브 인터페이스 외에도 AMBA 마스터 인터페이스를 갖추고 있다. 검증 문제를 더욱 까다롭게 만드는 것은 이러한 마스터들에 DMA 컨트롤러가 두 개 이상 내장할 수 있다는 점이다. 그림 2는 검증된 AHB 마스터 인터페이스의 간략한 블록도이다. AHB 트랜잭션을 생성할 수 있는 세 개의 FSM으로 구성되는데, 이 트랜잭션은 AHB 슬레이브 인터페이스를 통해 접근할 수 있는 레지스터들로 설정할 수 있다. 이 블록도는 전체 IP로부터 추출됐으며 일부 설정은 assume 구성체를 통해 제약을 받는다.

앞서 언급했듯 수많은 슬레이브 주변 장치들이 임의의 주어진 파생 제품의 버스에 추가되어 있다. 놀랍게도 ABVIP로 형식 분석을 수행하자 가장 발달한 주변장치들에 여러 개의 버그를 발견할 수 있었다. 이 IP는 전에 시뮬레이션을 거친 바 있으며 다른 설계에서도 널리 사용됐다. 프로젝트가 진행되는 동안에 우리는 7건의 AMBA 프로토콜 위배사항을 발견했다. 사실 이 버그 중 일부는 AMBA 프로토콜이 강력해서 그 영향이 최소화되어 큰 문제로 보이진 않지만 다른 버그들은 완성 제품(들)에서 문제를 일으켰을 수 있는 ‘필수 수정대상’ 버그들이었다.

요약

이전의 시뮬레이션 기반 기법들에 비교하여 익숙한 ‘앱’과 검증 IP 프레임워크의 형식 분석 기술을 활용하여 복잡한 피검소자를 더욱 짧은 시간 내에 더욱 철저하게 검증할 수 있었으며 고품질의 결과를 얻었다. 우리는 이 방법론을 이용한 첫 프로젝트의 성공 이래 이 같은 플로우를 이용해 여러 제품을 성공적으로 측정했으며 실리콘 검증 결과도 완벽했다. 전반적인 팀의 처리량 향상에도 이바지했으며 모든 제품의 비용 및 위험성을 크게 줄여줬다.