Arcane: 의미론적 클러스터링 및 MCTS 기반 규칙 탐색을 통한 어설션 감소 프레임워크

어설션 기반 검증 (Assertion-based Verification, ABV)은 하드웨어 설계가 의도된 사양을 준수하는지 확인하는 데 필수적입니다. 그러나 LLM 기반 프레임워크와 같은 기존의 자동화된 어설션 생성 방식은 종종 방대한 양의 중복된 어설션을 생성하며, 이는 시뮬레이션 효율성을 크게 저하시킵니다. 중복된 어설션으로 인한 시뮬레이션 오버헤드를 완화하기 위해, 본 논문은 효율적인 어설션 감소 프레임워크인 Arcane을 제안합니다. 이 프레임워크는 대규모 어설션 세트의 정확한 의미론적 분류를 위해 2단계 어설션 클러스터링 (Assertion Clustering) 방식을 통합하며, 효율적인 어설션 감소를 위한 최적의 규칙 적용 시퀀스를 탐색하기 위해 몬테카를로 트리 탐색 (Monte Carlo Tree Search, MCTS)을 채택합니다. Assertionbench [20]를 이용한 실험 결과, Arcane은 형식적 커버리지 (Formal Coverage)와 변이 탐지 (Mutation-detection) 능력을 완전히 보존하면서도 어설션 개수를 최대 76.2%까지 감소시켰습니다. 추가적인 시뮬레이션 연구를 통해 시뮬레이션 시간이 2.6배에서 6.1배까지 단축됨을 입증했습니다. 제안된 프레임워크는 https://anonymous.4open.science/r/Arcane1-0A6F/ 에서 공개되었습니다.