RTL2GDS: Logical Equivalance Check, LEC

RTL이 Tape-out 될 때까지 정말 많은 EDA Tool을 거칩니다. 이 과정에 Bug가 한 번도 없을까요? Tool이 버그로 Inverter 하나를 더 추가했다면 어떻게 될까요?

Formal Verification, 그중에서도 Logic Equivalence Checking, LEC은 현대 ASIC 설계 흐름에서 꼭 필요한 방법론입니다.

LEC는 시뮬레이션과 달리 테스트 벡터를 사용하지 않는다. 대신, 두 가지 Design Representation이 수학적으로, 그리고 논리적으로 모든 경우의 수에서 동일한 동작을 수행한다는 것을 Static Analysis하는 방법론이다.

LEC의 주된 목적은 설계 변환 과정에서의 Integrity 확인이다. RTL(Register Transfer Level) 코드가 Logic Synthesis을 거쳐 Gate-level Netlist로 변환될 때, 또는 P&R 툴이 타이밍 최적화를 위해 로직을 수정할 때, 그리고 DFT(Design for Testability) 과정에서 스캔 체인이 삽입될 때, 원래 설계자의 의도(Golden Design)가 변형된 설계(Revised Design)에서도 완벽하게 보존되었는지를 확인하는 것이다.

위의 도표에서 볼 수 있듯이, LEC는 RTL 대 합성 넷리스트(RTL s Netlist), 합성 넷리스트 대 DFT 넷리스트(Netlist vs Netlist), 그리고 최종 레이아웃 넷리스트 검증 등 다양한 단계에서 반복적으로 수행된다.

이는 각 단계에서 발생할 수 있는 툴의 버그나 사용자의 실수로 인한 논리적 결함을 즉시 포착하여, 값비싼 Re-spin Cost를 방지하는 안전장치 역할을 한다.

2. 형식 검증의 수학적 및 알고리즘적 기초

LEC가 "수학적으로 증명한다"는 말의 의미를 이해하기 위해서는 그 기저에 깔린 알고리즘적 원리를 살펴보아야 한다. LEC 툴은 크게 Binary Decision Diagrams, (BDD)과 Boolean Satisfiability, (SAT)라는 두 가지 핵심 기술을 기반으로 동작한다.

2.1 Miter 회로 구성과 Refutation 기반 검증

LEC의 기본 원리는 두 회로(Reference와 Test)를 비교하여 출력이 다른 경우가 '단 하나라도' 존재하는지를 찾는 것이다. 이를 위해 툴은 가상의 Miter 회로를 구성한다. Miter 회로는 두 회로의 동일한 입력 포트를 서로 묶고, 대응되는 출력 포트를 XOR 게이트로 연결한 구조다.

논리적으로 XOR 게이트는 두 입력이 다를 때만 '1'을 출력한다. 따라서 LEC 툴의 목표는 "XOR 게이트의 출력이 1이 되는 입력 조합이 존재하는가?"라는 질문에 답하는 것으로 귀결된다.

• 만약 그러한 입력 조합(반례, Counter-example)이 존재한다면, 두 회로는 Non-equivalent이다.
• 만약 모든 가능한 입력에 대해 XOR 출력이 항상 '0'이라면, 두 회로는 Equivalent이다.

이 접근 방식은 "동일함을 증명"하는 것보다 "다름을 찾아내는 것"이 알고리즘적으로 더 효율적일 수 있다는 반증법적 사고에 기반한다.

2.2 Binary Decision Diagrams, BDD

초기 LEC 툴의 근간이 되었던 BDD는 Boolean을 DAG 형태로 표현하는 자료 구조다. BDD의 가장 강력한 특징은 Canonical Form이라는 점이다.

Canonical Form이란 논리함수를 입력 조합 기준으로 완전히 풀어 쓴 표준 표현이다. 그 뜻은 특정 논리 함수에 대해 Variable Ordering이 고정되어 있다면, 그 함수를 표현하는 BDD 그래프의 모양은 유일하다는 것을 의미한다. 이는 검증 과정을 획기적으로 단순화한다.

Golden Circuit과 Revised Circuit의 BDD를 각각 생성한 뒤, 두 그래프가 메모리 상에서 동일한 구조를 가지는지(즉, Root Node에서 Terminal Node까지의 경로가 일치하는지)를 포인터 비교만으로 확인할 수 있기 때문이다.

