To offer more computing power to modern SoCs, transistors keep scaling in new technology nodes. Consequently, the power density is increasing, leading to higher thermal risks. Thermal issues need to be addressed as early as possible in the design flow, when the optimization opportunities are the highest. For early design stages, architects rely on virtual prototypes to model their designs' behavior with an adapted trade-off between accuracy and simulation speed. Unfortunately, accurate virtual prototypes fail to encompass thermal effects timescale. In this paper, we demonstrate that less accurate high-level architectural models, in conjunction with efficient power and thermal simulation tools, provide an adapted environment to analyze thermal issues and design software thermal mitigation solutions in the case of the Locomotiv MPSoC architecture.

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.

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.

The TLM modeling level of the systemC language emphasizes the transactions in a complex system, considered at a very high level of abstraction. This level of specification considerably improves simulation performance and is therefore increasingly being adopted. We address assertion-based verification (ABV) of TLM systemC models. We propose a framework for supervising during simulation the verification of temporal properties expressed in PSL. Very few modifications are needed in the original systemC code. The TLM specification can be timed or not. The properties can involve several channels, of different types.