JP3394888B2 - Logic circuit verification device, logic circuit verification method, and computer-readable recording medium storing logic circuit verification program - Google Patents

Description

Detailed Description of the Invention

[0001]

BACKGROUND OF THE INVENTION 1. Field of the Invention The present invention relates to automation of logic circuit design of an LSI using a computer, and more particularly to logic circuit verification for verifying whether or not a logic circuit is properly designed.

[0002]

2. Description of the Related Art In the design of an LSI logic circuit, a simulator is used to determine (verify) the equivalence of logic or function of two logic circuits designed to have the same logic or function but different circuit structures. Is done using. However, when using a simulator, the input pattern 0,
Since there are 2 ⁿ combinations of 1 (n is the number of inputs), there is a problem that the calculation takes time when the number of inputs is large.

Therefore, a logic circuit verification device is used as a tool for determining the equivalence of logic or function of two logic circuits. FIG. 13 is a circuit configuration diagram showing an example of a logical equivalence determination circuit generated by a conventional logic circuit verification device. The logic circuit verification device inputs two logic circuits to be verified, generates an equivalence judgment circuit as shown in FIG. 13, and outputs an output out_check when a combination pattern of 0 and 1 is given to inputs I1 and I2. Circuit 11 and circuit 12 to be verified depending on whether or not the value of is always 1.
, Are logically equivalent. here,
Whether or not the output is always 1 is determined by converting the function of the logic circuit into a logic function. In this form of expression,
A graph function called a BDD (Binary Decision Diagram) described later (which has the same expression form as long as it is logically equivalent even if the logical structures are different) is generally used.

In the judgment by such a logical function,
When the don't care condition is defined for the output terminal and the register input, it is determined whether or not they are functionally equivalent as follows. For example, in FIG. 13, the output terminal out1 of the circuit 11 is out11 and the output terminal o of the circuit 12 is o.
Let ut1 be out12 and the don't care function at the output terminal out1 be dc_out1. Where (ou
t11 ex-norout12) or dc_out
Equivalence of logic or function can be determined by checking whether 1 is always 1.

The don't care condition is expressed by a logical expression or a logical circuit in which the output terminal of the logical circuit and the value of the register are not related to the operation result regardless of the values. For example, as shown in FIG. 14A, a circuit in which outputs (data 1, data 2) of registers (Reg) 1 and 2 are calculated by an ALU (arithmetic unit) 3 and output to a register 4 will be described. . In the figure, A
Assuming that the control signals I0 and I1 to the LU3 are given as shown in (b) of the figure, when I0 and I1 are (0,0) or (0,1), the ALU3 outputs from the registers 1 and 2 respectively. Although + or-operation is performed on the data, I0,
When I1 is (1,0), data 1 is shifted and data 2 is not used. When I0 and I1 are (1, 1), neither data 1 nor data 2 is used. When I0 and I1 are (1, 0) and (1, 1), the data 2 is in a don't care state, that is, the data is not referenced. In this way, when the combination of input values is don't care, even if the outputs of the registers do not match, they are considered to be equivalent. That is, when the don't care condition is defined, it is determined whether it is functionally equivalent, not logically equivalent.

[0006]

The above-described logic circuit verification device is also used in the case of determining the equivalence of a logic circuit having a gated clock design. 15A and 15B show an example of a case where a certain partial circuit is designed by a gated clock. FIG. 15A shows a partial circuit which is not designed by the gated clock, and FIG. 15B is a partial circuit which is designed by the gated clock. Are shown respectively. Figure 15
In the partial circuit of (a), data (D) is captured at the rising edge of the clock signal (clk) input from the clock input port (CK) of the register (Reg) 13. Here, the data D is controlled by the enable logic output ena input to the multiplexer (MUX) 14,
It is given according to a * data + ena (NOT) * out. That is, when ena is 1, data is input to the D port, and when ena is 0, feedback from the register 13 is input to the D port.

On the other hand, in the partial circuit of FIG.
The data D is controlled by the enable logic output ena input to the AND gate 15, and is taken into the register 13 at the timing when ena * clk is established.

In the gated clock design, a logic circuit is added to the clock input port (CK) of the register 13 as shown in FIG. 15, and the two partial circuits shown in FIG. 15 are functionally equivalent. However, since the conventional logic circuit verification device cannot determine the logical or functional equivalence of these two partial circuits, it has been determined that they are not equivalent.

