系统与设计
的意见

形式验证保证了毅力探测器降落在火星上

时钟域交叉验证如何帮助宇宙飞船降落在一个具有挑战性的网站。

受欢迎程度

乔Hupcey三世和凯文·坎贝尔

安全着陆的宇宙飞船在火星是一个复杂的、高风险的挑战。更糟糕的是,地球的大多数科学有趣的地区被巨石守卫,沟渠,高高的悬崖——土地形成不太欢迎车辆。这样的火星探测器着陆地点:毅力Jezero火山口。这不是一个容易的地方找一个明确的地方土地,但是一旦实地潜在回报——找到了古老的微生物的证据——是深远的。(1)

在许多系统车载毅力着陆器需要支持一个安全、全自动着陆在敌对区域地形相对导航(环境)系统。(2)总而言之,环境是导航系统的登陆车在最后阶段的体面的表面。当毅力接近目标着陆点,TRN相比存储的图像周围的景观对由高分辨率摄像机实时拍摄的图像的底部探测器。如果存储图像和摄像头的直播“重叠”,宇宙飞船是在正确的轨道上,工艺每其预定的轨迹继续飞行。相反,如果有任何偏差之间的存储和现场图像,达到空前的处理器会直接登陆制动火箭系统引导飞船回到安全的课程。

概述的地形相对导航(环境)系统操作。(3)

开发工程师于2018年在帕萨迪纳的喷气推进实验室(JPL), CA,的核心电子产品的环境由以下几点:

惯性测量单元(IMU)和相机界面上的专用计算元素组成的一个通用飞行处理器(PowerPC)和现场可编程门阵列(FPGA)。FPGA倍传感器数据和执行高度并行图像处理算法。飞行处理器坐标数据流,消除了任何虚假的具有里程碑意义的比赛,估计车辆状态[7]。处理器也接口航天器获取航天器状态初始化环境。(3)

正式的时钟域交叉验证是至关重要的,以确保FPGA不会成为同步的时钟信号随着时间的推移,因此“挂”芯片。复杂的,今天的FPGA设计包括多个核心,接口,测试逻辑,甚至不同的内部权力和电压域。特别是,多个异步时钟和信号异步时钟域之间的交叉,可能会导致功能性错误。具体来说,当一个信号从一个异步时钟域被注册在一个不同的异步采样时钟域,设置/保存时间要求将违反目的寄存器。这个设置/持有时间违反意味着目的寄存器可能会成为亚稳态,所以目的寄存器将解决不可预测的价值,导致功能性错误。为了解决这个问题,,疾控中心的指导工具,从西门子EDA,喷气推进实验室FPGA设计者添加同步逻辑来防止亚稳态的传播事件。(4)

增加这个挑战是复位信号的叠加。过去,验证设计的复位信号是一个相当简单的过程——只是确认复位信号的连续性的垫环内所有的IP块和实例设计测试下。但随着环境的复杂的逻辑设计,有可能未知的错误可能产生积极优化的复位信号网络要求减少功率和面积开销。引入的bug也可以放在一起的IP块处理不同的时钟和复位。使用的喷气推进实验室的工程师们,RDC利用CDC路径和豁免信息取自,疾病预防控制中心分析,然后执行一个全面自动化,formal-based分析,关注实际的功能性reset-domain穿越路径来实现最高的吞吐量和最确定的路径可操作的结果。

因为即使是最写constrained-random模拟testbenches不能遍历每一个设计的状态空间的一部分,喷气推进实验室团队使用,PropCheck工具来补充他们的数字模拟的环境设计。形式分析与财产检查探索整个状态空间广度优先的方式,与深度优先的方法用于仿真。财产检查,因此,能够详尽发现任何可能发生的设计错误,不需要特定的刺激来检测错误。这确保了验证设计是在所有合法输入场景中没有错误。同时,这种方法本质上标识的报道点,这有助于加快保险关闭。

这样一个复杂和远程登陆过程,正确的设计是唯一的选择。形式分析与疾病预防控制中心、RDC和财产检查喷气推进实验室团队提供他们需要的工具来减轻风险和成功地毅力探测器在火星上。

引用:

(1)毅力探测器着陆地点:Jezero火山口
https://mars.nasa.gov/mars2020/mission/science/landing-site/

(2)高层文章:
危害之间的地形相对导航:着陆
https://science.nasa.gov/technology/technology-highlights/terrain-relative-navigation-landing-between-the-hazards

(3)更详细技术论文的环境系统:
实时地形相对导航测试结果从火星登陆的相关环境,安德鲁·e·约翰逊,杨成,詹姆斯·蒙哥马利Trawny的派遣,布伦特Tweddle和杰森郑,喷气推进实验室,加州理工学院,帕萨迪纳市,91109
https://trs.jpl.nasa.gov/bitstream/handle/2014/45631/14 - 5083 _a1b.pdf?sequence=1

(4)更多的背景在疾病预防控制中心对FPGA设计验证:
显著改善您的FPGA设计可靠性通过使用自定义某个浏览器疾控中心
https://blogs.sw.siemens.com/verificationhorizons/2018/04/24/significantly-improve-your-fpga-design-reliability-by-using-custom-cdc-synchronizers/

(5)更多的背景在重置域交叉(RDC)验证:
如何避免亚稳态上复位信号网络,/ k /重置检查新疾控中心吗
https://blogs.sw.siemens.com/verificationhorizons/2016/07/21/how-to-avoid-metastability-on-reset-signal-networks-aka-reset-check-is-the-new-cdc/

(6)技术论文在之前的应用,形式验证喷气推进实验室项目:
使用正式地确定安全时钟异步块之间的比率,喷气推进实验室的埃里克•Hendrickson -https://trs.jpl.nasa.gov/handle/2014/46428
(也在DVCon美国2018)

凯文·坎贝尔是西门子EDA技术产品经理。



留下一个回复


(注意:这个名字会显示公开)

Baidu