그러나 BDD는 치명적인 약점을 가지고 있다. 바로 Memory Explosion 문제다. Multiplier와 같은 특정 산술 연산 회로나 Input Variable이 많은 복잡한 Logic의 경우, BDD의 Node 수가 지수적으로 증가하여 물리적 메모리 한계를 초과하게 된다. 이로 인해 BDD 기반 검증은 대규모 SoC 설계 전체를 처리하는 데 한계를 보였다.

2.3 Satisfiability (SAT) Solver

BDD의 한계를 극복하기 위해 도입된 기술이 SAT Solver다. SAT는 주어진 Boolean 식(주로 CNF, Conjunctive Normal Form)을 True로 만드는 Variable Assignment가 존재하는지를 탐색하는 알고리즘이다.

LEC 관점에서 SAT Solver는 Miter 회로의 출력(XOR)이 '1'이 되도록 하는 Input Condition을 찾는다. SAT는 BDD처럼 전체 Truth Table을 압축하여 저장하려 하지 않고, Depth First Search (DFS)와 Backtracking, 그리고 Learning 기법을 사용하여 Solution을 찾는다.

• 장점: BDD에 비해 메모리 사용량이 훨씬 적고, 대규모 회로에서도 효율적으로 동작한다. 특히 Counter-example을 찾아내는 속도가 매우 빠르다.
• 단점: 특정 문제에 대해서는 Search Space가 너무 커서 해를 찾는 데 시간이 매우 오래 걸릴 수 있다(NP-Complete 문제). 따라서 현대의 LEC 툴은 BDD와 SAT를 혼합하여 사용하거나, 회로 구조에 따라 적절한 엔진을 자동으로 선택하는 Hybrid 방식을 채택한다.

2.4 Logic Cone 분할

전체 칩을 하나의 거대한 Boolean 방정식으로 놓고 푸는 것은 불가능하다. 따라서 LEC 툴은 설계를 Logic Cone이라는 작은 단위로 쪼개어 검증한다.

• Compare Points (Key Points): 검증의 기준점이 되는 요소들이다. 주로 Primary Output, Flip-Flop의 입력(D-pin), Black Box의 입력 핀 등이 해당된다.
• Logic Cone의 형성: 각 Compare Point를 Apex로 하고, 그 점에 영향을 미치는 모든 Primary Input, Flip-Flop 출력(Q-pin), Black Box 출력 핀 등을 Base로 하는 Combinational Logic 영역을 정의한다.

LEC는 이 Logic Cone 단위로 Golden과 Revised 디자인을 1:1 매핑한 후, 각 쌍이 등가인지를 독립적으로 검증한다. 이를 통해 전체 문제의 복잡도를 'Divide and Conquer' 방식으로 해결한다.

3. LEC 검증 프로세스의 세부 단계

실제 산업 현장에서 Synopsys Formality나 Cadence Conformal LEC와 같은 툴을 운용할 때, 검증 프로세스는 일반적으로 Setup, Mapping, Compare, Debug의 4단계 순환 구조를 따른다. 각 단계는 검증의 신뢰성을 확보하기 위해 필수적인 세부 작업들을 포함한다.

3.1 단계 1: Design modiling, Setup - 검증 환경의 구축

설정 단계는 비교할 두 디자인(Reference/Golden 및 Implementation/Revised)을 툴에 로드하고 올바른 검증 환경을 구성하는 과정이다. 이 단계에서의 사소한 실수가 추후 막대한 디버깅 비용을 초래하므로 가장 주의가 필요하다.

1. 라이브러리 로드 (Library Loading): 표준 셀(Standard Cell) 라이브러리, I/O 패드 라이브러리, 그리고 메모리나 Analog IP와 같은 블랙박스 모델을 로드한다.
   • Synopsys Formality는 주로 .db (Synopsys Liberty Binary) 형식을 사용한다.
   • Cadence Conformal은 .lib (Liberty) 또는 시뮬레이션용 Verilog 모델(.v)을 모두 지원한다. 중요한 점은 양쪽 디자인이 동일한 기능적 정의를 가진 라이브러리를 참조해야 한다는 것이다.
2. 디자인 읽기 (Read Design):
   • Golden Design: 검증의 기준이 되는 설계다. 주로 RTL (Verilog, VHDL, SystemVerilog) 코드가 된다. RTL을 읽을 때는 elaborate 과정을 통해 파라미터를 확정하고 계층 구조를 생성한다.
   • Revised Design: 비교 대상이 되는 설계다. Synthesis 후 생성된 Netlist 또는 P&R 후의 Netlist다.
