形式验证工具 文章 进入形式验证工具技术社区

利用先进形式验证工具来高效完成RISC-V处理器验证

• 我们在上一篇技术白皮书《基于形式验证的高效RISC-V处理器验证方法》中，以Codasip L31这款用于微控制器应用的32位中端嵌入式RISC-V处理器内核为例，介绍了一个基于形式验证的、易于调动的RISC-V处理器验证程序。它与RISC-V ISA黄金模型和RISC-V合规性自动生成的检查一起，展示了如何有效地定位那些无法进行仿真的漏洞。RISC-V的开放性允许定制和扩展基于RISC-V内核的架构和微架构，以满足特定需求。这种对设计自由的渴望也正在将验证部分的职责转移到不断壮大的开发人员社群。然而，随
• 关键字： 形式验证工具  RISC-V  验证