智猩猩一直关注国产EDA的技术突破和产品创新，并于2023年策划推出「智猩猩国产EDA技术公开课」，持续邀请该领域优秀企业的技术决策者与专家带来讲解。
9月12日19:30，「智猩猩国产EDA技术公开课」第6期将开讲，由阿卡思微电子技术总监冯煌主讲，主题为《基于形式化方法的C模型和RTL实现逻辑等价性检验》。
形式验证是一种基于数学推理的芯片设计验证方法，它通过对芯片设计的逻辑规范和实现进行严格的数学建模和分析，来确保芯片设计在所有可能的输入情况下都能正确地实现预期的功能。
等价性验证是形式验证的重要方法，主要用于比较两个设计在功能上是否完全等价，通常用于比较不同抽象层次的设计版本，比如C模型和RTL实现的逻辑、RTL设计和门级网表之间的等价性检验。
等价性验证可以在芯片设计流程的早期发现潜在的错误，避免错误在后续阶段被放大，从而降低设计成本和时间。同时，等价性验证不依赖于随机测试向量，能够提供更全面和准确的验证结果，且对于大规模复杂设计，等价性验证可以快速有效地检查设计的一致性。
阿卡思微电子自主研发的形式化验证工具AveCEC支持设计全流程，能独立于任何工具实现大规模芯片设计的形式化验证，采用数学方法确保设计实现和黄金设计一致，处理速度快，有较强的debug能力，能够快速查错。同时AveCEC支持复杂 datapath 优化、先进门钟设计优化，可以验证整个SOC设计，具有很强的可扩展性。
此次公开课，冯煌老师首先会介绍形验证的主要方法和流程，之后将重点讲解形式验证收敛方法、Sign-off检查中的C2RTL逻辑等价性验证。最后，冯煌老师将结合实际案例，解读香山RISC-V处理器的浮点乘法验证实现。
第6期信息
主 题
《基于形式化方法的C模型和RTL实现逻辑等价性检验》
提 纲
1、形式验证简介
-模型检查、等价性验证、C2RTL等价性验证、定理证明
2、AveHlec验证流程
-准备C model、约束和断言、反例和调试
3、验证收敛方法
-Case Splitting、Assume guarantee、Cut point、乘法器的验证
4、Sign-off检查
-C++ Coverage、RTL Coverage：avecov
5、例子演示：香山浮点乘法的验证
-浮点介绍、Softfloat介绍、香山及RISC-V介绍、浮点乘法的验证
主 讲 人
冯煌，北京大学微电子硕士，曾先后在AMD、新思科技担任高级芯片设计工程师、高级产品工程师，现任北京华大九天旗下上海阿卡思微电子技术有限公司技术总监。主要负责形式验证产品的客户支持及支持团队建立与管理，与各大芯片设计公司保持长期深入的产品沟通，负责产品建议及性能测试与验证。
直 播 时 间
9月12日19:30-20:30
报名方式
对公开课感兴趣的朋友，可以扫描下方二维码添加小助手陈晨进行报名。已经添加陈晨的老朋友，可以给陈晨私信，发送“国产EDA06”即可报名。我们会为报名成功的朋友推送直播链接。
同时，本次公开课也组建了交流群，直播开始前会邀请相关朋友入群交流。
往期回顾
「智猩猩国产EDA技术公开课」由智猩猩芯片与算力教研组策划推出，聚焦国产EDA的技术突破和产品创新，目前已完结5期。来自海思、芯华章、上海立芯、奇捷科技、思尔芯的5位技术决策者和专家先后进行了直播讲解。
需要观看回放的朋友，可以关注摩崖芯公众号，回复关键词【国产EDA往期回放】获取。
