JP2001142918A - Apparatus and method for generating property to be verified for hardware - Google Patents

Abstract

(57) [Summary] [PROBLEMS] To provide a method for automatically generating a property to be verified for hardware described in a hardware description language. A data resource and a data transfer described in a hardware description language are represented using a data transfer display graph (step S1). The data transfer graph is optimized (Step S2). The optimization process simplifies or minimizes the data transfer graph. A property to be verified by the verification tool is generated based on the topology of the optimized data transfer graph (Step S)
3). Properties to verify are resource conflicts and register omissions.

Description

DETAILED DESCRIPTION OF THE INVENTION

[0001]

BACKGROUND OF THE INVENTION 1. Field of the Invention The present invention relates to an apparatus and a method for generating a property to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources.

[0002]

2. Description of the Related Art In recent years, the design of semiconductor chips has become very complicated. That is, very complicated hardware (logic device) is being mounted on a semiconductor chip. For this reason, the design of a semiconductor chip is often performed by a joint work of a plurality of designers.

However, design information segmented by a plurality of designers may be erroneously interpreted by each designer. In this case, an error in some part (design error)
May cause the whole system to not operate properly at the register transfer level. And if there is such an error, a great deal of money and time will be wasted on debugging work and the like.

Meanwhile, resources (for example, registers, buses, input ports, output ports, etc.) that can be provided on a semiconductor chip are limited. For this reason, each resource is usually shared by a plurality of tasks. The data generated by the shared resource is often temporarily stored in a data storage resource (for example, a register).

[0005] Design errors that frequently occur in such a situation are "resource conflict" and "register omission". Resource contention is an error in which one resource (such as a register) is accessed simultaneously by multiple resources. On the other hand, register omission is an error related to the access order when a certain register is accessed by a plurality of resources.

[0006] An enormous number of resources are formed on a semiconductor chip on which complicated hardware is mounted. For this reason, the above errors (resource conflicts, register omissions, etc.)
It is practically impossible to find all of them manually. However, even a single error in the designed hardware may prevent the entire system from operating properly. Therefore, it is very important to find and eliminate all resource conflicts and register leaks.

[0007]

Many designers have recognized the importance of finding resource conflicts and register leaks early in the design process. However, to date, work to find resource conflicts and register omissions has
It is only performed by each designer for each subsystem in charge of that designer.

In order to guarantee the operation of the entire system,
Verification of each subsystem alone is not enough. It is necessary to search for resource conflicts and register leaks throughout the designed hardware and remove them. However, such an operation has not been conventionally performed. For this reason,
If errors are included in the hardware design, those errors are usually detected after the hardware design is mounted on a semiconductor chip.

To the knowledge of the applicant of the present patent application, resource conflicts and register omissions are automatically detected and formulated,
There is no tool to check. And without such a tool, it would be virtually impossible to achieve an error-free hardware design.

An object of the present invention is to provide an apparatus and a method capable of generating a property to be verified for hardware described by a hardware description language.

[0011]

SUMMARY OF THE INVENTION A property generating apparatus according to the present invention generates a plurality of resources described in a hardware description language and a property to be verified for hardware including data transfer using the resources. And the following means are provided. The graph generation means generates a data transfer graph corresponding to resources and data transfer described in a hardware description language. The optimizing unit optimizes the data transfer graph generated by the graph generating unit. The property generation unit generates a property to be verified for the hardware described in the above hardware description language, using the data transfer graph optimized by the optimization unit.

In the above configuration, the design information described in the hardware description language is graphed, and the properties to be verified for the hardware are automatically generated using the graph. At this time, since the data transfer graph is optimized before the property is generated, the property can be easily generated. The generated property is verified by a verification tool.

Resources are, for example, registers, buses, input ports, and output ports, and are each represented by a node in the data transfer graph. On the other hand, data transfer is represented using edges (arrows) in which the transfer source and the transfer destination are defined. Then, the optimizing means minimizes the graph based on the topology of the data transfer graph.

The properties to be generated are, for example, resource contention and register omission. The resource conflict property is detected in the data transfer graph at a node to which a plurality of fan-in edges are connected. On the other hand, a register leak is detected at a node representing a register to which a fan-in edge and a fan-out edge are connected in the data transfer graph.

[0015]

Embodiments of the present invention will be described below with reference to the drawings. FIG. 1 is a diagram illustrating an environment in which a property generation tool according to an embodiment of the present invention is used. The property generation tool 1 of the present embodiment includes:
The property is extracted from the hardware specification 2 created in advance and the verification tool 3 verifies the property.

The hardware specification 2 is a design description of a certain hardware (for example, a logic device such as a processor mounted on a semiconductor chip), a plurality of resources included in the hardware, and data between the resources. Define the transfer. This hardware specification 2 is described in, for example, a hardware description language of a register transfer level. The hardware description language is, for example, Verilog. The defined resources are, for example, registers, register files, buses, input ports, output ports, input / output ports, and the like.

The hardware described in the hardware specification 2 includes one or more modules. When there are multiple modules, they are often described hierarchically. In this case, an upper-layer module is often called a “parent” and a lower-layer module is sometimes called a “child”. Each module includes one or more resources.

The property generation tool 1 analyzes the input hardware specification 2 and determines properties (a verification tool 3
Extracts items or conditional expressions to be verified. In this embodiment, the properties are “resource conflict” and “register omission”, and are expressed by a temporal logic expression (conditional expression of signal change over time) such as CLT, for example.

The verification tool 3 is an existing logic verification tool, and verifies the properties extracted by the property generation tool 1. Specifically, it is verified whether or not “resource conflict” or “register omission” occurs in the hardware described by the hardware specification 2. The verification tool 3 can also verify other items.

FIG. 2 is a flowchart for explaining the operation of the property generation tool 1. This process is executed when the hardware specification 2 is input. Step S
1 (Phase 1), based on the description of the hardware specification 2, the data transfer graph (DTDA: Data Transfer Digraph)
rected Acyclic Graph) is created. At this time, the resources are recognized for each module defined in the hardware specification 2, and when the modules are described hierarchically, the parent-child relationship of those resources is also recognized. Also, conditions relating to data transfer are taken into account. These conditions are described in Hardware Specification 2. The data transfer graph represents resources and data transfer included in the hardware described by the hardware specification 2.

In step S2 (Phase2), step S2
The data transfer graph created in 1 is optimized (simplified or minimized). Specifically, of the resources and data transfers represented in the data transfer graph, resources or data transfers that are unlikely to cause “resource conflict” or “register omission” are deleted.

In step S3 (Phase3), step S3
In step 2, properties are extracted from the optimized data transfer graph, and corresponding input scripts are generated. This input script is described in a format that the verification tool 3 can process.

Next, a data transfer graph and properties to be extracted will be described with reference to FIG. FIG. 3 is an example of a data transfer graph. This data transfer graph is created based on the input hardware specifications, but the description of the creation method is omitted here.
Basically, the data transfer graph is not actually displayed on the computer screen. Therefore, FIG.
Is a data transfer graph. This is the same in the following drawings. However, it is possible to actually display the data transfer graph on the computer screen, and this may be done.

Each of the nodes A to F, H, and I corresponds to a data resource. For example, in the hardware specification 2, the node A has an “interface control register file”
Is a register given the name. Arrows drawn between nodes correspond to data transfer. Hereinafter, this arrow is referred to as “data transfer edge” or simply “edge”. Further, for example, the edge corresponding to the data transfer from the node A to the node D is a fan-out edge (or an output edge) for the node A, and at the same time, a fan-in edge (or an input edge) for the node D. is there.

Each data transfer edge is given a definition and a condition for the data transfer. “C” indicates that data transfer is “Concurrent Transfer”, and “S” indicates that data transfer is “Sequential Transfer”. Also,
"Gi" is the operating condition (guardor
enabling condition). For example, in the example shown in FIG. 3, when the condition G1 is satisfied, data transfer from the node A to the node D is executed.

In the above data transfer graph, when there are a plurality of fan-in edges for a certain node (Mu
ltiple fan-in), "resource competition" may occur. Attention is paid to node D. Node D is a 32-bit register "reg data out". Node D has an edge AD
And the edge BD are input. Therefore, when the condition G1 is satisfied, the node A (register "interfa
ce control registerfile ") is transferred to the node D (register" reg data out "), and when the condition G2 is satisfied, the data is transferred from the node B (input port" data out ") to the node D (Register "reg data ou
t "). In this case, if the conditions G1 and G2 are simultaneously satisfied in any clock cycle, two write accesses to the register" reg data out "occur simultaneously. That is,
"Resource contention" will occur.

[0027] "Resource contention" as described above can occur in a node where a plurality of fan-in edges exist in the data transfer graph. Therefore, the property generation tool 1 detects a node where a plurality of fan-in edges exists in the data transfer graph. Then, the verification tool 3 verifies whether or not “resource conflict” actually occurs, taking into account the data transfer timing relating to the node.

If a fan-in edge and a fan-out edge exist for a certain node, "register omission" may occur. For example, the node D has a fan-in edge AD, a BD, and a fan-out edge DF. Here, it is assumed that the hardware performs an operation of transmitting data of the node A to the node F via the node D and then writing data of the node B to the node D. Therefore, this operation is performed under the condition G
Obtained when 1, G6, G2 are satisfied in that order. However, if condition G6 is not satisfied before condition G6 is satisfied,
When 1 and the condition G2 are satisfied, the data transfer from the node D to the node F is executed after the node D is overwritten by data transferred from the node B. That is, "register omission" occurs.

Note that "register omission" can also occur when there is only one fan-in edge for a certain node.
For example, when data is transferred from the first node to the third node via the second node, the first node is transferred before the data transfer from the second node to the third node is performed. When other data is transferred from the first node to the second node, "register leak" may occur as in the above-described case.

As described above, "register omission" as described above can occur when one or more fan-in edges and one or more fan-out edges exist at a certain node in the data transfer graph. Therefore, the property generation tool 1 detects a node having a fan-in edge and a fan-out edge from the data transfer graph. Then, the verification tool 3 verifies whether or not “register leakage” actually occurs, taking into account the data transfer timing relating to the node.

Another problem is inherent when there is a fan-in edge and a fan-out edge for the node corresponding to the register. For example, if a condition related to a fan-in edge of a node corresponding to a certain register and a condition related to a fan-out edge of the node are satisfied in the same clock cycle, write access and read access to the register are performed. Will be performed simultaneously. Such a situation is not necessarily an error in the register transfer level model. However, in this situation, if clock distortion is taken into account at the gate level or the layout level, erroneous data may be read from the register. That is, if the clock is distorted, new data may be written to the register in a certain clock cycle before data reading from the register is completely completed. This problem appears as a register leakage property on an actual semiconductor chip. In the example shown in FIG. 3, for example, this kind of “resource conflict” may occur between the data transfer from the node I to the node C and the data transfer from the node C to the node D.

As described above, the verification tool 3 determines whether or not “resource conflict” and “register omission” actually occur.
Is verified by That is, the property generation tool 1
Automatically generates properties from which these problems may occur from the hardware specification 2 and passes them to the verification tool.

The above-mentioned properties ("resource conflict" and "register omission") relate to the topology of the described hardware resources and data transfer when the data transfer is represented by a data transfer graph. That is, by analyzing the topology of the data transfer graph, it is possible to determine the possibility of occurrence of “resource conflict” or “register omission”. Therefore, the property generation tool 1 can automatically generate a property from the topology of the data transfer graph. However, in this case, information related to resources and data transfer
It must be extracted from the register transfer level code.

When the hardware described in the hardware specification 2 becomes large in scale, the data transfer graph generated from the description necessarily becomes complicated. For this reason, the property generation tool 1 optimizes (minimizes or simplifies) the generated data transfer graph in order to generate the property accurately and in a short time. As an optimization method, optimization based on the topology of the data transfer graph (topology optimization) and optimization based on the operation conditions of data transfer (logic optimization) can be considered.

FIG. 4 is a flowchart of a process for optimizing a data transfer graph. This processing corresponds to step S2 in FIG. In step S11, "Unfragmented Equivalence" is detected.
In step S12, "Fragmented
Equivalence). In step S13,
Detects "Named Equivalence". In step S14, "Fragmented Edg
es) "is detected. In step S15, "Edges in Equivalence" is detected. Step S1
In step 6, "Register File" is detected. In steps S11 to S16, an equivalence relationship between resources is detected. Then, by using these equivalence relations, a portion that is unlikely to cause “resource conflict” or “register omission” is deleted from the data transfer graph. This optimizes (ie, minimizes) the data transfer graph.

