ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
reoTest.c
Go to the documentation of this file.
1
18
19#include "reo.h"
20
22
23
27
31
43void Extra_ReorderTest( DdManager * dd, DdNode * Func )
44{
45 reo_man * pReo;
46 DdNode * Temp, * Temp1;
47 int pOrder[1000];
48
49 pReo = Extra_ReorderInit( 100, 100 );
50
51//Extra_DumpDot( dd, &Func, 1, "beforReo.dot", 0 );
52 Temp = Extra_Reorder( pReo, dd, Func, pOrder ); Cudd_Ref( Temp );
53//Extra_DumpDot( dd, &Temp, 1, "afterReo.dot", 0 );
54
55 Temp1 = Extra_ReorderCudd(dd, Func, NULL ); Cudd_Ref( Temp1 );
56printf( "Initial = %d. Final = %d. Cudd = %d.\n", Cudd_DagSize(Func), Cudd_DagSize(Temp), Cudd_DagSize(Temp1) );
57 Cudd_RecursiveDeref( dd, Temp1 );
58 Cudd_RecursiveDeref( dd, Temp );
59
60 Extra_ReorderQuit( pReo );
61}
62
63
75void Extra_ReorderTestArray( DdManager * dd, DdNode * Funcs[], int nFuncs )
76{
77 reo_man * pReo;
78 DdNode * FuncsRes[1000];
79 int pOrder[1000];
80 int i;
81
82 pReo = Extra_ReorderInit( 100, 100 );
83 Extra_ReorderArray( pReo, dd, Funcs, FuncsRes, nFuncs, pOrder );
84 Extra_ReorderQuit( pReo );
85
86printf( "Initial = %d. Final = %d.\n", Cudd_SharingSize(Funcs,nFuncs), Cudd_SharingSize(FuncsRes,nFuncs) );
87
88 for ( i = 0; i < nFuncs; i++ )
89 Cudd_RecursiveDeref( dd, FuncsRes[i] );
90
91}
92
109DdNode * Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermuteReo[] )
110{
111 static DdManager * ddReorder = NULL;
112 static int * Permute = NULL;
113 static int * PermuteReo1 = NULL;
114 static int * PermuteReo2 = NULL;
115 DdNode * aFuncReorder, * aFuncNew;
116 int lev, var;
117
118 // start the reordering manager
119 if ( ddReorder == NULL )
120 {
121 Permute = ABC_ALLOC( int, dd->size );
122 PermuteReo1 = ABC_ALLOC( int, dd->size );
123 PermuteReo2 = ABC_ALLOC( int, dd->size );
124 ddReorder = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
125 Cudd_AutodynDisable(ddReorder);
126 }
127
128 // determine the permutation of variable to make sure that var order in bFunc
129 // will not change when this function is transfered into the new manager
130 for ( lev = 0; lev < dd->size; lev++ )
131 {
132 Permute[ dd->invperm[lev] ] = ddReorder->invperm[lev];
133 PermuteReo1[ ddReorder->invperm[lev] ] = dd->invperm[lev];
134 }
135 // transfer this function into the new manager in such a way that ordering of vars does not change
136 aFuncReorder = Extra_TransferPermute( dd, ddReorder, aFunc, Permute ); Cudd_Ref( aFuncReorder );
137// assert( Cudd_DagSize(aFunc) == Cudd_DagSize(aFuncReorder) );
138
139 // perform the reordering
140printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) );
141 Cudd_ReduceHeap( ddReorder, CUDD_REORDER_SYMM_SIFT, 1 );
142printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) );
143
144 // determine the reverse variable permutation
145 for ( lev = 0; lev < dd->size; lev++ )
146 {
147 Permute[ ddReorder->invperm[lev] ] = dd->invperm[lev];
148 PermuteReo2[ dd->invperm[lev] ] = ddReorder->invperm[lev];
149 }
150
151 // transfer this function into the new manager in such a way that ordering of vars does not change
152 aFuncNew = Extra_TransferPermute( ddReorder, dd, aFuncReorder, Permute ); Cudd_Ref( aFuncNew );
153// assert( Cudd_DagSize(aFuncNew) == Cudd_DagSize(aFuncReorder) );
154 Cudd_RecursiveDeref( ddReorder, aFuncReorder );
155
156 // derive the resulting variable ordering
157 if ( pPermuteReo )
158 for ( var = 0; var < dd->size; var++ )
159 pPermuteReo[var] = PermuteReo1[ PermuteReo2[var] ];
160
161 Cudd_Deref( aFuncNew );
162 return aFuncNew;
163}
164
165
180int Extra_bddReorderTest( DdManager * dd, DdNode * bF )
181{
182 static DdManager * s_ddmin;
183 DdNode * bFmin;
184 int nNodes;
185// abctime clk1;
186
187 if ( s_ddmin == NULL )
188 s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
189
190// Cudd_ShuffleHeap( s_ddmin, dd->invperm );
191
192// clk1 = Abc_Clock();
193 bFmin = Cudd_bddTransfer( dd, s_ddmin, bF ); Cudd_Ref( bFmin );
194 Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1);
195// Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
196 nNodes = Cudd_DagSize( bFmin );
197 Cudd_RecursiveDeref( s_ddmin, bFmin );
198
199// printf( "Classical variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
200 return nNodes;
201}
202
217int Extra_addReorderTest( DdManager * dd, DdNode * aF )
218{
219 static DdManager * s_ddmin;
220 DdNode * bF;
221 DdNode * bFmin;
222 DdNode * aFmin;
223 int nNodesBeg;
224 int nNodesEnd;
225 abctime clk1;
226
227 if ( s_ddmin == NULL )
228 s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
229
230// Cudd_ShuffleHeap( s_ddmin, dd->invperm );
231
232 clk1 = Abc_Clock();
233 bF = Cudd_addBddPattern( dd, aF ); Cudd_Ref( bF );
234 bFmin = Cudd_bddTransfer( dd, s_ddmin, bF ); Cudd_Ref( bFmin );
235 Cudd_RecursiveDeref( dd, bF );
236 aFmin = Cudd_BddToAdd( s_ddmin, bFmin ); Cudd_Ref( aFmin );
237 Cudd_RecursiveDeref( s_ddmin, bFmin );
238
239 nNodesBeg = Cudd_DagSize( aFmin );
240 Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1);
241// Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
242 nNodesEnd = Cudd_DagSize( aFmin );
243 Cudd_RecursiveDeref( s_ddmin, aFmin );
244
245 printf( "Classical reordering of ADDs: Before = %d. After = %d.\n", nNodesBeg, nNodesEnd );
246 printf( "Classical variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
247 return nNodesEnd;
248}
249
250
254
256
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
int Extra_bddReorderTest(DdManager *dd, DdNode *bF)
Definition reoTest.c:180
DdNode * Extra_ReorderCudd(DdManager *dd, DdNode *aFunc, int pPermuteReo[])
Definition reoTest.c:109
void Extra_ReorderTestArray(DdManager *dd, DdNode *Funcs[], int nFuncs)
Definition reoTest.c:75
int Extra_addReorderTest(DdManager *dd, DdNode *aF)
Definition reoTest.c:217
ABC_NAMESPACE_IMPL_START void Extra_ReorderTest(DdManager *dd, DdNode *Func)
DECLARATIONS ///.
Definition reoTest.c:43
struct _reo_man reo_man
Definition reo.h:63
void Extra_ReorderQuit(reo_man *p)
Definition reoApi.c:79
DdNode * Extra_Reorder(reo_man *p, DdManager *dd, DdNode *Func, int *pOrder)
Definition reoApi.c:262
void Extra_ReorderArray(reo_man *p, DdManager *dd, DdNode *Funcs[], DdNode *FuncsRes[], int nFuncs, int *pOrder)
Definition reoApi.c:283
reo_man * Extra_ReorderInit(int nDdVarsMax, int nNodesMax)
FUNCTION DECLARATIONS ///.
Definition reoApi.c:50