JP2008097504A - Action proposition generation system and verification system - Google Patents

Abstract

A system for automatically generating an operation proposition from time-series signal value data without human intervention, and a system for verifying an operation proposition capable of verifying an operation proposition before verification of a logic circuit are provided. .
Signal value extraction means for extracting signal value transition information relating to signal values for each clock cycle of a plurality of signals given time-series signal value data, and signal values of a plurality of signals in an initial state of the circuit Based on the initial state information 3 and the signal value transition information regarding the common database generating means 4 for generating a common database regarding the signal value in a clock cycle and the signal value in the clock cycle before and after the clock cycle, based on the common database Simultaneous deactivation signal extraction means 5A for extracting a simultaneous deactivation signal that is a combination of a plurality of signals that do not become active at the same time, and an operation proposition output for generating and outputting an operation proposition based on the extracted simultaneous deactivation signal Means 6 are provided.
[Selection] Figure 1

Description

  The present invention relates to a system for generating an operation proposition and a system for verification.

  In the design process of a semiconductor integrated circuit, first, an RTL description of a circuit operation and a function required for an integrated circuit to be designed is performed using a high-level RTL (register transfer level). Next, the logic synthesis process converts the RTL description into a gate level description at a gate level with a low level of abstraction considering the semiconductor manufacturing apparatus. Finally, a mask pattern is created from the gate level description and a semiconductor integrated circuit is manufactured.

  However, due to the recent increase in scale and complexity of circuits, the conventional verification methods using circuits and test vectors require enormous verification time. In addition, it has reached the limit that the design / verifier considers and verifies all cases.

  Even if a test vector capable of inspecting all cases can be created, it is extremely difficult to confirm that a large number of inspection results are inspected without fail by visual inspection.

  Therefore, in recent years, as one of the formal verification (formal logic verification) techniques, it is verified whether the operation proposition (property) and the logic circuit to be verified (Device Under Test, hereinafter referred to as DUT) match. An operational proposition verification system is used. That is, the verification means for comparing the circuit description and the operation proposition in which the operation specifications are expressed in a predetermined format, and whether or not the operation proposition is executed in the result of verifying the test vector and the logic circuit by simulation. Systems with assertion verification means to confirm are beginning to be introduced.

  Here, the operation proposition used heretofore had to be created manually by a designer / verifier from a specification written in natural language or waveforms / graphics. In recent years, methods have been developed to automatically extract verification items, such as whether there is an unnecessary description in the state transition description in the circuit, from the logic circuit to be verified, as an efficient process to create manually. Yes.

  However, the conventional verification method has the following problems.

  Usually, the operation proposition verification means can perform a comprehensive check as compared with the simulation verification means using test vectors. If the designer / verifier can always input the correct operation proposition, it will be a powerful means to realize complete prevention of verification omission.

However, when manually creating an operation proposition from a specification written in a conventional natural language, the following problems have occurred due to manual intervention.
1) Misdetection occurs due to inconsistency between specifications and operation propositions caused by design / verifier misidentification.
2) The operation proposition cannot be verified until the creation of the logic circuit is completed.
3) When a mismatch is included in both the logic circuit and the operation proposition, it is difficult to investigate the cause.

  Therefore, conventionally, it is not possible to confirm the contents of the action proposition and the action proposition description expressing the action proposition before the logic circuit is verified.

  Furthermore, since the operation proposition cannot be verified if there is no logic circuit to be verified, the verification of the generated operation proposition description itself and the circuit verification of the logic circuit that is the original purpose are performed separately. It was impossible to do so, and both tasks were mixed. As a result, even if a mismatch was detected, it took a long time to elucidate the cause.