Here, some of the processes in steps S11 to S16 will be briefly described. The processes in steps S11 to S16 will be described in detail with reference to a flowchart described later.

FIG. 5 shows an example of hardware. FIG.
FIG. 6 is a diagram illustrating a method of hierarchically describing the hardware illustrated in FIG. 5. Hardware resources and data transfer are often designed and described hierarchically, as shown in FIG. Here, “module 0” is an upper layer, and “module 1” and “module 2” are lower layers of “module 0”.

As described above, when data resources and data transfer are described for each hierarchy, different names are often given to the same resource or data. For example, in the example shown in FIG. 6, "input 1" which is an input to module 0 is "input 11" in module 1.
It is described as

In the hardware description language, data transfer between modules is usually described using an input port or an output port. For example, module 0
"Input 1" in module 1 and "input 11" in module 1
Is often associated with "input por" in module 0
This is expressed as data transfer from "t1" to "input port 11" of module 1. In the present embodiment, such a correspondence between ports is referred to as a "port association".
Call. The “port cooperation” is defined in the hardware specification 2.

In the hardware description language, when data stored in a register in a certain module is transferred to another module, the data is described so as to be transferred via an output port. In this case, the output port is usually given the same name as the name given to the register. In the present embodiment, this correspondence is referred to as “Named Association”.

FIG. 7 is a diagram showing an example of optimizing a data transfer graph using "equivalent of resources". Fig. 7 (a)
Shows a data transfer graph generated from the resource and data transfer definitions described in the hardware specification 2. In this embodiment, the module 1 is provided with three resources (input port SD-DQ-IN, register data-in, output port data-in). The output of the module 1 is transferred to the bus wire data-buf-out defined in the module 2 and further transferred to the register reg-data-out defined in the module 3.

Here, the register data-in and the output port data-in have a “name association” relationship with each other. That is, these two resources can be regarded as equivalent (name equivalent). Therefore, input port SD
Data transfer from -DQ-IN to register data-in can be treated as data transfer from input port SD-DQ-IN to output port data-in. The output port data-in and the bus wire data-buf-out have a “port cooperation” relationship with each other. That is, these two resources can be considered equivalent. Therefore, input port SD-DQ-
Data transfer from IN to output port data-in can be treated as data transfer from input port SD-DQ-IN to bus wire data-buf-out. By utilizing these equivalence relationships, the data transfer graph shown in FIG.
(b) is optimized (that is, simplified).

Note that, in order for the source resource of the data transfer and the destination resource to be equivalent, the bit widths of the data handled by those resources need to be the same. Therefore, the following definition is obtained. Definition 1: 1 adjacent to each other
If the sets of resources have the same bit width specification, their equivalent resources are "non-fragment equivalent".

FIG. 8 is a diagram for explaining a "fragment". In the example shown in FIG. 8, an output port OP having a 32-bit width is provided in the module C at the intermediate level, and output ports OP1 to OP4 having an 8-bit width are provided in the module B at the higher level.

Here, when there is data transfer between a data resource having a certain data width and a data resource having a data width smaller than the data width (or a data resource having a data width larger than the data width). , "Fragment equivalence" can occur. In the example shown in FIG. 8, the output ports OP1 to OP4 of the module B are regarded as “fragment equivalent” in relation to the output port OP of the module C.

The output port O in the model shown in FIG.
P and the output ports OP1 to OP4 are represented by nodes in the data transfer graph, and data transfer from the output port OP to the output ports OP1 to OP4 is performed by:
Each is represented by an edge. Here, as described above,
When the nodes respectively corresponding to the output ports OP1 to OP4 are “fragment equivalent”, the four edges corresponding to the data transfer are fragment edges. In the present embodiment, a plurality of edges connected to nodes that are “fragment equivalent” are referred to as “fragment edges”.

The utility of "fragment equality" is that non-fragment data transfers can be obtained by combining fragment data transfers. Also,
Whether the data transfer is a fragment data transfer or a non-fragment data transfer can be identified based on whether the source resource or the destination resource of the data transfer is “fragment equivalent”.

Another method for optimizing fragment data transfer is "independent fragment data transfer". The following definition is provided for this “independent fragment data transfer”. Definition 2: If there is no resource contention in any combination of edges among the fragment data transfer edges, those edges are "independent".

In the optimization processing of this embodiment, "independent" edges are deleted from the data transfer graph. This prevents the resource conflict property or the register leak property from being erroneously generated.

The register file is a technique for grouping a plurality of registers to simplify the connection between a bus and each register in order to reduce the hardware scale.
Thus, for example, the configuration shown in FIG.
Is simplified. However, each register belonging to the register file is often described as an independent register in the hardware description language. in this case,
The register file is represented as a plurality of registers in the data transfer graph. Therefore, in the data transfer graph optimizing process, a register file is recognized, and a plurality of nodes corresponding to a plurality of registers belonging to the register file are replaced with one node.

Next, specific examples will be described. First Embodiment FIGS. 10 to 15 are examples of hardware specifications 2 input to a property generation tool 1. FIG. Here, Verilog is used as a hardware description language.

FIG. 10 is a code describing module 0. According to the description in section 1 of this code, module 0 has two input ports (INPUT1,2),
And two output ports (OUTPUT1, 2). Each of these ports is 16 bits wide. Also,
The module 0 receives a clock and a control signal. Further, the module 0 is provided with a bus wire CONEKT having a width of 16 bits.

According to the description in section 2, module 1 is provided in a lower hierarchy of module 0. A port correspondence (port cooperation) between module 0 and module 1 is defined. In this example, for example, 8 to 1 of input port INPUT1 of module 0
Five bits are associated with input port IPORT3 of module 1, and bits 0 to 7 of input port INPUT1 of module 0 are associated with input port IPORT4 of module 1. In this case, input port INPUT1 is connected to input port IPORT3
And the input port IPORT4 is the “parent resource”, and the input port IPORT3 and the input port IPORT4 are the input ports
It is "child resource" of INPUT1. Also, bus wire CONEKT
Are connected to the input ports IPORT1 and IPORT2 of the module 1.

According to the description of section 3, module 2 is provided in a lower hierarchy of module 0. In section 3, the correspondence of ports between module 0 and module 2 is defined. The bus wire CONEKT is connected to the output port OPORT1 of the module 2.

FIG. 11 and FIG. 12 are codes describing module 1. According to the description in section 4, each input port (IPORT1-4), output port (OPORT1,
2) are each 8 bits wide. Section 5
According to the description, the module 1 is provided with the register A and the register B. Then, the data stored in the register A is transferred to the output port OPORT1, and the data stored in the register B is transferred to the output port OPORT2. Note that these data transfers are performed irrespective of the clock or control signal. That is, these data transfers belong to the simultaneous transfer (Concurrent Transfer) type. Specifically, "continuousassignment"
It is transfer by.

According to the description in section 6, the control signal 1
Is supplied, the data input to the input port IPORT1 is written into the register A, and the input port IPORT3
Is written into the register B. Also, according to the description in section 7, when the control signal 2 is given, the data input to the input port IPORT2 is written to the register A, and the data input to the input port IPORT4 is written to the register B. These data transfers are performed according to control signals. That is, these data transfers are performed sequentially (Sequential Transfer).
) Belongs to the type. Specifically, "sequential always bl
ock "transfer.

FIGS. 13 to 15 show codes describing the module 2. According to the description in section 8,
Each input port (IPORT5) and each output port (OPORT3, 4) are 16 bits wide. According to the description in section 9, the module 2 includes the registers C to F.
Then, the data stored in the register E is transferred to the output port OPORT3, and the data stored in the register F is transferred to the output port OPORT4. These data transfers are simultaneous transfers. Also, in each of the registers C to F,
Each is given a predetermined initial value.

According to the description in section 10, when the control signal 3 is applied, the data input to the input port IPORT5 is written to the register C. Otherwise, the data input to the input port IPORT5 is written to the register C. D is written. According to the description in section 11, when the control signal 4 is applied, predetermined operation result data is written into the registers C and D. Further, according to the description in section 12, predetermined operation result data is also written in the register F.

