用图神经网络聚类硬件属性，加速多属性验证
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
- 基于电路功能嵌入与运行时统计聚类属性
- 在HWMCC基准上实现比现有方法更快的验证速度
- 适合做硬件形式化验证的工程师和研究者
多属性形式化验证一直是验证领域的长期挑战。如何高效地将属性分组协同求解，已有多种方案，包括基于属性影响锥（COI）的结构聚类，以及利用运行时设计与验证统计数据的方法。本文提出一种新方法，利用图神经网络（GNN）嵌入实现硬件电路的功能表征，结合运行时统计信息，构建有效的属性聚类策略，以提升多属性验证（MPV）中边界模型检查（BMC）的性能。该方法根据属性的功能嵌入与设计统计智能分组，显著加快了验证进程。在HWMCC基准上的实验结果表明，本方法优于当前最优技术。
原文摘要 · Abstract (English)
Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved together has inspired a number of proposals, ranging from structural clustering based on the property cone of influence (COI) to leverage runtime design and verification statistics. In this paper, we present an attempt towards functional clustering of properties utilizing graph neural network (GNN) embeddings for creating effective property clusters. We propose a hybrid approach that can exploit neural functional representations of hardware circuits and runtime design statistics to speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification (MPV). Our method intelligently groups properties based on their functional embedding and design statistics, resulting in speedup in verification results. Experimental results on the HWMCC benchmarks show the efficacy of our proposal with respect to the state-of-the-art.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。