JP3703390B2 - Logic verification device - Google Patents

Description

[0001]
BACKGROUND OF THE INVENTION
The present invention relates to a method for detecting an oscillation component in a loop circuit, and particularly in a semiconductor device such as an ASIC (Application Specific IC) that is an application specific IC or an SOC (System On Chip) that is a composite IC. Therefore, there is a high risk that a negative feedback loop is formed by a logic gate. For this reason, the present invention relates to a method for detecting an oscillation component in a loop circuit improved so as to be detected in advance before a negative feedback loop is built in a chip.
[0002]
[Prior art]
In recent years, with the progress of miniaturization technology of semiconductor elements, LSIs composed of the semiconductor elements have also increased in scale, and semiconductor memories, microcomputers, or SOCs, which are composite LSIs incorporating these LSIs on a single chip, have also increased in capacity. Have been doing. Along with this increase in capacity, the circuit function also becomes complicated, and improving the accuracy of circuit verification at the design stage is one of the important issues.
[0003]
In these LSI internal circuits, there is a positive feedback loop or a negative feedback loop as a loop circuit with logic gates. In particular, when a negative feedback loop exists, the logic circuit in the actual machine changes from oscillation to intermediate voltage, causing leakage current. Become.
[0004]
Negative feedback loops that cause such problems are intentionally created in LSIs that are mainly small-scale (number of gates: 100K or less) designs and that require a lot of manpower in circuit design, such as external sales ASICs. As long as it was not inserted, it was not built into the internal circuit.
[0005]
However, in recent years, the design has become large-scale, and there has been an example in which circuit design can be created without consciousness due to the increased use of automatic design methods using logic synthesis tools. It has become.
[0006]
The circuit scale tends to further increase in the future, and it is considered that such examples will increase in the future.
[0007]
[Problems to be solved by the invention]
In conventional ASICs and SOCs such as those described above, a mechanism that specifically detects an oscillation loop location has not yet been developed even in such a change in the design environment. An example of a method for verifying such determination by using logic simulation is described in Japanese Patent Application No. 1-193668.
[0008]
Referring to the verification method described in the publication, it is determined whether or not the oscillation occurs from the logic transition at a specific time t to t + Δt. However, depending on the circuit configuration, an initial value cannot be put in the loop, Then, even at the time t and a little later t + Δt, the internal logic is indefinite to indefinite, and the logic transition cannot be seen and the determination cannot be made.
[0009]
For example, referring to FIG. 12 showing a circuit example for explaining the conventional verification method described above, this circuit has one loop of NAND12a → AND12b → NAND12a, and the input terminal B is clamped by HIGH_CLAMP (“1”). ) 12c is clamped to the logic level “1”, and therefore, in the logic simulation, the output of the NAND 12a is uncertain from the beginning, and the inversion of the uncertain is uncertain no matter how much time advances.
[0010]
Therefore, as shown in FIG. 13 showing the waveform diagram of the simulation result, since the input A at time t = 0 is X, X continues to circulate between the subsequent output Y → input A, and the first (time From the time t = 0) to the end, the indefinite X flows so that it is not known whether it is oscillating.
[0011]
However, referring to FIG. 14 showing the input / output waveform of the NAND 12a on the actual machine, it gradually becomes stable near the intermediate voltage while repeating the logic level HIGH (= 1) / LOW (= 0) value. This causes a through current to flow.
[0012]
In the method using a logic simulator, whether or not detection is possible depends greatly on the quality of VECTOR. However, the larger the circuit scale, the more difficult it is to create a VECTOR that toggles all internal nodes. The current situation is becoming.
[0013]
An object of the present invention is made in view of the above-described conventional drawbacks, and by preparing a library having information based on a specific rule for each logic gate, an oscillation loop circuit is provided for the circuit itself. It is to provide a verification method for detecting and verifying the above.
[0014]
[Means for Solving the Problems]
  The logic verification device of the present invention is a logic verification device for a circuit, and for each element type, a logic inversion path between input and output terminals and an oscillation stop condition that is a condition of an input terminal whose output terminal is a fixed output. Logic inversion path oscillation stop condition storage means for storing, loop detection means for detecting a loop circuit included in the circuit to be verified, and for each element included in the loop path of the detected loop circuit, the logic Refer to the inversion path oscillation stop condition storage means, detect whether the connection between the input terminal and the output terminal of the element in the loop path corresponds to the logic inversion path, and determine the number of logic inversion paths included in the loop path. Counting and positive / negative feedback check means for determining whether the loop circuit is a positive feedback loop or a negative feedback loop, and when determining that the positive / negative feedback check means is a negative feedback loop When each element included in the loop path of the loop circuit refers to the logic inversion path oscillation stop condition storage means, and an input terminal not included in the loop path among the input terminals of the element satisfies the oscillation stop condition Determining that there is no problem with the loop circuit, and depending on the condition of the input terminal, if the oscillation stop condition is satisfied, an out-of-loop input check means that clearly indicates the condition is provided, and the configuration of the circuit is an oscillation loop configuration. It is characterized by clearly indicating the determination result of whether or not and the condition for avoiding the oscillation state.
[0015]
  Also,The logic verification device of the present invention detects whether or not an exclusive OR or an exclusive negative OR exists in an element included in the loop path of the loop circuit, and if detected, the loop of the element is detected. Traces the input value of the input terminal not included in the path back to the previous stage, and the input of the input terminal is clamped. Depending on the clamped input value, the exclusive OR or exclusive negative OR is inverted. Or, when it can be reduced to a non-inverter, it further comprises an exclusive logic processing means for reducing, and when the exclusive logic processing means performs the reduction, the positive / negative feedback check means and the outside of the loop for the reduced loop circuit Determination by the input check means can be performed.
[0016]
  further,In the logic verification device according to the present invention, as a result of the exclusive logic processing means tracing the input value of the input terminal not included in the loop path of the element with respect to the exclusive logical sum or the exclusive negative logical sum, If the input is uncertain, the determination by the positive / negative feedback check means may not be performed, and the element other than the exclusive OR or exclusive negative OR may be determined by the out-of-loop input check means. .
[0017]
  Furthermore,The logic verification apparatus according to the present invention processes the input value trace of the input terminal by the exclusive logic processing unit as an indeterminate input value when the input terminal is included in another small loop. Input value trace to beYou can also
[0018]
  Also,In the logic verification device of the present invention, the out-of-loop input check means traces an input value of an input terminal not included in the loop path back to the previous stage, and the oscillation stop condition is satisfied by the traced input value. It can also be determined whether or not.
[0019]
  further,In the logic verification device of the present invention, the input value trace of the input terminal by the out-of-loop input check means cancels the input value trace when the input terminal is included in another small loop, and sets the input value as indeterminate. It can also be an input value trace to be processed.
[0020]
  Furthermore,In the logic verification device of the present invention, the input value trace of the input terminal by the out-of-loop input check means is traced back to the previous stage, as a result of sequential circuit, aliasing of the input / output circuit, adder, connection of all terminals of the parity generator, When connected to the output logic of the terminal connection of the enable portion of the latch, multiplexer and decoder, the input value can be treated as indeterminate.
[0021]
  Also,In the logic verification device according to the present invention, the input value trace of the input terminal by the out-of-loop input check means determines that the input value is indeterminate if the value is not confirmed or uncertain even after any specified number of stages. It can also be handled.