3. Constraints 설정: LEC 툴이 디자인을 올바르게 해석하도록 돕는 가이드라인이다.
   • Set Constant: 넷리스트에는 테스트를 위한 스캔 체인 로직이 포함되어 있어 RTL과 구조적으로 다르다. 따라서 Scan Enable 신호를 0(또는 비활성 값)으로 고정하여 툴이 스캔 경로가 아닌 기능적 경로(Functional Path)만을 검증하도록 강제해야 한다.
   • Undriven Signals 처리: 입력이 연결되지 않은 포트(Floating inputs)를 '0', '1', 'Z'(High-Z), 또는 'X'(Don't Care) 중 무엇으로 해석할지 정의한다. 이를 잘못 설정하면 불필요한 불일치가 발생할 수 있다.

3.2 단계 2: Design Mapping - 비교 대상의 연계

Mapping은 Golden 디자인의 비교 Key Points와 Revised 디자인의 비교 점을 1:1로 대응시키는 과정이다. Synopsys Tool chain의 경우, SVF라는 파일이 이를 돕는다.

• Name-based Mapping: Register나 Port의 이름이 동일하거나 규칙적인 패턴을 가질 때 사용한다. 툴은 기본적으로 이름 일치를 가장 먼저 시도한다.
• Function-based Mapping: 이름이 변경되었더라도(예: 합성 툴이 최적화 과정에서 임의로 이름을 변경한 경우나 Data bus로 된 Flip Flop이 Multibit flopflop으로 Banking되거나 De-banking된 경우), 해당 포트를 구동하는 논리적 기능(Logic Cone)이 유사함을 분석하여 Mapping을 시도한다. 이는 계산 비용이 높지만, 이름 규칙이 깨진 넷리스트 검증에서 필수적이다.
• Renaming Rules: 사용자가 직접 Mapping 규칙을 정의할 수 있다. 예를 들어, RTL의 reg이 넷리스트에서 reg_0_로 변경된 경우, 툴에게 _를 ``로 치환하여 매핑하라고 지시할 수 있다.
• Unmapped Points 분석: 매핑되지 않은 포인트는 비교 대상에서 제외된다. 이것이 의도된 것인지(예: 사용하지 않는 로직 삭제) 아니면 오류인지(예: 이름 변경 규칙 누락) 반드시 확인해야 한다.

여기서 Unmatch list들이 발생하게 된다. LEC Fail 뿐만 아니라, Umatch list들도 검증자의 분석이 필요하다.

3.3 단계 3: Design Compare

Mapped Point 쌍에 대해 LEC 검증을 수행한다. Tool은 효율성을 극대화하기 위해 다단계 전략을 사용한다.

• Random Pattern Simulation: 먼저 수천 개의 Random Input Pattern을 주입하여 빠르게 출력 값을 비교한다. 이 단계에서 Mismatch가 발생하면 즉시 Non-Equivalent로 판정하고, cost가 높은 Solver Resource를 절약한다.
• Structural Analysis 및 Formal Verification: Random Pattern을 통과한 포인트들에 대해 SAT 또는 BDD Solver를 가동하여 Formal Proof를 시도한다.

결과는 다음 네 가지로 분류된다:

1. Equivalent: 모든 입력 조합에 대해 출력이 동일함 (검증 성공).
2. Non-Equivalent: 특정 입력에 대해 출력이 다름 (Setup Issue 또는 Functional Bug).
3. Inverted-Equivalent: 출력이 정반대임 (예: Q와 Qbar의 매핑). 이는 기능적으로는 등가일 수 있으나(Phase Inversion 허용 시), 주의 깊게 확인해야 한다.
4. Abort / Inconclusive: Tool이 주어진 시간이나 메모리 한도 내에서 증명을 완료하지 못함. 이는 주로 거대한 Multiplier와 같은 Arithmetic Logic이나 매우 깊은 Logic Depth를 가진 회로에서 발생한다.

3.4 단계 4: Debug - Root Cause Analysis 및 수정

Compare Result가 Non-Equivalent나 Abort가 발생하면 Debug 단계로 진입한다. 이는 LEC 엔지니어의 역량이 가장 요구되는 단계다. 한마디로 LEC에서 Fail나면, Debug가 정말 어렵다.

• Diagnosis: 불일치를 유발하는 Counter-example을 생성하고, Logic Cone 내에서 어느 Gate가 Error Candidate인지 Backtrace한다.
• Pattern Analysis: Tool이 제공하는 Waveform Viewer나 Schematic Viewer를 통해 Mismatch Point까지 신호가 어떻게 전파되는지 시각적으로 분석한다. 사용자는 RTL Source Code와 Netlist Schematic을 나란히 놓고 비교하며 Logic의 차이를 찾아낸다.

4. 합성 최적화와 구조적 변환의 처리

LEC 검증의 가장 큰 난관은 RTL과 넷리스트가 구조적으로 매우 다르다는 점이다. 논리 합성 툴(Design Compiler, Genus 등)은 Area, Power, Timing을 최적화하기 위해 RTL의 논리 구조를 대대적으로 변형한다. 이러한 구조적 변환을 LEC 툴이 이해하지 못하면 기능이 동일함에도 불구하고 불일치(False Negative)로 판정하게 된다.

4.1 조합 논리 최적화 (Combinational Logic Optimization)

가장 기본적인 최적화는 Boolean Algebra 법칙을 이용한 로직 단순화다.

• 상수 전파 (Constant Propagation): 특정 입력이 상수로 고정된 경우, 관련 로직을 제거하거나 단순화한다. LEC 툴도 동일한 상수 제약 조건을 알지 못하면 이를 오류로 인식할 수 있다.
• 로직 복제 및 병합 (Logic Replication & Merging): 타이밍 해결을 위해 팬아웃(Fan-out)이 큰 게이트를 복제하거나, 반대로 면적을 줄이기 위해 동일한 로직을 병합한다. LEC 툴은 이러한 다대일(N:1) 또는 일대다(1:N) 매핑을 처리할 수 있어야 한다.

4.2 순차 논리 최적화 (Sequential Logic Optimization)

조합 논리뿐만 아니라 레지스터(플립플롭) 자체를 변형하는 최적화는 검증을 더욱 어렵게 만든다.

• 리타이밍 (Retiming): 리타이밍은 크리티컬 패스(Critical Path)의 지연 시간을 줄이기 위해 레지스터를 조합 논리 건너편으로 물리적으로 이동시키는 기술이다. 이 경우 RTL의 레지스터 위치와 넷리스트의 레지스터 위치가 달라져 1:1 매핑이 불가능해진다.
  • 해결책: 합성 툴이 생성한 SVF(Setup Verification File)나 가이드 파일이 필수적이다. 이 파일에는 "RTL의 레지스터 A가 넷리스트의 레지스터 B로 이동했음"을 설명하는 정보가 담겨 있어, LEC 툴이 이를 참조하여 비교 점을 재설정할 수 있게 한다.
  • 자세한 내용은 Formality® Automated Setup File (SVF) Manual에 있습니다.
  • 근데 SVF도 종종 Bug가 존재해서, SVF를 사용하면 Fail이 발생하고, SVF를 안 사용하면 Succeed 발생하는 경우들도 있습니다.
• 파이프라인 레지스터 최적화
• FSM Re-encoding

4.3 Hierarchy Modifications

설계의 계층 구조 또한 최적화 대상이다.

• Ungrouping (그룹 해제): 합성 툴은 최적화 효율을 높이기 위해 하위 모듈의 경계를 허물고(Ungroup) 상위 모듈과 합쳐서 평탄화(Flatten)하는 경우가 많다.
  • 문제점: 모듈 경계가 사라지면 계층적(Hierarchical) 비교가 불가능해지고, 전체 디자인을 평탄화하여 비교해야 하므로 검증 시간이 급증한다. 또한 submodule/reg가 submodule_reg와 같이 이름이 변경되어 매핑 실패를 유발한다.
  • 해결책: 자동 이름 매핑 기능을 활용하거나, 중요 모듈에 대해서는 합성을 할 때 set_ungroup false 속성을 주어 계층 구조를 보존하도록 유도해야 한다.
• 경계 최적화 (Boundary Optimization): 모듈 경계를 넘어 로직을 이동시키거나(예: 인버터를 모듈 밖으로 밀어내기), 입력 포트의 상수를 내부로 전파하는 기술이다. 이 역시 계층적 비교 시 경계 핀에서의 불일치를 유발하므로, LEC 설정에서 set flatten model -boundary_optimization 등의 옵션을 활성화해야 한다.

5.LEC with UPF for Low power design

현대 모바일 및 IoT 칩 설계에서 저전력 기술의 적용은 필수적이다. Multi-Voltage Domain과 Power Gating 기술의 도입은 LEC 검증에 새로운 복잡성을 더한다.

5.1 UPF/CPF와 Power Intent

RTL 코드 자체에는 Power Network에 대한 정보가 없다. Power domain, Isolation, Level Shifter 등의 정보는 별도의 파일인 UPF(Unified Power Format)나 CPF(Common Power Format)에 정의된다.

LEC 검증 시 이 UPF/CPF 파일을 함께 로드해야 한다. 툴은 이 정보를 바탕으로 가상의 Power Logic을 RTL 모델에 삽입하여, 실제 전력 소자가 포함된 넷리스트와 비교 가능한 상태로 만든다.

5.2 저전력 셀 검증 이슈

• Isolation Cell: 전원이 꺼진 도메인에서 켜진 도메인으로 신호가 넘어갈 때, 신호를 특정 값(0 또는 1)으로 고정(Clamp)해주는 셀이다. LEC 툴은 UPF에 정의된 격리 규칙(Isolation Strategy)이 넷리스트에 정확히 구현되었는지 확인한다. 만약 격리 셀이 누락되거나 제어 신호 연결이 잘못되면 불일치가 발생한다.
• Level Shifter: 서로 다른 전압 레벨을 가진 도메인 간의 신호 전달을 담당한다. 기능적으로는 버퍼(Buffer)와 같지만, LEC에서는 전압 레벨 규칙 준수 여부를 확인해야 한다.
• State Retention Cell: 전원이 꺼져도 데이터를 유지하는 특수 레지스터다. LEC는 일반 레지스터와 Retention 레지스터 간의 매핑을 처리해야 하며, 이를 위해 라이브러리 모델이 정확히 로드되어야 한다.

6. ECO (Engineering Change Order)와 LEC

칩 설계의 후반부, 특히 P&R이나 마스크 제작 직전에 버그가 발견되면, 전체 합성을 다시 하는 대신 최소한의 게이트만 수정하는 FECO(Functional Engineering Change Order)를 수행한다. LEC 툴은 ECO 과정에서도 핵심적인 역할을 한다.

• Functional ECO: RTL을 수정한 뒤, 기존 넷리스트에 최소한의 Patch만 가하여 RTL과 동일하게 만드는 과정이다. Conformal ECO와 같은 툴은 수정된 RTL과 기존 넷리스트를 비교하여, 차이점을 해소하기 위해 필요한 패치 로직을 자동으로 생성해준다.
• Spare ECO Cell 활용: Tape-out은 이미 완료된 상태이고, FEOL 공정까지 이미 완료된 경우, 칩 내부에 미리 뿌려둔 여분의 게이트(Spare Cells)를 사용하고, BEOL Metal layer를 수정하여 버그를 수정해야 한다. LEC 툴은 사용 가능한 Spare Cell 리스트를 입력받아 이를 활용한 최적의 패치 넷리스트를 생성할 수 있다.

결론: 무결점 설계를 위한 최후의 보루

LEC는 단순한 툴 실행 과정을 넘어, 설계의 무결성을 수학적으로 보증하는 엄밀한 엔지니어링 절차다. RTL에서 게이트로, 그리고 최종 레이아웃으로 이어지는 긴 설계 흐름 속에서 수많은 최적화와 구조적 변형이 일어나지만, LEC는 그 중심에서 기능적 본질이 훼손되지 않았음을 지키는 최후의 보루 역할을 한다.

성공적인 LEC 운용을 위해서는 BDD/SAT 등 형식 검증 이론에 대한 이해, 합성 및 DFT 변환 과정에 대한 깊은 지식, 그리고 체계적인 디버깅 방법론이 필수적이다. 향후 디자인 크기가 더욱 거대해지고 AI 반도체와 같이 복잡한 연산 로직이 증가함에 따라, 계층적 검증, 순차 논리 등가성 검증(SLEC), 그리고 클라우드 기반의 병렬 검증과 같은 진보된 기법의 중요성은 더욱 커질 것이다. 검증 엔지니어에게 LEC는 더 이상 선택이 아닌 필수 생존 기술이다.