The IEEE standard Property Specification Language (PSL) is increasingly used in many phases of the hardware design cycle, from specification to verification. PSL combines Linear Temporal Logic (LTL) with Sequential Extended Regular Expressions (SEREs), and thus provides a natural formalism to express all ω-regular properties.
In this paper, we propose a new method for efficiently converting PSL formulas into symbolically represented Nondeterministic (Generalized) B"uchi Automata (NGBA), that are typically used in many verification and analysis tools. The construction is based on a normal form that separates the LTL and the SERE components, and allows for a modular and specialized encoding. The compilation is enhanced by a set of syntactic transformations that aim at reducing the state space of the resulting NGBA. These rules enable to achieve, at low cost, the simplification that can be achieved with expensive, semantic techniques based on minimization.
A thorough experimental analysis over large sets of paradigmatic properties (from patterns of properties commonly used in practice) shows that our approach drastically reduces the construction time of the symbolic NGBA, and positively affects the overall search time.