According to the description in the section 13, when the control signal 5 is applied, the data stored in the register C is written into the register E. When control signal 6 is applied without application of control signal 5, register D
Is written to the register E.
Further, when control signal 7 is applied without application of control signals 5 and 6, and when control signals 5 to 7 are not applied, predetermined constant data is written in register E, respectively.

FIG. 16 is a data transfer graph generated from the hardware specifications shown in FIGS. This graph corresponds to step S in the flowchart shown in FIG.
Generated by The data resources defined in the hardware specification are as follows in the data transfer graph:
Expressed as a "node". And for each node,
The data resource name, data resource type (register, bus wire, port, etc.), module name, and node name are set. Each data transfer is represented by an edge (in FIG. 16, indicated by an “arrow”) in the data transfer graph.

The data transfer graph is schematically drawn for easy understanding of the present invention, and is actually composed of a module list, a data resource list, a data transfer edge list, an equivalent class list, and the like. You.

The module list stores the following information for each module defined in the hardware specifications. -Name of the module-Parent module (module of the upper layer of the module)-Child module (module of the lower layer of the module)-Layer level (layer to which the module belongs)-Processing state (represents an intermediate state in the optimization processing) Various pointers For example, as information to be stored in the module list for module 0, the following can be obtained from hardware specifications.

• Module name: MOD0 • Parent module: none • Child module: MOD1, MOD2 • Hierarchy level: 0 Note that the “processing state” is a flag or the like indicating an intermediate state in the optimization processing, and is a hardware specification. Not obtained from. Also, "pointers" are not derived from hardware specifications.

The data resource list stores the following information for each data resource defined in the hardware specifications. This list is generated for each type of resource (register, input port, output port, bus, data transfer, constant,...).

Resource name Parent module Hierarchy level Bit width specification Parent resource Child resource Non-fragment equivalent class Fragment equivalent class Edge Edge Processing state For example, data resource list for input port INPUT1 (node A) The following information is obtained from the hardware specifications as information to be stored in.

Resource name: INPUT 1 Parent module: None Hierarchical level: 0 Bit width specification: “15: 0” Parent resource: None Child resource: IPORT 5 Edge: Edge AF Note: “Non-fragment equivalent The "class" and "fragment equivalence class" are not obtained from the hardware specification but are obtained by analyzing the data transfer graph.

The data transfer edge list stores the following information for each data transfer defined in the hardware specification. -Name of edge-Transfer destination resource-Transfer source resource-Guard expression (data transfer condition)-Data transfer type (simultaneous transfer or sequential transfer, etc.)-Transfer destination or transfer source fragment state-Processing state in optimization processing For example , Input port IPORT1 (node J) to register RE
As information to be stored in the data transfer edge list for the edge corresponding to the data transfer to the GA (node 0), the following is obtained from the hardware specification.

Edge name: JO Transfer destination resource: register REG-A (node 0) Transfer source resource: input port IPORT1 (node J) Guard expression: CTRL1 Data transfer type: S (sequential transfer) , "Destination or source fragment state"
Obtained by analyzing the data transfer graph.

The equivalence class list stores the following information. These pieces of information can be obtained by analyzing the data transfer graph. -Equivalent class identifier-Resources belonging to each equivalence class-Processing status When creating a data transfer graph, first, the description of each module in the hardware specification is analyzed in order from the upper layer and defined. Recognize each data resource, the correspondence between those resources, and data transfer using those resources. At this time, to check whether there is a call from one module to another module,
The ral description is scanned. When such a call is made, a search queue is provided for each called module, and the correspondence of the interface definition with the previously recognized resource is recognized.

Further, it recognizes the bit width of each port (including an input port, an output port, and an input / output port), a bus wire, and a register, and further recognizes, for each bus wire, a driver and a register corresponding to the bus wire.

The information extracted from the hardware resource 2 is
Stored in the module list, data resource list, and data transfer edge list. In the example shown in FIGS.
By these processes, each of the nodes A to Y shown in FIG.
(Except E, G, P, Q, and R) are generated, and the bit width is set.

Further, conditions set for each data transfer are analyzed. These conditions are, for example, "gurded co
ntinuous assignment statement "," combinational alw
ausblock "and" sequential always block "These pieces of information are registered in the data transfer edge list for each data transfer as a" guard expression ". As a result, an edge corresponding to each data transfer is generated. For data transfer for which no conditions are set, “1” is assigned to the data transfer.

When an assignment expression is described in the hardware specification (for example, section 10 and section 11), as shown in FIG.
Is generated. This pseudo resource Sdt is a virtual data source that implements the described assignment expression. For example, a node P (Sdt3) corresponding to the assignment expression described in section 11 is generated. The same applies to nodes E and G. In addition, when a predetermined constant is written in a certain register (for example, section 13),
As shown in (b), a pseudo resource Sdc is generated. This pseudo resource Sdc is also a virtual data source. For example, nodes Q and R are generated corresponding to the definition described in section 13. Note that these pseudo resources are generated by registering predetermined information in a data resource list based on hardware specifications.

Subsequently, the data transfer graph generated as described above is optimized. In the example shown in FIG. 16, the data transfer graph is optimized by detecting “non-fragment equivalent”, “fragment equivalent”, and “independent edge” in the data transfer graph.

When detecting “non-fragment equivalent”,
A set of resources defined in the interface definition of the hardware specification as being "equivalent" to each other,
Recognize that the data widths are the same. In this case, the target resources are, for example, input ports, output ports, and input / output ports. Then, when a resource belonging to the non-fragment equivalence class is detected, information indicating the fact is registered in the storage area corresponding to the resource in the data resource list.

The above equivalence relation is checked for each port. At this time, the processing is continued for each port until it reaches the final resource or until it reaches a resource having a different bit width.

Here, "non-fragment equivalent" in the graph shown in FIG. 16 will be described. Node A (INPUT2 of Module 0) and Node F (IPORT of Module 2)
5) are both 16-bit input ports. Also, these input ports are described in Section 3 of the hardware specification.
Are resources that correspond to each other, as defined in
That is, the resource corresponding to the node F is a “child” of the resource corresponding to the node A. Therefore, nodes A and F are "non-fragment equivalent". Similarly, node C is equivalent to node D, and node X is equivalent to node W.

In this case, for example, if resources A and F belong to the non-fragment equivalence class # 1,
In the data resource list, “# 1” is registered in the “non-fragment equivalent class” of the resources A and F, respectively.

When detecting “fragment equivalent”,
Recognize the equivalent of the branched resources. In the example shown in FIG. 16, for example, data is transferred from node B to node H and node I. At this time, the bit specifications of the node B are 16 bits wide, while the bit specifications of the nodes H and I are each 8 bits wide. That is, the bit width used at each transfer destination node is smaller than the bit width used at the transfer source node. Therefore, the nodes H and I are “fragment equivalent”. This is the same for the nodes J and K.

On the other hand, data is transferred to node Y from nodes S and T. At this time, the bit width used at each transfer source node is smaller than the bit width used at the transfer destination node. Therefore, node S
And the node T are “fragment equivalent”.

In this case, for example, assuming that resource H and resource I belong to fragment equivalence class # 5, “# 5” is registered in “fragment equivalence class” of resources A and F in the data resource list. Is done.

The “independent edge” is as follows. For example, node P transfers data only to node U, and node U receives data only from node P. In this case, the edge corresponding to the data transfer from the node P to the node U is an independent edge. Also, at node Y,
Data is being transferred from the nodes S and T. At this time, 0-7 bits are transferred from the node S, and the node T
8 to 15 bits are transferred. That is,
The data bits do not overlap in these two data transfers. In this case, the edge corresponding to the data transfer from the node S to the node Y and the edge corresponding to the data transfer from the node T to the node Y are both independent edges. In the graph shown in FIG. 16, in addition to the above, for example, data transfer from node N to node S, data transfer from node O to node T, data transfer from node U to node D, and node V to node W Are also independent edges.

In connection with “independent edge”, the concepts of “fragment edge” and “equivalent edge” are introduced.
“Fragment edge” refers to an edge in which the source resource or the destination resource belongs to the fragment equivalence class. For example, in the example shown in FIG. 16, since the nodes J and K belong to the fragment equivalence class, in this case, the edge CJ, the edge CK, the edge JO,
The edge KO is a fragment edge related to this equivalence class. Note that each edge is (1) the state where both the source and destination resources are not "fragment equivalent", and (2)
A state where only the transfer source resource is "fragment equivalent",
(3) The state where only the resource of the transfer destination is “fragment equivalent”, and (4) the state where both the resources of the transfer source and the transfer destination are “fragment equivalent”. This classification is
Each edge is represented by a 2-bit flag.

An “equivalent edge” is a set of edges in which the source resource or the destination resource is a node belonging to the fragment equivalence class. For example, since the nodes J and K belong to the fragment equivalence class, in this case, the edge CJ, the edge CK, the edge JO, and the edge KO are the equivalent edges related to this equivalence class. Note that the independent edge is removed from the set of edges belonging to the equivalent edge.

After detecting the equivalence relation as described above,
Eliminate parts not related to "resource conflict" or "register omission" from the data transfer graph. Specifically, nodes A and F are "non-fragment equivalent".
Therefore, node A is removed. Also, the edge VW
Are “independent edges”, and the nodes W and X are “non-fragment equivalent”. Therefore, nodes W and X are removed. Further, the edge PU and the edge UD are “independent edges”, respectively, and the node D and the node C are “non-fragment equivalent”. Therefore, nodes P, U, and D are removed.

The nodes H and I are “fragment equivalent” as viewed from the node B. Therefore, node B is removed. Similarly, node C is also removed. The nodes S and T are “fragment equivalent” as viewed from the node Y. Therefore, node Y is removed. Furthermore, edge N
S and edge OT are both independent edges. Therefore, nodes S and T are eliminated.

As a result of the above processing, the data transfer graph shown in FIG. 16 is optimized to the state shown in FIG. The above-described process corresponds to a process of generating an edge list Efinal from a data resource list, a data transfer edge list, and the like. The edge list Efinal is a list of edges obtained as a result of the optimization processing.

