블루스펙(Bluespec) 스타일의 하드웨어 설계에서는 사양을 한 번에 구현하는 대신, 정확성이 증명된 변환 규칙을 차례로 적용해 구현을 도출할 수 있다. 애덤 치플라라(Adam Chlipala)는 캐시 일관성을 갖춘 멀티코어 CPU를 예로 들어 이 방식이 모듈 단위의 검증과 최적화를 어떻게 연결하는지 설명한다.
멀티코어 CPU는 여러 실행 흐름을 동시에 처리하지만, 여러 캐시에 복제된 메모리 값이 서로 일치하도록 관리해야 한다. 이 캐시 일관성 프로토콜을 포함한 하드웨어는 검증하기 까다로운 대상이다. 치플라라는 미티(MIT) 박사과정생 무랄리 비자야라가반(Murali Vijayaraghavan)과 함께 이 문제를 연구하면서, 하드웨어 모듈을 따로 명세하고 검증한 뒤 더 큰 시스템의 정확성을 조합해 증명하는 방법을 발전시켰다고 설명한다. 이 작업은 블루스펙 설계의 모듈형 증명 틀로 이어졌다.
이 접근법에서는 하드웨어가 실행 중 주고받는 메서드 호출과 결과를 기록한 로그를 행동의 기준으로 삼는다. 구현이 사양을 만족한다는 것은 구현에서 가능한 로그가 사양에서 허용하는 로그의 부분집합이라는 뜻이다. 블루스펙은 모듈 간 통신을 메서드 호출로 표현하고, 가드 조건이 충족되지 않으면 호출 전체의 부수 효과를 되돌린다. 또 아무 메서드도 호출되지 않은 실행 단계는 로그에서 생략해, 사양과 구현이 같은 동작을 하되 필요한 실행 단계 수는 달라도 되도록 한다.
이 정제(refinement) 관계는 반사성과 추이성을 갖고, 큰 설계 안의 하위 모듈에도 변환 규칙을 적용할 수 있는 합성 성질을 갖는다. 예를 들어 증명된 큐 구현을 이상화된 큐 사양으로 바꾸거나, 큐로 연결된 여러 파이프라인 단계를 하나의 연산 노드로 축약하는 규칙을 사용할 수 있다. CPU와 메모리를 분리한 시스템이 명령어 집합 사양을 만족하고, 캐시 일관성 메모리 시스템이 단순한 메모리 사양을 만족한다는 정제도 함께 적용하면 사양에서 효율적인 구현까지 이어지는 변환을 구성할 수 있다.
각 변환 규칙을 일반적인 형태로 독립 증명해 두면, 규칙을 어떤 순서로 적용해도 기능적으로 올바른 구현을 얻는다. AI 에이전트가 규칙의 순서를 선택하게 할 수도 있지만, 성능처럼 형식화하지 않은 속성에서 만족스럽지 않은 설계를 고를 수는 있어도 기능 동작이 틀린 설계로 이끌 수는 없다고 치플라라는 설명한다.
이런 추론 방식은 Kami에서 구체화됐고, 이후 Fjfj로 단순화됐다. 더 세밀한 시간 추론을 지원하는 Kôika는 하드웨어 보안 구역의 타이밍 보안을 증명하는 데 사용됐다. 다만 이 변환 틀은 지금까지 주로 사람이 작성한 하드웨어 설계를 검증하는 데 쓰였으며, 사양에서 설계를 단계적으로 도출하는 방식의 적용 사례는 아직 제한적이라고 설명한다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요