ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
reoTransfer.c File Reference
#include "reo.h"
Include dependency graph for reoTransfer.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START reo_unitreoTransferNodesToUnits_rec (reo_man *p, DdNode *F)
 DECLARATIONS ///.
 
DdNode * reoTransferUnitsToNodes_rec (reo_man *p, reo_unit *pUnit)
 

Function Documentation

◆ reoTransferNodesToUnits_rec()

ABC_NAMESPACE_IMPL_START reo_unit * reoTransferNodesToUnits_rec ( reo_man * p,
DdNode * F )

DECLARATIONS ///.

CFile****************************************************************

FileName [reoTransfer.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Transfering a DD from the CUDD manager into REO"s internal data structures and back.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id
reoTransfer.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Transfers the DD into the internal reordering data structure.]

Description [It is important that the hash table is lossless.]

SideEffects []

SeeAlso []

Definition at line 43 of file reoTransfer.c.

44{
45 DdManager * dd = p->dd;
46 reo_unit * pUnit;
47 int HKey = -1; // Suppress "might be used uninitialized"
48 int fComp;
49
50 fComp = Cudd_IsComplement(F);
51 F = Cudd_Regular(F);
52
53 // check the hash-table
54 if ( F->ref != 1 )
55 {
56 // search cache - use linear probing
57 for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
58 if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
59 {
60 pUnit = p->HTable[HKey].Arg2;
61 assert( pUnit );
62 // increment the edge counter
63 pUnit->n++;
64 return Unit_NotCond( pUnit, fComp );
65 }
66 }
67 // the entry in not found in the cache
68
69 // create a new entry
70 pUnit = reoUnitsGetNextUnit( p );
71 pUnit->n = 1;
72 if ( cuddIsConstant(F) )
73 {
74 pUnit->lev = REO_CONST_LEVEL;
75 pUnit->pE = (reo_unit*)(ABC_PTRUINT_T)(cuddV(F));
76 pUnit->pT = NULL;
77 // check if the diagram that is being reordering has complement edges
78 if ( F != dd->one )
79 p->fThisIsAdd = 1;
80 // insert the unit into the corresponding plane
81 reoUnitsAddUnitToPlane( &(p->pPlanes[p->nSupp]), pUnit ); // increments the unit counter
82 }
83 else
84 {
85 pUnit->lev = p->pMapToPlanes[F->index];
86 pUnit->pE = reoTransferNodesToUnits_rec( p, cuddE(F) );
87 pUnit->pT = reoTransferNodesToUnits_rec( p, cuddT(F) );
88 // insert the unit into the corresponding plane
89 reoUnitsAddUnitToPlane( &(p->pPlanes[pUnit->lev]), pUnit ); // increments the unit counter
90 }
91
92 // add to the hash table
93 if ( F->ref != 1 )
94 {
95 // the next free entry is already found - it is pointed to by HKey
96 // while we traversed the diagram, the hash entry to which HKey points,
97 // might have been used. Make sure that its signature is different.
98 for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
99 p->HTable[HKey].Sign = p->Signature;
100 p->HTable[HKey].Arg1 = (reo_unit *)F;
101 p->HTable[HKey].Arg2 = pUnit;
102 }
103
104 // increment the counter of nodes
105 p->nNodesCur++;
106 return Unit_NotCond( pUnit, fComp );
107}
Cube * p
Definition exorList.c:222
#define hashKey2(a, b, TSIZE)
Definition extraBdd.h:86
ABC_NAMESPACE_IMPL_START reo_unit * reoTransferNodesToUnits_rec(reo_man *p, DdNode *F)
DECLARATIONS ///.
Definition reoTransfer.c:43
#define Unit_NotCond(u, c)
Definition reo.h:176
#define REO_CONST_LEVEL
Definition reo.h:40
void reoUnitsAddUnitToPlane(reo_plane *pPlane, reo_unit *pUnit)
Definition reoUnits.c:135
reo_unit * reoUnitsGetNextUnit(reo_man *p)
FUNCTION DEFINITIONS ///.
Definition reoUnits.c:45
struct _reo_unit reo_unit
DATA STRUCTURES ///.
Definition reo.h:60
short lev
Definition reo.h:68
short n
Definition reo.h:71
reo_unit * pE
Definition reo.h:74
reo_unit * pT
Definition reo.h:75
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ reoTransferUnitsToNodes_rec()

