《社区大讲堂》DO-254中的高设计可靠性的逻辑综合（七）--支持逻辑等效型检查

心仪

《社区大讲堂》DO-254中的高设计可靠性的逻辑综合（七）--支持逻辑等效型检查 [复制链接]

设计可靠性在DO-254的A级和B级设计中尤其重要。.
附录B中对有这样的描述：“当设计可靠性级别增加后，
设计方法需要能够验证被测设计满足安全性要求，
这些要求有可能有重合的部分，需要有层次化的设计可靠性设计方法。

在任何设计过程中，如果逻辑综合工具可以被信任，那么逻辑综合会生成门级的设计，并且其功能和设计师输入工具的RTL代码功能一致。然而，在DO-254的流程中，是不存在信任这个词汇的。
取而代之的是每个环节，每个步骤以及每个工具都需要被多种不同的方法进行验证。

在DO-254的设计流程中，在门级来重复功能验证被看作是确认综合工具的方法，也被看作是重复检查RTL功能仿真结果的方法。然而，对大规模的复杂的设计而言，.这会花费太多的时间。取而代之的更快捷的方法是使用形式验证工具来验证综合结果。

LEC能够利用数学的方法来分析设计的模型之间的差异，例如逻辑综合生成的门级网表和输入的RTL代码。功能不同的地方会在模型中标记出来。
使用LEC能为设计可靠性提供多一层方法，可以弥补门级仿真的一些缺陷。
这对于大规模的复杂设计非常有帮助，
因为这些设计的门级仿真耗费的时间太多。

要提供对形式化验证流程的支持，需要综合工具能支持这个流程。.
综合工具需要能够提供一些从RTL到门级优化的对应的信息。
这些信息能够使逻辑等效性检查工具更有效率，更容易的完成这项工作。