广告

通过形式验证找到更多Bug

2020-05-17 Mark Eslinger,Ping Yeung 阅读:
本文将介绍在形式验证过程中找到最佳“钓鱼点”的方法。它利用功能仿真活动,从仿真轨迹中找到有价值的“钓鱼点”,进行形式验证。我们称这种方法为“河钓法”,它并不是从一个初始状态开始形式验证,而是从功能仿真轨迹中挑选出一些可疑的点,然后从这些“钓鱼点”开始形式验证。
ASPENCORE

经常有这样的事情发生,有些人总可以钓到很多鱼,而其他人却没有这样好的“运气”。之所以这样,很大程度上是因为那些成功的钓鱼者们知道最好的钓鱼点。他们知道鱼儿一般会藏在哪里,就会在哪里放线。0NsEETC-电子工程专辑

同样,验证的方法也可以引导我们找到合适的“钓鱼点”,大大增加我们捕获bug的数量。0NsEETC-电子工程专辑

本文提出了一种方法,它利用功能仿真活动,从仿真轨迹中找到有价值的“钓鱼点”,进行形式验证。我们称这种方法为“河钓法”,它并不是从一个初始状态开始形式验证,而是从功能仿真轨迹中挑选出一些可疑的点,然后从这些“钓鱼点”开始形式验证。0NsEETC-电子工程专辑

河钓法包含三个主要步骤:0NsEETC-电子工程专辑

●从仿真轨迹中识别并提取出一组合适的“钓鱼点”。0NsEETC-电子工程专辑

●根据形式验证引擎运行状况筛选并确定这些钓鱼点的优先级。0NsEETC-电子工程专辑

●在计算服务器上启动并监测多个形式验证的运行。0NsEETC-电子工程专辑

本文分享了我们最常用的钓鱼点,这在许多设计都可以找到;文中还说明了如何使用形式验证引擎来确定优先级、引导bug寻找过程,从而在形式回归环境中提高验证结果的质量。0NsEETC-电子工程专辑

我们开始钓鱼吧

在河钓技术中,我们并不是从一个初始状态开始形式验证,而是从功能仿真轨迹中挑选出一些可疑的点,然后从这些点开始进行形式验证。如果功能仿真已经进行了一些与目标有关的值得关注的活动,那么还可以找到其它一些不错的钓鱼点。此外,如果某些目标要求特定的前提条件,则可以利用不同的功能测试,为这些特定目标确定不同的钓鱼点。0NsEETC-电子工程专辑

实际上,河钓法利用了功能仿真已经执行的任务,来检查那些尽可能接近最终目标的可疑的初始状态,如图1所示。0NsEETC-电子工程专辑

图1:从一些有趣的钓鱼点启动形式验证。(来源:Mentor)0NsEETC-电子工程专辑

在以下章节中,我们将详细描述利用河钓法寻找bug的三个主要步骤(如图2所示):识别钓鱼点、引擎健康筛查,以及并发形式验证运行。0NsEETC-电子工程专辑

图2:使用河钓法进行形式验证。(来源:Mentor)0NsEETC-电子工程专辑

寻找最佳钓鱼点

钓鱼专家们都知道,最好的钓鱼地点是河流中那些有着不寻常活动的特殊区域。从仿真轨迹中挑出值得关注的点进行形式验证也与之相似。0NsEETC-电子工程专辑

图3:确定值得关注的钓鱼点。(来源:Mentor)0NsEETC-电子工程专辑

这里介绍一个快速全面的两层法,用于挑选那些要关注的钓鱼点。该方法的主要标准包括:0NsEETC-电子工程专辑

●接口交互:模块间通信和标准协议接口。0NsEETC-电子工程专辑

●控制和中断:包括FSM、总线控制器、内存控制器、流程图、算法控制等。0NsEETC-电子工程专辑

●并发事件:包括设计中的仲裁器、调度器、开关、多路复用逻辑等。0NsEETC-电子工程专辑

●反馈、循环和计数:包括FIFO、定时器、计数器等,用于处理设计中的数据传输、突发和计算。0NsEETC-电子工程专辑

●用户自定义断言和覆盖属性。次要标准与主要标准的纳入或排除有关。0NsEETC-电子工程专辑

●纳入标准:收集主要钓鱼点时,应该标记价值高的点,例如满足多个标准的状态、变化频率较低的状态以及出现新活动的状态。0NsEETC-电子工程专辑

●排除标准:同时,要过滤掉价值不高的钓鱼点,例如重复的状态、导致错误结果的错误状态,以及上电、重置、初始化或配置顺序的状态。0NsEETC-电子工程专辑

0NsEETC-电子工程专辑

选择最佳钓鱼点

形式验证不同于仿真。仿真运行是可预测、可完成的。但当对大量的断言进行形式验证时,很难预测何时以及是否会完成。因此,了解形式验证引擎的运行状况,并利用它来衡量形式验证取得的进展非常重要。0NsEETC-电子工程专辑