The following is a list of literatures that disclose conventional verification methods.
JP-A-2005-222371

  The present invention provides a system for automatically creating an operation proposition from time-series signal value data without human intervention, and a system for verifying an operation proposition capable of verifying an operation proposition before verifying a logic circuit. The purpose is to do.

  An operation proposition generation system according to an aspect of the present invention includes a signal value extraction unit that receives time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals, and an initial state of the circuit Based on the initial state information regarding the signal values of each of the plurality of signals and the signal value transition information, a common database regarding signal values in a certain clock cycle and signal values in clock cycles before and after the clock cycle is generated. A common database generation unit; a simultaneous deactivation signal extraction unit that extracts a simultaneous deactivation signal that is a combination of a plurality of signals that do not become active at the same time based on the common database; and the extracted simultaneous deactivation signal And a motion proposition output means for generating and outputting a motion proposition based on To.

  An operation proposition generation system according to an aspect of the present invention includes a signal value extraction unit that receives time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals, and an initial state of the circuit Based on the initial state information regarding the signal values of each of the plurality of signals and the signal value transition information, a common database regarding signal values in a certain clock cycle and signal values in clock cycles before and after the clock cycle is generated. Based on the common database generation means, based on the common database, signal transition regularity extraction means for extracting the regularity of the transition of the signal value that changes in clock cycles, and the regularity of the extracted transition of the signal value And an operation proposition output means for generating and outputting an operation proposition.

  An operation proposition verification system according to an aspect of the present invention includes a signal value extraction unit that receives time-series signal value data and extracts signal value transition information related to signal values for each clock cycle of a plurality of signals, and an initial state of the circuit Based on the initial state information regarding the signal values of each of the plurality of signals and the signal value transition information, a common database regarding signal values in a certain clock cycle and signal values in clock cycles before and after the clock cycle is generated. A common database generation means; a transition information extraction means for extracting a signal value transition information indicating a state satisfying a predetermined condition included in the behavior proposition given the behavior proposition; a signal value transition information based on the common database; Compare with the signal value transition information extracted by the signal value extracting means, And operation proposition analyzing means for constant, if it is determined that there is no consistency by the operation proposition analysis means, characterized in that it comprises an operation proposition correcting means for instructing modification of the operation proposition.

  An operation proposition verification system according to an aspect of the present invention includes a signal value extraction unit that receives time-series signal value data and extracts signal value transition information related to signal values for each clock cycle of a plurality of signals, and an initial state of the circuit Based on the initial state information regarding the signal values of each of the plurality of signals and the signal value transition information, a common database regarding signal values in a certain clock cycle and signal values in clock cycles before and after the clock cycle is generated. Common database generation means, logic circuit state transition extraction means for reading the logic circuit to be verified and extracting signal value transition information, signal value transition information included in the common database, and logic circuit state transition extraction means Transition information comparing means for comparing the signal value transition information that has been made, and the transition information ratio When the signal value transition information included in the common database is determined to be correct by the means, the transition information mismatch information output means for outputting information on mismatch included in the logic circuit, and the transition information comparison means, Time series signal value data output means for outputting additional time series signal value data to be added to the time series signal value data when it is determined that the signal value transition information extracted by the logic circuit state transition extraction means is correct With.

  An operation proposition verification system according to an aspect of the present invention includes a signal value extraction unit that receives time-series signal value data and extracts signal value transition information related to signal values for each clock cycle of a plurality of signals, and an initial state of the circuit Based on the initial state information regarding the signal values of each of the plurality of signals and the signal value transition information, a common database regarding signal values in a certain clock cycle and signal values in clock cycles before and after the clock cycle is generated. A common database generation means and a validity check that extracts signal value transition information from the common database and checks the validity of the common database based on whether or not there is an invalid state in the signal value for each clock cycle And the time-series signal value data based on the inspection result by the validity checking means. If it should do, and an alarm output means for outputting an alarm.

  According to the operation proposition generation system of the present invention, the operation proposition is automatically created from the time-series signal value data without human intervention. According to the operation proposition verification system, the operation proposition is verified before the logic circuit is verified. Can be verified.

  Embodiments of the present invention will be described below with reference to the drawings.