The present invention has been made to solve the above problems, and a logic circuit verification device and a logic circuit verification method capable of correctly determining the logical or functional equivalence of a gated clock designed logic circuit. And a computer-readable recording medium storing a logic circuit verification program.

[0010]

In order to achieve the above object, the invention of claim 1 is a circuit information input means for inputting information on at least two logic circuits to be verified and don't care information on the logic circuits. An equivalence judgment circuit generating means for generating an equivalence judgment circuit including the at least two logic circuits based on information about the logic circuit and don't care information about the logic circuit, and a gated clock design for the equivalence judgment circuit . Logic circuit
If included, it is included in the at least two logic circuits.
So that the clock inputs of the registers
Gated clock Multiplied to the designed logic circuit.
A gated clock partial correction means for inserting a lexer to correct the equivalence judgment circuit, and an equivalence judgment circuit generated by the equivalence judgment circuit generation means or an equivalence judgment corrected by the gated clock partial correction means. A logic circuit verification device comprising equivalence determining means for determining equivalence of logic or function of at least two logic circuits to be verified based on a circuit.

The equivalence judging circuit generating means and the gated clock partial correcting means can be constructed as follows.

When there is no don't care information regarding the logic circuit to be verified when generating the equivalence judgment circuit, the equivalence judgment circuit generation means generates an equivalence judgment circuit for judging the logic equivalence. If there is don't care information regarding the logic circuit to be verified, an equivalence judgment circuit for judging equivalence of functions is generated.

The gated clock partial correction means, when correcting the equivalence judgment circuit, generates a multiplexer for selecting data loading and data holding for the register of the logic circuit to be corrected, and uses the selection logic of the multiplexer as the selection logic. Modify the circuit to use clock enable logic.

When changing the circuit, the gated clock partial correction means changes the circuit by referring to the additional information regarding the gated clock design.

[0015]

According to a second aspect of the invention, there is provided circuit information input means,
Equivalence determination circuit generation means and gated clock partial modification
Logic circuit verification device including corrective means and equivalence judgment means
Of the logic or function of at least two logic circuits
A logic circuit verification method for determining equivalence, comprising:
The information input means has at least two logic circuits to be verified.
Information and don't care information about the logic circuit
Circuit information input step for inputting, and the equivalence determination circuit
The generating means stores information about the logic circuit and the logic circuit
Based on the don't care information about
Equivalence judgment to generate an equivalence judgment circuit including all logic circuits
Circuit generation step and partial correction of the gated clock
Means for designing a gated clock in the equivalence determination circuit
At least one of the above is included.
The clock inputs of the registers included in the two logic circuits are equal
The gated clock is designed to be
Insert a multiplexer into the logic circuit
Gated clock partial correction step to correct constant circuit
And the equivalence judging means generates the equivalence judging circuit generation step.
Equivalence determination circuit generated by step or the gated
Equivalence judgment circuit modified by the clock partial modification step
Of at least two logic circuits to be verified based on
Equivalence judgment step for judging equivalence of
It is characterized by including.

The equivalence judgment circuit generation step and the gated clock partial correction step may include the following processing.

In the equivalence judgment circuit generating step, when there is no don't care information regarding the logic circuit to be verified when the equivalence judgment circuit is generated, an equivalence judgment circuit for judging logic equivalence is generated, When there is don't care information regarding the logic circuit to be verified, an equivalence judgment circuit for judging equivalence of functions is generated.

The gated clock partial correction step is
When modifying the equivalence determination circuit, a multiplexer is generated which performs data loading and data holding selection for the register of the logic circuit to be modified, and the circuit is configured to use the clock enable logic for the selection logic of the multiplexer. change.

In the gated clock partial correction step, when the circuit is changed, the circuit is changed by referring to the additional information regarding the gated clock design.

[0021]

The invention of claim 3 is at least to be verified.
Information about two logic circuits and information about the logic circuits
Circuit information input step of inputting care information, and
Information about a logic circuit and don't care about the logic circuit
Based on information, including said at least two logic circuits
Equivalence judgment circuit generation step for generating equivalence judgment circuit
And a gated clock is designed in the equivalence judgment circuit.
At least two of the above logic circuits are included.
The clock inputs of the registers included in the
The theory that the gated clock is designed to be
Insert a multiplexer into the logic circuit to
Gated clock partial correction step to correct the path,
The equivalence judgment generated in the equivalence judgment circuit generation step
In the constant circuit or the gated clock partial correction step
Based on the modified equivalence decision circuit,
Determine equivalence of logic or function of at least two logic circuits
And the equivalence determination step
Computer, which is characterized by being executed by a computer.
A computer-readable recording medium storing a program
It is the body.

