WO2022000576A1 - Formal verification comparison point matching method and system, processor, and memory - Google Patents

Abstract

Disclosed are a formal verification comparison point matching method and system, a processor, and a memory. The method comprises: receiving a reference circuit model and an implemented circuit model of a sequential circuit to be verified; controlling test vectors of comparison points to be matched of the reference circuit model and the implemented circuit model to be randomly generated, so that binary tree matching can be performed on output values of the comparison points of the reference circuit model and the implemented circuit model; matching, on the basis of binary tree matching, the output values of the comparison points to be matched of the reference circuit model with the output values of the comparison points to be matched of the implemented circuit model until all the comparison points of the reference circuit model and the implemented circuit model are successfully matched on a one-to-one basis, and indicating that the verification is successful; and if the comparison points to be matched of the reference circuit model and the implemented circuit model fail to be matched, indicating that the verification fails. By means of the present invention, the matching complexity of corresponding comparison points in the equivalence checking process of a sequential circuit is reduced, the matching time is reduced, and the memory consumption is reduced.

Description

Formal verification comparison point matching method, system, processor and memory technical field

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.

Background technique

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 .

For sequential circuits, an important step in applying combinatorial equivalence testing is to identify and match the corresponding comparison points in the two circuit designs to be verified. The point of comparison in circuit design is the combinational logic endpoint during verification. Compare points can be output ports, registers, latches, or black-box input pins. Comparison point matching methods in commercial verification tools can be roughly divided into two categories: non-functional matching methods and functional matching 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.

At present, most methods of functional matching are based on precise methods of fixed-point computing, given N storage elements (latches, registers, etc.) in the design of each sequential circuit, there are N! possible combinations to match them. In the worst case, all of these exact methods may have to enumerate all combinations, which makes comparison point matching very complicated, resulting in long computation time and large memory footprint.

There are also heuristics based on feature matching, by establishing non-equivalence relations between comparison points, and then grouping the most likely equivalent points into pairs by using the non-equivalence information, assuming given N comparison points, adopt The computational complexity of this method is N-1, which is less than that of exact computation. However, when there are many comparison points, the calculation time will still be very long, and the memory occupied by storing the unequal information will also be very large.

Therefore, how to design a matching method that can quickly identify and match the corresponding comparison points in the two circuit designs to be verified is a technical problem to be solved urgently in the industry.

SUMMARY OF THE INVENTION

In order to solve the above-mentioned technical problem in the prior art that it takes a long time to identify and match corresponding comparison points in two circuit designs to be verified, 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. The output value of 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.

In one embodiment, 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.

In one embodiment, 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.

In one embodiment, 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.

In one embodiment, 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.

Next, 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.

In one embodiment, 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.

Compared with the prior art, 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 ₂ 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.

Description of drawings

In order to illustrate the technical solutions in the embodiments of the present invention more clearly, the following briefly introduces the accompanying drawings that need to be used in the description of the embodiments or the prior art. Obviously, the drawings in the following description are only for the present invention. In some embodiments, for those of ordinary skill in the art, other drawings can also be obtained from these drawings without any creative effort.

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;

3 is a schematic diagram of a circuit model of a function-based heuristic comparison point matching method in the conventional technology;

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;

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;

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;

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;

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;

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.

detailed description

In order to make the technical problems, technical solutions and beneficial effects to be solved by the present invention clearer, the present invention will be further described in detail below with reference to the accompanying drawings and embodiments. It should be understood that the specific embodiments described herein are only used to explain the present invention, but not to limit the present invention.

Thus, a reference to a feature in this specification will be used to describe one of the features of an embodiment of the invention and not to imply that every embodiment of the invention must have the described feature. Furthermore, it should be noted that this specification describes a number of features. Although certain features may be combined together to illustrate possible system designs, these features may also be used in other combinations not explicitly stated. Thus, unless otherwise stated, the combinations described are not intended to be limiting.

