Symbolic Compilation of PSL
Symbolic Compilation of PSL
复制标题
PSL的符号编译
DOI：
10.1109/tcad.2008.2003303
复制
发表时间：
2008
影响因子：
2.9
通讯作者：
S. Tonetta
中科院分区：
文献类型：
--
作者：
A. Cimatti;Marco Roveri;S. Tonetta
IEEE标准属性规范语言（PSL）越来越多地用于硬件设计周期的许多阶段，从规范到验证。 PSL将线性时间逻辑（LTL）与顺序扩展的正则表达式（Seres）结合在一起，因此提供了一种自然形式主义，以表达所有欧米茄规范的特性。在本文中，我们提出了一种新方法，以有效地将PSL公式转换为象征性代表的非确定性（广义）Buchi Automata（NGBA），该方法通常用于许多验证和分析工具。该结构基于将LTL和SERE组件分开的正常形式，并允许模块化和专业编码。旨在减少所得NGBA的状态空间的一组句法变换增强了汇编。这些规则可以以低成本的价格实现，可以通过基于最小化的昂贵语义技术来实现简化。对大量范式特性（从实践中通常使用的属性模式）进行了彻底的实验分析表明，我们的方法大大减少了汇编时间，并对整体搜索时间产生了积极影响。
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.