When the optimization process ends, the process of step S3 in the flowchart of FIG. 2 is executed. This process
As shown in FIG. 19, there are two steps. In step S21, an adjacent node list is created from the optimized data transfer graph. Subsequently, in step S22, a property and a verification script corresponding to the property are generated. In the present embodiment, all conditions that may cause “resource conflict” or “register omission” are extracted. Specifically, the number of input edges and the number of output edges for each node are counted using the adjacent node list, and a property is generated based on the count. Then, the conditions under which the extracted “resource conflict” or “register omission” may occur are converted into a script executable by the verification tool 3.

A process for generating a property from the graph shown in FIG. 18 will be described. First, a neighboring node list is created from the optimized graph. The adjacent node list is obtained by detecting the transfer source node and the transfer destination node for each edge on the data transfer graph. FIG. 20 shows an example of the adjacent node list. The information on the destination node and the source node for each edge is stored in an edge list Efinal obtained by the optimization process.

Subsequently, a node which may cause "resource conflict" or "register omission" is detected by using the adjacent node list. When detecting "resource conflict", a node having a plurality of input edges is detected. In the example shown in FIG. 20, there are two input edges at nodes L, M, N, and O, respectively, and there are four edges at node V. Therefore, these five nodes
In each case, it is considered that “resource conflict” may occur.

On the other hand, when "register omission" is detected, a node having one or more input edges and one or more output edges is detected. In the example shown in FIG. 20, at nodes L and M, two input edges and 1
There are book output edges. Therefore, these nodes are considered as having the potential for "register omission." In consideration of clock distortion, nodes (registers) that may have "register omission"
It is considered that "resource conflict" may occur.

FIG. 21 shows an example of the property of “resource conflict”. These properties are generated from the data transfer graph shown in FIG. The property of “resource conflict” is generated for each of the five nodes described above. At this time, conditions assigned to input edges existing at each node are extracted, and properties are generated by combining those conditions.

For example, when generating a property for the node L, the conditions assigned to the edge EL and the edge FL are extracted from the graph. That is, the “control signal CTRL4” is output from the edge EL and the edge FL, respectively.
And "control signal CTRL3" are extracted, and the following properties are obtained by combining them.

AG (CTRL4.CTRL3) When this property is input, the verification tool 3 verifies whether or not there is a clock cycle in which the control signal CTRL4 and the control signal CTRL3 are simultaneously generated. If there is a clock cycle in which these occur simultaneously, the verification tool 3 determines that “resource conflict” occurs in the node L. That is, it is assumed that a simultaneous write access to the register C occurs.

When there are three or more input edges at a certain node, two arbitrary input edges are extracted from them, and the condition given to the two input edges is represented by a graph. Extracted from This process is performed for all combinations. For example, node V is 4
Since there are six input edges, in this case, six combinations (edge QV and edge LV, QV and MV, QV and R
V, LV and MV, LV and RV, MV and RV). Then, a property is generated for each combination.

FIG. 22 shows an example of the property of “register omission”. These properties are also generated from the data transfer graph shown in FIG. Note that “register omission” detected in this embodiment is “write,
The sequence that should be "read, write" is "write,
It is assumed that the execution is performed in a sequence of “writing and reading”.

When focusing on the node L, the following four conditions may cause "register omission". That is, (1) When the data is transferred from the node E to the node L again without transferring the data from the node L to the node V after the data is transferred from the node E to the node L, (2) (3) When data is transferred from the node F to the node L again without the transfer from the node L to the node V after the data is transferred from the node F to the node L, When the data is transferred from the node E to the node L without being transferred from the node L to the node V after the data is transferred to (4) the data is transferred from the node E to the node L. Later, data is transferred from the node F to the node L without being transferred from the node L to the node V. Note that the properties are basically generated in the node M in the same manner. For example, in the case of (1), the property is EF (CTRL4 / ＼EX (E (（CTRL5UC)
TRL4))).

When this property is input, the verification tool 3 reads “control signal CTRL5 without generating control signal CTRL5 after the clock cycle in which control signal CTRL4 is generated.
Look for "4 clock cycles occur." Then, if such a situation exists, the verification tool 3 determines that “register omission” occurs at the node L.

FIG. 23 shows an example of the property of “resource conflict” in a register in consideration of clock distortion. These properties are also generated from the data transfer graph shown in FIG. In this case, the "resource conflict" assumes that a write access and a read access occur in a certain clock cycle.

When attention is paid to the node L, there are two conditions under which “resource conflict” may occur. That is, (1) data transfer from the node E to the node L and data transfer from the node L to the node V are performed within a moving clock cycle; and (2) data transfer from the node F to the node L. This is the case where data transfer from node L to node V is performed within the active clock cycle. Note that properties are basically generated in the node M in the same manner.

For example, the property in the case of (1) is represented as AG (CTRL4.CTRL5). When this property is input, the verification tool 3 searches for a clock cycle in which the control signal CTRL4 and the control signal CTRL5 occur simultaneously. If such a clock cycle exists, the verification tool 3 determines that “resource conflict” occurs in the node L. Second Embodiment FIGS. 24 to 26 show an example of hardware specifications 2 input to the property generation tool 1. In this example,
Verilog is used as a hardware description language.

In section 1, input control signals, input data and output data are defined.
According to the description in section 1, this module has five registers (BASES, ENDS, MODE, REG-ADR, REGA
-OUT) is provided. Section 2 contains control signals
The data transfer when the CNT-REG-ACC and the control signal WRITE are given is described. These data transfers are:
It is controlled by the value of the 5-bit control signal REG-ADR. Section 3 describes data transfer to the register REG-ADR or the output REGA-OUT when various control signals are given.

FIG. 27 is a data transfer graph generated from the hardware specifications shown in FIGS. The method of generating the data transfer graph from the hardware specifications is the same as that of the first embodiment, and the description is omitted here.

In the graph shown in FIG.
“G11” is a condition as a trigger for data transfer. FIG. 28 shows these conditions. For example, in the data transfer from the node A to the node D, according to the description in the section 2, the control signal CNT-REG-ACC and the control signal WRITE are given, and the fourth bit of the register REG-ADR is "1". It is executed in the clock cycle in which the third to zero bits of the register REG-ADR are "0001". “G1” shown in FIG. 28 describes this condition.

A set of elements included in each condition is called a “support set”. For example, the support set of condition G1 has seven elements (CNT-REG-ACC, WRITE, REG-ADR
(4), REG-ADR (3), REG-ADR (2), REG-ADR (1), REG-ADR
(0)).

In optimizing the data transfer graph, the concepts of “register file” and “name equivalence” are used. When detecting the “register file”, first, an edge whose transfer destination is a register or an edge whose transfer source is a register is extracted. Then, the support sets assigned to the edges are compared, and edges having the same edge are grouped. In this case, registers respectively connected to the plurality of grouped edges are regarded as a “register file”.

A specific example will be described with reference to FIG. Here, attention is paid to the edge AD whose transfer destination node is a register. The edge AD is given a condition G1. In this case, when detecting the register file, first,
From the fan-in edge to the node representing the register,
An edge having the same support set as the support set of G1 is extracted. The support set of the condition G1 is shown in FIG.
Are the same as the conditions G2 to G6, respectively.
Therefore, of the fan-in edge to the node representing the register, the edge for which the conditions G2 to G6 are set is extracted. Thereby, edges for which the conditions G1 to G6 are set are grouped. That is, edge A
D, AE, and AF are grouped. Therefore, the three nodes (D, E, F) to which these edges are transferred
Are considered to belong to the register file.

In the above example, the register file is detected based on the fan-in edge to the register.
As shown in FIG. 29, the same relationship can be obtained by using the fan-out edge from the register.

When detecting "name equivalence", nodes (particularly, registers and output ports) to which the same name is given are extracted from the nodes in the same module, and are regarded as equivalent resources. In the example shown in FIG. 27, since the names of the node J corresponding to the register and the node I corresponding to the output port are both "REGA-OUT", these nodes are regarded as equivalent.

After detecting the equivalence relation as described above,
Eliminate parts not related to "resource conflict" or "register omission" from the data transfer graph. That is, since the nodes D, E, and F are “register files”, these nodes are replaced with one node (node D ′). Further, the nodes J and I are “name equivalent”. Therefore, node I is eliminated. As a result of the above-described optimization processing, the data transfer graph shown in FIG.
Optimized to the state shown in

When the data transfer graph is optimized, the condition (support set) given to each edge changes accordingly. Specifically, the conditions G1 to G6 shown in FIG. 27 are consolidated into a condition G1 ′, while the conditions G7
And G8 are collected into a condition G2 '. FIG.
The support set of 1 ′ and the condition G2 ′ is shown.

In the hardware of the second embodiment, there is a possibility that “resource conflict” occurs in the node J. In this case, the property of “resource conflict” has four conditions (G
2 ′, G9, G10, G8) is a script for checking clock cycles occurring simultaneously. Also, with this hardware, there is a possibility that “register omission” may occur at the node D ′. In this case, the property of “register omission” is a script for checking that the conditions G1 ′ and G2 ′ occur in a predetermined order.

Next, the operation algorithm of the above-described property generation tool 1 will be described with reference to flowcharts. In the following description, the following definitions are used. L Module Hierarchy Level M Module Set Si Input Port Set So Output Port Set Sio Input / Output Port Set Sw Bus Wire Set Sr Register Set Sdt Data Element (Resource that Generates Result of Operation such as Substitution Expression) Sdc Data Constant (Resource for Generating Constant) Edt Data Transfer Edge N Node Set H Data Resource Equivalent Class Set FIGS. 32 to 34 are flowcharts illustrating a method for generating a data transfer graph. This process is executed when the hardware specification 2 described in the hardware description language is input.

In step S31, a memory area used to create a property is initialized. At this time,
“0” is set as the module hierarchy L. "Wb" is set as the minimum bit width parameter.

In step S32, the module list M
Register the root module in. All modules provided in the hardware specification 2 are registered in the module list M. Step S33 is a determination process for executing the processes from step S34 on for each module registered in the module list M.

In step S34, the module list M
From the module Mi. Step S35 is a process for executing steps S36 to S41 for each port described in the interface definition for the module Mi. In step S36, the port P is extracted from the interface definition. Then, it is determined whether or not the bit width of the port P is equal to or larger than the minimum bit width parameter Wb. If the bit width of the port P is equal to or larger than the minimum bit width parameter Wb, the process proceeds to step S37. If not, the process returns to step S35 to extract the next port.

