针对RISC-V处理器的验证

实验室开发的硬件系统验证方法专注于系统级设计中的协议正确性，特别是缓存一致性等复杂逻辑的验证。作为高性能RISC-V处理器设计的一个验证实例，我们对香山处理器的缓存协议进行了系统验证。传统的仿真手段难以全面覆盖缓存协议的所有交互场景，但通过形式化验证方法，我们能对协议的关键属性进行严格检验，最终定位出多个难以察觉的潜在错误。这一方法不仅验证了香山处理器缓存协议的稳定性，同时也展示了形式化方法在复杂硬件系统验证中的独特优势。