Enhancing the assertion-based verification of TLM designs with reentrancy

In this paper, we focus on the assertion-based verification (ABV) of designs described using the SystemC transactional level (TLM). Assertions are expressed in the PSL language, and the verification that the system fulfils these properties is performed dynamically i.e., during simulation. We have previously reported our results about the development of a dedicated ABV methodology that makes use of automatically generated checkers and of ad hoc observation mechanisms. The technique has also been improved to support the PSL Modeling Layer which enables the use of (global) auxiliary variables in assertions. A prototype tool, called ISIS, implements all these features. However, supporting the notion of global variables in assertions is not sufficient in general, for instance when components have a pipelined behaviour, thus enabling the simultaneous processing of several data. We propose here yet another improvement of the method, that provides for considering reentrant assertions (i.e., assertions simultaneously evaluated for different data) through the use of multiple checker instances, with local variables. We extend the PSL syntax with an appropriate syntactical construct, we adapt the semantics accordingly, and we describe the implementation in our tool. Experimental results are also reported.