技术论文题为“通过句E-Graph重写Datapath公司验证”是由英特尔公司和伦敦帝国理工学院的研究人员发表。
“datapath公司的正式验证电路是具有挑战性的,因为他们受到强烈的优化工作,在设计阶段。工业供应商和设计公司部署等价性检查对黄金或现有的参考设计满足正确性问题。最先进的datapath公司等价性检查工具部署一套技术,包括重写。我们提出一个重写框架部署进行依赖重写e-graph数据结构的基础上,提供一个强大的助理现有工具。重写的e-graph可以生成路径之间的参考设计和实现,可以检查一个值得信赖的行业工具。我们将演示如何生成的中间证明助理使收敛在一个先进的工具,没有工业工具运行24小时,没有取得进展。中间证明自动引入的助理也减少总运行时至多6 x的证据。”
找到技术论文。2023年8月出版(预印本)。
懦夫,撒母耳,埃米利亚诺·Morini布赖恩•谭Theo Drane,乔治Constantinides。通过句E-Graph重写“Datapath公司确认。“arXiv预印本arXiv: 2308.00431 (2023)。
相关阅读
设计和验证方法分解
随着芯片越来越复杂,现有的工具和方法到极点。
形式验证知识中心
留下一个回复