Abstract:
A hazard check method and device for making hazard checks of logic circuits containing asynchronous paths and multi-cycle paths. The hazard check device includes a means for equivalent conversion to only pre-embedded conjunctive normal form blocks if not all of the blocks in the logic circuit were embedded conjunctive normal form blocks; a means for tracing each termination point recorded in the signal information from the logic circuit, inputting the signal information to the circuit up to the flip-flop, and assigning numerals to each net; and a means for tracing each termination point recorded in the signal information from the logic circuit, referring to the logic library for each block, and searching for the same logic conjunctive normal form (CNF) as in the logic library, and substituting the conjunctive normal form into the numerals assigned to the connected network, and outputting it as the circuit conjunctive normal form; and a means for adding a circuit conjunctive normal form whose logic is equivalent to that numeral, to each net for each termination point recorded in the signal information.

Description:
BACKGROUND OF THE INVENTION 
       [0001]    1. Field of the Invention 
         [0002]    The present invention relates to a hazard check method and a hazard check device for checking logic circuit hazards, as well as to a circuit conjunctive normal form (also called CNF) generating method and circuit CNF generating device for generating circuit conjunctive normal forms utilized in hazard check devices and hazard check methods. 
         [0003]    2. Description of the Related Art 
         [0004]    Systems for generating logic circuits from functions written in hardware terminology are capable of generating circuits just as described in the hardware terminology. However these systems do not take glitches into account during logic optimizing. Synthesizing paths with exceptional timing such as asynchronous paths and multi-cycle paths causes glitches and a hazard occurs when these glitches are conveyed at the timing for inputting data to the flip-flop data, so that the circuit (mistakenly triggers) operation is defective. Moreover, no method was available for detecting these hazards. 
         [0005]    The following is a typical case where a hazard is generated at an exceptional timing. First of all, as shown in  FIG. 2 , a control signal (strobe signal) is installed for controlling whether or not to input data from an exceptional timing path. When that control signal is 0, nothing is input since that exceptional timing path was not set. Conversely, when the control signal is 1, the signal is input. The circuit in  FIG. 2  is designed so that no changes in asynchronous paths and multi-cycle paths will ever be conveyed to the flip-flop when that control signal is 0. 
         [0006]    However, systems for synthesizing logic circuits might include the circuit of  FIG. 3 . This circuit is logically identical to that in  FIG. 2 ; however, this circuit conveys data changes caused by effects from the exceptional timing path to the flip-flop even when the control signal is 0. When these changes occur, the flip-flop clock signal (pulse) rises and causes faulty logic circuit operation (hazard). 
         [0007]    Technology for checking these type of hazards was disclosed for example in Japanese Unexamined Patent Publication No. JP 2(1990)-112773A for selecting a logic gate from among the logic gates in the digital circuit for a hazard check, and then making a hazard check using judgment criteria described in the hazard generating conditions for that gate. 
         [0008]    Also as disclosed for example in Japanese Unexamined Patent Publication No. JP 5(1993)-35816 A, the input conditions in a simulation for detecting a hazard include not only “0” and “1”, but “x” which is neither “0” nor “1”, or in other words is an unfixed level. 
         [0009]    Technology was also disclosed for example in, “Fast Hazard Detection in Combinational Circuits”, by C. Jeongand S. M. Nowick, in In Proc. of Design Automation Conference 2004, pp. 592-595 where in  FIG. 1 , the signal states for inducing a hazard are six types other than 0 and 1. 
       SUMMARY OF THE INVENTION 
       [0010]    The present invention has the object of providing a hazard check method and a hazard check device for checking for hazards in logic circuits containing a synchronous paths and multi-cycle paths, and also a circuit conjunctive normal form (CNF) generating method and circuit conjunctive normal form generating device for generating circuit conjunctive normal forms utilized in hazard check devices and hazard check methods. 
         [0011]    A first aspect of the present invention provides a circuit conjunctive normal form generating method, including: reading a logic circuit and an information of an end point; outputting logic operation of a section from a start point traced from said end point to said end point in a conjunctive normal form; and setting a logic equivalent to a hazard to said end point and a net where exceptional timing signal exists. 
         [0012]    A second aspect of the present invention provides a hazard check method, including: reading a logic circuit and an information of an end point; outputting logic operation of a section from a start point traced from said end point to said endpoint in a conjunctive normal form; setting a logic equivalent to the hazard to said end point and said net where exceptional timing signal exists; and making a hazard check by deciding a satisfiability of said circuit conjunctive normal form. 
         [0013]    The first effect is an all-inclusive check for the occurrence of hazards. 
         [0014]    The reason for this is that the possibility of a hazard occurring is converted into a satisfiability problem, and an all-inclusive check is made on that problem. 
     
     
       BRIEF DESCRIPTION OF-THE DRAWINGS 
         [0015]      FIG. 1  is a block diagram showing the structure of the hazard check device of the first embodiment of this invention; 
           [0016]      FIG. 2  is a diagram showing a typical circuit prior to logic synthesis; 
           [0017]      FIG. 3  is a circuit diagram showing a typical circuit generated when a logic synthesizing device was applied to the circuit shown in  FIG. 2 ; 
           [0018]      FIG. 4  is a concept circuit diagram showing an example of a circuit to be checked by the hazard check device of the embodiment of this invention; 
           [0019]      FIG. 5  shows example of signal information in the circuit shown in  FIG. 4 ; 
           [0020]      FIG. 6  is a table showing a 3-value expression by the embodiment of this invention; 
           [0021]      FIG. 7  is a diagram showing parameters resulting when the 3-value expression was applied to a NOR gate in the embodiment of this invention; 
           [0022]      FIG. 8  is a table expressing the NOR gate input/output relation for the 3-value expression in the embodiment of this invention; 
           [0023]      FIG. 9  is another table expressing the NOR gate input/output relation for the 3-value expression in the embodiment of this invention; 
           [0024]      FIG. 10  shows logic conversion to be utilized in the embodiment of this invention; 
           [0025]      FIG. 11  is a table expressing the NOR gate as a circuit conjunctive normal form (CNF) in the embodiment of this invention; 
           [0026]      FIG. 12  shows a sequence of numbers converted from the formula shown in  FIG. 11 , so as to input to the satisfiability decision unit; and 
           [0027]      FIG. 13  shows a sequence of numbers showing the circuit conjunctive normal form (CNF) for checking the hazard in the circuit shown in  FIG. 4 . 
           [0028]      FIG. 14  is a flow chart showing example of operation of checking the hazard in the circuit shown in  FIG. 1 ; 
           [0029]      FIG. 15  is a flow chart showing example of operation performed in step S 2  of  FIG. 14 ; 
           [0030]      FIG. 16  is a flow chart showing example of operation performed in step S 3  of  FIG. 14 ; 
       
    
    
     DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENT 
       [0031]    The preferred embodiments of this invention are described next while referring to the drawings. 
         [0032]    The present invention makes an all-inclusive check of whether a hazard has occurred in circuits synthesized by logic synthesizing systems for paths with exceptional timing such as asynchronous and multi-cycle paths. 
         [0033]    The description is given while referring to  FIGS. 1 and 14 . This method starts up from an input device  1  (step S 1 ). A logic extractor unit  21  reads a logic circuit  31  after generation by logic synthesis as the logic synthesis results, traces from the circuit output and input pin of the flip-flop with the signal information subject to verification, to the input side, upto the flip-flop or the circuit input (it is called as start point), and refers to the logic information of each block stored in the logic library  32 , and outputs the logic operation of the subject section of the circuit expressed as a 3-value (0, 1, X) circuit operation, in the circuit conjunctive normal form (hereafter called CNF)  34  (step S 2 ). 
         [0034]    A boundary condition setter unit  22  reads the signal information  33  and adds boundary condition to the circuit CNF  34  (step S 3 ). That is, a boundary condition setter unit  22  specifies an X value for exceptional timing signals (asynchronous signals or multi-cycle signals); a logic value (specified value) so that signals with exceptional timing will not be conveyed to the control signal; and both logic values of 0 or 1 for other signals (usual synchronization signals) and adds these to the circuit CNF  34 . 
         [0035]    A satisfiability decision unit  23  reads the circuit CNF  34  and makes an all-inclusive search to find whether there is a solution to satisfy these values (step S 4 ). 
         [0036]    The satisfiability decision unit  23  is conventionally comprised of a particular section, and the section that generates the circuit CNF  34  is a section conforming to this invention. 
         [0037]    Documents of the conventional art relating to the satisfiability problem are described next:
       “Introduction to Logic Calculation” by Hisao Tanaka (author), honorary professor at Hosei University, pp. 118-124, published October 1997, ISBN4-7853-1505-9, Chapter 5 Calculation quantity problems involving propositional logic, 5.1 Satisfiability problem,   “Clarifying computer principles: Automaton Linguistic Theory and Computational Theory” by Akira Maruoka (author) professor at Tohoku University, pp. 234-241, ISBN4-7819-1104-8 published November 2005, by SAIENSU-SHA Co., Ltd., 9.6 Review of formula satisfiability problems for circuit satisfiability problems, and   GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactionson Computers, Vol. 48, No. 5, 1999, pp. 506-521.       
 
         [0041]    The circuit CNF is read by the satisfiability decision unit  23  in the related art; however, it also conforms to this invention. 
         [0042]    If the satisfiability decision unit  23  discovers a satisfaction solution then the result output unit  24  reports a hazard to the verification results  35  and if there is no satisfaction solution reports that there is no hazard to the verification results  35  (step S 5 ). 
         [0043]    The structure of the embodiment of this invention is next described in detail while referring to the drawings. 
         [0044]    The structure is described next while referring to  FIG. 1 . 
         [0045]    This invention includes an input device  1  such as a keyboard, a data processing device  2  for programming control operations, and a storage device  3  for storing information. 
         [0046]    The storage device  3  stores a logic circuit  31 , a logic library  32 , signal information  33 , a circuit CNF  34 , and a verification results  35  as data. 
         [0047]    The logic circuit  31  is the logic circuit to be checked. 
         [0048]    The logic library  32  is a library expressing the logic for each gate. 
         [0049]    The signal information  33  is a list of start/end point signal names for exceptional timing paths, and strobe signal names for controlling the exceptional timing signals, and logic values at the time that signal does not convey the exceptional timing signal. 
         [0050]    The circuit CNF  34  is a formula expressing the conjunctive normal form of the section to be checked (verified). The circuit CNF in the format as shown in  FIG. 11  is a sum-product Boolean type format. 
         [0051]    The verification results  35  is check results on whether a hazard will occur or not. 
         [0052]    The data processing device  2  includes a logic extractor unit  21 , a boundary condition setter unit  22 , a satisfiability decision unit  23 , and a result output unit  24 . 
         [0053]    The logic extraction unit  21  reads the logic circuit  31 , extracts the outputs one at a time from the flip-flop and circuits forming the end point for the exceptional timing signal recorded in the signal information  33 , traces them from that input side to the output pin of the flip-flop or input of the circuit, checks the logic on that input side with the logic library  32 , and converts that logic to the circuit CNF  34 . 
         [0054]    The boundary setter unit  22  refers to the signal unit  33 , and specifies an X value for start/end points of exceptional timing signals; specifies a designated logic value for strobe signals, specifies a designated 1-cycle signal for other input signals and adds and outputs those values to the circuit CNF  34 . 
         [0055]    The satisfiability decision unit  23  reads the circuit CNF  34  and makes an all-inclusive decision on whether there is a solution satisfying that CNF (conjunctive normal form) or in other words where an X value will be conveyed to that end point. 
         [0056]    If there is a satisfaction solution, then that circuit might generate a hazard, and if there is no solution then there is no possibility of a hazard. The result output unit  24  reports these results (possible hazard or no hazard) to the verification results  35 . 
         [0057]    The operation of the first embodiment of this invention is described next while referring to  FIG. 1 . 
         [0058]    First of all,  FIG. 4  shows an example of the logic circuit  31  for input. 
         [0059]      FIG. 5  shows an example of the signal information  33 . Here, the first line is an asynchronous path, from an input labeled multi-async (start point) (present in  FIG. 4 ) to a register (present in  FIG. 4 ) labeled the A_reg (end point), indicating this is a false path with no timing restrictions and is not 1 cycle operation. In the second line, the input (present in  FIG. 4 ) labeled strb is the control signal. When this value is 0, it indicates the above described path is inactive (does not convey the signal). 
         [0060]    Logic expressions used in this method are described next before starting a detailed description. This method utilizes three values 0, 1, X for circuit operation but a typical satisfiability problem only uses binary (two values) of 0 and 1. Internal expressions therefore utilize two variables for 0, 1, X. An example is shown in  FIG. 6 . Here 0 is expressed as (0, 0), 1 as (0,1), and X as (1,1). Note that there is no (1,0) (This combination of values was used here but other combinations may also be used.). 
         [0061]    A simple example using these logic values expresses the NOR gate input/output relation in  FIG. 7  as shown in  FIG. 8 . One input for example (i 1 , i 2 ) while the other input is (j 1 , j 2 ). When these inputs are respectively (0,0) and (0,1), then a (0,0) is output as shown here. This operation is equivalent to outputting a 0 when a 0 and a 1 are input and is called binary logic. A truth table as shown in  FIG. 9  can be derived from these results (.This truth table is not unified.). 
         [0062]    The truth table results are converted into the relation A→B (formula 1) (If A is established, the B is also established.) such as shown in the upper formula in  FIG. 10 . Moreover, as shown in  FIG. 10 , A→B can be converted into the Boolean expression A′+B=1 (formula 2). Here, the apostrophe (′) indicates a logic inversion. 
         [0063]    Each line of the truth table in  FIG. 9  is converted into the A→B format in the  FIG. 11  formulas, and those conversion results shown in the format of (formula 2). For example, 
         [0000]        i 1′* i 2→ o 1′* o 2′ 
         [0064]    is a format expressing the first line of  FIG. 9  as the formula 1, and 
         [0000]      ( i 1+ i 2′+ o 1′)( i 1 +i 2 ′+o 2′) 
         [0065]    is a format expressing the first line of  FIG. 9  as the formula 2. 
         [0066]    The formulas in  FIG. 11  are always established for the two-input NOR gate, and so can be summarized in the following formula 3. 
         [0000]    
       
         
           
             
               
                 
                   
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           j 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           j 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           2 
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           1 
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           2 
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           1 
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           1 
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           2 
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           2 
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           1 
                         
                       
                       ) 
                     
                     × 
                     
                       ( 
                       
                         
                           i 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           i 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             1 
                             ′ 
                           
                         
                         + 
                         
                           j 
                            
                           
                               
                           
                            
                           
                             2 
                             ′ 
                           
                         
                         + 
                         
                           o 
                            
                           
                               
                           
                            
                           2 
                         
                       
                       ) 
                     
                   
                   = 
                   1 
                 
               
               
                 
                   ( 
                   
                     formula 
                      
                     
                         
                     
                      
                     3 
                   
                   ) 
                 
               
             
           
         
       
     
         [0067]    In other words, the product of the items for each line of  FIG. 9  expressed in the format of (formula 2) are the left side of (formula 3). 
         [0068]    The following conversion is made to allow the data processor device (computer)  2  to convert it to any easy to use format. Namely, i 1  is expressed as 1, i 2  as 2, j 1  as 3, j 2  as 4, o 1  as 5, and o 2  as 6, and each negation (logic inversion) is shown by a minus. Also, the formula within the parentheses in (formula 3) is expressed by one line, the + (or) is omitted (not shown), and is a blank. These results are shown in  FIG. 12 . Namely, expressing (formula 3) in the format as shown in  FIG. 12 , allows input by the satisfiability decision unit  23 . The 0 at the end of each line indicates the termination of that item. This format is generally also called CNF by those in this field but in this invention is called the conjunctive normal form. In this system, the conjunctive normal form for the combination of logic circuit elements used in the logic circuit is embedded internally beforehand. 
         [0069]    The operation is described next referring to  FIG. 15 . 
         [0070]    The logic extractor unit  21  includes the following steps. 
         [0071]    Step  1 : The logic circuit  31  is read (step S 11 ). If the conjunctive normal form is not pre-embedded as to all blocks within the logic circuit then equivalent conversion is performed on blocks the conjunctive normal form of which is not embedded (step S 12 ). It is generally known that all logic circuits can be equivalently converted with an inverter and a two-input NOR gate. 
         [0072]    Step  2 : End points recorded in the signal information  33  are selected in sequence, one each from the logic circuit  31 . The following steps are performed on all end points (step S 13 ). 
         [0073]    Step  3 : The input side is traced from the selected end points, and two numerals (n 1 , n 2 ) are assigned in order starting from 1 for each net (step S 14 ) (Tracing back from the end point, the first net is (1,2) and from thereon continues as (3, 4) (5, 6). The trace is made from the circuit input up to the flip-flop.). 
         [0074]    Step  4 : The circuit is again traced from the end point to the input side, and the logic library  32  is referred to for each block, and a search made for logic of the same conjunctive normal form, the conjunctive normal form is substituted into numerals assigned to each connected net, and is output as the circuit CNF  34  (step S 15 ). 
         [0075]    Step  5 : The combination (1, 0) cannot occur in each net, so the logic equivalent to n 1 ′+n 2  (formula 4) is added to the circuit CNF  34  (step S 16 ). 
         [0076]    It is judged if the steps S 14  to S 16  are performed on all end points (step S 17 ). If No, the step S 13  is performed. 
         [0077]    The above steps are described while referring to  FIG. 4  and  FIG. 5 . 
         [0078]    Step  1 : The logic circuit  31  is read. This was read as per  FIG. 4  but in this example, there are only two-input NOR gates in the combination logic circuit blocks so the process proceeds to the next step. 
         [0079]    Step  2 : Read the signal information  33  ( FIG. 5 ) and set A-reg as the end point. 
         [0080]    Step  3 : A trace is made toward the input from A_reg, and (1,2) is assigned to net N001, (3,4) to N003, (5,6) to multi_async, (7,8) to other, (9,10) to N002, and (11, 12) to strb. In this example, the trace was made in sequence from the input pins below the block; however, the trace may also be made from the upper pins. 
         [0081]    Step  4 : A trace is again made to the input side from A_reg. A check of the logic library UO 1  is first of all made, and the circuit is two-input NOR gates so the embedded conjunctive normal form of the two-input NOR gate is extracted. This is expressed in  FIG. 12 . However, the numbers are made to match the node numbers. For example in the case of  FIG. 12 , the inputs are (1, 2) (3, 4) and the output is (5, 6), however the input for UO 1  is (3, 4) of N003, and (9, 10) of N002, and the output is (1, 2) of N001 so the inputs and output are substituted into these node numbers, and output to the circuit CNF  34 . Those results therefore correspond to line  1  through line  12  of  FIG. 13 . 
         [0082]    The same processing is subsequently performed for all gates to generate up through line  36  in  FIG. 13 . 
         [0083]    Step  5 : Logic incorporating the formula 4 is then output to all nets The result for net N 001  for example is −1, 2. That result corresponds to lines  37  through line  42  in In  FIG. 13 , the line  1  up to line  24  are written on the left side, while lines  25  and onward are written on the right side. 
         [0084]    The steps performed by the boundary condition setter unit  22  in S 4  of  FIG. 14  are described while referring to  FIG. 16 . 
         [0085]    The boundary condition setter unit  22  reads the signal information  22 , and outputs (1, 1) equivalent to X for the end point, adding the logic setting to the circuit CNF  34  (step S 21  in  FIG. 16 ). However, even specifying (1, ?) from formula 1 will yield an identical value to (1, 1) so (1, ?) may be output as a substitute for (1, 1). 
         [0086]    The specified logic value is set to the control signal (start point) (step S 22  in  FIG. 16 ). In other words, if 0 is specified then the logic setting (0, 0) for the control signal is added to the circuit CNF  34 , and if a 1 is specified then the logic setting (0, 1) at the control signal is added. 
         [0087]    For start points of exceptional timing signals, (1, 1) equivalent to X, is set, and the logic setting showing that is added to the circuit CNF  34  (step S 23  in  FIG. 16 ). However, even if a (1,?) is specified per formula 1, this value is equivalent to (1, 1) so a (1, ?) is output instead of (1, 1). 
         [0088]    For start points of other signals, either a 0 or a 1 can be used so a (0, ?) is set, and the logic setting showing that is added to the circuit CNF  34  (step S 24  in  FIG. 16 ). (Here, an ? signifies that nothing was specified.) 
         [0089]    In the case of  FIG. 5 , a (1, ?) equivalent to X is specified for A_reg, however that net is already assigned to (1, 2) at N 001  so a 1 is output (line  43  in  FIG. 13 ). 
         [0090]    The multi-async is an exceptional timing signal so a (1, ?) is applied. In that case, the multi-async net is assigned to (5, 6) so that a 5 is output (line  44  of  FIG. 13 ). 
         [0091]    For the control signal, a 0 is applied to the strb, so that (0, 0) is set. An (11, 12) are assigned to the strb net so that a −11 and −12 are output (line  45 ,  46  of  FIG. 13 ). 
         [0092]    The other of other signals is 0 or 1, and the net other is assigned to (7, 8) so that a −7 is output (line  47  of FIG. 13). 
         [0093]    When the control signal is the applied logic value in the circuit CNF  34 , and further under the condition that the exceptional timing signal start point is X, a satisfiability decision is made on whether the end point of the exceptional timing signal is X or not, after first considering all 0, 1 combinations of other input signals. 
         [0094]    The satisfiability decision unit  23  reads the circuit CNF  34 , and makes an all-inclusive search for a satisfaction solution. If there is a satisfaction solution, then that is decided, if not, then it is decided there is no satisfaction solution. In the current example, it is decided there is no satisfaction solution. 
         [0095]    If there is no satisfaction solution, the result output unit  24  reports there is no hazard. However if there is a satisfaction solution, then it reports the potential hazard to the verification results  35 . 
         [0096]    The effect of the first embodiment of this invention is described next. 
         [0097]    In the first embodiment of this invention, the satisfiability decision unit  23  makes an all-inclusive search of the circuit CNF  34  made by the logic extractor unit  21  and boundary condition setter unit  22  for a potential hazard occurrence to render the effect that a complete check can be made for conveyance of a hazard.