Temporally extended High-Level Decision Diagrams for PSL assertions simulation

The paper proposes a novel method for PSL language assertions simulation-based checking. The method uses a system representation model called High-Level Decision Diagrams (HLDD). Previous works have shown that HLDDs are an efficient model for simulation and convenient for diagnosis and debug. The presented approach proposes a temporal extension for the existing HLDD model aimed at supporting temporal properties expressed in PSL. Other contributions of the paper are methodology for direct conversion of PSL properties to HLDD and HLDD-based simulator modification for assertions checking support. Experimental results show the feasibility and efficiency of the proposed approach.