形式验证全面提升安全性，望安为领先数字芯片研发助力

　　随着工艺的高速发展和技术的升级迭代，芯片工业正变得日趋庞大复杂，而这一变化也在深刻地改变着数字芯片的设计。如何在芯片制造成本呈现指数型上升，同时上市时间（Time To Market）争分夺秒的今天，正确而高效地完成数字前端的工程实施， 对于无论是设计和验证团队的管理，还是其中的工程方法学，都提出了艰巨的挑战。
　　在如今的数字芯片前端开发流程中，验证工程师通常需要在整个研发设计周期，与设计工程师一同通力合作达成目标。在主流的基于动态仿真的方法论中，验证工程师在初期就需要对验证框架和环境进行设计和配置，以确保验证能在项目初期就介入设计流程，在项目早期捕捉问题。
　　图1.动态仿真简例
　　作为主流的验证方法，动态仿真手段具有很好的泛用性。但在上图中我们也可以观察到这一方法论的缺点：
　　• 仿真器往往包含多个组件的环境部署，至少包含激励生成器、驱动、DUT、参照模型、监测、检查器
　　• 需要随机激励生成器生成激励，且只能覆盖较有限的情况
　　• 依赖参照模型检验DUT生成的波形是否符合预期
　　在过去的三四十年间，随着形式化验证的技术的成熟，形式方法越来越多地渗透到了越来越多的验证场景中。一个典型的形式验证方法，包含：
　　• SVA形式规约描述：基于SVA的断言文件
　　• DUT：RTL设计代码
　　• 形式检查工具：检查断言和设计的一致性，生成覆盖率和功能验证报告
　　图2.形式化验证简例
　　在上图中我们可以看到，一方面，形式验证在验证架构上做了显著的简化，这大大地提高了验证环境搭建的成本和安全性；另一方面，当验证未通过时，形式化工具提供了很好的反例路径追溯手段。
　　除此之外，形式验证还有一个传统手段无可比拟的优势： 不同于仿真方法中的激励生成+逐次核对的方式，形式验证在理论上可以覆盖全体状态空间，从而从根源上避免了类似奔腾FDIV的高危隐患。
　　事实上，在那次臭名昭著的漏洞事件之后，英特尔也开始重视并极为广泛地引入了形式化团队和工具，为自己的芯片设计验证提供强有力支持。
　　对于现如今对安全性能要求越来越高的数字芯片，这一优势在许多场合无疑是至关重要的。
　　如果你初次接触形式化验证，「遍历状态空间」这一特性可能会令人困惑而着迷。
　　我们来举一个经典的例子，来说明形式化方法是如何实现这一看似不可能的任务的。考虑一个多元布尔函数
　　f:{0,1}ⁿ → {0,1}, (x_1,...x_n) ↦ y
　　我们尝试用一种称为二元决策树（ BDD ,  B inary  D ecision  D iagram）的数据结构来表示它：
　　图片来源：维基百科 二元决策图
　　比如在上图的这个例子中，我们把右侧的用列表形式表示的布尔函数f，用左边的二叉树表示出来。
　　具体方法为：
　　1.定义所有布尔变量的一个偏序：比如这里我们定义x_1>x_2>x_3。表现在图上，x_1出现在第一层作为父节点，x_2出现在第二层，以此类推；
　　2.确定每个叶节点值：每一条到达叶节点的路径，对应函数f的一次取值 —— 当路径从x_i出发后进入其左子树上时，表示参数x_i取值为0，否则为1。叶节点的值即为函数在这条路径对应的（x_i）上的取值。
　　这样，我们就用一个一棵二叉树表示了f。现在我们的想法是使用算法，在保留所有信息的情况下，对这个图进行简化。比如我们可以反复地使用下面的规则：
　　1.如果两个节点是叶节点且具有相同的值，或者是内部节点且具有相同的子节点，则将它们合并；
　　2.如果从内部节点出发且代表1的边和代表0的边指向相同的子节点，则将该节点从图中删除，并将其父节点重定向到子节点。
　　直至这两条规则无法再被应用，我们最终得到了一个称为既约偏序二元决策图（ROBDD,  R educed  O rdered  B inary  D ecision  D iagram）的数据结构。在我们的例子中，最终的ROBDD形如下图：
　　在许多现实情况下，通过ROBDD这一数据结构，大型逻辑电路对应的布尔函数的存储表示得到了简化，从而为RTL综合等流程中的逻辑等价性问题中提供了有力的处理手段。同样的，在功能属性验证问题上，形式方法都采用了各种不同的数据结构和算法，将状态空间进行抽象规约，从而在不丢失信息的情况化简化和解决问题。
　　当然，由于状态爆炸等问题，形式验证方法在实际使用过程中仍有一些技术和工程限制，目前更多地使用在模块级验证上。在当前先进的验证方法学中，形式方法、动态仿真和硬件加速等方法，正在更为积极地产生交融，取长补短，共同为芯片前端验证提供支持。
　　目前，望安科技基于k-framework，正着力研发System Verilog语法检查、功能属性验证、数据流安全等功能的芯片形式化验证APP工具。秉持将领先的形式化技术服务深入服务和支持数字芯片研发的信心，我们欢迎广大芯片和EDA厂商与我们联系沟通，合作共赢，在高速发展的芯片行业中抢占领先身位。
　　浙江望安科技有限公司
　　浙江望安科技有限公司是以＂形式化验证＂为核心技术的安全服务及产品提供商。公司致力于为国家重大项目、关键系统及行业企业提供安全认证保障。业务覆盖航空、航天、国防、轨道交通、区块链、物联网、工业控制、芯片设计制造等重大领域。
　　公司可提供信息技术安全评估标准CC EAL1-EAL7级安全保障级别咨询与技术服务。公司拥有自主研发、自主知识产权的覆盖软件全生命周期的望安形式化验证平台W-AVC、符合CC认证体系的标准化实施平台系统W-CaaS等重要核心资产。核心技术已应用于C919国产大飞机、载人航天工程、中航工业集团、航天科技集团、元心科技、中国移动、小米科技等，已覆盖相对广泛的合作领域和企业。