형식검증을 이용한 품질 및 타임투마켓 개선

0

2020년 9월 15일 (화)

품절

카테고리: 태그:

설명

1부 — 자동화된 형식검증 기반 앱
·동적 연결 검증, 레지스터 정책 검증 또는 중요한 신호 경로 및 레지스터의 무결성 확인과 같은 수많은 고가치 검증 작업에는 수 주일 또는 수 개월간의 테스트벤치 개발 및 실행이 필요합니다. 그럼에도 불구하고 예상치 못한 모든 코너 케이스를 밝혀내지는 못합니다. 이와는 대조적으로, 형식 기반 검증은 애플리케이션을 통해 이러한 문제를 철저하게 검증할 수 있습니다.

 

이러한 “앱”은 사실상 형식 분석의 내부 작동 방식에 대해 알 필요가 없을 정도로 자동화되어 있으면서도 필요한 모든 결과를 제공합니다. Questa Formal이 제공하는 일련의 강력한 자동화 앱은 설계 단계 초기부터 검증 프로세스 전반에 적용되어 찾아내기 힘든 코너 케이스를 검증 프로세스 초기에 확인함으로써 이를 보다 손쉽고 저렴하게 수정할 수 있습니다. 본 웹 세미나에서는 형식 검증 앱이 다음과 같은 고가치 검증 문제의 해결을 어떻게 도와줄 수 있는 지 보여드립니다.

 

강의 내용
·복잡한 로직 안에 깊이 숨어 있는 버그를 찾아내고 교착 상태를 방지하는 방법(UVM 테스트벤치가 제공되기 훨씬 전에!)
·데드 코드 분석을 통한 코드 커버리지 클로저 가속화
·레지스터 정책 코너 케이스를 찾아내는 방법
·모든 SoC 및 패드 링의 직접, 조건부 및 순차적 연결이 정확한 지 확인하는 방법
·중요한 보안/안전 스토리지로 들어가는, 의도하지 않은(또는 악의적으로 추가된) 백도어 또는 “잠복 경로”를 찾아내는 방법
·저전력이나 포스트 리셋 브링업 또는 X-옵티미즘(X-optimism)으로 인한 ‘X’ 전파가 초래하는 불규칙한 고장에 대한 근본 원인 분석
·저전력 클럭 게이팅 로직, 뒤늦은 ECO나 버그 수정 또는 결함/SEU 완화 로직의 검증

 

2부 — 직접적인 형식 속성 검사
·잘 작성된 제약조건 랜덤 테스트벤치로도 설계 상태 공간의 모든 부분을 망라할 수는 없습니다. 시뮬레이션 기반 검증은 근본적으로 불완전하여 소규모 DUT용으로도 미흡한 것이 현실입니다. 또한, 시뮬레이션 테스트벤치가 작성되기까지는 수 주일이 걸릴 수 있으므로, 그 사이에 IP 작성에서 복잡한 버그가 발생할 수 있습니다. 따라서 주어진 버그가 낡거나 잘못 안 사양 때문이든 또는 근본적인 설계 결함 때문이든, 이를 모르고 방치하는 기간이 길어질수록 이를 찾아내 수정하는 비용은 물론, 수정 작업을 통해 버그가 수정되었을 뿐만 아니라 원치 않는 부작용도 야기되지 않음을 철저히 검증하는 데 드는 비용도 더 커집니다.

 

본 웨비나에서는 형식 속성 점검을 통해, 다른 방법이 제공되기 훨씬 전에 고가치 검증을 수행하여 발생 가능한 모든 설계 오류를 철저하게 찾아내는 방법을 보여드립니다(게다가 특정 스티뮬러스도 필요 없습니다!).

 

강의 내용
·형식 분석의 작동 방식과 이것이 모든 입력과 시간에 대해 유효한 완전한 결과를 제공하는 방법
·효과적인 “형식 테스트벤치”를 매우 기본적이고 작성하기 쉬운 속성을 이용해 개발하는 방법
·일반적인 형식 검증 방법론 소개: 버그 헌팅, 중요한 DUT 기능의 정확성 완전 입증, 교착 상태의 부재 증명

 

대상 제품
·Questa® AutoCheck
·Questa® Connectivity Check
·Questa® CoverCheck
·Questa® Formal Assertion Library
·Questa® Post Silicon Debug
·Questa® PropCheck
·Questa® Register Check
·Questa® Secure Check
·Questa® X-Check

 

참여 대상자
·설계 및 검증 엔지니어와 매니저

– 세션 소개 –

2020년 9월 15일 (화)

시간주제자료다시보기
10:30~11:40

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

10:30~11:40

2부 직접적인 형식 속성 검사
·형식 분석의 작동 방식과 이것이 모든 입력과 시간에 대해 유효한 완전한 결과를 제공하는 방법
·효과적인 “형식 테스트벤치”를 매우 기본적이고 작성하기 쉬운 속성을 이용해 개발하는 방법
·일반적인 형식 검증 방법론 소개: 버그 헌팅, 중요한 DUT 기능의 정확성 완전 입증, 교착 상태의 부재 증명

– 연사 소개 –

프로필소개

마크 에슬링어 | Mentor

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

조 헙시 | Mentor

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