[go: up one dir, main page]

WO2022000576A1 - Procédé et système de mise en correspondance de points de comparaison de vérification formelle, processeur et mémoire - Google Patents

Procédé et système de mise en correspondance de points de comparaison de vérification formelle, processeur et mémoire Download PDF

Info

Publication number
WO2022000576A1
WO2022000576A1 PCT/CN2020/102281 CN2020102281W WO2022000576A1 WO 2022000576 A1 WO2022000576 A1 WO 2022000576A1 CN 2020102281 W CN2020102281 W CN 2020102281W WO 2022000576 A1 WO2022000576 A1 WO 2022000576A1
Authority
WO
WIPO (PCT)
Prior art keywords
circuit model
matched
comparison
reference circuit
comparison point
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.)
Ceased
Application number
PCT/CN2020/102281
Other languages
English (en)
Chinese (zh)
Inventor
张岩
刘美华
黄国勇
金玉丰
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
Smit Group Ltd
Original Assignee
Smit Group Ltd
Priority date (The priority date 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 date listed.)
Filing date
Publication date
Application filed by Smit Group Ltd filed Critical Smit Group Ltd
Publication of WO2022000576A1 publication Critical patent/WO2022000576A1/fr
Anticipated expiration legal-status Critical
Ceased legal-status Critical Current

Links

Images

Classifications

    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design
    • G06F30/39—Circuit design at the physical level
    • G06F30/398—Design verification or optimisation, e.g. using design rule check [DRC], layout versus schematics [LVS] or finite element methods [FEM]
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design
    • G06F30/32—Circuit design at the digital level
    • G06F30/33—Design verification, e.g. functional simulation or model checking
    • G06F30/3308—Design verification, e.g. functional simulation or model checking using simulation
    • G06F30/3312—Timing analysis
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F30/00—Computer-aided design [CAD]
    • G06F30/30—Circuit design
    • G06F30/32—Circuit design at the digital level
    • G06F30/33—Design verification, e.g. functional simulation or model checking
    • G06F30/3323—Design verification, e.g. functional simulation or model checking using formal methods, e.g. equivalence checking or property checking