DdNode * reoTransferUnitsToNodes_rec ( reo_man * p,
reo_unit * pUnit )

Function*************************************************************

Synopsis [Creates the DD from the internal reordering data structure.]

Description [It is important that the hash table is lossless.]

SideEffects []

SeeAlso []

Definition at line 120 of file reoTransfer.c.

121{
122 DdManager * dd = p->dd;
123 DdNode * bRes, * E, * T;
124 int HKey = -1; // Suppress "might be used uninitialized"
125 int fComp;
126
127 fComp = Cudd_IsComplement(pUnit);
128 pUnit = Unit_Regular(pUnit);
129
130 // check the hash-table
131 if ( pUnit->n != 1 )
132 {
133 for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
134 if ( p->HTable[HKey].Arg1 == pUnit )
135 {
136 bRes = (DdNode*) p->HTable[HKey].Arg2;
137 assert( bRes );
138 return Cudd_NotCond( bRes, fComp );
139 }
140 }
141
142 // treat the case of constants
143 if ( Unit_IsConstant(pUnit) )
144 {
145 bRes = cuddUniqueConst( dd, ((double)((int)(ABC_PTRUINT_T)(pUnit->pE))) );
146 cuddRef( bRes );
147 }
148 else
149 {
150 // split and recur on children of this node
151 E = reoTransferUnitsToNodes_rec( p, pUnit->pE );
152 if ( E == NULL )
153 return NULL;
154 cuddRef(E);
155
156 T = reoTransferUnitsToNodes_rec( p, pUnit->pT );
157 if ( T == NULL )
158 {
159 Cudd_RecursiveDeref(dd, E);
160 return NULL;
161 }
162 cuddRef(T);
163
164 // consider the case when Res0 and Res1 are the same node
165 assert( E != T );
166 assert( !Cudd_IsComplement(T) );
167
168 bRes = cuddUniqueInter( dd, p->pMapToDdVarsFinal[pUnit->lev], T, E );
169 if ( bRes == NULL )
170 {
171 Cudd_RecursiveDeref(dd,E);
172 Cudd_RecursiveDeref(dd,T);
173 return NULL;
174 }
175 cuddRef( bRes );
176 cuddDeref( E );
177 cuddDeref( T );
178 }
179
180 // do not keep the result if the ref count is only 1, since it will not be visited again
181 if ( pUnit->n != 1 )
182 {
183 // while we traversed the diagram, the hash entry to which HKey points,
184 // might have been used. Make sure that its signature is different.
185 for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
186 p->HTable[HKey].Sign = p->Signature;
187 p->HTable[HKey].Arg1 = pUnit;
188 p->HTable[HKey].Arg2 = (reo_unit *)bRes;
189
190 // add the DD to the referenced DD list in order to be able to store it in cache
191 p->pRefNodes[p->nRefNodes++] = bRes; Cudd_Ref( bRes );
192 // no need to do this, because the garbage collection will not take bRes away
193 // it is held by the diagram in the making
194 }
195 // increment the counter of nodes
196 p->nNodesCur++;
197 cuddDeref( bRes );
198 return Cudd_NotCond( bRes, fComp );
199}
DdNode * reoTransferUnitsToNodes_rec(reo_man *p, reo_unit *pUnit)
#define Unit_IsConstant(u)
Definition reo.h:177
#define Unit_Regular(u)
Definition reo.h:174
Here is the call graph for this function:
Here is the caller graph for this function: