24-杨晔.pdf

1、Copyright 芯华章科技股份有限公司 2024 All rights reserved从IP到系统的RISC-V敏捷验证方案杨晔 芯华章科技资深产品和业务规划总监Copyright 芯华章科技股份有限公司 2024 All rights reserved高性能RISC-V芯片的验证调试需求和挑战RISC-V core for xPU定制程度更高带来的验证需求从RV IP到多核SoC的过程需要大规模高性能的仿真和调试基于RISC-V的应用系统需要系统级验证及软件适配Copyright 芯华章科技股份有限公司 2024 All rights reservedRISC-V IP核的验证Part

2、 1Copyright 芯华章科技股份有限公司 2024 All rights reservedGalaxFV 快速完成处理器模块的形式化证明某国内车载处理器128指令压缩项目的属性证明：算法逻辑，数据通路证明状态空间巨大，数据位宽大，压缩算法证明收敛难度高，是传统Formal验证领域难点项目某世界主流形式验证工具30小时内无法完成验证收敛项目性能 GalaxFV性能 第三方编译时间证明时间证明时间128指令压缩15秒128 properties proven in 2 hours120 properties proven8 properties inconclusive in 30 hour

3、s评估结果：128条property证明结果正确，工具功能正确性能优越，2小时完成128条property的完备证明2 小时 VS 30 小时性能优势分析：GalaxFV基于字级模型(Word Level Model)建模，并为之开发出大量高性能字级形式验证引擎，相比于传统比特级模型(Bit Level Model)检测算法，字级求解引擎在处理复杂运算相关数据通路具备巨大优势。在保证验证目标一致的情况下，从验证方法学角度上优化property，减少证明复杂度，加速property收敛高性能自适应引擎调度系统，property自动分组与排序，实现复杂设计验证快速收敛Copyright 芯华章科技

4、股份有限公司 2024 All rights reserved基于GalaxEC HEC的C-RTL一致性证明，支持RISC-V的各种定制化算子完备的Datapath验证方案浮点运算、乘法单元、超越函数ldexp/pow等等，自带丰富的C原生算子模型支持AI芯片需要的FP16/BFloat16/TF32等数据类型算子；假设-保证和案例分割完全自动化；语法支持度广，C+11/Verilog/SystemVerilog Assertion基于Fusion Debug工具对证明（反例）进行波形和源代码调试；GalaxEC HECAssume EqualInputsUntimed Transactio

5、n Model ACycle Accurate Model BCompare Outputs at End ofTransaction(s)验证功能HEC证明用时其他工具用时FMUL162h+15h+Bfdot300+s8h未能证明FMUL64200+s8h未能证明支持RISC-V处理器扩展算子的C+模型到RTL、或C+模型之间的等价性验证基于高并发求解引擎的RISC-V验证案例40个算子的可证明性和性能均大幅提升Copyright 芯华章科技股份有限公司 2024 All rights reservedRISC-V 多核高速仿真Part 2Copyright 芯华章科技股份有限公司 2024

6、 All rights reservedRISC-V多核及SOC并行仿真验证 GalaxSim Turbo1-10Slow!100-1KFaster!1-10KFastest!Block0alwaysassignassignalwaysalwaysassignBlock1alwaysassignassignalwaysalwaysassignBlock2alwaysassignassignalwaysalwaysassignBlockNalwaysassignassignalwaysalwaysassignSingle ThreadPartition#1