In the step S37, it is checked whether or not the port P is an input port. If the port P is an input port, the port P is registered in the input port list Si in step S40. In step S38, it is checked whether the port P is an output port. If the port P is an output port, the port P is registered in the output port list So in step S41.
If the port P is neither the input port nor the output port, the port P is registered in the input / output port list Sio in step S39.

By the above processing, each port defined in the hardware specification 2 is stored in the input port list Si.
, Output port list So, or input / output port list Sio.

Step S51 is a process for executing steps S52 to S55 for each variable V described in the module declaration of the module Mi. In step S52, it is determined whether or not the bit width of the variable V is equal to or larger than the minimum bit width parameter Wb. If the bit width of the variable V is equal to or greater than the minimum bit width parameter Wb, step S5
Go to step 3, otherwise return to step S51 and extract the next variable.

In step S53, it is determined whether or not the variable V is a register variable. If the variable V is a register variable, the variable V is registered in the register variable list Sr in step S55, and if not, in step S5
In step 4, the variable V is registered in the bus wire variable list Sw.

By the above processing, each variable defined in the hardware specification 2 is stored in the register variable list Sr.
Alternatively, it is registered in the bus wire variable list Sw. Step S56 is a process for executing steps S57 and S58 for each module instantiation of the module Mi. In a step S57, the module instantiation mj is registered in the module list M. In step S58, the port of module instantiation mj is associated with the previously identified resource in module Mi.

Step S61 is a process for executing steps S62 to S72 for each simultaneous processing CP in the module Mi. In step S62, the simultaneous processing C
Check whether P is a continuous assignment type. Here, if the simultaneous processing CP is a continuous assignment type, in step S71, the processing CP
Is set to "C (Concurrent)" as the data transfer processing type. Then, in step S72, a data transfer edge is generated.

In step S63, the simultaneous processing CP is guar
Check if it is a ded continuous assignment type. In step S64, the simultaneous processing CP sets the combination
Check if it is a nalalways block type. Then, the determination result of step S63 or S64 is "Ye
If "s", in step S70, "C" is set as the data transfer processing type of the processing CP. on the other hand,
The determination results in steps S63 and S64 are both “No”
If so, in step S65, "S (Sequential)" is set as the data transfer processing type of the processing CP.

In step S66, all guard conditions are recognized. Here, each guard condition controls a different data transfer. In step S67, a guard expression and a guard signal are stored for each guard condition. At this time, the transfer source and the transfer destination of the data transfer controlled by the guard condition are recognized. Then, step S6
At 8, a data transfer edge is generated. Step S
69 indicates steps S66 to S68 for each data transfer.
Is a process for executing.

By the above processing, a data transfer edge corresponding to each data transfer defined in the hardware specification 2 is generated. FIG. 35 is a detailed flowchart of the process of generating a data transfer edge in step S68 or S72.

In step S81, it is checked whether or not the data transfer source is an assignment expression. If the transfer source is an assignment expression, a pseudo resource Sdt corresponding to the assignment expression is generated in step S82. In step S83, it is checked whether or not the data transfer source is a constant. If the transfer source is a constant, in step S84, a pseudo resource Sdc corresponding to the constant is generated.

If the transfer source of the data transfer is neither an assignment expression nor a constant, the source resource Source is recognized in step S85. In step S86, it is checked whether or not the transfer source of the data transfer belongs to the input port list Si, the input / output port list Sio, the bus wire variable list Sw or the register variable list Sr.

When the pseudo resource Sdt or the pseudo resource Sdc has been generated, or when the judgment result of step S86 is “Ye
s ", the transfer destination resource Sink is recognized in step S87. In step S88, it is checked whether or not the transfer destination of the data transfer belongs to the output port list So, the input / output port list Sio, the bus wire variable list Sw or the register variable list Sr.

If the decision result in the step S88 is "Yes", an edge E is generated in a step S89 based on the transfer source and the transfer destination of the data transfer.
In step S90, the generated edge E is added to the data transfer edge list Edt. In step S91, the edge E is associated with the transfer source and the transfer destination of the data transfer. In this embodiment, if the transfer source or the transfer destination of the data transfer is not any of the port, the register, the bus wire, and the pseudo resource, the edge E is not generated.

By the above processing, for each data transfer defined in the hardware specification 2, a data transfer edge in which the transfer source and the transfer destination of the data transfer are defined is generated.

FIG. 36 and FIG. 37 are flowcharts of a process for detecting “non-fragment equivalent”. This flowchart is an example of step S11 of the flowchart shown in FIG. Here, the input / output ports will be described, but the same processing is executed for the input ports and the output ports.

In step S101, the input / output port list Sio is scanned. Step S102 is processing for executing the processing of step S103 and thereafter for each element (input / output port) belonging to the input / output port list Sio. In step S103, the element Sio-k is extracted from the input / output port list Sio.

In step S104, the extracted element Sio
Add -k to queue Q. In step S105, it is checked whether the queue Q is empty. If the queue Q is empty, the process returns to step S102, and if one or more elements are held in the queue Q, the element q is extracted from the queue Q in step S106.

In the step S107, it is checked whether or not the element q has a “child resource”. Here, the “child resource” of the element q is, for example, a resource provided in a module in a lower hierarchy of the module in which the element q is provided, and is associated with the element q. A thing. The correspondence is described in hardware specifications or the like.

If the element q does not have “child resource”, the process returns to step S102 after deleting the element q from the queue Q in step S114. If the element q has “child resource”, Proceed to step S108.
In step S108, a non-fragment equivalent class Hek corresponding to the element Sio-k is generated. And step S
At 109, the Eqvl flag is reset.

Step S110 is a process for executing steps S121 to S126 for each "child resource" of the element q. In step S121, “child resource qc” is extracted from element q. In step S122, it is checked whether or not the bit width of the element q is the same as the bit width of the “child resource qc”. If the bit widths are different from each other, the process returns to step S110 to extract the next “child resource”. If the above bit widths are the same,
In step S123, "1" is set to the Eqvl flag. In step S124, "child resource qc" is added as an element of queue Q. In step S125,
“Child resource qc” is added as an element of the non-fragment equivalence class Hek. In step S126, the non-fragment equivalence class Hek is associated with the “child resource qc”.

Step S1 for all “child resources”
When the processes of S21 to S126 are performed, step S11 is performed.
At 1, it is checked whether the Eqvl flag is "1". E
If the qvl flag is "1", the element q is added to the non-fragment equivalence class Hek in step S112, and the non-fragment equivalence class Hek is associated with the element q in step S113. If the Eqvl flag is not “1”, the processing of steps S112 and S113 is skipped.

As described above, when the bit width of a certain port is the same as the bit width of the “child resource” of the port, the port and the “child resource” are regarded as “non-fragment equivalent”.

FIGS. 38 to 41 show “fragment equivalent”.
6 is a flowchart of a process for detecting the. This flowchart corresponds to step S1 of the flowchart shown in FIG.
2 is an embodiment of FIG. Here, the input / output ports will be described, but the same processing is executed for the input ports and the output ports.

In the step S131, the input / output port list Sio is scanned. Step S132 is processing for executing step S133 and subsequent steps for each element (input / output port) belonging to the input / output port list Sio.
In step S133, the element Sio-1 is extracted from the input / output port list Sio.

In step S134, it is determined whether or not the element Sio-1 belongs to any of the equivalence classes Hek. If the element Sio-l belongs to one of the equivalence classes Hek, the process proceeds to step S135. Otherwise, the process returns to step S132 after executing the processes of steps S141 to S146.

In the step S141, it is checked whether or not the element Sio-1 has a "child resource". If the element Sio-l has "child resource", the processing after step S142 is executed; otherwise, the processing returns to step S132.
In step S142, a fragment equivalent class OIFHel corresponding to the element Sio-1 is generated. Step S14
In element 3, the element Sio-l is set as the root (starting point)
Recognize "child resources" that have a bit width smaller than the bit width of io-l. In step S144, “fragment equivalence class OIFHel” is set in the fragment equivalence field for each “child resource”. Step S1
At 45, "Non-fragment equivalence class Hek" is set in the non-fragment equivalence field for each "child resource". In step S146, each “child resource” is added as an element of the fragment equivalence class OIFHel.

If the element Sio-1 belongs to any of the equivalence classes Hek, the fragment child-found flag is reset in step S135. Step S
At 136, with the element Sio-l as the root, a "child resource" having a bit width smaller than the bit width of the element Sio-l or a "child resource" having a bit width larger than the bit width of the element Sio-l Search for At this time, a set of extracted “fragment children” is set to “F-child”. On the other hand, a set of “non-fragment child resources” having a larger bit width is referred to as “UG-child”.

In the step S137, it is checked whether or not the element of the set F-child exists. If there is an element of the set F-child, a fragment child-found flag is set in step S138. Step S13
In step 9, the fragment equivalent class OIFHel corresponding to the element Sio-1 is generated.

In step S151, the set F-child is scanned. Step S152 is processing for executing steps S153 to S156 for each element belonging to the set F-child. In step S153, the set F-ch
Extract element Cd-i from ild. In step S154, "parent resource P-Cd-i" of element Cd-i is extracted. In step S155, the element Cd-i and the parent resource P-Cd-
Set "fragment equivalence class OIFHel" in the fragment equivalence field for i. Step S15
In element 6, element Cd-i is assigned to fragment equivalent class OIFH.
Add to el.

If the elements of the set F-child do not exist,
Steps S161 to S172 are performed. The processing of steps S161 to S165 is basically the same as the processing of steps S137 and S151 to S154. However, in steps S161 to S165, the element Cd-i is extracted from the set UG-child, and
The “parent resource Prnt-i” is extracted.

In the step S166, a fragment equivalent class OIFHel corresponding to the element Cd-i is generated. Step S167 is processing for executing steps S168 to S172 for each element of “parent resource Prnt-i”. In step S168, the element Pi-k belonging to "parent resource Prnt-i" is extracted. In step S169, the non-fragment equivalence class Hek to which the element Pi-k belongs is searched. In step S170, each element of the non-fragment equivalence class Hek is added to the fragment equivalence class OIFHel. In step S171, “fragment equivalent class OIFHel” is set in the fragment equivalent field for each element of the non-fragment equivalent class Hek. Then, in step S172, the non-fragment equivalence class Hek is deleted from the non-fragment equivalence field for each element.

