科研之友
微信
新浪微博
Facebook
分享链接
摘要
随着硬件设计复杂性和规模的大幅度提升，硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术，可以自动构建反例路径，也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。为了提高验证的规模和效率，硬件验证算法设计逐渐从底层的比特级向更高的抽象级别转变。研究目标是设计一个新型有效的字级IC3算法。针对研究目标，提出了一种将变量隐藏抽象和隐式抽象结合的字级IC3算法IC3VA。该方法尝试将变量隐藏抽象和IC3算法相结合，并设计了对应的泛化和精化方案。在开源社区和硬件验证大赛收集的测试集上和基于谓词抽象的方法进行对比，实验结果显示了基于变量隐藏抽象的IC3算法的有效性。
- 单位