(1) Embodiment 1
A system for automatically generating an operation proposition from time-series signal value data according to Embodiment 1 of the present invention will be described with reference to FIG.

  The first embodiment includes signal value extraction means 2, common database generation means 4, simultaneous inactive signal extraction means 5A, and operation proposition output means 6.

  Time-series signal value data 1 and signal initial state information 3 are input to the signal value extracting means 2. The time-series signal value data 1 is data indicating a change in the signal value with respect to the time described in the specification, and indicates a signal value that changes every clock cycle. The signal initial state information 3 is information relating to initial state information of each signal described in the specification, for example, a signal value in an idle state or an inactive state of a bus.

  Then, the signal value extraction unit 2 performs a process of extracting the value of each signal in units of clock cycles from the time series signal value data 1 and outputs time series signal value transition information.

  The common database generation unit 4 generates a common database to be described later using the time-series signal value transition information output from the signal value extraction unit 2 and the initial state information 3 of the signal.

  The simultaneous inactive signal extraction means 5A automatically performs a process of extracting a combination of a plurality of signals that are not simultaneously activated as verification items from the generated common database.

  The action proposition output means 6 outputs the action proposition 7 described using a specific language for the extracted verification item.

  Below, the specific content of the said process is explained in full detail. First, a process of outputting time-series signal value transition information performed by the signal value extracting unit 2 will be described.

  In the system bus read 1 operation, the designer / verifier uses the clock signal CLK having the waveform as shown in FIG. 2 and the six signals sigA and sigC to sigG defining the protocol as time series signal value data. Suppose you enter it. Here, the signal values of the signals sigA and sigC to sigG are determined at the rising edge of the clock signal CLK.

  In the example shown in FIG. 2, the specification is such that all signal values of the six signals sigA, sigC to sigG are activated at a low level. Further, the initial state of the signal sigA is represented by “X” indicating Don't Care because the signal value can take either a low level or a high level. This system bus requires a change of 3 clock cycles before the operation is confirmed.

  When the designer / verifier inputs such time-series signal value data to the system of the first embodiment, the signal value extracting means 2 uses the time axis, specifically, the number of clock cycles C1, C2, C3,. Matrix data indicating each signal value is generated.

  The designer / verifier is not limited to this lead 1 operation, but also applies other time-series signal value data as shown in FIG. To the system.

  It should be noted that the signal value extraction means 2 is not limited to the signal name existing in this read 1 operation, but complements the signal name existing in other operations, and is in the form of a matrix of signal values that change every clock cycle in each operation. Generate data. At this time, it is assumed that a complemented signal that does not exist in a certain operation has a signal value in an inactive state.

  For example, the signal sigB does not exist during the read 1 operation of the system bus shown in FIG. However, during the read 2 operation of the system bus shown in FIG. 4, the signal sigB exists. Therefore, the matrix data indicating the signal values for each clock cycle during the read 1 operation of the system bus shown in FIG. 3 is processed as shown in FIG. That is, the signal sigB included in the read 2 operation is automatically inserted. Then, the signal value of the signal sigB is extracted from the initial state information 3 of the signal shown in FIG. 1, and the value “1” at the time of inactivation is added to every clock cycle.

  As shown in FIG. 6, when the operations of the three leads 1, 2, and 3 exist in the system bus, the signals sigA to sigG for each clock cycle are based on the time-series signal value data for each operation. Matrix data indicating signal values is generated.

  Next, as shown in FIG. 7, matrix-like data indicating each signal value for each clock cycle C1, C2, C3 in a certain operation (here, read 1 operation) generated by the signal value extracting means 2, A common database is generated by the common database generation means 4 using the signal in the inactive state in the initial state information 3 of the signal shown in FIG.

  Here, as shown in FIG. 7, the common database indicates signal names (here, sigA to sigG) and respective initial value data (here, signal value “0” when inactive). This is a database that includes two types of data: data ({sigA, 0} {sigB, 0} {sigC, 0}, ..., {sigG, 0}) and data indicating a label structure described below.

  FIG. 8 shows two types of data included in the common database, initial value data and a label structure. These data are generated from time-series signal value data indicating changes in the signal values of the signals sigA to sigG every clock cycle C1, C2, and C3.

  The label structure is a state calculated from a combination of signal values “0110001” of all signals sigA to sigG at a certain time, for example, clock cycle C2, for example, a state label uniquely converted to a decimal number, The original state after the transition, that is, the state label calculated from the combination “X111111” of the signal values of the signals sigA to sigG in the clock cycle C1 one clock cycle before, and one clock cycle after the transition from the state And the state label calculated from the combination “0111111” of the signal values of the signals sigA to sigG in the clock cycle C3.

  In the example of the state label shown in FIG. 8, if the current state label is “LABEL_NAME”, for example, the state label one clock cycle before is “IN_LABEL”, and the state label after one clock cycle is “OUT_LABEL”. It becomes.

  In addition, although the label of the state before the current state label and the label of the subsequent state are present one each here, the present invention is not limited to this, and there may be a plurality of labels.

  When there is no state label before or after the current state label, NULL values are stored respectively.

  In the example shown in FIG. 8, the specific numerical values of the labels are converted from binary numerical values, which are combinations of signal values of the signals sigA to sigG in each clock cycle, into decimal numerical values. However, the present invention is not limited to this, and other calculation methods may be used as long as a numerical value uniquely representing each state is used.

