[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)로 내려가는 결정 그래프”라서, 입력값을 넣고 가지를 타고 내려가면 자동으로 결과에 도착하게 해 주는 구조라고 보면 된다.