JPH09179897A - Variable exchange method for binary decision graph - Google Patents

Abstract

PROBLEM TO BE SOLVED: To make it possible to exchange two adjacent variables of the binary decision diagram(BDD) at a high speed. SOLUTION: For each pair of variables to be exchanged, a set of nodes whose internal states are updated by variable exchanging and the internal states of the nodes before the update are stored. Then when the variable exchanging is performed for the same variable pair, the variables are exchanged at a high speed by utilizing the stored set of nodes whose internal states are updated by the variable exchanging and the internal states of the nodes before the update.

Description

Detailed Description of the Invention

[0001]

BACKGROUND OF THE INVENTION 1. Field of the Invention The present invention relates to a binary decision graph representing a logical function such as a logic circuit.
gram, sometimes referred to as BDD), for exchanging the order of two adjacent variables.

[0002]

2. Description of the Related Art A binary decision graph has been widely recognized as an efficient method of expressing a logic function, and has been widely used in many logic circuit design support tools such as logic synthesis, logic design verification, and test generation. ing. Since the binary decision graph is described in detail in the following document, detailed description is omitted here.

11 and 12 show examples of binary decision graphs. In either case,

[Expression 1] f (v ₁ , v ₂ , v ₃ , v ₄ ) = v ₁ · v ₃ + v ₂ · v ₄ (1) represents a logical function.

The difference between FIG. 11 and FIG. 12 is the difference in variable ordering. In FIG. 11, {v ₁ , v ₂ , v ₃ ,
While the variable order is v ₄ }, in FIG.
The variable order is ₁ , v ₃ , v ₂ , v ₄ }.
Due to the difference in the variable order, the number of nodes (which will be called the size of the binary decision graph) is different. FIG.
In 1, the size of the binary decision graph is 6, whereas
In FIG. 12, it is 4.

The difference in the number of nodes due to the difference in variable order is
The more complex the logical function to be expressed, the more remarkable it becomes. Therefore, in order to process a complicated logical function efficiently, it is important to find a variable order that reduces the number of nodes.

As one of methods for obtaining a binary decision graph using the variable order and the variable order in which the number of nodes becomes small, after the binary decision graph is created in an appropriate initial variable order, the variable order is slightly changed. There is a method of obtaining a smaller binary decision graph by transforming it by replacing it with each other. As one of the minimization algorithms for such a binary decision graph, shifting (sifti)
ng) algorithm (described in Reference 5). This algorithm can obtain smaller BDDs than other minimization algorithms, but it is known that it takes a long processing time.

The shifting algorithm sorts all variables in descending order of the number of nodes, finds the optimum position for each variable in the sorted order, and moves it to that position. Here, the optimum position of each variable is obtained as follows. The variable of interest is called a shifting variable.

[0008] 1. Swap the shifting variable with the variable immediately below until it becomes the lowest variable. After the exchange of each variable, if the BDD size is the minimum value, the minimum value and its position are stored.

[0009] 2. Next, the shifting variable is exchanged with the variable immediately above until it becomes the top variable. After each variable exchange, B
If the DD size is the minimum value, the minimum value and its position are stored.

3. Finally, the variable immediately below is exchanged until the BDD size reaches the minimum position.

FIG. 13 shows how the variable order changes when the shifting algorithm is applied to find the optimum position of the binary decision graph v ₂ of FIG. FIG. 12 is a binary decision graph of the variable order finally obtained. First,
v ₂ moves downward to the bottom while exchanging with the variable directly below. Next, this time, while moving to the variable immediately above, it moves upward and moves to the top. Finally, while exchanging with the variable directly below, it moves downward and moves to the optimum position (the third position from the top in this example).

In the case of this example, the variable exchange is performed 7 times in total. Some of these variable exchanges are performed on the same pair of variables. For example, with respect to v ₂ and v _3, it is done three times in total, and another variable pair, v ₂
And v ₁ and v ₂ and v ₄ are each performed twice. Thus, the shifting algorithm consists of a series of exchange processing of adjacent variables.

Next, FIG. 10 is a flow chart showing a method for exchanging variables of a binary decision graph used in the above-mentioned shifting algorithm. This flowchart is a process for exchanging the variable v and the variable w immediately below it.

In step S1001, a node in which at least one of the two child nodes is a node of w among the nodes of the shifting variable v is searched for, all such nodes are removed from the unique table, and stored in P. Such a node will be called a pivot node. Then, in step S1003, one node is taken out from P and the node is set to F. At this time, F to P
Delete from.