引擎运行状况可用于衡量通过形式验证取得的进展。而且,形式验证引擎健康是一个矩阵,可用于估计、确定优先级并监测形式验证运行。利用形式验证引擎健康状况,我们可以评估钓鱼点的成果,筛选出低质量的点,并对其余点进行优先排序以进行形式验证。在这些随后的形式验证运行期间,需要持续监控其引擎健康,以便尽早终止那些无效的运行,节省资源来运行新的形式验证。0NsEETC-电子工程专辑

我们用一组参数来定义形式验证引擎运行状况:0NsEETC-电子工程专辑

●达成的形式验证目标(proven/fired/covered/uncoverable)(已证明/被终止/被发现/无法发现)。0NsEETC-电子工程专辑

●探索的顺序深度或分析的影响锥(cone of influence)。0NsEETC-电子工程专辑

●获取的形式验证知识和引擎设置。0NsEETC-电子工程专辑

达成的目标和探索的顺序深度是两个完善的指标,已经普遍用于确定形式验证的总体运行进度。0NsEETC-电子工程专辑

另一方面,如果想了解形式验证在单个属性或目标上的表现,就必须更深入地研究影响锥以及通过这些目标获取的形式验证知识。影响锥提供了关于每个目标探查深度的更多信息,以及扇入逻辑及其对目标依赖性的信息。影响锥突显出扇入逻辑中的“绊脚石”,这时形式验证会被挂起,需要花费大量时间进行分析。这种难解的设计元素是可以被识别的,用户可以决定是否有必要进行干预。有效分析“绊脚石”并解决的方法包括:添加切点、抽象出设计元素,或启用某些特殊引擎。0NsEETC-电子工程专辑

一直以来,形式验证引擎运行状况被用于监测计算密集型的形式验证的运行。直到最近,我们才意识到它也可以是筛选钓鱼点的好方法。由于要在有限的计算资源(和许可证)上执行大量形式验证,我们发现经常需要不断地终止那些可能徒劳无功的运行。形式验证引擎健康参数可以用于确定计算服务器是否被分配来彻底探测这些钓鱼点。0NsEETC-电子工程专辑

图4:用引擎健康状况来筛查钓鱼点。(图片来源:Mentor)0NsEETC-电子工程专辑

放置多条钓鱼线 

有了钓鱼点优先级列表,就可以在服务器集群环境中同时启动大规模形式验证测试了。主服务器将管理和监测所有形式验证过程,它将持续不断地从每个形式验证运行中收集形式验证引擎的健康参数。图5捕获了一个形式验证运行开始时的目标分布,用户可以由此知道已经取得的进展。最初,33个目标中的大多数是不确定的 ,即inconclusive(I)。在多核并行的情况下,形式验证逐渐验证目标,并将它们划分为以下几个类别之一:firing (F)、vacuous (V)、uncoverable (U)、covered (C)和proof (P)。0NsEETC-电子工程专辑

图5:形式验证目标被证明或满足的快照。 (图片来源:Mentor)0NsEETC-电子工程专辑

一个全面的形式验证工具都具有一组形式化引擎,用以处理不同结构的设计。随着形式验证的运行,可以检查引擎的状态,以了解哪些引擎可以得出结果,而哪些引擎可能不会有收获。如果某个引擎对当前的任何结果都无贡献,可以将该引擎替换掉以节省资源,并将其它引擎集中在当前任务上。图6是一个分布式形式验证运行期间的引擎快照。0NsEETC-电子工程专辑

图6:形式验证引擎知识库快照。(图片来源:Mentor)0NsEETC-电子工程专辑

 “Proven/Unsatisfiable”列显示了哪些引擎可解决安全性、寿命、空白和覆盖类型检查。 “Fired/Satisfied”列显示了哪些引擎生成了反例。引擎7在查找大量证据和终止(firing)方面贡献很大。引擎0(管家引擎)和引擎10也找到了一些证据。另外,引擎12和17(针对某些难题设计)虽然也致力于解决问题,但并没有什么产出。“Inconclusive Targets”列(好、中、差)则显示了工作中(WIP)目标的单个引擎健康状况。引擎12正在研究75个健康状况良好的目标,也就是说,它进展顺利,只有三个目标健康状况中等和不良。同样,引擎10在51个属性上运行良好,但在其它很多目标上运行无效。0NsEETC-电子工程专辑

钓鱼收获如何?

在以下案例中,我们捕获了两种代表性的bug情况。而且只有在我们从仿真轨迹深处的钓鱼点开始形式验证之后,才成功捕获。形式验证引擎健康筛查也被用来清除许多不成功的验证运行,这在开始或验证过程中都可能发生。0NsEETC-电子工程专辑

图7:比率同步数据传输接口。(图片来源:Mentor)0NsEETC-电子工程专辑

