基于SystemC的时态逻辑属性验证方法研究

论文摘要

系统复杂性继续按照摩尔定律增加,而功能复杂性的增加速度则更加迅猛。为解决复杂性增加的问题,EDA行业提出了通过自动化来实现设计抽象(Design Abstraction)的概念。由于设计生产率的提升速度低于系统复杂性的增速,此时与设计相关的瓶颈已并非设计时间,而是验证时间,即验证瓶颈。为此,人们创建了能够在不同抽象级别上对复杂系统设计进行验证的新型验证语言,例如,高级验证语言SystemC。实践证明SystemC是一种优秀的系统设计描述验证语言,它能够完成从系统级到门级、从软件到硬件、从设计到验证的全部描述。本文阐述了基于SystemC的主要验证方法和相关理论,以及时态逻辑理论和在验证领域中的应用,一方面分析了在动态仿真中已有的基于SystemC时态逻辑属性验证方法存在的不足,改进了动态仿真中时态逻辑属性描述方法,并在此基础上提出了一种属性化简方案,提高了仿真性能;另一方面实现了SystemC电路的可达性分析,及基于可达性分析的时态逻辑属性验证算法,并通过实验证实了文中提出的属性验证方法的有效性。本文的主要贡献如下:1.从动态仿真的角度来验证时态逻辑属性,本文在R.Dechsler等人提出的基于SystemC属性检查器验证方法的基础上进一步研究,分析了已有属性描述方法的不足,提出了一种改进的属性化简的描述方法,并通过实验验证了改进方案的有效性。2.从可达性分析的角度来验证时序电路的时态逻辑属性,针对基于SvstemC描述的门级电路,提出了时序电路可达性分析的实现方案。主要包括门级时序电路信息提取方法和时序状态转移函数构建方法的实现,其中时序状态转移函数通过bdd来构造,然后通过对状态转移函数的bdd表示进行求解来获取状态间的转移关系。最后通过4个基本时序电路实例来说明可达性分析方案的可行性。3.在可达性分析的基础上,进一步验证时序电路的时态逻辑属性。时态逻辑属性仍然采取前面提到的动态仿真方法中属性描述方法。结合属性描述方法,提出了一种时态属性验证方案并实现了该算法,并将该属性验证算法应用于基于SystemC描述的时序电路等价性问题上,将时序等价问题转换成时态逻辑验证问题来完成等价性验证问题,并通过实例进行说明验证算法的有效性。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 SystemC的发展历史
• 1.2 基于SystemC的验证方法研究现状
• 1.3 本文主要工作
• 1.4 本文组织结构
• 第二章 SystemC
• 2.1 SystemC简介
• 2.2 SystemC基本库介绍
• 2.2.1 模块
• 2.2.2 数据类型
• 2.2.3 接口、端口和通道
• 2.2.4 进程
• 2.2.5 模块和通道例化
• 2.2.6 仿真与波形跟踪
• 2.3 SystemC新增标准介绍
• 2.4 SystemC仿真语义
• 2.5 本章小结
• 第三章 时态逻辑属性与可达性分析
• 3.1 断言验证与时态逻辑
• 3.1.1 属性规格语言简介
• 3.1.2 SystemC和属性断言
• 3.2 形式验证与时态逻辑
• 3.2.1 线性时态逻辑
• 3.2.2 计算树逻辑
• 3.2.3 时态逻辑的符号模型检验理论
• 3.2.4 基于BDD的符号计算
• 3.3 本章小结
• 第四章 基于属性描述的仿真验证方法研究与改进
• 4.1 属性定义
• 4.2 属性描述
• 4.3 属性描述改进和属性化简
• 4.3.1 属性描述方法改进
• 4.3.2 属性化简方案
• 4.3.3 改进前后实验结果对比
• 4.4 本章小结
• 第五章 基于可达性分析的属性验证方法研究与实现
• 5.1 SystemC电路的可达性分析
• 5.1.1 电路信息提取模块的实现
• 5.1.2 构建电路状态转移函数
• 5.1.3 实例说明
• 5.2 基于可达性分析的属性验证方法
• 5.2.1 线性时态逻辑属性验证算法的实现
• 5.2.2 将电路时序等价性问题转换成属性验证问题
• 5.3 实验结果分析
• 5.4 本章小结
• 第六章 结束语
• 6.1 本文的主要贡献
• 6.2 后续的工作展望
• 参考文献
• 附录
• 致谢
• 攻读学位期间发表的学术论文
• 北京化工大学硕士研究生学位论文答辩委员会决议书