浅析形式验证的分类、发展、适用场景
definition
formal verification：利用数学分析的方法，通过算法引擎建立模型，对待测设计的状态空间进行穷尽分析的验证。
kinds of formal verification
相比于动态仿真simulation veficiation，形式验证属于static verification，不需要手动灌入激励；通过数学分析的方式，对待测设计进行检查；
在这里插入图片描述
形式验证分为两大分支：equivalence checking 等价检查 和 property checking 属性检查 形式验证初次被eda工具采用，可以追溯到90年代，被应用于rtl code和gate level code的lec等价检查；后来形式验证开始慢慢发展，衍生出适用于不同场景的各类工具；
equivalence checking
combinational equivalence：用于rtl vs netlist的检查，检查寄存器之间的组合逻辑在综合前后是否一致，如formality，conformal。 sequential equivalence: 用于rtl vs rtl的检查，基于cycle的精确度；适用于对原有block级rtl做了非逻辑修改，如clock/power gating，对修改后的rtl进行等价检查。 transaction equivalence：用于c/c++ model vs rtl的检查，基于transaction的精确度；常用于数据通路的算法类设计。
property checking
属性检查基于psl/sva assertion languages，通过对property的assume,cover,assert语句分析，建立golden模型。fpv(formal property verification)需要用户直接书写property；从fpv衍生出各类app，适用于不同场景，可以根据相关配置，自动生成对应的property。
除了上述两类，cdc的检查也属于static verification；例如spyglass会对跨时钟域设计做structural 结构上的检查，检查跨时钟域的信号是否经过同步器处理；一般来讲，formal verification属于static verification;
simulation vs formal
simulation属于dynamic verification，formal属于static verification；两者是相互补充的验证手段，各有优缺点，在合适的场景采用合适的验证手段，达到最佳的roi。
在这里插入图片描述
simulation是time-based的，仿真器依据消耗时间的事件推进仿真的进行，激励需要用户施加；simulation虽然可以随机化发送激励，但是对于corner case的遍历需要花费大量时间；simulation适用于大规模的设计，仿真的时间深度可以轻松达到上万个cycle；
formal是state-space based的，依据算法探索所有可能的状态空间，不需要平台搭建和输入激励，便于快速启动验证；formal适用于小模块的验证，随着设计复杂度和cycle深度的增加，formal会占用大量资源，难以收敛；
formal适用于40,000 寄存器以内的模块验证（这个数据已经被刷新）；随着设计复杂度的增加，state space explosion，状态空间激增；一个设计包含n个dff，有2n种配置，m个input有2m种组合；该设计可能的状态达到2(n+m)个；对于一个10 input，10 dff的设计，为220=1,048,576。
回到开头所说的，simulation和formal是相互补充的；模块中的assertion语句既可以在formal中使用，也可以在simulation中使用；formal产生的覆盖率也可以merge到simulation的覆盖率中；设计人员可以通过formal免于平台的搭建，快速地跑通ip中的一些模块，再hand-off给验证人员使用simulation sign-off（shift-left）；simulation中的corner scenario，可以通过bug hunting fpv补充验证；
formal do better
不同的验证策略适合不同的验证场景；emulation适用于整个chip级的验证，加速仿真速度；uvm-simulation适用于复杂寄存器配置的传输packet的ip验证，便于提取transaction和随机化验证；formal（fpv）适合相对较小的模块，便于收敛；formal适合controllable的模块，例如fsms；formal适合observable的模块，便于assertion的书写，如axi bus；串行bus则不适合使用formal。开源项目opentitan中使用fpv的验证模块[2]。
适合formal的常见模块如下：
• arbiter、scheduler
• fifo 、fsms
• interrupt controller、dma controller、memory controller
• power manager unit、clock programing unit
• bus、bus bridge、bus fabric (crossbar noc etc)
• cache，cache-coherent protocols modeling and verification
• data transport
• pinmux, clock controller, reset controller
the growth of formal
formal property verification相关的工具也有十几年历史了，但由于其限制，formal tool并没有被用户广泛使用。但最近这些年，一些因素推动了formal的高速发展：
1. 之前繁多的语言（vera，'e'，摩托罗拉的cbv和英特尔的forspec）整合为systemverilog assertion，并加入ieee 1800协议，成为标准化的assertion languages。工程师在simulation中广泛使用sva，节省了在formal上的学习成本。
2. 随着工艺节点的缩小，流程成本大幅提高；对于corner scenario下可能会隐藏的bug，工程师更倾向fromal这类exhaustive的验证手段。
3. formal可以很好的匹配simulation；同一家eda的formal和simulation工具相互打通，formal产生coverage可以和simulation的coverage相互merge，formal产生的波形可以在simulaiton上复现，formal和simulaiton相同的gui debug工具等。
4. 各类formal apps的推出，使得formal更容易掌握和部署。
5. 随着企业服务器性能的提升和formal算法的发展，可以处理更复杂的设计规模。
6. 一些基于c/c++ model的包含大量运算单元的硬件产品，如ai/ml，gpu的需要爆发，推动了formal data path validation；
7. automotive chip需求激增及其高可靠性的要求，formal提供safety fault analysis的功能；
8. 芯片对security的要求越来越高，需要穷尽分析所有访问路径，适合采用formal；
9. 移动端芯片对于lower power的重视；pmu模块适合formal验证；
10. 采用敏捷开发的芯片团队，对于shift left的追求，采用formal快速进行模块验证及早发现bug;
deepchip
deepchip上一个forma系列的专访，全面的介绍了formal：
• jim hogan on how this is not your father's formal verification[3]
• where formal abv whomps hdl simulation for chip verification[4]
• 9 major and 23 minor formal abv tool metrics - plus their gotchas[5]
• 16 formal apps that make formal easy for us non-formal engineers[6]
• hogan on cadence, mentor, onespin, real intent, synopsys formal[7]
三招辨别净水器是否真的有效
一场有史以来最高规格的全球人工智能盛会即将开启
PCB布局27个小技巧
折叠屏的技术难点在哪里?
魅族最新消息：魅蓝E2将在本月底发布，或将采用全面屏设计！
浅析形式验证的分类、发展、适用场景
TIS的计算公式
如何去看待“5G无用论”
如何使用Y因子方法测量噪声系数(NF)
有图晶圆关键尺寸及套刻量测系统助力半导体产业发展
产品推荐 | 适合多种应用的低成本酒精传感器
图像处理怎么入门？
iOS11Beta2怎么样？苹果系统大改版，iOS11又增25个新特性，iOS11正式版和iPhone8一起来，你期待吗？
pcb表面涂层有什么优势劣势
TI的UCC21520驱动器实现业内最快的5.7k VRMS
中国移动与诺基亚等合作伙伴联合首发5G预商用核心网
如何使用NVIDIA建立纯声波图像
深度解析AP&CP AUTOSAR中的信息安全架构
PC VR及VR一体机的现状和未来总结分析
PI氮化镓的质量与可靠性介绍
formal verification：利用数学分析的方法，通过算法引擎建立模型，对待测设计的状态空间进行穷尽分析的验证。
kinds of formal verification
相比于动态仿真simulation veficiation，形式验证属于static verification，不需要手动灌入激励；通过数学分析的方式，对待测设计进行检查；
在这里插入图片描述
形式验证分为两大分支：equivalence checking 等价检查 和 property checking 属性检查 形式验证初次被eda工具采用，可以追溯到90年代，被应用于rtl code和gate level code的lec等价检查；后来形式验证开始慢慢发展，衍生出适用于不同场景的各类工具；
equivalence checking
combinational equivalence：用于rtl vs netlist的检查，检查寄存器之间的组合逻辑在综合前后是否一致，如formality，conformal。 sequential equivalence: 用于rtl vs rtl的检查，基于cycle的精确度；适用于对原有block级rtl做了非逻辑修改，如clock/power gating，对修改后的rtl进行等价检查。 transaction equivalence：用于c/c++ model vs rtl的检查，基于transaction的精确度；常用于数据通路的算法类设计。
property checking
属性检查基于psl/sva assertion languages，通过对property的assume,cover,assert语句分析，建立golden模型。fpv(formal property verification)需要用户直接书写property；从fpv衍生出各类app，适用于不同场景，可以根据相关配置，自动生成对应的property。
除了上述两类，cdc的检查也属于static verification；例如spyglass会对跨时钟域设计做structural 结构上的检查，检查跨时钟域的信号是否经过同步器处理；一般来讲，formal verification属于static verification;
simulation vs formal
simulation属于dynamic verification，formal属于static verification；两者是相互补充的验证手段，各有优缺点，在合适的场景采用合适的验证手段，达到最佳的roi。
在这里插入图片描述
simulation是time-based的，仿真器依据消耗时间的事件推进仿真的进行，激励需要用户施加；simulation虽然可以随机化发送激励，但是对于corner case的遍历需要花费大量时间；simulation适用于大规模的设计，仿真的时间深度可以轻松达到上万个cycle；
formal是state-space based的，依据算法探索所有可能的状态空间，不需要平台搭建和输入激励，便于快速启动验证；formal适用于小模块的验证，随着设计复杂度和cycle深度的增加，formal会占用大量资源，难以收敛；
formal适用于40,000 寄存器以内的模块验证（这个数据已经被刷新）；随着设计复杂度的增加，state space explosion，状态空间激增；一个设计包含n个dff，有2n种配置，m个input有2m种组合；该设计可能的状态达到2(n+m)个；对于一个10 input，10 dff的设计，为220=1,048,576。
回到开头所说的，simulation和formal是相互补充的；模块中的assertion语句既可以在formal中使用，也可以在simulation中使用；formal产生的覆盖率也可以merge到simulation的覆盖率中；设计人员可以通过formal免于平台的搭建，快速地跑通ip中的一些模块，再hand-off给验证人员使用simulation sign-off（shift-left）；simulation中的corner scenario，可以通过bug hunting fpv补充验证；
formal do better
不同的验证策略适合不同的验证场景；emulation适用于整个chip级的验证，加速仿真速度；uvm-simulation适用于复杂寄存器配置的传输packet的ip验证，便于提取transaction和随机化验证；formal（fpv）适合相对较小的模块，便于收敛；formal适合controllable的模块，例如fsms；formal适合observable的模块，便于assertion的书写，如axi bus；串行bus则不适合使用formal。开源项目opentitan中使用fpv的验证模块[2]。
适合formal的常见模块如下：
• arbiter、scheduler
• fifo 、fsms
• interrupt controller、dma controller、memory controller
• power manager unit、clock programing unit
• bus、bus bridge、bus fabric (crossbar noc etc)
• cache，cache-coherent protocols modeling and verification
• data transport
• pinmux, clock controller, reset controller
the growth of formal
formal property verification相关的工具也有十几年历史了，但由于其限制，formal tool并没有被用户广泛使用。但最近这些年，一些因素推动了formal的高速发展：
1. 之前繁多的语言（vera，'e'，摩托罗拉的cbv和英特尔的forspec）整合为systemverilog assertion，并加入ieee 1800协议，成为标准化的assertion languages。工程师在simulation中广泛使用sva，节省了在formal上的学习成本。
2. 随着工艺节点的缩小，流程成本大幅提高；对于corner scenario下可能会隐藏的bug，工程师更倾向fromal这类exhaustive的验证手段。
3. formal可以很好的匹配simulation；同一家eda的formal和simulation工具相互打通，formal产生coverage可以和simulation的coverage相互merge，formal产生的波形可以在simulaiton上复现，formal和simulaiton相同的gui debug工具等。
4. 各类formal apps的推出，使得formal更容易掌握和部署。
5. 随着企业服务器性能的提升和formal算法的发展，可以处理更复杂的设计规模。
6. 一些基于c/c++ model的包含大量运算单元的硬件产品，如ai/ml，gpu的需要爆发，推动了formal data path validation；
7. automotive chip需求激增及其高可靠性的要求，formal提供safety fault analysis的功能；
8. 芯片对security的要求越来越高，需要穷尽分析所有访问路径，适合采用formal；
9. 移动端芯片对于lower power的重视；pmu模块适合formal验证；
10. 采用敏捷开发的芯片团队，对于shift left的追求，采用formal快速进行模块验证及早发现bug;
deepchip
deepchip上一个forma系列的专访，全面的介绍了formal：
• jim hogan on how this is not your father's formal verification[3]
• where formal abv whomps hdl simulation for chip verification[4]
• 9 major and 23 minor formal abv tool metrics - plus their gotchas[5]
• 16 formal apps that make formal easy for us non-formal engineers[6]
• hogan on cadence, mentor, onespin, real intent, synopsys formal[7]
三招辨别净水器是否真的有效
一场有史以来最高规格的全球人工智能盛会即将开启
PCB布局27个小技巧
折叠屏的技术难点在哪里?
魅族最新消息：魅蓝E2将在本月底发布，或将采用全面屏设计！
浅析形式验证的分类、发展、适用场景
TIS的计算公式
如何去看待“5G无用论”
如何使用Y因子方法测量噪声系数(NF)
有图晶圆关键尺寸及套刻量测系统助力半导体产业发展
产品推荐 | 适合多种应用的低成本酒精传感器
图像处理怎么入门？
iOS11Beta2怎么样？苹果系统大改版，iOS11又增25个新特性，iOS11正式版和iPhone8一起来，你期待吗？
pcb表面涂层有什么优势劣势
TI的UCC21520驱动器实现业内最快的5.7k VRMS
中国移动与诺基亚等合作伙伴联合首发5G预商用核心网
如何使用NVIDIA建立纯声波图像
深度解析AP&CP AUTOSAR中的信息安全架构
PC VR及VR一体机的现状和未来总结分析
PI氮化镓的质量与可靠性介绍