JP4268620B2 - Circuit description language equivalence checking method and equivalence checking device - Google Patents

Description

  The present invention relates to a method for verifying equivalence of circuit description languages. In particular, the present invention relates to verification of equivalence between a RTL (Register Transfer Level) and a design description using a description language at a higher level than the RTL.

  Conventionally, a hardware description language (HDL) such as VHDL has been used for designing an LSI (Large Scale Integrated circuit) product. LSI design data described in such a language is hereinafter referred to as RTL description (hereinafter, LSI design data in various languages may be collectively referred to as hardware design description).

  In recent years, a language in which a general-purpose programming language such as C language is extended to hardware (for example, SystemC) has begun to be used as an LSI design language. The design data obtained in this case (hereinafter referred to as function description) does not have the concept of time unlike the RTL description, and has the advantage that the description amount is smaller than that of the RTL description.

The function description is converted into an RTL description using a synthesis tool, and then converted into design data at a logic circuit level. At this time, the function description and the RTL description must be functionally equivalent, and it is necessary to verify equivalence between the two. There are several proposals for verifying this equivalence (see, for example, Patent Document 1). However, the conventional method requires a very large amount of calculation and requires a long time for verification. was there.
JP 2005-316595 A

The present invention provides a circuit description language equivalence checking method and an equivalence checking device that can be easily verified.

In the circuit description language equivalence verification method according to one aspect of the present invention, the CPU synthesizes the first design data related to the semiconductor integrated circuit described in the first circuit description language, and the first description language Obtaining second design data described in a second circuit description language having a lower abstraction level and storing the second design data in a memory device; and the CPU synthesizes the second design data with a circuit, Obtaining first circuit information including a data path connected to the computing unit, and first control information for controlling a data flow in the first circuit information, and storing the first control information in the memory device; CPU synthesizes the third design data described in the second circuit description language, and includes second circuit information including an arithmetic unit and a data path connected to the arithmetic unit, and the second circuit information Data flow Obtaining the second control information for controlling this and storing it in the memory device; the CPU compares the first and second circuit information to verify the correspondence; Verifying whether the first and second circuit information are equivalent, and the CPU performs formal verification on the first and second control information to determine whether the first and second circuit information are equivalent. Verifying whether or not the two control information is equivalent, and if the first and second circuit information are equivalent and the first and second control information are equivalent, the first It is determined that the design data and the third design data are equivalent, and the CPU is obtained by synthesizing the second circuit description language when verifying the correspondence between the first and second circuit information. A computing unit, a data path connected to the computing unit, and the first circuit A library holding a correspondence relationship with a predicate language is read from the memory device, and it is checked whether or not the first and second circuit information are at least partially corresponding to each other. The formal verification is performed, and when the CPU verifies whether or not the first and second control information are equivalent, a state transition condition regarding a plurality of states that the first control information can take, and the first 2 Compare the state transition conditions regarding a plurality of states that can be taken by the control information, determine that the parts having the same state transition conditions are equivalent, and perform the formal verification on the parts that are not the same.

An equivalence verification apparatus for a circuit description language according to an aspect of the present invention includes first design data related to a semiconductor integrated circuit described in a first circuit description language and a lower abstraction level than the first circuit description language. An equivalence checking device for verifying whether or not second design data described in a two-circuit description language is equivalent, wherein the first design data is synthesized and described in the second circuit description language. First circuit information including a computing unit and a data path connected to the computing unit, and a data flow in the first circuit information First circuit control information is obtained, and the second design data is further synthesized, and second circuit information including a computing unit and a data path connected to the computing unit, and data in the second circuit information Control to control the flow A circuit synthesizing means for obtaining information, a computing unit obtained by synthesizing the second circuit description language, a data path connected to the computing unit, and a library in which a correspondence relationship between the first circuit description language is recorded The memory device to be held and the first and second circuit information are compared to verify the correspondence relationship, and the non-corresponding portion is formally verified to determine whether or not the first and second circuit information are equivalent. Data path comparison means for verification, and control section comparison means for performing formal verification on the first and second control information and verifying whether or not the first and second control information are equivalent, The data path comparison means refers to the library in the memory device to verify whether or not the first and second circuit information corresponds at least partially, and performs the formal verification on the non-corresponding portion. The control unit comparing means The state transition conditions relating to the plurality of states that can be taken by the first control information are compared with the state transition conditions concerning the plurality of states that can be taken by the second control information, and parts having the same state transition conditions are equivalent. And the formal verification is performed for non-identical parts .

