등가성 검사 란 무엇인가요?

등가성 검사 에는 세 가지 기본 단계가 있습니다:

1. 설정
2. 매핑
3. 비교하기

설정 단계의 입력 자료로는 검증된 참조 설계, 라이브러리 요소 및 수정된 설계가 포함됩니다. 이 단계에서는 입력 자료를 불러오고, 후속 단계를 원활하게 진행하기 위해 데이터 구조를 생성합니다.

매핑 단계에서는 설계의 주요 지점을 매핑하고 비교합니다. 비교 지점을 구성하는 데는 일반적으로 로직 콘이 사용됩니다. 로직 콘은 비교 지점을 구동하는 조합 논리 블록입니다. 로직 콘의 입력에는 레지스터 출력 핀, 1차 입력 포트 및 블랙박스 출력 핀이 포함됩니다. 비교 지점에는 레지스터, 1차 출력 포트 및 블랙박스 입력 핀이 포함됩니다.

비교 과정에서 매핑된 주요 지점들을 검토하여, 해당 지점들이 동등한지, 비동등한지, 아니면 반전된 동등한지 여부를 판단합니다. 결론이 나지 않은 결과를 반환하는 설계 부분은 해결을 위해 더 많은 노력을 들여 다시 실행할 수 있습니다.

아래 그림은 그 과정을 보여줍니다:

등가성 검사 이는 어떤 설계 워크플로우에도 강력한 보완 기능을 제공합니다. 형식적 방법을 적용하여 설계의 일관성을 검증할 수 있는 능력은 테스트 벤치의 완전성에 좌우되지 않는 결과물의 품질에 대한 통찰력을 제공합니다. 구체적인 이점은 다음과 같습니다:

• 효율성 향상.속도가 느린 게이트 레벨 시뮬레이션에 대한 의존도 감소.
• 신뢰도가 높아집니다.툴 체인이나 ECO로 인해 미묘한 오류가 발생했을 것이라는 우려가 줄어듭니다.
• 더 높은 품질.이 기법을 사용하면 설계에서 부실한 RTL 코딩을 파악할 수 있습니다.
• 예측 가능성이 더 높습니다.버그를 놓칠 가능성이 줄어듭니다.

논리 등가성 검사( 등가성 검사 , LEC)는 설계의 조합 논리 구조를 분석하여, 두 가지 대안 구현 방식의 구조가 동일한 동작을 보일지 여부를 판단합니다. 리타이밍과 같은 작업이 설계에 적용될 경우, 두 표현 방식 간의 설계 구조는 더 이상 대응 관계를 이루지 않게 됩니다.

시퀀스 동등성 검사(SEC)는 타이밍을 고려하여 여러 클럭 사이클에 걸쳐 두 설계 표현 간의 동등성을 검토합니다.

Synopsys 제안 Formality 등가성 검사 두 버전의 설계가 기능적으로 동등한지 판단하기 위해 형식적 및 정적 기법을 사용하는 방법입니다.