DocumentCode :
867790
Title :
Symbolic Compilation of PSL
Author :
Cimatti, Alessandro ; Roveri, Marco ; Tonetta, Stefano
Author_Institution :
Embedded Syst. Unit, Inst. for Sci. & Technol. Res., Trento
Volume :
27
Issue :
10
fYear :
2008
Firstpage :
1737
Lastpage :
1750
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.
Keywords :
automata theory; formal specification; formal verification; temporal logic; binary decision diagram; hardware design cycle; linear temporal logic; modular encoding; natural formalism; nondeterministic generalized Buchi automata; property specification language; sequential extended regular expressions; specialized encoding; symbolic compilation; Automata; Binary decision diagrams; Costs; Encoding; Hardware; Logic; Modular construction; Pattern analysis; Specification languages; State-space methods; BÜchi automata; Binary Decision Diagram (${tt BDD}$); Property Specification Language (PSL); Satisfiability ( ${tt SAT}$); Sequential Extended Regular Expressions (SEREs); formal methods; formal verification; symbolic compilation;
fLanguage :
English
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
Publisher :
ieee
ISSN :
0278-0070
Type :
jour
DOI :
10.1109/TCAD.2008.2003303
Filename :
4627535
Link To Document :
بازگشت