理论计算机科学电子笔记174（2007）3-7www.elsevier.com/locate/entcs从错误到错误：众核时代John Moondanos1形式化技术设计技术和解决方案英特尔公司， M/S SC12-6052200 Mission College Blvd.CA 95054，USA摘要当今多核微处理器的设计和制造必须克服主要的技术障碍，特别是在功耗和验证方面。更具体地说，验证领域的技术水平是这样的，在现代微处理器设计团队中，超过30%的人力资源致力于此。术语验证生产力差距已经被引入来描述这些不断增长的资源需求。正式验证技术是解决这一验证差距的许多方面的技术方法之一。因此，开发技术和方法来减少调试和纠正由形式验证技术检测到的逻辑错误所需的时间至关重要。这些发展将有助于在硅验证活动前后关键词：形式验证，等价性检验，性质验证，逻辑验证，逻辑电路校正。1引言在Pentium FDIV bug之后的十多年里，世界各地的设计工程师都在享受形式属性验证（FPV）和形式等效验证（FEV）工具的广泛使用带来的好处。这些工具多年来在无缺陷的流片中发挥的作用的重要性怎么强调都不过分。不幸的是，调试识别和纠正设计错误的根本原因的过程似乎仍然是一项劳动密集型的工作，并已成为FV活动的主要瓶颈之一一个工程师仍然需要注意到一些事情，质疑它为什么会发生，建立假设，然后试图证实或证伪它们。正如已经正确地指出的那样，似乎存在一个非算法的心理组件，以目前的调试方法。可惜1 电子邮件：john. intel.com1571-0661 © 2007由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2006.12.0354J. Moondanos/Electronic Notes in Theoretical Computer Science 174（2007）3顶级微处理器公司严格的上市时间要求不允许我们继续这种传统。引用这一领域的顶尖专家的话来说，调试应该像逻辑设计的其他领域一样有纪律、有系统和可量化--这意味着我们应该将其自动化。幸运的是，CAD工具的最新进展在我们的正式验证工具可以处理的电路尺寸和复杂性方面带来了突破性的改进。本次演讲的重点正是利用这一最新进展，通过利用先进的自动调试算法来提高设计人员在正式验证应用程序中的生产力。为了定义调试设计所涉及的操作，让我们首先回顾一下工程师在这个多核处理器时代正在研究的设计方面。在设计一个系统时，我们主要处理三个方面。它的规格（在不同抽象层次上的属性或电路），实际模型和模型运行的环境（通常表示为一组无关条件）。另一方面，术语“设计”是指三个独立但互补的活动。错误解释描述了帮助用户从特定故障示例转移到理解故障本质的任何方法。错误定位是一项更具体的任务，通过定位问题的根本原因组件来识别系统的故障核心。最后，错误纠正涉及实际纠正问题的技术。细心的读者会意识到自动化正式调试算法的重要性，除了它们能使逻辑调试过程更耗时和更少令人沮丧之外，还有其他原因。除了修复实现错误外，这些技术在由于规范更改而进行的设计修订过程中也至关重要。当在设计确认过程中发现高水平质量标准中的错误时，进行质量标准变更在实践中，正如我们许多人多年来所经历的那样，在设计周期的后期，当逻辑综合甚至布局和布线已经完成时，会发现规格错误为了重新使用已用过的工程资源，设计人员倾向于修补旧的实现并使其符合新的规范，而不是从头开始重新合成。这一过程被称为ECO [1]，它需要能够非常有效地进行设计修改的方法ECO和错误调试都可以清楚地表述为逻辑域中的纠正问题2逻辑整流技术故障诊断是一个交互式和迭代的过程，需要设计师亲自加快这一过程的一种方法是提高设计人员的能力，使他们能够使用先进的自动分析算法来理解这些算法将通过提供较小的可能错误位置集合和自动化的设计校正方法来提高设计者的生产力这些高级调试算法需要考虑：J. Moondanos/Electronic Notes in Theoretical Computer Science 174（2007）35追踪技术：FPV和FEV工具自动生成反例;然而，正如领先的研究人员所指出的，孤立的反例只是设计错误的症状，而不是根本原因的识别。为了增加反例在识别错误根本原因方面的价值，这类技术试图：(i) 在错误跟踪中定位错误的原因，(ii) 产生具有不同原因的不同错误跟踪。这种基于跟踪的技术在没有指定模型的情况下调试形式属性时特别有用。在理想的调试算法架构中，我们需要包括：(i) 反例最小化：通过产生导致相同错误状态的最小长度序列来帮助调试工程师。(ii) 跟踪聚类：将由于相同的根本原因而达到相同错误状态的反例序列分组在(iii) 正负轨迹生成：创建相似(with相对于距离度量）到导致错误状态（负迹线）和良好状态（正迹线）的给定反例。这些技术形成了所谓的Delta方法[9]的基础，由此，我们试图通过检查与原始反例略有不同的迹线的行为来找出设计中问题的根源。结构技术：这些技术包括利用门控制器[2]、各种切割点生成算法方案和其他电路结构信息，以识别和可视化规范和IMP之间的相似性。它们还包括锥相交，由此，不在错误输出扇入锥相交处的信号不能单独对错误负责，因此不能成为错误部位。此外，反向传播[12]技术试图通过跟踪信号路径来识别错误输出的根本原因，这些信号路径由输入设置为控制值的门调节符号技术：这些技术[1，3，5]采用降序BDD来制定信号或一组信号的必要和充分布尔条件，以成为错误的根本原因。此外，它们在校正过程中起着重要作用，因为它们编码了必须实现以校正电路的新逻辑的功能。分析技术：这些[6，7]采用SAT求解器和该领域已实现的最新在理想的调试算法体系结构中，我们应该有一个策略，通过该策略，我们试图识别电路中的哪些门必须被改变，以便纠正我们在电路输出端观察到的反例集的错误值，反例集的大小由用户定义。这种方法背后的直觉是，当改变时可以纠正大量反例的电路输出的门，可能是设计错误的实际根本原因。基于仿真的技术：这些方法[4，8]主要用作所提出的算法架构中的滤波器。他们逐渐排除信号从6J. Moondanos/Electronic Notes in Theoretical Computer Science 174（2007）3错误位置的候选列表一般来说，基于仿真的技术的主要优点是它们具有高度的可扩展性. 在许多情况下，它们也产生令人满意的诊断结果[10]。然而，基于模拟的方法不能提供关于如何修复错误的足够见解。因此，它们不太适合需要自动校正的应用（例如，ECO问题）。基于敏感化的滤波器补充门的输出，并试图在整个门扇出锥中传播此更改的效果如果此更改无法传播到输出，则从候选错误列表中获取门公共错误过滤器方法尝试使用快速仿真结果来潜在地识别一些公共门级错误（例如，缺失/额外的反相器/缓冲器、错误的门类型等）是FPV/FEV运行的根本原因。混合技术：这些技术包括自动测试模式生成技术（ATPG），该技术实际上结合了结构化和基于SAT的方法的基础技术[11]。如果我们认为D或D-bar表示对（spec，imp）值，而不是对（good，faulty）电路值，则错误定位问题可以转换为ATPG问题。3总结所有这些技术都需要改进，进一步扩展和组合，以适应当今众核处理器设计给形式验证技术带来的极其复杂的问题。特别是，针对协议验证的失败属性运行的调试似乎是实现正确多核设计的关键一步。引用[1] C.- C. Lin，K.- C.陈思C. Chang和M. M. Sadowska，工程变更的逻辑综合，程序。设计自动化会议，San Francisco，CA.第647-652页，一九九五年[2] H.- T. Liaw，J.- H. Tsaih和C.- H.林志光，数字电路的自动诊断技术，中国计算机科学院学报，第103页。464-467，1990.[3] J. C.马德雷岛Coudert和J. P Billon，使用PRIAM自动诊断和纠正数字错误，Proc. ICCAD，pp. 30-33，1989年。[4] V.Boppana和M.藤田，塑造未知！面向模型无关的故障和错误诊断，在Proc。测试确认，1998，pp. 1094-1101.[5] 李光辉，邵明，李晓伟，基于验证技术的设计错误诊断，第12届亚洲测试研讨会，第474-477页，2003年[6] Alexander Smith， Andreas Veneris和 Anastasios Viglas ， 使 用布 尔 可满 足 性的 设 计诊 断 ，Proc. ASP-DAC'04，pp. 218-223，2004年[7] Moayad Fahim Ali，Andreas Veneris，Sean Safarpour，Magdy Abadir，Rolf Drechsler，and AlexanderSmith，《使用布尔可满足性的时序电路》，第五届微处理器测试与验证国际研讨会，第100页。2004年第44-49号来文[8] Debashis Nayak，D.M.H.王志华，“组合式数位电路之设计错误诊断与校正”，第十七届IEEE超大型积体电路测试研讨会论文集，第70-78页，1999年[9] A. Zeller和R. 刘文，基于故障诊断的计算机辅助设计，北京大学出版社，2002年3月。J. Moondanos/Electronic Notes in Theoretical Computer Science 174（2007）37[10] S.- Y.黄，K- T. Cheng，K.- C. Chen和D.- I.郑文，错误追踪器：一种基于故障模拟的设计错误诊断方法，IEEE国际测试会议，Washington，DC. 974-981，1997年11月。[11]M. S. Abadir ， J. Ferguson and T. E. Kirkland ， 通 过 测 试 生 成 验 证 逻 辑 设 计 ， IEEE Trans.Computers，pp. 138-148，1月，一九八八年[12] A. Kuehlmann，D. I. Cheng，中国山核桃A. Srinivasan和D.李文生，晶体管级验证的误差诊断，计算机工程学报，Anaheim，CA，pp.466-471，9月1992.
我的内容管理
展开
