arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2603.04450cs.LOcs.AIcs.LGcs.SE
收藏

MPBMC: 多属性有界模型检查与基于图神经网络的聚类

MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering

Indian Statistical Institute(印度统计研究所);IBM Systems(IBM系统公司);Texas Instruments(德州仪器)

Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee, Raj Kumar Gajavelly, Sudhakar Surendran

AI总结:

本文提出基于图神经网络的多属性有界模型检查方法,通过功能聚类提升多属性验证效率。

摘要:

多属性设计的正式验证一直是验证研究社区长期面临的挑战。提出一种有效策略,能够高效地将需同时解决的属性进行聚类,已激发了众多提案,从基于属性影响锥(COI)的结构聚类到利用运行时设计和验证统计信息。本文提出了一种利用图神经网络(GNN)嵌入进行属性功能聚类的方法。我们提出了一种混合方法,可以利用硬件电路的神经功能表示和运行时设计统计信息,以加快多属性验证(MPV)中有界模型检查(BMC)的性能。我们的方法根据属性的功能嵌入和设计统计信息智能地将属性分组,从而提高了验证结果的速度。在HWMCC基准测试中的实验结果表明,我们的方法在与现有最先进方法相比方面表现出有效性。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