Definitions

  • the invention relates to the technical field of equivalence verification of sequential circuits, in particular to a formal verification comparison point matching method, system, processor and memory for identifying and matching corresponding comparison points of two sequential circuits.
  • Combinatorial equivalence testing is a verification method to prove or disprove the functional equivalence of two circuit designs. This verification method is particularly useful when optimizing using only combinatorial synthesis techniques. Corresponding combined blocks of two circuit designs (one called the reference circuit and the other called the implementation circuit) can be compared and verified using the combined form technique. As circuit designs become larger and more complex, verification methods utilizing combinatorial equivalence checking, which provide fast turnaround verification times and complete verification, are rapidly gaining ground over traditional simulation-based verification methods .
  • Methods of non-functional matching use name or structural comparisons to match comparison points in circuit design. In most production verification processes, a significant portion of the comparison points are usually matched using methods other than functional matching. Large numbers of comparison points often do not match because design transitions do not preserve signal names or significantly modify the circuit structure of parts of the design. The method of feature matching is the only feasible automatic method for matching the remaining comparison points.
  • the present invention proposes a formal verification comparison point matching method, system, processor and memory.
  • the present invention first proposes a formal verification comparison point matching method, which includes: step S1: receiving a reference circuit model and a realization circuit model of a sequential circuit to be verified, and further comprising: step S2: controlling the reference circuit model and realizing the circuit model to be matched
  • the test vector of the comparison point is randomly generated, so that the output value of the reference circuit model and the comparison point of the realization circuit model can be matched by a binary tree; Step S3: based on the binary tree matching, the output value of each comparison point to be matched of the reference circuit model is matched with the realization circuit.
  • each comparison point of the model to be matched is matched until all the comparison points of the reference circuit model and the realization circuit model are matched one by one, then the verification is successful; if there is a match between the reference circuit model and the comparison point to be matched by the realization circuit model If it fails, the validation fails.
  • the random generation of the test vectors that control the reference circuit model and the comparison points to be matched by the circuit model is controlled by the ATPG method, so that the sum of the output values of the comparison points to be matched of the reference circuit model or the output value of the circuit model to be matched is controlled.
  • the sum of the output values of the comparison points to be matched is equal to half of the number of comparison points to be matched or half of the number of comparison points to be matched plus one or minus one.
  • the step S2 includes: step S21, randomly generating the reference circuit model and the test vector of the comparison point to be matched by the realization circuit model; step S22, inputting the corresponding test vector into the reference circuit model and the realization circuit respectively model, obtain the reference circuit model and the output value of the comparison point to be matched in the realization circuit model; step S23, calculate the sum of the output values of the comparison point to be matched in the reference circuit model and the output value of the comparison point to be matched in the realization circuit model Sum; Step S24, judge whether the sum of the output values of the comparison points to be matched of the reference circuit model or the sum of the output values of the comparison points to be matched of the realization circuit model is equal to half of the number of the comparison points to be matched or to be matched The number of comparison points of , plus one or minus one half; if not, return to step S21 until the output value of the reference circuit model and the comparison point of the realized circuit model can be matched by a binary tree.
  • the number of comparison points to be matched for the first time by the reference circuit model or the realization circuit model is half of the total number of the reference circuit model or the realization circuit model or half of the total number plus one or minus one. ;
  • the number of comparison points to be matched for the nth time of the reference circuit model or the realization circuit model is half of the number of comparison points to be matched last time or the number of comparison points to be matched last time plus one or minus one Half; until the number of comparison points to be matched at the current time is less than 2, the n>1.
  • the reference circuit model or the test vector that realizes the comparison point to be matched by the circuit model includes a basic input vector input from the outside world, and/or a pseudo main input generated by the previous comparison point of each comparison point.
  • vector, the basic input vector of the reference circuit model and the realization circuit model are the same, and the pseudo main input vector of the reference circuit model and the realization circuit model are the same or different.
  • the present invention proposes a comparison point matching system for formal verification of sequential circuits, which uses the above-mentioned formal verification comparison point matching method to verify sequential circuits.
  • it includes: an input module for receiving the reference circuit model and an input module for implementing the circuit model; a test vector searching module for controlling the random generation of test vectors for the reference circuit model and the comparison point to be matched by the implementation circuit model , so that the output value of the reference circuit model and the comparison point of the realization circuit model can be matched by a binary tree; the matching module, based on the binary tree matching, compares the output value of each comparison point of the reference circuit model to be matched with each comparison of the realization circuit model to be matched The output values of the points are matched until all the comparison points of the reference circuit model and the realized circuit model are matched successfully.
  • the present invention also provides a processor for running a computer program, and the processor executes the above-mentioned formal verification comparison point matching method when running the computer program.
  • the present invention also provides a memory for storing a computer program, when the computer program executes the above-mentioned formal verification comparison point matching method.
  • the present invention has the following advantages.
  • the invention matches the comparison point of the realization circuit model Cimp with the comparison point of the reference circuit model Cref based on the binary tree matching method. After each input test vector is matched, the number of remaining comparison points to be matched is reduced by about half. All comparison points can be matched after a limited number of matches. Assuming that the number of comparison points to be matched is n, the matching of all comparison points can be achieved after about log 2 n times, that is, the complexity of comparison point matching is about log 2 n, which is the smallest in the traditional matching method. The complexity is n-1, and the invention significantly reduces the matching complexity of the corresponding comparison points in the equivalence checking process of the sequential circuit combination, reduces the calculation and matching time of the matching of the corresponding comparison points, and reduces the consumption of memory.
  • FIG. 1 is a schematic flowchart of a formal verification comparison point matching method in an embodiment of the present invention
  • Fig. 2 is the specific flow chart of the formal verification comparison point matching method in the embodiment of the present invention.
  • FIG. 3 is a schematic diagram of a circuit model of a function-based heuristic comparison point matching method in the conventional technology
  • FIG. 4 is a schematic diagram of a reference circuit model of a formal verification comparison point matching method in an embodiment of the present invention
  • FIG. 5 is a schematic diagram of an implementation circuit model of a formal verification comparison point matching method in an embodiment of the present invention.
  • FIG. 6 is a schematic table of the first group of test vectors and their matching results of the embodiment of the function-based heuristic comparison point matching method in the conventional technology of FIG. 3;
  • FIG. 7 is a schematic table of the second group of test vectors and their matching results of the embodiment of the function-based heuristic comparison point matching method in the conventional technology of FIG. 3;
  • FIG. 8 is a schematic table of the third group of test vectors and their matching results of the embodiment of the function-based heuristic comparison point matching method in the conventional technology of FIG. 3;
  • FIG. 9 is a schematic diagram of a first group of test vectors and their matching results of an embodiment of a formal verification comparison point matching method in an embodiment of the present invention.
  • FIG. 10 is a schematic table of the first group of test vectors and their matching results of the embodiment of the formal verification comparison point matching method in the embodiment of the present invention.
  • the present invention provides a formal verification comparison point matching method, comprising: step S1: receiving the reference circuit model and the realization circuit model of the sequential circuit to be verified; step S2: controlling the reference circuit model and the realization circuit model to be matched
  • the test vector of the comparison point is randomly generated, so that the output value of the reference circuit model and the comparison point of the realization circuit model can be matched by a binary tree; Step S3: based on the binary tree matching, the output value of each comparison point to be matched of the reference circuit model and the realization
  • the output value of each comparison point of the circuit model to be matched is matched until all the comparison points of the reference circuit model and the realization circuit model are matched successfully, then the verification is successful; if there are comparison points to be matched between the reference circuit model and the realization circuit model If the match fails, the verification fails.
  • the invention is used for the functional equivalence verification process of two sequential circuits, and is specifically used for identifying and matching the corresponding comparison points of the two sequential circuits.
  • the invention matches the comparison point of the realization circuit model Cimp with the comparison point of the reference circuit model Cref. After each input test vector is matched, the number of remaining comparison points to be matched is reduced by about half. All comparison points can be matched after one match. Assuming that the number of comparison points to be matched is n, all comparison points can be matched after about log 2 n times, that is, the complexity of comparison point matching is about log 2 n.
  • the present invention significantly reduces the matching complexity of the corresponding comparison point in the sequential circuit combination equivalence test process, and reduces the complexity of the comparison point matching. Comparing the calculation matching time of point matching reduces memory consumption.
  • step S1 receive the reference circuit model Cref and realize the circuit model Cimp.
  • the reference circuit model Cref includes basic input vectors PI 1 -PI p and pseudo main input vectors RPI 1 -RPI s corresponding to the reference circuit model Cref. For each comparison point to be matched in the reference circuit model Cref, the output value of each comparison point to be matched in the reference circuit model Cref is obtained according to the basic input vector PI 1 -PI p and/or the pseudo main input vector RPI 1 -RPI s RPO 1 -RPO n .
  • the realization circuit model Cimp includes basic input vectors PI 1 -PI p and pseudo main input vectors IPI 1 -IPI s corresponding to the realization circuit model Cimp.
  • Each comparison circuit model Cimp achieve point to be substantially matched in accordance with the input vector PI 1 -PI p and / or pseudo-primary input vector IPI 1 -IPI s IPO values obtained for each output circuit model implemented Cimp comparison points to be matched l - IPO n.
  • the p in the above PI 1 -PI p is the number of input reference circuit models Cref and basic input vectors that implement the circuit model Cimp.
  • s in RPI 1 -RPI s and IPI 1 -IPI s is the number of the input reference circuit model Cref and the pseudo main input vector implementing the circuit model Cimp.
  • RPO 1 -RPO n IPO 1 -IPO n or n denotes the number of comparison points to be matched.
  • p, s, and n are positive integers.
  • step S2 control the reference circuit model and the test vector of the comparison point to be matched by the realization circuit model to be randomly generated, so that the output value of the reference circuit model and the comparison point of the realization circuit model can carry out binary tree matching;
  • the test vector is used to match the comparison point of the realization circuit model Cimp with the comparison point of the reference circuit model Cref, and input the vectors of the realization circuit model Cimp and the reference circuit model Cref respectively.
  • the test vectors are generated by the ATPG method or the random generation method, and the test vectors generated each time are different.
  • the test vector includes the reference circuit model Cref from the external input and the basic input vector PI 1 -PI p for realizing the circuit model Cimp, and/or the pseudo main input vector generated by the previous comparison point of each comparison point (that is, the previous level).
  • the output value of the comparison point), the basic input vector of the reference circuit model and the realization circuit model are the same, and the pseudo main input vector of the reference circuit model and the realization circuit model are the same or different.
  • the pseudo main input vectors RPI 1 -RPI n are used for inputting the reference circuit model Cref, and the pseudo main input vectors IPI 1 -IPI n are used for inputting the realization circuit model Cimp.
  • the output values RPO 1 -RPO n of the comparison points to be matched in the reference circuit model Cref and the output values IPO 1 -IPO n of the comparison points to be matched in the realization circuit model Cimp can be performed in the form of a binary tree match.
  • Step S2 specifically includes the following steps:
  • Step S21 randomly generating a reference circuit model and a test vector that realizes the comparison point of the circuit model to be matched;
  • Step S22 input the corresponding test vectors to the reference circuit model and the realization circuit model respectively, and obtain the output value of the comparison point to be matched between the reference circuit model and the realization circuit model;
  • Step S23 calculating the sum of the output values of the comparison points to be matched of the reference circuit model and the sum of the output values of the comparison points to be matched of the realization circuit model;
  • step S23 is: the output value of the comparison point between the reference circuit model Cref and the realization circuit model Cimp is a logic value of 1 or 0. So the sum of the output values of the comparison points is 0-n.
  • the calculation in this step is expressed as a mathematical formula as:
  • Step S24 judging whether the sum of the output values of the comparison points to be matched of the reference circuit model or the sum of the output values of the comparison points to be matched of the realization circuit model is equal to half the number of the comparison points to be matched or the comparison points to be matched. plus or minus one half of the quantity;
  • step S21 If not, return to step S21 until the output value of the comparison point between the reference circuit model and the realized circuit model can be matched by a binary tree. If yes, go to step S3.
  • step S24 if the sum of the output values of the comparison points to be matched of the reference circuit model Cref and the output values of the comparison points to be matched of the realization circuit model Cimp is not equal to the number of comparison points to be matched half of the number of comparison points to be matched or not equal to half of the number of comparison points to be matched plus one or minus one, indicating that the effect of the test vector does not reach just enough to make half of the comparison points to be matched or the comparison points to be matched plus one or minus one The latter half is matched, which does not satisfy the matching form based on the principle of binary tree, so return to step S21.
  • step S21 randomly generates another group of test vectors and inputs the reference circuit model Cref and the realization circuit model Cimp, and repeats step S21-step S24, until the judgment result in step S24 is yes, that is, the comparison point of the reference circuit model Cref to be matched is
  • the sum of the output values and the output values of the comparison points to be matched that realize the circuit model Cimp is equal to half of the number of comparison points to be matched or not equal to one half of the number of comparison points to be matched plus one or minus one, namely Satisfy the matching form based on the principle of binary tree. It means that after the test vector is input to the reference circuit model and the realization circuit model, half of the comparison points to be matched are matched or half of the comparison points to be matched are matched by adding or subtracting one. Then it can go to step S3.
  • step S3 based on binary tree matching, the output value of each comparison point to be matched of the reference circuit model is matched with the output value of each comparison point to be matched of the realization circuit model, until all comparison points of the reference circuit model and the realization circuit model are matched If all the matching is successful, the verification is successful; if there is a reference circuit model and the comparison point to be matched by the realization circuit model fails to match, the verification fails.
  • the number of comparison points to be matched for the first time in the reference circuit model or the implementation circuit model is half of the total number of comparison points to be matched in the reference circuit model or the implementation circuit model, or the total number plus one or minus one. half. Then, it is necessary to detect the number of comparison points to be matched for the current time remaining in the reference circuit model Cref and the implementation circuit model Cimp, and to determine whether the number of comparison points to be matched for the current time is less than 2.
  • the number of comparison points to be matched at the current time is greater than or equal to 2, it means that there are at least 2 comparison points in the reference circuit model and the realized circuit model that have not been matched, that is, the comparison points in the realized circuit model Cimp are not completely one-to-one.
  • further matching is required to realize the remaining comparison points to be matched in the circuit model Cimp and the reference circuit model Cref.
  • step S2 it is necessary to return to step S2 again, generate a new set of test vectors and input them into the reference circuit model and the realization circuit model, and assign the value of the number of comparison points to be matched (n in the mathematical formula in step S2) as the updated The remaining value of the number of comparison points to be matched at the current time, and further matching is performed on the comparison points to be matched at the current time. Steps S2-S3 are repeated in this way.
  • the number of comparison points to be matched for the nth time of the reference circuit model or the realization circuit model is half of the number of comparison points to be matched last time (n-1th) or the number of comparison points to be matched last time plus one or Half after subtracting one. After about log 2 n times, the number of comparison points to be matched at the current time is less than 2, it means that each comparison point in the realization circuit model Cimp has a complete one-to-one correspondence with each comparison point in the reference circuit model Cref If there is a match, no further matching is required, the entire matching process ends, and the verification is successful. n>1.
  • the invention matches the comparison points in the circuit model Cimp and the reference circuit model Cref, and only needs log 2 n times to complete the one-to-one matching of all the comparison points, that is, the complexity of the comparison point matching is reduced to log 2 n.
  • the comparison point matching complexity is n-1, which significantly reduces the comparison point matching complexity and reduces the comparison point matching in the sequential circuit combination equivalence test process. Calculate the matching time and reduce the memory consumption.
  • the reference circuit model Cref has 2 basic input vectors PI 1 , PI 2 , and 4 comparison points M1 , M2 , M3 , M4 .
  • the realization circuit model Cimp has 2 basic input vectors PI 1 , PI 2 , and 4 comparison points N1 , N2 , N3 , N4 .
  • the number of pseudo main input vectors may be equal to the number of comparison points, or may not be equal to the number of comparison points.
  • the present invention proposes a comparison point matching system for formal verification of sequential circuits, which uses the above-mentioned formal verification comparison point matching method to verify sequential circuits.
  • the system includes: an input module for receiving the reference circuit model and an input module for realizing the circuit model; a test vector searching module for controlling the random generation of the reference circuit model and the test vector of the comparison point to be matched by the realization circuit model, so that the reference circuit
  • the output value of the comparison point between the model and the realization circuit model can be matched by a binary tree; the matching module, based on the binary tree matching, matches the output value of each comparison point to be matched of the reference circuit model and the output value of each comparison point to be matched of the realization circuit model. Matching is performed until all the comparison points of the reference circuit model and the realized circuit model are matched successfully.
  • the present invention also provides a processor for running a computer program, and the processor executes the above-mentioned formal verification comparison point matching method when running the computer program.
  • the present invention also provides a memory for storing a computer program, when the computer program executes the above-mentioned formal verification comparison point matching method.

