JP3943299B2 - Apparatus and method for generating properties to be verified for hardware - Google Patents

Description

[0001]
BACKGROUND OF THE INVENTION
The present invention relates to an apparatus and a method for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources.
[0002]
[Prior art]
In recent years, the design of semiconductor chips has become very complex. In other words, very complicated hardware (logic device) has been mounted on a semiconductor chip. For this reason, the design of a semiconductor chip is often performed by a collaborative work by a plurality of designers.
[0003]
However, design information subdivided by a plurality of designers may be misinterpreted by each designer. In this case, an error (design error) in a certain part may cause the entire system to not operate correctly at the register transfer level. And if there is such an error, a great amount of money and time are wasted on debugging work.
[0004]
By the way, resources (for example, a register, a bus, an input port, and an output port) 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 contention” and “register leakage”. Resource contention is an error in which one resource (such as a register) is simultaneously accessed by multiple resources. On the other hand, the register leakage is an error related to the access order when a certain register is accessed by a plurality of resources.
[0006]
A huge number of resources are formed on a semiconductor chip on which complex hardware is mounted. For this reason, it is virtually impossible to manually detect all the errors (resource conflict, register leakage, etc.) as described above. However, if there is only one error in the designed hardware, the entire system may not operate correctly. Therefore, it is very important to find and remove all resource conflicts and register leaks.
[0007]
[Problems to be solved by the invention]
Many designers recognize the importance of finding resource conflicts and register leaks early in the design process. However, until now, the task of finding resource conflicts and register omissions has only been performed by each designer for each subsystem that the designer is responsible for.
[0008]
In order to guarantee the operation of the entire system, it is not sufficient to perform verification for each subsystem. It is necessary to search for resource conflicts and register leaks throughout the designed hardware and remove them. However, conventionally, such work has not been done. For this reason, when errors are included in the hardware design, these errors are usually detected after the hardware design is mounted on the semiconductor chip.
[0009]
To the best of the knowledge of the applicant of this patent application, there are no tools to automatically detect, formulate and confirm resource conflicts and register leaks. And without such a tool, it would be virtually impossible to achieve a hardware design without errors.
[0010]
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 in a hardware description language.
[0011]
[Means for Solving the Problems]
The property generation device of the present invention is based on the configuration for generating properties to be verified for a plurality of resources described in a hardware description language and hardware including data transfer using these resources. Have. The graph generation means generates a data transfer graph corresponding to the resource and data transfer described in the hardware description language. The optimization unit optimizes the data transfer graph generated by the graph generation unit. The property generation means generates a property to be verified for the hardware described in the hardware description language using the data transfer graph optimized by the optimization means.
[0012]
In the above configuration, the design information described in the hardware description language is graphed, and the property to be verified for the hardware is 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.
[0013]
Resources are, for example, registers, buses, input ports, and output ports, and are represented by nodes in the data transfer graph. On the other hand, data transfer is represented using an edge (arrow) in which the transfer source and transfer destination are defined. Then, the optimization unit minimizes the graph based on the topology of the data transfer graph.
[0014]
Properties to be generated are, for example, resource contention and register leakage. The resource contention property is detected in a node to which a plurality of fan-in edges are connected in the data transfer graph. On the other hand, a register leak is detected in a node representing a register to which a fan-in edge and a fan-out edge are connected in the data transfer graph.
[0015]
DETAILED DESCRIPTION OF THE INVENTION
Hereinafter, embodiments of the present invention will be described 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 this embodiment extracts a property from a hardware specification 2 created in advance and causes the verification tool 3 to verify it.
[0016]
Hardware specification 2 is a design description of certain hardware (for example, a logical device such as a processor mounted on a semiconductor chip), and defines a plurality of resources included in the hardware and data transfer between these resources. To do. The hardware specification 2 is described in, for example, a register description level hardware description language. The hardware description language is, for example, Verilog. The defined resources are, for example, a register, a register file, a bus, an input port, an output port, and an input / output port.
[0017]
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, the upper layer module is often referred to as “parent” and the lower layer module is referred to as “child”. Each module includes one or more resources.
[0018]
The property generation tool 1 analyzes the input hardware specification 2 and extracts properties (items or conditional expressions to be verified by the verification tool 3). In this embodiment, the properties are “resource contention” and “register leak”, and are expressed by, for example, a temporal logic expression (conditional expression of signal change with time) such as CLT.
[0019]
The verification tool 3 is an existing logical verification tool, and verifies the properties extracted by the property generation tool 1. Specifically, it is verified whether or not “resource conflict” or “register leak” occurs in the hardware described by the hardware specification 2. The verification tool 3 can also verify other items.
[0020]
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.
In step S1 (Phase 1), a data transfer graph (DTTDAG: Data Transfer Directed Acyclic Graph) is created based on the description of the hardware specification 2. At this time, a resource is recognized for each module defined in the hardware specification 2, and further, when modules are described hierarchically, a parent-child relationship of these resources is also recognized. In addition, conditions related to data transfer are considered. These conditions are described in the hardware specification 2. The data transfer graph represents resources and data transfers included in the hardware described by the hardware specification 2.
[0021]
In step S2 (Phase 2), the data transfer graph created in step S1 is optimized (simplified or minimized). Specifically, among resources and data transfers represented in the data transfer graph, resources or data transfers that are unlikely to cause “resource conflict” or “register leakage” are deleted.
[0022]
In step S3 (Phase 3), properties are extracted from the data transfer graph optimized in step S2, and an input script corresponding to them is generated. This input script is described in a format that can be processed by the verification tool 3.
[0023]
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. The data transfer graph is created based on the input hardware specifications, but the description of the creation method is omitted here. The data transfer graph is basically not actually displayed on the computer screen. Therefore, the graph shown in FIG. 3 schematically shows the data transfer graph. The same applies to the following drawings. However, it is possible to actually display the data transfer graph on the computer screen, and it may be so.
[0024]
Each of the nodes A to F, H, and I corresponds to a data resource. For example, the node A is a register given the name “interface control register file” in the hardware specification 2. An arrow drawn between nodes corresponds to data transfer. Hereinafter, this arrow will be referred to as “data transfer edge” or simply “edge”. For example, the edge corresponding to the data transfer from the node A to the node D is a fan-out edge (or output edge) for the node A, and at the same time a fan-in edge (or input edge) for the node D. is there.
[0025]
Each data transfer edge is provided with definitions and conditions for the data transfer. “C” indicates that the data transfer is “Concurrent Transfer”, and “S” indicates that the data transfer is “Sequential Transfer”. “G i” represents an operation condition (guard or enabling condition) for data transfer. For example, in the example shown in FIG. 3, data transfer from the node A to the node D is executed when the condition G1 is satisfied.
[0026]
In the data transfer graph, when there are multiple fan-in edges for a certain node (Multiple fan-in), there is a possibility that “resource competition” may occur. Note node D. Node D is a 32-bit register “reg data out”. An edge AD and an edge BD are input to the node D. Therefore, when the condition G1 is satisfied, the data stored in the node A (register “interface control register file”) is transferred to the node D (register “reg data out”), and the condition G2 is satisfied. Data is transferred from node B (input port “data out”) to node D (register “reg data out”). In this case, if conditions G1 and G2 are met simultaneously in any clock cycle, two write accesses to register "reg data out" will occur simultaneously. That is, “resource competition” occurs.
[0027]
The “resource contention” as described above may occur in a node having a plurality of fan-in edges in the data transfer graph. Therefore, the property generation tool 1 detects a node in which a plurality of fan-in edges exist in the data transfer graph. Then, the verification tool 3 verifies whether or not “resource conflict” actually occurs, taking into account the timing of data transfer related to the node.
[0028]
Further, when a fan-in edge and a fan-out edge exist for a certain node, “register leakage” may occur. For example, the node D has fan-in edges AD and BD and a fan-out edge DF. Here, it is assumed that the hardware performs an operation of writing the data of the node B to the node D after sending the data of the node A to the node F via the node D. Therefore, this operation is obtained when the conditions G1, G6, G2 are satisfied in that order. However, if the condition G1 and the condition G2 are satisfied before the condition G6 is satisfied, the data transfer from the node D to the node F is overwritten (data overwrite) by the data transferred from the node D to the node B. ) Will be executed after. That is, “register leakage” occurs.
[0029]
Note that “register leakage” can also occur when there is one fan-in edge for a node. For example, when transferring data from a first node to a third node via a second node, the first node before the data transfer from the second node to the third node is executed. When other data is transferred from to the second node, a “register leak” can occur as in the case described above.
[0030]
As described above, the “register leakage” as described above may occur when one or more fan-in edges and one or more fan-out edges exist in a certain node in the data transfer graph. Therefore, the property generation tool 1 detects a node where a fan-in edge and a fan-out edge exist from the data transfer graph. Then, the verification tool 3 verifies whether or not “register leakage” actually occurs, taking into consideration the timing of data transfer related to the node.
[0031]
Still other problems are inherent when there are fan-in and fan-out edges 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 the fan-out edge of the node are satisfied within 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, in consideration of clock distortion at the gate level or the layout level, there is a possibility that erroneous data is read from the register. That is, if the clock is distorted, new data may be written to the register before the data is completely read from the register in a certain clock cycle. This problem appears as a register leakage property on an actual semiconductor chip. In the example illustrated in FIG. 3, for example, this type of “resource conflict” may occur between data transfer from the node I to the node C and data transfer from the node C to the node D.
[0032]
As described above, the verification tool 3 verifies whether or not “resource contention” and “register leakage” actually occur. That is, the property generation tool 1 automatically generates properties that may cause these problems from the hardware specification 2 and passes them to the verification tool.
[0033]
Note that the above-described properties (“resource conflict” and “register leakage”) relate to the topology of the described hardware resource and data transfer when the data transfer graph is represented. That is, by analyzing the topology of the data transfer graph, it is possible to determine the possibility of “resource conflict” or “register leak”. Therefore, the property generation tool 1 can automatically generate properties from the topology of the data transfer graph. However, in this case, information relating to resource and data transfer needs to be extracted from the register transfer level code.
[0034]
By the way, when the hardware described in the hardware specification 2 becomes large-scale, the data transfer graph generated from the description inevitably 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 data transfer operating conditions (logic optimization) can be considered.
[0035]
FIG. 4 is a flowchart of a process for optimizing the data transfer graph. This process corresponds to step S2 in FIG.
In step S11, “Unfragmented Equivalence” is detected. In step S12, "Fragmented Equivalence" is detected. In step S13, “Named Equivalence” is detected. In step S14, “Fragmented Edges” are detected. In step S15, “Equivalent Edges (Edges in Equivalence)” is detected. In step S16, a “register file (Register File)” is detected. Through steps S11 to S16, an equivalence relationship between resources is detected. Then, using these equivalence relations, a portion where there is no possibility of “resource conflict” or “register leakage” is deleted from the data transfer graph. This optimizes (ie, minimizes) the data transfer graph.
[0036]
Here, some of the processes in steps S11 to S16 will be briefly described. In addition, each process of step S11-S16 is demonstrated in detail, referring the below-mentioned flowchart.
[0037]
FIG. 5 is an example of hardware. FIG. 6 is a diagram for explaining a method of hierarchically describing the hardware shown in FIG. 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”.
[0038]
Thus, when data resources and data transfer are described for each hierarchy, different names are often given to the same resources or data. For example, in the example shown in FIG. 6, “input 1” that is an input to the module 0 is described as “input 11” in the module 1.
[0039]
By the way, in the hardware description language, data transfer between modules is usually described using an input port or an output port. For example, the correspondence between “input 1” in module 0 and “input 11” in module 1 is often expressed as a data transfer from “input port 1” in module 0 to “input port 11” in module 1. . In the present embodiment, such a correspondence between ports is referred to as “port association”. This “port cooperation” is defined in the hardware specification 2.
[0040]
In the hardware description language, when data stored in a register in a module is transferred to another module, the data is described to be transferred via an output port. In this case, the same name as that given to the register is usually given to the output port. In the present embodiment, this correspondence is referred to as “named association”.
[0041]
FIG. 7 is a diagram illustrating an example of optimizing a data transfer graph using “resource equivalence”. FIG. 7 (a) shows a data transfer graph generated from the resource and data transfer definitions described in the hardware specification 2. FIG. 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.
[0042]
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, data transfer from the input port SD-DQ-IN to the register data-in can be handled as data transfer from the input port SD-DQ-IN to the output port data-in. Further, the output port data-in and the bus wire data-buf-out have a “port linkage” relationship with each other. That is, these two resources can be regarded as equivalent. Therefore, data transfer from the input port SD-DQ-IN to the output port data-in can be handled as data transfer from the input port SD-DQ-IN to the bus wire data-buf-out. If these equivalent relationships are used, the data transfer graph shown in FIG. 7A is optimized (ie, simplified) to the form shown in FIG. 7B.
[0043]
Note that in order for the data transfer source resource and the transfer destination resource to be equivalent, the bit widths of the data handled by these resources must be the same. Therefore, the following definition is obtained.
Definition 1: When a set of adjacent resources has the same bit width specification,
These equivalent resources are “non-fragment equivalent”.
[0044]
FIG. 8 is a diagram for explaining “fragment”. In the example shown in FIG. 8, an output port OP having a 32-bit width is provided in the intermediate level module C, and output ports OP1 to OP4 having an 8-bit width are provided in the higher-level module B, respectively.
[0045]
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.
[0046]
The output port OP and the output ports OP1 to OP4 in the model shown in FIG. 8 are each represented by a node in the data transfer graph, and the data transfer from the output port OP to the output ports OP1 to OP4 is represented by an edge. Is done. Here, as described above, when the nodes 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 a node that is “fragment equivalent” are referred to as “fragment edges”.
[0047]
The usefulness of “fragment equivalence” is that non-fragmented data transfers may be obtained by combining fragment data transfers. Further, it is possible to identify whether the data transfer is a fragment data transfer or a non-fragment data transfer based on whether the transfer source resource or the transfer destination resource of the data transfer is “fragment equivalent”.
[0048]
Another way to optimize fragment data transfer is “independent fragment data transfer”. The following definitions are provided for this “independent fragment data transfer”.
Definition 2: It is useful for any combination of edges in the fragment data transfer edge.
Those edges are “independent” if they do not cause source contention.
[0049]
In the optimization processing of this embodiment, “independent” edges are deleted from the data transfer graph. This avoids erroneous generation of resource contention properties or register leak properties.
[0050]
The register file is a technique for grouping a plurality of registers and simplifying the connection between the bus and each register in order to reduce the hardware scale. Thereby, for example, the configuration shown in FIG. 9A is simplified to the configuration shown in FIG. 9B. 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 optimization process of the data transfer graph, 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.
[0051]
Next, specific examples will be described.
First embodiment
10 to 15 are examples of the hardware specification 2 input to the property generation tool 1. Here, Verilog is used as a hardware description language.
[0052]
FIG. 10 is a code describing module 0. According to the description of section 1 of this code, module 0 comprises two input ports (INPUT1,2) and two output ports (OUTPUT1,2). Each of these ports is 16 bits wide. Further, a clock and a control signal are input to the module 0. Further, the module 0 is provided with a 16-bit bus wire CONEKT.
[0053]
According to the description in section 2, module 1 is provided in the 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 15 bits of the input port INPUT1 of the module 0 are associated with the input port IPORT3 of the module 1, and 0 to 7 bits of the input port INPUT1 of the module 0 are associated with the input port IPORT4 of the module 1. It has been. In this case, the input port INPUT1 is a “parent resource” of the input port IPORT3 and the input port IPORT4, and the input port IPORT3 and the input port IPORT4 are “child resources” of the input port INPUT1. A bus wire CONEKT is connected to the input ports IPORT 1 and 2 of the module 1.
[0054]
According to the description in section 3, module 2 is provided in the lower hierarchy of module 0. Section 3 defines the port correspondence between module 0 and module 2. The bus wire CONEKT is connected to the output port OPORT1 of the module 2.
[0055]
FIG. 11 and FIG. 12 are codes describing module 1. According to the description in Section 4, each input port (IPORT1-4) and output port (OPORT1,2) are each 8 bits wide. Further, according to the description in section 5, the module 1 is provided with a register A and a register B. 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 executed regardless of the clock or control signal. That is, these data transfers belong to the concurrent transfer type. Specifically, it is transfer by “continuous assignment”.
[0056]
According to the description in section 6, when the control signal 1 is given, the data input to the input port IPORT1 is written to the register A and the data input to the input port IPORT3 is written to the register B. 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 executed according to the control signal. That is, these data transfers belong to the sequential transfer type. Specifically, the transfer is based on “sequential always block”.
[0057]
13 to 15 are codes describing module 2. According to the description in section 8, each input port (IPORT5) and output port (OPORT3, 4) is 16 bits wide. Also, according to the description in section 9, module 2 comprises registers C-F. 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. Each register C to F is given a predetermined initial value.
[0058]
According to the description in section 10, when the control signal 3 is given, 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 D. It is. Further, according to the description in section 11, when the control signal 4 is given, predetermined calculation result data is written in the registers C and D. Further, according to the description in section 12, predetermined calculation result data is also written in the register F.
[0059]
According to the description in section 13, when the control signal 5 is given, the data stored in the register C is written into the register E. When the control signal 6 is supplied without the control signal 5 being supplied, the data stored in the register D is written into the register E. Further, when the control signal 7 is applied without the control signals 5 and 6 and when the control signals 5 to 7 are not applied, predetermined constant data is written in the register E, respectively.
[0060]
FIG. 16 is a data transfer graph generated from the hardware specifications shown in FIGS. This graph is generated by step S of the flowchart shown in FIG. Note that data resources defined in the hardware specification are represented as “nodes” in the data transfer graph. For each node, a 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 (indicated by “arrow” in FIG. 16) in the data transfer graph.
[0061]
This data transfer graph is schematically drawn for easy understanding of the invention, and actually includes a module list, a data resource list, a data transfer edge list, an equivalent class list, and the like.
[0062]
The module list stores the following information for each module defined in the hardware specification.
Module name
-Parent module (upper layer module)
-Child module (module lower in the module)
-Hierarchy level (hierarchy to which the module belongs)
・ Processing status (such as flags indicating intermediate status in optimization processing)
・ Various pointers
For example, as information to be stored in the module list for module 0, the following is obtained from the hardware specification.
[0063]
-Module name: MOD0
-Parent module: None
・ Children modules: MOD1, MOD2
-Hierarchy level: 0
The “processing state” is a flag or the like representing an intermediate state in the optimization process, and is not obtained from the hardware specification. Also, the “pointer” is not obtained from the hardware specification.
[0064]
The data resource list stores the following information for each data resource defined in the hardware specification. This list is generated for each resource type (register, input port, output port, bus, data transfer, constant,...).
[0065]
・ Resource name
・ Parent module
・ Hierarchy level
・ Bit width specifications
・ Parent resources
・ Children resources
・ Non-fragment equivalence class
Fragment equivalence class
・ Edge
·Processing state
For example, as information to be stored in the data resource list for the input port INPUT1 (node A), the following is obtained from the hardware specification.
[0066]
-Resource name: INPUT1
-Parent module: None
-Hierarchy level: 0
-Bit width specification: “15: 0”
・ Parent resource: None
・ Children resources: IPORT5
・ Edge: Edge AF
Note that the “non-fragment equivalence class” and the “fragment equivalence class” are not obtained from the hardware specification, but are obtained by analyzing the data transfer graph.
[0067]
The data transfer edge list stores the following information for each data transfer defined in the hardware specification.
・ Name of edge
・ Transfer destination resources
・ Transfer source resource
-Guard expression (data transfer conditions)
・ Data transfer type (simultaneous transfer or sequential transfer, etc.)
-Fragment status of transfer destination or transfer source
・ Processing status in optimization processing
For example, the information to be stored in the data transfer edge list for the edge corresponding to the data transfer from the input port IPORT1 (node J) to the register REG-A (node 0) is obtained from the hardware specification as follows.
[0068]
・ Name of edge: 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)
The “transfer destination or transfer source fragment status” is obtained by analyzing the data transfer graph.
[0069]
The equivalence class list stores the following information. Such information can be obtained by analyzing the data transfer graph.
-Equivalent class identifier
-Resources belonging to each equivalence class
·Processing state
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 each defined data resource, the correspondence between those resources, and those resources are analyzed. Recognize data transfer using. At this time, the behavioral description is scanned to see if there is a call from one module to another. When such a call is made, a search queue is provided for each called module, and the correspondence relationship of the interface definition with the previously recognized resource is recognized.
[0070]
Also, the bit width of each port (including input port, output port, input / output port), bus wire, and register is recognized, and the driver and register corresponding to the bus wire are recognized for each bus wire.
[0071]
Information extracted from the hardware resource 2 is stored in a module list, a data resource list, and a data transfer edge list. In the example shown in FIGS. 10 to 15, the nodes A to Y (excluding E, G, P, Q, and R) shown in FIG. 16 are generated by these processes, and the bit width is set respectively.
[0072]
Further, the conditions set for each data transfer are analyzed. These conditions are, for example, “gurded continuous assignment statement”, “combinational alwaus block”, “sequential always block”. These pieces of information are registered as “guard expressions” in the data transfer edge list for each data transfer. As a result, an edge corresponding to each data transfer is generated. For data transfer for which no condition is set, “1” is assigned to the data transfer.
[0073]
When an assignment expression is described in the hardware specification (for example, section 10 and section 11), a pseudo resource Sdt is generated as shown in FIG. This pseudo resource Sdt is a virtual data source that implements the described substitution expression. For example, a node P (Sdt3) corresponding to the assignment expression described in section 11 is generated. The same applies to the nodes E and G. Further, when a predetermined constant is written in a certain register (for example, section 13), a pseudo resource Sdc is generated as shown in FIG. This pseudo resource Sdc is also a virtual data source. For example, nodes Q and R are generated corresponding to the definitions described in section 13. Note that these pseudo resources are generated by registering predetermined information in the data resource list based on the hardware specifications.
[0074]
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.
[0075]
When “non-fragment equivalence” is detected, a set of resources defined as being “equivalent” to each other in the interface definition of the hardware specification and having the same data width are recognized. In this case, the target resources are, for example, an input port, an output port, and an input / output port. When a resource belonging to the non-fragment equivalence class is detected, information indicating that is registered in a storage area corresponding to the resource in the data resource list.
[0076]
The equivalence relation is checked for each port. At this time, the process is continued for each port until the final resource is reached or a resource having a different bit width is reached.
[0077]
Here, “non-fragment equivalent” in the graph shown in FIG. 16 will be described. Node A (INPUT2 of module 0) and node F (IPORT5 of module 2) are both 16-bit input ports. These input ports are resources corresponding to each other as defined in section 3 of the hardware specification. That is, the resource corresponding to the node F is a “child” of the resource corresponding to the node A. Therefore, node A and node F are “non-fragment equivalent”. Similarly, node C is equivalent to node D, and node X is equivalent to node W.
[0078]
In this case, for example, if resource A and resource F belong to non-fragment equivalence class # 1, “# 1” is registered in “non-fragment equivalence class” of resource A and resource F, respectively, in the data resource list. The
[0079]
When “fragment equivalence” is detected, an equivalent one of the branched resources is recognized. In the example illustrated in FIG. 16, for example, data is transferred from the node B to the node H and the node I. At this time, the bit specifications of the node B are 16 bits wide, while the bit specifications of the node H and the node 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, node H and node I are “fragment equivalent”. The same applies to the nodes J and K.
[0080]
On the other hand, data is transferred from the node S and the node T to the node Y. 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, the node S and the node T are “fragment equivalent”.
[0081]
In this case, for example, if resource H and resource I belong to fragment equivalence class # 5, “# 5” is registered in “fragment equivalence class” of resource A and resource F in the data resource list.
[0082]
The “independent edge” is as follows. For example, the node P transfers data only to the node U, and the node U receives data only from the node P. In this case, the edge corresponding to the data transfer from the node P to the node U is an independent edge. In addition, data is transferred from the nodes S and T to the node Y. At this time, 0 to 7 bits are transferred from the node S, and 8 to 15 bits are transferred to the node T. 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, 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, node V to node W, for example. The edges corresponding to the data transfer are also independent edges.
[0083]
In connection with “independent edges”, the concepts of “fragment edges” and “equivalent edges” are introduced.
“Fragment edge” refers to an edge in which a transfer source resource or a transfer destination resource belongs to a fragment equivalence class. For example, in the example shown in FIG. 16, since the node J and the node K belong to the fragment equivalence class, in this case, the edge CJ, the edge CK, the edge JO, and the edge KO are fragment edges related to this equivalence class. Each edge consists of (1) the state where the source and destination resources are not "fragment equivalent", (2) the state where only the source resource is "fragment equivalent", and (3) only the destination resource Is "fragment equivalent", and (4) the source and destination resources are both "fragment equivalent". This classification is represented by a 2-bit flag for each edge.
[0084]
An “equivalent edge” is a set of edges in which a transfer source resource or a transfer destination resource is a node belonging to a 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 equivalent edges related to this equivalence class. The independent edge is removed from the set of edges belonging to the equivalent edge.
[0085]
After detecting the equivalence relationship as described above, the portion not related to “resource conflict” or “register leakage” is removed from the data transfer graph. Specifically, node A and node F are “non-fragment equivalent”. Therefore, node A is removed. The edge VW is an “independent edge”, and the node W and the node X are “non-fragment equivalent”. Therefore, the nodes W and X are removed. Furthermore, the edge PU and the edge UD are “independent edges”, respectively, and the node D and the node C are “non-fragment equivalent”. Therefore, the nodes P, U, and D are removed.
[0086]
Nodes H and I are “fragment equivalent” as viewed from the node B. Therefore, node B is removed. Similarly, node C is also removed. Nodes S and T are “fragment equivalent” as viewed from node Y. Therefore, node Y is removed. Furthermore, the edge NS and the edge OT are both independent edges. Therefore, the nodes S and T are removed.
[0087]
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 processing specifically corresponds to processing for generating the edge list Efinal from the data resource list and the data transfer edge list. The edge list Efinal is a list of edges obtained as a result of the optimization process.
[0088]
When the optimization process is finished, the process of step S3 in the flowchart of FIG. 2 is executed. This process includes two steps as shown in FIG. In step S21, an adjacent node list is created from the optimized data transfer graph. 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 leak” are extracted. Specifically, the adjacent node list is used to count the number of input edges and the number of output edges for each node, and a property is generated based on the count. Then, the extracted conditions that may cause “resource conflict” or “register leakage” are converted into a script that can be executed by the verification tool 3.
[0089]
Processing for generating properties from the graph shown in FIG. 18 will be described. First, an adjacent 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. Information about the transfer destination node and transfer source node for each edge is stored in the edge list Efinal obtained by the optimization process.
[0090]
Subsequently, by using the adjacent node list, a node where “resource contention” or “register leakage” may occur is detected. When detecting “resource competition”, a node having a plurality of input edges is detected. In the example shown in FIG. 20, there are two input edges in each of the nodes L, M, N, and O, and there are four edges in the node V. Therefore, these five nodes are considered to have the possibility of occurrence of “resource competition”.
[0091]
On the other hand, when detecting “register leakage”, a node having one or more input edges and one or more output edges is detected. In the example illustrated in FIG. 20, there are two input edges and one output edge at the nodes L and M. Therefore, these nodes are considered to have the potential for “register leaks”. In consideration of clock distortion, a node (register) that has a possibility of “register leakage” is considered to have a possibility of “resource conflict”.
[0092]
FIG. 21 shows an example of the “resource conflict” property. These properties are generated from the data transfer graph shown in FIG.
The “resource conflict” property is generated for each of the five nodes described above. At this time, conditions attached to input edges existing in each node are extracted, and a property is generated by combining these conditions.
[0093]
For example, when generating a property for the node L, the conditions given to the edge EL and the edge FL are extracted from the graph. That is, “control signal CTRL4” and “control signal CTRL3” are extracted from edge EL and edge FL, respectively, and the following properties are obtained by combining them.
[0094]
AG (CTRL4.CTRL3)
When this property is input, the verification tool 3 verifies whether there is a clock cycle in which the control signal CTRL4 and the control signal CTRL3 are generated simultaneously. When there are clock cycles in which they occur simultaneously, the verification tool 3 determines that “resource conflict” occurs in the node L. That is, it is assumed that simultaneous write access to the register C occurs.
[0095]
When there are three or more input edges in a certain node, any two input edges are extracted from them, and the conditions given to the two input edges are extracted from the graph. The This process is performed for all combinations. For example, node V has four input edges. In this case, there are six combinations (edge QV and edge LV, QV and MV, QV and RV, LV and MV, LV and RV, MV and RV). can get. A property is generated for each combination.
[0096]
FIG. 22 shows an example of the “register leak” property. These properties are also generated from the data transfer graph shown in FIG. The “register leakage” detected in this embodiment assumes a case where a sequence that should be “write, read, write” is executed in a sequence of “write, write, read”.
[0097]
When attention is paid to the node L, the following four conditions are likely to cause “register leakage”. That is, (1) When data is transferred from the node E to the node L 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) When data is transferred from the node F to the node L without transferring the data from the node L to the node V after the data is transferred from the node F to the node L, (3) When data is transferred from node E to node L without transfer from node L to node V after data is transferred to (4), data is transferred from node E to node L. This is a case where data is transferred from the node F to the node L without performing transfer from the node L to the node V later. Note that, in the node M, properties are generated basically in the same manner. For example, the property in case of (1) is
EF (CTRL4 / \ EX (E (~ CTRL5 U CTRL4)))
It is expressed.
[0098]
When this property is input, the verification tool 3 searches for “a clock cycle in which the control signal CTRL4 is generated without generating the control signal CTRL5 after the clock cycle in which the control signal CTRL4 is generated”. If such a situation exists, the verification tool 3 determines that “register leakage” occurs in the node L.
[0099]
FIG. 23 is 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, “resource contention” assumes a case where a write access and a read access occur in a certain clock cycle.
[0100]
When attention is paid to the node L, there are the following two conditions where “resource conflict” may occur. That is, (1) data transfer from node E to node L, and data transfer from node L to node V are performed within a dynamic clock cycle, and (2) data transfer from node F to node L. This is a case where the data transfer from the node L to the node V is executed within a moving clock cycle. Note that properties are generated in the same manner in the node M as well.
[0101]
For example, the property in case of (1) is
AG (CTRL4.CTRL5)
Represented as: 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 are generated simultaneously. If such a clock cycle exists, the verification tool 3 determines that “resource contention” occurs in the node L.
Second embodiment
24 to 26 are examples of hardware specifications 2 input to the property generation tool 1. In this embodiment, Verilog is used as a hardware description language.
[0102]
In section 1, input control signals, input data, and output data are defined. According to the description in section 1, this module is provided with five registers (BASES, ENDS, MODE, REG-ADR, REGA-OUT). Section 2 describes data transfer when the control signal CNT-REG-ACC and the control signal WRITE are given. These data transfers are 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.
[0103]
FIG. 27 is a data transfer graph generated from the hardware specifications shown in FIGS. Since the method for generating the data transfer graph from the hardware specifications is the same as in the first embodiment, the description thereof is omitted here.
[0104]
In the graph shown in FIG. 27, “G1” to “G11” are conditions as triggers for data transfer. These conditions are shown in FIG. For example, according to the description in section 2, the data transfer from the node A to the node D is given the control signal CNT-REG-ACC and the control signal WRITE, and the fourth bit of the register REG-ADR is “1”. Yes, and executed in a clock cycle in which the third to zeroth bits of the register REG-ADR are “0001”. “G1” shown in FIG. 28 describes this condition.
[0105]
A set of elements included in each condition is referred to as a “support set”. For example, the support set for Condition G1 has 7 elements (CNT-REG-ACC, WRITE, REG-ADR (4), REG-ADR (3), REG-ADR (2), REG-ADR (1), REG -ADR (0)) is included.
[0106]
When optimizing this data transfer graph, the concepts of “register file” and “name equivalence” are used. When a “register file” is detected, 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 the edges that are the same as each other are grouped. In this case, a register connected to each of a plurality of grouped edges is regarded as a “register file”.
[0107]
A specific example is shown with reference to FIG. Here, attention is paid to the edge AD whose transfer destination node is a register. The condition G1 is given to the edge AD. In this case, when detecting a register file, first, an edge having the same support set as the support set of G1 is extracted from fan-in edges to the node representing the register. The support set of the condition G1 is the same as the conditions G2 to G6, respectively, as shown in FIG. Therefore, among the fan-in edge edges to the node representing the register, the edges for which the conditions G2 to G6 are set are extracted. Thereby, the edges for which the conditions G1 to G6 are set are grouped. That is, the edges AD, AE, and AF are grouped. Accordingly, the three nodes (D, E, F) that are the transfer destinations of these edges are regarded as belonging to the register file.
[0108]
In the above example, the register file is detected based on the fan-in edge to the register. However, as shown in FIG. 29, the same relationship can be obtained by using the fan-out edge from the register.
[0109]
When detecting “name equivalence”, nodes (in particular, registers and output ports) to which the same name is assigned are extracted from the nodes in the same module, and these 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.
[0110]
After detecting the equivalence relationship as described above, the portion not related to “resource conflict” or “register leakage” is removed 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 ′). Node J and node I are “name equivalent”. Therefore, node I is removed. As a result of the above optimization process, the data transfer graph shown in FIG. 27 is optimized to the state shown in FIG.
[0111]
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 aggregated into the condition G1 ', while the conditions G7 and G8 are aggregated into the condition G2'. FIG. 31 shows a support set for the condition G1 'and the condition G2'.
[0112]
In the hardware of the second embodiment, there is a possibility that “resource conflict” may occur in the node J. In this case, the “resource contention” property is a script for examining clock cycles in which any two of the four conditions (G2 ′, G9, G10, and G8) occur simultaneously. Further, with this hardware, there is a possibility that “register leakage” may occur in the node D ′. In this case, the property of “register leak” is a script for checking whether the conditions G1 ′ and G2 ′ occur in a predetermined order.
[0113]
Next, an operation algorithm of the above-described property generation tool 1 will be described with reference to a flowchart. In the following description, the following definitions are used.
L module hierarchy level
Set of M modules
Si input port set
So output port set
Sio I / O port set
Sw set of bus wires
Set Sr register
Sdt data element (resource that generates the result of an operation such as an assignment expression)
Sdc data constants (resources that generate constants)
Edt Data transfer edge
Set of N nodes
H Set of equivalence classes for data resources
32 to 34 are flowcharts for explaining a method of generating a data transfer graph. This process is executed when the hardware specification 2 described in the hardware description language is input.
[0114]
In step S31, a memory area used for creating a property is initialized. At this time, “0” is set as the module hierarchy L. Further, “Wb” is set as the minimum bit width parameter.
[0115]
In step S32, the root module is registered in the module list M. In the module list M, all modules provided in the hardware specification 2 are registered. Step S33 is a determination process for executing the processes in and after step S34 for each module registered in the module list M.
[0116]
In step S34, the module Mi is extracted from the module list M. 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 checked 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, and if not, the process returns to step S35 to extract the next port.
[0117]
In step S37, it is checked whether 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 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 an input port nor an output port, the port P is registered in the input / output port list Sio in step S39.
[0118]
Through the above processing, each port defined in the hardware specification 2 is registered in the input port list Si, the output port list So, or the input / output port list Sio.
[0119]
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 checked 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 larger than the minimum bit width parameter Wb, the process proceeds to step S53. Otherwise, the process returns to step S51 to extract the next variable.
[0120]
In step S53, it is checked 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, the variable V is registered in the bus wire variable list Sw in step S54.
[0121]
Through the above processing, each variable defined in the hardware specification 2 is registered in the register variable list Sr or 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 step S57, the module instantiation m-j is registered in the module list M. In step S58, the port of module instantiation m-j is associated with the previously identified resource in module Mi.
[0122]
Step S61 is a process for executing steps S62 to S72 for each simultaneous process CP in the module Mi. In step S62, it is checked whether or not the simultaneous processing CP is a continuous assignment type. If the simultaneous processing CP is a continuous assignment type, “C (Concurrent)” is set as the data transfer processing type of the processing CP in step S71. In step S72, a data transfer edge is generated.
[0123]
In step S63, it is checked whether or not the simultaneous processing CP is a guarded continuous assignment type. In step S64, it is checked whether or not the simultaneous processing CP is a combinational always block type. If the determination result in step S63 or S64 is “Yes”, “C” is set as the data transfer processing type of the processing CP in step S70. On the other hand, if the determination results in steps S63 and S64 are both “No”, in step S65, “S (Sequential)” is set as the data transfer processing type of the processing CP.
[0124]
In step S66, all guard conditions are recognized. Here, each guard condition controls 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 transfer destination of the data transfer controlled by this guard condition are recognized. In step S68, a data transfer edge is generated. Step S69 is a process for executing steps S66 to S68 for each data transfer.
[0125]
With 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.
[0126]
In step S81, it is checked whether or not the data transfer source is an assignment expression. When 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.
[0127]
If the transfer source of the data transfer is neither an assignment expression nor a constant, the transfer source resource Source is recognized in step S85. In step S86, it is checked whether or not the data transfer source 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.
[0128]
When the pseudo resource Sdt or the pseudo resource Sdc is generated, or when the determination result in step S86 is “Yes”, the transfer destination resource Sink is recognized in step S87. In step S88, it is checked whether or not the data transfer destination 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.
[0129]
If the determination result in step S88 is “Yes”, an edge E is generated in step S89 based on the data transfer source and destination. 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 data transfer source and destination. In this embodiment, the edge E is not generated when the transfer source or transfer destination of the data transfer is not a port, a register, a bus wire, or a pseudo resource.
[0130]
With the above processing, for each data transfer defined in the hardware specification 2, a data transfer edge in which a transfer source and a transfer destination of the data transfer are defined is generated.
[0131]
36 and 37 are flowcharts of processing for detecting “non-fragment equivalence”. This flowchart is an example of step S11 of the flowchart shown in FIG. Although the input / output port is described here, the same processing is executed for the input port and the output port.
[0132]
In step S101, the input / output port list Sio is scanned. Step S102 is a process for executing the processing after step S103 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.
[0133]
In step S104, the extracted element Sio-k is added to the queue Q. In step S105, it is checked whether or not queue Q is empty. If the queue Q is empty, the process returns to step S102. If one or more elements are held in the queue Q, the element q is extracted from the queue Q in step S106.
[0134]
In step S107, it is checked whether or not the element q has “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 hierarchy in which the element q is provided, and is associated with the element q. Say things. The correspondence is described in the hardware specifications.
[0135]
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”, the process returns to step S108. move on. In step S108, a non-fragment equivalence class Hek corresponding to the element Sio-k is generated. In step S109, the Eqvl flag is reset.
[0136]
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 and the bit width of the “child resource qc” are the same. If these bit widths are different from each other, the process returns to step S110 to extract the next "child resource". If the bit widths are the same, “1” is set to the Eqvl flag in step S123. 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”.
[0137]
When the processing of steps S121 to S126 is executed for all “child resources”, it is checked in step S111 whether the Eqvl flag is “1”. If the Eqvl 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 processes in steps S112 and S113 are skipped.
[0138]
Thus, when the bit width of a port and the bit width of the “child resource” of the port are the same, the port and the “child resource” are regarded as “non-fragment equivalent”.
[0139]
38 to 41 are flowcharts of processing for detecting “fragment equivalence”. This flowchart is an example of step S12 of the flowchart shown in FIG. Although the input / output port is described here, the same processing is executed for the input port and the output port.
[0140]
In 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-l is extracted from the input / output port list Sio.
[0141]
In step S134, it is checked whether or not the element Sio-l belongs to any equivalence class Hek. If the element Sio-l belongs to any equivalence class Hek, the process proceeds to step S135. If not, the process returns to step S132 after executing the processes of steps S141 to S146.
[0142]
In step S141, it is checked whether or not the element Sio-l has “child resource”. If the element Sio-l has “child resource”, the process from step S142 is executed, and if not, the process returns to step S132. In step S142, a fragment equivalence class OIFHe corresponding to the element Sio-l is generated. In step S143, “child resource” having a bit width smaller than the bit width of element Sio-l is recognized using element Sio-l as a root (starting point). In step S144, “fragment equivalence class OIFHe” is set in the fragment equivalence field for each “child resource”. In step S145, “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.
[0143]
If the element Sio-l belongs to any equivalence class Hek, the fragment child-found flag is reset in step S135. In step S136, with the element Sio-l as the root, “child resource” having a bit width smaller than the bit width of the element Sio-l or “child resource having a bit width larger than the bit width of the element Sio-l”. Search for. At this time, the set of the extracted “fragment children” is defined as “F-child”. On the other hand, a set of “non-fragmented child resources” having a larger bit width is defined as “UG-child”.
[0144]
In step S137, it is checked whether or not an element of the set F-child exists. If there is an element of the set F-child, the fragment child-found flag is set in step S138. In step S139, a fragment equivalence class OIFHe corresponding to the element Sio-l is generated.
[0145]
In step S151, the set F-child is scanned. Step S152 is a process for executing steps S153 to S156 for each element belonging to the set F-child. In step S153, an element Cd-i is extracted from the set F-child. In step S154, the “parent resource P-Cd-i” of the element Cd-i is extracted. In step S155, “fragment equivalence class OIFHe” is set in the fragment equivalence field for element Cd-i and parent resource P-Cd-i. In step S156, the element Cd-i is added to the fragment equivalence class OIFHe.
[0146]
If there is no element of the set F-child, the processes of steps S161 to S172 are executed. 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 further extracted.
[0147]
In step S166, a fragment equivalence class OIFHe corresponding to the element Cd-i is generated. Step S167 is a process 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 equivalence class OIFHe” is set in the fragment equivalence field for each element of the non-fragment equivalence class Hek. In step S172, the non-fragment equivalence class Hek is deleted from the non-fragment equivalence field for each element.
[0148]
FIG. 42 is a flowchart of processing 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, the element (register) Sr-l is extracted from the register list Sr.
[0149]
In steps S184 to S186, the name of the extracted element Sr-l is compared with the name of each element in the output port list So. If there is an element So-j having the same name as the element Sr-l in the output port list So, the non-fragment equivalent class Hek to which the element So-j belongs is determined in step S187. look for. In step S188, “non-fragment equivalence class Hek” is set in the non-fragment equivalence class field for element Sr-l. In step S189, the element Sr-l is added as an element of the non-fragment equivalence class Hek.
[0150]
Through the above processing, a certain register and an output port assigned the same name as that 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 “fragment edge” or “non-fragment edge” is generated. This flowchart is an example of step S14 in the flowchart shown in FIG.
[0151]
In step S191, the data transfer edge list Edt is scanned. Step S192 is a process for executing steps S193 to S200 for each element of the data transfer edge list Edt. In step S193, an element (edge) Ej is extracted from the data transfer edge list Edt. At this time, the transfer source and transfer destination of the data transfer corresponding to the edge Ej are recognized.
[0152]
In step S194, it is checked whether or not the data transfer destination corresponding to the edge Ej is “fragment equivalent”. If the transfer destination is “fragment equivalent”, it is checked in step S195 whether the transfer source of the data transfer corresponding to the edge Ej is “fragment equivalent”. If both the transfer destination and the transfer source are “fragment equivalent”, both fragment flags are set in step S196, and if only the transfer destination is “fragment equivalent”, the transfer is performed in step S197. Set the destination fragment flag. On the other hand, if the transfer destination is not “fragment equivalent”, it is checked in step S198 whether or not the transfer source of the data transfer corresponding to the edge Ej is “fragment equivalent”. If only the transfer source is “fragment equivalent”, the transfer source fragment flag is set in step S199. If neither the transfer destination nor the transfer source is “fragment equivalent”, step S200 is performed. Set the non-fragment flag at.
[0153]
By the above processing, the edges corresponding to each data transfer are classified into both fragment edges, transfer destination fragment edges, transfer source fragment edges, or non-fragment edges.
[0154]
44 to 48 are flowcharts of processing for detecting an “equivalent edge”. This flowchart is an example of step S15 of the flowchart shown in FIG.
[0155]
In step S211, the data transfer edge list Edt is scanned. Step S212 is a process for executing the processes in and after step S213 for each element of the data transfer edge list Edt. In step S213, an element (edge) Ej is extracted from the data transfer edge list Edt. At this time, the transfer source and transfer destination of the data transfer corresponding to the edge Ej are recognized.
[0156]
In step S214, it is checked whether the edge Ej is a transfer source fragment. If the edge Ej is a transfer source fragment, the process proceeds to step S215. If not, the process proceeds to step S241. In step S215, the transfer source fragment equivalence is set to “FHej”. In step S216, the elements belonging to the fragment equivalent FHej are scanned. Step S217 is a process for executing steps S218 to S224 for each element belonging to the fragment equivalent FHej.
[0157]
In step S218, an element (port or the like) Ni is extracted from the fragment equivalent FHej. In step S219, all edges including the element Ni as the transfer source node or transfer destination node are extracted. In step S220, the extracted edge list is scanned. Step S221 is a process 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 edge list. At this time, the transfer destination node of the data transfer corresponding to the edge Ek is set to “Head-k”. In step S223, it is checked whether or not this transfer destination node Head-k is the same as the transfer destination extracted in step S213. If they are the same as each other, in step S224, the edge Ek is added to the set Eqv-Tail-Ej of equivalent edges of the edge Ej.
[0158]
When the processes of steps S218 to S224 are executed for all elements belonging to the fragment equivalent FHej, an interval graph IG is created based on the bit width vectors of the edge nodes belonging to the set Eqv-Tail-Ej in step S231.
[0159]
Here, the interval graph will be described with reference to FIGS. 49 to 51. Here, it is assumed that the data transfer graph shown in FIG. 49 is generated. Further, the data transfer between nodes shown in FIG. 49 is defined as shown in FIG. It is assumed that a control signal corresponding to the guard condition, a bit used at the transfer destination node, and a bit bit at 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 using T1 to T10.
[0160]
When creating an interval graph from a data transfer graph, first, each data transfer is represented by a dot (dot). Then, for each data transfer, the data transfer in which the bits to be used in the transfer destination node overlap is extracted and connected.
[0161]
For example, pay attention to data transfer T1. Data by the data transfer T1 is written to the 7th to 0th bits of the node T. At this time, the data transferred by the data transfer T2 is written into 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 from data transfers T3, T8, T9 and T10 also overlap at node T with data from data transfer T1. In this case, the point representing the data transfer T1 is connected to the points representing the data transfers T2, T3, T8, T9 and T10 as shown in FIG.
[0162]
Thereafter, an interval graph shown in FIG. 51 is obtained by executing the same method for other data transfers.
Return to the description of the flowchart. In step S232, the connection between the parts (“points” in FIG. 51) in the interval graph IG is examined. In step S233, a set NSCC of non-single parts is extracted. Each set NSCC includes a plurality of data transfers corresponding to points connected to each other in a mesh form 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 data transfers corresponding to these points belong to one set NSCC. In step S234, a set SCC of single parts is extracted. Data transfers that do not belong to any set NSCC belong to the set SCC.
[0163]
In step S235, an independent subset Ind-Eqv-Tail-Ej is created from the edges belonging to each set NSCC and included in the set Eqv-Tail-Ej. In step S236, the independent subset Ind-Eqv-Tail-Ej is deleted from the set Eqv-Tail-Ej. In step S237, the set Eqv-Tail-Ej is divided into one or more subgroups based on the set NSCC. In step S238, an edge list Efinal is obtained for each subgroup. In step S239, the set Eqv-Tail-Ej of each subgroup is added to the edge list Efinal.
[0164]
If the edge Ej is not a transfer source fragment (S214: No), it is checked in step S241 whether the edge Ej is a transfer destination fragment or both fragments. If the edge Ej is the transfer destination fragment or both fragments, the process proceeds to step S242; otherwise, the edge Ej is added to the edge list Efinal as a single block in step S249, and then the process returns to step S212.
[0165]
In step S242, the parent resource field of the data transfer destination corresponding to the edge Ej is traversed until a non-fragmented parent resource UF-Parent-j is found. In step S243, the non-fragment equivalence class to which the parent resource UF-Parent-j belongs is set to “UHPej”. In step S244, the non-fragment equivalence class UHPej is scanned. Step S245 is a process for executing steps S246 to S248 for each element belonging to the non-fragment equivalence class UHPej. In step S246, an element (node) Ni is extracted from the non-fragment equivalence class UHPej. In step S247, all edges including the node Ni as the transfer destination node are extracted. In step S248, each extracted edge is added to a set of equivalent edges Eqv-Head-Ej.
[0166]
In step S251, it is checked whether or not the node Ni extracted from the non-fragment equivalence class UHPej is fragment equivalent. If the node Ni is fragment equivalent, 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 equivalence class FHej is scanned. Step S254 is a process for executing steps S255 to S257 for each element belonging to the fragment equivalence class FHej. In step S255, the node Nk is extracted from the fragment equivalence class FHej. In step S256, all edges including the node Nk as the transfer destination node are detected. In step S257, the extracted edges are added to an equivalent edge set E-Head-Ej.
[0167]
When steps S246 to S248 are executed for each node (step S245: Yes), steps S261 to S268 are subsequently executed. Steps S261 to S268 are basically the same as steps S231 to S237 and S239. However, in steps S261 to S268, an interval graph IG related to edges belonging to the set Eqv-Head-Ej is created, and an edge list Efinal is obtained using the graph.
[0168]
52 to 55 are flowcharts of processing for detecting “register file”. This flowchart is an example of step S16 of the flowchart shown in FIG.
[0169]
In 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, an element (edge) Ej is extracted from the data transfer edge list Edt. Further, the transfer source Source and transfer destination sink of the data transfer corresponding to the edge Ej are detected.
[0170]
In step S274, it is checked whether the transfer source or transfer destination of the edge Ej is a register. If the transfer source or transfer destination is a register, the process proceeds to 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 checked whether or not the detected transfer destination is a register. If the transfer destination is a register, the process proceeds to step S277, and if not, steps S277 to 280 are skipped.
[0171]
In step S277, the control signal set SSS-Ej is associated with the transfer destination. In step S278, a set of control signals Sink-Support-Set included in the guard expression of data transfer whose transfer destination is a register is obtained. In step S279, the control signal set SSS-Ej is associated with the control signal set Sink-Support-Set. In step S280, the transfer destination is added to a set of transfer destination registers Sink-Registors.
[0172]
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. If not, the process returns to step S272. In step S282, the control signal set SSS-Ej is associated with the transfer source. In step S283, the control signal set SSS-Ej is associated with the control signal set Source-Support-Set. In step S284, the transfer source is added to a set of transfer source registers Source-Registors.
[0173]
When the processing of steps S273 to S284 is executed for all edges, a combined U-Source-Sets of control signal sets Source-Support-Set is created in step S291. In step S292, a combined U-Sink-Sets of control signal sets Sink-Support-Set is created. In step S293, random total order To-U-Source-Sets composed of unique elements belonging to the combined body U-Source-Sets is created. In step S294, random total order To-U-Sink-Sets composed of unique elements belonging to the combined body U-Sink-Sets is created.
[0174]
In step S295, Sink-Support-Set is scanned. Step S296 is a process for executing steps S297 to S300 for all sets belonging to the Sink-Support-Set. In step S297, SSS-Ej is extracted from Sink-Support-Set. In step S298, a bit vector representation BV-SSS-Ej of SSS-Ej is created based on To-U-Sink-Sets. 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 associated with SSS-Ej. In step S300, BV-SSS-Ej is added to SSS-Ej. At this time, BV-Sink-Support-Sets is a set of bit vector expressions of Sink-Support-Set.
[0175]
When the processes of steps S297 to S300 are executed for all sets, the process proceeds to step S311. Step S311 is a process for executing steps S312 to S315 for all sets belonging to Source-Support-Set. Steps S312 to S315 are basically the same as steps S297 to S300 described above.
[0176]
In step S316, the BV-Sink-Support-Set vector list is scanned. Step S317 is a process for executing steps S318 to S324 for each vector belonging to the vector list. In step S318, BV-SSS-Ej is extracted from the vector list. In step S319, the BV-Sink-Support-Set vector list is rescanned. Step S320 is a process 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. In step S322, it is checked whether BV-SSS-Ej and BV-SSS-Ek are the same. If they are the same, the transfer destination register Reg-sink-k corresponding to BV-SSS-Ek is detected in step S323. When the processes of steps S321 to S323 are executed for all vectors, the transfer destination register Reg-sink-k is added to the set of transfer destination register files Sink-Reg-Files in step S324.
[0177]
Steps S331 to S339 are basically the same as the processes of steps S316 to S324. However, in steps S331 to S339, each element belonging to the vector list of BV-Sink-Support-Set is processed, and a predetermined transfer source register is added to the set Source-Reg-Files of the transfer source register file.
[0178]
In step S341, a list of transfer destination register file sets Sink-Reg-Files is scanned. Step S342 corresponds to processing for executing steps S343 to S348 for each set belonging to the list. In step S343, the set Sink-Reg-File-k is extracted from the above list. In step S345, it is checked whether all sets have been processed. If there is an unprocessed set, the set Source-Reg-File-l is extracted in step S346. In step S347, it is checked whether or not the set Sink-Reg-File-k and the set Source-Reg-File-l are the same. If they are the same, in step S348, the set Source-Reg-File-k is added to the set Reg-Files. Through the above processing, registers belonging to the register file are obtained.
[0179]
As described above, the data transfer graph generated by the processing shown in the flowcharts of FIGS. 32 to 35 is optimized by the processing of the flowcharts described above. The result of the optimization is the edge list Efinal.
[0180]
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.
[0181]
In step S351, the edge list Efinal is scanned. Step S352 corresponds to a process for executing steps S353 to S361 for each subgroup belonging to the edge list Efinal. In step S353, the subgroup Pi is extracted from the edge list Efinal.
[0182]
Step S354 corresponds to the process for executing the processes of steps S355 to S361 for each edge belonging to the subgroup Pi. In step S355, an 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 equivalence 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 or not the non-fragment equivalence class Tail-Hej is an element of the node set N. If the non-fragment equivalence class Tail-Hej is not an element of the node set N, it is added to the node set N in step S359.
[0183]
In step S360, the non-fragment equivalent class Tail-Hej is added to the adjacent list of the non-fragment equivalent class Head-Hej in the node set N of the adjacent node list. Also, the number of input edges of the non-fragment equivalence class Head-Hej is incremented. On the other hand, in step S361, the non-fragment equivalent class Head-Hej is added to the adjacent list of the non-fragment equivalent class Tail-Hej in the node set N. Then, the number of input edges of the non-fragment equivalence class Tail-Hej is incremented.
[0184]
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.
[0185]
In step S371, the node set N in the adjacent node list is scanned. Step S372 is a process for executing the processes after step S373 for each node belonging to the node set N. In step S373, the node Nj is extracted from the node set.
[0186]
In step S374, it is checked whether the number of fan-in edges of the node Nj is 1 or more. If the number of fan-in edges is 1 or more, the process proceeds to step S375, and if not, the process returns to step S372. In step S375, a set Di-Arcs-into-Nj of edges (fan-in edge to the node Nj) whose transfer destination node is the node Nj is obtained. 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 1 or more, the process proceeds to step S377, and if not, step S377 is skipped.
[0187]
In step S377, a set Di-Arcs-out-of-Nj of edges (fan-out edges from the node Nj) whose transfer source node is the node Nj is obtained. In step S378, it is checked whether or not the node Nj is a register. If the node Nj is a register, the process proceeds to step S379, and if not, 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. If there is a fan-in edge belonging to the set Di-Arcs-into-Nj, a resource contention property between these fan-in edges is generated in step S380. Otherwise, the process returns to step S372.
[0188]
In step S381, it is checked whether there is a fan-out edge belonging to the set Di-Arcs-out-of-Nj. If there is a fan-out edge belonging to the set Di-Arcs-out-of-Nj, a product PS1 of the set Di-Arcs-into-Nj and the set Di-Arcs-out-of-Nj is generated in step S380. To do. PS1 is expressed as “Em, En”. “Em” and “En” are elements of the set Di-Arcs-into-Nj and the set Di-Arcs-out-of-Nj, respectively. On the other hand, if there is no fan-out edge belonging to the set Di-Arcs-out-of-Nj, the process returns to step S372.
[0189]
In step S391, PS1 is scanned. Step S392 corresponds to the process for executing the processes of steps S393 to S395 for each element of PS1. In step S393, the element PS-k (Ea, Eb) is extracted from PS1. 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 contention property for checking an error due to clock distortion is generated in step S395.
[0190]
In step S396, a product PS2 of the set Di-Arcs-into-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-Read =-(OR for each fanout edge Ei belonging to the set Di-Arcs-out-of-Nj. (Gi)) is generated. In step S398, PS2 is scanned. Step S399 corresponds to the processing for executing the processing 400 and S401 for each element belonging to PS2.
[0191]
In step S400, PS2-k = (Ec, Ed) is extracted from PS2. In step S401, a register leakage property EF (Gl "EX (E (No-ReadUGm))) is generated.
[0192]
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, it is checked in step S412 if an element exists in the set Di-Arcs-into-Nj. That is, it is checked whether there is a fan-in edge to the output port. If there is a fan-in edge, in step S413, a resource conflict property is generated for all combinations of the edges.
[0193]
In step S414, it is checked whether or not the node Nj is an input port. If the node Nj is an input port, a combination Union-Arcs-of-Nj of the set Di-Arcs-into-Nj and the set Di-Arcs-into-Nj is generated in step S415. In step S416, a product PS3 of Union-Arcs-of-Nj and Union-Arcs-of-Nj is generated.
[0194]
In step S417, PS3 is scanned. Step S418 corresponds to the process for executing the processes of steps S419 to S421 for each element belonging to PS3. In step S419, PS3-k = (Ee, Eg) is extracted from PS3. In step S420, 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.
[0195]
The function for generating the above-described property 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 the computer 100 that executes the program.
[0196]
The CPU 101 loads a program describing the processing shown in the above flowchart from the storage device 102 to the memory 103 and executes it. The storage device 102 is a hard disk, for example, and stores the program. On the other hand, the memory 103 is a semiconductor memory, for example, and is used as a work area of the CPU 101.
[0197]
The recording medium driver 104 accesses the portable recording medium 105 according to instructions from the CPU 101. The portable recording medium 105 is, for example, a semiconductor device (PC card or the like), a medium (floppy disk, magnetic tape, etc.) to which information is input / output by magnetic action, or a medium (optical disk) to which information is input / output by optical action. Etc.). The communication control device 106 transmits / receives data to / from the network according to instructions from the CPU 101.
[0198]
FIG. 23 is a diagram for explaining a method for providing a software program or the like according to the present invention. The program according to the present invention is provided by, for example, any one of the following three methods.
[0199]
(a) Provided by being installed in the computer 100. In this case, the program or the like is preinstalled before shipment, for example.
(b) Provided by being stored in a portable recording medium. In this case, the program stored in the portable recording medium 105 is basically installed in the storage device 102 via the recording medium driver 104.
[0200]
(c) Provided by a server on the network. In this case, basically, the computer 100 obtains the program or the like by downloading the program or the like stored in the server. The network includes a wireless network.
[0201]
In the above-described embodiment, resource contention and register leakage are taken as properties to be verified. However, the properties generated by the present invention are not limited to this.
[0202]
Further, although registers, ports, and buses are taken as data resources, the resources targeted by the present invention are not limited to these.
[0203]
【The invention's effect】
According to the present invention, it is possible to automatically generate a property for verifying whether resource conflict or register leakage occurs in the hardware from the specification described in the 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, since the debugging work is reduced, the designer can invest extra work into other work.
[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 specified.
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 optimization processing.
FIG. 5 is an example of hardware.
6 is a diagram for explaining a hierarchical method for describing the hardware shown in FIG. 5; FIG.
FIG. 7 is a diagram illustrating an example of optimizing a data transfer graph using “resource equivalence”.
FIG. 8 is a diagram for explaining “branching”;
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 (No. 5) of hardware specifications described in Verilog.
FIG. 15 is an example (No. 6) of hardware specifications described in Verilog.
FIG. 16 is a data transfer graph generated from the hardware specifications shown in FIGS.
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 property creation processing;
FIG. 20 is an example of an adjacent node list.
FIG. 21 is an example of a “resource conflict” property;
FIG. 22 is an example of a property of “register leak”.
FIG. 23 is an example of a “resource conflict” property in consideration of clock distortion.
FIG. 24 is an example (part 1) of the hardware specification described in Verilog.
FIG. 25 is an example (part 2) of the hardware specification described in Verilog.
FIG. 26 is an example (part 3) of the hardware specification 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 processing for detecting a register file.
FIG. 30 is an example of an optimized data transfer graph.
FIG. 31 is a diagram illustrating conditions used in an optimized graph.
FIG. 32 is a flowchart (No. 1) of a method for generating a data transfer graph;
FIG. 33 is a second flowchart of the method for generating the data transfer graph.
FIG. 34 is a flowchart (No. 3) of the method for generating the data transfer graph;
FIG. 35 is a detailed flowchart of processing for generating a data transfer edge;
FIG. 36 is a first flowchart of a process for detecting “non-fragment equivalence”;
FIG. 37 is a flowchart (part 2) of a process of detecting “non-fragment equivalence”;
FIG. 38 is a first flowchart 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 (No. 3) of a process for detecting “fragment equivalence”;
FIG. 41 is a flowchart (part 4) of a process of detecting “fragment equivalence”;
FIG. 42 is a flowchart of processing for detecting “name equivalence”;
FIG. 43 is a flowchart of processing for detecting a “branch edge”;
FIG. 44 is a flowchart (No. 1) of a process of detecting “equivalent edge”;
FIG. 45 is a flowchart (No. 2) of a process for detecting “equivalent edge”;
FIG. 46 is a flowchart (No. 3) of a process of detecting “equivalent edge”;
FIG. 47 is a flowchart (No. 4) of a process of detecting “equivalent edge”;
FIG. 48 is a flowchart (No. 5) of a process of detecting “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 (No. 1) of a process for detecting a “register file”;
FIG. 53 is a flowchart (No. 2) of a process for detecting a “register file”;
FIG. 54 is a flowchart (No. 3) of the process of detecting “register file”;
FIG. 55 is a flowchart (No. 4) of the process of detecting “register file”;
FIG. 56 is a flowchart (No. 5) of the process of detecting “register file”;
FIG. 57 is a flowchart of processing for creating an adjacent node list.
FIG. 58 is a first flowchart of a process for generating a property script.
FIG. 59 is a flowchart (part 2) of the process for generating a property script;
FIG. 60 is a flowchart (part 3) of the process for generating a property script;
FIG. 61 is a block diagram of a computer that executes a program describing functions of the present invention.
FIG. 62 is a diagram illustrating a method for providing a software program or the like according to the present invention.
[Explanation of symbols]
1 Property generation tool
2 Hardware specifications
3 Verification tools

Claims (13)

A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
When the bit width of each resource corresponding to two nodes adjacent to each other is the same, and one resource is a child of the other resource, the optimization means selects one of those nodes as the data Remove from transfer graph
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
When the data is transferred from the first resource to the second resource and the third resource, and the bit width of the second resource and the third resource is smaller than the bit width of the first resource, Delete the node corresponding to the first resource from the data transfer graph.
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
In the case where the optimization means transfers data from the first resource and the second resource to the third resource, and the bit width of the first resource and the second resource is smaller than the bit width of the third resource And deleting the node corresponding to the third resource from the data transfer graph.
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
When the data is transferred from the register to the output port having the same name as the register, the optimization unit deletes the node corresponding to the output port from the data transfer graph.
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
If the data sent from the first resource is transferred only to the second resource, and the second resource receives only the data transferred from the first resource, the optimization means receives the data sent from the first resource. An edge representing data transfer from one resource to the second resource is deleted from the data transfer graph.
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
If the bits to be transferred between the data transfer from the first resource to the second resource and the data transfer from the first resource to the third resource do not overlap, the optimization means Delete the edge corresponding to the data transfer from the above data transfer graph
A property generation device characterized by that . An apparatus for generating a property to be verified for the hardware, including a data transfer using a hardware multiple described by description language resources and their resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
If the bits to be transferred between the data transfer from the first resource to the second resource and the data transfer from the third resource to the second resource do not overlap, the optimization means Delete the edge corresponding to the data transfer from the above data transfer graph
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
When the plurality of registers belong to the same register file, the optimization means converts a plurality of nodes corresponding to the plurality of registers into one node.
A property generation device characterized by that . The property generation device according to claim 1,
The property generation means generates a property related to at least one of resource contention and register leakage.
A property generation device characterized by that . The property generation device according to claim 1,
When a plurality of fan-in edges are connected to a node, the property generation unit generates a resource contention property based on conditions given to data transfer corresponding to the plurality of fan-in edges.
A property generation device characterized by that . A device for generating properties to be verified for hardware including a plurality of resources described in a hardware description language and data transfer using the resources,
Graph generation means for generating a data transfer graph corresponding to the resource and data transfer described in the hardware description language;
Optimization means for optimizing the data transfer graph generated by the graph generation means;
Using a data transfer graph optimized by the optimization means, property generation means for generating a property to be verified for the hardware described in the hardware description language,
When the fan-in edge and the fan-out edge are connected to a certain node, the property generation unit generates a register leakage property based on conditions given to data transfer corresponding to the edges.
A property generation device characterized by that . 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,
Graph generation means realized by a computer generates a data transfer graph corresponding to the resource and data transfer described in the hardware description language,
The optimization means realized by the computer optimizes the data transfer graph,
The property generation means realized by the computer uses the optimized data transfer graph to generate a property to be verified for the hardware described in the hardware description language,
The graph generation means generates a data transfer graph representing the hardware using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
When the optimization means has the same bit width of each resource corresponding to two nodes adjacent to each other and one resource is a child of the other resource, one of those nodes is treated as the data Remove from transfer graph
A property generation method characterized by that . A recording medium storing a program for generating a plurality of resources described in a hardware description language and a property to be verified for hardware including data transfer using the resources,
The program, a computer,
Means to generate a data transfer graph corresponding to the described resources and data transfer the hardware description language,
Means to optimize the data transfer graph,
The optimized data transfer graph is used to function as a means for generating a property to be verified for hardware described in the hardware description language ,
The graph generation means generates a data transfer graph representing the hardware by using a node corresponding to each resource, and an edge representing a transfer source and a transfer destination of each data transfer,
When the bit width of each resource corresponding to two nodes adjacent to each other is the same, and one resource is a child of the other resource, the optimization means selects one of those nodes as the data Remove from transfer graph
A computer-readable recording medium.

Images