반도체를 설계할 때, 처음 기획한 의도한 대로 동작하는지를 확인하는 '검증'은 매우 중요합니다. 검증 과정을 잘 거쳐야 높은 품질의 반도체를 만들 수 있습니다. 다만 설계 디자인이 전보다 복잡해지고 어려워지면서 검증 방법의 난도도 크게 올라가고 있습니다. 칩 하나에 다양한 기능 블록을 넣은 시스템온칩(SoC) 같은 제품이 늘어나면서 부터입니다. 이 때문에 과거에는 설계 마지막 단에서 검증을 했지만, 최근에는 설계 중간 중간마다 수시로 검증을 하는 방식을 많이 씁니다.  지금까지 설계단에서 많이 사용되던 검증 방식은 '시뮬레이션 기반 검증'입니다. 시뮬레이션 기반 검증은 각각 기능을 구현할 시뮬레이션 환경을 만든 다음 그에 맞는 벤치테스트(benchtest)를 별도로 구현해서 검증하는 것입니다. 이 경우 시간이 오래 걸립니다. 엔지니어는 개발 마감 기간을 맞추기 위해 디자인 설계의 모든 케이스 검증을 수행하지 못한 채 다음 단계인 백엔드(back-end)로 넘기는 일도 있습니다. 문제가 있는지 없는지 모르고 넘어갈 수 있다는 것이지요. 이러한 시뮬레이션 기반 검증의 단점을 보완하기 위해 '형식(Formal) 검증'이 등장했습니다. 형식 검증은 전체를 한꺼번에 수학적인 방법으로 정확하게 검증 진단해 줍니다. 엔지니어의 실수로 인해 발생한 문제까지도 발견할 수 있습니다. 무엇보다도 설계 검증 시간이 짧기 때문에 전체 개발 기간을 단축시킬 수 있습니다. 시뮬레이션 기반 검증 기간이 2~3주 또는 한달이 걸렸다면, 형식 검증은 하루 또는 며칠 만에 해결할 수 있습니다. 두개의 검증 방식을 건축에 비유해서 설명하겠습니다. 건물을 짓기 전에 설계도를 그립니다. 그 다음 설계도를 바탕으로 건물에 들어가는 철근 또는 기둥이 몇 키로그램(kg)까지 버틸 수 있는지, 각각을 테스트하는 것이 '시뮬레이션 기반 검증'입니다. 반면 '형식 검증'은 수학적으로 골격을 분석해서 한번에 계산할 수 있는 방식이라고 생각하면 됩니다. 설계도를 검증한 후에는 땅을 파고, 철근을 심고, 콘크리트를 쌓아서 건물을 짓습니다. 이 과정이 백엔드입니다. 형식 검증을 처음 접하는 사용자라면 다소 어려울 수 있습니다. 사용자가 직접 검증하고자 하는 기능을 프로퍼티(사용자의 설정 정보)로 기술해야 하기 때문입니다. 이 때 '형식 검증 앱'을 사용하면 편하게, 검증 소요시간을 단축할 수 있습니다. 각각의 애플리케이션이 목적으로 하는 검증 타겟에 대한 속성을 툴이 자동으로 기술해주기 때문입니다.  멘토, 지멘스 비즈니스는 퀘스타(Questa) 형식 검증 앱을 제공하고 있습니다. 퀘스타 형식 검증 앱의 종류는 ▲오토체크(Autocheck) ▲커버체크(Covercheck) ▲엑스체크(Xcheck) ▲SLEC ▲커넥트체크(Connectcheck) ▲레지스터체크(Registercheck) ▲시큐어체크(Securechec) 등이 있습니다.  오토체크는 일반적으로 흔히 발생하는 버그를 검출하는 체커입니다. 커버체크는 커버리지를 빠르게 100% 까지 도달할 수 있도록 돕습니다. 엑스체크는 디자인에서 발생하는 X값 전파(Propagation)의 원인을 찾아줍니다. SLEC은 기능적 동일성 검증입니다. 커넥트체크는 연결 검증에 사용됩니다. 레지스터체크는 레지스터의 값과 속성이 의도한 대로 기술되었는지 검증합니다. 시큐어체크는 보안키가 유출될 수 있는지 여부를 검증합니다.  디일렉은 오는 9월 15일(화) 오전 10시 30분에 '형식검증을 이용한 품질 및 타임투마켓 개선' 웨비나 안내'라는 주제로 웨비나를 실시합니다. 글로벌 반도체 전자설계자동화툴(EDA) 업체인 멘토, 지멘스 비즈니스의 전문 엔지니어가 강의할 예정입니다. 웨비나에서는 형식 검증 앱의 사용법과 이를 통해 유효한 결과를 제공하는 방법을 소개합니다. 또 발생 가능한 모든 설계 오류를 철저하게 찾아내는 방법도 공유합니다. 설계 엔지니어, 검증 엔지니어 등에게 도움이 될 것으로 기대합니다. 

