8月24日，国微芯受邀参与了备受瞩目的2023 RISC-V中国峰会。本届峰会以“RISC-V生态共建”为主题,结合当下全球新形势,把握全球新时机,呈现RISC-V全球新观点、新趋势。国微芯销售总监邓金斌在此次盛会中发表了主题为《基于形式化的高效RISC-V处理器验证方法》的演讲，探讨形式化验证技术，视野开阔、引人深思。
在此次演讲中，邓金斌先生通过产品介绍和深入的案例分析展示了 “芯天成”形式化验证工具在RISC-V处理器设计领域突出的应用优势。
芯天成
全功能形式化验证平台
“芯天成”形式化验证平台EsseFormal包括C to RTL to Netlist的等价性验证工具、属性验证工具，以及各种实用验证Apps。这些工具通过数学和逻辑推理及形式化规范语言，能够帮助芯片开发人员识别和解决系统中潜在的错误、漏洞和安全隐患，在数字芯片设计的各个环节发挥重要作用。
EsseFormal平台工具概述
高效率
验证香山RISC-V处理器
香山处理器项目由中科院计算所于2019年发起，经历两代微架构迭代，第三代昆明湖架构由北京开源芯片研究院牵头联合开发研制。香山处理器是一款基于RISC-V指令集架构的自研处理器，相对于一般处理器，其设计更加复杂，包含更多的指令、寄存器、内存等组件，非常容易出现验证盲点。
邓金斌先生指出，形式化工具在验证RISC-V处理器时，不仅要关注功能正确性和时序正确性，还需要考虑特殊的指令和功能、多个开源实现和变体的差异等等。因此，形式验证工具需要具备灵活和全面的验证能力，以及深入理解RISC-V指令集架构和处理器设计特点，才能满足这些额外的验证需求。
在第二代香山南湖版本处理器的验证案例中，EsseFormal平台的等价性验证工具EsseFECT成功验证了基于RISC-V的整形模块和浮点模块中各类算子的C-RTL功能一致性。
EsseFECT不仅验证了整形模块中加减、乘除、逻辑操作等基本算子的准确性，还涵盖了浮点模块中加减、乘除、开方等更加复杂的操作。这些验证不仅仅是为了确认各个算子的功能正确性，更是为了验证整个处理器在执行复杂算术操作时的稳健性和一致性。此外，EsseFECT还验证了整形和浮点数之间的转换及比较操作，确保了不同数据类型之间的无误转换和可靠比较，从而增强了处理器在不同数据处理场景下的可靠性。
国微芯
助力RISC-V生态发展
RISC-V作为一种开源指令集架构，正在迅速发展并得到广泛应用。然而，由于其复杂的指令集和灵活的定制化需求，验证RISC-V处理器的挑战也越来越大。国微芯不仅拥有自主研发的EsseFormal工具，还积极参与RISC-V生态系统的建设和推动。通过与生态伙伴的紧密合作，国微芯致力于推动RISC-V处理器的发展，加速国内开源处理器产业的壮大和创新。