FIG. 42 is a flowchart of a process for detecting “name equivalence”. This flowchart is an example of step S13 of the flowchart shown in FIG. In step S181, the register list Sr is scanned. Step S182 is a process for executing the processes of steps S183 to S189 for each element of the register list Sr. In step S183, an element (register) Sr-1 is extracted from the register list Sr.

In steps S184 to S186, the name of the extracted element Sr-1 is compared with the name of each element of the output port list So. If an element So-j having the same name as the element Sr-l exists in the output port list So, in step S187, the non-fragment equivalence class Hek to which the element So-j belongs is determined. look for. In step S188, "non-fragment equivalent class Hek" is set in the non-fragment equivalent class field for element Sr-1. Then, in step S189, the element Sr-1 is added as an element of the non-fragment equivalence class Hek.

By the above processing, a register and an output port having the same name as the register are regarded as “name equivalent”. FIG. 43 is a flowchart of processing for detecting a “fragment edge”. In this process, information useful for determining whether each data transfer edge belongs to a “fragment edge” or a “non-fragment edge” is generated. This flowchart is an example of step S14 of the flowchart shown in FIG.

In the step S191, the data transfer edge list Edt is scanned. Step S192 is a step S1 for each element of the data transfer edge list Edt.
This is a process for executing steps S93 to S200. In step S193, the element (edge) Ej is extracted from the data transfer edge list Edt. At this time, the transfer source and the transfer destination of the data transfer corresponding to the edge Ej are recognized.

In step S194, it is checked whether the transfer destination of the data transfer corresponding to the edge Ej is "fragment equivalent". If the transfer destination is “fragment equivalent”, the edge Ej is determined in step S195.
The transfer source of the data transfer corresponding to "Fragment equivalent"
Check if it is. If both the transfer destination and the transfer source are “fragment equivalent”, both fragment flags are set in step S196. If only the transfer destination is “fragment equivalent”, the transfer is performed in step S197. Set the destination fragment flag. On the other hand, the transfer destination is "fragment equivalent"
If not, it is checked in step S198 whether the transfer source of the data transfer corresponding to the edge Ej is "fragment equivalent". Then, if only the transfer source is “fragment equivalent”, step S1
At 99, set the source fragment flag,
If neither the transfer destination nor the transfer source is “fragment equivalent”, a non-fragment flag is set in step S200.

By the above processing, edges corresponding to each data transfer are classified into both fragment edges, transfer destination fragment edges, transfer source fragment edges, and non-fragment edges.

FIGS. 44 to 48 are flowcharts of the processing for detecting the "equivalent edge". This flowchart is an example of step S15 of the flowchart shown in FIG.

In step S211, the data transfer edge list Edt is scanned. In step S212, each element of the data transfer edge list Edt is scanned in step S2.
This is a process for executing the processes after the thirteenth. In step S213, an element (edge) Ej is extracted from the data transfer edge list Edt. At this time, the transfer source and the transfer destination of the data transfer corresponding to the edge Ej are recognized.

In step S214, it is checked whether or not the edge Ej is a source fragment. If the edge Ej is the transfer source fragment, the process proceeds to step S215; otherwise, the process proceeds to step S241. In step S215, the fragment equivalent of the transfer source is set to “FHej”. In step S216, elements belonging to the fragment equivalent FHej are scanned. Step S217 is performed for each element belonging to the fragment equivalent FHej.
To S224.

In step S218, an element (port or the like) Ni is extracted from the fragment equivalent FHej. In step S219, all edges that include the element Ni as a source node or a destination node are extracted. Step S
At 220, the list of extracted edges is scanned.
Step S221 is processing for executing steps S222 to S224 for each edge extracted in step S219. In step S222, an element (edge) Ek is extracted from the extracted list of edges. At this time, the transfer destination node of the data transfer corresponding to the edge Ek is "Head-k". In step S223, it is checked whether or not the transfer destination node Head-k is the same as the transfer destination extracted in step S213. If they are the same, in step S224, the edge Ej
Is added to the set Eqv-Tail-Ej of the equivalent edges of.

When the processing of steps S218 to S224 is executed for all elements belonging to the fragment equivalent FHej, in step S231, the set Eqv-Tail-Ej
The interval graph IG is created based on the bit width vector of the node of the edge belonging to.

Here, referring to FIGS. 49 to 51,
The interval graph will be described. Here, FIG.
It is assumed that the data transfer graph shown in FIG. 9 has been generated. The data transfer between the nodes shown in FIG.
0 is defined. Then, it is assumed that a control signal corresponding to the guard condition, a bit used in the transfer destination node, and a bit to be bit in the transfer destination node are defined for each edge. According to this definition, for example, the edge RT indicates that the 7th to 0th bits of the node R are transferred to the 7th to 0th bits of the node T when the control signal G3 is given. Each data transfer is represented by using T1 to T10.

When an interval graph is created from a data transfer graph, each data transfer is first represented by a dot (dot). Then, for each data transfer, data transfer in which bits to be used in the transfer destination node overlap are extracted and connected.

For example, attention is paid to the data transfer T1. Data from the data transfer T1 is written to the 7th to 0th bits of the node T. At this time, the data from the data transfer T2 is written to the 3rd to 0th bits of the node T. Therefore, the data transferred by the data transfer T1 and the data transfer T2 overlap at the node T. Similarly, data transfer T3, T8, T9 and T
The data at 10 also overlaps at node T with the data at data transfer T1. In this case, the point representing the data transfer T1 is, as shown in FIG.
, T3, T8, T9 and T10.

Thereafter, the same method is applied to other data transfer, whereby an interval graph shown in FIG. 51 is obtained. Return to the description of the flowchart. In step S232, in the interval graph IG,
The connection between the parts ("points" in FIG. 51) is checked. In step S233, a set NSCC of non-single parts is extracted. Each set NSCC is composed of a plurality of data transfers corresponding to points connected to each other in a mesh in the interval graph. For example, in FIG. 51, points T1, T2, T3, and T10 are connected to each other in a mesh shape, and the data transfer corresponding to each of these points belongs to one set NSCC. In step S234,
A set SCC of single components is extracted. The data transfer that does not belong to any of the sets NSCC belongs to the set SCC.

In step S235, an independent subset Ind-Eqv-Tail-Ej is created from edges belonging to each set NSCC and included in the set Eqv-Tail-Ej. Step S2
36, the independent subset Ind-E is obtained from the set Eqv-Tail-Ej.
Delete qv-Tail-Ej. In step S237, the set N
The set Eqv-Tail-Ej is divided into one or more subgroups based on the SCC. Then, in step S238, an edge list Efinal is obtained for each subgroup. Then, in step S239, the set Eqv-Tail-Ej of each subgroup is added to the edge list Efinal.

If the edge Ej is not a source fragment (S214: No), it is checked in step S241 whether the edge Ej is a destination fragment or both fragments. If the edge Ej is a transfer destination fragment or both fragments, step S24
If not, in step S249, the edge Ej is set as a single block in the edge list E
After adding to final, the process returns to step S212.

In step S242, the parent resource field of the data transfer destination corresponding to the edge Ej is traversed until a non-fragment parent resource UF-Parent-j is found. In step S243, the parent resource UF-Parent-j
Let the non-fragment equivalence class to which "" belongs be "UHPej". In step S244, the non-fragment equivalence class UHPej is scanned. Step S245 is processing for executing steps S246 to S248 for each element belonging to the non-fragment equivalence class UHPej. In step S246, the element (node) Ni is extracted from the non-fragment equivalence class UHPej. In step S247, all edges including the node Ni as a destination node are extracted. In step S248, each extracted edge is added to a set of equivalent edges Eqv-Head-Ej.

In step S251, it is checked whether or not the node Ni extracted from the non-fragment equivalent class UHPej is fragment equivalent. If the node Ni is equivalent to a fragment, the process proceeds to step S252; otherwise, the process returns to step S245. In step S252, the fragment equivalence class of the node Ni is set to "FHej". In step S253, the fragment equivalent class FHej is scanned. Step S254 is performed for each element belonging to the fragment equivalence class FHej.
To S257. Step S2
In 55, the node N is transmitted from the fragment equivalence class FHej.
Extract k. In step S256, all edges including the node Nk as a transfer destination node are detected. Then, in step S257, each extracted edge is added to the set E-Head-Ej of equivalent edges.

Steps S246 to S2 for each node
After executing step S48 (step S245: Yes), steps S261 to S268 are subsequently executed. Step S
Steps S231 to S268 are basically performed in steps S231 to S231.
237 and S239. However, in steps S261 to S268, an interval graph IG relating to edges belonging to the set Eqv-Head-Ej is created, and an edge list Efinal is obtained using the graph.

FIGS. 52 to 55 show a "register file".
6 is a flowchart of a process for detecting the. This flowchart corresponds to step S1 of the flowchart shown in FIG.
6 is an embodiment of FIG.

In the step S271, the data transfer edge list Edt is scanned. Step S272 is processing for executing steps S273 to S284 for each element belonging to the data transfer edge list Edt. In step S273, the element (edge) Ej is extracted from the data transfer edge list Edt. Further, the transfer source Source and the transfer destination Sink of the data transfer corresponding to the edge Ej are detected.

In the step S274, it is checked whether or not the transfer source or the transfer destination of the edge Ej is a register. If the transfer source or the transfer destination is a register, step S275
Otherwise, the process returns to step S272. In step S275, a set SSS-Ej of control signals constituting a support set of the guard expression of the edge Ej is created. In step S276, it is determined whether the detected transfer destination is a register. If the transfer destination is a register, the process proceeds to step S277; otherwise, the process proceeds to step S2.
77 to 280 are skipped.

In step S277, a set S of control signals
Associate SS-Ej with the transfer destination. In step S278, a set Sink-Support-Set of control signals included in the guard expression of the data transfer whose transfer destination is the register is obtained. In step S279, the control signal set SSS-Ej is associated with the control signal set Sink-Support-Set. Step S
In 280, the transfer destination is set to a set of transfer destination registers Sink-Regis
Add to tors.

In step S281, it is checked whether or not the detected transfer source is a register. If the transfer source is a register, the process proceeds to step S282; otherwise, the process returns to step S272. In step S282, the control signal set SSS-Ej is associated with the transfer source. Step S
At 283, the control signal set SSS-Ej is associated with the control signal set Source-Support-Set. Then, in step S284, the transfer source is set to the set So of the transfer source registers.
Add to urce-Registors.