According to the present invention, it is possible to provide an equivalence checking method and an equivalence checking device for circuit description languages that can be easily verified.

  Embodiments of the present invention will be described below with reference to the drawings. In the description, common parts are denoted by common reference symbols throughout the drawings.

  A circuit description language equivalence checking method according to the first embodiment of the present invention will be described. First, a rough design method of an LSI according to this embodiment will be described with reference to FIG. FIG. 1 is a flowchart of an LSI design method.

  First, the system specification of the LSI to be designed is determined. Then, system level design is performed so as to satisfy the specifications (step S10). The description language used at this time is a C language having a higher abstraction level than the hardware description language and extended for hardware, such as SystemC and SpecC. The level of abstraction is the level of detail in design, and the level of detail is the order of LSI structure and operations. Through step S10, an LSI function description (LSI design data) 10 to be designed is obtained. The function description 10 obtained at this point has a high level of abstraction and does not have a concept of time. In other words, the timing of the clock and calculation, which is the reference for the operation of the LSI, is not defined at all.

  Next, the function description 10 is behaviorally synthesized using a synthesis tool (step S11). As a result, the function description 10 is converted into the RTL description 11. The RTL description 11 has several levels of abstraction, which will be described later. Further, the RTL description 11 is functionally synthesized and logically synthesized by a synthesis tool (step S12). As a result, the RTL description 11 is converted into a gate-level logic circuit (net list) 12.

  Thereafter, layout design is performed for the gate level logic circuit 12 (step S13), and mask layout data 13 is obtained. The LSI design is thus completed, and the mask layout data 13 is input to the actual LSI production line.

  In the above LSI design method, it is necessary to verify whether the function description 10 designed based on the C language is equivalent to the RTL description 11. In other words, it is necessary to verify whether or not the behavioral synthesis in step S11 is performed correctly. This is equivalence verification. Hereinafter, the equivalence checking method according to the present embodiment will be described with reference to FIG. FIG. 2 is a flowchart of the equivalence checking method according to this embodiment.

  First, when the function description 10 is behaviorally synthesized in step S11, the schedule-determined data 14 that is the first stage (highest level of abstraction) of the RTL description 11 is obtained. The schedule-determined data 14 is a circuit description in which it is completely determined in which clock each operation included in the function description 10 is performed. This gives the function description 10 the concept of time.

  Next, function synthesis is performed on the schedule determined data 14 (step S14). In function synthesis, first, the configuration of the memory to be used in the LSI, the number of registers, and the like are determined. Next, an arithmetic unit to be specifically used is assigned to an operation (for example, addition or subtraction) as a function to be realized. Furthermore, it is determined whether to use a bus or a multiplexer as a connection method between a plurality of arithmetic units. In this way, the abstraction level of the RTL decreases, and finally, data 15 of the data path unit composed of an arithmetic unit, a bus, a multiplexer, and the like, and data 16 of the control unit that generates a signal for controlling them are provided. can get. The data path part data 15 and the control part data 16 have the lowest abstraction in the RTL description 11, that is, design data in which the LSI structure and the execution order of operations are all specified and the LSI is most specifically described. It is.

  In addition, the LSI is designed with a hardware description language so as to satisfy the specifications used in step S10 (step S15). Thereby, the schedule determined data 20 is obtained. The schedule-determined data 20 obtained in this way is design data having the same abstraction level as the schedule-determined data 14 obtained based on the function description 10 and having the concept of time. Subsequently, by performing functional synthesis in the same manner as in step S14 (step S16), the data path part data 21 and the control part data 22 relating to the schedule determined data 20 are obtained.

  In the behavioral synthesis in step S11, it is first tried whether or not the synthesis can be performed with a restriction that the data path portion data 21 obtained from the description in step S15 is used. If this is not possible, normal behavioral synthesis is performed.