[0028]
DETAILED DESCRIPTION OF THE INVENTION
As a method for detecting a negative feedback loop by a logic gate in particular, the present invention eliminates defects due to leakage current by creating a database of prohibition information and constructing a verification system for circuit rule check (logic trace). It can supply high chips.
[0029]
First, a first embodiment of the present invention will be described in detail with reference to the drawings.
[0030]
Referring to FIG. 1, which is a flowchart showing a method for detecting an oscillation component in a loop circuit according to the first embodiment of the present invention, this method is applied to a logic verification device (not shown) and operates by program control. Loop detection process S1, exclusive OR or exclusive negative OR process S2 (FIG. 2 described later), positive / negative feedback check process S3 (described later FIG. 3), and outside-loop input check process S4 (described later) FIG. 4) shows output processing S5 such as display processing and printing processing for clearly displaying circuit locations and displaying problems, and “input stage tracing” processing started as a subroutine from processing S1 and processing S4. The process of FIG. 5 is included. Furthermore, it is configured to include a storage medium including truth value information 11 necessary for the control of the processes S2 and S4 and a dedicated library 12 (FIG. 6 described later).
[0031]
The loop detection process S1 is a process for searching for a loop portion by using an already known technique. That is, the output stage is traced starting from all elements, and when returning to the element visited so far, the element is detected as a loop.
[0032]
In the search, the purpose is to find a loop composed only of logic gates, and since a rule of thumb does not lead to oscillation when these elements are included, a specific element (described below) ) Is excluded from the search target, and another route is searched. That is, it is determined that the route is not a loop.
[0033]
Specific elements connected in a loop that is not verified:
Sequential circuit, ENABLE part of LATCH, MULTIPLEXER, and DECODER, I / O loopback, connection to ADDER.
[0034]
Elements connected in the loop to be verified:
INVERTER, NON-INVERTER, OR, NOR, AND, NAND, XOR, XNOR, composite gate, LATCH, MULTIPLEXER, and DECODER data parts.
[0035]
In the library required for execution of processing 3 and processing 4 (FIG. 6), two pieces of information are defined in advance for each element: (1) logic inversion path (2) oscillation stop condition. The logic inversion path literally defines “where is the path where the logic level is inverted in polarity between the input and output terminals” in the connection path in the loop.
[0036]
In addition, the oscillation stop condition defines information indicating “if the input value from the other input terminal outside the loop is fixed, it will not oscillate”.
[0037]
In the process S2, a process when there is XOR / XNOR is performed. Since XOR / XNOR changes whether or not the polarity of the signal level is inverted between the input and output terminals depending on the input value from the other input terminal outside the loop, the exception is that from the other input terminal outside the loop. Trace the input first to verify that the input value from outside the loop is fixed.
[0038]
If the input value from outside the loop can be fixed, these XOR / XNOR are replaced with INVERTER or NON-INVERTER based on the truth value information 11. If it is not replaced, the loop cannot perform positive feedback / negative feedback determination (process 3), and therefore, only from the outside-loop input check (process 4) of another block.
[0039]
In process S3, each element in the loop is compared with the logic inversion path stored in the library, and the number of inversion paths in the entire loop is calculated. Based on the result, positive / negative feedback of the loop is determined.
[0040]
When the determination result is an odd number, it is determined as a negative feedback loop, and when it is “0” or an even number, it is determined as a positive feedback loop. In the case of the positive feedback loop, since there is no oscillation in the circuit, it is determined that there is no problem with the loop. As described above, when there is XOR or XNOR that cannot be replaced with INVERTER or NON-INVERTER, this processing is not performed.
[0041]
In the process S4, the possibility that the output logic is fixed by the input value from the other input terminal outside the loop of each element in the loop is verified. As a method, an element corresponding to the preceding stage of these elements is verified.
[0042]
It is determined that the element in the previous stage is a logic gate, etc., and is fixed at a specific value when it is connected to the clamp or external terminal. Since the output of the element is not fixed, it is determined that the value is not fixed by the connection. In the case of other elements, the previous element is further verified.
[0043]
Connection element that determines that the logic level is not fixed and does not perform further preceding trace:
Sequential circuit, I / O loopback, adder, all connections of parity generator, connection of latch, multiplexer and decoder enable part.
[0044]
If the input value from the other input terminal outside the loop of the element is fixed for the element in the loop as a result of the previous trace, it is checked against the oscillation stop condition stored in the library. Determine whether the output logic level of the elements in the loop is fixed. If it is fixed depending on the usage condition of the external terminal, the condition is also specified.
[0045]
Strictly speaking, since the preceding trace itself is possible even with the above-described elements / connections, it may be possible to select whether or not to arbitrarily verify.
[0046]
In addition, the number of stages in the preceding trace is determined in principle, but it is not verified, but verification is performed until it becomes clear. If confirmation is not decided, it may be handled as indeterminate.
[0047]
Another condition for ending the input trace is that an element that has already been visited has come out. In such a case, the structure is a double loop, and the loop is cut in order to keep rotating forever.
[0048]
When sufficient confirmation sufficient to determine that there is no problem in the output process S5 cannot be obtained, information on which elements are in a loop configuration is clearly indicated on the external display means, and the verification on the loop is completed. .
[0049]
In the description, a unique name given in the circuit data for each element is used to specifically indicate which connection is a loop that may oscillate on the actual machine.
[0050]
Finally, in process S6, it is confirmed whether all the loops detected in the loop detection process S1 have been detected.
[0051]
Next, FIG. 1 showing a detailed description, conditions, implementation reasons, and an overall flowchart of the verification method of the present invention, and FIGS. 2 to 5 showing detailed flowcharts of the respective processes. The embodiment will be specifically described with reference to the above.
[0052]
First, the processing in FIG. 1 will be described. In the “find loop configuration” of process S1, a loop portion is searched. When the process S1 is completed, the process proceeds to process S2. The algorithm for finding the loop and its conditions are as described above.
[0053]
In the process S2 “XOR / XNOR process”, if there is an XOR / XNOR in the loop detected in the process S1, an attempt is made to replace it with INVERTER / NON-INVERTER. When there is XOR / XNOR and replacement cannot be performed, the process S3 is not performed and the process proceeds to the process S4. Otherwise, the process proceeds to process S3.
[0054]
In the process S3 “positive / negative feedback check”, it is determined in the process S1 whether the loop in which XOR / XNOR is replaced with another block in the process S2 is a positive feedback loop or a negative feedback loop.
[0055]
In the case of a positive feedback loop, the verification of the loop ends and the process proceeds to step S6. In the case of a negative feedback loop, the process proceeds to step S4. The determination is made by verifying how many “logic inversion paths” described in the “dedicated library” are used for connection in the loop.
[0056]
The process S4 “in-loop input check” is a process that is performed when the negative feedback loop is determined in the process S3 or when all the XOR / XNOR cannot be replaced in the process S2.
[0057]
Input value from the other input terminal outside the loop for each element (excluding XOR / XNOR) in the loop detected in process S1 or in the loop in which XOR / XNOR is replaced with another element in process S2 To determine whether the output is fixed.
[0058]
As a result, if the input outside the loop is clamped and does not oscillate universally when compared with the “oscillation stop condition” defined in the “dedicated library”, verify this loop. Ends and proceeds to step S6. In other cases, that is, when the condition is OK or there is a problem, the process proceeds to step S5.
[0059]
The process S5 “display the problem by specifying the circuit location” is performed when there is no confirmation that the oscillation does not occur universally as a result of the process S4. Specifically, the case where the verification verified in step S4 cannot be stopped by the input value from the other input terminal outside the loop, and the case where the oscillation is stopped depending on how the external terminal is used. including. In the latter case, the usage conditions of the external terminal are also displayed here. When this process ends, the process proceeds to process S6.
[0060]
In process S6 “Is there another loop?”, It is checked whether there is another loop to be verified in the circuit. If there is, the process proceeds again to step S2, and a series of verifications are performed. If not, the process ends.
[0061]
Next, the flow of FIG. 2 that shows the detailed verification method of the process S2 “XOR / XNOR process” in FIG. Since the processing S1 and the processing S6 in FIG. 1 are known techniques, a detailed description of the operation is omitted here.
[0062]
The process S2a “presence / absence of XOR / XNOR” checks whether XOR / XNOR is included in the loop found in the process S1. If even one is included, the process proceeds to step S2b. If not, the process immediately proceeds to step S3 in FIG.
[0063]
Process S2b “input stage trace” selects one of the XOR / XNOR discovered in process S2a that has not been verified yet, and the input value from the other input terminal outside the loop for that element is fixed. Verify whether it has been.
[0064]
Regarding the operation of the “input stage trace” portion, there is FIG. 5 showing a more detailed verification method, which will be described later. As a result of executing the processing shown in FIG. 5, if a return value is obtained, the processing proceeds to processing S2c.
[0065]
The process S2c “Can be replaced with (NON−) INVERTER?” Determines whether or not the XOR / XNOR traced in the previous stage in the process S2b can be replaced with INVERTER / NON-INVERTER.
[0066]
Specifically, if the input value from the other input terminal outside the loop input to XOR / XNOR verified in step S2b is “1”, it can be replaced with INVERTER, and if “0”, it is replaced with NON-INVERTER. Is determined to be possible, and the process proceeds to step S2d.
[0067]
In other cases (indefinite), it is determined that the replacement is impossible, and the process moves to the process S4 in FIG. In the case where there are a plurality of XOR / XNORs, if there is one that cannot be replaced, the process moves to the process 4 in FIG.
[0068]
The process S2d “execute replacement” receives the determination result of the process S2c and replaces the XOR / XNOR determined in the process S2c with INVERTER / NON-INVERTER.
[0069]
Thereafter, the process proceeds to process S2e. In the process S2e “is there any other XOR / XNOR?”, If there is another XOR / XNOR found in the process S2a, the process from the process S2b is performed again. If not, the process moves to step S3 shown in FIG.
[0070]
Next, the process S3 in FIG. 1 will be described with reference to FIG. 3 describing the detailed verification method. This process can be replaced with INVERTER / NON-INVERTER if XOR / XNOR does not exist in the loop detected in process S1 as a result of XOR / XNOR verification in process S2, or XOR / XNOR exists but all exist. If it is, it is determined whether the loop is a positive feedback loop or a negative feedback loop.
[0071]
In the process S3a “determine start point”, an arbitrary element in the loop discovered in the process S1 and partially converted in the process 2 is selected as a verification element. Since all S elements are finally verified under the same conditions, this selection method is arbitrary and causes no problem. If it selects, it will move to process S3b.
[0072]
In the process S3b “pass through inversion path?”, It is verified whether the polarities of the input and output signals are inverted between the input / output terminals in the loop of the currently verified element.
[0073]
The currently verified element is the element first selected in the process S3a or the element newly selected as the verification element in the process S3d described later. In the verification method, if the connection of the “logic inversion path” defined in the library (FIG. 6) is in the loop, the process proceeds to step S3c assuming that the inversion path is passed. Otherwise, the process proceeds to process S3d.
[0074]
The process S3c “inversion number + 1” is performed when the polarity of the input and output signals is inverted between the input and output terminals in the loop of the element being verified as a result of the verification in the process S3b.
[0075]
Internally, the inversion number is increased by 1. The internal memory is cleared when processing S3 is completed, but is retained until then. After this process is completed, the process proceeds to process S3d.
[0076]
In process S3d “next stage”, the element being verified is transferred to another element. Specifically, the subsequent element is selected as an element to be newly verified. The process moves to the next process S3e of this process.
[0077]
In process S3e “return to start point?”, It is determined whether the element selected as the element to be verified is the same as the element selected in process S3a as a result of the process S3d.
[0078]
If the selected elements are the same, all the elements in the loop have been verified, and the process proceeds to process S3f. If they are not the same, the process returns to step S3b to perform the same verification.
[0079]
The process S3f “determination” is performed depending on whether the inversion number stored internally as a result of the processes S3b to S3e is an even number or an odd number. If it is an even number, it is determined as a positive feedback loop, and the next destination is the process S5 in FIG.
[0080]
On the other hand, if the number is odd, the process S4 in FIG. In either case, the inversion number held as the internal memory is cleared once here.
[0081]
Next, processing S4 in FIG. 1 will be described with reference to FIG. 4 showing a flowchart of the detailed verification method.
[0082]
This processing is performed when all of the XOR / XNORs detected in the processing S1 are detected when the negative feedback loop is verified as a result of the positive / negative feedback check verified in the processing S3c and when the XOR / XNOR verification of the processing S2b is performed. This is performed when it cannot be replaced with another element.
[0083]
The contents are detected by the processing S1 and, depending on the input signal from the other input terminal outside the loop, for all the elements in the loop in which XOR / XNOR is replaced by other elements in the processing S2. Verify whether the output value is fixed.
[0084]
In the process S4a “determine start point”, when verifying all the elements in the loop detected in the process S1 and possibly having the XOR / XNOR replaced with another element in the process S2, an arbitrary element is verified first. Select as an element.
[0085]
Since all elements are finally verified, the selection of this element is arbitrary and causes no problem. After this process, the process proceeds to process S4b.
[0086]
In process S4b “XOR / XNOR?”, It is determined whether or not the currently verified element is XOR / XNOR. The element currently being verified is the element selected first in the process S4a or newly selected as the verification element in the process S4i described later.
[0087]
If the currently verified element is XOR / XNOR, whether or not the input value from the other input terminal outside the loop is fixed has already been performed in step S2b. Accordingly, no further verification on this element is necessary, and the process immediately moves to process 4i. In other cases, the process proceeds to step S4c in order to perform verification as usual.
[0088]
In process S4c “Is oscillation stop condition present?”, It is checked whether or not the currently verified element has an “oscillation stop condition” defined in the dedicated library (FIG. 6).
[0089]
The element currently being verified is the element selected first in the process S4a or newly selected as the verification element in the process S4i described later. For example, an element that has only one input terminal and cannot stop oscillation from outside the loop, such as INVERTER, does not have the “oscillation stop condition”.
[0090]
If there is no “oscillation stop condition”, the output value is not fixed by the input value from the other input terminal outside the loop, and no further verification on this element is required, so the process proceeds to step S4i. If there is an “oscillation stop condition”, the process proceeds to step S4d.
[0091]
The process S4d “input stage trace” verifies whether or not the input value from outside the loop of the currently verified element is fixed. The element currently being verified is the element selected first in the process S4a or newly selected as the verification element in the process S4i described later.
[0092]
In step S4c, this is performed when the currently verified element has an “oscillation stop condition” defined in the dedicated library (FIG. 6). Regarding the operation of this part, FIG. 5 shows a more detailed verification method, and FIG. 5 will be described later. If a return value is obtained as a result of the process shown in FIG. 5, the process proceeds to process S4e.
[0093]
The process S4e “comparison with oscillation stop condition” includes the input value from the other input terminal outside the loop of the currently verified element obtained in process S4d and the “oscillation stop condition” in the dedicated library (FIG. 6). A comparison is made as to whether or not the condition defined as “is satisfied.
[0094]
When the input value from outside the loop obtained in the process S4d is indefinite (X), it does not satisfy the condition presented as the “oscillation stop condition” in the dedicated library (FIG. 6). Thereafter, the process proceeds to process S4f.
[0095]
In the process S4f “Oscillation stopped?”, The next destination changes depending on the result of the determination performed in the process S4e. Specifically, if the determination result obtained in step S4e satisfies the condition presented as the “oscillation stop condition” in the dedicated library (FIG. 6), the loop will not oscillate. To step S4g.
[0096]
This includes a case where there is a condition such as “satisfied but only when the external terminal is OO”. If not, the process proceeds to process S4i to verify other elements.
[0097]
The process S4g “has a condition?” Is a process that is performed in the process S4f when the currently verified element can stop oscillating by the input value from the other input terminal outside the loop. The element currently being verified is the element selected first in the process S4a or newly selected as the verification element in the process S4i described later.
[0098]
In process S4d, when the input from the outside of the loop is traced and it is determined that the input value of the other input terminal from the outside of the loop is fixed, is the value fixed universally by the clamp? The next destination is branched depending on whether it is fixed depending on the usage conditions.
[0099]
When the clamp is universally fixed, since it can be determined that the loop found in the currently verified process S1 does not oscillate at this time, the verification of this loop is completed, and the place in FIG. Control goes to step S6. If it is determined whether or not the oscillation stops depending on the use condition of the external terminal, the process proceeds to step S4h.
[0100]
The process S4h “Condition explicit” indicates the condition when there is a condition for stopping the oscillation in the above-described process S4g. After this process, the process proceeds to process S4i.
[0101]
The process S4i “to next stage” is performed when there is no confirmation from the currently verified element that the oscillation can be stopped by the input value from the other input terminal outside the loop. This is done when it is attached and not universal.
[0102]
In order to perform verification on other elements in the loop, an element subsequent to the currently verified element is selected as a new currently verified element. After the process, the process moves to process S4j.
[0103]
In the process S4j “Return to start point?”, It is determined whether or not the element selected as the element to be verified is the same as the element selected in the process S4a as a result of the process S4g.
[0104]
In the case of the same, all the elements in the loop have been verified, and therefore, as a verification result of the entire process S4, “conditional OK or problematic” process S5 in FIG. Move on. If they are not the same, the process returns to step S4b to perform the same verification.
[0105]
Finally, FIG. 2 will be described with reference to FIG. 5 showing a detailed flowchart of “input stage tracing” started as a subroutine in the processing S2b and the processing S4d in FIG.
[0106]
In the process SRa “view previous stage”, the element immediately preceding the currently verified element is newly selected as the currently verified element. When visiting here for the first time, the element in the previous stage is selected as an element to be verified from the other input terminal outside the loop of the element being verified when activated from the processes S2b and S4d. If there are multiple, all will be selected. The determination regarding the (their) elements is performed in the next process SRb.
[0107]
If the element (group) selected in the process SRa has been visited before, the process SRb “has visited before?” Falls into an infinite loop if the path is continuously traced, and therefore needs to be cut. . If there is such a part, the process proceeds to processing SRc. If not, the process proceeds directly to the process SRd.
[0108]
The process SRc “cuts a small loop. The value is X” indicates that the element (group) currently verified in the process SRb is an element that has been visited so far. The value from the route is not determined (X). Thereafter, the process proceeds to the process SRd.
[0109]
The process SRd “confirmed to any one of 0, 1 and X?” Determines that if the currently verified element (group) is a clamp, it is determined to be “0” or “1” depending on the type and connection. .
[0110]
In the case of an external terminal, it can be determined to be an arbitrary value of “0” or “1” (in this case, it will be displayed in step S5 on the condition that the determined arbitrary value is used later). In the case of a sequential circuit or the like, it is determined that it is not fixed (X). In the case of other elements, the determination is suspended.
[0111]
Each detailed determination condition is as described above. From the places where these values obtained up to this point are determined / not determined / determination pending places, the input value from outside the loop for the element that has been verified when activated from the processing S2b / processing S4d is “0”. It is determined whether or not “/” 1 ”/“ X ”is fixed.
[0112]
If neither “0” / “1” / “X” is determined, the process returns to the process SRa. If not, the process returns to the process S2c or S4e with the determined value as a return value.
[0113]
Next, a first embodiment to which the above-described verification method is applied will be described with reference to FIG. 7 showing a specific circuit example to be verified.
[0114]
Process S1 (FIG. 1): find loop configuration (this process is an application of known technology)
As an example, assume that only one loop of AND7a → NON-INVERTER7b → 2-input OR7c → AND7a with INVERTER shown in FIG. 7 is found.
[0115]
Process S2 (FIG. 1): The XOR / XNOR process is performed when XOR / XNOR exists in the loop found in process S1.
[0116]
Process S2a (FIG. 2) → “Is XOR / XNOR in the loop?” → No, so move to process S3 with “Continue verification”.
[0117]
Process S3 (FIG. 1): The positive / negative feedback check verifies whether the loop found in process S1 is a positive feedback loop or a negative feedback loop.
[0118]
Process S3a (FIG. 3): One starting point for verification is determined in the loop found in process S1. Here, it is assumed that AND (7a in FIG. 7) is assumed.
[0119]
Process S3b (FIG. 3): It is verified whether the input / output path (input A → output Y) in the AND (7a in FIG. 7) loop is logically inverted. The dedicated library is checked against the “logic inversion path” in FIG. 6 to determine whether it passes through the logic inversion path.
[0120]
In the case of the AND (7a) in FIG. 7, when referring to the library, the path from input A to output Y corresponds to the logic inversion path, and thus “passes”, and the process proceeds to step S3c.
[0121]
Process S3c (FIG. 3): As an internal memory, the inversion number is incremented by 1, and the process proceeds to process S3d.
[0122]
Process S3d (FIG. 3): Since the verification of the AND 7a has been completed, the process proceeds to verification of another element.
[0123]
It moves to NON-INVERTER 7b, which is a subsequent block. Control goes to step S3e.
[0124]
Process S3e (FIG. 3): It is confirmed whether or not all elements have been verified. Since the start point selected in the process S3a is AND7a and not NON-INVERTER7b, the process moves to “NO”. This corresponds to the process S3b (second time) on the flowchart.
[0125]
Process S3b (FIG. 3) -2: It is verified whether the input / output path (input A → output Y) in the loop in INVERTER (7b in FIG. 7) is logically inverted. The dedicated library is checked against the “logic inversion path” column in FIG. 6 to determine whether the inversion path is passed. In the case of NON-INVERTER 7b in FIG. 7, since there is no inversion path from the library, the process proceeds to “does not pass” and proceeds to the next process S3d.
[0126]
Process S3d (FIG. 3) -2: Since the verification of NON-INVERTER 7b has been completed, the process proceeds to verification of another element. Here, the process moves to the subsequent block OR7c, and then moves to the next process S3e.
[0127]
Process S3e (FIG. 3) -2: It is confirmed whether or not all elements have been verified. Since the start point selected in the process S3a is the NAND 7a and not the OR 7c, it moves to “NO”. This corresponds to step S3b (third time) on the flowchart.
[0128]
Process S3b (FIG. 3) -3: It is verified whether the input / output path in the loop in the OR (7c in FIG. 7) is logically inverted. The dedicated library is checked against the “logic inversion path” in FIG. 6 to determine whether it passes through the inversion path. In the case of OR7c in FIG. 7, since there is no inversion path with reference to the library, the process proceeds to “does not pass” and proceeds to the next process S3d.
[0129]
Process S3d (FIG. 3) -3: Since the verification of the OR 7c is completed, the process proceeds to verification of another element. Here, it moves to AND7a which is a latter block, and moves to the next process S3e.
[0130]
Process S3e (FIG. 3) -3: It is confirmed whether or not all elements have been verified. Since the start point selected in the process S3a is the AND 7a and has returned to the start point, the series of verifications is terminated, the process proceeds to “NO”, and the process proceeds to the next process S3f.
[0131]
Process S3f (FIG. 3): Determine. The total number of inversions stored internally is 1 and an odd number (defined in step S3c). The process proceeds to “inversion number = odd number”, and “negative feedback” is returned as a result as processing S3.
[0132]
If it is “negative feedback” when returning to the process S3 in FIG. 1 again, the process moves to the process S4. Note that the inversion number of the internal storage is once cleared when the verification of the loop found in the processing S1 is completed. (Return to 0)
Process S4 (FIG. 1): It is verified whether the oscillation can be stopped by the input from the other input terminal (B) outside the loop.
[0133]
Process S4a (FIG. 4): One element as a verification starting point is arbitrarily selected in the loop found in process S1. It is assumed that AND (7a in FIG. 7) is assumed.
[0134]
Process S4b (FIG. 4): It is confirmed whether AND7a is not XOR / XNOR (because it was traced by another method in process S2). Since the AND 7a is not XOR / XNOR, the process proceeds to “NO” and moves to the next process S4c.
[0135]
Process S4c (FIG. 4): The AND 7a checks whether or not it has an oscillation stop condition. In the case of AND7a, if the input B = 0 is fixed with reference to the library of FIG. 6, the oscillation can be stopped, so that the process proceeds to “YES”, and the process proceeds to the next process S4d.
[0136]
Process S4d (FIG. 4): The input stage from the other input terminal outside the loop to the AND 7a is traced (subroutine).
[0137]
Process SRa (FIG. 5): Traces the previous stage of AND7a. The input B of the AND 7a comes from the external terminal “IN1”.
[0138]
Process SRb (FIG. 5): It is confirmed whether the element immediately before AND7a found in process SRa has visited before. Since it has not yet been visited, the process proceeds to “NO” and proceeds to the next process SRc.
[0139]
Process SRc (FIG. 5): It is determined whether the value is determined to be “0” / “1” / “X” (undefined) by the preceding input of AND7a found in process SRa. The input B of the AND 7a can be determined by connection from an external terminal. Therefore, the process proceeds to “YES” and proceeds to the process S4e in FIG.
[0140]
Process S4e (FIG. 4): The return value through process S5 is compared with the oscillation stop condition.
[0141]
From the oscillation stop condition obtained in the process S4c, the oscillation can be stopped as long as the external terminal obtained in the process SRc is fixed at “0”. Therefore, the process proceeds to process S4f.
[0142]
Process S4f (FIG. 4): It is determined from the result of process S4e whether oscillation stops. As a result of the determination, the process stops, so the process proceeds to “YES” and proceeds to the next process S4g.
[0143]
Process S4g (FIG. 4): It is determined from the result of process S4e whether there is a condition for stopping oscillation. From process S4e, since there is a condition that the external terminal “IN1” is “0” and fixed, the process proceeds to “YES” and proceeds to the next process S4h.
[0144]
Process S4h (FIG. 4): The conditions confirmed in process S4g are specified. For example, in this example, “if the external terminal“ IN1 ”is fixed at 0, there is no problem”.
[0145]
Process S4i (FIG. 4): Since the verification of the AND 7a is completed, the verification of another element is performed. The subsequent block NON-INVERTER 7b is selected as a new verification element, and the process proceeds to step S4j.
[0146]
Process S4j (FIG. 4): It is checked whether the current verification element NON-INVERTER 7b has returned to the start point in the currently verified loop discovered in process S1. Since the starting point is AND7a and the currently verified element is NON-INVERTER7b, the process proceeds to "NO" and proceeds to the next process S4b (second time).
[0147]
Process S4b (FIG. 4) -2: Check whether NON-INVERTER 7b is not XOR / XNOR (because it has been traced by another method in process S2). Since NON-INVERTER 7b is not XOR / XNOR, the process proceeds to “NO” and moves to the next process S4c-2.
[0148]
Process S4c (FIG. 4) -2: It is confirmed whether NON-INVERTER 7b has an oscillation stop condition. Referring to the library of FIG. 6, since there is no oscillation stop condition, the process proceeds to “NO”, and the process proceeds to process S4i-2.
[0149]
Process S4i (FIG. 4) -2: Since the verification of NON-INVERTER 7b has been completed, the process proceeds to verification of another element.
[0150]
The subsequent block OR7c is selected as a new element to be verified, and the process proceeds to S4j-2.
[0151]
Process S4j (FIG. 4) -2: It is confirmed whether or not the OR7c, which is the currently verified element, has returned to the start point in the currently verified loop found in Process S1. The starting point is AND7a. Since the currently verified element is OR7c, the process proceeds to “NO”, and the process proceeds to step S4b (third time).
[0152]
Process S4b (FIG. 4) -3: Check whether OR7c is not XOR / XNOR (because it was traced by another method in process S2). Since OR7c is not XOR / XNOR, the process proceeds to “NO” and proceeds to process S4c-3.
[0153]
Process S4c (FIG. 4) -3: It is confirmed whether OR7c has an oscillation stop condition.
[0154]
Referring to the library of FIG. 6, if input B = 1 is fixed, the oscillation can be stopped, so that the process proceeds to “YES”, and the process proceeds to the next process S4d-3.
[0155]
Process S4d (FIG. 4) -3: The input stage from the input terminal B which is outside the loop to the OR 7c is traced (subroutine). The process proceeds to the next process SRa-3.
[0156]
Process SRa (FIG. 5) -3: Traces the immediately preceding element from the other input terminal B outside the OR7c loop. The input B of the OR 7c is clamped at “0” (LOW). Control proceeds to the next process SRb-3.
[0157]
Process SRb (FIG. 5) -3: It is confirmed whether the element immediately before OR7c found in process SRa has visited before. Since it has not yet been visited, the process proceeds to “NO” and proceeds to the next process SRc-3.
[0158]
Process SRc (FIG. 5) -3: It is determined whether the value is fixed to any one of “0” / “1” / “X” (undefined) based on the preceding input of OR7c found in process SRa. In this case, since it is clamped at “0”, it is fixed at “0”, so the process proceeds to “YES”, and the process proceeds to step S4e-3.
[0159]
Process S4e (FIG. 4) -3: The oscillation stop condition is compared with the input value “0” from the other input terminal B outside the loop to OR7c obtained in process SRc-3. From the oscillation stop condition obtained in the process S4c-3, the oscillation is not stopped even if it is clamped at “0”. The process proceeds to the next process S4f-3.
[0160]
Process S4f (FIG. 4) -3: As a result of the process S4e-3, it is determined whether or not the oscillation stops. As a result, the oscillation does not stop, so the process proceeds to “NO”, and the process proceeds to the process S4i-3.
[0161]
Process S4i (FIG. 4) -3: Since the verification of the OR 7c is completed, the verification of another element is performed. The subsequent block AND7a is selected as a new verification element, and the process proceeds to step S4j-3.
[0162]
Process S4j (FIG. 4) -3: It is confirmed whether or not the AND7a, which is the currently verified element, has returned to the start point in the currently verified loop found in Process S1. The starting point is AND7a, and since the currently verified element is also AND7a, the process proceeds to “YES”, and the process proceeds to step S5.
[0163]
Process S5 (FIG. 1): The loop circuit location found in process S1 is clearly indicated, and the problem is displayed. In this example, AND7a, NON-INVERTER7a, and OR7c are clearly shown using unique names given for each block in the circuit data, and there is a possibility of oscillation on the actual machine, and the external terminal IN1 = 0 fixed. Clarify that there is no problem as long as it is used in.
[0164]
Process S6 (FIG. 1): Is there another loop found in process S1? → Proceed to “None” because there is no. (End of processing)
As described above, the present invention can supply a product with better quality by detecting a problematic circuit configuration and clearly specifying conditions for avoiding an oscillation state on an actual machine in advance. In addition, the analysis, discovery, and recovery TAT when a defect occurs, which takes several times to several tens of times that of normal development itself, can be completely cut.
[0165]
Furthermore, for each element, a library of information on the input conditions necessary to determine the output value regardless of the path where the signal polarity is inverted between the input and output terminals and other input values. It is possible to determine whether or not the oscillation loop configuration is established without depending on the circuit configuration.
[0166]
Furthermore, the library itself can be easily created and updated based on the truth value information 11.
[0167]
Next, a second embodiment to which the above-described verification method is applied will be described with reference to FIG. 8 showing a specific circuit example to be verified. In this example, XOR is included in the loop portion.
[0168]
The difference from the first embodiment described above is that when XOR / XNOR is included, signal polarity inversion and non-inversion change depending on the input value from the other input terminal outside the loop. It is in the point which cannot judge whether is a positive feedback loop or a negative feedback loop by a normal means.
[0169]
In the present invention, inversion and non-inversion verification can be performed by substituting INVERTER / NON-INVERTER for the case where the logic outside the input outside the loop is fixed. Even if it cannot be replaced, it also checks the input outside the loop of other blocks, and searches for the possibility of a pseudo error.
[0170]
Process S1 (FIG. 1): A loop configuration is found (application of a known technique as described above).
[0171]
It progresses to process S2. As an example, assume that only one loop of AND8a with INVERTER as shown in FIG. 8 → NON-INVERTER8b → 2-input XOR8c → AND8a with INVERTER is found.
[0172]
Process S2 (FIG. 1): XOR / XNOR process. That is, the process proceeds to process 2a.
[0173]
Process S2a (FIG. 2): Is there an XOR / XNOR in the loop found in process S1? -> Since XOR 8c exists, the process proceeds to "present" and proceeds to the next process S2b.
[0174]
Process S2b (FIG. 2): Traces the input stage from the other input terminal B outside the loop of the XOR 8c found in the process S2a.
[0175]
Process SRa (FIG. 5): Look at the previous stage where the input from outside the loop of XOR 8c comes from. The input from the other input terminal B which is outside the loop of the XOR 8c is clamped (8e) by LOW and fixed at the logic level “0”. The process proceeds to the next process SRb.
[0176]
Process SRb (FIG. 5): Has the clamp (8e) been visited before? → Since it has not been visited, the process proceeds to “NO” and proceeds to the next process SRc.
[0177]
Process SRc (FIG. 5): So far, is it determined whether the input from outside the loop of the XOR 8c is “0”, “1”, or “X”? → Since the input from outside the loop of XOR 8c is the LOW clamp (8e), the process proceeds to “YES” to determine “0”, and proceeds to process S2c.
[0178]
Process S2c (FIG. 2): Is it possible to replace XOR8c with INVERTER or the like in the loop found in process S1? → From the result of the process SRc, since the outside of the loop is fixed LOW, the truth value information 11 can be replaced with NON-INVERTER, and the process proceeds to the next process S2d.
[0179]
Process S2d (FIG. 2): XOR 8c in the loop found in process S1 is replaced with NON-INVERTER. Thereafter, analysis is performed on the circuit shown in FIG. 9 replaced internally, and the process proceeds to the next process S2e.
[0180]
Process S2e (FIG. 2): Are there other XOR / XNORs in the loop found in process S1? → Since there is no “verification continued”, the process proceeds to step S3.
[0181]
Process S3 (FIG. 1): It is determined whether the loop discovered in process S1 is a positive feedback loop or a negative feedback loop, and the process proceeds to process S3a.
[0182]
Process S3a (FIG. 3): When verifying each element, it is arbitrarily determined from which element the verification is started. It is assumed that AND (9a in FIG. 9) is assumed.
[0183]
Subsequent processes until the element to be verified in the process S3 moves to the NON-INVERTER 9c are the same as those in the first embodiment described above, and a description thereof will be omitted.
[0184]
Process S3d (FIG. 3) -2: Since the verification of the currently verified element is completed, the next stage element is selected as a new element to be verified. The process moves to the subsequent block NON-INVERTER (originally XOR8c) 9c, and proceeds to the next process S3e-2.
[0185]
Process S3e (FIG. 3) -2: Check whether the currently verified element has made a round on the loop found in process S1 and returned to the starting point? → The starting point is 9a, not 9c, so the process proceeds to “NO”, and the process proceeds to step S3b-2.
[0186]
Process S3b (FIG. 3) -3: It is determined whether the path to which the currently verified element is connected in the loop is included in the “logic inversion path” defined in the dedicated library (FIG. 6). . In the case of NON-INVERTER 9c in FIG. 9, since there is no logic inversion path when referring to the library, the process proceeds to “does not pass”.
[0187]
The subsequent operation is the same as that of the first embodiment described above, and a description thereof is omitted here.
[0188]
Next, a third embodiment to which the above-described verification method is applied will be described with reference to FIG. 10 showing a specific circuit example to be verified. In this example, a case where XOR / XNOR cannot be degenerated as in the second embodiment described above will be described.
[0189]
Here, the degeneration means that a redundant part or configuration can be replaced with a more simplified one. In this example, XOR / XNOR is replaced by BUFFER / It is to replace with INVERTER.
[0190]
If the degeneration cannot be performed, the loop inversion / non-inversion verification is not performed, and only the input outside the loop of other blocks is checked.
[0191]
Process S1 (FIG. 1): As an example of finding a loop configuration (application of a known technique), it is assumed that only one loop of AND10a with INVERTER → NON-INVERTER 10b → 2-input XOR10c → AND 10a with INVERTER is found as shown in FIG. Assume.
[0192]
Process S2 (FIG. 1): The XOR / XNOR process in the loop found in process S1 is performed. Move to processing S2a.
[0193]
Process S2a (FIG. 2): Is there an XOR / XNOR in the loop found in process S1? → Yes → Transfer to process S2b.
[0194]
Process S2b (FIG. 2): The input stage trace of the other input terminal B outside the XOR / XNOR loop found in process S2a is performed. That is, the process proceeds to the process SRa.
[0195]
Process SRa (FIG. 5): The input from the preceding block outside the XOR / XNOR loop found in process S2a is viewed. The input value from outside the loop of the XOR 10c comes from the sequential circuit 10e, and it is difficult to think that the value is fixed. The process proceeds to the next process SRb.
[0196]
Process SRb (FIG. 5): Has the sequential circuit 10e been visited before? → Because it has not been visited, the process proceeds to “NO” and proceeds to the next process SRc.
[0197]
Process SRc (FIG. 5): Is the output of the sequential circuit 10e determined to be “0”, “1”, or “X”? → Proceed to “YES” to confirm X. It returns to process S2c.
[0198]
Process S2c (FIG. 2): Can the XOR / XNOR found in process S2a be replaced with INVERTER or the like? → Since the input from outside the loop is not fixed, it cannot be replaced.
[0199]
The subsequent operations are the same as those in the first embodiment described above until the element to be verified in the process S4 moves to 10c, and thus the description thereof is omitted here.
[0200]
Process S4b (FIG. 4): The input value from the other input terminal outside the loop is traced, but since XOR / XNOR has already been verified, is the currently selected verification target element not XOR / XNOR? Confirm (because it has been traced by another method in process S2). Proceed to “YES” for XOR. That is, the input stage verification is skipped and the process proceeds to process S4i.
[0201]
Process S4i (FIG. 4): The next-stage element of the currently verified element is newly selected as the verification element. Here, AND10a is selected. Control goes to step S4j.
[0202]
Process S4j (FIG. 4): Has the element selected in process S4i returned to the start point? → The starting point is AND10a and the process proceeds to “YES”.
[0203]
Since the subsequent operation is the same as that of the first embodiment described above, description thereof is omitted here.
[0204]
Next, a fourth embodiment to which the above-described verification method is applied will be described with reference to FIG. 11 showing a specific circuit example to be verified. Here, an example in the case of a double loop configuration will be described.
[0205]
If there is a smaller negative feedback loop, for example, in the found loop, the trace will not be terminated during the input stage tracing. Small loops can be verified separately, and if the value is confirmed within a small loop, it can be discovered by continuing tracing after the loop cut. The input value outside the loop in the portion is indeterminate (X), and the trace is continued by cutting the loop once.
[0206]
Process S1 (FIG. 1): As an example of finding a loop configuration (this process is an application of known technology), a loop of NAND11a → INVERTER11b → NAND11c → AND11d → NAND11a as shown in FIG. Assume that it has been discovered.
[0207]
The subsequent operations are the same as those in the first embodiment described above until the verification element is moved to the NAND 11c in the process S4, and thus the description thereof is omitted here.
[0208]
Process S4b (FIG. 4): When tracing the input value from the other input terminal outside the loop, it is confirmed whether the currently verified element is not XOR / XNOR. As described above, the currently verified element is the NAND 11c and not the XOR. Therefore, the process proceeds to “NO”, and the process proceeds to the next process S4c.
[0209]
Process S4c (FIG. 4): Does the NAND 11c, which is the currently verified element, have an oscillation stop condition? → Referring to the library of FIG. 6, if the input A = 0 is fixed, the oscillation can be stopped, so that the process proceeds to “YES” and proceeds to the next process S4d.
[0210]
Process S4d (FIG. 4): The input value from the other input terminal A outside the loop of the element NAND11c is traced.
[0211]
Process SRa (FIG. 5): The element to be verified at present is the NAND 11c, but the AND 11d, which is the element immediately preceding from the outside of the loop, is newly selected as the element to be verified at present, and the process proceeds to the next process SRb.
[0212]
Process SRb (FIG. 5): Has this element AND11d been visited before? → Since it has not been visited, the process proceeds to “NO” and proceeds to the next process SRc.
[0213]
Process SRc (FIG. 5): It is determined whether the output value of the element AND11d is determined to be “0” / “1” / “X” (indeterminate), but it is impossible to determine only with this information Therefore, the process proceeds to “NO” and proceeds to the next process SRa (second time).
[0214]
Process SRa (FIG. 5) -2: The element to be verified at present is AND11d, but it comes from NAND11c (from input A) and NON-INVERTER11e (from input B), which are the previous stage elements. The two are selected as newly verified elements, and the process proceeds to the next process SRb-2.
[0215]
Process SRb (FIG. 5) -2: When these elements have been visited before, the AND 11c has visited before, so that the process proceeds to “YES” and proceeds to the next process SRd-2.
[0216]
Process SRd (FIG. 5) -2: Since this loop is NAND11c → AND11d → NAND11c, this path is cut. The input A of the NAND 11c is determined as indeterminate (X), and the process proceeds to the next process SRc-2.
[0217]
Process SRc (FIG. 5) -2: From process SRd-2, the input A of the NAND 11c is determined to be indeterminate (X), and the process returns to process S4e.
[0218]
Process S4e (FIG. 4): Finally, the process returns to the NAND 11c, which is the element verified in the loop, and compared with the oscillation stop condition. The oscillation stop condition obtained in process S4c is not satisfied. The process proceeds to the next process S4f.
[0219]
Process S4f (FIG. 4): Since the oscillation cannot be stopped by the input value from process S4e, the process proceeds to “NO” and proceeds to process S4i.
[0220]
Process S4i (FIG. 4): The next-stage AND11d is newly selected as the currently verified element, and the process proceeds to process S4j.
[0221]
Process 4S4j (FIG. 4): Is the element selected in process S4i selected as the starting point when first entering process S4? → Since the starting point is AND11a, the process proceeds to “NO” and proceeds to the process S4b (second time).
[0222]
Process S4b (FIG. 4) -2: Confirm whether AND11d selected in process S4i is not XOR / XNOR? → Proceed to "NO" and proceed to the next process S4c-2.
[0223]
Process S4c (FIG. 4) -2: Does the AND 11d selected in process S4i have the oscillation stop condition in the dedicated library (FIG. 6)? → If the input B is fixed at “0”, the oscillation is stopped to proceed to “YES”, and the process proceeds to the next process S4d-2.
[0224]
Process S4d (FIG. 4) -2: In order to trace the input from outside the loop of AND11d selected in process S4i, the process proceeds to subroutine SRa-3.
[0225]
Process SRa (FIG. 5) -3: The previous element from outside the loop of AND11d is confirmed. The input B of the AND 11d comes from the NON-INVERTER 11e. Control proceeds to the next process SRb-3.
[0226]
Process SRb (FIG. 5) -3: Check whether the NON-INVERTER 11e selected in the process SRa-3 is a previously visited element. → Since it has not been visited, the process proceeds to “NO” and proceeds to the next process SRc-3.
[0227]
Process SRc (FIG. 5) -3: It is determined whether the output value from the element selected in process SRa-3 is fixed to “0” / “1” / “X” (indeterminate). It comes from the output of NON-INVERTER 11e, and it is not known from this information alone. Return to process SRa-4.
[0228]
Process SRa (FIG. 5) -4: Traces one more stage before NON-INVERTER 11e. The input A of NON-INVERTER 11e comes from LOW_CLAMP (clamped LOW) 11g. The process proceeds to the next process SRb-4.
[0229]
Process SRb (FIG. 5) -4: Has the element selected in Process SRa-4 been visited before? → Since it has not been visited, the process proceeds to “NO” and proceeds to the next process SRc-4.
[0230]
Process SRc (FIG. 5) -4: It is determined whether the output value of the element selected in process SRa-4 is fixed to “0” / “1” / “X” (indeterminate). The LOW_CLAMP 11g discovered in the process SRa-4 is connected to the input terminal B of the AND 11d via the NON-INVERTER 11e. As a result, only “0” appears from the AND 11d.
[0231]
Since the subsequent operation is the same as that of the first embodiment described above, description thereof is omitted here.
[0232]
【The invention's effect】
As described above, the detection method of the oscillation constituent location in the loop circuit of the present invention is a loop detection means for detecting a prohibited negative feedback loop among the loop circuits by the positive feedback and the negative feedback in the internal circuit at the logic verification stage. Information on input conditions necessary to determine the output value regardless of the input value of the other input terminal and the path where the signal polarity is inverted between at least one input terminal and the output terminal of each element constituting the internal circuit Are created and updated based on predetermined truth value information to create a library in the storage means of the logic verification device, and it is determined whether the internal circuit configuration is an oscillation loop configuration while quoting the library. Because the judgment result is displayed on an external display means, it is possible to detect a problematic circuit configuration and avoid an oscillation state on the actual machine. Conditions or the like can be pre-explicitly for the reason, it is possible to supply a better quality of products.
[0233]
In addition, the analysis, discovery, and recovery TAT when a defect occurs, which usually takes several times to several tens of times that of development itself, can be completely cut.
[0234]
In addition, for each element, a library that contains information on the path that inverts between input and output, and information on the input conditions necessary to determine the output regardless of other input values. It is possible to easily determine whether or not the oscillation loop configuration has been established without depending on it.
[0235]
Furthermore, the library itself can be easily created and updated based on truth value information.
[Brief description of the drawings]
FIG. 1 is an overall flowchart showing a method for detecting an oscillation component in a loop circuit according to an embodiment of the present invention.
FIG. 2 is a detailed flowchart of processing S2.
FIG. 3 is a detailed flowchart of processing S3.
FIG. 4 is a detailed flowchart of processing S4.
FIG. 5 is a detailed flowchart of processes S2b and S4d.
FIG. 6 is a diagram illustrating an example of a library.
FIG. 7 is a diagram showing a circuit example of a first embodiment to which the verification method of the present invention is applied.
FIG. 8 is a diagram showing a circuit example of a second embodiment to which the verification method of the present invention is applied.
9 is a diagram in which XOR 8c in FIG. 8 is replaced with NON-INVERTER 9c.
FIG. 10 is a diagram showing a circuit example of a third embodiment to which the verification method of the present invention is applied.
FIG. 11 is a diagram showing a circuit example of a fourth embodiment to which the verification method of the present invention is applied.
FIG. 12 is a diagram illustrating a circuit example for explaining a conventional verification method;
FIG. 13 shows a waveform diagram of a simulation result.
FIG. 14 is a diagram showing input / output waveforms of a NAND on an actual machine.
[Explanation of symbols]
11 Truth information
12 Library
7a, 8a, 9a, 10a AND with INVERTER
7b, 8b, 9c, 10b, 11e, 12b NON-INVERTER
7c OR
8c, 10c XOR
10e Sequential circuit
11a, 11c, 12a NAND
11b INVERTER
11d AND
11g LOW_CLAMP
12c HIGH_CLAMP

