Auxiliary Variables in Temporal Specifications: Semantic and Practical Analysis for System-Level Requirements

International audienceAssertion-based verification (ABV) for IP blocks given as synchronous RTL (register transfer level) descriptions has now widely gained acceptance. The challenge addressed here is ABV for systems on chip (SoC) modeled at the system level in SystemC TLM (Transactional Level Modeling). Requirements to be verified at this level of abstraction usually express temporal constraints on the interactions and communications in the SoC. We use the IEEE standard language PSL to formalize these temporal assertions which represent properties on communication actions and their parameters. Auxiliary variables are often indispensable for this formalization, but their use may induce semantic issues. This article discusses this matter, analyzes various existing approaches and proposes a summary of their advantages and shortcomings. They are also compared to our syntactic and semantic framework, implemented in a verification tool. The proposed operational semantics has the advantages of being simple and intuitive while supporting both global and local auxiliary variables. Experimental results on industrial case studies illustrate its applicability