了解一种使用Operational SVA来形式化RISC-V ISA的保护RISC-V IP的方法。本文说得到的断言集没有差距和不一致。
RISC-V处理器ip正越来越多地集成到用于各种应用的片上系统设计中。然而，目前仍缺乏支持高完整性、可信赖集成电路的专用功能验证解决方案。本文研究了一种高效、新颖、基于形式化的RISC-V处理器验证方法。RISC-V ISA是在一组Operational SystemVerilog断言中形式化的。每个断言都根据处理器的RTL模型进行正式验证。至关重要的是，断言集随后在数学上被证明是完整的，并且没有空白，从而确保所有可能的RTL行为都已被检查。这个系统验证过程可以检测到RTL代码中存在的蓄意硬件木马和真正的功能错误。该解决方案使用商业上可用的正式工具在开源RISC-V实现上进行了演示，可以说是对之前发布的RISC-V ISA验证方法的重大改进，提高了基于RISC-V设计的硬件保证和信任。
欲了解更多，请点击这里。
|
|
|
|
|
|
|
|
留下回复