Next, equivalence verification of both is performed (step S17). The equivalence checking method will be described with reference to FIG. FIG. 3 is a flowchart of the equivalence checking method. Equivalence verification is performed using both data path data 15 and 21 and control data 16 and 22.
First, in the equivalence verification, first, the data path part data 15 and the data path part data 21 are compared (step S18). If the correspondence between the two is obtained, the two are regarded as equivalent. If the data path portion data 21 obtained from the description in step S15 can be used in step S11, the data path portion data 15 and 21 are naturally the same, and both of them can correspond. Also, in the comparison, the correspondence library 17 is used as necessary to determine whether or not both correspond. The correspondence library 17 is information regarding the correspondence between the different data paths that have the same operation to be realized. In the data path data 21, when all the data paths cannot be matched (step S 19, NO), a formal verification is performed for the part that could not be taken (step S 20). Formal verification is performed using the verification method library 18 as necessary. For formal verification, many equivalence verification methods using exchange rules are known. What has been registered is the verification method library 19. When the verification method library 19 is used, not only the data path data 15 and 21 but also the control data 16 and 22 are referred to as necessary. This is because some of those registered in the verification method library 19 may include an instruction for referring to the control unit data.

  As a result of the formal verification, if both have unequal portions (step S21, NO), it is determined that the scheduled data 14 and 20, that is, the function description 10 and the RTL description 20 are not equivalent (step). S22).

  If both are equal in step S21 (step S21, YES), and if all the data paths are matched in step S19 (step S19, YES), then formal verification is performed on the control unit data 16 (step S19). S23). Also in this case, the verification method library 19 is used as necessary. If the control unit data 16 and 22 are equal as a result of formal verification (step S24, YES), it is determined that the function description 10 and the RTL description 20 are equivalent (step S25). If they are not equal (step S24, NO), it is determined that they are not equivalent (step S22).

  The equivalence is verified as described above. The equivalence checking method according to this embodiment will be described below with a specific example. FIG. 4 is obtained by synthesizing the function description 10 and the data path unit data 15 and the control unit data 16 obtained by synthesizing the function description 10 and the scheduled data 20 described using the hardware description language. 4 is a schematic diagram of data path unit data 21 and control unit data 22. FIG.

  The function description 10 and the schedule determined data 20 will be briefly described. The function description 10 is the following design data. That is, in the second to fourth lines, input In, outputs A and B, and variables X and Y are defined. In the fifth and sixth lines, variables X and Y take in In. In the seventh and eighth lines, 0 and X are assigned to outputs A and B, respectively. In the ninth to twelfth lines, the calculation for subtracting Y from the output B and adding 1 to the output A is repeated for a period in which the output B is a value equal to or greater than the variable Y. That is, design data for performing division by dividing B by Y.

  The schedule-determined data 20 defines the clock CL at the fourth line, and further between the third and fourth lines in the function description 10, between the fourth and fifth lines, the fifth and sixth lines. It is further provided with an instruction (Waitfor (CL) statement) that waits for the clock CL between the 6th and 7th lines, the 8th and 9th lines, and the 11th and 12th lines. is there. The Waitfor (CL) statement has a function that does not execute an instruction on the next line unless a new clock CL is input. Other than that, the scheduled data 20 is the same as the function description 10. In other words, the schedule-determined data 20 is defined by the function description 10 in which the execution timing for the clock of each row is specified.

  By inputting these into the synthesis tool, data path part data 15 and 21 and control part data 16 and 22 shown in FIG. 4 are obtained. As shown in the figure, the data path section data 15 includes multiplexers mux 1 to mux 4, an adder 30, a subtractor 31, and a comparator 32. The multiplexers mux1 and mux2 select the input signal in1 according to the control signals cd1 and cd2, respectively, and set the selected input signal in1 as variables x and y, respectively. The multiplexer mux3 selects “0” according to the control signal cd3, selects the addition result of the adder 30 according to the control signal cd4, and uses this as the output a. The multiplexer mux4 selects the variable x according to the control signal cd5, selects the output of the subtractor 31 according to the control signal cd6, and sets this as the output b. The adder 30 adds “1” to the output a. The subtractor 31 subtracts the variable y from the output b. The comparator 32 compares the output b with the variable y and outputs the comparison result as a comparison signal dc1. Then, the control unit 16 controls the control signals cd1 to cd6 according to the comparison signal dc1. The same applies to the data path portion data 21 and the control portion data 22 obtained from the schedule determined data 20.

  After the data path part data 15 and 21 and the control part data 16 and 22 are obtained as described above, equivalence is verified (step S17). First, a corresponding portion between data path portion data is detected (step S18). Then, as shown in FIG. 4, the function description 10 and the schedule determined data 20 are all the same except for the description about the clock. Accordingly, without referring to the correspondence library 17, the data path portion data 15 and 21 relating to both are the same (step S19), and formal verification of the data path becomes unnecessary. Therefore, next, formal verification is performed on the control unit data 16 and 22 (step S23). As described above, the function description 10 and the schedule-determined data 20 are all the same except for the description related to the clock, and therefore the control unit data 16 and 22 need only be verified for the clock. As a result, if the control unit data 16 and 22 are equal (step S24), it is determined that the function description 10 is equivalent to the RTL description 20 described in the hardware description language (step S25).

  Another example is shown in FIG. FIG. 5 is obtained by synthesizing the function description 10 and the data path part data 15 and the control part data 16 obtained by synthesizing the function description 10 and the scheduled data 20 described using the hardware description language. 4 is a schematic diagram of data path unit data 21 and control unit data 22. FIG.

  The function description 10 is as described with reference to FIG. The schedule-determined data 20 described in the hardware description language is different from that in FIG. 4, and the 14th to 16th lines in FIG. 4 are replaced with (A, B) = Divider (X, Y) statements.

  By inputting these into the synthesis tool, the data path part data 15 and 21 and the control part data 16 and 22 shown in FIG. 5 are obtained. As shown in the figure, the data path part data 15 and the control part data 16 obtained by synthesizing the function description 10 are the same as those in FIG. On the other hand, the data path portion data 21 obtained by synthesizing the RTL description 20 described in the hardware description language has the following configuration. That is, the data path includes multiplexers mux 11 to mux 14 and a divider 33. The multiplexers mux11 and mux12 select the input signal in1 according to the control signals cd11 and cd12, respectively, and set the selected input signal in1 as variables x and y, respectively. The multiplexers mux13 and mux14 output the division results in the divider 33 and the remainders as outputs a and b in accordance with the control signals cd13 and cd14, respectively. Then, the control unit 16 controls the control signals cd11 to cd14.

  After the data path part data 15 and 21 and the control part data 16 and 22 are obtained, the equivalence is verified (step S17). First, a corresponding portion between data path portion data is detected (step S18). Then, unlike the case of FIG. 4, the block 34 that performs division in the data path portion data 15 is replaced with a divider 33. That is, the configuration of the two is different. However, if it is known that the two functions are the same but the functions are the same, formal verification is not necessary. Therefore, the correspondence library 17 is referred to as to whether the block 34 and the divider 33 are equivalent. FIG. 6 is a schematic diagram showing an example of the correspondence library 17. As shown in the figure, it is assumed that it is registered in the correspondence library 17 that the descriptions on the 7th to 12th lines in the function description 10 are equal to the divider in the data path portion data. Then, since it is understood that the block 34 and the divider 33 are equivalent in FIG. 5, there is no need to perform formal verification. As a result, it can be seen that the data path data 15 and 21 are equivalent (step S19).

  Therefore, next, formal verification is performed on the control unit data 16 and 22 (step S23). FIG. 7 is a schematic diagram of the control unit data 16. As shown in the figure, the control unit 16 has six states sr1 to sr6. In FIG. 7, the signal names before and after the slash (/) described between the states indicate that the state transitions based on those signals, the comparison signal dc1 before the slash, and the control signal cd1 after the slash. ~ Cd6. “-” Indicates that there is no question regarding the comparison signal dc1, and “done” indicates the end of the calculation.

  First, in the initial state sr1, when the control signal cd1 becomes “1”, the multiplexer mux1 selects the input in1, sets it to x, and the state transitions to sr2. When the control signal cd2 becomes “1” in the state sr2, the multiplexer mux2 selects the input in1, sets it to y, and the state transits to sr3. When cd3 and cd5 become “1” in the state sr3, the multiplexers mux3 and mux4 set “0” and the variable x to the outputs a and b, respectively, and transition to the state sr4. In the state sr4, when cd4 and cd6 become “1” and the comparison signal dc1 becomes “1”, the state transitions to the state sr6. The comparison signal dc1 being “1” indicates that the output b is less than the variable y. In the state sr6, division is repeated as long as dc1 is “1”. When the comparison signal cd1 becomes “0”, that is, when the calculation is completed (done), the state transits to the final state sr5. Also in the state sr4, when the comparison signal dc1 becomes “0”, the calculation is completed, and the state sr5 is entered without moving to the state sr6.

  FIG. 8 is a schematic diagram of the control unit data 22. As illustrated, the control unit 22 has four states sr11 to sr14. First, in the initial state sr11, when the control signal cd11 becomes “1”, the multiplexer mux11 selects the input in1, sets it to x, and the state transitions to sr12. When the control signal cd12 becomes “1” in the state sr12, the multiplexer mux12 selects the input in1 and sets it to y, and the state transits to sr13. When cd13 and cd14 become “1” in the state sr13, the state transitions to the state sr14, the divider 33 performs division, and the calculation ends (done).

  When comparing the control unit 16 shown in FIGS. 7 and 8, the state transition condition from the state sr1 to sr3 in the control unit 16 and the state transition condition from the state sr11 to sr13 in the control unit 22 are exactly the same. That is, both control methods and the data flow by them are the same. Therefore, it can be understood that the control from the state sr1 to sr3 in the control unit 16 and the control from the control unit 22 to the states sr11 to sr13 are equivalent. Therefore, a formal verification is performed as to whether or not the states sr4 to sr6 in the control unit 16 and the control of sr4 in the control unit 22 are equivalent (step S23). Formal verification is performed using a verification method library 19 in which equivalence verification methods are registered. As a result of formal verification, if it is derived that both are performing the same control, it is determined that the function description 10 and the RTL description 20 in FIG. 5 are equivalent.

  In the equivalence checking method, all the processes described can be performed mainly by a computer. FIG. 9 is a block diagram showing an internal configuration of a computer that performs the equivalence verification. As illustrated, the computer 40 includes a CPU 41, a main memory 42, a memory 43, a display 44, and an input device (keyboard) 45. The memory 43 holds design data 46, a control unit comparison program 47, a path comparison program 48, a circuit synthesis program 49, various libraries 50, and the like. The design data 46 includes the function description 10 and the RTL description (including schedule determined data, data path part data, and control part data) 12 described above. The various libraries 50 are the correspondence library 17 and the verification method libraries 18 and 19. The main memory 42 temporarily holds each program, data, etc. in the memory 43. The CPU 41 executes a synthesis tool by the circuit synthesis program 49 and functions as circuit synthesis means for performing the above-described behavioral synthesis (step S11), function synthesis (steps S14 and S16), and logic synthesis (step S12). Further, when verifying equivalence, the CPU 41 reads the path comparison program 48, various libraries 50, and design data 46 into the main memory 42, and functions as a data path comparison verification unit that performs the processes of steps S18 to S21. Furthermore, by reading out the control unit comparison program 47 instead of the path comparison program 48, it also functions as a control unit comparison means for performing the above steps S23 and S24. The display 44 displays the processing result by the CPU 41. The input device 45 receives a user command input.

