| 摘要 | 第1-4页 |
| Abstract | 第4-9页 |
| 第一章 绪论 | 第9-21页 |
| ·研究的背景及意义 | 第9-11页 |
| ·研究的现状 | 第11-18页 |
| ·基于断言的验证 | 第11-13页 |
| ·基于形式化方法的验证 | 第13-14页 |
| ·等价性检查 | 第14-15页 |
| ·模型检验 | 第15-17页 |
| ·定理证明 | 第17-18页 |
| ·作者的主要工作和创新点 | 第18-19页 |
| ·作者的主要工作 | 第18-19页 |
| ·创新点 | 第19页 |
| ·本文的组织结构 | 第19-21页 |
| 第二章 三值逻辑模型检验 | 第21-57页 |
| ·二值逻辑的模型检验 | 第21-24页 |
| ·Kripke 结构 | 第21-22页 |
| ·CTL 公式 | 第22-23页 |
| ·模型检验 | 第23-24页 |
| ·不完全 Kripke 结构（Partial Kripke Structure PKS） | 第24-25页 |
| ·不完全 Kripke 结构 | 第24-25页 |
| ·操作符的解释 | 第25页 |
| ·三值逻辑CTL 公式 | 第25-26页 |
| ·三值时态逻辑公式的模型检验 | 第26-34页 |
| ·三值逻辑公式的模型检验算法 | 第26-30页 |
| ·例子 | 第30-31页 |
| ·公平性约束的三值逻辑公式模型检验 | 第31-33页 |
| ·模型检验的复杂度分析 | 第33-34页 |
| ·三值时态逻辑公式的符号模型检验 | 第34-44页 |
| ·三叉判定图（TDD） | 第34-36页 |
| ·在化简的OTDD 上实现的操作 | 第36-40页 |
| ·基于OTDD 的符号模型检验 | 第40-44页 |
| ·三值逻辑模型检验的正例和反例 | 第44-52页 |
| ·存在路径量词的证明规则 | 第45-47页 |
| ·自动证明的产生 | 第47-50页 |
| ·通过证明过程产生正例的方法 | 第50-52页 |
| ·全称路径量词的反例 | 第52页 |
| ·应用 | 第52-54页 |
| ·在硬件验证中的应用 | 第52-53页 |
| ·在SOC 验证中的应用 | 第53-54页 |
| ·小结 | 第54-57页 |
| 第三章 模态转移系统到不完全 KRIPKE 结构的转换 | 第57-67页 |
| ·引言 | 第57页 |
| ·模态转移系统（Modal Transition System MTS） | 第57-60页 |
| ·模态转移系统 | 第57-58页 |
| ·Hennessy-Milner 逻辑公式（HML） | 第58-60页 |
| ·不完全 Kripke 结构下的命题模态逻辑 | 第60页 |
| ·MTS 转换成PKS | 第60-64页 |
| ·MTS 转换成PKS | 第60-61页 |
| ·逻辑公式的转换 | 第61-62页 |
| ·转换的正确性 | 第62-63页 |
| ·基于MTS 的模型检查算法 | 第63-64页 |
| ·MTS 转换成不完全 Kripke 结构复杂度分析 | 第64-65页 |
| ·相关的工作 | 第65-66页 |
| ·小结 | 第66-67页 |
| 第四章 模型检验中对 CTL 公式的空属性探测 | 第67-75页 |
| ·空属性（vacuity） | 第67-68页 |
| ·公式的空属性探测 | 第68-71页 |
| ·子公式集合的空属性探测 | 第68-70页 |
| ·有极性的CTL 公式的空探测 | 第70页 |
| ·空探测的方法 | 第70-71页 |
| ·一个例子 | 第71-73页 |
| ·总体设计 | 第71-72页 |
| ·描述 | 第72页 |
| ·模型检验及属性的空探测 | 第72-73页 |
| ·小结 | 第73-75页 |
| 第五章 基于 PSL 的模型检验的关键技术 | 第75-85页 |
| ·基于PSL 的模型检验技术 | 第75-76页 |
| ·属性描述语言PSL | 第76-78页 |
| ·基础语言部分（FL） | 第76页 |
| ·布尔表达式 | 第76-77页 |
| ·序列（SERES）公式 | 第77-78页 |
| ·FL 公式 | 第78页 |
| ·自动机的构造 | 第78-84页 |
| ·PSL 的形式化语法 | 第78-79页 |
| ·自动机的构造 | 第79-84页 |
| ·小结 | 第84-85页 |
| 第六章 用 PSL 验证宽带交换芯片 | 第85-105页 |
| ·SDH 技术 | 第85-87页 |
| ·SDH 概念 | 第85页 |
| ·SDH 速率 | 第85-86页 |
| ·SDH 帧结构 | 第86-87页 |
| ·SDH 帧中字节位置确定 | 第87页 |
| ·宽带电路交换芯片 | 第87-91页 |
| ·总体描述 | 第87-88页 |
| ·结构框图 | 第88-91页 |
| ·断言的必要性 | 第91页 |
| ·芯片验证思路 | 第91-92页 |
| ·验证步骤 | 第92-96页 |
| ·断言引入 | 第96-101页 |
| ·结果分析 | 第101-103页 |
| ·验证结果 | 第101-102页 |
| ·原因分析 | 第102-103页 |
| ·断言心得 | 第103页 |
| ·小结 | 第103-105页 |
| 第七章 PSL 在静态验证中的应用 | 第105-121页 |
| ·PSL 在 VIS 中的应用 | 第105-111页 |
| ·基于PSL 的VIS 验证原型系统 | 第105页 |
| ·VIS 使用的概要 | 第105-111页 |
| ·基于PSL 的仲裁器的验证 | 第111-119页 |
| ·仲裁器的设计 | 第111-114页 |
| ·仲裁器的属性 | 第114-115页 |
| ·对PSL 属性的验证 | 第115-119页 |
| ·小结 | 第119-121页 |
| 第八章 结论以及将来的工作 | 第121-123页 |
| ·总结 | 第121-122页 |
| ·基于三值逻辑的模型检验 | 第121页 |
| ·CTL 公式空属性的探测 | 第121-122页 |
| ·属性描述语言PSL 在基于断言的验证中的应用 | 第122页 |
| ·存在的问题和将来的工作 | 第122-123页 |
| 附录仲裁器设计及验证中的反例 | 第123-128页 |
| 致谢 | 第128-129页 |
| 参考文献 | 第129-136页 |
| 研究成果 | 第136-137页 |
