RVFI로 바이트 하나의 부호 확장을 끝까지 검증하기

같은 RISC-V 명령을 한 코어는 두 클록 만에 끝내고, 다른 코어는 다섯 클록 만에 끝낸다. 내부 신호를 같은 시간에 비교하면 대부분 다르지만, 이것만으로 어느 코어가 틀렸다고 말할 수는 없다. RVFI는 명령이 ISA 관점에서 무엇을 했는지 관측하는 인터페이스다. 실행에 걸린 시간이 달라도, 명령 전후의 상태 변화가 ISA와 맞는지 같은 기준으로 검사할 수 있게 한다.

파이프라인 단계 대신 명령의 효과를 기록하기

RVFI는 RISC-V Formal Interface의 약자다. 코어가 명령 정보를 내보내는 출력 신호들로 구성되며, rvfi_valid가 1인 구간에서 해당 명령의 정보가 유효하다. 한 사이클에 여러 명령을 보고할 수 있도록 NRET개의 채널을 둘 수 있다. valid가 0일 때 데이터 필드가 임의의 값을 갖는 것은 그 자체로 명령 실행을 뜻하지 않는다. RVFI 원문 사양

기록에는 명령어 비트와 순서를 나타내는 order, 읽은 레지스터 주소와 실행 전 값, 쓴 레지스터 주소와 실행 후 값, 실행 전후 PC가 들어간다. 메모리를 읽거나 썼다면 주소와 바이트 마스크, 관련 데이터도 필요하다. 마이크로아키텍처마다 다른 forwarding 신호나 ALU 단계의 이름 대신, 명령의 입력 상태와 결과를 설명하는 정보다.

다만 결과 레지스터 하나만 보고하면 충분한 것은 아니다. 값이 맞아도 잘못된 주소에서 읽었거나, 다른 레지스터에 썼거나, 다음 PC가 달라졌다면 명령 전체는 틀렸다. RVFI의 여러 필드는 이 관계를 함께 확인할 수 있게 한다.

바이트 하나가 32비트 음수가 되는 과정을 따라가기

RV32 코어에서 LB x5, 3(x2)를 실행한다고 하자. x2의 실행 전 값은 0x00001000, 명령 PC는 0x00000100이며 주소 0x1003에 0x80이 저장돼 있다. 접근 가능한 메모리이고 예외가 없으며, 압축 명령이 아닌 32비트 LB라고 가정한다.

유효 주소는 x2에 즉시값 3을 더한 0x1003이다. LB는 8비트 값을 읽고 부호를 32비트로 확장한다. 0x80의 최상위 비트는 1이므로 결과는 0xFFFFFF80이다. LBU라면 0x00000080이 되겠지만 이 명령은 LB다. 공식 RV32I 사양은 기준 레지스터와 부호 확장한 오프셋으로 주소를 계산하고, LB와 LBU의 확장 방식을 구분한다. RISC-V RV32I의 load 정의

여기서는 RISCV_FORMAL_ALIGNED_MEM을 정의하지 않는 RVFI 구성을 사용한다. 메모리 필드는 접근한 바이트 자체를 가리키고, 읽은 0x80을 데이터의 낮은 바이트에 둔다. 설명에 필요한 일부 필드를 적으면 다음과 같다.

rs2를 읽지 않는 이 명령에서 rs2 주소와 값은 둘 다 0으로 출력하도록 선택할 수 있다. 메모리 읽기 데이터의 나머지 세 바이트는 이 예의 rmask가 검사 대상으로 지정하지 않는다. 이 부분을 무조건 0이어야 한다고 비교하면 인터페이스가 요구하지 않는 제한을 만들 수 있다.

또 정렬된 메모리 필드를 쓰는 구성과 섞으면 안 된다. 그 구성이면 이 바이트를 담은 4바이트 정렬 주소와 대응 바이트 위치로 보고해야 한다. RVFI 주소가 실제로 읽은 바이트를 직접 가리키는지, 정렬된 묶음의 시작을 가리키는지는 원문과 해당 define을 함께 확인해야 한다. 0x1003에서 바이트를 읽는 것 자체는 바이트 크기에 자연 정렬된 접근이다.

시간 차이를 제거해도 없어지지 않는 책임

이 명령을 두 코어가 각각 사이클 2와 사이클 5에서 보고한다고 가정하자. 같은 초기 상태와 같은 메모리 값을 사용했다면, ISA 검사는 두 기록의 위 관계를 같은 방식으로 판단할 수 있다. 한 코어가 값을 0x00000080으로 출력했다면, 완료 시간과 무관하게 LB의 부호 확장을 위반한 것이다. 반면 같은 값을 더 늦게 내보냈다는 사실은 이 의미 검사만으로 성능이나 제한 시간 위반이 되지는 않는다.

기록의 순서와 실행 간 의존성은 여전히 중요하다. 원문은 order가 중복이나 빈 번호 없이 명령 순서를 나타내야 하며, 재정렬된 보고도 원인 관계를 보존해야 한다고 정한다. 추측 실행 기록을 허용하는 구성에서는 rollback 규칙도 따라야 한다. 단순히 valid마다 번호를 하나 더 붙이는 로거가 모든 구현에 충분한 것은 아니다.

RVFI 연결 자체도 검증 대상이다. 코어는 잘못된 값을 사용했는데 관측 포트만 기준 모델의 정답을 내보낸다면, 포트 검사만으로 실제 구현이 검증되지 않는다. 메모리 버스와 보고 정보의 일관성, 내부 명령과 기록의 대응을 확인할 필요가 있다. 원문에는 외부 버스 관측을 연결하는 RVFI_BUS 확장도 설명돼 있다.

RVFI로 비교 기준을 바꾸면 파이프라인 구조를 일일이 맞추는 부담은 줄어든다. 그 대신 명령 하나가 읽고 쓴 상태를 정확히 보고해야 한다. 바이트 마스크, 부호 확장과 PC까지 작은 명령 하나를 끝까지 추적해 보면, 코어별 시간 차이를 걷어낸 뒤에도 ISA 검증에 필요한 정보가 무엇인지 분명해진다.