unique case가 약속하는 것과 불법 입력에서 남는 것

디코더의 case 앞에 unique를 붙이면 조건이 더 안전해진 것처럼 보인다. 시뮬레이터가 실수를 알려 주고 합성기도 병렬로 처리할 수 있다니 유용한 선언이다. 하지만 unique case는 잘못된 입력을 안전한 입력으로 바꾸는 장치가 아니라, 조건의 배타성과 경우의 범위에 대해 설계자가 약속하는 문법이다. 약속이 현실과 어긋나면 경고를 하나 추가하면서 다른 위험을 만들 수도 있다.

여기서는 두 개의 동작과 비활성 상태를 선택하는 작은 디코더를 생각하자. mode=0은 비활성, 1은 읽기, 2는 쓰기이고 3은 불법 입력이라고 가정한다. 불법 입력에서 동작을 중단해야 하는지, 오류를 보고해야 하는지는 시스템 요구사항으로 따로 정해야 한다.

default를 비워 둔 순간 추가되는 약속

always_comb begin
  read_en  = 1'b0;
  write_en = 1'b0;
  unique case (mode)
    2'd0: ;
    2'd1: read_en  = 1'b1;
    2'd2: write_en = 1'b1;
  endcase
end

정상 값에서는 한 case만 일치한다. 그러나 mode=3이면 아무 항목도 일치하지 않는다. 앞에서 read_en과 write_en을 0으로 기본 대입했으므로 RTL 시뮬레이션의 출력은 0, 0이다. 동시에 default가 없는 unique case의 불일치 검사에서 경고가 발생할 수 있다.

여기서 위험한 해석은 “기본값을 넣었으니 실제 회로에서도 mode=3은 반드시 두 출력을 0으로 만든다”다. unique 선언은 열거한 경우가 모두를 포괄한다는 정보를 합성에 전달할 수 있다. 도구는 열거하지 않은 입력을 정상 운용에서 발생하지 않는 경우로 활용해 최적화할 수 있다. 이 경우 불법 입력에 대한 하드웨어 동작을 시뮬레이션의 기본값만으로 보장해서는 안 된다.

mode=3에서도 아무 동작이 일어나지 않아야 한다면 default를 통해 그 동작을 분명히 정의해야 한다. 그리고 불법 입력이라는 사실도 별도의 검사로 표현한다.

always_comb begin
  read_en  = 1'b0;
  write_en = 1'b0;
  unique case (mode)
    2'd1: read_en  = 1'b1;
    2'd2: write_en = 1'b1;
    default: ;
  endcase
end

assert property (@(posedge clk) disable iff (!rst_n)
  mode inside {2'd0, 2'd1, 2'd2});

default가 있는 unique case는 항목이 없을 때 default로 처리하므로, 불법 mode가 자동으로 경고된다고 기대할 수 없다. 그래서 합법 입력 집합을 따로 검사했다. 출력의 정의와 입력의 합법성은 서로 다른 요구다. 위 assertion은 reset 이후 매 에지에서 mode가 의미 있다는 가정 아래의 예제다. mode가 특정 valid 사이클에만 의미 있다면 검사도 그 valid로 제한해야 한다.

하나도 맞지 않는 것과 둘이 맞는 것은 다르다

unique case의 또 다른 계약은 case 항목이 동시에 여러 개 일치하지 않는다는 것이다. 와일드카드를 사용하면 이 약속을 깨기 쉽다.

unique casez (request)
  3'b1??: chosen = 2'd2;
  3'b?1?: chosen = 2'd1;
  3'b001: chosen = 2'd0;
  default: chosen = 2'd3;
endcase

request=3'b110이면 첫 번째와 두 번째 항목이 모두 일치한다. 시뮬레이션은 먼저 적힌 항목을 실행하면서 unique 위반을 경고할 수 있다. 반면 합성 도구에는 배타적인 항목이라는 약속을 줬으므로, 코드의 첫 항목 우선순위가 위반 입력에서도 보존된다고 기대하기 어렵다.

이 코드의 의도가 높은 번호의 요청 우선이라면 조건이 겹치는 것이 정상이다. 그때에는 우선순위를 표현하는 if-else 체인 같은 구조가 의도에 맞다. 동시에 켜진 요청을 불법으로 보는 디코더라면 입력의 one-hot 성질을 별도로 확인해야 한다. unique를 붙이는 것만으로 외부 요청이 배타적으로 변하는 것은 아니다.

lowRISC의 case 지침은 unique와 default, 각 출력의 기본 대입을 함께 다룬다. full_case나 parallel_case 같은 주석 기반 힌트가 왜 위험한지도 설명한다. 핵심은 최적화 정보와 실행 가능한 동작 정의를 어긋나지 않게 만드는 일이다.

assertion은 검사지만 assume은 범위다

unique case를 검증하기 위해 형식 도구를 쓴다면 어떤 입력을 허용했는지 다시 봐야 한다. mode가 합법이라는 assertion을 세우면, 불법 mode가 도달할 수 있는지를 반례로 찾는다. 같은 조건을 assume으로 넣으면 도구는 처음부터 불법 mode를 탐색 대상에서 제외한다. 그 가정 아래의 디코더는 올바르게 증명될 수 있지만, 입력 생성기가 정말 그 가정을 지킨다는 증거는 별도로 필요하다.

OpenTitan의 형식 검증 문서는 속성 검증에서 가정과 검사를 사용하는 흐름을 제공한다. 디코더에 적용할 때 유용한 관점은 “좋은 입력만 넣으면 출력이 맞다”와 “시스템이 항상 좋은 입력만 만든다”를 나눠 확인하는 것이다. 두 명제가 모두 필요할 수 있다.

또 RTL 단계의 경고가 충분한 고장 검출 장치는 아니다. 합성 이후 상태 인코딩이나 논리가 바뀔 수 있고, fault로 생기는 불법 조합은 정상 실행의 도달 가능성 가정과 다르다. 불법 상태에서도 안전한 출력을 반드시 보장해야 하는 회로라면 그 요구를 명시하고 구현 단계에서 유지되는지 확인해야 한다. unique는 검증 속성의 일부를 표현할 뿐, 별도의 보호 회로를 자동으로 넣는 기능이 아니다.

선언 하나보다 명확한 세 문장

unique case를 리뷰할 때에는 세 가지를 나눠 말할 수 있어야 한다. 정상 입력의 집합은 무엇인지, 그 집합에서 항목은 하나만 일치하는지, 집합 밖의 입력에서는 어떤 출력을 내야 하는지다. 앞의 두 질문만 답하고 마지막을 생략하면 “정상적으로는 안 나온다”는 가정이 실제 실패 동작을 대신하게 된다.

처음의 디코더에서 unique가 유용한 이유는 분명하다. 배타적으로 선택되어야 하는 동작에 중첩이 생겼다는 사실을 발견하게 해 준다. 하지만 그 유용함은 약속이 정확하고 검사 결과를 실제로 처리할 때 생긴다. unique case를 안전하게 쓰는 방법은 선언을 더 믿는 것이 아니라, 선언이 전달하는 약속과 불법 입력의 동작을 각각 명확하게 적는 것이다.