don't-care로 비운 입력 한 행은 안전 동작을 만들지 않는다

“이 입력은 절대 들어오지 않는다”는 이유로 출력에 X를 적으면 합성기가 회로를 줄일 수 있다. 그런데 시스템에서 그 입력이 실제로 들어오면 출력은 무엇일까? 합성 don't-care는 특정 경우의 구현을 선택할 자유다. 회로가 그 경우를 감지해 경고하거나 안전하게 복구하도록 만드는 기능은 아니다. 자유를 준 조건이 실제 사용 조건과 맞는지 별도로 확인해야 한다.

한 행을 비우면 서로 다른 함수가 허용된다

1비트 입력 a·b에 대해 다음의 가상 명세가 있다고 하자. 00에서는 0, 01과 10에서는 1을 출력한다. 11에서는 두 입력이 동시에 활성화되는 경우를 시스템이 만들지 않는다고 가정해 출력값을 정하지 않았다.

마지막 행을 0으로 구현하면 XOR와 같은 함수다. 1로 구현하면 OR와 같은 함수다. 두 함수는 지정한 세 행에서 모두 같고, 마지막 행에서만 다르다. don't-care가 있는 원래 명세와 비교하면 둘 다 허용될 수 있지만, 두 구현을 아무 입력에서나 같은 함수라고 부를 수는 없다.

RTL에서 이 의도를 default: y = 1'bx 같은 형태로 표현할 수 있는 흐름도 있다. 다만 X를 적으면 특정 도구가 반드시 OR나 XOR 중 하나를 선택한다는 뜻은 아니다. 합성 설정과 다른 사용처, 라이브러리가 구현을 결정한다. 위 표는 선택의 자유를 설명하는 예이며 실제 매핑 결과가 아니다.

Yosys의 opt_expr 설명은 don't-care와 관련해 X의 전파 의미가 달라지는 최적화가 있을 수 있고, keepdc 옵션으로 해당 변환들을 제한할 수 있다고 설명한다. X를 포함한 RTL을 읽을 때는 단순한 0·1 진리표만으로 흐름 전체의 의미를 판단하지 않아야 한다. Yosys의 don't-care 관련 최적화 옵션

금지 조건은 누가 만들지 않아야 하는가

11을 외부 환경이 만들지 않는다는 계약이라면, 상위 회로가 두 요청을 동시에 보내지 않는지 확인해야 한다. 형식 검증에서 assume(!(a && b))를 넣으면 세 행만 검사하는 환경을 만들 수 있다. 그러나 그 가정을 넣은 증명은 실제 시스템이 동시에 두 입력을 올리지 않는다는 사실을 증명하지 않는다. SymbiYosys의 가정 의미

동시에 들어올 수 있는 요청을 단순히 편의상 제외했다면, 명세의 필요한 행을 삭제한 것이다. 상위가 정상 동작에서 11을 만들 수 있는데도 XOR 구현을 연결하면 결과는 0, OR 구현을 연결하면 1이 된다. 시스템이 우선순위를 기대하거나 에러 표시를 기대한다면 어느 쪽이든 그 요구를 검사하지 않은 채 통과할 수 있다.

금지 조합이 내부 상태에서 나온다면 책임도 달라진다. 초기·리셋 상태에서 시작해 전이가 항상 그 조합을 피한다는 근거가 필요하다. 밖에서 제공되는 입력 계약과 내부에서 증명해야 하는 도달 불가능 상태를 같은 이유로 assume 처리하면, 구현이 위반한 상태를 증명의 대상에서 지워 버릴 수 있다.

더구나 정상 동작의 도달성만으로 고장이나 일시적인 전원 상태까지 모두 설명되지는 않는다. 불법 조합을 만나면 특정 안전 출력이나 복구를 해야 한다는 요구가 있다면 그 행의 동작도 명세에 넣어야 한다. 정상 입력의 최적화 자유와 비정상 입력의 복구 요구를 함께 만족하는 구현을 찾아야 한다.

X를 기준으로 한 통과 결과의 범위

EQY의 safe-replacement 설명은 기준 gold의 X 출력을 gate의 구체적 값과 호환되는 것으로 비교한다. 따라서 위처럼 기준에서 11의 출력을 X로 표현했다면, gate가 11에서 0을 출력해도 1을 출력해도 그 행만으로 반례가 되지 않을 수 있다. 이 통과는 기준이 정하지 않은 행동에 정답을 만들어 주지 않는다. EQY의 formal X 해석

이를 11에서 반드시 출력이 1이어야 하는 요구의 증거로 사용하면 잘못이다. 그 요구를 갖고 싶다면 gold에도 알려진 1을 넣거나, 해당 동작을 별도 속성으로 정의해야 한다. gold의 X는 구현 자유를 준 자리이므로 특정 출력값을 요구하는 검사와 역할이 다르다.

시뮬레이션의 X 역시 실제 칩이 “정해지지 않은 전압”이라는 상태로 친절하게 알려 준다는 의미가 아니다. 실제 구현은 선택된 셀의 함수와 상태에 따라 값을 내보낸다. 시뮬레이션에서 경고처럼 보였던 X만을 기대해 불법 입력 처리를 설계하면 기능이 빠질 수 있다. keepdc 같은 옵션도 물리 회로에 경고 기능을 만들어 주는 것은 아니다.

don't-care를 사용하는 곳에는 제외한 조건과 그 조건을 보장하는 주체를 남겨 두는 편이 좋다. 외부 계약이면 상위 연결과 입력 생성기를, 내부 도달성이라면 초기 상태와 전이 관계를 확인한다. 환경이 바뀌면 그 근거도 다시 검사한다. 작은 회로를 얻는 이득은 유효한 자유에서 나와야 한다. 정하지 않은 행이 무엇인지 끝까지 유지할 때 최적화 결과와 시스템의 실제 책임이 어긋나지 않는다.