Subsequently, in step S1004, child nodes F ₁ ′ and F ₀ ′ after variable exchange for F are obtained, and in step S1005 the internal state of the node F (variable, child node).
To a new state (w, F ₁ ′, F ₀ ′), and in step S1006, the rewritten F is registered in the unique table (unique table).

From step S1003 to step S
The process up to 1006 is performed until there is no node stored in P (step S1002).

It should be noted that the main processing in this variable exchange processing is the update of the internal state of the pivot node.

Here, the unique table is a data structure used to prevent nodes having the same child nodes from being created, and all nodes are registered in this unique table. The unique table, for example, gives a variable of a node and two child nodes, checks whether an equivalent node exists, returns the node if it exists, and returns the node if it does not exist. Nodes are created so that nodes can be accessed from variables and child nodes in a fixed time. Also, by dividing the unique table for each variable, it is possible to check all nodes of a certain variable. It can be easily realized by scanning.

Next, FIG. 14 shows an example of a programmatic expression of a conventional variable exchange algorithm. The procedure collect_pivot_node used in this expression example is the same as the procedure find_or_creat in step S1001.
te_new_then_node and find_o
For r_create_new_else_node, the procedure overwrite_node is performed in step S1004.
_State is step S1005, and the procedure add_n
ode_to_unique_table is step S
1006 respectively.

Reference [1] KSBrace, RL Rudell, and REBryant. Efficien
t implementation of a BDD package. In Proc. 27th Des
ign Automation Conference, pages 40-45, June 1990. [2] REBryant. Graph-based algorithms for Boolean
function manipulation.IEEE Trans.Comput., C-35
(8): 677-691, Aug. 1986. [3] M. Fujita, H. Fujisawa, and Y. Matsunaga. Variable
ordering algorithms for ordered binary decision di
agrams and their evaluation.IEEE Trans. Comput.-Ai
ded Des. of Integrated Circuits and Syst., 12 (1): 6-
12, Jan 1993.

[4] S. Malik, ARWang, RK Brayton, and
A. Sangiovanni-Vincentelli. Logic verification usi
ng binary decision diagrams in a logic synthesis e
nvironment. In Proc. International Conference on C
omputer-Aided Design, pages 6-9, Nov.1988. [5] R. Rudell. Dynamic variable ordering for ordere
d binary decision diagrams. In Proc. International
Conference on Computer-Aided Design, pages 42-47,
Nov.1993.

[0022]

The shifting algorithm has a smaller BDD than other algorithms.
It has been proved that the above can be obtained, and it is effective in that respect. But on the other hand, this algorithm
There is a practical problem that the execution time is longer than that of other algorithms, and its speeding up is desired.

Since most of the processing of the shifting algorithm is the variable exchanging process, the speed of the shifting algorithm can be increased by accelerating the variable exchanging process.

In considering the speedup of the variable exchange processing, s
Let's see how variable exchange is performed in the ifing algorithm. As can be seen from the example of FIG. 3, in order to obtain the optimum position for one shifting variable, it is necessary to perform variable exchange three times for one variable pair in the worst case. Here, it should be noted that the binary decision graphs are exactly the same immediately before the first variable exchanging process and immediately after the second variable exchanging process, and immediately after the first variable exchanging process. Even just before the second variable exchange process, the binary decision graph should be exactly the same. That is, it can be said that the first and second variable exchanging processes are reverse processes and are reversible. The first and third variable exchanging processes are exactly the same.

As described above, in the shifting algorithm, the variable exchanging process is performed a plurality of times for the same variable set, and the variable exchanging processes have an inverse or the same relation. However, the conventional variable exchange method does not consider such a matter.

The present invention has been made in view of the above circumstances, and an object of the present invention is to provide a variable after the second time when reversible variable exchange is performed a plurality of times for the same set of variables. An object of the present invention is to provide a method for exchanging variables in a binary decision graph, which enables the exchange to be executed at high speed.

[0027]

In order to achieve the above object, a feature of the first invention is a method of exchanging variables of a binary decision graph representing a logical function, in which two adjacent binary decision graphs are connected. When exchanging two variables, the internal state of the node before the update is stored for each node whose internal state is updated by the variable exchange, and when exchanging the two variables again, The variable exchange is performed by storing the internal state of the node before update stored at that time as the internal state of the new node and storing the internal state of the current node as the internal state of the node before update.