Here, as a specific label generation procedure, a description will be given of a procedure for generating a label using matrix-shaped data indicating each signal value for each clock cycle shown in FIG.
1) As shown in FIG. 8, all signal names sigA to sigG and signal initial state information 3 are extracted from matrix data indicating signal values in clock cycles C1, C2, and C3, and a common database is extracted. Store in “SIG_INFO {sigA, 0} to {sigG, 0}”.
2) As indicated by “(a)” in FIG. 8, column information for each operation mode and for each clock cycle is extracted.
For example, when the signal values of the signals sigA to sigG are extracted as column information in the clock cycle C1, information “X111111” is acquired.
3) As indicated by “(b)” in FIG. 8, “X” indicating that the signal value is indeterminate (Don't Care) has two possible data, that is, “0”. ”Or“ 1 ”and rework.
4) As a result, as indicated by “(c)” in FIG. 8, the column data “X1111111” in the clock cycle C1 at the time of the read 1 operation is divided into “01111111” and “11111111” and reprocessed. .
5) The column data for each clock cycle C1, C2, C3,... Is regarded as a binary number and converted into a decimal number to generate a label structure on the database.
For example, the column data “01111111” in the clock cycle C1 during the read 1 operation is converted to “LABEL_NAME = 63” and “11111111” is converted to “LABEL_NAME = 127”.
6) As shown as “(d)” in FIG. 8, the label structure of the common database has data for storing the name of the label itself and the IN / OUT transition label of the signal transition.
For example, if the label structure in a certain clock cycle C2 is “LABEL_NAME = 49”, the label structure in the previous clock cycle C1 is “IN_LABEL = 63 or 127”, and the next clock cycle C3. The label structure in is “OUT_LABEL = 63”.
7) In the procedures 1) to 5) as described above, the data for the label structure is repeatedly constructed for each operation mode and for each clock cycle, and the transitioned label name is added.

  In the case of a label that already exists, data is added to the existing label structure in the common database. In the case of a new label, the process of creating a new label structure is repeated.

  When a new label structure is generated, there is no previous signal value in a certain clock cycle C1, and therefore, the label structure in that case stores “NULL” in “IN_LABEL”.

  After the common database is generated by the common database generation means 4, an operation proposition is generated. The action proposition is generated based on the extracted data automatically extracted from the verification item.

  Here, as an example of automatic extraction of verification items, a case where a plurality of signals are not in an active state simultaneously in a certain clock cycle (in the first embodiment, the signal value is low “0”) is taken as an example. explain. This process is performed by the simultaneous inactive signal extracting means 5A shown in FIG.

  The simultaneous deactivation signal extraction means 5A first extracts all label names from the common database. In the system bus read 1 operation, label names from LABEL_NAME = 52 to LABEL_NAME = 127 are extracted.

  The signal names sigA to sigG in the initial data “SIG_INFO {sigA, 0} to {sigG, 0}” included in the common database are arranged in rows and columns as shown in FIG. Create an array. In the figure, the upper right half area to which hatching is applied overlaps with the lower left half area.

  Here, the signal names in the two-dimensional array are arranged in rows and columns in the order of the signal names sigA to sigG in the initial data “SIG_INFO {sigA, 0} to {sigG, 0}”.

  In other words, the test for checking that two signals are not activated at the same time is, in other words, whether or not a state in which the signals are simultaneously activated, that is, a row “here,“ 0 ”” exists as a label in the common database. Is to find out.

  Therefore, first, a matrix-like two-dimensional array in which signals sigA to sigG as shown in FIG. 9 are arranged on the vertical axis and the horizontal axis is prepared.

  In the two-dimensional array shown in FIG. 9, it is necessary to inspect 21 (= 7 * 6/2) sets of signals for seven signals sigA to sigG. 21 inspection flags whose initial value is “0” are prepared.

  Then, in each combination of two signals, the inspection flag is changed to a value “1” indicating that it has already been inspected for a combination that is simultaneously in an active state, that is, a signal value of low “0” at the same time. . In FIG. 9, a check indicating the end of the inspection is written in the inspection flag of the combination of the inspected signals, for example, the combination of the signals sigC and sigA, sigD and sigB.

  On the other hand, the combination of signals that have not been found to be active at the same time, for example, the combination of the signals sigB and sigA and the combination of sigG and sigB shown in FIG. It will be.

  After completion of the inspection for all 21 signal combinations, a combination of signals whose inspection flag remains “0” indicating that it is in an initial state, here, combinations of signals sigB and siGA, and sigG and sigB are extracted. By doing so, it is possible to automatically extract a verification item that the two signals are in the active state simultaneously, that is, the signal values cannot be low “0” at the same time.

  The verification items extracted by the simultaneous inactive signal extraction means 5A are obtained from the action proposition output means 6 which is the format of the action proposition that is input to the simulator verification system and action proposition verification system (not shown), that is, the action proposition. Output as a description.

  In FIG. 10, as an example of the behavioral proposition description, the format “forever (! (SigB == 1 ′)” indicates that the signal sigB and the signal sigG are not in the active state (1′b0, that is, “0”) at the same time. b0 && sigG == 1′b0)) ”, and the format“ forever (! (sigA == 1′b0 && sigB == 1′b0)) ”indicating that the signal sigA and the signal sigB are not active at the same time. Show.

  As described above, according to the system of the first embodiment, before the logic circuit (DUT) is verified, an operation proposition is automatically created from the time-series signal value data without human intervention. Thus, the LSI verification time can be shortened. Here, in the first embodiment, it is possible to generate an operation proposition based on a verification item that a plurality of signals cannot be simultaneously activated from time-series signal value data.

  In the first embodiment, the simultaneous inactivation signal extraction process is performed in the combination of two signals. However, the present invention is not limited to this, and the simultaneous deactivation signal extraction for combinations of three or more signals can also be performed in the same procedure as in the first embodiment.

