This session covers 3 different aspects in high-level modelling and verification.  The first presentation introduces a methodology by ST Microelectronics to create and use virtual platforms based on industry standards like SystemC TLM standards and IP-XACT.  The second presentation focuses on simulation and describes a mutation model at transaction level, its injection and simulation and its relationships with qualification of properties and testbenches.  Finally, the third presentation discusses two different aspects in TLM to RTL equivalence verification, i.e., comparing TLM C code to manually created RTL and comparing TLM C code to synthesised RTL.