Further, a feature of the second invention is that in a method of exchanging variables of a binary decision graph expressing a logical function,
When exchanging adjacent variables of the binary decision graph, a set of nodes whose internal states are updated by the variable exchange is stored, and when exchanging the two variables again, the previous variable exchange is performed. The variable exchange is performed by updating the internal state of each node included in the stored set of nodes.

In the above invention, when the variable exchange of the same two adjacent variable sets is performed a plurality of times, the second and subsequent variable exchanges are performed at high speed.

At the time of the first variable exchange of the same pair of two adjacent variables, the set of nodes whose internal state is changed is stored, and the state before the change is stored. By doing so, the second and subsequent variable exchanges can be performed at high speed.

First, it is necessary to find a node whose internal state should be changed, but the set of nodes whose internal state is changed may be used as it is in the first variable exchange. This is because the nodes whose internal states are changed are exactly the same even in the second and subsequent variable exchanges.

In the process of obtaining the set of nodes whose internal states are changed, in the conventional technique, it is necessary to check all the nodes of the upper variable of the two variables to be exchanged, and the number of nodes of the upper variable is calculated. If n, it is necessary to calculate O (n). However, in the present invention, since it has already been calculated for the first time, this part does not need to be calculated.

Next, the internal state is changed for the node whose internal state needs to be changed. At that time, the internal state of the node before the change of the previous variable exchange is used. That is, the internal state of the node is updated to the retained internal state of the node before the change, and at the same time, the internal state of the node before the change is stored and retained for the next variable exchange. In other words, the internal state of the node before the change in the previous variable exchange held and the internal state of the current node are exchanged. Also, if both the internal state before conversion and the internal state after conversion are held separately from the current internal state, the variable exchange process will be performed on the two internal states that hold the current internal state. Just replace it with one of the internal states.

In the conventional technique, the process of updating the internal state of a node is a process of obtaining a child node after variable exchange, and a process of obtaining a cofactor, a process of determining whether an equivalent node exists, and the like are used to access a unique table. However, in the present invention, since the child node after the variable exchange is already held, the process for obtaining the child node is unnecessary, and the process can be performed at a high speed.

[0035]

BEST MODE FOR CARRYING OUT THE INVENTION Embodiments of a variable exchange method for a binary decision graph according to the present invention will be described in detail below with reference to the drawings.

In this embodiment, an ordinary computer system will be used. The hardware configuration of this computer system includes a CPU for performing various processes,
An input device such as a keyboard, a mouse, a light pen, or a flexible disk device, an external storage device such as a memory device or a disk device, and an output device such as a display device or a printer device are provided. The CPU is
An arithmetic unit that executes various instructions and a main storage unit that stores the instructions are provided.

Here, in the present embodiment, it is assumed that it is executed as shown in the shifting algorithm shown in FIG. 13. The description of this shifting algorithm is the same as that described above, and therefore its explanation is omitted.

FIG. 1 is a flow chart showing a method of exchanging variables for a binary decision graph of this embodiment. This flowchart represents the variable exchange process used in the shifting algorithm, and the shifting variable v and the variable w immediately below v are exchanged. In this flow chart, the set of pivot nodes for the exchange of the set of variables (v, w) is the data structure w. I try to save it in P. Usually, this data structure is preferably a linked list structure.

Although not shown, when the shifting variable w and the variable v immediately above w are exchanged, the set of pivot nodes for the exchange of the set of variables (v, w) is
data structure belonging to v Save it in P. The flowchart of FIG. 1 will be described below.

First, in step S101, it is determined whether or not it is the first variable exchange for v and w. If it is the first variable exchange, the process proceeds to step S102. Step S102
Then, among the nodes of the shifting variable v, at least one child node is a node of w (a pivot node
Nodes) and w. Store in P.

Succeedingly, in a step S103, w. It is determined whether or not there is an unprocessed node among the nodes stored in P. In step S104, this w. Select one unprocessed node stored in P. For convenience of the following description, this selected node is designated as F. Step S105
Then, the internal state of the selected node in step S104 is saved.

Succeedingly, in a step S106, child nodes F ₁ ′ and F ₀ ′ after the variable exchange with respect to F are obtained, and in a step S107, the node state of F is (w, F ₁ ′, F).
Rewrite as ₀ ').

Steps S104 to S1 described above
07 to w. The process is repeated until there are no nodes stored in P (step S103).

