中文 英语
系统与设计
的意见

核安全控制器的FPGA等价性检验

当芯片故障的后果可能是致命的时,挑战和解决方案。

受欢迎程度

每个芯片开发团队都希望找到并修复他们在硅前验证中可能存在的所有错误。用芯片来解决培育实验室中发现的问题会带来高昂的成本和产品延误;在现场发现的bug修复成本甚至更高。但对于一些应用,包括军事/航空航天、植入医疗设备和自动驾驶汽车,有缺陷的芯片的后果可能是致命的。核电站的电子系统是具有极高核查标准的设计的另一个明显例子。在OneSpin的就职典礼上渗透在慕尼黑的用户小组会议上,我们的一位专家用户就用于核应用的FPGA设计的形式等效性检查进行了引人入胜的演讲。

Jürgen Dennerlein是Framatome GmbH的产品开发、I&C硬件开发专家和平台架构师。他首先介绍了法马通公司,这家拥有60年历史的公司为世界各地的92座核电站提供了设备。他们设计工厂,提供蒸汽供应系统,设计和制造部件和燃料组件,集成自动化系统,并为所有类型的核反应堆提供服务。Jürgen专门从事核蒸汽供应系统的仪器仪表和控制(I&C)。他自豪地报告说,法马通已经在欧洲、亚洲、南美和北美17个国家的44座核电站安装了82套安全I&C系统。

他们创造的产品受到标准的严格监管,特别是IEC SC 45A标准系列中的IEC 62566。虽然这个标准没有规定开发过程,但它包含了Jürgen团队使用的验证流程中很重要的要求。例如,验证活动必须由独立于执行设计和实现的人员进行。该标准侧重于实现后验证和检测逻辑简化和门重复的潜在不利影响,以及由开发工具本身或其使用引起的潜在故障。Framatome对标准添加了另一个补充要求:验证活动必须由独立于用于设计和实现的工具运行。

一种完全符合标准范围的验证方法是形式等价检查,以验证芯片的后路由网络列表在数学上与原始RTL设计等效。与模拟不同,等价性检查是详尽的,不需要测试向量。Jürgen指出,基于定向测试的网表模拟很难发现来自逻辑综合或位置和路线工具的系统错误,因为测试向量可能不会激发正确的转角案例来触发错误。

Framatome I&C设计使用fpga,这增加了流程的复杂性。FPGA实现工具提供了广泛的优化,其中许多优化显著地改变了设计中的状态元素。传统的asic风格的组合等价性检查依赖于RTL中的状态元素和网络列表中的状态元素之间的直接映射。对于fpga,顺序等价性检查是必需的,以处理优化所做的更改。Jürgen表示,他们为此选择了OneSpin 360 EC-FPGA,并指出OneSpin 360 EC-FPGA完全独立于Intel Quartus Prime FPGA合成和位置-路由软件。

Jürgen给出了一个用于Framatome紧凑型安全控制器的英特尔Cyclone V FPGA的具体示例。他表示,整个控制器系统中要求最高的模块是处理模块,该模块的核心是双精度浮点单元(FPU)。这个FPU不仅实现了预期的加法、减法和乘法,还实现了除法、平方根和对数等复杂操作。仅通过模拟来验证后路由网表将需要“许多、许多、许多”年。当然,再多的模拟也不可能是彻底的,也不可能提供形式上等价检验的确定性。运行EC-FPGA比较FPU后合成Verilog网表和FPU后放置和路由Verilog网表的结果包括:

  • 培训和自学初期工作量低(共5个工作日)
  • 基于OneSpin的简单模板脚本的简单和直接的设置
  • 两个网表之间不需要手动映射
  • 由于自动映射而具有回归功能
  • 在FPU内不需要减少RAM

底线:EC-FPGA能够在不到一个小时的总运行时间内证明这个复杂设计的两个网列表等效。Jürgen评论说,他对这些结果感到满意,并赞扬了OneSpin应用工程团队的“高度参与,非常灵敏的支持,甚至在周末!”我们很高兴听到这个消息,非常感谢Jürgen和Framatome与我们的用户社区分享他们的故事。如果你自己不能参加渗透课程,你可以观看演示视频.核查没有比核电站电子设备更重要的了,所以我们相信你会发现这个演讲和我们一样引人注目。



留下回复


(注:此名称将公开显示)

Baidu