99905银河[中国]精粹研究院|官方网站

8月24日，99905银河官方网站受邀参与了备受瞩目的2023 RISC-V中国峰会。本届峰会以“RISC-V生态共建”为主题,结合当下全球新形势,把握全球新时机,呈现RISC-V全球新观点、新趋势。99905银河官方网站销售总监邓金斌在此次盛会中发表了主题为《基于形式化的高效RISC-V处理器验证方法》的演讲，探讨形式化验证技术，视野开阔、引人深思。

此次演讲，邓金斌先生通过产品介绍和深入的案例分析展示了 “芯天成”形式化验证工具在RISC-V处理器设计领域突出的应用优势。

全功能形式化验证平台

“芯天成”形式化验证平台EsseFormal包括C to RTL to Netlist的等价性验证工具、属性验证工具，以及各种实用验证Apps。这些工具通过数学和逻辑推理及形式化规范语言，能够帮助芯片开发人员识别和解决系统中潜在的错误、漏洞和安全隐患，在数字芯片设计的各个环节发挥重要作用。

（EsseFormal平台工具概述）

香山RISC-V处理器验证

香山处理器项目由中科院计算所于2019年发起，经历两代微架构迭代，第三代昆明湖架构由北京开源芯片研究院牵头联合开发研制。香山处理器是基于RISC-V指令集架构的自研处理器，相对于一般处理器，其设计更加复杂，包含更多的指令、寄存器、内存等组件，非常容易出现验证盲点。

邓金斌先生指出，形式化工具在验证RISC-V处理器时，不仅要关注功能正确性和时序正确性，还需要考虑特殊的指令和功能、多个开源实现和变体的差异等等。因此，形式验证工具需要具备灵活和全面的验证能力，以及深入理解RISC-V指令集架构和处理器设计特点，才能满足这些额外的验证需求。

在香山南湖V2版本处理器的验证案例中，EsseFormal平台的等价性验证工具EsseFECT成功验证了基于RISC-V的整形模块和浮点模块中各类算子的C-RTL功能一致性。

EsseFECT不仅验证了整形模块中加减、乘除、逻辑操作等基本算子的准确性，还涵盖了浮点模块中加减、乘除、开方等更加复杂的操作。这些验证不仅仅是为了确认各个算子的功能正确性，更是为了验证整个处理器在执行复杂算术操作时的稳健性和一致性。此外，EsseFECT还验证了整形和浮点数之间的转换及比较操作，确保了不同数据类型之间的无误转换和可靠比较，从而增强了处理器在不同数据处理场景下的可靠性。

助力RISC-V生态发展

RISC-V作为一种开源指令集架构，正在迅速发展并得到广泛应用。然而，由于其复杂的指令集和灵活的定制化需求，验证RISC-V处理器的挑战也越来越大。99905银河官方网站不仅拥有自主研发的EsseFormal工具，还积极参与RISC-V生态系统的建设和推动。通过与生态伙伴的紧密合作，99905银河官方网站致力于推动RISC-V处理器的发展，加速国内开源处理器产业的壮大和创新。