Landscapes

  • Engineering & Computer Science (AREA)
  • Computer Hardware Design (AREA)
  • Physics & Mathematics (AREA)
  • Theoretical Computer Science (AREA)
  • Evolutionary Computation (AREA)
  • Geometry (AREA)
  • General Engineering & Computer Science (AREA)
  • General Physics & Mathematics (AREA)
  • Tests Of Electronic Circuits (AREA)

Abstract

L'invention concerne un procédé et un système d'appariement de points de comparaison de vérification formelle, un processeur et une mémoire. Le procédé comprend : la réception d'un modèle de circuit de référence et d'un modèle de circuit mis en œuvre d'un circuit séquentiel à vérifier ; la commande de vecteurs de test de points de comparaison à apparier du modèle de circuit de référence et du modèle de circuit mis en œuvre pour être généré de manière aléatoire, de telle sorte qu'une mise en correspondance d'arbre binaire peut être effectuée sur des valeurs de sortie des points de comparaison du modèle de circuit de référence et du modèle de circuit mis en œuvre ; la mise en correspondance, sur la base de la mise en correspondance d'arbres binaires, des valeurs de sortie des points de comparaison à mettre en correspondance du modèle de circuit de référence avec les valeurs de sortie des points de comparaison à mettre en correspondance du modèle de circuit mis en œuvre jusqu'à ce que tous les points de comparaison du modèle de circuit de référence et du modèle de circuit mis en œuvre soient mis en correspondance avec succès sur une base biunivoque, et indiquant que la vérification est réussie ; et si les points de comparaison à mettre en correspondance du modèle de circuit de référence et du modèle de circuit mis en œuvre ne peuvent pas être mis en correspondance, l'indication que la vérification a échoué. Au moyen de la présente invention, la complexité de mise en correspondance des points de comparaison correspondants dans le processus de vérification d'équivalence d'un circuit séquentiel est réduite, le temps de mise en correspondance est réduit, et la consommation de mémoire est réduite.
PCT/CN2020/102281 2020-07-03 2020-07-16 Procédé et système de mise en correspondance de points de comparaison de vérification formelle, processeur et mémoire Ceased WO2022000576A1 (fr)

