如何降低Formal assertion的复杂性呢？
分解一个复杂端到端断言属性的一种方法是基于模块化分级断言证明，如下图所示：
端到端属性被分解为分别验证每个子模块：
P1 验证 Sub1
P2 验证 Sub2
P3 验证 Sub3
我们使用P1已证明的属性作为P2断言证明的假设，所以模块化分级证明的要点就在于“后级模块的证明假设，一定要有前级断言的证明保证”，即“assume-guarantee”原则，这个原则在EDA仿真验证环境集成时也是适用的。
由于这种“assume-guarantee”原则的保证，上面3个模块如果都完成了证明，那么也相当于端到端的断言属性完成了证明。
分而治之，各个击破的方法，在大规模芯片验证中非常适用，但是也很容易引入质量风险。
审核编辑：刘清
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。
举报投诉
-
eda
+关注
关注
72文章
3053浏览量
181466 -
EDA仿真技术
+关注
关注
0文章
5浏览量
5555
原文标题：如何降低Formal assertion的复杂性(二)
文章出处：【微信号：芯片验证工程师，微信公众号：芯片验证工程师】欢迎添加关注！文章转载请注明出处。
发布评论请先 登录
相关推荐
热点推荐
基于构件回归测试的复杂性度量框架
的软件修改需求，维护者可以实施不同的修改手段．不同的修改手段会导致不同的回归测试复杂性，这种复杂性是软件维护成本和有效性的重要因素．目前的研究没有强调构件软件的回归测试复杂性问题．基于
发表于 01-19 16:41
•0次下载
如何降低人工智能的复杂性
人工智能的复杂性导致了两个不利的结果，其一是人工智能领域的研发投入过高，而且研发周期过长，这本身会把大量的创业者挡在门外，其二是人工智能产品对于落地应用的条件要求也过高，导致产业领域应用人工智能产品的意愿降低。
发表于 09-22 16:09
•1407次阅读
大数据分析学习的挑战：复杂性、不确定性及涌现性
来源：ST社区 科多分享的大数据分析学习与研究的新挑战：对于习惯结构化数据研究的统计学来说，大数据分析显然是一种崭新的挑战。 挑战来自何方?来自于大数据的复杂性、不确定性和涌现性三个方面，其中复杂性
降低无线连接、共存的复杂性
。 讨论降低无线连接复杂性的小组成员。 “降低无线连接的复杂性”是最近 NXP Connects 会议上的一个小组讨论的主题，我们主持了 Google、HID Global、三星和
可以通过降低约束的复杂度来优化Formal的执行效率吗？
我们可以通过降低约束的复杂度来优化Formal的执行效率，但是这个主要是通过减少Formal验证空间来实现的，很容易出现过约，导致bug遗漏。
Formal Verification的基础知识
，如Intel，使用自研formal工具；还有一些提供formal解决方案的公司，如OneSpin(已与Siemens EDA合作)，Oski Tec(已被NVIDIA收购)。 Assertion 具体
如何利用AI降低电子系统设计的复杂性呢？
在电子系统设计领域，复杂性一直是一个主要的挑战。随着技术的进步和对更高效、更强大的电子设备的需求的增长，工程师们面临着越来越复杂的设计要求。
发表于 08-02 09:14
•812次阅读
工商网监
评论