As described above, the equivalence verification method of the circuit description language according to the first embodiment of the present invention can facilitate the verification of equivalence. This effect will be described in detail below.
Hereinafter, for simplification of description, the schedule-determined data is simply referred to as “RTL description”, and the data path portion data and the control portion data are collectively referred to as “data / control information”. Conventionally, even when an RTL description is created by a hardware description language and the function / logic synthesis is performed using a synthesis tool, it is necessary to verify equivalence between the RTL description and the data / control information. Conventionally, the synthesizing tool performs equivalence verification between the two, and the reliability of the equivalence verification is relatively high. Therefore, the data / control information obtained by the synthesis tool can be considered to be almost equivalent to the RTL description.

  On the other hand, in recent years, a design method based on the C language has begun to be used. In this case, the function description described in the description language based on the C language is converted into data / control information by the synthesis tool. Therefore, it is important to verify equivalence between the function description and the data / control information. In this regard, a conventional method is known in which a simulation is performed between an RTL description and a function description, and equivalence is verified based on the result. However, when determining equivalence using simulation, in order to guarantee 100% equivalence, it is necessary to perform all possible combinations of signals. This requires an enormous amount of calculation and is not realistic.

  However, in this embodiment, equivalence is first verified using formal verification without using simulation. By using formal verification, 100% equivalence can be easily guaranteed as compared with the case of using simulation. Therefore, in the present embodiment, the following method is used. First, a function description is created and data / control information is obtained by a synthesis tool (this is called first data / control information). At the same time, an RTL description that realizes the same function as the function description is created using a conventional hardware description language, and data / control information is obtained by a synthesis tool (this is referred to as second data / control information). As described above, it is almost guaranteed that the second data / control information is equivalent to the RTL description. Therefore, by verifying the equivalence between the second data / control information and the first data / control information, whether the function description satisfies the desired function, that is, the function description and the first data / control information are equivalent. It verifies whether it is. If it turns out that both are equivalent, it turns out that the said function description can obtain correct data and control information by the said synthesis tool.

  When verifying the equivalence between the first data / control information and the second data / control information, as described in the above-described embodiment, mutually equivalent parts are found for each part. Formal verification is applied only to portions where it is not known whether the stored data is equivalent even if conventional stored data is used. In other words, equivalence is verified from the bottom up. As a result, the number of places where formal verification should be performed can be minimized, the amount of calculation for equivalence verification can be reduced, and equivalence verification can be easily performed.