Applications Claiming Priority (2)

Application Number Priority Date Filing Date Title
CN202010632501.7A CN111797588B (zh) 2020-07-03 2020-07-03 一种形式验证比较点匹配方法、系统、处理器及存储器
CN202010632501.7 2020-07-03

Publications (1)

Publication Number Publication Date
WO2022000576A1 true WO2022000576A1 (fr) 2022-01-06

Family

ID=72810228

Family Applications (1)

Application Number Title Priority Date Filing Date
PCT/CN2020/102281 Ceased WO2022000576A1 (fr) 2020-07-03 2020-07-16 Procédé et système de mise en correspondance de points de comparaison de vérification formelle, processeur et mémoire

Country Status (2)

Country Link
CN (1) CN111797588B (fr)
WO (1) WO2022000576A1 (fr)

Cited By (1)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN116429160A (zh) * 2023-02-07 2023-07-14 北京奕斯伟计算技术股份有限公司 一种用于追踪编码器测试的控制方法及装置

Families Citing this family (2)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN114896921B (zh) * 2022-06-10 2023-06-27 深圳国微芯科技有限公司 一种集成电路形式验证方法、系统及存储介质
CN115048887A (zh) * 2022-06-21 2022-09-13 深圳国微芯科技有限公司 带门控时钟的实现电路的处理方法、验证方法、存储介质