Claims (8)

A circuit logic verification device,
  For each type of element, a logic inversion path between the input and output terminals, and a logic inversion path oscillation stop condition storage means storing an oscillation stop condition that is a condition of the input terminal where the output terminal is a fixed output,
  Loop detection means for detecting a loop circuit included in the circuit to be verified;
  For each element included in the loop path of the detected loop circuit, the logic inversion path oscillation stop condition storage means is referred to, and the connection between the input terminal and the output terminal of the element in the loop path corresponds to the logic inversion path. Positive / negative feedback check means for determining whether the loop circuit is a positive feedback loop or a negative feedback loop, and counting the number of logic inversion paths included in the loop path,
  When it is determined that the positive / negative feedback check means is a negative feedback loop, for each element included in the loop path of the loop circuit, the logic inversion path oscillation stop condition storage means is referred to and the input terminal of the element If the input terminal not included in the loop path satisfies the oscillation stop condition, it is determined that there is no problem with the loop circuit. Depending on the input terminal condition, if the oscillation stop condition is satisfied, the condition is clearly indicated. An external input check means,
  A logic verification apparatus characterized by clearly indicating a determination result as to whether or not the circuit configuration is an oscillation loop configuration and a condition for avoiding an oscillation state. It is detected whether an exclusive OR or an exclusive negative OR exists in an element included in the loop path of the loop circuit, and if detected, an input terminal not included in the loop path of the element is detected. Trace the input value back to the previous stage, and the input of the input terminal is clamped, and the exclusive OR or exclusive negative OR can be reduced to an inverter or non-inverter depending on the clamped input value. Further comprises an exclusive logic processing means for degeneration,
  When the exclusive logic processing means performs the degeneration, for the degenerated loop circuit,
  2. The logic verification apparatus according to claim 1, wherein determination is performed by the positive / negative feedback check means and the out-of-loop input check means. As a result of tracing the input value of the input terminal not included in the loop path of the element for the exclusive logical sum or exclusive negative logical sum as a result of the exclusive logical processing means, when the input of the input terminal is uncertain, 3. The logic according to claim 2, wherein the determination by the out-of-loop input check means is performed for elements other than the exclusive logical sum or exclusive negative logical sum without performing the determination by the positive / negative feedback check means. Verification device. The input value trace of the input terminal by the exclusive logic processing means is an input value trace that stops the input value trace and processes the input value as indeterminate when the input terminal is included in another small loop. 4. The logic verification apparatus according to claim 3, wherein The out-of-loop input check means traces the input value of the input terminal not included in the loop path back to the previous stage, and determines whether or not the oscillation stop condition is satisfied based on the traced input value. The logic verification device according to claim 1, wherein the logic verification device is characterized in that: The input value trace of the input terminal by the out-of-loop input check means is an input value trace that stops the input value trace and processes the input value as indeterminate when the input terminal is included in another small loop. 6. The logic verification device according to claim 5, wherein: The input value trace of the input terminal by the out-of-loop input check means is traced back to the previous stage. 7. The logic verification apparatus according to claim 5, wherein the input value is treated as indefinite when connected to the output logic of the terminal connection of the part. The input value trace of the input terminal by the out-of-loop input check means treats the input value as uncertain if the value is not confirmed or uncertain even after any specified number of stages. The logic verification device according to any one of 5 to 7.

Images