Further, in the present embodiment, data / control information is divided into a data path part and a control part. That is, the equivalence is verified for each of the circuit configuration and the data flow in the circuit. As for the circuit configuration, a portion equivalent to bottom-up is detected as described above (corresponding to a computing unit), and formal verification is performed only for necessary portions. Therefore, if both of the circuit configurations completely match, formal verification may be performed only for the data flow. Focusing on the data flow is equivalent to focusing on the control method for the circuit configuration, and it is sufficient to verify at what timing the control signal becomes “1” or “0”. When formal verification is applied to the circuit configuration, the calculation amount increases because the data width is large, for example, 16 bits or 32 bits, whereas the control signal is usually 1 bit. The amount is very small. In other words, the amount of calculation for equivalence verification can be greatly reduced by reducing formal verification for the circuit configuration or omitting it completely.
By using the method as described above, the reliability of LSI design using a C language-based circuit description language that requires a small amount of description due to its high level of abstraction is improved. Of course, verification can be performed from the bottom up without being divided into the data path unit and the control unit.

  Next, a circuit description language equivalence checking method according to a second embodiment of the present invention will be described. The present embodiment relates to the timing at which equivalence is to be determined when determining equivalence by focusing on the data flow (control unit) in the first embodiment. FIG. 10 is a timing chart of the clock, data A, and data B. Assuming that there is certain data A and B in the LSI, these data A and B do not always have meaningful values. For example, the data A has a meaningful value from time t0 to time t3, but the values before and after that are not determined to be specific values. Data B also has a meaningful value from time t1 to time t2, but before and after that is not determined. In such a case, it is not necessary to require that the data A and B be equivalent even to a time zone where the data A and B are not determined. Therefore, it is necessary to determine at which timing the equivalence is judged.

  In this respect, the RTL description has the concept of a clock, and already has the above-mentioned timing definition. However, since there is no concept of clock in the function description, it is impossible to define the timing with the clock. The present embodiment relates to a method for defining the timing in the function description under such circumstances.

  FIG. 11 is an example of the function description 10 according to the present embodiment. As shown in the figure, in the function description 10 of FIGS. 4 and 5 described in the first embodiment, descriptions of the 13th and 14th lines are added. The data to be output is specified in the 13th line, and at which timing data to be output is specified in the 14th line. Hereinafter, the description on the 13th and 14th lines is referred to as a read command. When the function description 10 shown in FIG. 11 is given, the synthesis tool searches for a read command in behavioral synthesis (step S11) and function synthesis (step S14). When a read command is found, the data path unit data 15 and the control unit data 16 are generated so that the data specified in the read command is output at the specified timing. As described above, since the function description has no concept of time, the output timing is specified as the number of lines in the function description or as a response to the signal. In other words, the following designation method can be considered. For example, in the case of FIG. 11, the output timing of the data (A, B) is designated as “after the processing of the 12th row is completed”. Alternatively, “when the value of signal A changes” is designated.

