Integrating PSL properties into SystemC transactional modeling — Application to the verification of a modem SoC

This paper focuses on the assertion-based verification (ABV) of hardware/software embedded systems, described at the Electronic System Level. We first summarize the features of a tool that enables the automatic instrumentation of SystemC TLM platforms with property checkers produced from PSL assertions and the runtime verification of these requirements. We also present its last improvements. Then we describe a return of experience using as case study a SoC modem for digital radio reception developed by Thales Communications & Security. Various temporal properties that capture the intended requirements, regarding hardware or hardware/software interactions, are formalized in PSL and checked during simulation.