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 omega-regular properties. In this paper, we propose a new method for efficiently converting PSL formulas into symbolically represented nondeterministic (generalized) Buchi 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 compilation time and positively affects the overall search time.
Symbolic Compilation of PSL
Cimatti, Alessandro;Roveri, Marco;Tonetta, Stefano
2008-01-01
Abstract
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 omega-regular properties. In this paper, we propose a new method for efficiently converting PSL formulas into symbolically represented nondeterministic (generalized) Buchi 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 compilation time and positively affects the overall search time.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
