컴파일러가 만든 회로를 같다고 부르려면 무엇을 비교해야 할까
컴파일러 최적화 전후의 회로가 같은 답을 냈다는 설명에는 빠진 질문이 있을 수 있다. 같은 답이 어느 시점에 나왔는가? 리셋 뒤 같은 상태에서 출발했는가? 출력이 막힐 때도 입력을 잃지 않았는가? 하드웨어 IR 동치성을 확인하려면 비교할 의미를 먼저 정해야 한다. 숫자 하나의 일치만으로는 회로 전체의 동작을 설명하기 어렵다.
첫 번째 층은 값의 의미다. 같은 덧셈 기호를 썼어도 폭과 절단 위치가 다르면 결과가 달라진다. 다음 두 모델은 8비트 무부호 입력 a, b를 받고 출력은 16비트라고 하자.
원래 모델: 8비트 덧셈 결과를 만든 뒤 16비트로 zero-extend
변경 모델: 입력을 각각 16비트로 zero-extend한 뒤 덧셈
a=200, b=100이면 원래 모델은 300을 8비트로 절단해 44를 내보낸다. 변경 모델은 300을 그대로 내보낸다. 0부터 255까지 모든 입력 쌍 65,536개 중 합이 256 이상인 쌍은 32,640개다. a가 1일 때 해당 b는 1개, a가 2일 때는 2개이며, 마지막에는 255개이므로 1+…+255로 셀 수 있다. 대부분 작은 값만 넣은 시험으로는 이 차이를 놓치기 쉽다.
반면 두 모델 모두 마지막에 8비트로 절단하도록 계약을 바꾸면 이 덧셈의 낮은 8비트는 모든 입력에서 같다. 그러므로 넓은 연산으로 바꾸는 변환 자체를 항상 맞거나 항상 틀리다고 말할 수 없다. 어느 비트가 관찰되는지와 절단이 어떤 후속 계산보다 앞에 있는지가 판단에 필요하다. 여기의 계산은 완전한 작은 입력 공간을 직접 비교한 예이며 실제 컴파일러에서 오류를 발견했다는 뜻은 아니다.
두 번째 층은 시간이다. 입력 x=5를 경계 0에서 받고 y=x+1을 경계 1에 내는 회로와, 경계 2에 내는 회로는 값만 보면 둘 다 6이다. 하지만 한 사이클 뒤 결과를 요구하는 연결 회로에는 서로 대체할 수 없다. 같은 클록의 출력들을 직접 비교하는 동치 검증에서 지연 차이는 관찰 가능한 차이다.
변경 가능한 지연을 인터페이스가 허용한다면 세 번째 층인 거래의 의미를 볼 수 있다. valid와 ready가 함께 성립해 수락된 입력마다 결과가 정확히 한 번 나오고, 필요한 순서를 지키는지 비교하는 방식이다. 출력 준비 신호가 내려간 구간에서도 값과 상태를 유지하고, 입력을 더 받을 수 있다고 약속한 만큼 보관해야 한다. 이렇게 정한 비교를 쓰려면 두 회로의 수락 사건을 어떻게 대응시킬지도 명확해야 한다. 늦게 나온 값만 골라 같은 수열로 보이게 하는 것은 입력 손실이나 중복을 숨길 수 있다.
실제 도구는 이 계약을 자동으로 모두 추측하지 않는다. YosysHQ의 EQY는 gold와 gate 설계를 읽고 대응 구간을 구성해 RTL 동작의 동치성을 검증하는 도구다. 공식 예제는 별도 쉬프터들을 공유 구조로 바꾼 회로를 비교하며, 시프트 양의 입력 비트를 잘못 고른 경우 반례를 보여 준다. EQY가 임의의 고수준 IR을 그대로 받아 모든 변환을 증명한다는 설명과는 범위가 다르다. YosysHQ EQY, Getting Started
증명의 초기 상태도 결과를 바꾼다. 모든 플립플롭의 초기값이 정해진 모델과 일부가 미정인 모델은 같은 비교가 아니다. EQY는 미정 값이 포함될 때 gold의 허용 행동을 gate가 안전하게 대체하는 관점으로 다룬다. 이는 방향이 있는 관계이며 두 설계를 바꾸어 놓아도 같은 의미의 결과가 나온다고 가정할 수 없다. 리셋으로 정해져야 할 값이 gold에서 계속 미정이면 그 출력에 대한 요구가 너무 약해질 수 있다. EQY, Equivalence and X-Propagation
검증 깊이의 숫자 역시 맥락을 읽어야 한다. 단순히 처음 10사이클만 비교해 차이가 없었다면 그 이후를 증명한 것은 아니다. 그러나 EQY의 sat 전략은 k-induction을 사용하고, sby 전략은 prove 모드에서 선택한 엔진을 사용한다. depth 10이라는 설정이 붙어 있어도 귀납 조건까지 성립해 증명을 마친 결과는 10사이클 시험과 의미가 다르다. 반대로 도구가 증명을 완료하지 못한 사실만으로 두 회로가 반드시 다르다고 결론낼 수도 없다. EQY Strategies, sat·sby
하드웨어 IR 동치성에 필요한 첫 작업은 비교표의 PASS를 얻는 일보다 비교 문장을 정확히 쓰는 일이다. 관찰할 비트, 출력 시점 또는 거래 대응, 초기 상태와 허용 입력을 적어 보자. 그 조건에서 반례를 찾거나 증명을 완료했다는 근거가 붙을 때, 최적화가 하드웨어 의미를 보존했다는 말을 검토 가능한 주장으로 만들 수 있다.