As described above, the equivalence verification method according to the second embodiment of the present invention can further facilitate the verification of equivalence as compared with the first embodiment. This effect will be described below.
As described above, equivalence does not have to be satisfied at all times (timing), but it is usually sufficient if it is satisfied at a specific timing. Therefore, in this embodiment, the output timing of data necessary for equivalence verification is specified by using a read command in the function description. The verification can be simplified by generating the data path part data and the control part data so that the equivalence can be verified only at the timing specified by the read command.

  Further, for example, assuming that an expression X = A + B + C exists in the function description, it is assumed that a value of (A + B) is necessary for equivalence verification. Such an internal variable may be very useful for verification of equivalence even if it is not output to the outside, or may be essential. However, the synthesis tool collectively calculates the value of X, and the value of (A + B) may not be reflected in the data path part data and the control part data. In this respect, in the present embodiment, a value to be reflected in the data path portion data and the control portion data is designated by a read command. That is, in the above case, the value of (A + B) can be observed by the data path part data and the control part data. Therefore, values necessary for equivalence verification can be reliably reflected in the data path portion data and the control portion data, and the equivalence verification can be facilitated.

  As described above, the function description has no concept of time. Therefore, for example, the timing can be designated by designating the number of lines in the function description or designating which command is a signal obtained in response to the command. Further, the read command may be outside the function description. That is, the read command is held in a file different from the function description. When performing circuit synthesis, the CPU 41 may read a file holding a read command into the main memory 42 and perform circuit synthesis based on the read command in the file and the design data 46.

  FIG. 12 is a schematic diagram of the function description 10 according to a modification of the second embodiment. The function description 10 shown in FIG. 12 has a read command different from the function description shown in FIG. That is, in the function description 10 shown in FIG. 4, the first read command (CareStart (A, B)) indicating the beginning of the specified range is provided between the 8th and 9th lines, and indicates the end of the specified range. A second read instruction (CareEnd (A, B)) is provided in the last line. The first and second read commands mean that the values A and B are observed each time the values A and B obtained in the sentence between the 10th and 13th lines sandwiched between them change. That is, each time the division shown in the 10th to 13th lines is performed, the data path part data and the control part data are generated so that the division results A and B are observed.

  As described above, in the circuit description language equivalence verification method according to the first and second embodiments of the present invention, equivalence is verified using a formal verification technique. Then, when comparing RTL descriptions, based on the information obtained in the past about equivalence, the equivalent parts are found individually from the entire configuration. As a result, formal verification is performed only for the parts that have not been proved to be equivalent. Thereby, the amount of calculation required for equivalence verification can be reduced. Also, equivalence is verified at the stage of data path part data and control part data in the RTL description. Therefore, when equivalence is proved with respect to the data path part data, it is sufficient to perform formal verification only for the control part data, and the amount of calculation can be reduced. Thus, it is possible to provide a hardware design description equivalence verification method that facilitates verification.

  In the above embodiment, the equivalence verification between the function description written in the C language base and the RTL description written in the hardware description language has been described as an example. However, for example, the above verification method can be applied even when equivalence verification is performed between function descriptions or between RTL descriptions. FIG. 13 is a flowchart when equivalence checking is performed between function descriptions. Specifically, the following cases can be considered. For example, it is assumed that certain design data (referred to as first design data) is programmed using a C language-based circuit description language. In this case, it is assumed that a relatively good circuit cannot be obtained even if it is input to the synthesis tool, but the equivalence between the two is guaranteed. Then, it is assumed that design data (referred to as second design data) is programmed using a C language-based circuit description language so that the same function as the first design data can be achieved. Of course, the program description is different from the first design data. It is assumed that the circuit obtained by inputting the second design data into the synthesis tool is superior to the first design data. However, the equivalence between the second design data and the RTL description has not been verified. In such a case, the equivalence between the first design data and the second design data is verified. If they are equivalent, the second design data can be used thereafter.

  That is, as shown in FIG. 13, function descriptions 10 and 60 are created using a C language-based circuit description language (steps S10 and S30), respectively. Then, behavioral synthesis and functional synthesis are performed for each of them (steps S14 and S32), and data path unit data 15 and 62 and control unit data 16 and 63 are obtained. Thereafter, the equivalence between the data path unit data 15 and 62 and the equivalence between the control unit data 16 and 63 are verified by the method described in the first and second embodiments.

  FIG. 14 is a flowchart for verifying RTL descriptions written in a hardware description language. As shown in the figure, RTL descriptions 20 and 70 are created using a hardware description language, respectively (steps S15 and S40). Then, function synthesis is performed for each of them (steps S16 and S41), and data path part data 21 and 72 and control part data 22 and 71 are obtained. Thereafter, the equivalence between the data path data 21 and 72 and the equivalence between the control data 22 and 71 are verified by the method described in the first and second embodiments.

  In the above-described embodiment, the description has been given by taking as an example the language based on the C language as the description language used in the system level design. Not.

  Note that the present invention is not limited to the above-described embodiment, and various modifications can be made without departing from the scope of the invention in the implementation stage. Furthermore, the above embodiments include inventions at various stages, and various inventions can be extracted by appropriately combining a plurality of disclosed constituent elements. For example, even if some constituent requirements are deleted from all the constituent requirements shown in the embodiment, the problem described in the column of the problem to be solved by the invention can be solved, and the effect described in the column of the effect of the invention Can be extracted as an invention.

