Towards analyzing functional coverage in SystemC TLM property checking
Towards analyzing functional coverage in SystemC TLM property checking
复制标题
致力于分析 SystemC TLM 属性检查中的功能覆盖率
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
H. M. Le;Daniel Große;R. Drechsler
对于电子系统级别（ESL）设计，由于其对交易级建模（TLM）的出色支持，SystemC已成为标准语言。但是，即使可以使用TLM提供的抽象水平来处理系统的复杂性 - 最抽象的含量是未进行的，并且专注于功能 - 仍然是主要的瓶颈。特别是，由于不合时宜的TLM模型是必须确保其正确性的参考。因此，已经开发出正式的验证方法来证明这些模型的特性。但是，即使已经检查了几个属性，也不能保证已经验证了TLM模型的完整功能。因此，在本文中，我们考虑了正式TLM属性检查中功能覆盖分析的问题。我们提出了一种覆盖范围方法，该方法可以分析该属性集是否明确描述了SystemC TLM模型中的所有交易。开发的覆盖范围分析方法确定了未发现的场景，因此可以缩小所有覆盖范围。例如，我们考虑使用自动柜员机，并展示了提出方法的好处。
For Electronic System Level (ESL) design SystemC has become the standard language due to its excellent support of Transaction Level Modeling (TLM). But even if the complexity of the systems can be handled using the abstraction levels offered by TLM - the most abstract one is untimed and focuses on functionality - still verification is the major bottleneck. In particular, as untimed TLM models are the reference for the following refinement steps their correctness has to be ensured. Thus, formal verification approaches have been developed to prove properties for these models. However, even if several properties have been checked this does not guarantee that the complete functionality of the TLM model has been verified. Thus, in this paper we consider the problem of functional coverage analysis in formal TLM property checking. We present a coverage approach which can analyze whether the property set unambiguously describes all transactions in a SystemC TLM model. The developed coverage analysis method identifies uncovered scenarios and hence allows to close all coverage gaps. As an example we consider an automated teller machine and we show the benefits of the proposed approach.