VLSI Korea 팀 가이드: 반도체 회사의 각 팀이 실제로 무슨 일을 하는지, 현직자 시점으로 정리합니다. 취준생과 5년차 이내 주니어를 위한 시리즈.
핵심 답변: Formal Verification은 시뮬레이션처럼 자극을 흘려보지 않고, RTL의 properties를 수학적으로 증명한다. JasperGold나 VC Formal을 켜놓고 cache coherence, arbiter fairness, X-propagation, security isolation 같은 corner case를 tapeout 전에 잡아내는 팀이다. 이 글은 한국 반도체 회사에서 Formal 팀이 실제로 어떤 위치에 있고, 신입부터 5년차까지 무엇을 배우며, 시장에서 얼마를 받는지 솔직하게 정리한다.
1. 한 줄로 말하면
Formal Verification 팀은 RTL이 의도대로 동작한다는 것을 수학적으로 증명하는 팀이다. 시뮬레이션은 입력 시나리오를 흘려보고 결과가 맞는지 확인하는 방식이라 cover하지 못한 입력 조합이 항상 남지만, formal은 모든 가능한 입력 시퀀스에 대해 properties가 깨지지 않음을 boolean/temporal logic 위에서 증명한다. 칩이 만들어지는 흐름에서는 RTL 설계와 DV(Design Verification) 사이에 끼어 있고, 특히 control logic, FSM, arbiter, cache coherence, security isolation 같이 상태 공간이 폭발하는 부분에서 dynamic simulation이 손도 못 대는 corner를 잡는다.
2. 회사 안에서의 자리
대부분의 한국 회사에서 Formal 팀은 독립 조직이라기보다 DV 본부 안의 specialist 그룹이다. 삼성 LSI나 SK하이닉스의 SoC 사업부에서는 Verification 본부 산하에 Formal 그룹이 따로 있고, 큰 프로젝트(모뎀, AP의 fabric, 메모리 컨트롤러)에 1~3명씩 붙는다. 보고는 보통 DV manager나 verification architect로 올라가고, 옆자리는 RTL designer와 UVM-based DV 엔지니어다.
팹리스(텔레칩스, 리벨리온, 퓨리오사AI, 사피온)는 조직이 작아서 별도 Formal 팀이 없는 경우가 많다. 보통 senior DV 엔지니어 한두 명이 형식적 검증까지 겸하고, 외부 service(Cadence, Synopsys AE)에 의존한다. 반면 외국계(ARM 코리아, Synopsys 코리아, Cadence 코리아)는 Formal이 product 자체이거나 핵심 IP의 sign-off 조건이라 전담팀이 두텁다. TSMC는 자체 IP 검증 외에는 거의 안 쓰고, Intel/Nvidia는 control-heavy block마다 formal을 표준 절차로 박아 둔다. 즉, 한국 IDM에 들어가면 'DV 안의 specialist'로 자리잡고, 글로벌 fabless로 가면 'sign-off owner'에 더 가까워진다.
3. 진짜 하루/일주일
9시 출근하면 가장 먼저 하는 일은 어젯밤 regression이 끝난 JasperGold 결과를 확인하는 것이다. proof가 unbounded로 도달했는지, bounded(예: 50 cycles)에서 멈췄는지, counterexample(CEX)이 떨어졌는지 본다. CEX 하나에 보통 오전이 다 간다. waveform을 띄우고 RTL designer를 불러서 'spec상 이 transaction이 outstanding 4개를 넘으면 어떻게 되어야 하느냐'를 같이 본다. 절반은 진짜 RTL 버그, 절반은 property가 spec을 잘못 옮긴 것이다.
점심 먹고 오후엔 새 property를 작성한다. 새로 받은 IP의 spec PDF를 보면서 SVA(SystemVerilog Assertions)로 변환한다. 'arbiter는 fair해야 한다'는 한 줄을 'request가 grant 받기까지 starvation 없이 N cycle 안에 처리된다'는 LTL 비슷한 형식으로 풀어 쓴다. constraint도 같이 짠다. 입력에 절대 일어나지 않는 시퀀스(예: reset 중 valid 신호가 토글되는 일)를 assume으로 넣지 않으면 false fail이 산처럼 쌓인다.
주중 한 번은 RTL designer와 walk-through 미팅이 있다. 어떤 module을 black-box으로 abstract할지, 어떤 register를 cut-point로 잡을지 정한다. formal은 state explosion이 본질적 적이라, 실력의 절반은 abstraction을 잘 잡는 능력에서 나온다. 큰 IP 하나를 통째로 돌리면 tool이 며칠을 돌고도 inconclusive로 끝나기 때문에, 검증 대상을 잘게 쪼개고 인접 logic을 약속(assume)으로 묶어야 한다.
마일스톤 사이클은 simulation 팀과 다르다. RTL freeze 직전 한 달은 새로 들어오는 ECO마다 property가 깨져서 야근이 잦다. tapeout 직전 2주는 'inconclusive 항목을 어디까지 sign-off로 쳐줄 것인가'를 두고 verification lead와 협상하는 시간이다. 반면 RTL freeze 후 다음 프로젝트 시작 전 1~2달은 비교적 여유가 있어, 이때 사내 property library를 정리하거나 새 EDA 버전 평가를 한다. 즉 일이 평탄하지 않고, 'idle 같다가 갑자기 두 달 야근' 패턴이 반복된다.
코드보다 PDF와 waveform을 더 많이 읽는 직무다. 하루 평균 SVA 30~50줄을 새로 쓰거나 고치고, 그것보다 훨씬 많은 spec 문장을 읽는다. lab 장비는 거의 만질 일이 없고, 책상에서 머리 싸매는 시간이 80%다.
4. 핵심 기술 스택
- 언어/포맷: SystemVerilog (RTL 읽기), SVA(SystemVerilog Assertions), PSL(레거시), Tcl(JasperGold 스크립팅), Python(결과 파싱/regression).
- EDA 툴: Cadence JasperGold(시장 점유 1위), Synopsys VC Formal, Siemens Questa Formal, OneSpin(Siemens 인수). 회사마다 표준 툴이 정해져 있고 다른 툴 경험은 plus alpha다.
- 방법론: assume-guarantee, abstraction(blackbox/cut-point), induction depth 튜닝, k-induction, BMC(Bounded Model Checking), Sequential Equivalence Checking(SEC), Formal Property Verification(FPV), Connectivity Check, Coverage Closure App, X-propagation Check.
- 인접 도메인 지식: 디지털 회로/FSM 이론, temporal logic(LTL/CTL 기초), CDC/RDC 이슈, low-power UPF에서 isolation/retention 검증, RISC-V/ARM 같은 protocol 사양, AXI/CHI 같은 interconnect, security primitives(secure boot, key isolation).
SVA는 입사하면 1~2주에 기본을 떼지만, 'property를 잘 쓰는 것'은 5년 가도 끝이 없다. 같은 spec을 두 사람이 SVA로 옮기면 한쪽은 30줄로 모든 corner를 커버하고 다른 쪽은 200줄로도 holes가 남는다. EDA 툴 GUI 사용법은 며칠이면 익숙해지지만, tool이 inconclusive라고 멈췄을 때 cut-point를 어디 박아야 proof가 살아나는지를 아는 것은 경험이 쌓여야 보인다. abstraction을 잘 잡는 사람이 이 팀에서 가장 비싸다.
5. 1년차 → 3년차 → 5년차 성장 곡선
1년차는 SVA 문법 익히는 데 첫 3개월을 쓴다. 사수가 만들어 놓은 property library를 읽고, 이미 끝난 IP의 testbench를 변형하면서 감을 잡는다. 이 시기엔 'CEX가 떨어져도 그게 진짜 RTL bug인지, 자기가 assume을 빠뜨려서 false fail인지'를 구분하지 못한다. 보통 옆 시니어가 '이건 디자이너 문제, 이건 네 문제'라고 분류해 준다. 1년이 끝날 때쯤이면 작은 IP(예: small FSM, simple arbiter) 하나의 property set을 처음부터 끝까지 자기가 짤 수 있다.
3년차가 첫 진짜 owned deliverable을 받는 시기다. 보통 중간 크기 IP(memory controller의 한 sub-module, security wrapper, interrupt controller) 하나를 통째로 책임진다. spec 작성자(architect)와 직접 회의에 들어가고, RTL designer와 spec 해석 충돌이 났을 때 자기 의견을 낸다. abstraction 결정도 자기가 한다. 이 시기에 'inconclusive를 어디까지 좁힐 수 있는가'가 그 사람의 실력 척도다. 같은 IP를 다른 3년차에게 주면 proof depth가 두 배 차이 나는 일이 흔하다.
5년차는 두 갈래로 갈린다. 한쪽은 'methodology owner'로, 사내 형식 검증 flow 자체를 설계한다. 어떤 IP에 어떤 app(FPV vs SEC vs CSR check)을 적용할지 가이드를 만들고, 신입 onboarding을 책임진다. 다른 한쪽은 'IP architect'로 넘어간다. formal로 단련된 corner case sense는 RTL 설계자로 전향했을 때 굉장한 무기가 된다. 5년차에 시니어 자리가 한국 IDM에서 좁은 편이라, 매니저 트랙으로 가지 않으면 외국계나 fabless로 점프하는 경로가 흔하다. 정직하게 말하면, formal로 박사급 시니어 자리를 한국에서 잡는 길은 삼성 LSI/하이닉스의 specialist 트랙 외엔 잘 안 보인다.
6. 한국 시장에서의 평가 (이직 시장 가치)
한국에서 Formal Verification 인력을 본격적으로 운영하는 곳은 사실상 손에 꼽힌다. 삼성 LSI는 모뎀, AP fabric, 보안 IP에 formal을 표준으로 쓰고 팀 규모도 가장 크다. SK하이닉스는 메모리 controller와 솔루션 SoC에서 formal 사용이 늘고 있고, 최근 채용도 활발하다. 삼성 파운드리는 자체 SoC보다는 IP 검증과 customer support 성격이 강하다.
팹리스로 내려오면 리벨리온, 퓨리오사AI, 사피온, 텔레칩스가 formal을 쓰지만 전담 팀보다 senior DV가 겸직하는 구조다. 작은 회사일수록 'formal만 하는 사람'은 비효율적이라 보고, DV 전반을 같이 시키는 경우가 많다. ARM 코리아, Synopsys 코리아, Cadence 코리아는 formal이 product의 일부거나 customer-facing AE 업무라 전담 인력이 있다. MediaTek 코리아는 본사 정책에 따라 formal 사용 범위가 정해진다.
이직 시장에서 formal 경험은 'DV 일반'보다는 좁고 깊은 트랙으로 본다. 삼성↔하이닉스 직접 이동, 삼성↔리벨리온/퓨리오사 이동이 가장 흔하고, 글로벌은 미국(Apple, Nvidia, AMD, Qualcomm, Intel) 옵션이 열려 있다. 미국 빅테크는 control-heavy IP의 formal sign-off 인력을 항상 찾고 있어서, 영어와 비자만 풀리면 한국 IDM에서 5년 이상 경력으로 인터뷰까지는 비교적 쉽게 간다. 대만(MediaTek 본사)은 formal 사용이 한국과 비슷하고, 이스라엘 fabless도 채용 많은 편이다.
7. 연봉 가이드 (2026년 기준 한국)
잡플래닛/링크드인 공개 정보와 현직자 인터뷰 기반 추정이다. 회사·고과·박사 여부에 따라 편차가 크고, 모두 base+성과급(PS/PI 포함) 합산 기준이다. 외국계 RSU는 별도 표기.
- 신입 (학사): 약 ₩5,500만 ~ ₩6,500만 (삼성/하이닉스 기준, 팹리스는 비슷하거나 +α)
- 신입 (석사): 약 ₩6,500만 ~ ₩8,000만
- 3-5년차: 약 ₩8,500만 ~ ₩1억 2,000만 (대기업 기준, 고과·PS 변동 큼)
- 시니어 (8년+): 약 ₩1억 3,000만 ~ ₩1억 8,000만 (스톡/RSU 별도)
외국계 코리아 지사(ARM/Synopsys/Cadence)는 base가 한국 대기업과 비슷하거나 약간 낮지만 RSU와 bonus 비중이 커서 5년차 기준 총보상 ₩1억 2,000만~₩1억 6,000만 추정. 미국 offer로 환산하면 신입 석사가 약 USD 150~180k(₩2억~₩2억 4,000만, RSU 4년 vest 포함) 수준으로 점프하는 게 일반적이고, 시니어(L5~L6 equivalent)는 USD 280~400k(₩3억 7,000만~₩5억 3,000만)까지 보인다. 단, 미국 offer는 거주비/세금 차이가 커서 실수령 비교가 단순하지 않다.
같은 연차의 RTL 디자이너나 일반 DV와 비교하면, 한국 IDM 기준 formal은 비슷하거나 살짝 낮다는 게 일반적인 인식이다. 대신 외국계 이직 시 가산점이 더 명확하다.
8. 진입 장벽 / 이 팀에 가려면
전공은 전자/전기/컴공이 압도적이고, 수학과·물리과 출신도 가끔 있다. 형식 검증의 백본이 boolean satisfiability, model checking, temporal logic이라 이산수학·논리회로·자동기계론(automata theory)을 좋아한 사람이 잘 적응한다. 학부생 중 'CSE 디지털 시스템 설계' 수업에서 FSM 만들고 testbench 짜는 게 재미있었던 사람이라면 후보군이다.
학력 권장도는 석사 이상이다. 학사 신입을 formal 전담으로 뽑는 한국 회사는 드물고, 보통 DV로 입사 후 사내 이동이나 specialist 트랙으로 분화된다. 박사는 메리트가 분명히 있지만 필수는 아니다. 박사라면 model checking, theorem proving(Coq, Isabelle, ACL2), hardware security 같은 주제로 공부했을 때 채용 시 가산점이 크다.
가장 도움 되는 학부 수업: 디지털 시스템 설계, 컴퓨터 구조, 이산수학, 컴파일러(SAT/SMT 노출), 알고리즘. SystemVerilog와 UVM은 학교에서 거의 안 가르치니 따로 익혀야 한다. 인턴십은 삼성/하이닉스 DV 인턴이 가장 흔한 진입로고, 학회 발표(DAC, DVCon, ICCAD)에 학생 논문을 낸 경험이 있으면 이력서 weight가 확실히 올라간다. 오픈소스 기여는 RISC-V Rocket이나 OpenLane에 verification 관련 PR 한두 개만 있어도 인터뷰에서 얘깃거리가 되고, formal 쪽 오픈소스(EBMC, SymbiYosys)에 기여한 학생은 한국에서 거의 못 봤다는 점에서 오히려 차별점이다.
9. 추천 학습 경로
- 책: Ben Cohen 외, SystemVerilog Assertions Handbook(SVA의 표준 레퍼런스, 책상 위에 두는 책). Erik Seligman 외, Formal Verification: An Essential Toolkit for Modern VLSI Design(Intel 현직자가 쓴 가장 실용적인 입문서). Christoph Kern, Mark R. Greenstreet 등의 Formal Methods in System Design 논문 모음(이론 기반 다지기).
- 강의/MOOC: Coursera의 'Hardware Security' 시리즈 일부 강의에서 formal 사용 사례가 나온다. 유튜브의 Cadence/Synopsys 공식 채널에 JasperGold/VC Formal tutorial이 있어 무료로 GUI 흐름을 파악할 수 있다. UC Berkeley CS 219C(Formal Methods) 자료가 공개되어 있어 이론 보강에 좋다.
- 핵심 논문/표준 문서: IEEE 1800 SystemVerilog LRM의 SVA 챕터(반드시 한 번은 정독). Clarke, Grumberg, Peled의 Model Checking(고전, 1999년이지만 여전히 유효). DVCon US/Europe 매년 발표 자료(현업 사례가 가장 빨리 올라옴).
- 오픈소스 프로젝트: SymbiYosys(Yosys 기반 open formal flow, 무료로 BMC/induction 돌려볼 수 있음), EBMC(Edinburgh Bounded Model Checker), Cocotb(Python 기반 testbench, formal과 연동 사례 있음), RISC-V Rocket Chip(formal property 작성 연습 대상으로 적합), OpenLane/OpenROAD의 verification flow.
- 커뮤니티: Verification Academy(Siemens 운영, 포럼 질의응답 활발), DVCon 컨퍼런스, 한국에서는 SoC 학회와 IEEK(대한전자공학회) 시스템 분과. 글로벌은 Reddit r/FPGA, r/chipdesign에 formal 관련 토론이 가끔 있고, X/Twitter의 formal verification 커뮤니티(Clifford Wolf, Yosys 메인테이너 등)가 작지만 활발하다.
10. 한 줄 코멘트
Formal은 '시뮬레이션이 못 본 corner를 잡았다'는 deliverable이 명확하고 한 번 익히면 시장 가치가 오래가는 직무지만, 한국에서 전담 자리가 좁아 5년차쯤 매니저 트랙·외국계 이직·RTL 전향 중 하나를 정해야 하는 갈림길이 빨리 온다.
다른 팀 가이드도 시리즈로 발행 중입니다. 전체 시리즈 보기 · 매일 글로벌 반도체 브리프는 vlsi.kr.
