TRANSFORMATION OF SIMPLE SUBSET OF PSL INTO SERE IMPLICATION FORMULAS FOR VERIFICATION WITH MODEL CHECKING AND SIMULATION ENGINES USING SEMANTIC PRESERVING REWRITE RULES

摘要

Simple-Subset PSL formulas are transformed to SERE implications (Figure 3). Verification engines are required to support the basic formula only (320). The basic formula is a form of automata in the property specification language. This is called SERE implication. The efficiency of verification is dependent on size of automata.