封面
前折页
书名页
译者序
第2版序
第1版序
致谢
第1章 形式化验证（FV）：从梦想到现实
 1.1 FV是什么
 1.2 为什么是这本书
 1.3 一个鼓舞人心的轶事
 1.4 FV：更深层次
  1.4.1 FV的整体优势
  1.4.2 FV的一般使用模型
  1.4.3 完整覆盖的FV
  1.4.4 本书未讨论的FV方法
 1.5 实用FV的出现
  1.5.1 早期自动推理
  1.5.2 计算机科学应用
  1.5.3 模型检查变得切实可用
  1.5.4 断言的标准化
 1.6 实施FV的挑战
  1.6.1 数学的基本局限性
  1.6.2 复杂性理论
  1.6.3 好消息
 1.7 增强形式化的力量
 1.8 充分利用这本书
 1.9 本章实用建议
 进一步阅读
第2章 基础形式化验证（FV）算法
 2.1 验证过程中的FV
 2.2 一个简单的自动售货机示例
 2.3 模型比较
 2.4 影响锥
 2.5 规范操作定义
  2.5.1 智能构建真值表
  2.5.2 添加顺序逻辑
 2.6 布尔代数符号
  2.6.1 布尔代数基本定律
  2.6.2 规范比较
 2.7 二元决策图（BDD）
  2.7.1 计算电路设计的BDD
  2.7.2 使用BDD进行模型检查
 2.8 布尔可满足性（SAT）
  2.8.1 有界模型检查
  2.8.2 解决SAT问题
  2.8.3 Davis-Putnam SAT算法
  2.8.4 Davis-Logemann-Loveland SAT算法
 2.9 总结
 进一步阅读
第3章 SystemVerilog断言简介
 3.1 基本断言概念
  3.1.1 一个简易仲裁器实例
  3.1.2 断言是什么
  3.1.3 假设是什么
  3.1.4 覆盖属性是什么
  3.1.5 断言语句的说明
  3.1.6 SVA语言基础
  3.1.7 即时断言
  3.1.8 编写即时断言
  3.1.9 过程代码的复杂性及采用assert final的动机
  3.1.10 过程块中的位置
  3.1.11 布尔构建块
  3.1.12 并发断言基础和时钟控制
  3.1.13 采样和断言时钟
  3.1.14 采样值函数
  3.1.15 并发断言的时钟边沿
  3.1.16 并发断言的重置（禁用）条件
  3.1.17 设置默认时钟和重置
 3.2 序列、属性和并发断言
  3.2.1 序列语法和示例
  3.2.2 属性语法和示例
  3.2.3 命名序列和属性
  3.2.4 断言和隐式多线程
  3.2.5 常量的挑战
  3.2.6 编写属性
 3.3 总结
 3.4 本章实用建议
 进一步阅读
第4章 形式化属性验证（FPV）
 4.1 什么是FPV
 4.2 本章示例：组合锁
 4.3 搭建基础的FPV环境
  4.3.1 编译RTL
  4.3.2 创建覆盖属性
  4.3.3 创建假设
  4.3.4 创建断言
  4.3.5 时钟和复位
  4.3.6 运行验证
 4.4 FPV与仿真有何不同
  4.4.1 可以运行哪些类型和规模的模型
  4.4.2 如何达到目标行为
  4.4.3 检查哪些值
  4.4.4 我们如何约束模型
  4.4.5 如何处理内部节点的约束
  4.4.6 我们用什么进行调试
  4.4.7 典型轨迹有多长
 4.5 决定在哪里以及如何运行FPV
  4.5.1 运行FPV的动机
  4.5.2 使用设计探索FPV
  4.5.3 使用错误搜索FPV
  4.5.4 使用签核级FPV
  4.5.5 使用特定应用FPV
 4.6 总结
 4.7 本章实用建议
 进一步阅读
第5章 用于设计探索的有效形式化属性验证（FPV）
 5.1 本章示例：交通灯控制器
 5.2 创建设计探索计划
  5.2.1 设计探索目标
  5.2.2 设计探索的主要属性
  5.2.3 复杂性分级计划
  5.2.4 退出标准
  5.2.5 整合计划
 5.3 设置设计探索FPV环境
  5.3.1 覆盖属性
  5.3.2 假设
  5.3.3 断言
  5.3.4 时钟和复位
  5.3.5 健全性（sanity）检查
 5.4 波形调试迭代（wiggling）设计
  5.4.1 wiggling过程
  5.4.2 wiggling阶段1：我们的第一个短波形
  5.4.3 调试另一个短波形
 5.5 探索更关键的行为
  5.5.1 回答一些新问题
  5.5.2 证明断言
 5.6 移除简化并探索更多行为
  5.6.1 面对复杂性问题
 5.7 总结
 5.8 本章实用建议
 进一步阅读
第6章 有效形式化属性验证（FPV）
 6.1 确定FPV目标
  6.1.1 错误搜索FPV
  6.1.2 签核级FPV
 6.2 FPV工作的分阶段进行
 6.3 本章示例：简单的ALU
 6.4 理解设计
 6.5 FPV验证计划的制定
  6.5.1 FPV目标
  6.5.2 FPV主要属性
  6.5.3 处理复杂性
  6.5.4 质量检查与退出标准
  6.5.5 初始覆盖属性
  6.5.6 扩展wiggling
  6.5.7 扩展覆盖属性
 6.6 去除简化和探索更多行为
  6.6.1 演进到签核级FPV
 6.7 总结
 6.8 本章实用建议
 进一步阅读