The equivalence judgment circuit generation step and the gated clock partial correction step may include the following processing.

The equivalence judging circuit generating step judges the presence / absence of don't care information about the logic circuit to be verified, and if it is judged that there is no don't care information about the logic circuit to be verified, the equivalence of the logic is judged. A process of generating an equivalence determination circuit for determining and a process of generating an equivalence determination circuit for determining functional equivalence when it is determined that there is don't care information regarding the logic circuit to be verified.

The gated clock partial correction step is
A process of generating a multiplexer that performs data loading and data holding selection for the register of the logic circuit to be modified, and a process of changing the circuit so that the clock enable logic is used as the selection logic of the multiplexer.

In the gated clock partial correction step, the circuit is changed by referring to the additional information regarding the gated clock design.

[0027]

BEST MODE FOR CARRYING OUT THE INVENTION An embodiment of a logic circuit verification device, a logic circuit verification method, and a computer-readable recording medium storing a logic circuit verification program according to the present invention will be described below.

FIG. 1 is a block diagram showing the functional configuration of the logic circuit verification device according to this embodiment. The logic circuit verification device 10 includes a circuit information input unit 1, a don't care information input unit 2, an equivalence judgment circuit generation unit 3, an equivalence judgment circuit storage unit 4, a gated clock information input unit 5, a gated clock partial correction unit 6, It is composed of an equivalence determination unit 7.

The circuit information input unit 1 inputs information about two logic circuits whose logical or functional equivalents are to be verified, and transfers the information to the equivalence judgment circuit generation unit 3.

The don't care information input unit 2 inputs the don't care information about the two logic circuits input from the circuit information input unit 1 and transfers it to the equivalence judgment circuit generation unit 3.

The equivalence judgment circuit generator 3 receives the input 2
Determines the presence or absence of don't care information for one logic circuit,
When there is no don't care information, an equivalence determination circuit for determining logic equivalence is generated based on the information about the two logic circuits. When there is don't care information, an equivalence judgment circuit for judging the equivalence of functions is generated based on the information on the two logic circuits and the don't care information on these logic circuits.

The equivalence judgment circuit storage unit 4 stores the circuit data of the equivalence judgment circuit generated by the equivalence judgment circuit generation unit 3 and the equivalence judgment circuit corrected by the gated clock partial correction unit 5 described later. The circuit data of is stored.

The gated clock information input unit 5 inputs additional information related to the gated clock design and transfers it to the gated clock partial correction unit 6. The additional information about the gated clock design is information about the characteristic configuration of the gated clock part when the gated clock is designed. Is referred to.

For example, in a second embodiment described later, information that the flip-flop added by the gated clock design is inserted to remove the glitch in the clock enable logic is input as the additional information about the gated clock design. Therefore, the gated clock partial correction unit 6 removes the flip-flop as a part unrelated to the equivalence judgment based on this information when correcting the part for which the gated clock is designed.

The gated clock partial correction section 6 determines whether or not a partial circuit (logical circuit) included in the equivalence judgment circuit generated by the equivalence judgment circuit generation section 3 is designed as a gated clock and the CK port of the register. Judgment is made based on whether the input has a gate such as AND or OR. When the gated clock is designed, the generated equivalence determination circuit is configured so that the clock inputs of the registers of the two logic circuits become equal while referring to additional information regarding the gated clock design as necessary. Fix the designed part of the gated clock.

Here, in order to correct the gated clock designed portion, a multiplexer for selecting data load and data retention for the register of the logic circuit to be corrected is generated, and a clock enable is applied to the selection logic of this multiplexer. I am trying to change the circuit to use logic. The corrected equivalence determination circuit is stored in the equivalence determination circuit storage unit 4.

At least the equivalence judgment unit 7 should be verified based on the equivalence judgment circuit generated by the equivalence judgment circuit generation unit 3 or the equivalence judgment circuit corrected by the gated clock partial correction unit 6. Determine equivalence of logic or function of two logic circuits.