(2) Embodiment 2
An operation proposition generation system according to Embodiment 2 of the present invention will be described. In the second embodiment, the regularity existing in the signal transition is found and the operation proposition is automatically generated. FIG. 11 shows the configuration of the system according to the second embodiment.

  Compared to the first embodiment, the means for automatically extracting verification items from the common database generated by the common database generation means 4 is different. That is, instead of the simultaneous inactive signal extraction means 5A in the first embodiment, the second embodiment includes a signal transition rule extraction means 5B. The time-series signal value data 1, the signal initial state information 3, the signal state extraction means 2, and the common database generation means 4 used until the process of generating the common database are the same as those in the first embodiment, and will be described. Omitted.

  As in the first embodiment, the common database is generated by the common database generation unit 4. As described in the first embodiment, the common database makes clear the transition of the signal values of the signals sigA to sigG in three consecutive clock cycles C (j−1), Cj, and C (j + 1). .

  From this common database, a signal that transitions from an inactive state to an active state and then to an inactive state is extracted between three consecutive clock cycles. Here, the active state of all the signals sigA to sigG is when the signal value is low “0”. Therefore, a signal whose signal value transitions as “1” → “0” → “1” is extracted.

  As a specific procedure, the signal names sigA to sigG and signal value transitions over three clock cycles for each signal are extracted from the common database and arranged as shown in FIG. At that time, when it is determined that the change in the signal value of a certain signal is not “1” → “0” → “1”, the extraction of the signal value of that signal is terminated.

  That is, when the signal value of each signal is already “0” at the start time, it is not necessary to extract the signal value to transit next. In the example shown in FIG. 12A, since the signal sigA is “0” at the start time, it is not necessary to consider the signal value in the subsequent clock cycle, and the verification frame is masked by hatching.

  The signals sigB to sigG are all “1” at the start time, but only the signals sigD and sigE become “0” and the other signals become “1” in the next clock cycle, and the signal values in the subsequent clock cycles are changed. There is no need to consider.

  Since only the signal sigD becomes “1” in the next clock cycle, only this signal sigD is extracted. Also in the example shown in FIG. 12B, only the signal sigD is detected.

  In this way, it is determined whether or not further signal values need to be taken into consideration every clock cycle, and a signal name for performing a transition of a predetermined signal value is automatically extracted while omitting unnecessary tests.

  The verification items extracted by the signal transition rule extraction unit 5B in such a procedure are output by the operation proposition output unit 6 as an operation proposition format (property description) to be input to the simulator verification system or the operation proposition verification system. The

  In FIG. 13, as an example of a format indicating that the signal value of the signal sigD is always “1” in the next cycle when the signal sigD becomes active, (sigD == 1′b0 → next_C (sigD == 1′b1)).

  As described above, according to the second embodiment, it is possible to automatically extract an action proposition based on the verification items regarding the regularity of signal transition from the time-series signal value data.

  Before the verification of the logic circuit (DUT) to be verified, consistency between the specification and the operation proposition is taken, and the verification of the generated operation proposition and the verification of the logic circuit that is the original purpose are separated. As a result, the overall time required for verifying the logic circuit can be reduced.

  In the second embodiment, an operation proposition is generated based on verification items for signal value transitions in three clock cycles, but the clock cycle to be verified can be arbitrarily set. Then, it is possible to automatically extract regular signal transitions by the same procedure as in the above example.

(3) Embodiment 3
In the operation proposition verification system according to the third embodiment, an operation proposition already exists, and this operation proposition is verified.

  The operation proposition may not be automatically generated from the waveform information of the specification because the specification is described only in a natural language. According to the third embodiment, the operation proposition can be verified by utilizing the common database even for the inconsistency with the specifications existing in the operation proposition involving manpower.

  FIG. 14 shows the configuration of an operation proposition verification system according to the third embodiment. As in the first and second embodiments, the system further includes the signal value extraction unit 2 to which the time-series signal value data 1 and the initial state information 3 of the signal are input, and the common database generation unit 4. It comprises a common database, transition information extraction means 16 to which an action proposition 15 is input, action proposition analysis means 17 and action proposition modification request means 19.

  The operations of the signal value extraction unit 2 and the common database generation unit 4 are the same as those described in the first and second embodiments, and a description thereof will be omitted.

  The transition information extraction unit 16 is given the transition information of the signal value extracted from the common database generated by the common database generation unit 4 and the existing operation proposition 15, and a predetermined conditional expression described in the operation proposition is obtained. A process of extracting a satisfying state from signal value transition information is performed.

  The action proposition analysis means 17 converts the action proposition 15 into signal value transition information in which the signal value of each signal changes every clock cycle, and determines whether the description in the action proposition 15 is logically correct. Compare and analyze the transition information extracted from the common database.

  When it is determined by the analysis of the action proposition analysis means 17 that the transition information of the signal value converted from the action proposition 15 and the transition information of the signal value converted from the common database are consistent, the action proposition Since there is no error to be corrected in 15, the process is terminated.

  On the other hand, if it is determined that there is no consistency between the signal transition information from the operation proposition 15 and the signal transition information from the common database, the operation proposition modification requesting means 19 operates the operation proposition 15. A message that prompts the designer / verifier to correct the error is output. The operation proposition 15 is corrected by the design / verifier. After this message is output, the process returns to the process of the transition information extraction unit 16.

  According to the third embodiment described above, an existing operation proposition is determined by determining the consistency between the state transition information converted from the operation proposition 15 and the state transition information extracted from the waveform information of the specification. It becomes possible to perform verification.

