自动机理论在验证PSL中的应用

论文摘要

随着信息技术的发展，集成电路的规模和复杂度不断扩大，验证在这个项目的开发周期越来越长，而且集成电路市场竞争也越来越激烈。保证设计功能的正确性并尽量缩短产品投入市场的时间成为产品成功的关键，这也对验证技术和方法提出了越来越高的要求。要保证功能正确性，就要保证设计在实现时符合设计规范。因此，作为设计规范的描述语言必须有强大的表达能力，能够精确描述设计要求，同时还要易于使用。PSL就是符合这种要求的语言之一。PSL可以描述断言，并且可以嵌入到设计之中，为验证提供便利，能有效地缩短了验证时间。PSL还有一个更吸引人的地方：它既可以用于动态验证的输入，也可以作为形式验证工具的属性刻画语言。凭借着这些优点，PSL已经成为工业界属性刻画语言的标准。本文研究了如何使用自动机理论实现PSL的动态验证与模型检验。在动态验证PSL的讨论中，本文介绍了序列自动机以及如何将PSL转化为序列自动机。在模型检验PSL的研究中，本文提出了一个为PSL构造Büchi自动机的方法，该方法是构造LTL Büchi自动机的扩展。

论文目录

• 摘要
• ABSTRACT
• 目录
• 第一章 绪论
• 1.1 设计与验证
• 1.2 验证方法论
• 1.2.1 模拟仿真技术
• 1.2.2 模型检验
• 1.3 基于断言的验证（ABV）
• 1.4 本文的研究内容和意义
• 第二章 PSL介绍
• 2.1 属性规范语言 PSL
• 2.2 基本术语
• 2.3 概念
• 2.3.1 有限行为与无限行为
• 2.3.2 “强”的概念
• 2.4 PSL语法和语义
• 2.4.1 语法
• 2.4.2 语义
• 2.5 小结
• 第三章 动态验证 PSL
• 3.1 概念
• 3.2 为SEREs构造自动机
• 3.2.1 正则表达式与自动机
• 3.2.2 SEREs与序列自动机
• 3.3 责任模式下的自动机
• 3.3.1 确定化序列自动机
• 3.3.2 构造失败序列自动机
• 3.4 属性转化为自动机
• 3.5 小结
• 第四章 模型检测 LTL
• 4.1 基于自动机理论的模型检测
• 4.2 自动机理论
• 4.2.1 Büchi 自动机
• 4.2.2 Büchi 自动机的一些结论
• 4.2.3 交替（alternating）自动机
• 4.2.4 交替 Büchi 自动机
• 4.3 为 LTL 构造 Büchi 自动机
• 4.3.1 LTL 语法语义
• 4.3.2 构造交替 Büchi 自动机
• 4.4 小结
• 第五章 模型检测 PSL
• 5.1 模型检测 PSL 的研究现状
• WR 逻辑'>5.2 LTL_WR 逻辑
• WR 构造交替 Büchi 自动机'>5.3 为 LTL_WR 构造交替 Büchi 自动机
• 5.3.1 几个命题
• WRA 逻辑'>5.3.2 LTL_WRA 逻辑
• WRA构造交替 Büchi 自动机'>5.3.3 为件LTL_WRA构造交替 Büchi 自动机
• 5.4 小结
• 第六章 总结
• 参考文献
• 致谢