---
title: "합성 전후의 등가성은 초기 상태와 출력 시점까지 맞아야 한다"
author: "브레이브브라우저쓰자"
published_at: "2026-10-20T09:21:03.461Z"
updated_at: "2026-10-06T01:20:41.401Z"
tags: ["sequential equivalence"]
canonical_url: "https://ariser.io/@writer_a9817d5a8de0/%ED%95%A9%EC%84%B1-%EC%A0%84%ED%9B%84%EC%9D%98-%EB%93%B1%EA%B0%80%EC%84%B1%EC%9D%80-%EC%B4%88%EA%B8%B0-%EC%83%81%ED%83%9C%EC%99%80-%EC%B6%9C%EB%A0%A5-%EC%8B%9C%EC%A0%90%EA%B9%8C%EC%A7%80-%EB%A7%9E%EC%95%84%EC%95%BC-%ED%95%9C%EB%8B%A4"
ai_assisted: true
---

# 합성 전후의 등가성은 초기 상태와 출력 시점까지 맞아야 한다

이 글은 AI가 활용됐습니다.

[원문](https://ariser.io/@writer_a9817d5a8de0/%ED%95%A9%EC%84%B1-%EC%A0%84%ED%9B%84%EC%9D%98-%EB%93%B1%EA%B0%80%EC%84%B1%EC%9D%80-%EC%B4%88%EA%B8%B0-%EC%83%81%ED%83%9C%EC%99%80-%EC%B6%9C%EB%A0%A5-%EC%8B%9C%EC%A0%90%EA%B9%8C%EC%A7%80-%EB%A7%9E%EC%95%84%EC%95%BC-%ED%95%9C%EB%8B%A4)

합성 결과의 레지스터 이름과 논리 구조가 RTL과 달라도 기능은 같을 수 있다. 반대로 계산식이 맞아 보여도 출력이 한 클록 늦으면 외부 회로가 보는 동작은 달라진다. sequential equivalence는 이 차이를 다룬다. **한순간의 출력값이 아니라, 같은 입력 이력에서 관측되는 상태와 출력의 시간 관계**를 비교하는 것이다.

## 상태가 있는 회로의 같음을 정하기

조합 회로라면 입력 하나를 넣었을 때 두 출력이 같은지 비교할 수 있다. 상태가 있는 회로에서는 초기 상태부터 정해야 한다. 같은 입력을 넣어도 앞서 어떤 값이 저장됐는지에 따라 출력이 달라지기 때문이다. 기준 회로와 변경 회로에 같은 입력을 주고, 정해진 초기 조건 아래에서 관측 출력의 관계가 모든 동작 동안 유지되는지 확인한다.

EQY의 공식 설명은 모든 플립플롭이 고정값으로 초기화되고 don't-care가 없는 경우, 두 회로의 출력을 비교하는 miter로 등가성을 안전 속성으로 표현할 수 있다고 설명한다. 여기서 기준을 gold, 비교 대상을 gate라고 부르지만, gate가 반드시 실제 배치 배선까지 끝난 회로일 필요는 없다. RTL 리팩터링의 전후 버전에도 같은 종류의 검사를 적용할 수 있다. [EQY의 등가성 정의](https://yosyshq.readthedocs.io/projects/eqy/en/latest/xprop.html)

예를 들어 같은 동기식 리셋으로 0이 되는 8비트 상태 q가 있고, enable이 1일 때마다 3을 더한다고 하자. 기준 회로는 `q + 3`, 변경 회로는 `q + 1 + 2`를 저장한다. 결과는 모두 8비트로 잘리므로 254에서 시작하면 두 회로 모두 1이 된다. enable=0이면 기존 값을 유지한다.

두 회로의 q가 같다면 다음 q도 같다는 관계를 256개 상태와 enable 두 경우에 대해 확인할 수 있다. 공통 리셋이 두 상태를 같게 시작시킨다는 사실과 결합하면, 이 작은 회로에서는 같은 상태 관계가 계속 유지됨을 설명할 수 있다. 이는 식과 상태 전이를 비교한 가상 예이며 실제 EQY 실행 결과를 보고하는 것은 아니다.

## 답이 같아도 한 클록 늦으면 다른 계약이다

이제 변경 회로에 출력을 한 번 더 저장하는 레지스터를 추가하자. 리셋 직후 enable=1인 첫 에지에서 기준 출력은 3이 되지만, 변경 출력은 이전 q인 0을 내보낸다고 가정한다. 그다음 에지에서 3을 내보낼 수 있어도 같은 에지의 출력은 같지 않다.

처리한 숫자가 같다는 이유로 이 차이를 등가라고 부를 수는 없다. 외부가 매 에지 출력을 읽는 계약이라면 파이프라인 지연은 기능의 일부다. 지연을 허용하는 비교를 하고 싶다면 어느 입력과 어느 출력이 대응하는지, valid와 리셋 직후 비어 있는 구간을 어떻게 처리할지 관계를 새로 정해야 한다. 단순한 같은 사이클 출력 비교가 그 계약을 자동으로 만들어 주지는 않는다.

내부 구조가 크게 달라졌을 때도 비교할 관계가 중요하다. 이름이 비슷한 두 레지스터가 같은 역할인지 먼저 살펴야 하고, 반대로 이름이 달라도 같은 상태를 표현할 수 있다. EQY는 net matching과 collect·partition 규칙으로 비교 대상을 나누고 각 부분에 증명 전략을 적용한다. 매칭은 증명할 대응을 구성하는 단계이지, 이름이 같다는 이유만으로 동작이 같아졌다는 결론은 아니다. [EQY의 matching·partition 설정](https://yosyshq.readthedocs.io/projects/eqy/en/latest/config.html)

## 초기 X를 양쪽에 똑같이 해석하지 않는 경우

초기값이 없는 레지스터나 don't-care가 있으면 “같다”의 뜻은 더 조심스러워진다. EQY는 safe-replacement라는 방향성이 있는 관계를 사용한다. 같은 입력에서 gate가 보여 줄 수 있는 출력이 gold의 허용 동작과 호환돼야 한다는 뜻이다. 일반적인 대칭 비교처럼 두 회로의 역할을 바꿔도 언제나 같은 결론이 나오지는 않는다.

가장 작은 예로, 초기화되지 않은 q를 그대로 출력하고 이후에도 변경하지 않는 gold를 생각해 보자. gate는 q를 0으로 고정한다. gold의 초기 X에 대해 gate의 0이 허용되는 구체화일 수 있다. 그러나 역할을 바꾸면 새 gold는 0만 출력하는데, 새 gate의 미정 상태는 1도 선택할 수 있다. 그 동작은 새 기준의 0과 호환되지 않는다.

공식 문서에서 gold는 0·1·X의 3값 의미로, gate의 X는 제약 없는 2값 선택으로 해석한다. gold 출력의 X는 gate의 어느 값과도 호환되지만 gold의 알려진 0을 gate의 1로 바꾸는 것은 허용하지 않는다. 이 모델의 X는 실리콘이 물리적으로 X라는 전압을 출력한다는 뜻이 아니다. 또한 초기 X를 모두 임의의 don't-care로 간주해 시스템 요구를 생략해도 된다는 허가도 아니다. [EQY의 formal X 해석](https://yosyshq.readthedocs.io/projects/eqy/en/latest/xprop.html)

리셋 후에만 출력을 유효하게 사용하는 설계라면 그 시작 조건과 관측 구간을 비교에도 반영해야 한다. 불법 입력에서의 동작을 제외한다면 무엇이 불법인지 환경 계약에 남겨야 한다. 설정으로 X를 제거하거나 초기 상태를 바꿨다면, 증명한 대상 역시 그 설정을 적용한 회로라는 사실을 기록한다.

합성 전후의 기능 보존을 판단할 때는 PASS라는 단어 앞에 조건을 붙이는 편이 정확하다. 어떤 입력을 허용했는지, 어디서 시작했는지, 어느 출력을 어떤 시간 관계로 비교했는지, gold의 미정 값을 어떻게 해석했는지가 그 조건이다. 이들이 실제 사용 계약과 맞아야 구조를 바꾼 회로를 안심하고 같은 자리에 넣을 수 있다.