형식 검증과 시뮬레이션 차이, 증명과 샘플링의 갈림길

새 교차로를 열기 전에 신호 체계를 점검하는 방법은 크게 두 가지입니다. 하나는 시험 운행으로, 여러 시간대와 교통량을 가정해 차량을 실제로 흘려 보며 충돌이 나는지 지켜보는 방식입니다. 다른 하나는 신호 설계도를 논리적으로 따져서 서로 교차하는 두 방향이 동시에 녹색이 될 수 없음을 증명하는 방식입니다.

칩 검증에서는 시험 운행이 시뮬레이션이고 설계도 증명이 형식 검증에 해당하며, 형식 검증과 시뮬레이션은 서로를 대체하기보다 맡는 영역이 다릅니다. 시험 운행은 아무리 많이 해도 해 보지 않은 상황이 남고, 설계도 증명은 도로의 실제 사정이 설계도와 달라지면 의미가 줄어듭니다.

비유와 다른 점도 있습니다. 칩에서는 가능한 입력의 수가 상상보다 훨씬 많고, 증명이 닿는 범위가 설계의 크기에 따라 급격히 줄어듭니다. 이 글에서는 두 방식이 각각 무엇을 보증하고 어디에서 막히는지를 구조로 풀어 보겠습니다.

형식 검증과 시뮬레이션이 검증에서 맡는 역할

검증(verification)은 설계가 스펙대로 동작하는지 확인하는 일입니다. 제조를 마친 칩에서 오류가 발견되면 비용이 매우 크기 때문에, 제조 전에 최대한 많은 오류를 잡아내는 것이 목표입니다.

이 확인의 방식이 크게 시뮬레이션과 형식 검증으로 나뉩니다. 시뮬레이션은 입력을 넣어 보고 출력을 확인하므로, 확인한 범위 안에서만 답을 줍니다.

형식 검증은 입력을 하나씩 넣는 대신 수학적 추론으로 모든 경우를 한꺼번에 따집니다. 증명이 끝나면 정해진 조건 안에서는 예외가 없다는 뜻이 됩니다.

시뮬레이션 기반 검증의 구조, 자극과 기대값 비교

시뮬레이션 기반 검증(simulation-based verification)은 검증 대상 설계(DUT, Design Under Test)에 입력을 넣고 출력이 기대와 같은지 비교하는 방식입니다. 입력을 만드는 테스트벤치(testbench), 출력을 기대값과 비교하는 스코어보드(scoreboard), 동작 규칙을 코드로 적어 두는 어서션(assertion)이 기본 부품입니다.

장점은 거의 모든 설계에 적용할 수 있고 블록부터 시스템 전체까지 확대할 수 있다는 점입니다. 실패했을 때 파형으로 상황을 그대로 볼 수 있어 원인을 추적하기도 쉽습니다.

한계는 입력을 사람이 만든 시나리오와 무작위 자극에 의존한다는 점입니다. 오류를 한 번도 건드리지 못한 채 통과할 수 있으므로, 시뮬레이션이 통과했다는 말은 오류가 없다는 뜻이 아니라 해 본 범위에서는 찾지 못했다는 뜻입니다.

입력 조합이 너무 많아 생기는 시뮬레이션의 한계

시뮬레이션이 닿지 못하는 영역은 입력의 조합 수에서 나옵니다. 입력이 n비트이면 조합이 2의 n제곱 개이고, 상태를 가진 회로에서는 입력의 순서까지 달라지므로 경우의 수가 더 크게 늘어납니다.

그래서 시뮬레이션은 모든 입력 대신 스펙에서 중요한 시나리오와 경계 조건, 무작위로 뽑은 조합을 시험합니다. 이 선택이 충분했는지는 커버리지 같은 지표로 가늠하지만, 지표가 채워졌다고 해서 증명이 되는 것은 아닙니다.

FIFO가 가득 찬 순간에 읽기와 쓰기가 동시에 들어오는 경우처럼 드물게 겹치는 사건을 코너 케이스(corner case)라고 부르며, 이런 조합이 시뮬레이션에서 가장 놓치기 쉬운 오류의 자리입니다.

형식 검증의 원리, 모든 입력을 한꺼번에 따지는 증명

형식 검증(formal verification)은 설계를 수학적 모델로 보고, 어떤 성질이 모든 입력과 도달 가능한 모든 상태에서 성립하는지를 도구가 추론으로 확인하는 방법입니다. 입력을 하나씩 넣지 않고, 성질을 깨는 입력이 존재하는지를 논리식으로 풀어 찾습니다.

결과는 대체로 세 가지입니다. 성질이 증명되면 해당 조건 아래에서는 어떤 입력으로도 위반이 없다는 뜻이고, 실패하면 위반을 일으키는 입력 순서인 반례(counterexample)가 파형으로 나옵니다. 나머지 하나는 정해진 시간 안에 결론이 나지 않거나 특정 사이클 깊이까지만 증명되는 미결 결과입니다.