The principle and structure of the present invention will be described in detail below with reference to the accompanying drawings and embodiments.

Referring to Fig. 1, 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. Based on the binary tree principle, 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 ₂ n. Compared with the comparison point matching complexity of the heuristic matching method without logical constraints in the traditional technology is n-1, 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. The above-mentioned formal verification comparison point matching method will be described in detail below.

Please refer to Fig. 2, 4-5, in step S1: receive the reference circuit model Cref and realize the circuit model Cimp.

Specifically, 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 ₁ -RPI _s RPO ₁ -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 ₁ -PI _p and / or pseudo-primary input vector IPI ₁ -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 ₁ -PI p is the number of input reference circuit models Cref and basic input vectors that implement the circuit model Cimp. s in RPI ₁ -RPI _s and IPI ₁ -IPI _s is the number of the input reference circuit model Cref and the pseudo main input vector implementing the circuit model Cimp. RPO ₁ -RPO _n IPO ₁ -IPO _n or n denotes the number of comparison points to be matched. p, s, and n are positive integers.

In 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;

Specifically, 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. Among them, the pseudo main input vectors RPI ₁ -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. It should be noted that reference Cref circuit model vector PI ₁ -PI _p and the dummy main RPI ₁ -RPI _n input vectors to obtain an output value of each point to be matched comparison RPO ₁ -RPO _n basic input. Circuit model implemented Cimp vector PI ₁ -PI _p and the dummy main IPI ₁ -IPI _n input vectors obtained for each point to be matched comparison output values IPO ₁ -IPO _n basic input. In this step, by controlling the test vector, the output values RPO ₁ -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;

It should be noted that 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:

The sum of the output values of the comparison points to be matched of the reference circuit model Cref is:

The sum of the output values of the comparison points to be matched to realize the circuit model Cimp is:

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;

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.

The calculation in this step is expressed as a mathematical formula as:

When the number of comparison points to be matched is an even number, it is judged whether 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 equal to the comparison to be matched Half the number of points, the formula is:

When the number of comparison points to be matched is odd, it is judged whether 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 equal to the comparison to be matched The number of points plus one or minus one half, the formula is:

or

It should be noted that in 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. Then 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.

In 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.

It should be noted that 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. If 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. Correspondingly, to complete the matching with the comparison points in the reference circuit model Cref, further matching is required to realize the remaining comparison points to be matched in the circuit model Cimp and the reference circuit model Cref. Therefore, 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 ₂ 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.

Based on the binary tree principle, the invention matches the comparison points in the circuit model Cimp and the reference circuit model Cref, and only needs log ₂ 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 ₂ n. Compared with the heuristic matching method without logical constraints in the traditional technology, 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.

In order to facilitate the understanding of the principles and methods of the present invention and the advantages of the present invention compared with the traditional technology, the principles, methods and advantages of the present invention are described below with a pair of embodiments with certain values.

In this embodiment, the reference circuit model Cref has 2 basic input vectors PI ₁ , PI ₂ , and 4 comparison points M1 , M2 , M3 , M4 . The realization circuit model Cimp has 2 basic input vectors PI ₁ , PI ₂ , and 4 comparison points N1 , N2 , N3 , N4 .

Referring to Figures 3, 6-8, the function-based heuristic comparison point matching method using traditional techniques is as follows:

1) Referring to Figure 6, through the first set of test vectors, [M1, N1], [M2, M3, M4, N2, N3, N4] are obtained. where [M1,N1] is the matching comparison point.

2) Referring to Figure 7, through the second set of test vectors, [M1, N1], [M2, N3], [M3, M4, N2, N4] are obtained. where [M2,N3] is the matching comparison point.

3) Referring to Figure 8, through the third set of test vectors, [M1, N1], [M2, N3], [M3, N2], [M4, N4] are obtained. where [M3, N2], [M4, N4] are matching comparison points.