Step S273 for all edges
When the processing of S284 is performed, in step S291, the combination U-So of the set of control signals Source-Support-Set
Create urce-Sets. Also, in step S292, the union U-Sink-S of the set of control signals Sink-Support-Set
Create ets. In step S293, the conjugate U-Sour
Create a random total order To-U-Source-Sets composed of unique elements belonging to ce-Sets. Also,
In step S294, a random total order To composed of unique elements belonging to the combination U-Sink-Sets To
-Create U-Sink-Sets.

In step S295, Sink-Support-Set
To scan. Step S296 is Sink-Support-S
Step S297-for all sets belonging to et
This is processing for executing S300. Step S29
In step 7, SSS-Ej is extracted from the Sink-Support-Set. In step S298, based on the To-U-Sink-Sets, the bit vector representation BV-SSS-Ej of SSS-Ej
Create Here, "1" is set in the entry corresponding to the element of SSS-Ej, and "0" is set in the other elements. In step S299, BV-SSS-Ej is set to SS
S-Ej. Then, in step S300, BV-SSS-Ej is added to SSS-Ej.
At this time, BV-Sink-Support-Sets becomes Sink-Support-S
A set of bit vector representations of et.

Step S297 for all sets
After performing the processing of steps S300 to S300, the process proceeds to step S311. Step S311 is processing for executing steps S312 to S315 for all sets belonging to the Source-Support-Set. Steps S312 to S315
Are basically the same as steps S297 to S300 described above.

In step S316, BV-Sink-Suppor
Scan the t-Set vector list. Step S3
17 is a process for executing steps S318 to S324 for each vector belonging to the vector list. In step S318, BV-
Extract SSS-Ej. In step S319, the BV
-Rescan the vector list in Sink-Support-Set. Step S320 is processing for executing steps S321 to S323 for each vector belonging to the vector list. In step S321, BV-SSS-Ek is extracted from the vector list. Step S3
At 22, it is checked whether BV-SSS-Ej and BV-SSS-Ek are the same. If they are the same, a transfer destination register Reg-sink-k corresponding to BV-SSS-Ek is detected in step S323. Then, steps S321 to S3 are performed for all the vectors.
After executing the process of step S23, in step S324,
The transfer destination register Reg-sink-k is added to the transfer destination register file set Sink-Reg-Files.

Steps S331 to S339 are basically the same as the processing of steps S316 to S324. However, in steps S331 to S339, BV-Sink-Supp
Processing is performed for each element belonging to the vector list of ort-Set, and a predetermined transfer source register is added to the source register file set Source-Reg-Files.

In step S341, a list of a set Sink-Reg-Files of transfer destination register files is scanned.
Step S342 corresponds to processing for executing steps S343 to S348 for each set belonging to the list. In step S343, a set Sink-Reg-File-k is extracted from the above list. In step S345, it is determined whether all sets have been processed. If there is an unprocessed set, in step S346, the set So
Extract urce-Reg-File-l. In step S347,
Check whether the set Sink-Reg-File-k is the same as the set Source-Reg-File-l. If they are the same, in step S348, the set Source-Reg
Add -File-k to the set Reg-Files. Through the above processing, registers belonging to the register file are obtained.

As described above, the data transfer graph generated by the processing in the flowcharts shown in FIGS.
It is optimized by the processing of the above-described flowchart. The result of the optimization is an edge list Efinal.

FIG. 57 is a flowchart of a process for creating an adjacent node list from the optimized data transfer graph. This flowchart is an example of step S21 in the flowchart shown in FIG.

In the step S351, the edge list Efi
Scan nal. Step S352 is a step S352 for each subgroup belonging to the edge list Efinal.
This corresponds to processing for executing steps 353 to S361. In step S353, the subgroup Pi is extracted from the edge list Efinal.

Step S354 corresponds to processing for executing the processing of steps S355 to S361 for each edge belonging to the subgroup Pi. Step S35
In step 5, the edge Ej is extracted from the subgroup Pi.
At this time, the equivalent class Head-Hej and the equivalent class Tail-Hej corresponding to the non-fragment equivalent class to which the transfer destination node and the transfer source node of the edge Ej belong are extracted. In step S356, it is checked whether or not the non-fragment equivalence class Head-Hej is an element of the node set N in the adjacent node list. If the non-fragment equivalent class Head-Hej is not an element of the node set N, it is added to the node set N in step S357. Similarly, in step S358, it is checked whether the non-fragment equivalence class Tail-Hej is an element of the node set N. And the non-fragment equivalence class Tail
If -Hej is not an element of the node set N, it is added to the node set N in step S359.

In step S360, the non-fragment equivalent class He in the node set N of the adjacent node list
Non-fragment equivalence class Tail-H in ad-Hej adjacency list
Add ej. Also, the non-fragment equivalence class Head-H
Increment the number of input edges of ej. On the other hand, in step S361, the non-fragment equivalence class Head-Hej is added to the adjacent list of the non-fragment equivalence class Tail-Hej in the node set N. Then, the number of input edges of the non-fragment equivalent class Tail-Hej is incremented.

FIGS. 58 to 60 are flowcharts of processing for generating a property script to be input to the verification tool. This flowchart is an example of step S22 of the flowchart shown in FIG.

In the step S371, the node set N in the adjacent node list is scanned. Step S372
Is a process for executing the processes from step S373 on for each node belonging to the node set N. In step S373, the node Nj is extracted from the node set.

In the step S374, it is checked whether or not the number of fan-in edges of the node Nj is one or more. If the number of fan-in edges is one or more, the process proceeds to step S375; otherwise, the process returns to step S372. In step S375, a set Di-Arcs of edges where the transfer destination node is the node Nj (fan-in edge to the node Nj)
-into-Nj. In step S376, it is checked whether the number of fan-out edges of the node Nj is 1 or more.
If the number of output edges is one or more, the process proceeds to step S377; otherwise, step S377 is skipped.

In step S377, a set Di-Arcs-out-of-Nj of edges whose transfer source nodes are the nodes Nj (fan-out edges from the nodes Nj) is obtained. Step S
At 378, it is checked whether the node Nj is a register. If the node Nj is a register, the process proceeds to step S379; otherwise, the process proceeds to step S411. In step S379, it is checked whether there is a fan-in edge belonging to the set Di-Arcs-into-Nj. Set Di-Arcs
If there are fan-in edges belonging to -into-Nj, in step S380, a resource conflict property between the fan-in edges is generated. Otherwise, the process returns to step S372.

In the step S381, the set Di-Arcs-out
Check whether a fan-out edge belonging to -of-Nj exists. If there is a fan-out edge belonging to the set Di-Arcs-out-of-Nj, in step S380,
A product PS1 of the set Di-Arcs-into-Nj and the set Di-Arcs-out-of-Nj is generated. PS1 is represented as "Em, En". Note that "Em" and "En" are each a set Di-Arcs-i
nto-Nj and the elements of the set Di-Arcs-out-of-Nj. On the other hand, when there is no fan-out edge belonging to the set Di-Arcs-out-of-Nj, the process returns to step S372.

In step S391, PS1 is scanned. Step S392 corresponds to processing for executing the processing of steps S393 to S395 for each element of PS1. In step S393, the element P
Sk (Ea, Eb) is extracted. In step S394, it is checked whether or not the processing type of the element Eb of the set Di-Arcs-out-of-Nj is sequential transfer. If the processing type is sequential transfer, a resource conflict property for checking an error due to clock distortion is generated in step S395.

In the step S396, the set Di-Arcs-int
A product PS2 of o-Nj and the set Di-Arcs-into-Nj is generated.
Subsequently, in step S397, when the guard expression of the edge Ej is "Gi", the logical expression No-Rea is applied to each fan-out edge Ei belonging to the set Di-Arcs-out-of-Nj.
Generate d =-(OR (Gi)). In step S398, PS
Scan 2. Step S399 corresponds to processing for executing processing 400 and S401 for each element belonging to PS2.

In step S400, PS2 is converted to PS2.
-k = (Ec, Ed) is extracted. Then, step S4
01, the register leak property EF (Gl "EX (E (No-
ReadUGm))) is generated.

If the node Nj is not a register (step S378: No), it is checked in step S411 whether the node Nj is an output port. If the node Nj is an output port, step S41
In step 2, it is checked whether or not an element exists in the set Di-Arcs-into-Nj. That is, it is determined whether a fan-in edge to the output port exists. If there is a fan-in edge, in step S413, resource conflict properties are generated for all combinations of the edges.

In the step S414, it is checked whether or not the node Nj is an input port. If the node Nj is an input port, in step S415, the set Di-Arcs-int
Union-Arcs-o, a union of o-Nj and the set Di-Arcs-into-Nj
Generate f-Nj. Then, in step S416,
A product PS3 of Union-Arcs-of-Nj and Union-Arcs-of-Nj is generated.

In step S417, PS3 is scanned. Step S418 corresponds to processing for executing the processing of steps S419 to S421 for each element belonging to PS3. In step S419, PS3-k = (Ee, Eg) is extracted from PS3. Step S42
At 0, it is checked whether the edge Ee and the edge Eg are the same. If the edges are the same, a resource conflict property is generated in step S421.

The function of generating the above-described properties is realized by executing a program describing the processing shown in the above-described flowchart using a computer. FIG. 61 shows a block diagram of a computer 100 that executes the program.

The CPU 101 loads a program describing the processing shown in the flowchart from the storage device 102 into the memory 103 and executes it. Storage device 102
Is, for example, a hard disk and stores the above program. On the other hand, the memory 103 is, for example, a semiconductor memory and is used as a work area of the CPU 101.

The recording medium driver 104 is the CPU 101
The portable recording medium 105 is accessed according to the instruction.
The portable recording medium 105 is, for example, a semiconductor device (P
C media, etc.), media for inputting / outputting information by magnetic action (floppy disk, magnetic tape, etc.), and media for inputting / outputting information by optical action (optical disc, etc.). The communication control device 106 transmits and receives data to and from a network according to an instruction from the CPU 101.

FIG. 23 is a diagram for explaining a method of providing a software program or the like according to the present invention. The program according to the present invention is provided, for example, by any of the following three methods.

