CREST：使用ANSI-C参考规范进行硬件形式化验证
CREST: Hardware Formal Verification with ANSI-C Reference Specifications
摘要：
本文介绍了CREST，一个原型前端工具，旨在作为一个附加的商业EDA形式验证环境。CREST是CBMC有界模型检查器C的一个适应，CBMC有界模型检查器是一个广泛用于软件分析和属性验证的学术工具。它利用CBMC的功能来处理以任意ANSI-C编写的硬件数据路径规范，而不限制对可合成子集的限制。我们简要勾勒了我们的工具的架构，并显示其使用范围内的验证案例研究。
英文摘要：
This paper presents CREST, a prototype front-end tool intended as an add-on to commercial EDA formal verifcation environments. CREST is an adaptation of the CBMC bounded model checker for C, an academic tool widely used in industry for software analysis and property verification. It leverages the capabilities of CBMC to process hardware datapath specifications written in arbitrary ANSI-C, without limiting restrictions to a synthesizable subset. We briefly sketch the architecture of our tool and show its use in a range of verification case studies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