(4) Embodiment 4
A system according to Embodiment 4 of the present invention will be described with reference to FIG. In the fourth embodiment, when the logic circuit (DUT) to be verified already exists, the verification of the consistency between the logic circuit and the time-series signal value data is performed.

  As in the first to third embodiments, this system includes signal state extraction means 2 to which time-series signal value data 1 and signal initial state information 3 are input, and common database generation means 4, and further includes a common database. And logic circuit transition information extraction means 26 to which a verification target logic circuit (DUT) 25 is input, transition information comparison means 27, time series signal value data output means 28 for outputting additional time series signal value data 29, and And transition information mismatch information output means 30. Processing until the common database is generated is the same as in the first to third embodiments, and the description thereof is omitted.

  The processing after generating the common database is described below. The logic circuit (DUT) 25 to be verified and the common database are input to the logic circuit transition information extraction unit 26. From the circuit structure of the logic circuit (DUT) to be inspected as shown as an example in FIG. 16, for example, a signal indicating the transition of signal values in the clock cycles C1, C2, and C3 of the signals sigA to sigG in the read 3 operation Value transition information is extracted. From this signal value transition information, the label name of the signal transition is extracted as shown in FIG. Here, it can be seen that in clock cycles C1, C2, and C3, the signal values of the signals sigA to sigG are arranged in binary numbers, and then converted to decimal numbers, the value transitions from 63 to 51 to 57. . Such a transition label name is extracted.

  The transition information comparison unit 27 compares and determines the label name of the signal transition extracted by the logic circuit transition information extraction unit 26 and the label name of the signal transition extracted by the common database generation unit 4.

  As a result of the comparison, when it is determined that both are consistent, the process is terminated. When it is determined that there is no consistency, the following four cases can be considered.

1) When signal transitions existing in the logic circuit (DUT) to be verified do not exist in the signal transitions of the common database extracted from the time-series signal value data In this case, there are the following two cases.

1-1) Case where time-series signal value data is correct This case corresponds to a case where time-series signal value data is correct. In this case, an unnecessary circuit exists in the logic circuit (DUT). In this case, the logic circuit 29 is not correct, and the transition information mismatch information output means 30 outputs mismatch information necessary for correcting the logic circuit to the design / verifier to prompt the circuit to be corrected. .

1-2) When the logic circuit is correct A specification change occurred during the design, and the additional specifications were reflected in the logic circuit (DUT), but the additional specifications were not reflected in the specifications, and time-series signal value data Corresponds to the case where is not correct. In such a case, the logic circuit is correct, and the time-series data output means 31 generates additional time-series signal value data 32 for updating the specifications. 2) Logic circuit (DUT) to be verified If there is a signal transition that does not exist in the signal transition of the common database extracted from the time series signal value data In this case, there are two cases as follows.

2-1) When the time-series signal value data is correct This corresponds to the case where there is no necessary circuit that should exist in the logic circuit, and the logic circuit is incorrect. Therefore, a message to that effect is output to the design / verifier, and the transition information mismatch information output means 30 outputs mismatch information necessary for correcting the logic circuit to prompt the logic circuit to be corrected.

2-2) When the logic circuit is correct The specification change occurred during the design, and the specification change was reflected in the logic circuit (DUT), but it was not reflected in the specification, and the time-series signal value data was incorrect. Case corresponds. In such a case, the logic circuit is correct, a message is output to the design / verifier, and the time-series data output means 31 generates correct time-series signal value data based on the signal transition information extracted from the logic circuit. Additional time-series signal value data 32 necessary for the generation is generated.

  The above four cases (1-1, 1-2, 2-1, 2-2) do not occur at the same time and are in a contradictory relationship. Therefore, when the transition information comparison unit 27 outputs a comparison result indicating that there is a mismatch, the transition information mismatch information output unit 29 given the output displays four possibilities. Based on this display, the design / verifier determines which case is applicable, and performs the correction as described above.

  The time series signal value data output means 28 given the comparison result from the transition information comparison means 27 generates and outputs additional time series signal value data 29 indicating the time series signal to be added based on the comparison result. .

  As described above, according to the fourth embodiment, when the logic circuit (DUT) 25 to be verified exists, the consistency between the specification and the logic circuit is compared using the logic circuit 25, and inconsistency is found. If it exists, the verification efficiency can be improved by outputting information necessary for correction.

