형식적 동등성 검사

Formal equivalence checking

공식 등가성 검사 프로세스는 전자 설계 자동화(EDA)의 일부로, 디지털 집적회로의 개발 중에 일반적으로 사용되며 회로 설계의 두 표현이 정확히 동일한 동작을 나타낸다는 것을 공식적으로 증명합니다.

동등성 검사 및 추상화 수준

일반적으로, 다양한 추상화 수준과 다양한 타이밍 상세 입도 간의 비교를 포함하는 기능적 동등성에 대한 광범위한 가능한 정의가 있다.

  • 가장 일반적인 접근방식은 클럭마다 유효한 입력 신호의 시퀀스에 대해 정확하게 동일한 출력 신호를 생성하는 경우 기능적으로 동등한 2개의 동기 설계 사양을 정의하는 기계 동등성 문제를 고려하는 것입니다.
  • 마이크로프로세서 설계자는 명령어 세트 아키텍처(ISA)에 지정된 기능과 레지스터 전송 레벨(RTL) 구현을 비교하기 위해 동등성 체크를 사용합니다.이것에 의해, 양쪽 모델에서 실행되는 프로그램이, 메인 메모리 컨텐츠의 같은 갱신이 가능하게 됩니다.이것은 보다 일반적인 문제입니다.
  • 시스템 설계 흐름에서는 예를 들어 SystemC에 기술된 트랜잭션레벨 모델(TLM)과 대응하는 RTL 사양 간의 비교가 필요합니다.이러한 체크는 시스템 온 어 칩(SoC) 설계 환경에 대한 관심이 높아지고 있습니다.

동기식 기계 동등성

디지털 칩의 Register Transfer Level(RTL; 레지스터 전송 레벨) 동작은 보통 Verilog 또는 VHDL 등의 하드웨어 기술 언어로 기술됩니다.이 설명은 어떤 클럭 사이클 중에 어떤 작업이 수행되는지, 어떤 하드웨어에 의해 어떤 작업이 수행되는지 자세히 설명하는 골든 레퍼런스 모델입니다.일단 논리설계자가 시뮬레이션 및 다른 검증방법에 의해 레지스터 전송 기술을 검증하면, 그 설계는 보통 논리합성툴에 의해 넷리스트로 변환된다.동등성은 기능적 정확성과 혼동해서는 안 되며 기능적 검증에 의해 결정되어야 한다.

초기 넷리스트는 보통 최적화, Design For Test(DFT; 테스트 설계) 구조 추가 등 여러 가지 변환을 거쳐 논리 요소를 물리적 레이아웃에 배치하는 기준으로 사용됩니다.또, 현대의 물리 설계 소프트웨어에서는, 넷 리스트를 큰폭으로 수정하는 일이 있습니다(예를 들면, 논리 요소를 드라이브 강도나 면적이 높거나 낮은 동등한 유사 요소로 교체하는 등).매우 복잡한 다단계 절차의 모든 단계에서 원래 기능 및 원래 코드로 설명된 동작을 유지해야 합니다.최종 테이프 아웃이 디지털 칩으로 이루어지면 많은 다른 EDA 프로그램과 일부 수동 편집으로 인해 넷 리스트가 변경될 수 있습니다.

이론적으로, 논리 합성 도구는 첫 번째 넷리스트가 RTL 소스 코드와 논리적으로 동등함을 보증한다.netlist를 변경하는 프로세스의 후반부에 있는 모든 프로그램도 이론적으로는 이러한 변경이 이전 버전과 논리적으로 동등함을 보증합니다.

실제로 프로그램에는 버그가 있기 때문에 RTL에서 최종 테이프 아웃 넷 리스트에 이르기까지 모든 단계가 오류 없이 수행되었다고 가정하면 큰 위험이 있습니다.또, 설계자는, 일반적으로 Engineering Change Order(ECO)라고 불리는 넷 리스트를 수동으로 변경하는 것이 일반적이기 때문에, 주요한 에러 요인이 추가되고 있습니다.따라서 오류가 없다고 맹목적으로 가정하는 대신, 넷리스트의 최종 버전과 설계의 원래 기술(골든 레퍼런스 모델)의 논리적 동등성을 확인하는 검증 단계가 필요하다.

