CN107798203A - A kind of combinational logic circuit equivalence detection method - Google Patents
A kind of combinational logic circuit equivalence detection method Download PDFInfo
- Publication number
- CN107798203A CN107798203A CN201711136173.6A CN201711136173A CN107798203A CN 107798203 A CN107798203 A CN 107798203A CN 201711136173 A CN201711136173 A CN 201711136173A CN 107798203 A CN107798203 A CN 107798203A
- Authority
- CN
- China
- Prior art keywords
- combinational circuit
- variable
- value
- product term
- circuit
- 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.)
- Granted
Links
Classifications
-
- 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/327—Logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist
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)
- Logic Circuits (AREA)
Abstract
本发明公开了一种组合逻辑电路等效性检测方法，通过扩展余子式概念，将逻辑覆盖等效性检测问题分成分解成电路包含检测子问题,逐一求取其中一个电路表达式对另一个电路表达式各乘积项的余子式，然后在建立各乘积项余子式的香农结构图基础上判断其是否重言式，最后根据重言式判别结果确定两电路间是否覆盖等效关系；优点是通过求取乘积项余子式对逻辑函数进行分解和降阶处理,从而加快了覆盖等效性验证速度，可操作性和检测效率均较高，且不会出现内存爆炸问题，实验结构表明，本发明的方法稳定有效的，对EXPRESSO软件集成的三种算法所得电路的测试结果表明,与基于真值表和BDD的两种检测算法相比,具有明显的速度优势。The invention discloses a method for detecting equivalence of combined logic circuits. By extending the concept of remainder formula, the problem of equivalence detection of logic coverage is divided into subproblems of circuit inclusion detection, and one by one the expression of one of the circuits is calculated for the other circuit. The cofactor of each product term of the expression, and then judge whether it is a tautology on the basis of establishing the Shannon structure diagram of each product term cofactor, and finally determine whether the equivalence relationship between the two circuits is covered according to the result of the tautology discrimination; the advantage is that through The logic function is decomposed and order-reduced by obtaining the remainder of the product term, thereby speeding up the coverage equivalence verification speed, high operability and detection efficiency, and no memory explosion problem. The experimental structure shows that the present invention The method is stable and effective. The test results of the circuit obtained by the three algorithms integrated in the EXPRESSO software show that it has obvious speed advantages compared with the two detection algorithms based on the truth table and BDD.
Description
技术领域technical field
本发明涉及一种检测方法，尤其是涉及一种组合逻辑电路等效性检测方法。The invention relates to a detection method, in particular to a combinational logic circuit equivalence detection method.
背景技术Background technique
逻辑等效性检测以逻辑层表达式不同的2个组合电路等效性检验为目的，根据给定 的2个组合电路的逻辑表达式，检测它们是否实现相同的逻辑功能。目前组合逻辑电路等效性检测方法主要有代数法、真值表判定法和功能性方法。The logic equivalence test is aimed at the equivalence test of two combinational circuits with different logic layer expressions. According to the given logical expressions of the two combinational circuits, it is tested whether they realize the same logic function. At present, the equivalence detection methods of combinational logic circuits mainly include algebraic method, truth table judgment method and functional method.
代数法是检验组合逻辑电路等效性的一种直观方法，该方法采用逻辑代数的基本公 式处理2个组合电路的逻辑表达式，若能得到相同的结果，则2个组合电路的逻辑表 达式是逻辑等效的。但是，由于逻辑代数的基本公式数量较多，该方法中，基本公式选 择、所选若干个基本公式的应用顺序以及所选的每个基本公式处理对象的选择等环节都 存在多种可选方案，具体方案的选择与电路结构有直接关系，尚没有统一可行的指导路 线可用。因此，采用代数法对组合逻辑电路等效性进行检测具有很大的盲目性，该方法 可操作性差，且计算量和计算时间也随电路规模急剧增长，检测效率很低，在实际中很 少单独采用。The algebraic method is an intuitive method to test the equivalence of combinational logic circuits. This method uses the basic formula of logic algebra to process the logical expressions of two combinational circuits. If the same result can be obtained, the logical expressions of the two combinational circuits are logically equivalent. However, due to the large number of basic formulas in logic algebra, in this method, there are many options for the selection of basic formulas, the application order of several selected basic formulas, and the selection of processing objects for each selected basic formula. , the choice of a specific scheme is directly related to the circuit structure, and there is no unified and feasible guiding route available. Therefore, using the algebraic method to detect the equivalence of combinational logic circuits has great blindness. This method has poor operability, and the amount of calculation and calculation time also increase sharply with the scale of the circuit. Taken alone.
真值表判定法通过利用真值表来判定2个组合电路的逻辑表达式是否存在逻辑等效 关系。该方法中，将2个组合电路的输入变量取值的所有可能组合逐一代入2个组合电路的逻辑表达式，然后根据结果是否都相同即可得出结论。虽然该方法相对于代数法， 可操作性较高，但是很明显，当电路规模增大时，组合电路的输入变量取值也将急剧增 加，该方法的时间开销将急剧增加，检测效率仍然较低。The truth table judgment method uses the truth table to judge whether there is a logical equivalence relationship between the logical expressions of two combinational circuits. In this method, all possible combinations of the input variable values of the two combinational circuits are substituted into the logical expressions of the two combinational circuits one by one, and then a conclusion can be drawn according to whether the results are the same. Although this method is more operable than the algebraic method, it is obvious that when the circuit scale increases, the value of the input variable of the combinational circuit will also increase sharply, the time cost of this method will increase sharply, and the detection efficiency is still relatively low. Low.
功能性方法是目前常用的组合逻辑电路等效性检测方法，该方法将2个组合电路表 示成一种规范形式，如二进制决策图(BDD),若2个组合电路的规范形式同构则它们等效。该方法也不存在可操作性的问题，虽然相对于真值表判定法检测效率有所提高，但 是仍不能满足目前超大规模电路的需求，而且该方法在某些输入变量顺序下会面临内存 爆炸的问题。The functional method is a commonly used equivalence detection method for combinational logic circuits. This method expresses two combinational circuits in a canonical form, such as a binary decision diagram (BDD). If the canonical forms of two combinational circuits are isomorphic, then they are equal effect. This method does not have the problem of operability. Although the detection efficiency has been improved compared with the truth table determination method, it still cannot meet the needs of current ultra-large-scale circuits, and this method will face memory explosion under certain input variable sequences. The problem.
发明内容Contents of the invention
本发明所要解决的技术问题是提供一种可操作性和检测效率均较高，且不会出现内 存爆炸问题的组合逻辑电路等效性检测方法。The technical problem to be solved by the present invention is to provide a combinational logic circuit equivalence detection method with high operability and detection efficiency, and no memory explosion problem.
本发明解决上述技术问题所采用的技术方案为：一种组合逻辑电路等效性检测方法，包括以下步骤：The technical scheme adopted by the present invention to solve the above-mentioned technical problems is: a method for detecting the equivalence of a combinational logic circuit, comprising the following steps:
(1)将待检测的两个组合电路记为a和b，其中，a的逻辑表达式为：(1) Record the two combined circuits to be detected as a and b, where the logical expression of a is:
b的逻辑表达式为：The logical expression of b is:
其中，n为组合电路a和b的变量数，∑为求和运算符号，p为组合电路a的乘积项的数量，q为组合电路b的乘积项的数量，ai为组合电路a的第i个乘积项，ai＝xi'1xi'2…xi'k…xi'n， k为大于等于1且小于等于n的整数，xi'k为乘积项ai第k位的文字变量，表示对应输入变量 xk在乘积项ai第k位的出现形式，xi'k∈{0,1,-}，当xi'k＝0时，xk以其反变量的形式出现 在乘积项ai第k位，当xi'k＝1时，xk以其原变量xk的形式出现在乘积项ai第k位，当xi'k＝- 时，表示xk的值恒为1，xk不出现在乘积项ai第k位中；bj为组合电路b的第j个乘积项， bj＝y'j1y'j2…y'jh…y'jn，h为大于等于1且小于等于n的整数，y'jh为乘积项bj第h位的文字 变量，表示对应输入变量yh在乘积项bj第h位的出现形式，y'jh∈{0,1,-}，当y'jh＝0时，yh以其反变量yh的形式出现在乘积项bj第h位，当y'jh＝1时，yh以其原变量yh的形式出现 在乘积项bj第h位，当y'jh＝-时，表示yh的值恒为1，yh不出现在乘积项bj第h位；Among them, n is the variable number of combinational circuits a and b, ∑ is the summation symbol, p is the number of product terms of combinational circuit a, q is the number of product terms of combinational circuit b, and a i is the number of product terms of combinational circuit a i product items, a i = x i ' 1 x i ' 2 ... x i ' k ... x i ' n , k is an integer greater than or equal to 1 and less than or equal to n, x i ' k is the kth product item a i The text variable of the bit, which represents the appearance form of the corresponding input variable x k in the kth bit of the product item a i , x i ' k ∈ {0,1,-}, when x i ' k = 0, x k is its inverse variable The form appears in the kth position of the product term a i , when xi ' k = 1, x k appears in the kth position of the product term a i in the form of its original variable x k , when xi ' k =-, Indicates that the value of x k is always 1, and x k does not appear in the kth bit of the product item a i ; b j is the jth product item of the combinational circuit b, b j =y' j1 y' j2 …y' jh … y' jn , h is an integer greater than or equal to 1 and less than or equal to n, y' jh is a text variable at the hth position of the product term b j , indicating the appearance form of the corresponding input variable y h at the hth position of the product term b j , y ' jh ∈ {0,1,-}, when y' jh =0, y h appears in the hth position of the product term b j in the form of its inverse variable y h , when y' jh =1, y h appears as The form of the original variable y h appears in the h position of the product term b j , when y' jh =-, it means that the value of y h is always 1, and y h does not appear in the h position of the product term b j ;
(2)判断组合电路a是否包含组合电路b，具体过程为：(2) Judging whether the combinational circuit a includes the combinational circuit b, the specific process is:
A.设定变量f，初始化变量f，令变量f＝1；A. Set variable f, initialize variable f, make variable f=1;
B.设定变量u，初始化变量u，令u＝1；设定变量t，初始化变量t，令变量t＝1；B. set variable u, initialize variable u, make u=1; set variable t, initialize variable t, make variable t=1;
C.将组合电路a对组合电路b的第f个乘积项bf的余子函数表示为af(x1,x2,…,xn)，将组合电路a的第t个乘积项at对组合电路b的第f个乘积项bf的余子式记为 C. Express the cosubfunction of the f-th product term b f of the combinational circuit a to the combinational circuit b as a f (x 1 ,x 2 ,…,x n ), and the t-th product term a t of the combinational circuit a The remainder of the fth product term b f of the combinational circuit b is written as
D.令xt”k为第k位的文字变量，表示对应输入变量xk在第k位的出现形式，xt”k∈{0,1,-,NULL}，当xt”k＝0时，xk以其反变量的形式出现在第k位， 当xt”k＝1时，xk以原变量其xk的形式出现在第k位，当xt”k＝-时，表示xk的值恒为1，xk不出现在第k位，当xt”k＝NULL时，表示xk的值恒为0；D. order x t ” k is The text variable at the kth position indicates that the corresponding input variable x k is in The appearance form of the kth bit, x t ” k ∈ {0,1,-,NULL}, when x t ” k = 0, x k takes its inverse variable in the form of At bit k, when x t ” k =1, x k appears in the form of x k of the original variable The kth bit, when x t ” k =-, means that the value of x k is always 1, and x k does not appear in The kth bit, when x t ” k = NULL, means that the value of x k is always 0;
按照以下规则依次对的第u位文字变量xt”u进行赋值：According to the following rules in order The u-th literal variable x t ” u is assigned:
若xt'u＝y'fu，则令xt”u＝-；If x t ' u =y' fu , then make x t ” u =-;
若xt'u≠y'fu，且xt'u＝-，y'fu＝0，则令xt”u＝-；If x t ' u ≠y' fu , and x t ' u ＝-, y' fu ＝0, then make x t ” u ＝-;
若xt'u≠y'fu，且xt'u＝-，y'fu＝1，则令xt”u＝-；If x t ' u ≠y' fu , and x t ' u ＝-, y' fu ＝1, then make x t ” u ＝-;
若xt'u≠y'fu，且xt'u＝0，y'fu＝1，则令xt”u＝NULL；If x t ' u ≠y' fu , and x t ' u =0, y' fu =1, then let x t ' u =NULL;
若xt'u≠y'fu，且xt'u＝1，y'fu＝0，则令xt”u＝NULL；If x t ' u ≠y' fu , and x t ' u = 1, y' fu = 0, then set x t ” u = NULL;
若xt'u≠y'fu，且xt'u＝0，y'fu＝-，则令xt”u＝0；If x t ' u ≠y' fu , and x t ' u =0, y' fu =-, then let x t ' u =0;
若xt'u≠y'fu，且xt'u＝1，y'fu＝-，则令xt”u＝1；If x t ' u ≠y' fu , and x t ' u =1, y' fu =-, then set x t ' u =1;
E.判断xt”u的值是否为NULL，如果xt”u的值为NULL，则直接令得到组合电路a的第t个乘积项at对组合电路b的第f个乘积项bf的余子式的表达式，然后进入步骤F；否则，判断u的当前值是否等于n，如果u的当前值等于n，则表明的第1位～第n位 文字变量全部赋值完成，将第1位～第n位文字变量全部赋值完成的的表达式作为组合电路a的第t个乘积项at对组合电路b的第f个乘积项bf的余 子式的表达式，然后进入步骤F，如果u的当前值不等于n，则采用u的当前值加1后的 值去更新u，然后重复步骤D和步骤E；E. Determine whether the value of x t " u is NULL, if the value of x t " u is NULL, directly make get the remainder of the tth product term a t of the combinational circuit a to the fth product term b f of the combinational circuit b expression, and then go to step F; otherwise, judge whether the current value of u is equal to n, if the current value of u is equal to n, it indicates The 1st to the nth literal variables of all assignments are completed, and the 1st to nth literal variables are all assigned values the expression of As the remainder of the tth product term a t of the combinational circuit a to the fth product b f of the combinational circuit b expression, and then enter step F, if the current value of u is not equal to n, use the current value of u plus 1 to update u, and then repeat steps D and E;
F.判断的第1位文字变量～第n位文字变量的值是否都为-，如果是，表明的值恒为1，则直接令af(x1,x2,…,xk,…,xn)＝1，得到组合电路a对组合电路b的第f个乘积项bf的余子函数af(x1,x2,…,xn)的表达式，然后进入步骤G，如果否，则判断t的当前值是否 等于p，如果等于，则令得到组合电路a对组合电 路b的第f个乘积项bf的余子函数af(x1,x2,…,xn)的表达式，然后进入步骤G，如果不等 于p，则采用t的当前值加1后的值去更新t，，并重复步骤D～步骤F；F. Judgment Whether the values of the 1st character variable to the nth character variable are all -, if yes, indicate is always 1, then directly set a f (x 1 ,x 2 ,…,x k ,…,x n )=1, and obtain the cosubfunction of the fth product term b f of combinational circuit a to combinational circuit b a f (x 1 ,x 2 ,…,x n ), then go to step G, if not, judge whether the current value of t is equal to p, if so, let Obtain the expression of the cosubfunction a f (x 1 ,x 2 ,…,x n ) of the f-th product term b f of the combinational circuit a to the combinational circuit b, then enter step G, if not equal to p, use t Add 1 to the current value of t to update t, and repeat steps D to F;
G.判定组合电路a对组合电路b的第f个乘积项bf的余子函数af(x1,x2,…,xn)的表达 式是否为重言式，具体过程为：G. Determine whether the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) of the combinatorial circuit a to the fth product term b f of the combinatorial circuit b is a tautology, the specific process is:
G-1.首先判断余子函数af(x1,x2,…,xn)的表达式的值是否为0，如果余子函数 af(x1,x2,…,xn)的表达式的值为0，则余子函数af(x1,x2,…,xn)的表达式不是重言式，组 合电路a不包含组合电路b，组合电路a和组合电路b不是逻辑等效关系，检测完成；如果 余子函数af(x1,x2,…,xn)的表达式的值不为0，则进入步骤G-2，对余子函数 af(x1,x2,…,xn)的表达式的值是否为1进行判断；G-1. First judge whether the value of the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is 0, if the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) The value of the formula is 0, then the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is not a tautology, the combinational circuit a does not contain the combinational circuit b, the combinational circuit a and the combinational circuit b are not logic, etc. If the value of the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is not 0, go to step G-2, for the cofactor function a f (x 1 ,x 2 ,...,x n ) to determine whether the value of the expression is 1;
G-2.如果余子函数af(x1,x2,…,xn)的表达式的值是1，则余子函数af(x1,x2,…,xn)的 表达式是重言式，进入步骤G-6，如果余子函数af(x1,x2,…,xn)的表达式的值不是1，则进入步骤G-3；G-2. If the value of the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is 1, then the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is Tautology, go to step G-6, if the value of the expression of the cofactor a f (x 1 ,x 2 ,…,x n ) is not 1, go to step G-3;
G-3.从余子式中随机选取一个未被选取过的不等于0的余子式，将其记为v为整数且1≤v≤p，从的表达式中随机选取一个不等于-的文字变量，将其记为 x'v's，s为大于等于1且小于等于n的整数，将x'v's对应的变量xs作为拆分变量，根据香农展开定理计算余子函数af(x1,x2,…,xn)的表达式对xs的原变量xs的余子式，将得到的余子 式记为根据香农展开定理计算余子函数af(x1,x2,…,xn)的表达式对xs的反变量的 余子式，将得到的余子式记为然后进入步骤G-4，判断是否是重言式；G-3. From the remainder formula Randomly select an unselected remainder not equal to 0, and record it as v is an integer and 1≤v≤p, from Randomly select a text variable not equal to - in the expression of , record it as x' v ' s , s is an integer greater than or equal to 1 and less than or equal to n, and take the variable x s corresponding to x' v ' s as the split variable, according to the Shannon expansion theorem to calculate the cofactor function a f (x 1 ,x 2 ,…,x n ) expression for the cofactor of the original variable x s of x s , and write the cofactor formula obtained as According to Shannon's expansion theorem, calculate the inverse variable of the expression of cosubfunction a f (x 1 ,x 2 ,…,x n ) to x s The remainder formula of , and the obtained remainder formula is denoted as Then go to step G-4, judge whether it is a tautology;
G-4.判断是否是重言式，具体为：如果的值为0，则不是重言式，组合电 路a不包含组合电路b，组合电路a和组合电路b不是逻辑等效关系，检测完成；如果的值不为0，则继续判断的值是否为1，如果的值不是1，则重复步骤G-3和步骤G-4；如果的值是1，则是重言式，进入步骤G-5；G-4. Judgment Whether it is a tautology, specifically: if is 0, then Not a tautology, the combinational circuit a does not contain the combinational circuit b, the combinational circuit a and the combinational circuit b are not logically equivalent, the detection is completed; if If the value is not 0, continue to judge Is the value of 1, if is not 1, repeat steps G-3 and G-4; if is 1, then is a tautology, go to step G-5;
G-5.采用判定是否为重言式的方法来判断是否是重言式，若不是重言式，则组合电路a不包含组合电路b，组合电路a和组合电路b不是逻辑等效关系，检测完成； 若是重言式，则表明af(x1,x2,…,xn)是重言式，进入步骤G-6；G-5. Adoption judgment Whether it is a tautology method to judge Is it a tautology, if is not a tautology, then the combinational circuit a does not contain the combinational circuit b, the combinational circuit a and the combinational circuit b are not logically equivalent, and the detection is completed; if is a tautology, it shows that a f (x 1 ,x 2 ,…,x n ) is a tautology, go to step G-6;
G-6.判断f的当前值是否为q，如果f的当前值不为q，则采用f的当前值加1后的值去更新f，然后重复步骤(2)的步骤B～步骤G，如果f的当前值为q，则表明组合电路a 包含组合电路b，进入步骤(3)；G-6. Determine whether the current value of f is q, if the current value of f is not q, then use the current value of f plus 1 to update f, and then repeat steps B to G of step (2), If the current value of f is q, it indicates that the combinational circuit a contains the combinational circuit b, and enter step (3);
(3)采用判定组合电路a是否包含组合电路b相同的方法来判定组合电路b是否包含 组合电路a，如果组合电路b包含组合电路a，则表明组合电路a和组合电路b是逻辑等效关系，如果组合电路b不包含组合电路a，则组合电路a和组合电路b不是逻辑等效关系， 检测完成。(3) Use the same method of judging whether the combinational circuit a includes the combinational circuit b to determine whether the combinational circuit b includes the combinational circuit a, if the combinational circuit b includes the combinational circuit a, it indicates that the combinational circuit a and the combinational circuit b are logically equivalent , if the combinational circuit b does not contain the combinational circuit a, then the combinational circuit a and the combinational circuit b are not logically equivalent, and the detection is completed.
与现有技术相比，本发明的优点在于通过扩展余子式概念，将逻辑覆盖等效性检测 问题分成分解成电路包含检测子问题,逐一求取其中一个电路表达式对另一个电路表达 式各乘积项的余子式，然后在建立各乘积项余子式的香农结构图基础上判断其是否重言 式，最后根据重言式判别结果确定两电路间是否覆盖等效关系，本发明的方法通过求取乘积项余子式对逻辑函数进行分解和降阶处理,从而加快了覆盖等效性验证速度，可 操作性和检测效率均较高，且不会出现内存爆炸问题，实验结构表明，本发明的方法稳 定有效的，对EXPRESSO软件集成的三种算法所得电路的测试结果表明,与基于真值表 和BDD的两种检测算法相比,具有明显的速度优势。Compared with the prior art, the present invention has the advantage that by extending the concept of the remainder formula, the logic coverage equivalence detection problem is decomposed into circuit inclusion detection sub-problems, and one by one obtains one circuit expression for another circuit expression. The cofactor of the product term, then judge whether it is a tautology on the basis of the Shannon structure diagram of each product covariant, and finally determine whether the equivalence relationship is covered between the two circuits according to the result of the tautology discrimination. The method of the present invention obtains Taking the remainder of the product term decomposes and reduces the order of the logic function, thereby speeding up the coverage equivalence verification speed, the operability and detection efficiency are high, and the problem of memory explosion will not occur. The experimental structure shows that the present invention The method is stable and effective. The test results of the circuit obtained by the three algorithms integrated in the EXPRESSO software show that it has obvious speed advantages compared with the two detection algorithms based on the truth table and BDD.
具体实施方式Detailed ways
以下结合实施例对本发明作进一步详细描述。Below in conjunction with embodiment the present invention is described in further detail.
实施例：一种组合逻辑电路等效性检测方法，包括以下步骤：Embodiment: a kind of combinatorial logic circuit equivalence detection method comprises the following steps:
(1)将待检测的两个组合电路记为a和b，其中，a的逻辑表达式为：(1) Record the two combined circuits to be detected as a and b, where the logical expression of a is:
b的逻辑表达式为：The logical expression of b is:
其中，n为组合电路a和b的变量数，∑为求和运算符号，p为组合电路a的乘积项的数量，q为组合电路b的乘积项的数量，ai为组合电路a的第i个乘积项，ai＝xi'1xi'2…xi'k…xi'n， k为大于等于1且小于等于n的整数，xi'k为乘积项ai第k位的文字变量，表示对应输入变量 xk在乘积项ai第k位的出现形式，xi'k∈{0,1,-}，当xi'k＝0时，xk以其反变量的形式出现 在乘积项ai第k位，当xi'k＝1时，xk以其原变量xk的形式出现在乘积项ai第k位，当xi'k＝- 时，表示xk的值恒为1，xk不出现在乘积项ai第k位中；bj为组合电路b的第j个乘积项， bj＝y'j1y'j2…y'jh…y'jn，h为大于等于1且小于等于n的整数，y'jh为乘积项bj第h位的文字 变量，表示对应输入变量yh在乘积项bj第h位的出现形式，y'jh∈{0,1,-}，当y'jh＝0时，yh以其反变量的形式出现在乘积项bj第h位，当y'jh＝1时，yh以其原变量yh的形式出现 在乘积项bj第h位，当y'jh＝-时，表示yh的值恒为1，yh不出现在乘积项bj第h位；Among them, n is the variable number of combinational circuits a and b, ∑ is the summation symbol, p is the number of product terms of combinational circuit a, q is the number of product terms of combinational circuit b, and a i is the number of product terms of combinational circuit a i product items, a i = x i ' 1 x i ' 2 ... x i ' k ... x i ' n , k is an integer greater than or equal to 1 and less than or equal to n, x i ' k is the kth product item a i The text variable of the bit, which represents the appearance form of the corresponding input variable x k in the kth bit of the product item a i , x i ' k ∈ {0,1,-}, when x i ' k = 0, x k is its inverse variable The form appears in the kth position of the product term a i , when xi ' k = 1, x k appears in the kth position of the product term a i in the form of its original variable x k , when xi ' k =-, Indicates that the value of x k is always 1, and x k does not appear in the kth bit of the product item a i ; b j is the jth product item of the combinational circuit b, b j =y' j1 y' j2 …y' jh … y' jn , h is an integer greater than or equal to 1 and less than or equal to n, y' jh is a text variable at the hth position of the product term b j , indicating the appearance form of the corresponding input variable y h at the hth position of the product term b j , y ' jh ∈{0,1,-}, when y' jh ＝0, y h takes its inverse variable appears in the hth position of the product term b j , when y' jh =1, y h appears in the hth position of the product term b j in the form of its original variable y h , when y' jh =-, it means y The value of h is always 1, and y h does not appear in the hth position of the product term b j ;
(2)判断组合电路a是否包含组合电路b，具体过程为：(2) Judging whether the combinational circuit a includes the combinational circuit b, the specific process is:
A.设定变量f，初始化变量f，令变量f＝1；A. Set variable f, initialize variable f, make variable f=1;
B.设定变量u，初始化变量u，令u＝1；设定变量t，初始化变量t，令变量t＝1；B. set variable u, initialize variable u, make u=1; set variable t, initialize variable t, make variable t=1;
C.将组合电路a对组合电路b的第f个乘积项bf的余子函数表示为af(x1,x2,…,xn)，将组合电路a的第t个乘积项at对组合电路b的第f个乘积项bf的余子式记为 C. Express the cosubfunction of the f-th product term b f of the combinational circuit a to the combinational circuit b as a f (x 1 ,x 2 ,…,x n ), and the t-th product term a t of the combinational circuit a The remainder of the fth product term b f of the combinational circuit b is written as
D.令xt”k为第k位的文字变量，表示对应输入变量xk在第k位的出现形式，xt”k∈{0,1,-,NULL}，当xt”k＝0时，xk以其反变量的形式出现在第k位， 当xt”k＝1时，xk以原变量其xk的形式出现在第k位，当xt”k＝-时，表示xk的值恒为1，xk不出现在第k位，当xt”k＝NULL时，表示xk的值恒为0；D. order x t ” k is The text variable at the kth position indicates that the corresponding input variable x k is in The appearance form of the kth bit, x t ” k ∈ {0,1,-,NULL}, when x t ” k = 0, x k takes its inverse variable in the form of At bit k, when x t ” k =1, x k appears in the form of x k of the original variable The kth bit, when x t ” k =-, means that the value of x k is always 1, and x k does not appear in The kth bit, when x t ” k = NULL, means that the value of x k is always 0;
按照以下规则依次对的第u位文字变量xt”u进行赋值：According to the following rules in order The u-th literal variable x t ” u is assigned:
若xt'u＝y'fu，则令xt”u＝-；If x t ' u =y' fu , then make x t ” u =-;
若xt'u≠y'fu，且xt'u＝-，y'fu＝0，则令xt”u＝-；If x t ' u ≠y' fu , and x t ' u ＝-, y' fu ＝0, then make x t ” u ＝-;
若xt'u≠y'fu，且xt'u＝-，y'fu＝1，则令xt”u＝-；If x t ' u ≠y' fu , and x t ' u ＝-, y' fu ＝1, then make x t ” u ＝-;
若xt'u≠y'fu，且xt'u＝0，y'fu＝1，则令xt”u＝NULL；If x t ' u ≠y' fu , and x t ' u =0, y' fu =1, then let x t ' u =NULL;
若xt'u≠y'fu，且xt'u＝1，y'fu＝0，则令xt”u＝NULL；If x t ' u ≠y' fu , and x t ' u = 1, y' fu = 0, then set x t ” u = NULL;
若xt'u≠y'fu，且xt'u＝0，y'fu＝-，则令xt”u＝0；If x t ' u ≠y' fu , and x t ' u =0, y' fu =-, then let x t ' u =0;
若xt'u≠y'fu，且xt'u＝1，y'fu＝-，则令xt”u＝1；If x t ' u ≠y' fu , and x t ' u =1, y' fu =-, then set x t ' u =1;
E.判断xt”u的值是否为NULL，如果xt”u的值为NULL，则直接令得到组合电路a的第t个乘积项at对组合电路b的第f个乘积项bf的余子式的表达式，然后进入步骤 F；否则，判断u的当前值是否等于n，如果u的当前值等于n，则表明的第1位～第n位 文字变量全部赋值完成，将第1位～第n位文字变量全部赋值完成的的表达式作为组合电路a的第t个乘积项at对组合电路b的第f个乘积项bf的余 子式的表达式，然后进入步骤F，如果u的当前值不等于n，则采用u的当前值加1后的 值去更新u，然后重复步骤D和步骤E；E. Determine whether the value of x t " u is NULL, if the value of x t " u is NULL, directly make get the remainder of the tth product term a t of the combinational circuit a to the fth product term b f of the combinational circuit b expression, and then go to step F; otherwise, judge whether the current value of u is equal to n, if the current value of u is equal to n, it indicates The 1st to the nth literal variables of all assignments are completed, and the 1st to nth literal variables are all assigned values the expression of As the remainder of the tth product term a t of the combinational circuit a to the fth product b f of the combinational circuit b expression, and then enter step F, if the current value of u is not equal to n, use the current value of u plus 1 to update u, and then repeat steps D and E;
F.判断的第1位文字变量～第n位文字变量的值是否都为-，如果是，表明的值恒为1，则直接令af(x1,x2,…,xk,…,xn)＝1，得到组合电路a对组合电路b的第f个乘积项bf的余子函数af(x1,x2,…,xn)的表达式，然后进入步骤G，如果否，则判断t的当前值是否 等于p，如果等于，则令得到组合电路a对组合电 路b的第f个乘积项bf的余子函数af(x1,x2,…,xn)的表达式，然后进入步骤G，如果不等 于p，则采用t的当前值加1后的值去更新t，，并重复步骤D～步骤F；F. Judgment Whether the values of the 1st character variable to the nth character variable are all -, if yes, indicate is always 1, then directly set a f (x 1 ,x 2 ,…,x k ,…,x n )=1, and obtain the cosubfunction of the fth product term b f of combinational circuit a to combinational circuit b a f (x 1 ,x 2 ,…,x n ), then go to step G, if not, judge whether the current value of t is equal to p, if so, let Obtain the expression of the cosubfunction a f (x 1 ,x 2 ,…,x n ) of the f-th product term b f of the combinational circuit a to the combinational circuit b, then enter step G, if not equal to p, use t Add 1 to the current value of t to update t, and repeat steps D to F;
G.判定组合电路a对组合电路b的第f个乘积项bf的余子函数af(x1,x2,…,xn)的表达 式是否为重言式，具体过程为：G. Determine whether the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) of the combinatorial circuit a to the fth product term b f of the combinatorial circuit b is a tautology, the specific process is:
G-1.首先判断余子函数af(x1,x2,…,xn)的表达式的值是否为0，如果余子函数 af(x1,x2,…,xn)的表达式的值为0，则余子函数af(x1,x2,…,xn)的表达式不是重言式，组 合电路a不包含组合电路b，组合电路a和组合电路b不是逻辑等效关系，检测完成；如果 余子函数af(x1,x2,…,xn)的表达式的值不为0，则进入步骤G-2，对余子函数 af(x1,x2,…,xn)的表达式的值是否为1进行判断；G-1. First judge whether the value of the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is 0, if the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) The value of the formula is 0, then the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is not a tautology, the combinational circuit a does not contain the combinational circuit b, the combinational circuit a and the combinational circuit b are not logic, etc. If the value of the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is not 0, go to step G-2, for the cofactor function a f (x 1 ,x 2 ,...,x n ) to determine whether the value of the expression is 1;
G-2.如果余子函数af(x1,x2,…,xn)的表达式的值是1，则余子函数af(x1,x2,…,xn)的 表达式是重言式，进入步骤G-6，如果余子函数af(x1,x2,…,xn)的表达式的值不是1，则进入步骤G-3；G-2. If the value of the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is 1, then the expression of the cofactor function a f (x 1 ,x 2 ,…,x n ) is Tautology, go to step G-6, if the value of the expression of the cofactor a f (x 1 ,x 2 ,…,x n ) is not 1, go to step G-3;
G-3.从余子式中随机选取一个未被选取过的不等于0的余子式，将其记为v为整数且1≤v≤p，从的表达式中随机选取一个不等于-的文字变量，将其记为 x'v's，s为大于等于1且小于等于n的整数，将x'v's对应的变量xs作为拆分变量，根据香农展开定理计算余子函数af(x1,x2,…,xn)的表达式对xs的原变量xs的余子式，将得到的余子 式记为根据香农展开定理计算余子函数af(x1,x2,…,xn)的表达式对xs的反变量的 余子式，将得到的余子式记为然后进入步骤G-4，判断是否是重言式；G-3. From the remainder formula Randomly select an unselected remainder not equal to 0, and record it as v is an integer and 1≤v≤p, from Randomly select a text variable not equal to - in the expression of , record it as x' v ' s , s is an integer greater than or equal to 1 and less than or equal to n, and take the variable x s corresponding to x' v ' s as the split variable, according to the Shannon expansion theorem to calculate the cofactor function a f (x 1 ,x 2 ,…,x n ) expression for the cofactor of the original variable x s of x s , and write the cofactor formula obtained as According to Shannon's expansion theorem, calculate the inverse variable of the expression of cosubfunction a f (x 1 ,x 2 ,…,x n ) to x s The remainder formula of , and the obtained remainder formula is denoted as Then go to step G-4, judge whether it is a tautology;
G-4.判断是否是重言式，具体为：如果的值为0，则不是重言式，组合电 路a不包含组合电路b，组合电路a和组合电路b不是逻辑等效关系，检测完成；如果的值不为0，则继续判断的值是否为1，如果的值不是1，则重复步骤G-3和步骤 G-4；如果的值是1，则是重言式，进入步骤G-5；G-4. Judgment Whether it is a tautology, specifically: if is 0, then Not a tautology, the combinational circuit a does not contain the combinational circuit b, the combinational circuit a and the combinational circuit b are not logically equivalent, the detection is completed; if If the value is not 0, continue to judge Is the value of 1, if is not 1, repeat steps G-3 and G-4; if is 1, then is a tautology, go to step G-5;
G-5.采用判定是否为重言式的方法来判断是否是重言式，若不是重言式，则组合电路a不包含组合电路b，组合电路a和组合电路b不是逻辑等效关系，检测完成； 若是重言式，则表明af(x1,x2,…,xn)是重言式，进入步骤G-6；G-5. Adoption judgment Whether it is a tautology method to judge Is it a tautology, if is not a tautology, then the combinational circuit a does not contain the combinational circuit b, the combinational circuit a and the combinational circuit b are not logically equivalent, and the detection is completed; if is a tautology, it shows that a f (x 1 ,x 2 ,…,x n ) is a tautology, go to step G-6;
G-6.判断f的当前值是否为q，如果f的当前值不为q，则采用f的当前值加1后的值去更新f，然后重复步骤(2)的步骤B～步骤G，如果f的当前值为q，则表明组合电路a 包含组合电路b，进入步骤(3)；G-6. Determine whether the current value of f is q, if the current value of f is not q, then use the current value of f plus 1 to update f, and then repeat steps B to G of step (2), If the current value of f is q, it indicates that the combinational circuit a contains the combinational circuit b, and enter step (3);
(3)采用判定组合电路a是否包含组合电路b相同的方法来判定组合电路b是否包含 组合电路a，如果组合电路b包含组合电路a，则表明组合电路a和组合电路b是逻辑等效关系，如果组合电路b不包含组合电路a，则组合电路a和组合电路b不是逻辑等效关系， 检测完成。(3) Use the same method of judging whether the combinational circuit a includes the combinational circuit b to determine whether the combinational circuit b includes the combinational circuit a, if the combinational circuit b includes the combinational circuit a, it indicates that the combinational circuit a and the combinational circuit b are logically equivalent , if the combinational circuit b does not contain the combinational circuit a, then the combinational circuit a and the combinational circuit b are not logically equivalent, and the detection is completed.
本发明的方法在PentiumⅣ1.60GHz,1.00GB内存的Windows XP环境下,采用C 语言编程实现，并通过VC6.0进行编译和调试。测试包括有效性测试和效率测试：1)采 用输入变量数不大于4的多个单输出电路测试算法有效性，利用卡诺图优化原电路表达 式，将优化前后的表达式均写成标准的BLIF文件作为算法的测试电路对；测试结果表 明：每对测试电路均为覆盖等效的；2)测试前通过以下一种或多种方式修改测试电 路:随机改变若干乘积项的若干位变量取值、删除或添加若干行ONSET项或无关项， 测试结果与预期结果均相符合；3)采用ESPRESSO软件集成的本发明的方法和现有 的两种优化算法优化不同规模的MCNC Benchmark电路，由原电路分别与不同优化算 法所得电路组成测试电路对,继续测试本发明的有效性，同时观察算法的效率。表1所 示为12个测试电路的简要信息,包括电路名称、输入/输出数量、原始电路乘积项数量 以及三种算法优化结果电路的乘积项数量；Esp1代表最优化算法优化结果电路、Esp2 代表ESPRESSO算法优化结果电路，Esp3代表快速ESPRESSO算法优化结果电路。The method of the present invention is realized by programming in C language under the Windows XP environment of Pentium Ⅳ 1.60GHz and 1.00GB memory, and compiling and debugging through VC6.0. The test includes validity test and efficiency test: 1) Use multiple single-output circuits with input variables not greater than 4 to test the validity of the algorithm, use Karnaugh map to optimize the original circuit expression, and write the expressions before and after optimization as standard BLIF The file is used as the test circuit pair of the algorithm; the test results show that each pair of test circuits is equivalent in coverage; 2) the test circuit is modified by one or more of the following methods before the test: randomly changing the values of some bit variables of several product items , delete or add some rows of ONSET items or unrelated items, and the test results are consistent with the expected results; 3) adopt the method of the present invention integrated by ESPRESSO software and existing two optimization algorithms to optimize the MCNC Benchmark circuits of different scales, by the original The circuits respectively form test circuit pairs with the circuits obtained by different optimization algorithms, continue to test the effectiveness of the present invention, and observe the efficiency of the algorithms at the same time. Table 1 shows the brief information of the 12 test circuits, including the circuit name, input/output quantity, the number of product items of the original circuit, and the number of product items of the circuit optimized by the three algorithms; Esp1 represents the circuit optimized by the optimization algorithm, and Esp2 represents the circuit ESPRESSO algorithm optimization result circuit, Esp3 represents fast ESPRESSO algorithm optimization result circuit.
表1ESPRESSO优化前后Table 1 Before and after ESPRESSO optimization
12个MCNC Benchmark电路的乘积项数Number of product terms for 12 MCNC Benchmark circuits
为便于比较本发明的方法与现有的方法的有效性和效率；采用以上测试电路对分别 测试基于真值表的等效性检测算法(简称真值表法)、基于BDD的等效性检测算法(简称BDD法)和本发明的方法。其中，真值表法在相同环境下采用C语言编程,在实现基于 真值表的重言式判定算法基础上进一步实现；BDD法采用文献(Somenzi F.CUDD:CU decisiondiagram package release 3.0.0[OL].[2015-12-31]. http://vlsi.colorado.edu/～fabio/CUDD/cudd.pdf)公开的CUDD中的组合电路等价性检验 算法，该算法将测试电路对分别构建最优输入变量顺序下的OBDD，然后对每个输出的 等效节点逐一比较。当所有的输出节点都确认等效时，判定测试电路对等效。三种等 效性检测算法结果均表明：以上测试电路对都满足覆盖等效关系。该一致性结论也同时 表明本发明的方法的有效性。表2所示为相应检测过程的运行时间及比较情况,均为5 次运行时间的平均值.其中；tTr、tBDD和tOur分别为真值表法、BDD法和本发明方法测 试对应电路对所用的时间；S1为本发明相比真值表法的时间节省百分比，S2为本发明相 比BDD法的时间节省百分比。For the convenience of comparison method of the present invention and the effectiveness and efficiency of existing methods; Adopt above test circuit to test respectively the equivalence detection algorithm (abbreviation truth table method) based on truth table, the equivalence detection based on BDD Algorithm (abbreviated BDD method) and the method of the present invention. Among them, the truth table method uses C language programming in the same environment, and is further realized on the basis of realizing the tautology decision algorithm based on the truth table; the BDD method adopts the literature (Somenzi F. OL].[2015-12-31]. http://vlsi.colorado.edu/～fabio/CUDD/cudd.pdf) discloses the combinational circuit equivalence test algorithm in CUDD, the algorithm will test the circuit pair respectively Construct the OBDD under the optimal input variable order, and then compare the equivalent nodes of each output one by one. When all output nodes confirm equivalence, it is determined that the test circuit is equivalent. The results of the three equivalence detection algorithms all show that the above test circuit pairs all satisfy the coverage equivalence relation. The consistent conclusion also shows the effectiveness of the method of the present invention. Table 2 shows the running time and comparative situation of the corresponding detection process, which are the average value of 5 running times . Wherein ; The time used by the circuit pair; S 1 is the time saving percentage of the present invention compared with the truth table method, and S 2 is the time saving percentage of the present invention compared with the BDD method.
表2 12个MCNC Benchmark电路优化前后用3种算法进行等效性测试所需时间Table 2 The time required for equivalence testing with 3 algorithms before and after optimization of 12 MCNC Benchmark circuits
从表2可以看出：1)显然，随着输入变量数量增长，真值表法所需时间显著增长，本发明方法和BDD法运行时间与输入变量数量没有明显的关系；2)乘积项数量对本发 明方法和真值表法速度影响明显，对BDD法影响相对较小，例如电路cordic和duke2 输入变量数仅相差1，前者乘积项数是后者的10倍以上，真值表法对前者不同测试对的 运行时间均是后者的10倍以上，本发明方法对cordic电路对的测试时间则是duke2的 50倍以上，而BDD法对cordic电路的测试时间反而减少为duke2的近十分之一，另外 seq,cordic和alu4电路的乘积项数相对最多,本发明方法对这3个电路的测试时间相比 其他电路更多,也说明乘积项数是本文算法效率的最重要影响因素；3)电路输出数量对 BDD法测试时间影响最大,对真值表法和本发明方法影响相对较小，这个结论通过比较 cps,seq,duke2等电路的测试时间容易得到；4)就三种方法法的整体运行效率而言，真 值表法效率最低，但当输入变量和乘积项数量较少时仍具有相对较高的运行效率，当电 路具有输出量少、输入量和乘积项较多时,如seq和cordic电路，BDD法速度最快，对 于输入和输出量较多、乘积项数量相对较少的电路，适合采用本发明方法进行测试.就 所涉及测试电路而言,本发明方法平均效率最高,相比真值表法和BDD法的时间平均 节省率均超过60％。As can be seen from Table 2: 1) obviously, along with the increase of the input variable quantity, the required time of the truth table method increases significantly, and the running time of the inventive method and the BDD method has no obvious relationship with the input variable quantity; 2) the product term quantity The method of the present invention and the speed of the truth table method are significantly affected, and the impact on the BDD method is relatively small. For example, the number of input variables of the circuit cordic and duke2 only differs by 1, and the number of product items of the former is more than 10 times that of the latter. The running time of different test pairs is more than 10 times of the latter, the test time of the inventive method to the cordic circuit is then more than 50 times of duke2, and the test time of the BDD method to the cordic circuit is reduced to nearly ten times of duke2 on the contrary. One, in addition seq, cordic and alu4 circuits have the largest number of product terms, and the method of the present invention has more testing time for these 3 circuits than other circuits, which also shows that the number of product terms is the most important factor affecting the efficiency of this paper's algorithm; 3) The number of circuit outputs has the greatest impact on the test time of the BDD method, and relatively little impact on the truth table method and the method of the present invention. This conclusion is easily obtained by comparing the test times of circuits such as cps, seq, and duke2; 4) with regard to three methods In terms of the overall operating efficiency of the method, the truth table method has the lowest efficiency, but it still has relatively high operating efficiency when the number of input variables and product terms is small. Such as seq and cordic circuits, the BDD method is the fastest, and for circuits with relatively few input and output quantities and relatively few product items, the method of the present invention is suitable for testing. With regard to the test circuits involved, the average efficiency of the method of the present invention is The highest, compared with the truth table method and BDD method, the average time saving rate is more than 60%.
Claims (1)
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201711136173.6A CN107798203B (en) | 2017-11-16 | 2017-11-16 | A Combination Logic Circuit Equivalence Detection Method |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201711136173.6A CN107798203B (en) | 2017-11-16 | 2017-11-16 | A Combination Logic Circuit Equivalence Detection Method |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN107798203A true CN107798203A (en) | 2018-03-13 |
| CN107798203B CN107798203B (en) | 2019-07-26 |
Family
ID=61536181
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN201711136173.6A Active CN107798203B (en) | 2017-11-16 | 2017-11-16 | A Combination Logic Circuit Equivalence Detection Method |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN107798203B (en) |
Cited By (3)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN109188825A (en) * | 2018-10-09 | 2019-01-11 | 宁波大学 | Optics half adder based on graphene surface plasmon |
| CN111797588A (en) * | 2020-07-03 | 2020-10-20 | 国微集团(深圳)有限公司 | Formal verification comparison point matching method, system, processor and memory |
| CN119476148A (en) * | 2024-10-31 | 2025-02-18 | 同济大学 | A TB-RM circuit logic detection method, storage medium and device |
Citations (6)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US6611947B1 (en) * | 2000-08-23 | 2003-08-26 | Jasper Design Automation, Inc. | Method for determining the functional equivalence between two circuit models in a distributed computing environment |
| US6993730B1 (en) * | 2001-01-10 | 2006-01-31 | Tempus Fugit, Inc. | Method for rapidly determining the functional equivalence between two circuit models |
| US7890901B2 (en) * | 2006-03-24 | 2011-02-15 | International Business Machines Corporation | Method and system for verifying the equivalence of digital circuits |
| CN103258079A (en) * | 2013-04-08 | 2013-08-21 | 宁波大学 | Equivalent function test method for digital combined logic circuits |
| CN104133931A (en) * | 2013-05-02 | 2014-11-05 | 国际商业机器公司 | Method and system for detecting corresponding paths in combinationally equivalent circuit designs |
| CN106997408A (en) * | 2016-01-22 | 2017-08-01 | 奇捷科技股份有限公司 | Circuit verification |
-
2017
- 2017-11-16 CN CN201711136173.6A patent/CN107798203B/en active Active
Patent Citations (6)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US6611947B1 (en) * | 2000-08-23 | 2003-08-26 | Jasper Design Automation, Inc. | Method for determining the functional equivalence between two circuit models in a distributed computing environment |
| US6993730B1 (en) * | 2001-01-10 | 2006-01-31 | Tempus Fugit, Inc. | Method for rapidly determining the functional equivalence between two circuit models |
| US7890901B2 (en) * | 2006-03-24 | 2011-02-15 | International Business Machines Corporation | Method and system for verifying the equivalence of digital circuits |
| CN103258079A (en) * | 2013-04-08 | 2013-08-21 | 宁波大学 | Equivalent function test method for digital combined logic circuits |
| CN104133931A (en) * | 2013-05-02 | 2014-11-05 | 国际商业机器公司 | Method and system for detecting corresponding paths in combinationally equivalent circuit designs |
| CN106997408A (en) * | 2016-01-22 | 2017-08-01 | 奇捷科技股份有限公司 | Circuit verification |
Non-Patent Citations (6)
| Title |
|---|
| Y. MATSUNAGA: ""An efficient equivalence checker for combinational circuits"", 《33RD DESIGN AUTOMATION CONFERENCE PROCEEDINGS, 1996》 * |
| YUAN YUE等: ""An Equivalence Checking Method for Circuits with Black Boxes Based on Logic Cone and SAT"", 《2010 INTERNATIONAL CONFERENCE ON MANAGEMENT AND SERVICE SCIENCE》 * |
| 曾琼 等: ""组合电路等价性检验方法研究"", 《计算机工程》 * |
| 曾琼: ""基于递归学习的组合电路等价性检验方法研究"", 《成都信息工程学院学报》 * |
| 李光辉 等: ""基于BDD的组合电路等价性检验方法"", 《微电子学与计算机》 * |
| 郑飞君 等: ""使用布尔可满足性的组合电路等价性验证算法"", 《电子与信息学报》 * |
Cited By (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN109188825A (en) * | 2018-10-09 | 2019-01-11 | 宁波大学 | Optics half adder based on graphene surface plasmon |
| CN111797588A (en) * | 2020-07-03 | 2020-10-20 | 国微集团(深圳)有限公司 | Formal verification comparison point matching method, system, processor and memory |
| WO2022000576A1 (en) * | 2020-07-03 | 2022-01-06 | 国微集团(深圳)有限公司 | Formal verification comparison point matching method and system, processor, and memory |
| CN119476148A (en) * | 2024-10-31 | 2025-02-18 | 同济大学 | A TB-RM circuit logic detection method, storage medium and device |
Also Published As
| Publication number | Publication date |
|---|---|
| CN107798203B (en) | 2019-07-26 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Kunz et al. | Reasoning in Boolean Networks: logic synthesis and verification using testing techniques | |
| CN112257366B (en) | CNF generation method and system for equivalence verification | |
| US20050240885A1 (en) | Efficient SAT-based unbounded symbolic model checking | |
| CN107798203A (en) | A kind of combinational logic circuit equivalence detection method | |
| Kunz et al. | Logic optimization and equivalence checking by implication analysis | |
| US9965575B2 (en) | Methods and systems for correcting X-pessimism in gate-level simulation or emulation | |
| WO2022103668A1 (en) | Faster coverage convergence with automatic test parameter tuning in constrained random verification | |
| Lakshmi et al. | A study on classifying imbalanced datasets | |
| CN102226947B (en) | Controllable test vector generator based on linear feedback shift register | |
| CN104809233A (en) | Attribute weighting method based on information gain ratios and text classification methods | |
| CN115952754B (en) | Data processing system for generating standard cell target display structure | |
| Hattori et al. | Mapping a quantum circuit to 2D nearest neighbor architecture by changing the gate order | |
| Huang et al. | A hardware trojan trigger localization method in RTL based on control flow features | |
| Jayanthy et al. | Simulation–based ATPG for low power testing of crosstalk delay faults in asynchronous circuits | |
| Krstic et al. | Primitive delay faults: Identification, testing, and design for testability | |
| Dobai et al. | SAT-based generation of compressed skewed-load tests for transition delay faults | |
| Nandha Kumar et al. | Single‐configuration fault detection in application‐dependent testing of field programmable gate array interconnects | |
| Mondal et al. | Boolean difference technique for detecting all missing gate faults in reversible circuits | |
| Hromkovič et al. | Ambiguity and communication | |
| Shirinzadeh et al. | A Comprehensive Synthesis and Verification Approach for RRAM-Based Neuromorphic Computing | |
| Sharma et al. | Implementation of BDDs by various techniques in Low power VLSI design | |
| Das et al. | Fault-detection experiments for parallel-decomposable sequential machines | |
| US9489338B1 (en) | Systolic array based architecture for branch and bound algorithms | |
| Su et al. | Formal verification of constrained arithmetic circuits using computer algebraic approach | |
| CN111177713B (en) | XGBoost-based hardware Trojan detection method and device |
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 | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant | ||
| TR01 | Transfer of patent right | ||
| TR01 | Transfer of patent right |
Effective date of registration: 20250718 Address after: B205, No.179 Chezhan Road, Liushi Town, Leqing City, Wenzhou City, Zhejiang Province, 325600 Patentee after: Zhipu Qiwang (Wenzhou) Electric Power Technology Research Institute Co.,Ltd. Country or region after: China Address before: 315211 Zhejiang Province, Ningbo Jiangbei District Fenghua Road No. 818 Patentee before: Ningbo University Country or region before: China |