基于形式化方法的C模型和RTL实现逻辑等价性检验｜智猩猩国产EDA技术公开课预告

智猩猩一直关注国产EDA的技术突破和产品创新，并于2023年策划推出「 智猩猩国产EDA技术公开课 」，持续邀请该领域优秀企业的技术决策者与专家带来讲解。

9月12日19:30 ，「智猩猩国产EDA技术公开课」第6期将开讲，由 阿卡思微电子技术总监冯煌 主讲，主题为《 基于形式化方法的C模型和RTL实现逻辑等价性检验 》。

形式验证是一种基于数学推理的芯片设计验证方法，它通过对芯片设计的逻辑规范和实现进行严格的数学建模和分析，来确保芯片设计在所有可能的输入情况下都能正确地实现预期的功能。

等价性验证是形式验证的重要方法，主要用于比较两个设计在功能上是否完全等价，通常用于比较不同抽象层次的设计版本，比如C模型和RTL实现的逻辑、RTL设计和门级网表之间的等价性检验。

等价性验证可以在芯片设计流程的早期发现潜在的错误，避免错误在后续阶段被放大，从而降低设计成本和时间。同时，等价性验证不依赖于随机测试向量，能够提供更全面和准确的验证结果，且对于大规模复杂设计，等价性验证可以快速有效地检查设计的一致性。

阿卡思微电子自主研发的形式化验证工具AveCEC支持设计全流程，能独立于任何工具实现大规模芯片设计的形式化验证，采用数学方法确保设计实现和黄金设计一致，处理速度快，有较强的debug能力，能够快速查错。同时AveCEC支持复杂 datapath 优化、先进门钟设计优化，可以验证整个SOC设计，具有很强的可扩展性。

此次公开课，冯煌老师首先会介绍形验证的主要方法和流程，之后将重点讲解形式验证收敛方法、Sign-off检查中的C2RTL逻辑等价性验证。最后，冯煌老师将结合实际案例，解读香山RISC-V处理器的浮点乘法验证实现。