Btor2MLIR: A Format and Toolchain for Hardware Verification

당신이 미스터리를 풀려는 탐정이라고 상상해 보십시오. 하지만 단서들이 오직 소수의 전문가만이 읽을 수 있는 비밀 코드로 작성되어 있습니다. 컴퓨터 과학의 세계에서 이 "비밀 코드"는 컴퓨터 칩(하드웨어)이 어떻게 동작해야 하는지를 설명하는 언어입니다. 엔지니어들은 당신의 스마트폰부터 우주에 있는 인공위성까지 모든 것을 실행할 수 있는 칩을 만듭니다. 하지만 설계 과정에서 아주 작은 실수라도 발생하면 전체 시스템이 충돌하거나 이상하게 작동할 수 있습니다. 이를 방기하기 위해 연구자들은 "형식 기법(formal methods)"이라는 도구를 사용하는데, 이는 설계가 완벽하다는 것을 증명하는 초강력 맞춤법 검사기 역할을 하는 수학적 도구입니다.

오랫동안 이러한 맞춤법 검사기들은 서로 다른 언어를 사용해 왔습니다. 어떤 것들은 하드웨어 경진대회에서 인기 있는 형식인 "BTOR2"를 말했고, 다른 것들은 소프트웨어 컴파일러가 코드를 점검하는 데 사용하는 언어인 "LLVM-IR"을 말했습니다. 이는 마치 프랑스어를 영어로 번역하는 법만 아는 번역가와, 스페인어를 영어로 번역하는 법만 아는 또 다른 번역가가 있는 것과 같았습니다. 만약 프랑스어 번역가에게 스페인어 책을 번けて달라고 요청한다면, 결과는 낭패일 것입니다. 그때마다 매번 완전히 새로운 번역기를 만들어야 했습니다. 이 논문은 BTOR2MLIR이라는 새로운 마법 같은 번역기를 소개합니다. 이것은 중간에 위치하여 하드웨어 설계가 매번 바퀴를 다시 발명할 필요 없이 소프트웨어 도구들과 대화할 수 있게 해주는 보편적인 가교 역할을 합니다.

문제점: 너무 많은 방언, 부족한 가교

하드웨어 검증의 세계에서 BTOR2 형식은 하드웨어 모델 체킹 경진대회(HWMCC)와 같은 경진대회를 위한 회로 기술의 표준이 되었습니다. BTOR2를 디지털 회로가 숫자를 세거나, 더하거나, 오류를 확인하는 방식을 설명하는 매우 구체적이고 효율적인 방언이라고 생각하십시오. BTORMC와 같은 도구들은 이 방언을 읽고 회로가 안전한지 확인하도록 특별히 제작되었습니다.

하지만 소프트웨어 검증의 세계는 거대하고 강력합니다. SEAHORN과 같은 도구들은 LLVM-IR 언어로 작성된 소프트웨어 코드를 점검하는 데 전문가입니다. 이 도구들은 LLVM 컴파일러 인프라와 같은 거대한 프로젝트에 의해 수십 년 동안 정교하게 다듬어진 매우 성숙한 도구들입니다. 이들은 코드 최적화, 버그 찾기, 시뮬레이션 실행을 위한 내장 기능을 갖추고 있습니다.

문제는 이 두 세계가 거의 대화를 나누지 않는다는 점입니다. 하드웨어 설계를 검증하기 위해 강력한 소프트웨어 도구를 사용하려면, 연구자들은 커스텀 방식의 일회성 번역기를 작성해야 했습니다. 이는 마치 매번 사각형 못을 둥근 구멍에 억지로 끼워 맞추려는 것과 같았습니다. 이러한 번역기들은 이미 소프트웨어 도구에 존재하는 기본 기능(예: 숫자나 루프를 처리하는 방법)을 재구현해야 했으며, 이는 노력의 낭비와 잠재적인 오류로 이어졌습니다.

해결책: 만능 어댑터 (BTOR2MLIR)

이 논문의 저자인 워털루 대학교의 Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel은 더 나은 다리를 만들기로 결했습니다. 그들은 MLIR(Multi-Level Intermediate Representation)을 기반으로 한 새로운 형식과 툴체인인 BTOR2MLIR을 만들었습니다.

MLIR을 이해하기 위해, 이를 거대한 모듈형 레고 세트라고 상상해 보십시오. 매번 다른 종류의 집을 지을 때마다 처음부터 전체 성을 새로 만드는 대신, MLIR은 당신이 서로 결합할 수 있는 기본 브릭 세트(방언)를 제공합니다. 당신은 BTOR2와 똑같이 생기고 똑같이 작동하는 새로운 "하드웨어" 브릭을 정의할 수 있으며, 이것은 기존의 "소프트웨어" 레고 구조에 직접 끼워 맞출 수 있습니다.

이들의 새로운 도구가 작동하는 방식은 다음과 같습니다:

