形式验证中的光计算

集成电路设计中的形式验证

  当代科技中的集成电路设计，既精密又复杂，在芯片设计流程中，电子设计自动化(Electronic Design Automation, EDA)软件至关重要，其中芯片设计验证过程是非常重要的过程，芯片验证是对芯片设计是否正确与安全进行检查，占芯片设计近1/2的成本和时间。形式验证通过使用形式证明的方式来验证设计的功能是否正确，是保证芯片正确性与安全性的非常重要的手段，已经成为EDA软件关键模块。

  芯片验证的一大优势是它可以在设计早期就进行，无需实际制造芯片或进行物理测试。这使得设计者能够在芯片投入制造前发现和解决问题，从而节省时间和成本。此外，芯片验证还可以帮助设计者发现那些难以通过传统仿真方法检测到的错误，提高设计的可靠性。

  然而，形式验证也面临一些挑战。对于复杂的电路设计，形式验证需要大量的计算资源和时间，近年来，集成电路规模不断提高，芯片中使用的晶体管数量不断加大，如Apple的双芯片M1 Ultra片上系统，共集成1140亿个晶体管，英伟达最新的H100芯片，共有800亿个晶体管，这些都对形式验证的算力和计算时间提出新的挑战。形式验证方法包括等价性验证(Equivalence Checking)和基于断言的形式验证(Formal Assertion-based Verification)。主要两种方式求解:

l基于二元决策图(Binary Decision Diagrams, BDD)

l命题逻辑可满足性(PropositionalSatisfiability,SAT)求解

SAT 问题

  可满足性问题（SAT问题）是一种重要的计算机科学问题，它涉及确定一个布尔逻辑公式是否存在满足其变量的赋值。该问题的背景可以追溯到20世纪60年代，当时研究者开始关注用计算机来解决布尔逻辑问题。SAT问题在理论计算机科学中被广泛研究，它被用于硬件和软件验证、自动定理证明、人工智能和优化等领域。在芯片设计中，可以使用SAT求解器来验证电路是否满足给定的规范。在软件开发中，SAT问题可以帮助找到程序的错误或优化代码。通过将问题转化为SAT问题，可以利用现有的高效算法和工具进行求解。SAT问题的研究不仅推动了计算机科学的发展，还在多个领域的实际应用中发挥了重要作用。

  首先在SAT问题中，我们一般给定：

•   变量集合，是一组有n个变量variable的集合 {x1, x2, ⋯ , }，以及每一个变量相关联的2个文字（literal）组成的集合` {x1, ¬x1, x2, ¬x2, ⋯ , x , ¬x }`（其中，对于变量 而言，文字是正文字，文字¬ 是负文字）。

•  子句（clause）则是由文字集合中的部分若干文字的析取（disjunction）所构成的；即每个子句都可以写成`x1 ∨ x2 ∨ x3⋯`的形式，也就是各个变量的或操作集合（or）。

•  合取范式，我们通过将m个子句 c1 c2 c3... cn 用与（and）的形式进行合取，这样我们就很容易的构成了一个合取范式（Conjunctive Normal Form，CNF）形式的命题公式。` F = c1 ∧ c2 ∧ ⋯ cm`

•  一个命题逻辑公式可以看成由一个变量集合和一个子句集合构成的二元组。

  显而易见，公式中的任意一个子句都处于下列两种状态之一：

（1） 满足（satisfied）状态  ；（2）未满足（unsatisfied）状态。

  一个子句处于满足状态当且仅当该子句中至少有一个文字在真值指派下是真的(如果一个子句是满足状态的，那么在初始赋值时它其中的一个变量一定为真,因为子句中的变量是or操作相联的)。SAT问题也就是研究，如果给定了一个CNF合取范式的命题 F，SAT问题也就是判断是否存在一个完整的赋值方案 ，这个赋值方案能使得F中的所有子句都能被满足（也就是所有子句都为真）。

  目前，SAT 问题的求解算法大致可以分为两类：完备性算法和非完备性算法。

•  完备性算法，由于其完备性的搜索技术，能判定一个SAT实例是可满足的还是不可满足的，但有可能不能在合理的时间对SAT实例进行判定。

•  非完备性算法，通常指局部搜索算法，仅能判定一个SAT 实例是可满足的，但其能非常高效地对可满足的 SAT 实例进行判定。

