Formal semantics for PSL modeling layer and application to the verification of transactional models

The IEEE standard PSL is now a commonly accepted specification language for the Assertion-Based Verification (ABV) of complex systems. In addition to its Boolean and Temporal layers, it is syntactically extended with the Modeling layer that borrows the syntax of the HDL is which the PSL assertions are included, to manage auxiliary variables. In this paper we propose a formal, operational, semantics of PSL enriched with the Modeling layer. Moreover we describe the implementation of this notion in our tool for the dynamic ABV of SystemC TLM models. Illustrative examples are presented.