| 开本：16开 |
| 纸张：胶版纸 |
| 包装：平装-胶订 |
| 是否套装：否 |
| 国际标准书号ISBN：9787111782681 |
| 所属分类：图书>工业技术>金属学与金属工艺 |
团购优惠，咨询在线客服
商品详情
基本信息（以实物为准）
商品名称：芯片形式化验证原理、方法与实战
作者：王亮 谭永亮 定 开
出版社：机械工业 号 页数
出版时间 版次 商品类型：图书
印刷时间 印次
目 录
目 录
序
前言
基础篇
第章 芯片验证
什么是芯片验证
芯片验证的种类和过程
验证的现状
本章小结
第章 验证策略概述
动态验证
仿真
硬件仿真
原型验证
三种动态验证方式的比较
静态检查
语法语义检查
形式化验证
形式化验证和动态验证的优缺点
对比
形式化验证的现状和商业
学习形式化验证能做什么
本章小结
第章 形式化验证基本原理和算法
形式化验证概述
等价性验证
模型检查
定理证明
硬件电路的形式化验证原理
二叉决策图概述
二叉决策图原理
有序二叉决策图
精简有序二叉决策图
的不足
基于的形式化验证
原理
有界模型检查问题
和的比较
本章小结
第章 形式化验证的流程和方法
形式化验证“三板斧”
——语言、工具和设计
语言
工具
设计
形式化验证相关的重要概念
安全属性和活性属性
断言的反例
有界证明和有界证明深度
过约束与欠约束
假成功
简化
形式化验证规划
形式化验证工具的适用场景
时序等价性检查的适用场景
不可达检查的适用场景
连接性检查的适用场景
态传播检查的适用场景
形式化验证流程
验证计划
搭建验证平台
调试迭代
收集覆盖率和断言证出率
签核
形式化验证示例——定时器
定时器设计概述
定时器验证计划
定时器形式化验证过程
定时器形式化验证小结
本章小结
第章 形式化验证断言语言
断言概述
什么是断言
为什么用断言
如何实现断言
断言语言
断言结构及分类
序列
蕴含操作符
延时
系统函数
重复操作符
序列操作符
参数化
局部变量
合入断言的方式
多时钟
基于断言的设计
态检查
独热码检查
格雷码检查
计数器溢出检查
仲裁器检查
先出队列
数据完整性检查
死锁检查
对形式化验证友好的代码
风格
本章小结
第章 形式化验证工具命令语言
简介及其在中的应用
高频语法
例程
数据类型和基础操作
分支和循环等控制流
操作
子程序、命名空间
文件操作
正则表达式
本章小结
实战篇
第章 形式化验证工具介绍
概述
新思科技的
楷登电子的
西门子的
工具的对标比较
本章小结
第章 形式化属性验证——
基于的微型
的特性列表
的设计框图
的顶层接口
的地址映射
概述
总线概述
各个子模块的
功能
的验证
计划
验证策略和验证对象功能
规范
形式化验证平台描述
验证对象的断言规则描述
和 验证平台
验证平台搭建和常见问题集锦
常见问题一：脚本中没有
正确的复位信号
常见问题二：错误的约束导致
前置条件不成立
常见问题三：个别标准单元
没有模型，导致被黑
盒化，功能和预期不符
常见问题四：约束有冲突，
导致运行终止并报错
常见问题五：内部子模块使用的复位信号不是顶层 的复位信号，导致断言失败
常见问题六：约束的语法有误，导致约束“不符合预期”
其他常见问题
的验证过程和结果
形式化验证重要建议——加入
覆盖属性
形式化验证发现
的缺陷和断言缺陷
形式化验证只能发现
缺陷吗
约束、断言和覆盖属性的
实现方式
本章小结
第章 时序等价性检查
时序等价性检查应用场景
门控时钟插入验证
不改变功能的功耗优化验证
重新切割流水线和时序优化
验证
删除某个不需要的特性或者
删除一些冗余代码
新增功能不影响原有功能
工程变 命令相关验证
硬编码到参数化的设计改动
验证
寄存器从带复位的改成不带
复位的
在可测性设计使能扫描模式
下，确保态不会传播到下
游逻辑
验证环境和脚本流程
时序面积优化验证示例
流水线级数不变的多位数据
按位异或设计
位加法器从一级增加到两
级流水线
门控时钟案例
使用工具验证的常见问题
使用语法中的
操作错误
真正的设计缺陷
简化和签核
本章小结
章 不可达检查
什么是不可达检查
常见的代码覆盖率的种类
常见的不可达的场景
信号值固定
某些功能的禁用导致
不可达
存在冗余代码
中信号存在多余位
信号之间存在依赖关系导致
不可达
代码本身存在缺陷导致
不可达
不可达检查流程
不可达检查的使用阶段
早期验证阶段
动态仿真测试平台可用阶段
动态仿真测试平台成熟阶段
不可达检查实例
不读入覆盖率数据库的 的不可达检查
动态仿真的覆盖率结果
读入覆盖率数据库文件的
不可达检查
动态仿真和形式化验证合并
的覆盖率结果
子模块的不可达检查结果
合并
本章小结
章 连接性检查
连接性检查概述
连接性检查方法学
基本流程示例
实例—— 的连接性
检查
的设计规范
连接规范对应的电路
表格形式的连接规范
检查结果
本章小结
章 态传播检查
什么是态传播
形式化态传播检查工具的
用途
实例—— 的态
传播检查
的态传播
分析
的态传播
检查流程
的脚本
及运行结果
本章小结
章 事务级等价性检查
为什么使用事务级等价性检查
流程和示例
实践
本章小结
进阶篇
章 形式化验证关键技术——
简化
形式化验证的复杂度问题
复杂度简化策略
初始值简化
合理的过约束
断开设计中的某个信号
黑盒化
压缩设计单元大小
分治法
使用简化模型
使用符号变量、局部变量
或者加辅助代码
常见单元的简化示例
计数器的简化
存储器的简化
本章小结
章 形式化验证签核
形式化验证签核概述
形式化验证签核的要素
断言
约束
复杂度
覆盖率
形式化验证签核的流程
计划阶段
验证平台编写阶段
回归阶段
签核阶段
形式化验证签核的挑战
本章小结
章 形式化验证加速
复用或断言库
使用厂商提供的
自研——
协议
断言库
开发自动化脚本
化利用机器资源
使用形式化验证工具提供的
拆分任务的命令
使用形式化验证工具提供的
加速命令
选择引擎
本章小结
章 形式化验证的道与术
形式化验证的道、法、术、器
道
法
术
器
形式化验证与动态仿真融合
区分形式化验证和动态仿真
的模块
合理规划形式化验证的应用
程序
复用断言和约束
动态仿真和形式化验证融合，
加速覆盖率收敛
回片后的调试
如何解决形式化验证遇到的问题
不理解设计
工具使用问题
断言语法问题
不确定断言是否生效
运行结果与预期不一致
无法 证明
形式化验证的三重境界
本章小结
附录 代码包的目录及说明
技术术语表
参考文献
显示全部信息
作者简介
王亮
工程师，年毕业于西北工业大学计算机系统结构专业，拥有接近年的芯片行业工作经验，先后就职于 （，年）、艾萨华科技（，年）、超微半导体（，年），目前就职于 部门做验证工作。
谭永亮
设计工程师，年研究生毕业于西北工业大学电路与系统专业，拥有接近年的工作经验，目前就职于某创业公司，担任芯片设计经理。
商品详情
基本信息（以实物为准）
商品名称：芯片形式化验证原理、方法与实战
作者：王亮 谭永亮 定 开
出版社：机械工业 号 页数
出版时间 版次 商品类型：图书
印刷时间 印次
目 录
目 录
序
前言
基础篇
第章 芯片验证
什么是芯片验证
芯片验证的种类和过程
验证的现状
本章小结
第章 验证策略概述
动态验证
仿真
硬件仿真
原型验证
三种动态验证方式的比较
静态检查
语法语义检查
形式化验证
形式化验证和动态验证的优缺点
对比
形式化验证的现状和商业
学习形式化验证能做什么
本章小结
第章 形式化验证基本原理和算法
形式化验证概述
等价性验证
模型检查
定理证明
硬件电路的形式化验证原理
二叉决策图概述
二叉决策图原理
有序二叉决策图
精简有序二叉决策图
的不足
基于的形式化验证
原理
有界模型检查问题
和的比较
本章小结
第章 形式化验证的流程和方法
形式化验证“三板斧”
——语言、工具和设计
语言
工具
设计
形式化验证相关的重要概念
安全属性和活性属性
断言的反例
有界证明和有界证明深度
过约束与欠约束
假成功
简化
形式化验证规划
形式化验证工具的适用场景
时序等价性检查的适用场景
不可达检查的适用场景
连接性检查的适用场景
态传播检查的适用场景
形式化验证流程
验证计划
搭建验证平台
调试迭代
收集覆盖率和断言证出率
签核
形式化验证示例——定时器
定时器设计概述
定时器验证计划
定时器形式化验证过程
定时器形式化验证小结
本章小结
第章 形式化验证断言语言
断言概述
什么是断言
为什么用断言
如何实现断言
断言语言
断言结构及分类
序列
蕴含操作符
延时
系统函数
重复操作符
序列操作符
参数化
局部变量
合入断言的方式
多时钟
基于断言的设计
态检查
独热码检查
格雷码检查
计数器溢出检查
仲裁器检查
先出队列
数据完整性检查
死锁检查
对形式化验证友好的代码
风格
本章小结
第章 形式化验证工具命令语言
简介及其在中的应用
高频语法
例程
数据类型和基础操作
分支和循环等控制流
操作
子程序、命名空间
文件操作
正则表达式
本章小结
实战篇
第章 形式化验证工具介绍
概述
新思科技的
楷登电子的
西门子的
工具的对标比较
本章小结
第章 形式化属性验证——
基于的微型
的特性列表
的设计框图
的顶层接口
的地址映射
概述
总线概述
各个子模块的
功能
的验证
计划
验证策略和验证对象功能
规范
形式化验证平台描述
验证对象的断言规则描述
和 验证平台
验证平台搭建和常见问题集锦
常见问题一：脚本中没有
正确的复位信号
常见问题二：错误的约束导致
前置条件不成立
常见问题三：个别标准单元
没有模型，导致被黑
盒化，功能和预期不符
常见问题四：约束有冲突，
导致运行终止并报错
常见问题五：内部子模块使用的复位信号不是顶层 的复位信号，导致断言失败
常见问题六：约束的语法有误，导致约束“不符合预期”
其他常见问题
的验证过程和结果
形式化验证重要建议——加入
覆盖属性
形式化验证发现
的缺陷和断言缺陷
形式化验证只能发现
缺陷吗
约束、断言和覆盖属性的
实现方式
本章小结
第章 时序等价性检查
时序等价性检查应用场景
门控时钟插入验证
不改变功能的功耗优化验证
重新切割流水线和时序优化
验证
删除某个不需要的特性或者
删除一些冗余代码
新增功能不影响原有功能
工程变 命令相关验证
硬编码到参数化的设计改动
验证
寄存器从带复位的改成不带
复位的
在可测性设计使能扫描模式
下，确保态不会传播到下
游逻辑
验证环境和脚本流程
时序面积优化验证示例
流水线级数不变的多位数据
按位异或设计
位加法器从一级增加到两
级流水线
门控时钟案例
使用工具验证的常见问题
使用语法中的
操作错误
真正的设计缺陷
简化和签核
本章小结
章 不可达检查
什么是不可达检查
常见的代码覆盖率的种类
常见的不可达的场景
信号值固定
某些功能的禁用导致
不可达
存在冗余代码
中信号存在多余位
信号之间存在依赖关系导致
不可达
代码本身存在缺陷导致
不可达
不可达检查流程
不可达检查的使用阶段
早期验证阶段
动态仿真测试平台可用阶段
动态仿真测试平台成熟阶段
不可达检查实例
不读入覆盖率数据库的 的不可达检查
动态仿真的覆盖率结果
读入覆盖率数据库文件的
不可达检查
动态仿真和形式化验证合并
的覆盖率结果
子模块的不可达检查结果
合并
本章小结
章 连接性检查
连接性检查概述
连接性检查方法学
基本流程示例
实例—— 的连接性
检查
的设计规范
连接规范对应的电路
表格形式的连接规范
检查结果
本章小结
章 态传播检查
什么是态传播
形式化态传播检查工具的
用途
实例—— 的态
传播检查
的态传播
分析
的态传播
检查流程
的脚本
及运行结果
本章小结
章 事务级等价性检查
为什么使用事务级等价性检查
流程和示例
实践
本章小结
进阶篇
章 形式化验证关键技术——
简化
形式化验证的复杂度问题
复杂度简化策略
初始值简化
合理的过约束
断开设计中的某个信号
黑盒化
压缩设计单元大小
分治法
使用简化模型
使用符号变量、局部变量
或者加辅助代码
常见单元的简化示例
计数器的简化
存储器的简化
本章小结
章 形式化验证签核
形式化验证签核概述
形式化验证签核的要素
断言
约束
复杂度
覆盖率
形式化验证签核的流程
计划阶段
验证平台编写阶段
回归阶段
签核阶段
形式化验证签核的挑战
本章小结
章 形式化验证加速
复用或断言库
使用厂商提供的
自研——
协议
断言库
开发自动化脚本
化利用机器资源
使用形式化验证工具提供的
拆分任务的命令
使用形式化验证工具提供的
加速命令
选择引擎
本章小结
章 形式化验证的道与术
形式化验证的道、法、术、器
道
法
术
器
形式化验证与动态仿真融合
区分形式化验证和动态仿真
的模块
合理规划形式化验证的应用
程序
复用断言和约束
动态仿真和形式化验证融合，
加速覆盖率收敛
回片后的调试
如何解决形式化验证遇到的问题
不理解设计
工具使用问题
断言语法问题
不确定断言是否生效
运行结果与预期不一致
无法 证明
形式化验证的三重境界
本章小结
附录 代码包的目录及说明
技术术语表
参考文献
显示全部信息
作者简介
王亮
工程师，年毕业于西北工业大学计算机系统结构专业，拥有接近年的芯片行业工作经验，先后就职于 （，年）、艾萨华科技（，年）、超微半导体（，年），目前就职于 部门做验证工作。
谭永亮
设计工程师，年研究生毕业于西北工业大学电路与系统专业，拥有接近年的工作经验，目前就职于某创业公司，担任芯片设计经理。