A logic circuit verification device 10 including the above-mentioned respective parts
Is an input device such as a keyboard, a mouse, a light pen, or a flexible disk device, a CPU, and this CP
It is constituted by an ordinary computer system including a ROM, RAM, a storage device such as a magnetic disk connected to the U, and an output device such as a display device and a printer device.

Next, in the logic circuit verification device 10 configured as described above, the processing procedure for determining the equivalence of the logic or function of the logic circuit to be verified will be described with reference to the flowchart of FIG.

First, 2 to be verified from the circuit information input section 1
Enter information about one logic circuit (step 10
1) and subsequently, don't care information input section 2 inputs don't care information about the two logic circuits (step 1).
02). At this time, additional information regarding the gated clock design of the logic circuit is input from the gated clock information input unit 5 as needed. Next, the equivalence determination circuit generation unit 3 determines whether there is don't care information regarding the two input logic circuits (step 10).
3). If there is no don't care information, an equivalence judgment circuit for judging the logic equivalence as shown in FIG. 3 is generated based on the information about the two logic circuits (step 104). If there is don't care information, an equivalence judgment circuit for judging the equivalence of the functions as shown in FIG. 4, for example, based on the don't care information about the two logic circuits and the don't care information about these logic circuits. It is generated (step 105). In FIG. 4, symbols such as dc_ol represent don't care functions of outputs or registers. The circuit data of the equivalence judgment circuit generated in step 104 or step 105 is stored in the equivalence judgment circuit storage unit 4.

Next, the gated clock partial correction unit 6
Determines whether the generated equivalence checking circuit is designed as a gated clock (step 10).
6). Here, when the gated clock is designed, the gated clock designed portion of the equivalence determination circuit is corrected by referring to the additional information regarding the gated clock design as necessary.

First, with respect to the equivalence judgment circuit stored in the equivalence judgment circuit storage unit 4, an enable signal of a portion having a gated clock design is taken out (step 1).
07), a multiplexer having this enable signal as a control signal is generated in the data input portion of the register, the circuit is modified to use the clock enable logic as the selection logic of this multiplexer, and the gated clock portion is further removed ( Step 108). next,
Based on the gated clock information, the circuit portion not related to the equivalence determination is removed (step 109). The circuit data of the equivalence judgment circuit modified in steps 107 to 109 is stored in the equivalence judgment circuit storage unit 4.

Next, the equivalence judgment unit 7 is an equivalence judgment circuit stored in the equivalence judgment circuit storage unit 4, that is, the equivalence judgment circuit generated by the equivalence judgment circuit generation unit 3, or the equivalence judgment circuit. Based on the equivalence determination circuit corrected by the gated clock partial correction unit 6, the equivalence of logic or function of at least two logic circuits to be verified is determined (step 110).

The determination result is obtained by displaying an equivalent or non-equivalent message on a display device (not shown) or by printing out the same message by the printer device. If it is determined that they are not equivalent, in addition to the above message, a combination of inputs whose output results are not 1 may be displayed or printed out. in this case,
The designer can easily change the design of the original logic circuit by examining the logic of the logic circuit based on the combination of inputs whose output results are not 1.

Next, specific examples of the case of determining the equivalence of logic circuits in the logic circuit verification device 10 described above will be described as the first and second embodiments. The first embodiment
Shows an example in which there is no don't care information about the logic circuit to be verified, and the second embodiment shows an example in which there is don't care information.

[First Embodiment] First, FIGS. 5A and 5B.
It is assumed that two logic circuit circuits 1 and 2 as shown in (1) are input from the circuit information input unit 1. FIG. 5A does not have a gated clock design, and FIG. 5B has a gated clock design. In this example, since the input circuit has no don't care information, the equivalence judgment circuit generation unit 3 generates the equivalence judgment circuit for judging the logic equivalence as shown in FIG. It is stored in the circuit storage unit 4. In FIG. 6, the partial circuit 201 is shown in FIG.
The partial circuit 202 corresponds to FIG. 5A and corresponds to FIG.