案例一:为节省能耗,如今的设计中都应用了很多比率同步时钟,它们尽可能慢地运行每个组件。因此,比率同步接口很常见。在数据有效条件确定时,这些接口中的快速时钟域被设计为在慢时钟周期结束时对数据进行采样。但是,在某些特殊情形下(设计团队最初不知道),即使未声明有效条件,数据也会被采样。结果,损坏的数据被注册并在系统内传递。根据两个接口、计数器和控制逻辑上的活动可以确定钓鱼点。在初始化设计之后,以及两个接口之间的数据经过数百个周期的正确传输之后,挑选出几个钓鱼点。形式验证揭示出两个接口之间不完整的握手信息,这种不完整导致数据采样无效。0NsEETC-电子工程专辑

案例二:在此数据传输控制器中,设置了动态传输通道以处理具有不同优先级的数据包。 在这种情况下,当多个通道同时完成传输时,一组地址指针将被解除分配两次,而另一组地址指针却没有被解除分配,从而导致内存泄漏和数据损坏。根据并发事件、计数器和复杂控制逻辑的活动可以确定钓鱼点。在这种类型的设计中,形式验证很难设置这些数据传输。但是,它们很容易在仿真回归中获得。通过利用仿真运行深处的多个钓鱼点,并基于引擎健康对它们进行优先排序,形式验证可以暴露通道去分配逻辑中的弱点,并同步两个通道以同时完成传输。0NsEETC-电子工程专辑

图8:数据传输控制器。(图片来源:Mentor)0NsEETC-电子工程专辑

河钓技术

河钓技术利用了功能仿真活动,从仿真轨迹中找到可疑的捕鱼点开始形式验证。识别一组合适钓鱼点的标准有很多,包括接口交互、控制和中断、并发事件、反馈循环和计数、用户自定义断言和覆盖属性等。然后,根据形式验证引擎健康状况对这些钓鱼点进行筛选和优先级排序,可以被定义为:已证明或已摒弃的验证目标、已探查顺序深度,以及所获取形式验证知识库。之后,当集中式数据库将所有结果汇总在一起时,使用一组钓鱼点来初始化多个形式验证运行。根据得出的结果和发现的复杂bug,我们可以看到,在形式验证回归环境中,河钓技术确实有助于提高验证结果的质量。0NsEETC-电子工程专辑

(参考原文:Catch More Bugs with Formal Verification0NsEETC-电子工程专辑

责编:Amy Guan0NsEETC-电子工程专辑

本文为《电子工程专辑》2020年5月刊杂志文章,版权所有,禁止转载。点击申请免费杂志订阅 0NsEETC-电子工程专辑

ASPENCORE
本文为EET电子工程专辑 原创文章,禁止转载。请尊重知识产权,违者本司保留追究责任的权利。
您可能感兴趣的文章
  • 恒基兆业集团主席李家杰:加速RISC-V开源芯片生态建设 两会期间,全国政协委员、全国工商联副主席、香港恒基兆业集团主席李家杰(Peter Lee)呼吁,加速推进RISC-V开源芯片生态建设,打造国家芯片创新高地,助力数字新基建。作为《福布斯》全球富豪榜第24位李兆基的长子,李家杰热衷于科技领域的投资……
  • Arm公布新CPU、GPU和NPU,超大核Cortex-X1亮相 Arm日前正式公布了其最新产品Cortex-A78和Cortex-X1 CPU,Mali-G78 GPU以及Ethos-N78 NPU。如果一切顺利的话,使用这些新设计的芯片将用于2021年及以后的下一代旗舰智能手机和移动设备上……
  • 搭一条没有美国设备的芯片产线,可行吗? 业内传华为正试图说服三星及台积电,为其打造不采用美系设备的先进工艺生产线。贸易禁令下,各大Fabless厂都担心成为下一个被美国制裁的对象,知名分析师陆行之也建议台积电极力扶持非美系半导体材料与设备供应商,来打消客户疑虑。但与台积电方面踌躇不定相比,三星在这方面似乎比较积极,有媒体报道称三星已与日本、欧洲相关厂商合作,搭建了一条采用非美系设备的7nm小型产线,正在进行测试……
  • IC Insights:中国大陆半导体10年内仍难自给自足 中美紧张的贸易关系,让各界预期中国将加速半导体自主化发展。然而据IC Insights最新报告数据显示,2019年,中国大陆的IC产量占其近1250亿美元IC市场的15.7%,仅略高于2014年的15.1%。IC Insights强调,尽管自2005年以来中国一直是全球最大的集成电路消费市场,但这并不意味着中国本土集成电路产量自此大幅增长……
  • 半导体IP供应商芯原股份IPO成功过会 5月21日,上海证券交易所科创板股票上市委员会召开了2020年第25次审议会议,根据审议结果显示,芯原股份IPO成功过会。
  • 中芯国际:“与泰康一对一交流纪要”内容纯属网络捏造 5月21日凌晨,多名财经博主在社交平台上发布了一则名为《中芯国际-泰康一对一交流纪要》的中芯国际机构交流会内容,指出“如果严格按照法令申请许可,整个华为的渠道都会被管控;新订单理论上不能接了”。21日中午,中芯国际在官方微信上发布澄清说明……
相关推荐
    广告
    近期热点
    广告
    广告
    广告
    可能感兴趣的话题
    广告
    向右滑动:上一篇 向左滑动:下一篇 我知道了