(5) Embodiment 5
An operation proposition verification system according to Embodiment 5 of the present invention will be described. In the first, second, and third embodiments, an operation proposition is automatically extracted based on a common database generated from time-series signal value data.

  However, there may be a description omission in the time-series signal value data itself written in the specification. Therefore, it is necessary to check the validity of given time-series signal value data before extracting verification items from the common database.

  As shown in FIG. 17, the system according to the fifth embodiment includes a signal value extraction unit 2, a common database generation unit 4, a common database, to which time-series signal value data 1 and signal initial state information 3 are input. 47, a validity checking means 45 for outputting 47 and an alarm output means 46 are provided.

  The processing until the common database is generated by the signal value extracting means 2 and the common database generating means 4 is the same as in the first to fourth embodiments, and the description thereof is omitted.

  The validity checking means 45 is a means for checking the validity of the common database created based on the time series signal value data so as to correct the time series signal value data of the specification. As a result of the inspection, if it is determined that there is validity, the common database 47 whose validity is confirmed is output. If it is determined that the data is not valid, the warning output means 46 outputs a warning to prompt the design / verifier to correct the time-series signal value data.

  In the fifth embodiment, the time series signal value data is insufficient by using the common database created based on the time series signal value data of the system bus reads 1, 2, and 3 in the first embodiment. The transition information of the existing signal value is detected.

  As described with reference to FIG. 8 in the first embodiment, the common database includes the signal value transition information, that is, the signal value at the present time, the signal value at the previous clock cycle, the clock for each signal. A label structure for the signal value after one cycle is included.

  Each label “LABEL_NAME”, “IN_LABEL”, and “OUT_LABEL” in such a label structure is inspected. In the example shown in FIG. 19, “LABEL_NAME = 62, 56, 48, 50” has four “OUT_LABEL” in the label structure in the “NULL” state, that is, the signal value is invalid in the next clock cycle. It is a state. “LABEL_NAME = 127” is a state in which “IN_LABEL” is in a “NULL” state, that is, a signal value in the previous clock cycle is invalid. Assuming that the circuit operation always returns to the idling state after performing a certain operation, an effective signal value is obtained before and after any clock cycle. Therefore, the presence of an invalid signal value before or after a certain clock cycle means that not all state transitions have been described.

  In particular, “IN_LABEL” being in the “NULL” state means that the signal value immediately before the clock cycle is invalid, so that the clock cycle may be an initial state of the read operation. High nature.

  As the initial state information of the signal, the signal value at the initial stage of the signal is, for example, as shown in FIG. 18 as an example, “INIT_SIG: sigA = 0, sigB = 1, sigC = 1, sigD = 1, sigE = 1, When “sigF = 1, sigG = 1;” is written, “IN_LABEL” in the label structure is added according to the signal value.

  On the other hand, when “OUT_LABEL” is in the “NULL” state, there are two possibilities.

  The first possibility corresponds to the case where all the desired operations are described in the specification, and the transition from one cycle clock to the next cycle clock is in the initial state. When it is determined that all desired operations are described in this way, the initial state is added to the final clock cycle in the time-series signal value data so that the initial state is described in “OUT_LABEL”.

  The second possibility corresponds to a case where there is a description omission of a desired operation in the specification document. In this case, if “OUT_LABEL” is in the “NULL” state, a message warning that effect is output.

  When the designer / verifier receives a message indicating that “OUT_LABEL” is in the “NULL” state, the designer / verifier checks whether or not the desired operation is all described in the time-series signal value data included in the specification. .

  If the label transition diagram of the common database as shown in FIG. 19 is displayed on a monitor screen (not shown), the transition from the last location where the connection is broken in the transition diagram on the screen to the initial clock cycle. Connect. Through this process, the common database is updated.

  In the label structure shown in FIG. 19, it is assumed that the signal value in the next clock cycle from a certain clock cycle, that is, “OUT_LABEL” is in the “NULL” state, “62”, “56”, “48”. , “50” exists. As described above, there is no signal value in the subsequent clock cycle after the signal value is stopped in a certain clock cycle, and there is a final clock cycle having no connection destination. Further, there is a clock cycle such as “127” in which there is no signal value in the previous clock cycle.

  In such a case, as shown in FIG. 20, the signal value of the next clock cycle from the last clock cycle “62”, “56”, “48”, “50” in which the connection is broken is set as “ By connecting to “127”, correction is performed.

  Such a modification guarantees consistency between the specification and time-series signal value data, and when an operation proposition is created using this time-series signal value data, the consistency between the operation proposition and the specifications. Is also secured.

  As described above, according to the fifth embodiment, before the verification is performed using the logic circuit (DUT) to be verified, the consistency between the specification and the time-series signal value data is ensured, and the operation proposition is further ensured. It is possible to ensure consistency with the specifications.

  The above-described embodiment is an example, and does not limit the present invention, and various modifications can be made within the technical scope of the present invention.