In the partial circuit 201 of FIG. 6, when the Q port output of the D type flip-flop FF1 is FF1_Q, the logic of the D port input FF1_D of FF1 can be expressed by a Boolean expression as ^ I2 * FF1_Q + I2 * I1. Here, * represents a logical product, + represents a logical sum, and ^ represents a negative logic.
Further, in the partial circuit 202 of FIG. 6, the D port F of FF1
The logic of F1_D is expressed as ^ I1 * I2, which is different from the partial circuit 201 of FIG. On the other hand, at the output terminal O1, the logic is I3 * FF for both the partial circuits 201 and 202 of FIG.
The same logic can be expressed as 1_Q. In the circuit of FIG. 6, F
Since the logic of the D port input of F1 is different, as a result, out_check in FIG. 6 does not always become 1, and the equivalence determination circuit as it is determines that it is not equivalent.

Therefore, the gated clock partial correction unit 6
Corrects the equivalence determination circuit of FIG. 6 so that the CK port inputs of the two flip-flops FF1 become the same signal. This modification is done as follows. That is, in the partial circuit 201 of FIG. 6, the logic of the CK port input of FF1 is CLK, and in the partial circuit 202, the logic of the CK port input of FF1 is CLK + ^ I2, so that the logic of both CK port inputs is CLK. Change the circuit.

First, in the partial circuit 201 of FIG.
Since it is LK, no operation is performed. On the other hand, FIG.
In the partial circuit 202 of, when ^ I2 is 1, that is, I
When 2 is 0, the clock is not supplied to the port of FF1. That is, when I2 is not 0, the value of FF1 is held. Therefore, the FF in the partial circuit 202 of FIG.
To set the logic of CK port input of 1 to CLK, I
When 2 is 0, a logic for holding the value of FF1 may be added. In this example, the MUX 51 for selecting data loading and data holding for the FF1 is connected to the D port input of the FF1, and the circuit is modified so that the clock enable logic is given to the selection logic of this MUX51. As a result of such modification, the equivalence judgment circuit as shown in FIG. 7 is generated. The circuit element MUX in FIG.
51 can be constituted by a logic circuit as shown in FIG. 8, for example.

The equivalence judgment circuit of FIG. 7 stored in the equivalence judgment circuit storage unit 4 by the above modification is judged to be equivalent by the equivalence judgment unit 7. Looking at the circuit of FIG. 7, the partial circuit 203 and the partial circuit 204 are provided at the output terminal O1.
In both cases, the logic can be expressed as I3 * FF1_Q and the same logic is obtained. Further, regarding the logic of the D port input FF1_D of FF1, both the partial circuit 203 and the partial circuit 204 are BDD.
When expressed using, it is understood that they are expressed in the same format as in FIG. 9A and have the same logic.

That is, in FIG. 9A, FF1_D
Substituting 0 for I2 of (the dashed arrow of 0), FF1_Q
, And if FF1_Q is 0 here (broken line arrow of 0), the output becomes 0. If FF1_Q is 1 (solid arrow 1), the output will be 1. Also, FF1_D
When 0 is substituted for I1 (solid arrow of 1), I1 remains, and when I1 is 0 (broken arrow of 0), the output becomes 0. If I1 is 1 (solid arrow 1),
The output is 1. The partial circuit 203 and the partial circuit 204
In both cases, when 0 and 1 of the same combination are input to I1 and I2, the process proceeds in the arrow direction of the same path, and the D port input FF1_D of FF1 has the same output result. Therefore, BDD representing the logic of out_check in FIG.
Is always 1 as shown in FIG. Therefore, the equivalence determination unit 6 determines that the logic circuit of FIG. 5A and the logic circuit of FIG. 5B are equivalent.

[Embodiment 2] Next, another embodiment will be described. First, it is assumed that two logic circuits as shown in FIG. 10 are input from the circuit information input unit 1. Figure 10 (a)
In the figure, the gated clock is not designed.
It is designed with a gated clock. In this example,
It is assumed that B as a don't care function for the flip-flop FF1 and ^ I2 as a don't care function for the output terminal O1 are input from the don't care information input unit 2.

Next, the equivalence judgment circuit generation unit 3 generates an equivalence judgment circuit for judging the equivalence of the functions as shown in FIG. 11 in consideration of the don't care information and stores it in the equivalence judgment circuit storage unit 4. Store. In FIG. 11, even if the don't care information is taken into consideration, the function of the D port input of the FF1 is different between the partial circuit 205 and the partial circuit 206, and out_check is not always 1, and it is determined that the equivalence determination circuit is not equivalent. Will be done.