1 is a flowchart of a semiconductor integrated circuit design method according to a first embodiment of the present invention. 3 is a flowchart of a circuit description language equivalence verification method according to the first embodiment of the present invention; 3 is a flowchart of a circuit description language equivalence verification method according to the first embodiment of the present invention; It is a schematic diagram of the equivalence verification method of the circuit description language according to the first embodiment of the present invention, showing an example of a function description and an RTL description. It is a schematic diagram of the equivalence verification method of the circuit description language according to the first embodiment of the present invention, showing an example of a function description and an RTL description. The schematic diagram of the correspondence library used with the equivalence verification method of the circuit description language which concerns on 1st Embodiment of this invention. It is a schematic diagram of the equivalence verification method of the circuit description language concerning the 1st Embodiment of this invention, and is a figure which shows an example of the control part in RTL description. It is a schematic diagram of the equivalence verification method of the circuit description language concerning the 1st Embodiment of this invention, and is a figure which shows an example of the control part in RTL description. 1 is a block diagram of an internal configuration of a computer that realizes a circuit description language equivalence checking method according to a first embodiment of the present invention. The timing chart of a clock and the data signal synchronized with it. The schematic diagram of the function description in the equivalence verification method of the circuit description language which concerns on 2nd Embodiment of this invention. The schematic diagram of the function description in the equivalence verification method of the circuit description language which concerns on the modification of the 2nd Embodiment of this invention. The flowchart of the equivalence verification method of the circuit description language which concerns on the 1st modification of 1st, 2nd embodiment of this invention. The flowchart of the equivalence verification method of the circuit description language which concerns on the 2nd modification of 1st, 2nd embodiment of this invention.

