CAREER: GoldMine:Automatic Assertion Generation in System Design Using Data Mining and Static Analysis

职业：金矿：使用数据挖掘和静态分析的系统设计中的自动断言生成Shobha Vasudevan伊利诺伊大学厄巴纳香槟分校断言是设计意图的总结陈述，已成为硬件和软件开发周期中最流行的检查工件。在硬件方面，断言用于形式验证、动态验证、运行时监控、仿真、硅后调试和现场诊断。今天，断言的生成是一项高度手动的任务。在每个系统开发周期中，许多人月和资源都花费在断言生成上。这项工作提出了一个自动断言生成技术和工具，金矿，系统使用数据挖掘和静态分析相结合。数据挖掘通过对系统动态行为的统计分析来推断知识。静态分析在不执行系统的源代码或模型的情况下进行推理，并分析可能的行为。这两种技术可以协同使用。静态分析技术可以用来推断领域信息，指导数据挖掘。GoldMine将为一套数据挖掘算法提供目标设计的模拟数据，并沿着进行静态分析，以推断？可能不变量？可能的不变量将通过一个正式的验证器过滤真正的断言。正式验证的反馈将被提供给挖掘算法，以及对生成的断言的设计者/用户评估。这个迭代过程将自动生成高质量的断言。在1000+处理器RTL的Rigel上获得了初步结果。统计和静态分析之间的婚姻在这里提出了一个系统产生的知识是一个？Meta技？可以以多种形式使用。在任何结构化系统中提取和提供领域知识的系统方法论，沿着基于统计的学习技术，可以创建非常强大的组合。静态领域分析和统计数据挖掘的联盟可以用于软件系统，嵌入式系统和其他需要推断知识的领域。此举旨在节省经济和人力资源，从而提高社会的生产力。GoldMine也将被广泛传播（沿着源代码），用于研究和教育目的，有助于学生的实际学习。系统设计的优点在于，我们建议研究和系统化设计的人类认知方面。

CAREER: GoldMine:Automatic Assertion Generation in System Design Using Data Mining and Static AnalysisShobha VasudevanUniversity of Illinois at Urbana ChampaignAssertions are summarized statements of design intent that have emerged as the most popular checking artifacts in hardware and software development cycles. In hardware, assertions are used in formal verification, dynamic verification, runtime monitoring, emulation, post-Silicon debug and in-field diagnosis. The generation of assertions today is an intensely manual task. During each system development cycle, many man-months and resources are spent in assertion generation. This work proposes an automatic assertion generation technique and tool, GoldMine, for systems using data mining and static analysis in combination. Data mining infers knowledge by statistical analysis of dynamic behavior of a system. Static analysis reasons with the source code or model of the system without executing it, and analyzes possible behavior. These two technologies can be used synergisti-cally. Static analysis techniques can be used to infer domain information and guide the data mining. GoldMine will provide simulation data of the target design along with static analysis to a suite of data mining algorithms that will infer ?likely invariants?. The likely invariants will be passed through a formal verifier for filtering the true assertions. Feedback from formal verification will be given to the mining algorithms, as will the designer/user evaluation of the generated assertions. This iterative process will produce high quality assertions automatically. Preliminary results have been obtained on Rigel, a 1000+ processor RTL. The marriage between statistical and static analyses proposed here for generating knowledge about a system is a ?meta technique? that can be used in a multitude of forms. A systematic methodology to extract and provide domain knowledge in any structured system, along with statistics based learning techniques can create a very powerful combination. The alliance of static domain analysis and statistical data mining that has been introduced can be used for software systems, embedded systems and other domains where knowledge needs to be inferred.This proposal seeks to automate a manual, all-pervasive system process. This aims at saving economic and human resources, thereby increasing the productivity of the community. GoldMine will also be widely disseminated (along with the source code) for research and education purposes, contributing to practical learning of students. The merit in the system design world is that we are proposing to study and systematize the human cognition aspect of design.