Therefore, the gated clock partial correction unit 6
Corrects the equivalence determination circuit of FIG. 11 so that the CK port inputs of the two flip-flops FF1 become the same signal. Here, it is assumed that the gated clock information input unit 5 inputs information that the flip-flop ENA_FF is a flip-flop inserted to remove a glitch in the clock enable logic. In the gated clock partial correction unit 6, ENA_FF
Recognize that the logic of the D port input of is the clock enable logic. In the partial circuit 206 of FIG. 11, ENA_F
When the Q port output of F is 0, no clock is supplied to the CK port of FF1. This is because when the enable logic recognized as described above is 0, that is, when the logical expression ^ A + B is 1, the value of FF1 is held. Therefore, FIG.
In the partial circuit 206 of, FF when ^ A + B is 1
A logic in which a value of 1 is held is added. In this example, EN
The circuit is modified so that the A_FF is deleted, the MUX 61 for selecting data loading and data holding for the FF 1 is connected to the D port input of the FF 1, and the clock enable logic is given to the selection logic of the MUX 61. As a result of such modification, the equivalence judgment circuit as shown in FIG. 12 is generated. On the other hand, in the partial circuit 205 of FIG. 11, since the CK port input of FF1 is CLK, no logic is added. The equivalence judgment circuit shown in FIG. 12 generated in the equivalence judgment circuit storage unit 4 by this modification is judged in the equivalence judgment unit 6 for equivalence. As a result,
The BDD representing the logic of out_check in No. 2 is as shown in FIG. 9B, and it can be seen that it is always 1. Therefore, the equivalence determination unit 7 has the logic circuit of FIG.
The 0 (b) logic circuits are determined to be equivalent.

As described above, the gated clock design adds a logic circuit to the clock input port (CK) of the register, so that even if the two partial circuits are functionally equivalent, the conventional The logic circuit verification device cannot judge the logical or functional equivalence of these two partial circuits, and it has been judged that they are not equivalent. However, according to the logic circuit verification device of the present embodiment, it is possible to verify the gated clock designed portion by modifying the circuits so that the clock inputs of the registers of the two logic circuits become equal. It becomes possible to verify the logical or functional equivalence of a gated clock designed logic circuit that could not be correctly verified by the device.

In the above embodiment, I1 and I2 are 1
Although described as bits, the case of 32 bits or 64 bits can be applied. In particular, when the number of input bits is large, the calculation time can be significantly shortened as compared with the case where a simulator is used.

Further, in the above embodiment, the logic or functional equivalence of the logic circuit is verified with respect to the two circuits, but the equivalence verification can be carried out with respect to a plurality of logic circuits. Further, in the above-described embodiment, the register circuit configured by the flip-flop is shown as an example of the logic circuit to be verified, but the synchronous memory (synchronous RA
It can also be applied to a register circuit composed of memory cells that write data in synchronization with a clock as in M).

The program for realizing the operation of the logic circuit verification device described above can be stored in a computer-readable recording medium. By reading this recording medium by a computer system and executing the program to control the computer, the processing by the logic circuit verification device described above can be realized. Here, the recording medium includes, for example, all recording devices such as a memory device, a magnetic disk device, and an optical disk device capable of recording a program.

[0059]

As described above, according to the logic circuit verification device, the logic circuit verification method, and the computer-readable recording medium storing the logic circuit verification program according to the present invention, the generated equivalence judgment circuit is gated. Since the circuit is modified so that the clock-designed portion can be verified, the logic or functional equivalence of the gated-clock-designed logic circuit, which cannot be correctly verified by the conventional device, can be obtained. Verification is possible.

[Brief description of drawings]

FIG. 1 is a block diagram showing a functional configuration of a logic circuit verification device according to an embodiment.

FIG. 2 is a flowchart showing a processing procedure when determining the equivalence of logic or function of a logic circuit in a logic circuit verification device.

FIG. 3 is a circuit configuration diagram showing an example of an equivalence judgment circuit for judging equivalence of logics generated by an equivalence judgment circuit generation unit.

FIG. 4 is a circuit configuration diagram showing an example of an equivalence judgment circuit for judging equivalence of functions generated by an equivalence judgment circuit generation unit.

5A and 5B are circuit configuration diagrams showing a logic circuit input from a circuit information input unit in the first embodiment.

FIG. 6 is a circuit configuration diagram showing an equivalence judgment circuit for judging the equivalence of the logic generated by the equivalence judgment circuit generation unit of the first embodiment.

