Logical Equivalence Check는 언제 하는걸까?: Synthesis, DFT, P&R, ECO 네 번의 관문

TL;DR

• Logical Equivalence Check는 A 설계와 A' 설계의 기능 차이를 비교하는 것이다.
• ASIC Design flow 사이에 수십번의 단계가 있다.
• LEC는 ASIC 설계 flow에서 여러번 수행된다:
  • (1) RTL vs Synthesized netlist
  • (2) RTL vs DFT-inserted netlist
  • (3) Synthesis vs P&R netlist
  • (4) 각 ECO 단계 적용 후 verification ...
  • 이 외에도 더 많은 설계 단계가 있는데, 이 때마다 LEC를 하고, 양산 과제에서는 Tape-out 까지 한 디자인 당 최소 5번은 LEC를 돌린다고 보면 된다.

당신은 완벽한 RTL Code를 작성했다.

• EDA Tool의 Logic Synthesis 단계에서 Bug로 인해 Inverter 1개를 더 넣었다고 하자. 당신은 이것을 검증할 방법이 있는가?
• 2~3nm GAA 공정의 mask set cost는 $30M 이상이다.

LEC 혹은 EQ는 이런 것을 검증하는 것인데, EDA Tool을 이용해서 설계 하는 단계가 엄청나게 많다.

Stage 1: RTL vs Synthesized Netlist

Design Compiler가 RTL을 gate-level로 변환한 직후. 이 단계에서 Formality는 RTL의 functional intent가 gate-level netlist에 보존되었는지 검증한다.

비교 대상:

• Reference: RTL (Verilog/VHDL original source)
• Implementation: Design Compiler 출력 netlist (.ddc, .v)
  • SVF source: Synopsys Design Compiler가 synthesis 중 생성한 파일. Synopsys Tool chain에서 TAT 효율 높이려고 쓰는 파일이다.

SVF의 역할:

• DC가 적용한 설계 변경 정보를 Formality에 전달. register가 combinational logic 경계를 넘어 이동했을 때 state correspondence를 알려준다.

SVF가 없으면 Formality는 모든 state element 조합을 brute-force로 시도하는데, 이게 런타임 문제로 일어날 수도 있고, LEC Fail로 발생할 수도 있다.

Stage 2: Synthesized Netlist vs DFT-Inserted/stitched Netlist

DFT Insertion을 RTL Level에서 하는 경우도 있고, Synthesized netlist에 하는 경우도 있다. Synthesis 이후에 했다고 가정하면,

DFT insertion 이후, netlist에는 scan chain, test compression, BIST logic이 추가된다.

비교 대상:

• Reference: Synthesized Netlist
• Implementation: DFT-inserted netlist

즉, Reference는 chip의 기본 function 기능만하고, Implementation은 기본 function 기능과 DFT 기능까지 한다.

DFT가 netlist에 추가하는 것:

• Scan chain: 모든 flip-flop을 직렬로 연결. scan_enable=1일 때 shift register로 동작
• Test compression: EDT(Embedded Deterministic Test) logic. decompressor/compressor pair
• Boundary scan: JTAG TAP controller + boundary scan cells
• BIST: Memory BIST, Logic BIST controller

LEC의 검증 포인트:

• Chip의 동작 모드를 기본 function mode로 고정 시켜놓고, reference와 implementation과 비교해야한다.

Stage 3: Synthesis/DFT Netlist vs P&R Netlist

P&R 이후 netlist는 다음 변경을 포함한다:

• Clock tree synthesis (CTS): clock buffer insertion으로 인한 hierarchical 변경
• Hold time fixing: delay buffer insertion
• Scan chain reordering: 배치 최적화를 위한 scan flip-flop 순서 변경
• Power optimization: clock gating cell 추가, isolation cell 삽입

Formality는 P&R tool (ICC2, Innovus)이 출력한 netlist를 synthesis netlist (또는 DFT netlist)와 비교한다. 이 단계의 핵심은 physical optimization이 functional equivalence를 깨지 않았음을 증명하는 것이다.

P&R 단계에서도 마찬가지로 SVF를 추출할 수 있다. (Clock gate restructuring 같은걸 할때, 좀 구조가 바뀌니까.)

Stage 4: ECO 검증

ECO는 크게 두 종류다:

• Functional ECO: RTL bug fix 또는 new feature addition. logic cone이 변경됨
• Timing ECO: setup/hold violation fix. buffer/resize 변경만 있고 logic은 불변

Functional ECO에서 LEC는 꽤 유용하다.

이런 경우들이 프로젝트마다 꼭 발생한다.

Tape-out까지 2주 남았는데, RTL 코드 버그 발견되어 핫픽스 필요한 상황.

"RTL 엔지니어는 RTL 코드에서 20줄만 바꿨어요" 하는데

"Physical Design engineer"는 이거 20줄이 바뀌면 얼마나 많이 바뀌는지 아세요 Timing close 끝났는데 이거 다시 처음부터 해야한다구요" 하는 상황.

이런 때를 위해, Formality 같은 상용 LEC Tool은 ECO Script를 출력해준다.

• A의 RTL Code로 Synthesis한 Netlist
• A'의 RTL Code로 Synthesis한 Netlist

위 두개를 LEC 돌리고 ECO Script generate 하면, 어떤 셀들을 추가하고, 빼야하는지, 어떤 커넥션 변경해야하는지가 스크립트가 나온다.

그리고 그 스크립트 넣고 새 LEC 돌리고, 새로 Timing close까지 달리면 된다.

말이 쉬운데, LEC는 고수 or 런돌이가 확실히 갈리는 분야다.

UPF 넣은 복잡한 회로에서 LEC Fail 나는 Tool bug 몇 번 경험을 해보면 LEC 고수가 될 수 있다.