역사적으로 동등성을 확인하는 한 가지 방법은 최종 넷리스트를 사용하여 RTL의 정확성을 검증하기 위해 개발된 테스트 케이스를 다시 시뮬레이션하는 것이었습니다.이 프로세스를 게이트레벨 로직 시뮬레이션이라고 합니다.그러나 이 문제의 문제는 검사의 품질이 테스트 케이스의 품질만큼만 우수하다는 것입니다.또한 게이트 레벨 시뮬레이션은 실행 속도가 느리기로 악명이 높으며, 이는 디지털 설계의 크기가 기하급수적으로 계속 증가하고 있기 때문에 큰 문제입니다.

이것을 해결하는 다른 방법은, RTL 코드와 그것으로부터 합성된 넷 리스트가, 모든 (관련하는) 케이스에서 정확하게 같은 동작을 가지는 것을 정식으로 증명하는 것입니다.이 과정은 공식 동등성 검사라고 불리며, 공식 검증의 광범위한 영역에서 연구됩니다.

정식 등가성 체크는 설계의 임의의 2가지 표현(RTL <> netlist, netlist <> netlist 또는 RTL <> RTL) 간에 실행할 수 있습니다.단, 처음 두 가지 표현에 비해 RTL <> RTL은 거의 없습니다.일반적으로 공식 등가성 검사 도구는 두 표현 사이에 차이가 있는 지점을 매우 정확하게 나타냅니다.

방법들

동등성 검사 프로그램에서 부울 추론에 사용되는 두 가지 기본 기술이 있습니다.

  • 바이너리 결정 다이어그램(BDD): 부울 함수에 대한 추론을 지원하기 위해 설계된 특수 데이터 구조입니다.BDD는 효율성과 다재다능성 때문에 큰 인기를 끌고 있다.
  • 연결 정규 형식 만족도: SAT 해결사는 이러한 할당이 존재하는 경우 이를 충족하는 명제 공식의 변수에 할당을 반환합니다.거의 모든 부울 추론 문제는 SAT 문제로 표현될 수 있습니다.

동등성 검사를 위한 상용 응용 프로그램

EDA의 Logic Equivalence Checking(LEC) 영역의 주요 제품은 다음과 같습니다.

일반화

  • 리타이밍된 회선의 등가성 체크:레지스터의 한쪽에서 다른 쪽으로 로직을 이동하면 편리할 수 있으며, 이로 인해 체크 문제가 복잡해질 수 있습니다.
  • 순차 등가 검사:때때로 두 기계는 조합 수준에서 완전히 다르지만 동일한 입력이 주어진 경우 동일한 출력을 제공해야 합니다.일반적인 예는 상태에 대해 서로 다른 인코딩을 사용하는 두 개의 동일한 상태 머신입니다.이것은 조합의 문제로 환원할 수 없기 때문에, 보다 일반적인 기술이 필요합니다.
  • 소프트웨어 프로그램의 동등성, 즉 N개의 입력을 받아 M개의 출력을 생성하는 두 개의 잘 정의된 프로그램이 동일한지 확인합니다.개념적으로 소프트웨어를 스테이트 머신으로 만들 수 있습니다(컴퓨터와 메모리를 조합하면 매우 큰 스테이트 머신이 되기 때문에 컴파일러의 조합이 그렇게 됩니다).그러면 이론적으로 다양한 형태의 특성 검사를 통해 동일한 결과를 얻을 수 있습니다.이 문제는 두 프로그램의 출력이 서로 다른 시간에 나타날 수 있기 때문에 순차적 동등성 검사보다 훨씬 더 어렵습니다. 하지만 가능합니다. 그리고 연구자들은 이 문제를 연구하고 있습니다.

「 」를 참조해 주세요.

레퍼런스

  • Lavagno, Martin 및 Scheffer의 집적회로를 위한 전자 설계 자동화 핸드북 ISBN0-8493-3096-3 현장조사.이 기사는 Fabio Somenzi와 Andreas Kuehlmann에 의해 제2권 제4장 등가 검사에서 인용되었다.
  • R.E. Bryant, 부울 함수 조작을 위한 그래프 기반 알고리즘, IEEE Transactions on Computers., C-35, 페이지 677–691, 1986.BDD의 원래 참조.
  • RTL 모델에 대한 순차적 동등성 검사.Nikhil Sharma, Gagan Rusher, Venkat Krishnaswamy.EE 타임즈

외부 링크