芯片形式化验证原理、方法与实战

本书系统介绍了形式化验证的概念和原理，并通过丰富的实例生动展示了形式化验证所需的TCL和SVA语言语法规则，同时揭示了其在商业上的潜在价值和广阔前景。书中以目前广泛采用的RISC-V架构为例，借助新思科技的VC Formal形式化验证工具，深入浅出地讲解了各种形式化验证应用的流程、使用方法以及常见陷阱，为读者提供了从基础知识到高级应用的学习途径。 本书包括三个部分： ? 基础篇（第1～6章），主要介绍形式化验证的工具、语言和设计； ? 实战篇（第7～13章），主要展示相关工具的使用方法、常见问题以及对应的解决方案； ? 进阶篇（第14～17章），主要探讨简化、签核和加速等关键形式化验证技术。 本书不仅适合芯片设计和开发领域的从业人员快速入门和实践形式化验证，也可以作为电子工程等相关专业的教学参考书。

王亮 <br />IC工程师，2008年毕业于西北工业大学计算机系统结构专业，拥有接近20年的芯片行业工作经验，先后就职于S3 Graphics（VIA，2年）、艾萨华科技（LSI，6年）、超微半导体（AMD，9年），目前就职于AMD GPU部门做GPU验证工作。<br /><br />谭永亮 <br />IC设计工程师，2008年研究生毕业于西北工业大学电路与系统专业，拥有接近20年的工作经验，目前就职于某IC创业公司，担任芯片设计经理。

