| 致谢 | 第5-6页 |
| 摘要 | 第6-8页 |
| ABSTRACT | 第8-10页 |
| 1 绪论 | 第14-28页 |
| 1.1 研究背景及意义 | 第14-18页 |
| 1.2 相关研究 | 第18-24页 |
| 1.2.1 验证技术 | 第18-20页 |
| 1.2.2 断言验证方法学 | 第20-23页 |
| 1.2.3 代数化验证理论 | 第23-24页 |
| 1.3 论文的研究内容 | 第24-26页 |
| 1.4 论文的结构安排 | 第26-28页 |
| 2 相关知识 | 第28-46页 |
| 2.1 符号计算 | 第28-33页 |
| 2.1.1 Groebner基方法 | 第28-31页 |
| 2.1.2 吴方法 | 第31-33页 |
| 2.2 符号模拟验证方法 | 第33-40页 |
| 2.2.1 基本思想 | 第35-38页 |
| 2.2.2 基于STE的符号模拟 | 第38-40页 |
| 2.3 形式化验证方法 | 第40-45页 |
| 2.3.1 定理证明方法 | 第41-42页 |
| 2.3.2 等价性检验 | 第42-43页 |
| 2.3.3 模型检验 | 第43-45页 |
| 2.4 本章小结 | 第45-46页 |
| 3 基于代数化符号模拟的布尔层PSL性质验证 | 第46-60页 |
| 3.1 引言 | 第46-47页 |
| 3.2 PSL布尔层及其代数表示 | 第47-49页 |
| 3.3 布尔层组合电路建模 | 第49-50页 |
| 3.4 基于Groebner基验证算法及实例 | 第50-54页 |
| 3.4.1 基于Groebner基的验证算法 | 第50-52页 |
| 3.4.2 基于Groebner基的验证实例 | 第52-54页 |
| 3.5 基于吴方法验证算法及实例 | 第54-59页 |
| 3.5.1 基于吴方法的验证算法框架 | 第54-57页 |
| 3.5.2 基于吴方法的验证实例 | 第57-59页 |
| 3.6 本章小结 | 第59-60页 |
| 4 基于代数化符号模拟的SERE时序断言验证 | 第60-82页 |
| 4.1 引言 | 第60-61页 |
| 4.2 基于周期的符号模拟 | 第61-62页 |
| 4.3 系统多项式表示模型 | 第62-67页 |
| 4.3.1 算术、逻辑以及分支单元建模 | 第62-63页 |
| 4.3.2 时序单元建模及展开 | 第63-65页 |
| 4.3.3 时序操作符建模 | 第65-67页 |
| 4.4 SERE转换方法 | 第67-70页 |
| 4.4.1 代数化过程 | 第67-68页 |
| 4.4.2 布尔层建模 | 第68-70页 |
| 4.5 基于Groebner基算法框架 | 第70-74页 |
| 4.5.1 基于定理证明的验证理论 | 第70-71页 |
| 4.5.2 验证算法 | 第71-74页 |
| 4.6 基于Groebner基验证实例分析 | 第74-77页 |
| 4.6.1 电路及PSL建模 | 第74-76页 |
| 4.6.2 使用Maple进行断言验证 | 第76-77页 |
| 4.7 基于吴方法的SERE时序断言验证 | 第77-81页 |
| 4.7.1 基于吴方法验证的算法框架 | 第77-79页 |
| 4.7.2 基于吴方法验证的实例研究 | 第79-81页 |
| 4.8 本章小结 | 第81-82页 |
| 5 基于代数化符号模拟的SystemVerilog的并发断言验证 | 第82-116页 |
| 5.1 引言 | 第82-83页 |
| 5.2 SystemVerilog基础 | 第83-85页 |
| 5.3 同步数字系统以及多项式表示 | 第85-87页 |
| 5.3.1 组合逻辑模型 | 第85页 |
| 5.3.2 时序单元建模 | 第85-86页 |
| 5.3.3 符号模拟系统模型 | 第86-87页 |
| 5.4 多项式集合表示SVA表达式 | 第87-96页 |
| 5.4.1 多项式概念以及代数化 | 第87-88页 |
| 5.4.2 时间区间及其展开模型 | 第88-89页 |
| 5.4.3 时序的深度计算 | 第89-91页 |
| 5.4.4 时序操作符建模 | 第91-93页 |
| 5.4.5 局部变量表示及属性操作符建模 | 第93-95页 |
| 5.4.6 SystemVerilog断言的约束子集 | 第95-96页 |
| 5.5 基于Groebner基的SVA验证理论及算法 | 第96-98页 |
| 5.5.1 基于Groebner基断言验证原理 | 第96-97页 |
| 5.5.2 验证算法框架 | 第97-98页 |
| 5.6 基于Groebner基断言验证实例 | 第98-103页 |
| 5.6.1 电路及断言建模 | 第98-101页 |
| 5.6.2 使用Maple进行计算 | 第101-103页 |
| 5.7 基于吴方法的SVA验证理论及算法 | 第103-104页 |
| 5.7.1 基于吴方法的SVA验证原理 | 第103-104页 |
| 5.7.2 基于吴方法的SVA验证算法 | 第104页 |
| 5.8 基于吴方法的SVA实例验证及实验 | 第104-113页 |
| 5.8.1 电路及断言建模 | 第105-106页 |
| 5.8.2 使用MMP验证断言 | 第106-107页 |
| 5.8.3 经典仲裁器电路的实验 | 第107-112页 |
| 5.8.4 实验讨论 | 第112-113页 |
| 5.9 本章小结 | 第113-116页 |
| 6 总结与展望 | 第116-120页 |
| 6.1 研究工作总结 | 第116-118页 |
| 6.2 未来工作展望 | 第118-120页 |
| 参考文献 | 第120-126页 |
| 作者简历及攻读博士学位期间取得的研究成果 | 第126-132页 |
| 学位论文数据集 | 第132页 |
