• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Harmonizing data mining and static analysis to tackle hardware and system level verification.
【24h】

Harmonizing data mining and static analysis to tackle hardware and system level verification.

机译：协调数据挖掘和静态分析以解决硬件和系统级验证。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Verification continues to pose one of the greatest challenges for today's chip design. Formal verification and simulation-based verification have been widely adopted. Both of them always rely on assertions (a.k.a. properties) to express a design's intended behaviors. State-of-the-art formal verification suffers from the scalability issue, and the simulation based method does not suffice in covering design behaviors. Moreover, the used assertions are always manually written, which greatly lowers the usability of hardware verification. For complex system on chip (SoC) design, the electronic system level (ESL) methodology creates a high level abstract view of the design, and the model is used for verifying functionality and performance at the early stage. Due to the fast simulation speed and high model complexity, the entire verification methodology is unsystematic and ad hoc, and lacks the support from EDA tools.;In this dissertation, we first present two systematic input stimulus generation methods for simulation based verification of register transfer level (RTL) design. The first method is based on STAR, a technique for generating input vector patterns for all paths of an RTL design using RTL symbolic execution. To attack the path explosion problem in STAR, we present HYBRO and the symbolic state caching method. HYBRO uses branch coverage metric to guide the path exploration. It is a best-effort method that produces excellent coverage for practical designs. Symbolic state caching considers the reachable state space when exploring different paths. It only generates tests for paths leading to previously uncovered state space. As a result, the path explosion problem is mitigated, and the entire method is much more scalable than the original STAR.;Another method for simulation based verification is based on GoldMine, an automatic assertion generation tool that was developed at the University of Illinois. We use the counterexamples generated from formal verification of GoldMine assertions to incrementally refine the internal decision tree. The counterexamples in every iteration can deterministically increase the coverage of the design and eventually cover the whole reachable input space.;To improve the quality of generated assertions, we present a novel technique that combines static and dynamic analysis of RTL source code to discover word level features for assertion mining algorithm. That allows the mined assertions to be at the same level of abstraction as RTL instead of the Boolean bit level. The machine learning algorithm, as such, is thus agnostic to the level of abstraction of its features.;For ESL verification, we present our technique for generating assertions from transaction level models (TLMs) using GoldMine. The generated assertions, which are in the form of frequent patterns in simulation traces of TLMs, are able to express functionality specification as well as performance specification. Our static analysis technology also guides the mining algorithm to generate assertions capturing the data propagation relationships among function parameters and return values in TLMs. We attempt two mining algorithms for TLM assertion generation: sequential pattern mining and episode mining. We demonstrate that episode mining is more scalable and generates higher quality assertions than does sequential pattern mining.;Diagnosing performance violations in ESL verification is still a manual and time-consuming process in industry. We present an intelligent method to localize root causes of performance violations from simulation traces. We propose a concurrent mining method to discover concurrent patterns from the traces, which are potential root causes of the violations. We apply three categories of domain knowledge to increase the effectiveness of the mining results. We show that the concurrent pattern mining with domain knowledge pinpoints the root cause of a violation to a few patterns among transaction traces of massive size.
机译：验证仍然是当今芯片设计面临的最大挑战之一。形式验证和基于仿真的验证已被广泛采用。它们都总是依靠断言（也就是属性）来表达设计的预期行为。最新的形式验证存在可伸缩性问题，并且基于仿真的方法不足以涵盖设计行为。此外，使用的断言始终是手动编写的，这大大降低了硬件验证的可用性。对于复杂的片上系统（SoC）设计，电子系统级（ESL）方法创建了该设计的高级抽象视图，并且该模型用于在早期阶段验证功能和性能。由于仿真速度快，模型复杂度高，因此整个验证方法是非系统的，临时性的，缺乏EDA工具的支持。本文首先提出了两种系统的输入激励生成方法，用于基于仿真的寄存器转移验证。级别（RTL）设计。第一种方法基于STAR，STAR是一种使用RTL符号执行为RTL设计的所有路径生成输入矢量模式的技术。为了解决STAR中的路径爆炸问题，我们提出了HYBRO和符号状态缓存方法。 HYBRO使用分支覆盖率度量标准来指导路径探索。这是一种尽力而为的方法，可以为实际设计提供出色的覆盖范围。符号状态缓存在探索不同路径时会考虑可到达的状态空间。它仅生成通向先前未发现状态空间的路径的测试。结果，缓解了路径爆炸问题，并且整个方法比原始的STAR具有更大的可伸缩性。另一种基于模拟的验证方法基于伊利诺伊大学开发的自动断言生成工具GoldMine。我们使用从GoldMine断言的形式验证中生成的反例来逐步完善内部决策树。每次迭代中的反例都可以确定性地增加设计的覆盖范围，并最终覆盖整个可到达的输入空间。为了提高所生成断言的质量，我们提出了一种新颖的技术，该技术结合了RTL源代码的静态和动态分析以发现单词级别断言挖掘算法的功能。这样就可以使挖掘的断言与RTL具有相同的抽象级别，而不是布尔位级别。这样，机器学习算法就无法抽象其功能的抽象水平。对于ESL验证，我们提出了使用GoldMine从事务级别模型（TLM）生成断言的技术。所生成的断言以TLM的仿真轨迹中的频繁模式的形式出现，能够表达功能规范以及性能规范。我们的静态分析技术还指导挖掘算法生成断言，以捕获在TLM中函数参数与返回值之间的数据传播关系。我们尝试两种用于TLM断言生成的挖掘算法：顺序模式挖掘和情节挖掘。我们证明，情节挖掘比顺序模式挖掘更具可伸缩性，并且可以产生更高质量的断言。;在ESL验证中诊断性能违规仍然是一个手动且耗时的过程。我们提出了一种智能方法，可以从仿真跟踪中定位性能违规的根本原因。我们提出了一种并发挖掘方法，以从跟踪中发现并发模式，这是违规的潜在根本原因。我们应用三类领域知识来提高挖掘结果的有效性。我们显示，具有领域知识的并发模式挖掘可将违反行为的根本原因精确定位到大规模交易痕迹中的一些模式。

著录项

  • 作者

    Liu, Lingyi.;

  • 作者单位

    University of Illinois at Urbana-Champaign.;

  • 授予单位 University of Illinois at Urbana-Champaign.;
  • 学科 Engineering Computer.;Engineering Electronics and Electrical.;Computer Science.
  • 学位 Ph.D.
  • 年度 2013
  • 页码 185 p.
  • 总页数 185
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号