반례가 나온다는 점은 시뮬레이션의 실패와 비슷하지만, 사람이 그 시나리오를 떠올리지 못했는데도 도구가 찾아낸다는 점이 다릅니다. 예를 들어 아비터가 두 요청에 동시에 허가를 줄 수 있는지를 성질로 적어 두면, 그런 상황이 가능한 입력 순서를 도구가 직접 찾아 줍니다.

내부에서는 SAT 풀이기나 BDD 같은 논리 연산 기법을 씁니다. 일정 사이클 깊이까지 모든 경우를 확인하는 바운디드 모델 체킹(BMC, Bounded Model Checking)이나, 한 사이클에서 성립하는 성질이 다음 사이클에도 이어짐을 보이는 귀납 증명을 조합하기도 합니다.

형식 검증의 두 갈래, 등가성 검사와 속성 검사

형식 검증은 쓰임새에 따라 크게 두 갈래입니다. 등가성 검사(equivalence checking)는 두 설계가 같은 기능을 하는지 비교하는 방법으로, 논리 합성 전후의 RTL과 게이트 넷리스트가 같은지 확인하는 용도가 대표적입니다. 합성 툴이 최적화로 회로를 바꿨을 때 기능이 변하지 않았음을 입력을 넣지 않고 확인합니다.

속성 검사(property checking)는 설계가 지켜야 할 규칙을 어서션이나 속성 언어로 적어 두고 위반 가능성을 확인하는 방법입니다. 시뮬레이션에서 쓰던 어서션을 그대로 증명에도 쓸 수 있다는 점이 실무에서 큰 장점입니다.

형식 검증의 한계, 상태 폭발과 가정의 함정

가장 큰 한계는 상태 폭발(state explosion)입니다. 레지스터가 n개면 상태가 최대 2의 n제곱개이므로 설계가 커질수록 따져야 할 공간이 기하급수로 늘어 증명이 끝나지 않을 수 있습니다. 그래서 FIFO 제어, 아비터, 프로토콜 상태기계처럼 제어 중심의 작은 블록에 잘 맞고, 곱셈기처럼 데이터 연산이 깊은 블록이나 칩 전체에는 어렵습니다.

두 번째 함정은 가정입니다. 입력이 가질 수 있는 값을 제한하는 가정(assumption)을 적어야 현실에서 일어나지 않는 입력 때문에 생기는 가짜 실패를 막을 수 있는데, 가정이 너무 강하면 실제로 일어날 수 있는 입력까지 배제해 증명이 의미를 잃습니다. 증명되었으니 안전하다는 말이 위험한 이유입니다.

또 하나는 조건이 한 번도 만족되지 않아 규칙이 자명하게 참이 되는 경우입니다. 조건부 규칙에서 조건이 실제로 도달 가능한지를 확인하는 cover 속성을 함께 두어 이런 빈 증명을 걸러냅니다.

두 방식을 함께 쓰는 검증 흐름

형식 검증과 시뮬레이션은 실무에서 한쪽을 고르지 않고 대상에 맞게 나눠 씁니다. 블록 수준에서는 형식 검증으로 제어 로직의 코너 케이스를 맡기고, 시스템 수준에서는 시뮬레이션으로 큰 시나리오를 맡기는 식입니다.

UVM은 시뮬레이션 쪽의 표준 방법론이고, 형식 검증은 같은 어서션을 증명에 재사용할 수 있어 두 방식이 자산을 나누어 쓰기도 합니다.

형식 검증과 시뮬레이션 비교 표

구분	시뮬레이션	형식 검증
확인 방식	입력을 넣어 출력을 비교	논리 추론으로 성질을 증명
보증 범위	시험한 입력의 범위	가정 아래의 모든 입력, 깊이 제한 시 그 깊이까지
오류를 찾는 힘	준비한 시나리오에 의존	떠올리지 못한 입력도 반례로 제시
잘 맞는 대상	블록부터 시스템 전체	제어 중심의 작은 블록, 합성 전후 비교
주된 한계	시험하지 않은 조합이 남음	상태 폭발과 가정의 오류
주요 산출물	커버리지와 파형	증명 결과와 반례

핵심 정리

형식 검증과 시뮬레이션은 오류를 찾는 방식이 다릅니다. 시뮬레이션은 입력을 골라 시험하므로 범위가 넓지만 해 보지 않은 부분이 남고, 형식 검증은 가정 아래의 모든 입력을 증명하지만 설계가 커지면 닿지 못합니다.

교차로의 비유로 돌아가면 시험 운행은 현실에 가까운 사고를 잡고, 설계도 증명은 동시에 녹색이 되는 일 자체를 막습니다. 칩에서는 제어 로직의 코너 케이스와 합성 전후의 동일성은 증명에 맡기고, 큰 시나리오와 시스템 동작은 시뮬레이션에 맡기는 분담이 현실적입니다.

면접 대비 질문