Here, in the case of the first variable exchange, the processing is similar to the variable exchange shown in the conventional example, but in the case of the variable exchange in the present embodiment, the pivot node is replaced by
w. It is different from the conventional variable exchange in that it is stored in P and that the pivot node is not returned to the unique table even after the internal state of the pivot node is updated.

On the other hand, in step S102, if it is not the first variable exchange for v and w, that is, if it is the second and subsequent variable exchanges, step S108 and the subsequent steps are executed. First, in step S108, w. Among the nodes stored in P, it is judged whether there is an unprocessed node, and w.
Select one unprocessed node stored in P (step S
109). Then w. For all pivot nodes stored in P, the internal state before the previous variable exchange and the current internal state are exchanged (step S110).

Next, the variable exchanging method of the binary decision graph of this embodiment will be described using a concrete example. FIG. 2 is a binary decision graph used to describe a specific example of this embodiment. This binary decision graph is the same as that used in the conventional example, but for convenience of explanation, A, B, ...
The alphabets up to F are attached. Here, FIG.
Of the variable exchanges shown in No. 3, the first four will be described.

FIG. 3A is a diagram showing the binary decision graph shown in FIG. For example, in node A, the variable is v
₁ indicates that the child nodes are B and C. Further, this state is the state before the variable exchange and there is no child node before the update, so nothing is shown. Further, FIG. 6B is a diagram showing the relationship between each variable and the node. For example, it indicates that the nodes registered in the unique table of the variable v ₂ are B and C. here,
The column P indicates a set of pivot nodes at the time of exchanging variables with the shifting variable v ₂ .

Next, regarding this FIG. 3A, v ₂ and v ₃
The variables are exchanged with the following procedure. Since this variable exchange is the first exchange, step S10 in the flowchart of FIG.
In case 1, the procedure proceeds to “YES”. In the variable exchange this time, v in step S101 is v ₂ ,
w is v ₃ .

Find the pivot node of v ₂ v ₃ . P
Save (step S102) v _3. The internal state of the node P = {B} B is saved, that is, the child nodes D and E are saved as the child nodes before updating (step S105). The child node after the variable exchange of B is obtained (step S10).
6) Rewrite the internal state of the node of F ₁ ′ = 1 F ₀ ′ = C B to (v ₃ , 1, C) (step S107) v ₃ .. Since P is only B ends in this v _3. P is left as it is for the next variable exchange. The state after the exchange of v ₂ and v _{3 by} the above procedure is shown in FIG. 4 (a). Where D was a child node
And E are stored in the child node before the update, and the newly calculated node is stored in the child node column. In this case 1 and C. In addition, "*" in the figure means a dead node (a node that is not used, the same applies below). In the same figure (b), the node B changes the variable v by the variable exchange.
_It is stored in the P column of the variable v ₃ by exchanging ₂ with the variable v ₃ and deleted from the unique table of the variable v ₂ .

Next, FIG. 5A is a chart showing the state after the exchange of v ₂ and v ₄ . Since this variable exchange is the first exchange, step S10 in the flowchart of FIG.
In case 1, the procedure proceeds to “YES”. In the variable exchange this time, v in step S101 is v ₂ ,
w is v ₄ .

Here, the child nodes F and 0 are stored in the child node before updating, and the newly calculated node is stored in the child node column. In this case G and 0. However, the node G is a newly created node, the variable is v ₂ , and “1” and “0” are child nodes. In the same figure (b), the node C has variables v ₂ and v due to variable exchange.
_It is stored in the P column of the variable v ₄ by the exchange with _4, and the variable v
It has been removed from the ₂ unique tables. Also, the newly added node G is added to v ₂ .

Next, FIG. 6A is a chart showing the state after the exchange of v ₄ and v ₂ . Since this variable exchange is the second exchange, step S1 in the flowchart of FIG.
At 01, the process proceeds to “NO”. In the variable exchange this time, v in step S101 is v ₄ ,
w is v ₂ .

Here, G and 0 which are child nodes are stored in the child node before updating, and F and 0 which are stored in the child node before updating are stored in the child node column. That is, the child node is exchanged with the child node before the update.

Next, regarding this FIG. 6A, v ₃ and v ₂
The variables are exchanged with the following procedure. Since this variable exchange is the second exchange, step S1 in the flowchart of FIG.
At 01, the process proceeds to “NO”.