FIG. 7 is a circuit configuration diagram showing an equivalence judgment circuit for judging equivalence of logics generated by the equivalence judgment circuit generation unit of the first embodiment.

FIG. 8 is a logical structure diagram of MUX.

9A and 9B are explanatory diagrams showing an example of a BDD generated by an equivalence determination unit.

10A and 10B are circuit configuration diagrams showing a logic circuit input from a circuit information input unit in the second embodiment.

FIG. 11 is a circuit configuration diagram showing an equivalence judgment circuit for judging equivalence of logic generated by an equivalence judgment circuit generation unit according to the second exemplary embodiment.

FIG. 12 is a circuit configuration diagram showing an equivalence judgment circuit for judging equivalence of functions generated by an equivalence judgment circuit generation unit according to the second exemplary embodiment.

FIG. 13 is a circuit configuration diagram showing an example of a logical equivalence determination circuit generated by a conventional logic circuit verification device.

14A is a logic circuit diagram for explaining a don't care condition, and FIG. 14B is an explanatory diagram showing a relationship between a control signal and a function of an ALU.

15A is a circuit configuration diagram showing a partial circuit for which a gated clock is not designed, and FIG. 15B is a circuit configuration diagram showing a partial circuit for which a gated clock is designed.

[Explanation of symbols]

1 Circuit information input section 2 Don't care information input section 3 Equivalence determination circuit generator 4 Equivalence determination circuit storage 5 Gated clock design support section 6 Equivalence determination unit 7 Gated clock information input section

Claims (3)

(57) [Claims] 1. A circuit information input means for inputting information about at least two logic circuits to be verified and don't care information about the logic circuits, and the at least 2 based on the information about the logic circuits and the don't care information about the logic circuits. Equivalence judgment circuit generating means for generating an equivalence judgment circuit including two logic circuits, and a gated clock design for the equivalence judgment circuit.
If at least two logic circuits are included,
Clock inputs of registers included in the logic circuit become equal
The gated clock is designed as a logical time
A gated clock partial correction means for correcting the equivalence judgment circuit by inserting a multiplexer in the path, and the equivalence judgment circuit generated by the equivalence judgment circuit generation means or the equivalence corrected by the gated clock partial correction means. At least 2 to be verified based on the sex determination circuit
A logic circuit verification device, comprising: an equivalence judging means for judging equivalence of logic or function of one logic circuit. 2. A logic circuit verifying device comprising circuit information input means, equivalence judgment circuit generation means, gated clock partial correction means, and equivalence judgment means is used to determine the logic or logic of at least two logic circuits. A logic circuit verification method for determining the equivalence of functions, wherein the circuit information input means inputs information about at least two logic circuits to be verified and don't care information about the logic circuits, the circuit information input step Based on the information about the logic circuit and the don't care information about the logic circuit,
An equivalence judgment circuit generating step of generating an equivalence judgment circuit including at least two logic circuits; and a case where the gated clock partial correction means includes a logic circuit having a gated clock design in the equivalence judgment circuit. A gated clock partial correction step of correcting the equivalence judgment circuit by inserting a multiplexer into the logic circuit having the gated clock design so that clock inputs of registers included in the at least two logic circuits become equal. At least two logic circuits to be verified by the equivalence judgment means based on the equivalence judgment circuit generated in the equivalence judgment circuit generation step or the equivalence judgment circuit modified in the gated clock partial modification step. Equivalence judgment step to judge equivalence of logic or function of Logic circuit verification method, which comprises a. 3. A circuit information input step of inputting information about at least two logic circuits to be verified and don't care information about the logic circuits, and the at least 2 based on the information about the logic circuits and the don't care information about the logic circuits. An equivalence judgment circuit generating step of generating an equivalence judgment circuit including two logic circuits; and, if the equivalence judgment circuit includes a logic circuit having a gated clock design, registers included in the at least two logic circuits. Generated by the gated clock partial correction step of correcting the equivalence judgment circuit by inserting a multiplexer into the logic circuit having the gated clock design so that the clock inputs of are equal to each other, and the equivalence judgment circuit generation step. Equivalence determination circuit or the gated clock An equivalence judgment step of judging equivalence of logic or functions of at least two logic circuits to be verified based on the equivalence judgment circuit corrected in the partial correction step, and causing a computer to execute these steps. A computer-readable recording medium storing a characteristic logic circuit verification program.