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

摘要

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

目录

文摘

英文文摘

声明

第一章绪论

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的研究现状

5.2 LTL_WR逻辑

5.3为LTL_WR构造交替Büchi自动机

5.3.1几个命题

5.3.2 LTL_WRA逻辑

5.3.3为LTL_WRA构造交替Büchi自动机

5.4小结

第六章总结

参考文献

致谢