(A) Installed and provided in the computer 100. In this case, the program or the like is pre-installed before shipment, for example. (b) Provided by being stored in a portable recording medium. In this case, the programs and the like stored in the portable recording medium 105 are basically installed in the storage device 102 via the recording medium driver 104.

(C) Provided from a server on the network. In this case, basically, the computer 100 obtains the program and the like by downloading the program and the like stored in the server. The network includes a wireless network.

In the above embodiment, resource contention and register omission are taken as properties to be verified, but the properties generated by the present invention are not limited to these.

Although the registers, ports, and buses are used as data resources, the resources to which the present invention is applied are not limited to these.

[0203]

According to the present invention, it is possible to automatically generate a property for verifying whether or not resource contention or register omission occurs in hardware from a specification described in a hardware description language. Therefore, a hardware design error can be corrected at an early stage, and time and cost for developing an IC or the like can be saved. In addition, the number of debugging operations is reduced, so that the designer can dedicate extra labor to other operations.

[Brief description of the drawings]

FIG. 1 is a diagram illustrating an environment in which a property creation tool according to an embodiment of the present invention is used.

FIG. 2 is a flowchart illustrating an operation of a property generation tool.

FIG. 3 is an example of a data transfer graph.

FIG. 4 is a flowchart of an optimization process.

FIG. 5 is an example of hardware.

FIG. 6 is a diagram for explaining a hierarchical method for describing the hardware shown in FIG. 5;

FIG. 7 is a diagram illustrating an example of optimizing a data transfer graph using “equivalent of resources”.

FIG. 8 is a diagram illustrating “branch”.

FIG. 9 is a diagram illustrating a register file.

FIG. 10 is an example (part 1) of hardware specifications described in Verilog.

FIG. 11 is an example (part 2) of hardware specifications described in Verilog.

FIG. 12 is an example (part 3) of hardware specifications described in Verilog.

FIG. 13 is an example (part 4) of hardware specifications described in Verilog.

FIG. 14 is an example (part 5) of hardware specifications described in Verilog.

FIG. 15 is an example (part 6) of hardware specifications described in Verilog.

FIG. 16 is a data transfer graph generated from the hardware specifications shown in FIGS. 10 to 15;

FIG. 17 is a diagram illustrating a pseudo resource.

FIG. 18 is an example of an optimized data transfer graph.

FIG. 19 is a flowchart of a property creation process.

FIG. 20 is an example of an adjacent node list.

FIG. 21 is an example of a property of “resource conflict”.

FIG. 22 is an example of a property of “register omission”.

FIG. 23 is an example of a property of “resource conflict” when clock distortion is considered.

FIG. 24 is an example (part 1) of hardware specifications described in Verilog.

FIG. 25 is an example (part 2) of hardware specifications described in Verilog.

FIG. 26 is an example (No. 3) of hardware specifications described in Verilog.

FIG. 27 is a data transfer graph generated from the hardware specifications shown in FIGS.

FIG. 28 is a diagram showing data transfer conditions in the graph shown in FIG. 27;

FIG. 29 is a diagram illustrating a process of detecting a register file.

FIG. 30 is an example of an optimized data transfer graph.

FIG. 31 is a diagram showing conditions used in an optimized graph.

FIG. 32 is a flowchart (part 1) of a method for generating a data transfer graph.

FIG. 33 is a flowchart (part 2) of a method for generating a data transfer graph.

FIG. 34 is a flowchart (part 3) of a method for generating a data transfer graph.

FIG. 35 is a detailed flowchart of a process for generating a data transfer edge.

FIG. 36 is a flowchart (part 1) of a process for detecting “non-fragment equivalent”;

FIG. 37 is a flowchart (part 2) of a process for detecting “non-fragment equivalent”;

FIG. 38 is a flowchart (part 1) of a process for detecting “fragment equivalence”;

FIG. 39 is a flowchart (part 2) of a process for detecting “fragment equivalence”;

FIG. 40 is a flowchart (part 3) of a process for detecting “fragment equivalence”;

FIG. 41 is a flowchart (part 4) of a process for detecting “fragment equivalent”;

FIG. 42 is a flowchart of a process for detecting “name equivalence”.

FIG. 43 is a flowchart of a process for detecting a “branch edge”.

FIG. 44 is a flowchart (part 1) of a process for detecting an “equivalent edge”.

FIG. 45 is a flowchart (part 2) of a process for detecting an “equivalent edge”;

FIG. 46 is a flowchart (part 3) of a process of detecting an “equivalent edge”.

FIG. 47 is a flowchart (part 4) of a process of detecting an “equivalent edge”;

FIG. 48 is a flowchart (part 5) of a process for detecting an “equivalent edge”;

FIG. 49 is an example of a data transfer graph.

FIG. 50 is a definition of data transfer.

FIG. 51 is an example of an interval graph.

FIG. 52 is a flowchart (part 1) of a process for detecting a “register file”.

FIG. 53 is a flowchart (part 2) of a process for detecting a “register file”;

FIG. 54 is a flowchart (part 3) of a process for detecting a “register file”;

FIG. 55 is a flowchart (part 4) of a process for detecting a “register file”;

FIG. 56 is a flowchart (part 5) of a process for detecting a “register file”.

FIG. 57 is a flowchart of processing for creating an adjacent node list.

FIG. 58 is a flowchart (part 1) of a process for generating a property script.

FIG. 59 is a flowchart (part 2) of a process for generating a property script.

FIG. 60 is a flowchart (part 3) of a process for generating a property script.

FIG. 61 is a block diagram of a computer that executes a program describing the functions of the present invention.

FIG. 62 is a diagram illustrating a method of providing a software program and the like according to the present invention.

[Explanation of symbols]

 1 Property generation tool 2 Hardware specifications 3 Verification tool

──────────────────────────────────────────────────の Continued on the front page (51) Int.Cl. ⁷ Identification symbol FI Theme coat ゛ (Reference) H01L 27/04 U (72) Inventor Tsuneo Nakata 4-1-1, Kamiodanaka, Nakahara-ku, Kawasaki City, Kanagawa Prefecture Fujitsu F term (reference) 5B046 AA08 DA04 DA06 JA01 5F038 CA03 CA17 CD05 DF11 EZ10 EZ20 5F064 BB09 BB18 DD03 DD04 DD25 HH06 HH09 HH10 HH14

Claims (17)

[Claims] 1. A device for generating a plurality of resources described in a hardware description language and properties to be verified for hardware including data transfer using the resources, the device being described in the hardware description language. Generating means for generating a data transfer graph corresponding to resources and data transfer, optimizing means for optimizing the data transfer graph generated by the graph generating means, and data transfer optimized by the optimizing means A property generating unit configured to generate a property to be verified for the hardware described in the hardware description language by using a graph; 2. The property generating device according to claim 1, wherein said optimizing means minimizes a data transfer graph based on a topology of the graph. 3. The property generating apparatus according to claim 1, wherein the graph generating means uses the nodes respectively corresponding to the resources, and edges indicating a transfer source and a transfer destination of each data transfer. Generate a data transfer graph representing the ware. 4. The property generating apparatus according to claim 3, wherein said optimizing means has the same bit width of each resource corresponding to two nodes adjacent to each other, and one of the resources is the other. , Delete one of those nodes from the data transfer graph. 5. The property generating apparatus according to claim 3, wherein said optimizing means transfers data from the first resource to the second resource and the third resource, and transfers the data to the second and third resources. If the bit width of the resource is smaller than the bit width of the first resource, the node corresponding to the first resource is deleted from the data transfer graph. 6. The property generating apparatus according to claim 3, wherein said optimizing means transfers data from a first resource and a second resource to a third resource, and said first and second resources. If the bit width of the third resource is smaller than the bit width of the third resource, the node corresponding to the third resource is deleted from the data transfer graph. 7. The property generating apparatus according to claim 3, wherein the optimizing means outputs the data when the data is transferred from a register to an output port to which the same name as the name of the register is assigned. The node corresponding to the port is deleted from the data transfer graph. 8. The property generating apparatus according to claim 3, wherein the optimizing means is configured to transfer data transmitted from the first resource to only the second resource, and to determine whether the second resource is transmitted to the second resource. When receiving only data transferred from the first resource, an edge representing a data transfer from the first resource to the second resource is deleted from the data transfer graph. 9. The property generating apparatus according to claim 3, wherein said optimizing means transfers data from the first resource to the second resource and transfers data from the first resource to the third resource. If the bits to be transferred do not overlap, the edges corresponding to the two data transfers are deleted from the data transfer graph. 10. The property generating apparatus according to claim 3, wherein said optimizing means transfers data from a first resource to a second resource and transfers data from a third resource to a second resource. If the bits to be transferred do not overlap, edges corresponding to the two data transfers are deleted from the data transfer graph. 11. The property generating device according to claim 3, wherein, when the plurality of registers belong to the same register file, the optimizing unit sets the plurality of nodes corresponding to the plurality of registers to one node. Convert to 12. The property generation device according to claim 1, wherein the property generation unit generates a property related to at least one of resource conflict and register omission. 13. The property generating device according to claim 1, wherein, when a plurality of fan-in edges are connected to a certain node, the property generating unit performs data transfer corresponding to the plurality of fan-in edges. A resource conflict property is generated based on the conditions given respectively. 14. The property generating device according to claim 1, wherein the property generating unit is configured to connect a fan-in edge and a fan-out edge to a certain node.
A register leakage property is generated based on conditions given for data transfer corresponding to those edges. 15. An apparatus for generating a plurality of resources described in a hardware description language and properties to be verified for hardware including data transfer using the resources, the apparatus being described in the hardware description language. Graph generation means for generating a data transfer graph corresponding to the resources and data transfer, and a property to be verified for the hardware described in the hardware description language using the topology of the data transfer graph. Property generation means, comprising: 16. A method of generating a property to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources, the method being described in the hardware description language. Generates a data transfer graph corresponding to the resources and data transferred, optimizes the data transfer graph, and verifies the hardware described in the above hardware description language using the optimized data transfer graph A property generation method that generates the properties that should be. 17. A recording medium storing a program for generating a property to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using those resources, wherein: Means for generating a data transfer graph corresponding to the resources and data transfer described in the hardware description language when the program is executed by a computer; means for optimizing the data transfer graph; A means for generating a property to be verified for hardware described in the hardware description language using the data transfer graph.