Explanation of symbols

  DESCRIPTION OF SYMBOLS 10 ... Function description, 11 ... RTL description, 12 ... Gate level logic circuit, 13 ... Mask layout data, 14, 20 ... Schedule determined data, 15, 21 ... Data path part data, 16, 22 ... Control part data, 17 ... correspondence library, 18, 19 ... verification method library, 30 ... adder, 31 ... subtractor, 32 ... comparator, 33 ... divider, 40 ... calculator, 41 ... CPU, 42 ... main memory, 43 ... memory, 44 ... display, 45 ... input device, 46 ... design data, 47 ... control unit comparison program, 48 ... path comparison program, 49 ... circuit synthesis program, 50 ... various libraries

Claims (5)

The CPU synthesizes the first design data related to the semiconductor integrated circuit described in the first circuit description language, and the second description described in the second circuit description language having a lower abstraction level than the first description language. give the design data, the steps that stores in the memory device,
The CPU synthesizes the second design data, and first circuit information including an arithmetic unit and a data path connected to the arithmetic unit, and first data for controlling a data flow in the first circuit information. Obtaining control information and storing it in the memory device ;
The CPU synthesizes third design data described in the second circuit description language, and includes second circuit information including an arithmetic unit and a data path connected to the arithmetic unit, and the second circuit information obtain a second control information for controlling the flow of data in a step that stores it in the memory device,
The CPU compares the first and second circuit information to verify the correspondence, performs formal verification on the non-corresponding portion, and verifies whether the first and second circuit information is equivalent. Steps,
The CPU performing formal verification on the first and second control information and verifying whether or not the first and second control information are equivalent, and the first and second circuits When the information is equivalent and the first and second control information are equivalent, it is determined that the first design data and the third design data are equivalent ,
The CPU, when verifying the correspondence between the first and second circuit information, an arithmetic unit obtained by synthesizing the second circuit description language, a data path connected to the arithmetic unit, and the first A library that holds a correspondence relationship with a circuit description language is read from the memory device, is referred to to verify whether or not the first and second circuit information are at least partially corresponding, and a portion that does not correspond Formal verification for
When the CPU verifies whether or not the first and second control information are equivalent, a state transition condition regarding a plurality of states that can be taken by the first control information and a plurality that can be taken by the second control information. Circuit description language equivalence by comparing the state transition conditions with respect to the states of the two, determining that the portions having the same state transition conditions are equivalent, and performing the formal verification on the portions that are not the same Method of verification. Said fourth design data and circuit synthesis described by the first circuit description language, claim 1 Symbol, characterized by further comprising the step of obtaining the third design data described by the second circuit description language Method for verifying equivalence of circuit description languages Of the first and second circuit description languages, the second circuit description language has a concept of time,
Among the first to third design data, the second and third design data are timings of a clock signal serving as a reference for the operation of the semiconductor integrated circuit and operations included in the second and third design data. claim 1 or 2 equivalence checking method of a circuit description language, wherein the containing information about. The first design data includes information related to a variable to be output in the second design data among operations included in the first design data, and information designating a timing for outputting the variable. The circuit description language equivalence checking method according to claim 3 .   The first design data relating to the semiconductor integrated circuit described in the first circuit description language is equivalent to the second design data described in the second circuit description language having a lower abstraction level than the first circuit description language. An equivalence verification device for verifying whether or not
  Circuit synthesis of the first design data to obtain third design data described in the second circuit description language, circuit synthesis of the third design data, and data connected to the computing unit and the computing unit First circuit information including a path and first control information for controlling the flow of data in the first circuit information are obtained, and further, the second design data is synthesized with a circuit and connected to the computing unit and the computing unit. Circuit synthesizing means for obtaining second circuit information including a data path and second control information for controlling a data flow in the second circuit information;
  An arithmetic unit obtained by synthesizing the second circuit description language, a data path connected to the arithmetic unit, and a memory device holding a library in which a correspondence relationship between the first circuit description language is recorded;
  Data path comparing means for comparing the first and second circuit information to verify the correspondence, performing formal verification on the non-corresponding portion, and verifying whether or not the first and second circuit information are equivalent When,
  Control unit comparing means for performing formal verification on the first and second control information and verifying whether or not the first and second control information are equivalent;
  And the data path comparison means refers to the library in the memory device to verify whether or not the first and second circuit information corresponds at least partially and Perform formal verification,
  The control unit comparing means compares a state transition condition relating to a plurality of states that can be taken by the first control information with a state transition condition relating to a plurality of states that can be taken by the second control information, and the state transition conditions are the same. Are determined to be equivalent, and the formal verification is performed for non-identical parts.
  A circuit description language equivalence verification device characterized by the above.

Images