공식적인 마음 들것에 대한 인텔 기조연설

플라톤에 의해 재발행

팔로워 : 0

Synopsys는 Intel Graphics의 Theo Drane 박사가 진행한 흥미로운 강연을 SolvNet 사이트에 게시했습니다. 주제는 데이터 경로 동등성 검사입니다. 또 다른 Synopsys VC 공식 DPV 보증처럼 들릴 수도 있지만 어쨌든 시청해야 합니다. 이것은 일상적인 사용자 가이드 유형의 피치를 넘어 더 흥미로운 영역으로 여러분을 안내할 공식적인 사용 및 고려 사항에 대한 마음을 넓히는 토론입니다.

인텔 공식 기조연설

지적 이해와 샘플 테스트

모든 형태의 테스트 기반 시뮬레이션은 설계 사양이나 구현의 정확성을 검증하는 데 탁월하며 대체할 수 없는 경우가 많습니다. 시작하는 것도 쉽습니다. 테스트 프로그램을 작성하고 시뮬레이션을 시작하면 됩니다. 하지만 그 단순함의 이면은 우리가 그럴 필요가 없다는 것입니다. 충분히 시작하기 위해 무엇을 테스트하고 있는지 이해하세요. 우리는 사양을 주의 깊게 읽고 모든 특수 사례를 이해했다고 스스로 확신하지만, 우리의 이해를 압도하기 위해 복잡한 복잡성이 필요하지는 않습니다.

Formal은 (적어도 가치 있는 결과를 제공하려는 경우) 심층적인 수준에서 기능을 이해하도록 권장합니다. 위의 예에서 간단한 질문(z가 모두 1이 될 수 있습니까?)은 시뮬레이터에서 188억 주기의 예를 보여주지 못합니다. 이는 극단적인 경우이기 때문에 놀라운 일은 아닙니다. 공식 테스트는 XNUMX초 안에 구체적이고 매우 명확하지 않은 예를 제공하며 이것이 약간 더 짧은 시간 내에 유일한 사례임을 증명할 수 있습니다.

OK 형식은 동적 테스트가 할 수 없는 일을 해냈지만 더 중요한 것은 시뮬레이터가 결코 말하지 않았을 수도 있는 것을 배웠다는 것입니다. 그런 상황이 일어날 수 있는 경우는 딱 한 가지뿐이었다. Formal은 유한한 테스트 케이스 세트에 대한 확률적 요약이 아닌 지적 수준에서 디자인을 더 잘 이해하는 데 도움이 되었습니다.

사양 문제

Theo의 다음 예는 버그 자동 판매기를 기반으로 합니다(버튼을 누르면 버그가 발생하기 때문에 소위 불림). 이는 매우 간단한 C 대 RTL 동등성 확인 문제처럼 보입니다. 왼쪽은 C 모델, 오른쪽은 RTL 모델입니다. 공식 분야 초기에 Theo가 놀랐던 점 중 하나는 gcc가 합리적으로 작동하더라도 C 모델의 오른쪽 시프트 동작이 C 표준에서 완전히 정의되지 않았다는 것입니다. 그러나 DPV는 RTL과의 비교에서 불일치에 대해 불평할 것입니다. 정의되지 않은 동작은 의존하기 위험한 것입니다.

벌레 자판기로 정식

C와 RTL 간의 사양 비교에는 특히 비트 폭과 관련된 다른 위험이 있습니다. 중간 신호(위의 #3)에서 캐리 비트의 잘림이나 손실이 좋은 예입니다. 이게 사양 문제인가요? 사양과 구현 선택 사이의 회색 영역일 수도 있습니다.

동등성 검사를 넘어

DPV의 주요 목적은 C 또는 RTL 참조와 RTL 구현 간의 동등성을 확인하는 것 같습니다. 그러나 그러한 필요성은 상대적으로 드물며, 약간만 벗어나면 그러한 기술을 적용할 수 있는 다른 유용한 방법이 있습니다. 첫 번째는 구현 세계의 고전입니다. 변경하고 버그를 수정했습니다. 결과적으로 새로운 버그가 생겼습니까? 클럭 게이팅을 추가한 후 SEQ를 확인하는 것과 비슷합니다. 블록 출력의 도달 가능성 분석은 경우에 따라 또 다른 유용한 애플리케이션이 될 수 있습니다.

단순히 동등성 검사가 아닌

테오는 더욱 창의적이 되어 훈련생들에게 디자인을 더 잘 이해하기 위해 반대 사례를 사용하도록 요청하고, 스도쿠 풀기 or 정수 인수분해. 그는 DPV가 그러한 문제에 접근하는 이상한 방법이라는 것을 인정하지만 그의 의도는 DPV가 동등성 확인에만 사용된다는 환상을 깨는 것임을 지적합니다. 흥미로운 아이디어이며 그러한 도전을 통해 생각하는 것은 확실히 두뇌 확장입니다. (그가 스도쿠 문제를 언급하자마자 나는 즉시 스도쿠 문제에 대해 생각하기 시작했다고 고백합니다.)