形式验证如何加速超大规模芯片设计？
引言
随着集成电路规模的不断扩大，从设计到流片（Tape-out）的全流程中，验证环节的核心地位日益凸显。有效的验证不仅是设计完美的基石，更是确保电路在实际应用中稳定运行的保障。尤为关键的是，逻辑或功能错误是导致流片失败的首要原因，占比高达50%。功能验证正是解决这一难题的利器，它助力工程师精准识别逻辑设计漏洞、性能不达标问题以及设计代码中的功能缺陷，从而最大限度地规避流片风险。针对超大规模集成电路（VLSI）设计，目前功能验证有两种方法：动态仿真验证和形式验证（Formal Verification）。形式验证采用数学方法来比较原设计和修改设计之间的逻辑功能的异同，而动态仿真验证是对两设计施加相同的激励后，观测电路对激励的反应异同。面对大型设计，传统的动态仿真验证方法在覆盖率和效率上面临挑战。为了达到100%的覆盖率，动态仿真验证所需要的矢量就会越多，这时形式验证在这方面就有优势了，成为现代IC设计验证流程中的关键一环。本文就以 “芯天成EsseFCEC”工具为例，来介绍形式验证的流程和基本概念。
什么是形式验证
形式验证是一种基于严格数学推理的设计验证技术，它摒弃了物理测试与模拟的依赖，专注于通过静态、全面的逻辑分析来确保设计的正确性。此方法显著降低了对庞大测试集的需求，并力求实现接近完美的验证覆盖率。形式验证作为EDA、数学及编程语言等多学科交叉的产物，自上世纪90年代起便崭露头角，最初应用于RTL代码与门级网表的LEC（逻辑等价性检查），随后逐步扩展到各类EDA工具，以应对不同验证场景的需求。目前，形式验证主要分为两个技术方向：等价性检查和属性检查。其中。等价性检查，作为核心验证手段，通过对比功能验证后的HDL设计与综合后的网表功能，确保两者在功能层面上的完全一致，从而保证门级电路与寄存器传输级（Register Transfer Level, RTL）模型之间的一致性。这一方法有效防范了综合工具潜在的缺陷及人为误操作，对于提升设计质量至关重要。
形式验证的实施涉及多个关键环节：属性定义（Properties）：精确阐述设计需遵循的特性与规范，涵盖时序逻辑、状态转换规则及各项约束条件。规约语言：采用如SystemVerilog Assertions（SVA）、Property Specification Language（PSL）等形式化规约语言，将属性与约束转化为可验证的表达式。定理证明器（Theorem Provers）：依托形式化逻辑与推理机制，自动验证属性是否成立，为设计逻辑的正确性提供坚实保障。模型检查器（Model Checkers）：全面探索系统状态空间，寻找可能违反预定性质的执行路径，确保设计在所有可能情况下均能满足既定要求。形式验证的基本流程是一个连贯且系统化的过程。这一过程从明确验证目标开始，设计团队首先需要界定哪些部分或功能需要接受形式验证的严格审查。接着，采用形式规约语言（如SystemVerilog Assertions、PSL）定义属性和规约，作为验证基础。进入验证环境配置阶段，团队选择适合的验证工具（定理证明器、模型检查器），并依据设计特性和需求进行优化配置，以确保验证效率与准确性。验证执行为核心，定理证明器通过数学推理验证属性与规约的正确性，模型检查器则全面探索系统状态空间，检查违规执行序列。验证结束后，团队分析验证结果，识别并修正设计中的错误或不一致。此过程可能多次迭代，直至设计完全符合验证要求。
形式验证工具的挑战
形式验证的流程虽然复杂且严谨，但它为设计团队提供了一种高效且可靠的验证方法。通过遵循这一流程，设计团队可以显著降低设计错误的风险，提高产品的质量和可靠性。然而，随着现代芯片设计的复杂性和规模不断增长，形式验证在实际应用中面临多重挑战：复杂性增加，性能不足：现代芯片设计的复杂性和规模不断增长，对验证工具的性能提出了更高要求。现有工具在处理大规模设计时可能面临性能瓶颈，导致验证过程耗时过长。多样化的设计环境：不同的设计团队可能使用不同的设计语言和平台，这要求验证工具具备广泛的兼容性和集成能力。然而，多样化的设计环境可能导致兼容性和集成性方面的挑战。可扩展性需求增加：随着技术的不断进步和新的设计需求的出现，验证工具需要具备良好的可扩展性，以快速适应新的设计规范和标准。这对工具的开发和维护提出了更高要求。复杂的设计错误检测：在复杂的设计中，子系统之间的交互和逻辑路径可能非常复杂，验证工具需要能够准确地检测这些复杂场景中的错误和不一致之处。这要求工具具备强大的错误检测能力和智能化的分析手段。
芯天成EsseFormal形式验证软件
芯天成EsseFormal形式验证软件是一款功能全面的验证解决方案，专为数字芯片设计领域的复杂验证挑战而设计。其核心包含五种工具套件，每一种都针对特定的验证需求提供高效、精准的支持。EsseFECT（形式化等价性验证）：该工具专注于验证C-to-RTL的转换过程中，设计的等价性是否得以保持。这确保了设计在不同抽象层次间的转换无误，是确保设计一致性的重要环节。EsseFCEC（组合逻辑等价性验证）：作为EsseFormal的明星产品，EsseFCEC专门用于验证芯片设计中各电路模块之间的组合逻辑等价性。它不仅支持RTL到Netlist的转换验证，还涵盖版本间差异的比较，确保设计更改不会引入错误。其强大的综合优化技术支持（如Clock-gating、multibit register banking和FSM recoding）显著提升了验证效率和性能。此外，对DesignWare元件库的支持以及大位宽datapath验证的能力，进一步拓宽了EsseFCEC的应用范围。
EsseFPV（模型检查）：通过遍历设计的状态空间，EsseFPV能够发现设计中可能存在的违反预定义属性的行为，是确保设计行为符合预期的关键工具。EsseCC与EsseUNR（实用验证Apps）：这两个工具提供了额外的实用功能。EsseCC是一个高效的连接性检查验证工具，为用户提供快速的错误检测以及信号到信号的预期设计行为验证。EsseCC以RTL电路和连接规范作为输入，快速检查设计是否符合连接规范。而EsseUNR是一款高效的覆盖不可达性检查工具。使用传统的验证方式，在验证后期，通过编写测试用例提升验证覆盖率的难度陡然上升。该工具具有更高效、更准确、更易上手的优点，可对未覆盖的代码进行全面的不可达性检查。
芯天成EsseFormal的定制化和集成化特点，使得它能够精准匹配不同用户的特定需求，从而显著降低验证时间，提高验证的完整性和准确性。其简洁易用的图形用户界面，让验证过程更加直观和高效，即使是初次接触形式验证的用户也能快速上手。
验证发展方向：覆盖率的提升
在当前的硬件设计领域中，随着设计复杂度的急剧增加，验证已成为确保芯片功能和性能可靠性的关键环节。验证技术的发展方向，尤其是覆盖率的提升，成为了行业关注的焦点。思尔芯的软件仿真芯神驰PegaSim通过其创新性的解决方案，与国微芯的形式验证工具进行无缝集成，为提升验证的全面性和效率树立了新的标杆。覆盖率是衡量验证完整性的重要指标，它反映了验证过程中测试向量对设计代码覆盖的广度和深度。然而，在复杂的硬件设计中，往往存在难以触及的代码区域，即所谓的“不可达部分”。这些区域若未经充分验证，就可能成为潜在的设计漏洞。因此，提升覆盖率，特别是针对不可达部分的验证，对于确保设计质量和可靠性至关重要。思尔芯的软件仿真PegaSim通过与国微芯的形式验证工具相结合，实现了对覆盖率中不可达部分进行深入验证。这一解决方案不仅增强了软件仿真过程中的代码覆盖率，还通过增加激励或优化代码的方式，进一步提高了验证的全面性和准确性。同时，PegaSim还支持对指定模块或特定代码行进行精细化的覆盖不可达性检查，帮助设计团队精准定位并消除无意义或冗余的代码，从而优化内在逻辑，提升整体设计质量。面对日益复杂的硬件设计，单一的验证方法已难以满足全面验证的需求。因此，验证技术的发展趋势是多种验证方法的融合与互补。软件仿真、硬件仿真、原型验证、以及形式验证等方法各有千秋，它们在不同的验证阶段和侧重点上发挥着不可替代的作用。通过综合运用这些验证方法，可以实现对硬件设计的全方位、多角度检验，从而确保设计的正确性和可靠性。
关于思尔芯 S2C
思尔芯（S2C）自 2004 年设立上海总部以来始终专注于集成电路 EDA 领域。作为国内首家数字 EDA 供应商，公司业务已覆盖架构设计、软件仿真、硬件仿真、原型验证、数字调试、EDA 云等工具及服务。已与超过 600 家国内外企业建立了良好的合作关系，服务于人工智能、高性能计算、图像处理、数据存储、信号处理等数字电路设计功能的实现，广泛应用于物联网、云计算、5G 通信、智慧医疗、汽车电子等终端领域。
公司总部位于上海，并建立了全球化的技术研发与市场服务网络，在北京、深圳、西安、香港、东京、首尔及圣何塞等地均设有分支机构或办事处。
思尔芯在 EDA 领域的技术实力受到了业界的广泛认可，通过多年耕耘，已在数字前端 EDA 领域构筑了技术与市场的双优势地位。并参与了我国 EDA 团体标准的制定，承担了多项国家及地方重大科研项目，获国家级专精特新“小巨人”企业、国家工业软件优秀产品、上海市级企业技术中心等多项荣誉资质。