The block diagram which shows the structure of the system by Embodiment 1 of this invention. The wave form diagram which shows an example of the time series signal value data described in the specification in Embodiment 1. Explanatory drawing which showed the matrix data which shows the signal value of each signal for every clock cycle extracted from the time-sequential signal value data in the first embodiment. The wave form diagram which shows an example of the additional time series signal value data described in the specification in Embodiment 1. FIG. 3 is an explanatory diagram showing matrix data indicating signal values of each signal for each clock cycle during read 1 and read 2 operations in the first embodiment. In the first embodiment, matrix data indicating the signal value of each signal for each clock cycle at the time of read 1 and read 2 operations obtained by converting from three time-series signal value data written in the specification is shown. Illustration. Explanatory drawing which shows an example of the signal information data contained in a common database in Embodiment 1. FIG. Explanatory drawing which shows an example of the label structure contained in a common database in Embodiment 1. FIG. Explanatory drawing which shows the test flag of a simultaneous inactive signal in the same Embodiment 1. FIG. Explanatory drawing which shows an example of the operation proposition obtained based on the test result of the simultaneous inactive signal in the first embodiment. The block diagram which shows the structure of the system by Embodiment 2 of this invention. Explanatory drawing which shows the process which extracts the rule in which a signal changes over 3 continuous clock cycles in the same Embodiment 2. FIG. Explanatory drawing which shows an example of the operation proposition extracted in the same Embodiment 2. FIG. The block diagram which shows the structure of the system by Embodiment 3 of this invention. The block diagram which shows the structure of the system by Embodiment 4 of this invention. Explanatory drawing which shows the example which extracts signal transition information from the logic circuit description of verification object in the same Embodiment 4. FIG. The block diagram which shows the structure of the system by Embodiment 5 of this invention. Explanatory drawing which shows an example of the initial state information of a signal in Embodiment 5 of this invention. Explanatory drawing which shows an example of the transition of the label structure in the same Embodiment 5. FIG. Explanatory drawing which shows the transition at the time of correcting the transition state of the label structure in FIG.

Explanation of symbols

1 time-series signal value data 2 signal value extraction means 3 signal initial state information 4 common database generation means 5A simultaneous inactive signal extraction means 5B signal transition rule extraction means 6 action proposition output means 7 action proposition 15 action proposition 16 transition information extraction Means 17 Behavior proposition analysis means 19 Behavior proposition correction request means 25 Logic circuit 26 to be verified Logic circuit state transition extraction means 27 Transition information comparison means 28 Time series signal value data output means 29 Additional time series signal value data 30 Transition information mismatch Information output means 45 Validity checking means 46 Alarm output means 47 Common database

Claims (5)

A signal value extraction unit which is given time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals;
Based on the initial state information about each signal value of a plurality of signals in the initial state of the circuit and the signal value transition information, the signal value in a certain clock cycle and the signal values in the clock cycle before and after the clock cycle are common A common database generation means for generating a database;
Simultaneously inactive signal extraction means for extracting a simultaneous inactive signal that is a combination of a plurality of signals that do not become active at the same time based on the common database;
An operation proposition output means for generating and outputting an operation proposition based on the extracted simultaneous inactivation signal;
A system for generating a motion proposition characterized by comprising: A signal value extraction unit which is given time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals;
Based on the initial state information about each signal value of a plurality of signals in the initial state of the circuit and the signal value transition information, the signal value in a certain clock cycle and the signal values in the clock cycle before and after the clock cycle are common A common database generation means for generating a database;
Signal transition regularity extracting means for extracting regularity of transition of the signal value that changes in units of clock cycles based on the common database;
An action proposition output means for generating and outputting an action proposition based on the regularity of the extracted transition of the signal value;
A system for generating a motion proposition characterized by comprising: A signal value extraction unit which is given time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals;
Based on the initial state information about each signal value of a plurality of signals in the initial state of the circuit and the signal value transition information, the signal value in a certain clock cycle and the signal values in the clock cycle before and after the clock cycle are common A common database generation means for generating a database;
Transition information extracting means for extracting signal value transition information given a motion proposition and indicating a state satisfying a predetermined condition included in the motion proposition;
An operation proposition analysis unit that compares the signal value transition information based on the common database with the signal value transition information extracted by the signal value extraction unit, and determines the presence or absence of consistency;
When it is determined by the action proposition analysis means that there is no consistency, action proposition correction means for instructing correction of the action proposition;
A proposition verification system characterized by comprising: A signal value extraction unit which is given time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals;
Based on the initial state information about each signal value of a plurality of signals in the initial state of the circuit and the signal value transition information, the signal value in a certain clock cycle and the signal values in the clock cycle before and after the clock cycle are common A common database generation means for generating a database;
Logic circuit state transition extraction means for reading a logic circuit to be verified and extracting signal value transition information;
Transition information comparing means for comparing the signal value transition information included in the common database with the signal value transition information extracted by the logic circuit state transition extracting means;
Transition information mismatch information output means for outputting information on mismatch included in the logic circuit when the transition information comparison means determines that the signal value transition information included in the common database is correct;
When the transition information comparison unit determines that the signal value transition information extracted by the logic circuit state transition extraction unit is correct, it outputs additional time series signal value data to be added to the time series signal value data. Time-series signal value data output means;
A proposition verification system characterized by comprising: A signal value extraction unit which is given time-series signal value data and extracts signal value transition information related to a signal value for each clock cycle of a plurality of signals;
Based on the initial state information about each signal value of a plurality of signals in the initial state of the circuit and the signal value transition information, the signal value in a certain clock cycle and the signal values in the clock cycle before and after the clock cycle are common A common database generation means for generating a database;
Validity checking means for extracting signal value transition information from the common database and checking the validity of the common database based on whether an invalid state exists in the signal value for each clock cycle;
An alarm output means for outputting an alarm when the time series signal value data is to be corrected based on the inspection result by the validity inspection means;
A proposition verification system characterized by comprising:

Images