CN115906731A - 电路的划分方法、等价性验证方法、存储介质 - Google Patents
电路的划分方法、等价性验证方法、存储介质 Download PDFInfo
- Publication number
- CN115906731A CN115906731A CN202211537212.4A CN202211537212A CN115906731A CN 115906731 A CN115906731 A CN 115906731A CN 202211537212 A CN202211537212 A CN 202211537212A CN 115906731 A CN115906731 A CN 115906731A
- Authority
- CN
- China
- Prior art keywords
- circuit
- register
- equivalence verification
- verification
- local
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Pending
Links
Images
Classifications
-
- Y—GENERAL TAGGING OF NEW TECHNOLOGICAL DEVELOPMENTS; GENERAL TAGGING OF CROSS-SECTIONAL TECHNOLOGIES SPANNING OVER SEVERAL SECTIONS OF THE IPC; TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
- Y02—TECHNOLOGIES OR APPLICATIONS FOR MITIGATION OR ADAPTATION AGAINST CLIMATE CHANGE
- Y02D—CLIMATE CHANGE MITIGATION TECHNOLOGIES IN INFORMATION AND COMMUNICATION TECHNOLOGIES [ICT], I.E. INFORMATION AND COMMUNICATION TECHNOLOGIES AIMING AT THE REDUCTION OF THEIR OWN ENERGY USE
- Y02D10/00—Energy efficient computing, e.g. low power processors, power management or thermal management
Landscapes
- Tests Of Electronic Circuits (AREA)
Abstract
本发明公开了一种电路的划分方法、等价性验证方法、存储介质。其中电路的划分方法，包括：先对参考电路与实现电路的组合逻辑进行等价性验证，得到匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器；将得到的匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器作为分割可能节点，查找各分割可能节点的所有锥顶；当任意两个分割可能节点具有相同的锥顶，则划分为一组；以组为单位对所述参考电路及其对应的实现电路进行划分，将一组内的寄存器以及对应的组合电路划分为局部电路。本发明可以简化大规模网表电路等价性验证的复杂度，使得大规模网表电路等价性验证的效率提升。
Description
技术领域
本发明涉及时序电路的等价性验证的技术领域，尤其涉及一种电路的划分方法，即识别并分割局部时序等价电路的方法。
背景技术
等价性验证是形式化验证的一种，是指从数学上完备地证明或验证电路的实现方案是否实现了电路设计所描述的功能。等价性验证多用于底层电路之间的功能一致性验证，例如综合前后RTL级与门级网表之间的验证等。随着集成电路规模的快速增长使得验证的难度越来越大，传统的模拟和仿真的方法暴露出耗时长，验证覆盖率低等缺点。相比于传统方法，等价性验证采用的数学上的方法，将实现电路和参考电路直接进行比较，不需要开发测试向量，可以大量缩短验证时间，且验证覆盖率可达到100％。
传统的组合电路功能等价性验证是通过构造两个电路的规范表示形式，如真值表或二叉判定图bdds，当且仅当它们的规范形式同构时，这两个电路功能等价。为了验证两个时序电路的等价性，通常需要把它们当成有限状态机，并构造这两者的积自动机。brand将这种计算模型称为miter。它是通过把两个状态机相应的每—对原始输入联接到一起，同时把相应的每一对原始输出联接到一个异或门，而这些异或门就构成了积自动机的输出。如果对于每一个输入序列，积自动机的每个原始输出恒为0，那么这两个时序电路就是等价的。换句话说，就是对于任何输入向量和可达状态，积自动机的原始输出响应总是为0。通常，证明状态机等价性的第一步是从初始状态开始，计算所有可达状态。这就是典型的基于有限状态机遍历算法。
因此，要验证两个组合电路等价，可以通过构造它们输出的miter电路(共用输入信号，输出用异或门相连)，然后利用SAT solver(可满足性问题求解器)对miter电路进行结算，如果SAT solver找不出一组输入使得miter电路的输出为1，则证明这两个电路等价。对于时序电路，需要将电路沿着寄存器切分成多个组合逻辑块，并将分割后的组合逻辑块一一映射起来并创建miter电路，然后使用SAT solver进行求解。
但是，由于综合工具的优化策略，综合后的门级网表有可能与其RTL级网表在组合逻辑等价性验证时有一些匹配点是不等价的，但是对这两个网表进行时序等价性验证时则是等价的。然而对两个完整的网表做时序等价性验证的要求比较高，需要网表的规模必须足够小。当网表的规模比较大的时候，要完成时序等价性验证所需要的时间会让人难以接受。
因此，如何提供一种电路的划分方法，将规模较大的网表切割成局部电路是一个待解决的技术问题。
发明内容
为了解决现有技术中规模较大的网表完成时序等价性验证所需的时间难以让人接受的技术问题，本发明提出了电路的划分方法、等价性验证方法、存储介质。
本发明提出的电路的划分方法，包括：
先对参考电路与实现电路的组合逻辑进行等价性验证，得到匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器；
将得到的匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器作为分割可能节点，查找各分割可能节点的所有锥顶；
当任意两个分割可能节点具有相同的锥顶，则划分为一组；
以组为单位对所述参考电路及其对应的实现电路进行划分，将一组内的寄存器以及对应的组合电路划分为局部电路。
进一步，所述实现电路是时序优化后的电路。
进一步，所述锥顶为负载方向下寄存器的D端，和/或顶层模块的主输出。
本发明提出的电路的等价性验证方法，采用上述技术方案所述的电路的划分方法对参考电路及其对应的实现电路进行划分，得到参考电路的局部电路，以及实现电路的局部电路；
判断参考电路及其对应的实现电路的局部电路的输入输出是否相等并相互匹配，若是，则将参考电路的局部电路与实现电路对应的局部电路进行等价性验证；否则，指定参考电路及其对应的实现电路的局部电路的输入输出，使参考电路及其对应的实现电路的局部电路的输入输出相等并相互匹配后，再进行等价性验证。
本发明提出的计算机可读存储介质，用于存储计算机程序，所述计算机程序运行时执行上述技术方案所述的电路的划分方法。
本发明使得电路在有了组合等价性验证的结果之后，正确地识别并分割潜在的局部时序等价电路，并对分割后的局部电路进行时序等价性验证。本发明解决了综合工具对电路做了局部的时序优化的情况下，RTL级电路和门级电路组合等价性验证不通过，而全局做时序等价性验证复杂度太高的问题。本发明在RTL级电路和门级电路的形式验证中的应用将大大减少验证时间。
附图说明
下面结合实施例和附图对本发明进行详细说明，其中：
图1是本发明一实施例的流程图。
具体实施方式
为了使本发明所要解决的技术问题、技术方案及有益效果更加清楚明白，以下结合附图及实施例，对本发明进行进一步详细说明。应当理解，此处所描述的具体实施例仅用以解释本发明，并不用于限定本发明。
由此，本说明书中所指出的一个特征将用于说明本发明的一个实施方式的其中一个特征，而不是暗示本发明的每个实施方式必须具有所说明的特征。此外，应当注意的是本说明书描述了许多特征。尽管某些特征可以组合在一起以示出可能的系统设计，但是这些特征也可用于其他的未明确说明的组合。由此，除非另有说明，所说明的组合并非旨在限制。
参考电路是指等价性验证中作为参考标准的电路，实现电路需要被证明为跟参考电路等价。参考电路通常为RTL级别的verilog代码，实现电路通常为经过综合后的门级电路。此发明所指的等价性验证是指两个时序电路的等价性验证，即参考电路及实现电路。时序电路包含有寄存器和相关的组合逻辑电路。等价性验证分为组合逻辑等价性验证和时序等价性验证。组合逻辑等价性验证是指对两个只包含组合逻辑的电路进行等价性验证。时序等价性验证是指对两个包含时序逻辑即寄存器和相关组合逻辑的电路进行等价性验证。所以组合逻辑不包含寄存器。组合逻辑等价性验证实质上是将两个时序电路的寄存器进行一一匹配，然后切割出驱动这一对寄存器的一对组合逻辑电路，最后对这一对组合逻辑电路进行组合逻辑等价性验证。
如图1所示，本发明提出的电路的划分方法，主要包括以下步骤。
对参考电路及其实现电路的组合逻辑进行等价性验证，得到匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器。即，先对寄存器进行匹配，得到匹配失败的寄存器，之后将匹配成功的寄存器对应的组合逻辑进行等价性验证，得到组合逻辑等价性验证不通过的寄存器。匹配失败的寄存器不会进行组合逻辑等价性验证，因为没有对应的寄存器及驱动该寄存器的组合逻辑电路跟它比较。
将得到的匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器作为分割可能节点，查找各分割可能节点的所有锥顶；
当任意两个分割可能节点具有相同的锥顶，则划分为一组；
以组为单位对所述参考电路及其对应的实现电路进行划分，将一组内的寄存器以及对应的组合电路划分为局部电路。
在一个实施例中，查找锥顶的流程包含了以下步骤。
先收集组合逻辑等价性验证失败的寄存器和匹配失败的寄存器，以下将这些寄存器称之为分割可能节点。
从这些分割可能节点的输出端的方向出发进行深度优先遍历，即从一个门的输入端到这个门的输出端这个方向，遍历到顶层模块的输出端口或者在第一轮的组合逻辑等价性验证中验证通过的寄存器的D端则停止遍历，记录下遍历到的寄存器作为锥顶，即顶层模块的输出。
例如，经过上述查找锥顶的步骤，得到寄存器A的锥顶有寄存器2，寄存器B的锥顶有寄存器2、寄存器3，寄存器C的锥顶有寄存器3，那么寄存器A、寄存器B、寄存器C都被分到同一组。因首先寄存器A和寄存器B有共通的锥顶——寄存器2，所以它们先被分为同一组。此时组内有两个寄存器，这两个寄存器的锥顶的并集构成分组的锥顶，即如果寄存器A的锥顶为2的话，此时寄存器A所在的分组的锥顶为2、3。需要被分组的寄存器的锥顶集合如果与某一分组的锥顶集合相交的话，则将该寄存器划入该分组，然后该分组的锥顶集合为该分组内所有寄存器的锥顶集合的并集。
在一个实施例中，可以对实现电路进行时序优化，然后将时序优化后的实现电路与参考电路的组合逻辑进行等价性验证，得到匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器。
在一个实施例中，锥顶可以是负载方向下寄存器的D端，和/或顶层模块的主输出。
负载方向即从一个门的输入端到这个门的输出端这个方向。顶层模块是指层次结构处于最顶层的模块。电路设计中通过是由一个顶层模块然后该模块内部有若干子模块构成的。
本发明的电路的等价性验证方法，采用上述电路的划分方法对参考电路及其对应的实现电路进行划分，得到参考电路的局部电路，以及实现电路的局部电路，判断参考电路的局部电路与实现电路对应的局部电路的输入输出是否相等且相互匹配，若输入输出数量相等且相互匹配，将参考电路的局部电路与实现电路对应的局部电路进行等价性验证。否则，通过人工等方式来指定不匹配的局部电路的输入输出，使得考电路的局部电路与实现电路对应的局部电路可以满足等价性验证的输入输出条件。
分割后的局部电路的输入输出不一定数量相等且相互匹配，只有输入输出数量相等及相互匹配的局部电路才能做时序等价性验证。一般如果实现电路的时序优化导致不匹配的寄存器占比比较多的时候，会有切割后的局部电路输入输出数量不等或不互相匹配的情况，此时需要人工介入来指定局部电路的输入和输出从而根据指定的输入输出来切割局部电路并进行时序等价性验证。
通过本发明的电路的划分方法，可以将规模较大的网表电路划分为局部电路，从而降低验证的复杂度，减少电路的验证时间，提升电路的验证效率。
本发明还保护计算机可读存储介质，该计算机可读存储介质用于存储计算机程序，该计算机程序运行时执行本发明上述技术方案的电路的划分方法。
以上所述仅为本发明的较佳实施例而已，并不用以限制本发明，凡在本发明的精神和原则之内所作的任何修改、等同替换和改进等，均应包含在本发明的保护范围之内。
Claims (7)
1.一种电路的划分方法，其特征在于，包括：
先对参考电路与实现电路的组合逻辑进行等价性验证，得到匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器；
将得到的匹配失败的寄存器和/或组合逻辑等价性验证不通过的寄存器作为分割可能节点，查找各分割可能节点的所有锥顶；
当任意两个分割可能节点具有相同的锥顶，则划分为一组；
以组为单位对所述参考电路及其对应的实现电路进行划分，将一组内的寄存器以及对应的组合电路划分为局部电路。
2.如权利要求1所述的电路的划分方法，其特征在于，所述实现电路是时序优化后的电路。
3.如权利要求1所述的电路的划分方法，其特征在于，所述锥顶为负载方向下寄存器的D
端，和/或顶层模块的主输出。
4.如权利要求1所述的电路的划分方法，其特征在于，任意一组的锥顶为该组内所有分割可能节点的锥顶的并集。
5.如权利要求1所述的电路的划分方法，其特征在于，所述查找各分割可能节点的所有锥顶包括：
从各分割可能节点的输出端的方向出发进行遍历，遍历到顶层模块的输出端口或者在第一轮的组合逻辑等价性验证中验证通过的寄存器的D端则停止遍历，记录下遍历到的寄存器作为锥顶。
6.一种电路的等价性验证方法，其特征在于，采用权利要求1至5任意一项所述的电路的划分方法对参考电路及其对应的实现电路进行划分，得到参考电路的局部电路，以及实现电路的局部电路；
判断参考电路及其对应的实现电路的局部电路的输入输出是否相等并相互匹配，若是，则将参考电路的局部电路与实现电路对应的局部电路进行等价性验证；否则，指定参考电路及其对应的实现电路的局部电路的输入输出，使参考电路及其对应的实现电路的局部电路的输入输出相等并相互匹配后，再进行等价性验证。
7.一种计算机可读存储介质，用于存储计算机程序，其特征在于，所述计算机程序运行时执行如权利要求1至5任意一项所述的电路的划分方法。
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202211537212.4A CN115906731A (zh) | 2022-12-01 | 2022-12-01 | 电路的划分方法、等价性验证方法、存储介质 |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202211537212.4A CN115906731A (zh) | 2022-12-01 | 2022-12-01 | 电路的划分方法、等价性验证方法、存储介质 |
Publications (1)
| Publication Number | Publication Date |
|---|---|
| CN115906731A true CN115906731A (zh) | 2023-04-04 |
Family
ID=86479297
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN202211537212.4A Pending CN115906731A (zh) | 2022-12-01 | 2022-12-01 | 电路的划分方法、等价性验证方法、存储介质 |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN115906731A (zh) |
-
2022
- 2022-12-01 CN CN202211537212.4A patent/CN115906731A/zh active Pending
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Huang et al. | Formal equivalence checking and design debugging | |
| CN114742001B (zh) | 一种基于多fpga的系统静态时序分析方法 | |
| JP2000148808A (ja) | スケジュ―リングされた動作記述に対するストラクチュラルｒｔｌの正当性検証方法 | |
| US8719752B1 (en) | Hierarchical crosstalk noise analysis model generation | |
| Huang et al. | Match and replace: A functional ECO engine for multierror circuit rectification | |
| US11455451B2 (en) | Verifying a hardware design for a component that implements a permutation respecting function | |
| US5491639A (en) | Procedure for verifying data-processing systems | |
| US8762907B2 (en) | Hierarchical equivalence checking and efficient handling of equivalence checks when engineering change orders are in an unsharable register transfer level | |
| JP3851357B2 (ja) | トランジスタ回路のタイミング特性抽出方法、タイミング特性ライブラリを記憶した記憶媒体、ｌｓｉの設計方法、及びゲート抽出方法 | |
| Anastasakis et al. | A practical and efficient method for compare-point matching | |
| US6993740B1 (en) | Methods and arrangements for automatically interconnecting cores in systems-on-chip | |
| JP2000207440A (ja) | 半導体集積回路の設計検証装置、方法及び記憶媒体 | |
| US20030221173A1 (en) | Method and apparatus for detecting connectivity conditions in a netlist database | |
| US7380228B2 (en) | Method of associating timing violations with critical structures in an integrated circuit design | |
| CN111797588B (zh) | 一种形式验证比较点匹配方法、系统、处理器及存储器 | |
| Chen et al. | Logic restructuring using node addition and removal | |
| CN115906731A (zh) | 电路的划分方法、等价性验证方法、存储介质 | |
| Pan et al. | A Semi-Tensor Product based Circuit Simulation for SAT-sweeping | |
| CN116976248A (zh) | 使用冗余节点的电路设计调整 | |
| US11087059B2 (en) | Clock domain crossing verification of integrated circuit design using parameter inference | |
| CN113919256A (zh) | 一种布尔可满足性验证方法、系统、cnf生成方法及存储装置 | |
| US11341310B1 (en) | Layout-versus-schematic (LVS) debugging and error diagnosis via type of graph matching | |
| US20230177244A1 (en) | Creation of reduced formal model for scalable system-on-chip (soc) level connectivity verification | |
| Srinath | Rectification of Integer Arithmetic Circuits | |
| US20230016865A1 (en) | Diagnosis of inconsistent constraints in a power intent for an integrated circuit design |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination |