Towards analyzing functional coverage in SystemC TLM property checking

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.