- 웨비나 개요 -

웨비나명 : 형식검증을 이용한 품질 및 타임투마켓 개선 
일시 : 9월 15일 오전 10시 30분
장소 : 디일렉 웨비나 사이트(webinar.bestwatersport.com)
등록 비용 : 무료

- 프로그램 - 

시간	주제
10:30~11:00	1부 자동화된 형식검증 기반 앱 ·복잡한 로직 안에 깊이 숨어 있는 버그를 찾아내고 교착 상태를 방지하는 방법(UVM 테스트벤치가 제공되기 훨씬 전에!) ·데드 코드 분석을 통한 코드 커버리지 클로저 가속화 ·레지스터 정책 코너 케이스를 찾아내는 방법 ·모든 SoC 및 패드 링의 직접, 조건부 및 순차적 연결이 정확한 지 확인하는 방법 ·중요한 보안/안전 스토리지로 들어가는, 의도하지 않은(또는 악의적으로 추가된) 백도어 또는 “잠복 경로”를 찾아내는 방법 ·저전력이나 포스트 리셋 브링업 또는 X-옵티미즘(X-optimism)으로 인한 ‘X’ 전파가 초래하는 불규칙한 고장에 대한 근본 원인 분석 ·저전력 클럭 게이팅 로직, 뒤늦은 ECO나 버그 수정 또는 결함/SEU 완화 로직의 검증
11:00~11:30	2부 직접적인 형식 속성 검사 ·형식 분석의 작동 방식과 이것이 모든 입력과 시간에 대해 유효한 완전한 결과를 제공하는 방법 ·효과적인 “형식 테스트벤치”를 매우 기본적이고 작성하기 쉬운 속성을 이용해 개발하는 방법 ·일반적인 형식 검증 방법론 소개: 버그 헌팅, 중요한 DUT 기능의 정확성 완전 입증, 교착 상태의 부재 증명

-연사 소개-

마크 에슬링어 

칩 설계 및 검증, 판매 사전/사후 지원, 기술 마케팅 분야에서 20년 이상의 경력을 갖춘 멘토 그래픽스 설계검증 기술 부문의 기술 마케팅 전문가. 특히 어서션 기반의 방법과 형식 검증 분야에 관심을 갖고 있으며, 전 세계 고객들의 첨단 방법론 채택을 돕고 있다. 멘토에 합류하기 전에는 반도체, 시스템 및 EDA 산업 분야의 엔지니어링 및 기술 마케팅 업체인 록히드, 시높시스(Synopsys), 앱스트랙트(Abstract), Sente/Sequence, 애버란트(Averant), 액셀칩(AccelChip) 등의 여러 직위를 두루 거쳤다. 산타 클라라 대학에서 전기공학 석사(MSEE) 학위를 받았다.

조 헙시 

멘토의 설계 및 검증 기술 부문 제품관리 팀의 일원으로서, 캘리포니아 주 실리콘밸리에 소재한 멘토 사무소에서 일하고 있다. Questa Formal 제품군의 자동화 애플리케이션 및 고급 속성 점검 분야를 담당하고 있다. 멘토에 합류하기 전에는 여러 전자 설계 자동화(EDA) 업체의 제품 관리 및 마케팅 직책에서 하드웨어 및 소프트웨어 기능 검증의 여러 측면을 망라하는 제품들을 섭렵했다. 마케팅 분야로 옮기기 전에는 FPGA 설계, FPGA 및 ASIC용의 EDA 툴, ASIC 검증 부문의 전기 엔지니어로 일했다. 뉴욕주 이타카 소재의 코넬 대학교에서 전기공학 학사(BSEE), 전기공학 석사(MSEE) 및 경영학 석사(MBA) 학위를 받았다.