[VLSI CAD] kbdd · MiniSAT · Espresso · SIS?

🆓 무료 글 · 누구나 무료로 읽을 수 있는 글입니다

EDA, VLSI CAD 수업을 듣다 보면, 갑자기 이런 도구들이 튀어나온다.

• kbdd
• MiniSAT
• Espresso
• SIS

처음엔 다 비슷해 보인다.
“다 논리식 만지는 거 아님?”
“이걸 실무에서 쓰긴 하나?”

결론부터 말하면 이 도구들은 ‘칩이 맞는지 증명하는 세계’의 도구들이다.

이런 기본적인 개념들이 Logic Synthesis, DFT 등 많은 디지털 EDA Tool에 사용된다.

1. 큰 그림: 이 수업의 진짜 주제

이 수업의 핵심은 Boolean Function을 다루는 방법이다.

“이 논리 회로가 수학적으로 맞는가?”

이를 위해 사용하는 접근이 세 갈래로 나뉜다.

2. kbdd — “같은 논리면 같은 그래프”

kbdd가 하는 일

kbdd는 BDD(Binary Decision Diagram) 기반 논리 계산기다.

BDD의 핵심 성질은 이거다.

같은 Boolean function이면,
항상 동일한 그래프 구조를 가진다.

즉:

• 논리식이 아무리 달라도
• 회로 구조가 달라도
• 기능이 같으면 → BDD는 같다

그래서 kbdd로 할 수 있는 대표 작업은:

• 논리 동치 검증 (verify)
• 가능한 입력 조합 찾기 (satisfy)
• 변수 제거 (quantification)
• 회로 자동 복구(Logic repair)

kbdd는 언제 쓰나

• RTL vs Spec 검증
• Gate-level logic debugging
• Formal verification 이론

👉 “이 두 회로가 진짜 같은 기능이냐?”
이 질문에 수학적으로 답하는 도구다.

BDD의 예시를 보면 아래와 같다.

BDD는 “0/1로만 되는 간단한 규칙”을 질문 나무처럼 그려 놓은 거라고 보면 된다.

자세한 설명은 아래 문서 참고:

https://www.sciencedirect.com/topics/computer-science/binary-decision-diagram

Example: XOR f(x1,x2)=x1⊕x2

• Truth table of XOR:
  • x1=0,x2=0→f=0
  • x1=0,x2=1→f=1
  • x1=1,x2=0→f=1
  • x1=1,x2=1→f=0

이걸 BDD로 만들면, 변수 순서 x1→x2라고 할 때:

1. Root에 x1 노드가 하나 있다 (루트 노드).
2. x1에서
   • x1=0이면 왼쪽(0-edge)으로 내려가고
   • x1=1이면 오른쪽(1-edge)로 내려간다.
3. 그 아래에는 x2 노드가 각각 하나씩 있다.
4. 각 x2 노드에서 다시
   • x2=0이면 왼쪽, x2=1이면 오른쪽으로 내려가고,
   • 마지막에는 Leaf에 도착한다.

그림을 그려보면 아래와 같다.

즉, “입력 값을 따라서 0/1 가지를 내려가면, 맨 끝의 리프 값이 그 불 함수의 값”이 되는 구조다.

BDD가 왜 좋은가?

• 진리표는 행이 2^n개라서 n 커지면 복잡도 문제가 발생한다.
• BDD는 같은 패턴을 공유해서 노드를 재사용할 수 있다보니, Big(n)의 복잡도를 낮춘다.

정리하면,

• BDD = “Boolean function에 대해, 변수 → yes/no(0/1)로 내려가는 결정 그래프”라서, 입력값을 넣고 가지를 타고 내려가면 자동으로 결과에 도착하게 해 주는 구조라고 보면 된다.

자주 묻는 질문

kbdd, MiniSAT, Espresso·SIS는 각각 무엇을 하나요?

kbdd는 BDD 기반 canonical representation, MiniSAT은 SAT solving 기반 탐색, Espresso와 SIS는 논리 최소화를 담당합니다. 세 접근 모두 Boolean Function이 수학적으로 맞는지를 다루는 도구입니다.

BDD가 논리 동치 검증에 유리한 이유는 무엇인가요?

같은 Boolean function이면 항상 동일한 그래프 구조를 갖기 때문입니다. 논리식이나 회로 구조가 달라도 기능이 같으면 BDD가 같아져 동치 검증, 입력 조합 찾기, 변수 제거, 논리 복구에 쓸 수 있습니다.

BDD는 진리표와 무엇이 다른가요?

진리표는 행이 2의 n제곱개로 늘어나지만, BDD는 같은 패턴을 공유해 노드를 재사용하므로 복잡도를 낮출 수 있습니다. 입력값을 따라 0·1 가지를 내려가면 리프 값이 함수값이 되는 결정 그래프 구조입니다.

관련 글

• [VLSI CAD] Espresso in EDA
• [VLSI CAD] 최적해가 어려운 이유: NP-hard, heuristic, AI EDA
• [VLSI CAD] MiniSAT?
• [VLSI CAD] Two-Level Logic Minimization이 어려운 이유
• [VLSI CAD] placement가 “진짜로” 중요한 이유와, placer들이 쓰는 3가지 전략