1. 번역기: 그들은 MLIR 내부에 "BTOR 방언"을 구축했습니다. 이것은 BTOR2 형식의 직접적이고 손실 없는 번환입니다. BTOR2 파일이 있다면, BTOR2MLIR은 이를 즉시 이 MLIR 방언으로 변환할 수 있습니다.
2. 가교: MLIR은 확장 가능하도록 설계되었기 때문에, 그들은 자신들의 BTOR 방언을 표준 LLVM 방언으로 변환하는 "변환 패스(conversion pass)"를 만들었습니다. 이것이 마법 같은 단계입니다. 이것은 하드웨어 설명을 가져와서 SEAHORN과 같은 소프트웨어 도구가 네이티브하게 이해할 수 있는 형식으로 바꿉니다.
3. 결과: 출력물은 소프트웨어 검증 엔진이 받아들여 분석할 수 있는 언어인 LLVM-IR입니다.

실험: 실제로 작동하는가?

팀은 단순히 다리를 만든 것에 그치지 않고, 다리가 무게를 견디는지 확인하기 위해 트럭을 몰고 건너갔습니다. 그들은 실제 세계의 하드웨어 벤치마크 모음(구체적으로 2020년 및 2019년 세트)을 가져와 새로운 툴체인을 통과시켜 실행했습니다.

먼저, 그들은 정확성을 확인했습니다. 그들은 BTOR2 파일을 가져와 MLIR 형식으로 변환한 다음, 다시 BTOR2로 변환했습니다. 그리고 원래의 파일과 라운드 트립(round-tripped)된 파일을 비교했습니다. 결과는 어떠했을까요? 두 파일은 동일했습니다. 안전 속성(회로가 따라야 하는 규칙)이 완벽하게 보존되었습니다. 심지어 원래의 도구들이 시간 초과되거나 메모리가 부족했던 까다로운 경우에도, 그들의 라운드 트립 버전은 때때로 문제를 해결해 냈는데, 이는 번역이 오류를 도입하지 않았음을 시사합니다.

다음으로, 그들은 성능을 테스트했습니다. 그들은 이 도구를 유명한 소프트웨어 모델 체커인 SEAHORN 및 빠른 솔버인 BOOLECTOR에 연결했습니다. 이 새로운 "하이브리드" 파이프라인을 BTOR2 전용으로 제작된 골드 스탠다드 도구인 BTORMC와 비교했습니다.

결과는 놀랍고 고무적이었습니다:

• 속도: 많은 경우, 하이브리드 파이프라인(BTOR2MLIR + SEAHORN + BOOLECTOR)은 전용 BTORMC 도구와 경쟁할 만한 수준이었으며, 때로는 더 빨랐습니다. 예를 들어, "19/mann" 카테고리의 벤치마크에서 하이브리드 접근 방식은 약 3,190초 만에 44개의 인스턴스를 해결한 반면, BTORMC는 더 많은 인스턴스에서 시간이 오래 걸리거나 시간 초과가 발생했습니다.
• 유연성: 이 도구는 나눗셈과 비트 벡터(bit-vectors)와 같은 복잡한 연산을 성공적으로 처리하여, MLIR의 "레고 브릭"이 하드웨어 로직의 무거운 작업을 처리할 수 있음을 입증했습니다.
• 한계: 저자들은 아직 자신의 도구가 할 수 없는 부분에 대해 솔직했습니다. 현재 비트 벡터와 배열은 지원하지만, "공정성(fairness)" 및 "정의(justice)" 제약 조건(시스템이 무한한 시간 동안 어떻게 행동하는지에 대한 규칙)은 아직 처리하지 못합니다. 또한 잘 작동하긴 하지만, 모든 카테고리에서 전용 하드웨어 도구들을 완전히 압도하지는 못했습니다. 그것은 강력한 경쟁자였지, 완전한 대체제는 아니었습니다.

이것이 왜 중요한가

이 논문은 하드웨어 검증의 모든 문제를 해결했다고 주장하는 것이 아닙니다. 대신, 새로운 사고방식을 제시합니다. 비디오 게임부터 웹 브라우저까지 모든 것을 구동하는 LLVM 컴 compiler 인프라의 성숙하고 견고한 인프라를 활용함으로써, 하드웨어 연구자들은 바퀴를 다시 발명하는 일을 멈출 수 있습니다.

저자들은 하드웨어 설계를 보편적인 언어로 번역한 다음, 강력하고 기존에 존재하는 소프트웨어 도구들을 사용하여 이를 검증할 수 있다는 것을 보여줍니다. 이는 신속한 프로토타이핑의 문을 엽니다. 만약 연구자가 새로운 검증 기법을 시도하고 싶다면, 전체 엔진을 새로 만들 필요 없이, 단지 자신의 아이디어를 MLIR 프레임워크에 꽂기만 하면 됩니다.

향ual적으로, 팀은 이 가교를 현재 소프트웨어에 사용되고 있지만 하드웨어의 버그를 찾는 데 혁명을 일으킬 수 있는 KLEE(심볼릭 실행 엔진) 및 LIBFUZZER(퍼징 도구)와 같은 더 많은 도구에 연결할 계획입니다. 또한 AIGER 및 SMT-LIB와 같은 다른 형식들도 생성할 계획입니다.

궁극적으로, BTOR2MLIR은 하드웨어와 소프트웨어 검증 사이의 벽이 허물어지고 있다는 개념 증명입니다. 이는 우리가 공통된 언어로 대화함으로써, 우리의 디지털 세계를 더 안전하고, 빠르고, 만들기 쉽게 만들 수 있음을 시사합니다.