在集成电路设计领域，验证方法主要分为两种：一种是依据激励响应模式的UVM（Universal Verification Methodology）方法，另一种则是基于数学定理证明的形式化验证方法。作者结合自己多年的形式化验证经验，系统地阐述了形式化验证的概念和原理，通过丰富的实例生动地展示了形式化验证所需的TCL语言和SVA语言语法规则。书中以目前广泛采用的RISC-V架构为例，借助业界领先的新思科技VC Formal形式化验证工具，全面展示了该工具中六种应用的使用方法、常见问题及其解决方案，为读者提供了从基础学习到高级应用的学习之路。 全书内容分为三个部分：第1至6章深探讨了形式化验证的优势、基础原理以及编程语言的语法规则；第7至12章首先对比介绍了三大EDA厂商提供的形式化验证工具集，随后给出六种形式化验证工具的实战部分，详细阐述了每种工具的用途、流程、使用方法和关键问题解决策略；第13至15章则聚焦于形式化验证的高级技术，包括形式化验证的关键技术—如何简化设计，以及如何通过自动化脚本和复用仿真环境的约束和检查器来提高验证的效率等。本书旨在帮助广大的IC工程师和学生快速门和实践形式化验证，避免到处搜集资料和频繁求助他人的低效学习模式，实现“一书在手，Formal无忧” 的目标。
售 价：¥
纸质售价：¥71.30购买纸书
6.5
温馨提示：数字商品不支持退换货，不提供源文件，不支持导出打印
为你推荐
推荐序
前言
基础篇
第1章 芯片验证
1.1 什么是芯片验证
1.2 芯片验证的种类和过程
1.3 验证的现状
1.4 本章小结
第2章 验证策略概述
2.1 动态验证
2.2 静态检查
2.3 形式化验证和动态验证的优缺点对比
2.4 形式化验证的现状和商业价值
2.5 学习形式化验证能做什么
2.6 本章小结
第3章 形式化验证基本原理和算法
3.1 形式化验证概述
3.2 硬件电路的形式化验证原理
3.3 二叉决策图概述
3.4 基于SAT的形式化验证
3.5 BDD和SAT的比较
3.6 本章小结
第4章 形式化验证的流程和方法
4.1 形式化验证“三板斧”——语言、工具和设计
4.2 形式化验证相关的重要概念
4.3 形式化验证规划
4.4 形式化验证流程
4.5 形式化验证示例——定时器
4.6 本章小结
第5章 形式化验证断言语言
5.1 断言概述
5.2 断言语言SVA
5.3 基于断言的设计
5.4 对形式化验证友好的SVA代码风格
5.5 本章小结
第6章 形式化验证工具命令语言
6.1 TCL简介及其在IC中的应用
6.2 TCL高频语法
6.3 本章小结
实战篇
第7章 形式化验证工具介绍
7.1 概述
7.2 新思科技的VC Formal
7.3 楷登电子的JasperGold
7.4 西门子的Questa Formal
7.5 工具的对标比较
7.6 本章小结
第8章 形式化属性验证——FPV
8.1 基于RISC-V的微型SoC
8.2 RISC-V SoC的FPV验证计划
8.3 FPV和RISC-V SoC验证平台
8.4 验证平台搭建和常见问题集锦
8.5 RISC-V SoC的验证过程和结果
8.6 本章小结
第9章 时序等价性检查
9.1 时序等价性检查应用场景
9.2 验证环境和脚本流程
9.3 时序面积优化验证示例
9.4 RISC-V SoC门控时钟案例
9.5 使用SEQ工具验证的常见问题
9.6 简化和签核
9.7 本章小结
第10章 不可达检查
10.1 什么是不可达检查
10.2 常见的代码覆盖率的种类
10.3 常见的不可达的场景
10.4 不可达检查流程
10.5 不可达检查的使用阶段
10.6 不可达检查实例
10.7 本章小结
第11章 连接性检查
11.1 连接性检查概述
11.2 连接性检查方法学
11.3 基本流程示例
11.4 实例——RISC-V SoC的连接性检查
11.5 本章小结
第12章 X态传播检查
12.1 什么是X态传播
12.2 形式化X态传播检查工具的用途
12.3 实例——RISC-V SoC的X态传播检查
12.4 本章小结
第13章 事务级等价性检查
13.1 为什么使用事务级等价性检查
13.2 DPV流程和示例
13.3 DPV实践
13.4 本章小结
进阶篇
第14章 形式化验证关键技术——简化
14.1 形式化验证的复杂度问题
14.2 复杂度简化策略
14.3 常见单元的简化示例
14.4 本章小结
第15章 形式化验证签核
15.1 形式化验证签核概述
15.2 形式化验证签核的要素
15.3 形式化验证签核的流程
15.4 形式化验证签核的挑战
15.5 本章小结
第16章 形式化验证加速
16.1 复用AIP或断言库
16.2 开发自动化脚本
16.3 最大化利用机器资源
16.4 本章小结
第17章 形式化验证的道与术
17.1 形式化验证的道、法、术、器
17.2 形式化验证与动态仿真融合
17.3 如何解决形式化验证遇到的问题
17.4 形式化验证的三重境界
17.5 本章小结
附录 代码包的目录及说明
技术术语表
参考文献
买过这本书的人还买过
读了这本书的人还在读
同类图书排行榜
购物车
个人中心
