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

职业：GoldMine：使用数据挖掘和静态分析在系统设计中自动生成断言

• 批准号: 0953767
• 负责人: Shobha Vasudevan
• 金额: $ 43万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-03-15 至 2015-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0953767&HistoricalAwards=false
• 关键词: CAREER; GoldMine; Automatic; Assertion; Generation

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.

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