形式验证中的SAT

  假设我们有一个电路设计，其中包含多个逻辑门和连线。我们想要验证这个设计是否满足一些特定的属性，比如安全性、正确性或性能要求。为了进行形式验证，我们可以将该问题转化为一个SAT（可满足性问题）。

  首先，我们定义一个布尔逻辑公式，描述该电路设计的行为规范。这个公式包含输入变量、输出变量和逻辑门之间的关系。例如，我们可以使用布尔表达式来表示电路的输出应该在特定输入条件下取特定的值。

  其次，我们将这个布尔逻辑公式转化为一个SAT问题。SAT问题是一个判断是否存在一组变量赋值使得给定的布尔公式为真的问题。我们可以将电路的输入变量视为SAT问题的变量，并将电路的行为规范转化为一个逻辑公式，作为SAT问题的输入。

  最后，我们使用SAT求解器来求解这个SAT问题。SAT求解器会尝试找到一组变量赋值，使得布尔公式成立。如果SAT求解器找到了满足公式的变量赋值，那么意味着我们的电路设计满足了给定的行为规范。如果SAT求解器未能找到满足条件的变量赋值，那么我们可以从求解器返回的结果中获取一组不满足公式的赋值。这些赋值可以帮助我们识别设计中存在的问题，并进行进一步的调试和修复。

光计算求解SAT算法

   光计算求解算法主要是求解形式验证转换后的SAT问题。

1. 前处理过程

  对于一个n个变量，m个子句的SAT问题，可以使用一个n x m的矩阵M来表示，矩阵M的每一行代表一个子句中每个变量的位置以及对应的符号，同时我们使用一个长度为m的向量L来记录每个子句长度。此时，我们设定模型的阈值为T=1-L，此时我们可以计算模型的初始能量的向量表示：G=sign(M×S-T)，其中S为状态向量（Si=±1）。这样设计能量的好处在于对于满足的子句，其对应的能量值为1，否则为0。

2. 光计算异步算法

现在已知根据能量向量G可以得到在当前赋值下的每个子句的满足情况（判断1或0），这可以帮助我们快速找到未满足的子句并进行更新，从而获得比伊辛算法更快的收敛速度。这套基于光计算的异步算法具体迭代步骤如下：

    1.   随机初始化一个状态向量S
    2.   计算能量向量G=sign(M×S-T) 多次取平均（可应用光计算加速）
    3.   记录最低能量G和对应的状态向量S
    4.   从未满足的子句集合中随机挑选一个子句C
    5.   计算子句C中每个变量σ_k翻转后的能量G_k+ Noise（可应用光计算加速）
    6.   挑选出能量下降最大时对应的变量，更新状态向量S
    7.   如果最佳满足子句数目小于m且未达到最大迭代次数，则回第2步；否则程序结束，给出找到的最佳状态向量S以及对应的最大满足子句数目。
    * 第5步可以利用光计算芯片自有的噪声来帮助算法跳出局部最优解。

应用案例

曦智科技携手芯华章 联合推进“光芯片+EDA”战略性技术研发

  近日，全球光电混合计算领军企业曦智科技宣布，联手系统级验证EDA解决方案提供商芯华章科技，布局面向未来的“光芯片+EDA”战略性技术研发。双方将基于光芯片的异构加速能力，开展赋能EDA领域异构计算加速的联合研究，并打造软硬件一体化的光电混合“交钥匙”解决方案，以满足大数据、人工智能等应用领域日益增长的数据处理与运算需求。

  传统电子芯片的性能提速和传输数据的方式，已逐渐无法满足日益增长的数据处理与节能要求。光子芯片凭借高通量、低延时、低功耗等特点，可以有效提升电子集成器件的速度和带宽，因此光电混合计算就成为了突破现有IC设计瓶颈的有效途径之一。

  芯华章科技首席市场战略官、芯华章研究院执行副院长谢仲辉表示，“光子芯片是一个快速增长的市场，将为众多行业带来巨大改变，并为未来数字化发展创造令人兴奋的新机会。基于曦智先进的光计算和光网络技术，我们将充分利用光电混合计算的潜力，开启EDA验证算力加速的新纪元，进一步提升芯华章系统级验证工具的运算效率，并通过与曦智的深入合作积极布局光芯片验证领域，加速光子芯片开发，为数字经济高质量发展提供坚强后盾。”