Citations (3)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US6408424B1 (en) * 1999-06-04 2002-06-18 Fujitsu Limited Verification of sequential circuits with same state encoding
CN1560769A (zh) * 2004-03-05 2005-01-05 中国科学院计算技术研究所 基于可满足性的组合电路等价性检验方法
CN107798203A (zh) * 2017-11-16 2018-03-13 宁波大学 一种组合逻辑电路等效性检测方法

Family Cites Families (2)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN102567165B (zh) * 2011-12-29 2014-04-23 中国科学院自动化研究所 对寄存器传输级硬件实现进行验证的系统及方法
CN105589993B (zh) * 2015-12-18 2019-01-15 中国科学院微电子研究所 微处理器功能验证设备及微处理器功能验证方法

Patent Citations (3)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US6408424B1 (en) * 1999-06-04 2002-06-18 Fujitsu Limited Verification of sequential circuits with same state encoding
CN1560769A (zh) * 2004-03-05 2005-01-05 中国科学院计算技术研究所 基于可满足性的组合电路等价性检验方法
CN107798203A (zh) * 2017-11-16 2018-03-13 宁波大学 一种组合逻辑电路等效性检测方法

Cited By (1)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN116429160A (zh) * 2023-02-07 2023-07-14 北京奕斯伟计算技术股份有限公司 一种用于追踪编码器测试的控制方法及装置