It can be seen that using the function-based heuristic matching method in the traditional technology, in the absence of logical constraints, it takes 3 times (n-1 times) to complete the matching of all comparison points, that is, the complexity of comparison point matching is 3 (n-1).

Please refer to Fig. 9-10, adopt the formal verification comparison point matching method of the present invention as follows:

1) Referring to Figure 9, through the first set of test vectors (PI ₁ , PI ₂ , RPI ₁ , RPI ₂ , RPI ₃ , RPI ₄ , IPI ₁ , IPI ₂ , IPI ₃ , IPI ₄ ), the comparison points can be divided into There are 2 groups: [M1,M2,N1,N3], [M3,M4,N2,N4].

2) Referring to Figure 10, through the second set of test vectors (PI ₁ , PI ₂ , RPI ₁ , RPI ₂ , RPI ₃ , RPI ₄ , IPI ₁ , IPI ₂ , IPI ₃ , IPI ₄ ), the comparison points can be divided into For 4 groups, [M1, N1], [M2, N3], [M3, N2], [M4, N4].

It can be seen that, using the formal verification comparison point matching method of the present invention, in the case of logical constraints based on the principle of binary tree, it takes 2 times (log ₂ n times) to complete the matching of all comparison points, that is, the complexity of comparison point matching. is 2(log ₂ n).

It should be noted that in other embodiments, 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.

Next, 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.

The above descriptions are only preferred embodiments of the present invention and are not intended to limit the present invention. Any modifications, equivalent replacements and improvements made within the spirit and principles of the present invention shall be included in the protection of the present invention. within the range.

Claims (9)

1. 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, and it is characterized in that, it also includes:

   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 be matched by a binary tree;

   Step S3: Match the output value of each comparison point of the reference circuit model to be matched with the output value of each comparison point to be matched of the realization circuit model based on the binary tree matching, until all comparison points of the reference circuit model and the realization circuit model are all the same. Once 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.
2. The formal verification comparison point matching method according to claim 1, wherein the random generation of the test vector for controlling the reference circuit model and the comparison point to be matched by the circuit model is controlled by the ATPG method, so that the to-be-matched reference circuit model is controlled by the ATPG method. The sum of the output values of the comparison points or the sum of the output values of the comparison points to be matched implementing the circuit model is equal to half the number of comparison points to be matched or the number of comparison points to be matched plus one or minus one.
3. The formal verification comparison point matching method according to claim 1, wherein the step S2 comprises:

   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 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;

   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.
4. Formal verification comparison point matching method as claimed in claim 1, is characterized in that,

   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 half of the number of comparison points to be matched last time plus one or minus one ; Until the number of comparison points to be matched at the current time is less than 2, the n>1.
5. The formal verification comparison point matching method according to claim 1, wherein the reference circuit model or the test vector for realizing the comparison point to be matched by the circuit model includes a basic input vector input from the outside, and/or a The reference circuit model and the basic input vector of the realization circuit model are the same, and the reference circuit model and the pseudo main input vector of the realization circuit model are the same or different.
6. A comparison point matching system for formal verification of sequential circuits is characterized in that the sequential circuit is verified by using the formal verification comparison point matching method of any one of claims 1-5.
7. The comparison point matching system of sequential circuit formal verification as claimed in claim 6, is characterized in that, comprises:

   an input module for receiving the reference circuit model and an input module for implementing the circuit model;

   The test vector search module is used to control the random generation of the test vector of the reference circuit model and the comparison point of the realization circuit model to be matched, 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 is used for matching the output value of each comparison point of the reference circuit model to be matched with the output value of each comparison point to be matched of the realization circuit model based on binary tree matching, until all comparison points of the reference circuit model and the realization circuit model are matched All matched successfully.
8. A processor for running a computer program, characterized in that, when the processor runs the computer program, the formal verification comparison point matching method according to claims 1 to 5 is executed.
9. A memory for storing a computer program, characterized in that the computer program executes the formal verification comparison point matching method according to claims 1 to 5.

Images