目　　录<br />推荐序<br />前言<br />基础篇<br />第1章　芯片验证　2<br />1.1　什么是芯片验证　2<br />1.2　芯片验证的种类和过程　3<br />1.3　验证的现状　5<br />1.4　本章小结　7<br />第2章　验证策略概述　8<br />2.1　动态验证　9<br />2.1.1　EDA仿真　9<br />2.1.2　硬件仿真　11<br />2.1.3　FPGA原型验证　13<br />2.1.4　三种动态验证方式的比较　14<br />2.2　静态检查　15<br />2.2.1　语法语义检查　15<br />2.2.2　形式化验证　15<br />2.3　形式化验证和动态验证的优缺点<br />对比　19<br />2.4　形式化验证的现状和商业价值　21<br />2.5　学习形式化验证能做什么　26<br />2.6　本章小结　27<br />第3章　形式化验证基本原理和算法　28<br />3.1　形式化验证概述　28<br />3.1.1　等价性验证　28<br />3.1.2　模型检查　32<br />3.1.3　定理证明　32<br />3.2　硬件电路的形式化验证原理　33<br />3.3　二叉决策图概述　34<br />3.3.1　二叉决策图原理　34<br />3.3.2　有序二叉决策图　36<br />3.3.3　精简有序二叉决策图　36<br />3.3.4　BDD的不足　38<br />3.4　基于SAT的形式化验证　38<br />3.4.1　SAT原理　38<br />3.4.2　有界模型检查问题　40<br />3.5　BDD和SAT的比较　42<br />3.6　本章小结　42<br />第4章　形式化验证的流程和方法　43<br />4.1　形式化验证“三板斧”<br />——语言、工具和设计　43<br />4.1.1　语言　44<br />4.1.2　工具　44<br />4.1.3　设计　44<br />4.2　形式化验证相关的重要概念　45<br />4.2.1　安全属性和活性属性　45<br />4.2.2　断言的反例　45<br />4.2.3　有界证明和有界证明深度　45<br />4.2.4　过约束与欠约束　46<br />4.2.5　假成功　46<br />4.2.6　简化　47<br />4.3　形式化验证规划　48<br />4.3.1　形式化验证工具的适用场景　48<br />4.3.2　时序等价性检查的适用场景　49<br />4.3.3　不可达检查的适用场景　50<br />4.3.4　连接性检查的适用场景　50<br />4.3.5　X态传播检查的适用场景　50<br />4.4　形式化验证流程　51<br />4.4.1　验证计划　52<br />4.4.2　搭建验证平台　53<br />4.4.3　调试迭代　54<br />4.4.4　收集覆盖率和断言证出率　55<br />4.4.5　签核　55<br />4.5　形式化验证示例——定时器　55<br />4.5.1　定时器设计概述　56<br />4.5.2　定时器验证计划　59<br />4.5.3　定时器形式化验证过程　60<br />4.5.4　定时器形式化验证小结　67<br />4.6　本章小结　68<br />第5章　形式化验证断言语言　69<br />5.1　断言概述　69<br />5.1.1　什么是断言　69<br />5.1.2　为什么用断言　69<br />5.1.3　如何实现断言　70<br />5.2　断言语言SVA　73<br />5.2.1　断言结构及分类　73<br />5.2.2　序列　76<br />5.2.3　蕴含操作符　76<br />5.2.4　延时　78<br />5.2.5　SVA系统函数　79<br />5.2.6　重复操作符　80<br />5.2.7　disable iff　82<br />5.2.8　s_eventually　82<br />5.2.9　序列操作符　83<br />5.2.10　参数化　86<br />5.2.11　局部变量　86<br />5.2.12　合入断言的方式　87<br />5.2.13　多时钟　88<br />5.3　基于断言的设计　88<br />5.3.1　X态检查　89<br />5.3.2　独热码检查　89<br />5.3.3　格雷码检查　90<br />5.3.4　计数器溢出检查　90<br />5.3.5　仲裁器检查　90<br />5.3.6　先进先出队列　91<br />5.3.7　数据完整性检查　92<br />5.3.8　死锁检查　92<br />5.4　对形式化验证友好的SVA代码<br />风格　92<br />5.5　本章小结　93<br />第6章　形式化验证工具命令语言　94<br />6.1　TCL简介及其在IC中的应用　94<br />6.2　TCL高频语法　95<br />6.2.1　TCL例程　96<br />6.2.2　TCL数据类型和基础操作　97<br />6.2.3　TCL分支和循环等控制流<br />操作　107<br />6.2.4　TCL子程序、命名空间　109<br />6.2.5　TCL文件操作　111<br />6.2.6　TCL正则表达式　113<br />6.3　本章小结　115<br />实战篇<br />第7章　形式化验证工具介绍　118<br />7.1　概述　118<br />7.2　新思科技的VC Formal　119<br />7.3　楷登电子的JasperGold　120<br />7.4　西门子的Questa Formal　121<br />7.5　工具的对标比较　121<br />7.6　本章小结　124<br />第8章　形式化属性验证——FPV　125<br />8.1　基于RISC-V的微型SoC　125<br />8.1.1　RISC-V SoC的特性列表　125<br />8.1.2　RISC-V SoC的设计框图　126<br />8.1.3　RISC-V SoC的顶层接口　127<br />8.1.4　RISC-V SoC的地址映射　127<br />8.1.5　RISC-V SoC概述　128<br />8.1.6　Wishbone总线概述　131<br />8.1.7　RISC-V SoC各个子模块的<br />功能　134<br />8.2　RISC-V SoC的FPV验证<br />计划　137<br />8.2.1　验证策略和验证对象功能<br />规范　137<br />8.2.2　形式化验证平台描述　137<br />8.2.3　验证对象的断言规则描述　138<br />8.3　FPV和RISC-V SoC验证平台　144<br />8.4　验证平台搭建和常见问题集锦　146<br />8.4.1　常见问题一：TCL脚本中没有<br />指定正确的复位信号　146<br />8.4.2　常见问题二：错误的约束导致<br />前置条件不成立　147<br />8.4.3　常见问题三：个别标准单元<br />没有Verilog模型，导致被黑<br />盒化，功能和预期不符　148<br />8.4.4　常见问题四：约束有冲突，<br />导致运行终止并报错　149<br />8.4.5　常见问题五：内部子模块使用的复位信号不是顶层指定的复位信号，导致断言失败　150<br />8.4.6　常见问题六：约束的SVA语法有误，导致约束“不符合预期”　150<br />8.4.7　其他常见问题　151<br />8.5　RISC-V SoC的验证过程和结果　152<br />8.5.1　形式化验证重要建议——加入<br />覆盖属性　152<br />8.5.2　RISC-V SoC形式化验证发现<br />的RTL缺陷和断言缺陷　154<br />8.5.3　形式化验证只能发现RTL<br />缺陷吗　161<br />8.5.4　约束、断言和覆盖属性的<br />实现方式　162<br />8.6　本章小结　163<br />第9章　时序等价性检查　164<br />9.1　时序等价性检查应用场景　165<br />9.1.1　门控时钟插入验证　165<br />9.1.2　不改变功能的功耗优化验证　166<br />9.1.3　重新切割流水线和时序优化<br />验证　167<br />9.1.4　删除某个不需要的特性或者<br />删除一些冗余代码　167<br />9.1.5　新增功能不影响原有功能　168<br />9.1.6　工程变更命令相关验证　168<br />9.1.7　硬编码到参数化的设计改动<br />验证　168<br />9.1.8　寄存器从带复位的改成不带<br />复位的　169<br />9.1.9　在可测性设计使能扫描模式<br />下，确保X态不会传播到下<br />游逻辑　169<br />9.2　验证环境和脚本流程　170<br />9.3　时序面积优化验证示例　172<br />9.3.1　流水线级数不变的多位数据<br />按位异或设计　172<br />9.3.2　32位加法器从一级增加到两<br />级流水线　174<br />9.4　RISC-V SoC门控时钟案例　175<br />9.5　使用SEQ工具验证的常见问题　178<br />9.5.1　使用SystemVerilog语法中的<br />bind操作错误　178<br />9.5.2　真正的设计缺陷　179<br />9.6　简化和签核　181<br />9.7　本章小结　184<br />第10章　不可达检查　187<br />10.1　什么是不可达检查　187<br />10.2　常见的代码覆盖率的种类　188<br />10.3　常见的不可达的场景　188<br />10.3.1　信号值固定　189<br />10.3.2　某些功能的禁用导致<br />不可达　189<br />10.3.3　RTL存在冗余代码　190<br />10.3.4　RTL中信号存在多余位　190<br />10.3.5　信号之间存在依赖关系导致<br />不可达　191<br />10.3.6　RTL代码本身存在缺陷导致<br />不可达　191<br />10.4　不可达检查流程　192<br />10.5　不可达检查的使用阶段　193<br />10.5.1　早期验证阶段　193<br />10.5.2　动态仿真测试平台可用阶段　193<br />10.5.3　动态仿真测试平台成熟阶段　194<br />10.6　不可达检查实例　194<br />10.6.1　不读入覆盖率数据库的RISC-V SoC的不可达检查　194<br />10.6.2　动态仿真的覆盖率结果　195<br />10.6.3　读入覆盖率数据库文件的<br />不可达检查　196<br />10.6.4　动态仿真和形式化验证合并<br />的覆盖率结果　196<br />10.6.5　子模块的不可达检查结果<br />合并　197<br />10.7　本章小结　197<br />第11章　连接性检查　198<br />11.1　连接性检查概述　198<br />11.2　连接性检查方法学　200<br />11.3　基本流程示例　202<br />11.4　实例——RISC-V SoC的连接性<br />检查　202<br />11.4.1　RISC-V SoC的设计规范　202<br />11.4.2　连接规范对应的电路　203<br />11.4.3　表格形式的连接规范　205<br />11.4.4　检查结果　206<br />11.5　本章小结　207<br />第12章　X态传播检查　208<br />12.1　什么是X态传播　208<br />12.2　形式化X态传播检查工具的<br />用途　210<br />12.3　实例——RISC-V SoC的X态<br />传播检查　211<br />12.3.1　RISC-V SoC的X态传播<br />分析　211<br />12.3.2　RISC-V SoC的X态传播<br />检查流程　213<br />12.3.3　RISC-V SoC的TCL脚本<br />及运行结果　213<br />12.4　本章小结　214<br />第13章　事务级等价性检查　215<br />13.1　为什么使用事务级等价性检查　217<br />13.2　DPV流程和示例　217<br />13.3　DPV实践　219<br />13.4　本章小结　220<br />进阶篇<br />第14章　形式化验证关键技术——<br />简化　222<br />14.1　形式化验证的复杂度问题　224<br />14.2　复杂度简化策略　225<br />14.2.1　初始值简化　225<br />14.2.2　合理的过约束　226<br />14.2.3　断开设计中的某个信号　227<br />14.2.4　黑盒化　228<br />14.2.5　压缩设计单元大小　229<br />14.2.6　分治法　231<br />14.2.7　使用简化模型　232<br />14.2.8　使用符号变量、局部变量<br />或者加辅助代码　233<br />14.3　常见单元的简化示例　237<br />14.3.1　计数器的简化　237<br />14.3.2　存储器的简化　242<br />14.4　本章小结　243<br />第15章　形式化验证签核　244<br />15.1　形式化验证签核概述　244<br />15.2　形式化验证签核的要素　246<br />15.2.1　断言　246<br />15.2.2　约束　246<br />15.2.3　复杂度　247<br />15.2.4　覆盖率　248<br />15.3　形式化验证签核的流程　251<br />15.3.1　计划阶段　251<br />15.3.2　验证平台编写阶段　252<br />15.3.3　回归阶段　253<br />15.3.4　签核阶段　255<br />15.4　形式化验证签核的挑战　255<br />15.5　本章小结　256<br />第16章　形式化验证加速　257<br />16.1　复用AIP或断言库　258<br />16.1.1　使用EDA厂商提供的AIP　259<br />16.1.2　自研AIP——Valid-Ready<br />协议　260<br />16.1.3　断言库　264<br />16.2　开发自动化脚本　265<br />16.3　最大化利用机器资源　266<br />16.3.1　使用形式化验证工具提供的<br />拆分任务的命令　266<br />16.3.2　使用形式化验证工具提供的<br />AI加速命令　266<br />16.3.3　选择引擎　267<br />16.4　本章小结　267<br />第17章　形式化验证的道与术　268<br />17.1　形式化验证的道、法、术、器　268<br />17.1.1　道　269<br />17.1.2　法　269<br />17.1.3　术　269<br />17.1.4　器　270<br />17.2　形式化验证与动态仿真融合　270<br />17.2.1　区分形式化验证和动态仿真<br />的模块　270<br />17.2.2　合理规划形式化验证的应用<br />程序　271<br />17.2.3　复用断言和约束　271<br />17.2.4　动态仿真和形式化验证融合，<br />加速覆盖率收敛　272<br />17.2.5　回片后的调试　274<br />17.3　如何解决形式化验证遇到的问题　275<br />17.3.1　不理解设计　275<br />17.3.2　工具使用问题　276<br />17.3.3　断言语法问题　276<br />17.3.4　不确定断言是否生效　276<br />17.3.5　运行结果与预期不一致　277<br />17.3.6　无法完全证明　277<br />17.4　形式化验证的三重境界　277<br />17.5　本章小结　278<br />附录　代码包的目录及说明　280<br />技术术语表　281<br />参考文献　285<br />