Also Published As

Publication number Publication date
CN111797588B (zh) 2022-11-11
CN111797588A (zh) 2020-10-20

Similar Documents

Publication Publication Date Title
JP7029873B2 (ja) 人工知能チップのテスト方法、装置、機器、及び記憶媒体
WO2022000576A1 (fr) Procédé et système de mise en correspondance de points de comparaison de vérification formelle, processeur et mémoire
GB2549933A (en) Verification of hardware designs to implement floating point power functions
US5491639A (en) Procedure for verifying data-processing systems
WO2022077645A1 (fr) Procédé et système de génération de fnc pour vérification d'équivalence
CN116050311B (zh) 一种基于完备仿真的组合运算电路等价性验证方法及系统
EP3557455A1 (fr) Vérification de conception de matériel d'un composant mettant en uvre une fonction respectant la permutation
CN120781760B (zh) 时序分析方法、装置、计算机设备、存储介质及程序产品
CN113486613A (zh) 数据链路的提取方法、装置、电子设备和存储介质
CN115062570B (zh) 一种形式验证方法、装置、设备及计算机存储介质
CN116976248A (zh) 使用冗余节点的电路设计调整
CN112733474B (zh) 基于与门反相器图的网表级电路面积优化方法及存储介质
US10852354B1 (en) System and method for accelerating real X detection in gate-level logic simulation
US20220147677A1 (en) Verification of hardware design for an integrated circuit that implements a function that is polynomial in one or more sub-functions
CN110763984B (zh) 逻辑电路失效率确定方法、装置、设备及存储介质
CN113496106A (zh) 用于验证排序器的方法和系统
CN112904187A (zh) 一种扫描链构建方法、装置、设备及存储介质
CN116483633A (zh) 一种数据增广方法及相关装置
Parthasarathy et al. Combining ATPG and symbolic simulation for efficient validation of embedded array systems
CN116029237A (zh) 一种基于fpga原型验证的等价性验证方法及系统
CN114490367A (zh) 基于覆盖率信息的蜕变测试用例对排序方法
CN109933948B (zh) 一种形式验证方法、装置、形式验证平台及可读存储介质
CN111695321B (zh) 电路设计方法及相关的电脑程序产品
CN113449477A (zh) 数字电路的连接方法、装置、电子设备和存储介质
US12488169B1 (en) Performing timing constraint equivalence checking on circuit designs

Legal Events

Date Code Title Description
121 Ep: the epo has been informed by wipo that ep was designated in this application

Ref document number: 20943815

Country of ref document: EP

Kind code of ref document: A1

NENP Non-entry into the national phase

Ref country code: DE

122 Ep: pct application non-entry in european phase

Ref document number: 20943815

Country of ref document: EP

Kind code of ref document: A1