高工课堂 集成电路形式验证两大技术原则

在计算机硬件集成电路和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。在本文中，专业的工程师将会为我们展现形式验证的两个重要原则，一起来看看这两个在软件系统设计过程中常常用到的技术原则都有哪些具体内容吧。

形式验证的类型很多，且都十分有用

形式验证包括一系列技术，如等效性检验和模型校验。模型检验器（MC）可以根据它的应用，复杂性和效益不同而进一步分类，其中端对端形式验证是最重要的。

自动形式被构建到许多lint工具中来检测简单的设计问题，如违规编译或无作用程序代码。正规的应用程序被用于解决验证空间中的特定问题，如低功耗，连接检查，或跨时钟域。基于断言的验证（ABV）使用户能够编写对设计具有针对性的断言，验证简单的寄存器传输级（RTL）功能。端对端形式被用来验证被验设计模块（DUT）的完整功能，使用端对端形式检验器替代这层次的模拟结构。

各种类型的形式化技术在验证过程中都是有用的。为了实现形式符号指令，即形式是验证DUT的唯一验证手段，端对端形式是必备的。

在验证流程中，形式验证是必备的

无论是什么形式类型，如果一个验证流程不包含形式化技术，那么它就是不完整的。在系统级芯片（SoC）设计中，单独使用模拟会留下大量的系统漏洞。形式化技术的好处很多，包括依靠其全面性涵盖所有的输入脚本，以发现极端情况错误的能力。

由于后晶片错误，Oski Technology经常被要求做形式验证服务项目。一个更好的策略应该是从项目开始的时候便部署形式，以尽早发现错误，来减少验证周期，最终，能够减少整个项目的周期。

通常情况下，采用形式化技术的障碍在于公司缺乏形式资源，能够以一种有意义的方式进行部署。与模拟相比，形式需要不同的思维。因此，工程管理人员不能指望一个模拟工程师从一开始就采用并运行形式。最好的策略是向专家学习，从内部打造自己的强大团队。一旦形式被部署，验证工程师会意识到这对验证流程来说是必须的。

结语

工程师在进行计算机集成硬件设计的过程中，可以参考上述两大原则，进行形式验证并减少试验周期。这对于新产品型号的研发和推广都具有较大的辅助作用。