Already v ₃ . P = {B} (step S102) B is (v ₃ , 1, C, D, E) where 1 and C are the current child nodes, and D and E are the pre-update child nodes. The internal state of the B node is exchanged (step S11).
0) B = (v ₂ , D, E, 1, C) v ₃ . Since P is only B, end v ₃ . P is left as it is for the next variable exchange. FIG. 7A is a chart showing the state after the exchange of v ₃ and v ₂ . Here, G and 0 which are the child nodes before the update are stored in the child node before the update, and F and 0 shown in the column of the child node before the update are stored in the child node column. That is, the values of the child node and the previous child node are exchanged. In the same figure (b), the node B changes the variable v
_It is stored in the P column of the variable v ₃ by exchanging ₂ with the variable v ₃ and deleted from the unique table of the variable v ₂ .

Although description of the subsequent variable exchange is omitted, the internal state of the node before the update is stored for each node in this way, and when the two variables are exchanged again, the previous variable exchange is performed. The variable exchange is performed by storing the internal state of the node stored at that time as the internal state of the new node and storing the internal state of the current node as the internal state of the node before the update. As a result, the second and subsequent variable exchanges can be executed at high speed.

Next, FIG. 8 shows a programmatic expression example of the variable exchange method of the binary decision graph used in the present embodiment.

The procedure coll used in this expression example
ect_pivot_node is set to step S102,
The procedure save_node_state is step S10.
5, the procedure find_or_create_new_t
hen_node and find_or_create
_New_else_node is set in step S106,
The procedure overwrite_node_state proceeds to step S107, where the procedure exchange_node_s.
The state corresponds to step S110.

The distinction between the first variable exchange and the second and subsequent variable exchanges is made by w. It is performed depending on whether or not the data of P already exists. Also, si of v
At the end of the fting, all pivot nodes that have been fetched from the unique table need to be returned to the unique table.

FIG. 9 shows a comparison result between the case of using this embodiment and the case of using the conventional technique. This result was required for the dynamic variable reordering when the dynamic variable reordering using the sifting algorithm was applied when the process of creating the binary decision graph was simultaneously performed on all the outputs of the combinational circuit. The execution time (prior art and the present invention) and the speed-up rate according to the present invention are shown. From this comparison result, if the variable exchanging method of the binary decision graph according to the present invention is used, 1.
It can be seen that a speedup of 9 to 7.9 times can be achieved.

[0061]

As described above, according to the variable exchanging method for a binary decision graph according to the present invention, the variable exchanging for the same variable pair can be executed at high speed for the second and subsequent variable exchanging. It will be possible.

[Brief description of the drawings]

FIG. 1 is a flowchart of a variable exchange method for a binary decision graph according to the present invention.

FIG. 2 is a diagram showing an example of a binary decision graph.

FIG. 3 is a diagram showing a first state of a binary decision graph.

FIG. 4 is a diagram showing a state after exchanging v ₂ and v ₃ .

FIG. 5 is a diagram showing a state after exchanging v ₂ and v ₄ .

FIG. 6 is a diagram showing a state after exchanging v ₄ and v ₂ .

FIG. 7 is a diagram showing a state after exchanging v ₃ and v ₂ .

FIG. 8 is a diagram showing an example of a program according to the embodiment of the present invention.

FIG. 9 is a chart showing a comparison between the present invention and the prior art.

FIG. 10 is a flowchart showing a conventional method of exchanging variables for a binary decision graph.

FIG. 11 is a diagram showing an example of a binary decision graph.

FIG. 12 is a diagram showing an example of a binary decision graph.

FIG. 13 is a diagram showing a change in variable order when a shifting algorithm is executed.

FIG. 14 is a diagram showing a program example of a variable exchange method according to a conventional technique.

Claims (2)

[Claims] 1. A method for exchanging variables of a binary decision graph representing a logical function, wherein when an adjacent two variables of the binary decision graph are exchanged, an internal state is updated by the variable exchange. For each node, the internal state of the node before the update is stored, and when the two variables are exchanged again, the internal state of the node before the update stored at the previous variable exchange is set as the internal state of the new node, A variable exchanging method for a binary decision graph, characterized in that variable exchanging is performed by storing an internal state of a current node as an internal state of a node before updating. 2. A method for exchanging variables of a binary decision graph representing a logical function, wherein, when two adjacent variables of the binary decision graph are exchanged, an internal state is updated by the variable exchange. When the two variables are exchanged again, the variable exchange is performed by updating the internal state of each node included in the set of the nodes stored in the previous variable exchange. A method for exchanging variables in a binary decision graph, which is characterized in that