第7章 针对特定问题的形式化属性验证（FPV）APP
 7.1 可重用协议验证
  7.1.1 可重用属性集的基本设计
  7.1.2 属性方向问题
  7.1.3 验证属性集一致性
  7.1.4 完整性检查
  7.1.5 动态验证兼容性
 7.2 不可达覆盖消除
  7.2.1 在UCE中使用断言的作用
  7.2.2 覆盖组和其他覆盖类型
 7.3 连通性验证
  7.3.1 连通性模型构建
  7.3.2 指定连通性
  7.3.3 可能的连通性FPV复杂性
  7.3.4 连通性FPV的覆盖率
 7.4 控制寄存器验证
  7.4.1 指定控制寄存器要求
  7.4.2 控制寄存器的SVA
  7.4.3 控制寄存器验证的主要挑战
 7.5 硅后调试和反应性FPV
  7.5.1 硅后FPV的挑战
  7.5.2 UNEARTH：一种实用的硅后FPV方法
 7.6 总结
 7.7 本章实用建议
 进一步阅读
第8章 形式化等价性验证（FEV）
 8.1 等价性检查的类型
  8.1.1 组合等价性
  8.1.2 顺序等价性
  8.1.3 事务级等价性
 8.2 FEV用例
  8.2.1 RTL到网表FEV
  8.2.2 网表到网表FEV
  8.2.3 RTL到RTL FEV
 8.3 运行FEV
  8.3.1 选择模型
  8.3.2 关键点选择和映射
  8.3.3 假设和约束
  8.3.4 调试不匹配
 8.4 额外的FEV挑战
  8.4.1 状态元素优化
  8.4.2 条件等价性
  8.4.3 不关心空间
  8.4.4 复杂性
 8.5 总结
 8.6 本章实用建议
 进一步阅读
第9章 形式化验证最大的失误：误报的危险
 9.1 滥用SVA语言
  9.1.1 缺少分号
  9.1.2 两个时钟边沿均置位
  9.1.3 带断言的短路函数
  9.1.4 信号采样的微妙影响
  9.1.5 非生命状态的活性属性
  9.1.6 错误地假设一个序列
  9.1.7 预防与SVA相关的误报
 9.2 空洞问题
  9.2.1 误导性的覆盖属性与糟糕的重置
  9.2.2 经过验证但模拟失败的内存控制器
  9.2.3 假设与约束的矛盾
  9.2.4 队列永远不会满，因为它永远不会开始
  9.2.5 防止空洞工具和用户的责任
 9.3 隐含或未说明的假设
  9.3.1 具有实施假设的库
  9.3.2 对多重驱动信号的期望
  9.3.3 无法到达的逻辑元素：需要吗
  9.3.4 防止误解
 9.4 分工
  9.4.1 胶合逻辑缺失
  9.4.2 缺失案例的拆分
  9.4.3 撤销临时黑客攻击
  9.4.4 安全分工
 9.5 总结
 9.6 本章实用建议
 进一步阅读
第10章 应对复杂性
 10.1 设计状态和相关复杂性
 10.2 本章示例：内存控制器
 10.3 观察复杂性问题
 10.4 简单的收敛技术
  10.4.1 选择正确的战斗
  10.4.2 时钟和复位
  10.4.3 引擎调校
  10.4.4 黑盒化
  10.4.5 参数和尺寸减小
  10.4.6 案例拆分
  10.4.7 硬案例与软案例拆分
  10.4.8 属性简化
  10.4.9 切点
  10.4.10 增量FEV
 10.5 辅助假设与非辅助假设
  10.5.1 编写自定义辅助假设
  10.5.2 利用已证实的断言
  10.5.3 您是否有太多的假设
 10.6 使用自由变量进行概括分析
  10.6.1 利用刚性自由变量的对称性
  10.6.2 自由变量的其他用途
  10.6.3 自由变量的缺点
 10.7 降低复杂性的抽象模型
  10.7.1 反抽象
  10.7.2 序列抽象
  10.7.3 内存抽象
  10.7.4 影子模型
 10.8 半形式化验证
 10.9 规避复杂性问题：设计和验证协同工作
 10.10 总结
 10.11 本章的实用建议
 进一步阅读
第11章 实际项目中的形式化签核
 11.1 整体签核方法论
 11.2 规划和架构
  11.2.1 分治法识别DUT
  11.2.2 审查设计流程
  11.2.3 选择应用程序
  11.2.4 定义FPV细节
  11.2.5 填补空白
  11.2.6 制定应急计划
  11.2.7 FV融入设计节点中
 11.3 应用和实施
  11.3.1 确保定期进展
  11.3.2 做好应对反应性FV的准备
 11.4 覆盖和回归
  11.4.1 代码覆盖
  11.4.2 覆盖属性
  11.4.3 FV回归
  11.4.4 机器学习和回归
  11.4.5 网络与云端运行
  11.4.6 晚期重检
 11.5 跟踪和结束
  11.5.1 FV的质量
  11.5.2 时间线跟踪
  11.5.3 验证何时才算完成
 11.6 总结
 11.7 本章实用建议
第12章 全新的具有FV风格的生活方式
 12.1 使用FV
  12.1.1 设计探索
  12.1.2 错误搜索FPV
  12.1.3 签核级FV
  12.1.4 专用的FV应用程序
  12.1.5 形式化等价性验证
 12.2 个人使用FV的准备
 12.3 启动团队的FV工作
  12.3.1 设定合理的期望
  12.3.2 培养“领军人物”
  12.3.3 争取各级的支持
  12.3.4 合理跟踪FV的进展
  12.3.5 建立高效的基础设施
 12.4 使管理层开心
  12.4.1 ROI计算
  12.4.2 错误复杂性排名
 12.5 FV工作者实际做了什么
 12.6 总结
 12.7 本章实用建议
 进一步阅读
版权
后折页
封底