Automatic generation of assertions from system level design using data mining

Automatic generation of assertions from system level design using data mining
复制标题

DOI:
10.1109/memcod.2011.5970526
复制
发表时间:
2011-07
期刊:
Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011)
影响因子:
--
通讯作者:
Lingyi Liu;David Sheridan;V. Athavale;Shobha Vasudevan
Lingyi Liu;David Sheridan;V. Athavale;Shobha Vasudevan
中科院分区:
其他
文献类型:
--
作者:
Lingyi Liu;David Sheridan;V. Athavale;Shobha Vasudevan

文献摘要

被引文献

相似文献

系统级建模在系统开发的早期阶段被广泛使用,以简化设计验证和体系结构探索。基于断言的验证已经成为RTL验证方法中公认的一部分。在传统的基于断言的验证流程中,断言是手动编写的。在本文中,我们使用GOLDMINE从系统级设计生成断言,这是一个使用数据挖掘和静态分析的自动断言生成引擎。在系统级设计的仿真轨迹中,以频繁模式的形式挖掘候选断言。我们同时考虑了周期精确度和事务级别的设计,并为每种设计开发了一种挖掘方法。对于周期精确的设计,我们使用了基于决策树的监督学习算法以及覆盖引导的关联挖掘算法来搜索模拟轨迹中的相关性。对于事务级设计,应用序列模式挖掘从跟踪中生成函数调用和事件的频繁序列。我们还使用符号执行引擎来泛化函数的参数和返回值,以帮助数据挖掘人员找到相关的行为。我们表明,我们的技术在周期精确的RISC CPU设计和基于AMBA的事务级DMA控制器上都产生了有意义的断言。
System level modeling is widely employed at early stages of system development for simplifying design verification and architectural exploration. Assertion based verification has become a well established part of RTL verification methodology. In the traditional assertion based verification flow, assertions are manually written. In this paper, we generate assertions from system level designs using GoldMine, an automatic assertion generation engine that uses data mining and static analysis. Candidate assertions are mined in the form of frequent patterns in the simulation traces of the system level designs. We consider both cycle accurate and transaction level designs and develop a methodology for the mining of each. For cycle accurate designs, we use both a decision tree based supervised learning algorithms as well as a coverage guided association mining algorithm to search for correlations in the simulation trace. For transaction level designs, sequential pattern mining is applied to generate frequent sequences of function calls and events from traces. We also use a symbolic execution engine to generalize the parameters and return values of the functions to help the data miner find relevant behavior. We show that our technique generates meaningful assertions on both a cycle accurate RISC CPU design and a transaction level AMBA-based DMA controller.