1 /**CFile****************************************************************
2
3 FileName [casCore.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
8
9 Synopsis [Entrance into the implementation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - Spring 2002.]
16
17 Revision [$Id: casCore.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24
25 #include "base/main/main.h"
26 #include "base/cmd/cmd.h"
27 #include "bdd/extrab/extraBdd.h"
28 #include "cas.h"
29
30 ABC_NAMESPACE_IMPL_START
31
32
33 ////////////////////////////////////////////////////////////////////////
34 /// static functions ///
35 ////////////////////////////////////////////////////////////////////////
36
37 DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose );
38 DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc );
39 DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew );
40
41 extern int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose );
42
43 void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName );
44
45 DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
46
47 ////////////////////////////////////////////////////////////////////////
48 /// static varibles ///
49 ////////////////////////////////////////////////////////////////////////
50
51 //static FILE * pTable = NULL;
52 //static long s_RemappingTime = 0;
53
54 ////////////////////////////////////////////////////////////////////////
55 /// debugging macros ///
56 ////////////////////////////////////////////////////////////////////////
57
58 #define PRD(p) printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 )
59 #define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
60 #define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
61 #define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
62
63
64 ////////////////////////////////////////////////////////////////////////
65 /// EXTERNAL FUNCTIONS ///
66 ////////////////////////////////////////////////////////////////////////
67
68 /**Function*************************************************************
69
70 Synopsis []
71
72 Description []
73
74 SideEffects []
75
76 SeeAlso []
77
78 ***********************************************************************/
Abc_CascadeExperiment(char * pFileGeneric,DdManager * dd,DdNode ** pOutputs,int nInputs,int nOutputs,int nLutSize,int fCheck,int fVerbose)79 int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose )
80 {
81 int i;
82 int nVars = nInputs;
83 int nOuts = nOutputs;
84 abctime clk1;
85
86 int nVarsEnc; // the number of additional variables to encode outputs
87 DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
88
89 int nNames; // the total number of all inputs
90 char * pNames[MAXINPUTS]; // the temporary storage for the input (and output encoding) names
91
92 DdNode * aFunc; // the encoded 0-1 BDD containing all the outputs
93
94 char FileNameIni[100];
95 char FileNameFin[100];
96 char Buffer[100];
97
98
99 //pTable = fopen( "stats.txt", "a+" );
100 //fprintf( pTable, "%s ", pFileGeneric );
101 //fprintf( pTable, "%d ", nVars );
102 //fprintf( pTable, "%d ", nOuts );
103
104
105 // assign the file names
106 strcpy( FileNameIni, pFileGeneric );
107 strcat( FileNameIni, "_ENC.blif" );
108
109 strcpy( FileNameFin, pFileGeneric );
110 strcat( FileNameFin, "_LUT.blif" );
111
112
113 // create the variables to encode the outputs
114 nVarsEnc = Abc_Base2Log( nOuts );
115 for ( i = 0; i < nVarsEnc; i++ )
116 pbVarsEnc[i] = Cudd_bddNewVarAtLevel( dd, i );
117
118
119 // store the input names
120 nNames = nVars + nVarsEnc;
121 for ( i = 0; i < nVars; i++ )
122 {
123 // pNames[i] = Extra_UtilStrsav( pFunc->pInputNames[i] );
124 sprintf( Buffer, "pi%03d", i );
125 pNames[i] = Extra_UtilStrsav( Buffer );
126 }
127 // set the encoding variable name
128 for ( ; i < nNames; i++ )
129 {
130 sprintf( Buffer, "OutEnc_%02d", i-nVars );
131 pNames[i] = Extra_UtilStrsav( Buffer );
132 }
133
134
135 // print the variable order
136 // printf( "\n" );
137 // printf( "Variable order is: " );
138 // for ( i = 0; i < dd->size; i++ )
139 // printf( " %d", dd->invperm[i] );
140 // printf( "\n" );
141
142 // derive the single-output function
143 clk1 = Abc_Clock();
144 aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose ); Cudd_Ref( aFunc );
145 // aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( aFunc );
146 // if ( fVerbose )
147 // printf( "Single-output function computation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
148
149 //fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) );
150 //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) );
151
152 // dispose of the multiple-output function
153 // Extra_Dissolve( pFunc );
154
155 // reorder the single output function
156 // if ( fVerbose )
157 // printf( "Reordering variables...\n");
158 clk1 = Abc_Clock();
159 // if ( fVerbose )
160 // printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) );
161 // Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1);
162 Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
163 Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
164 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
165 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
166 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
167 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
168 if ( fVerbose )
169 printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) );
170 if ( fVerbose )
171 printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
172 // printf( "\n" );
173 // printf( "Variable order is: " );
174 // for ( i = 0; i < dd->size; i++ )
175 // printf( " %d", dd->invperm[i] );
176 // printf( "\n" );
177 //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
178 //fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) );
179
180 // write the single-output function into BLIF for verification
181 clk1 = Abc_Clock();
182 if ( fCheck )
183 WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
184 // if ( fVerbose )
185 // printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
186
187 /*
188 ///////////////////////////////////////////////////////////////////
189 // verification of single output function
190 clk1 = Abc_Clock();
191 {
192 BFunc g_Func;
193 DdNode * aRes;
194
195 g_Func.dd = dd;
196 g_Func.FileInput = Extra_UtilStrsav(FileNameIni);
197
198 if ( Extra_ReadFile( &g_Func ) == 0 )
199 {
200 printf( "\nSomething did not work out while reading the input file for verification\n");
201 Extra_Dissolve( &g_Func );
202 return;
203 }
204
205 aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] ); Cudd_Ref( aRes );
206
207 if ( aRes != aFunc )
208 printf( "\nVerification FAILED!\n");
209 else
210 printf( "\nVerification okay!\n");
211
212 Cudd_RecursiveDeref( dd, aRes );
213
214 // delocate
215 Extra_Dissolve( &g_Func );
216 }
217 printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
218 ///////////////////////////////////////////////////////////////////
219 */
220
221 if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) )
222 return 0;
223
224 /*
225 ///////////////////////////////////////////////////////////////////
226 // verification of the decomposed LUT network
227 clk1 = Abc_Clock();
228 {
229 BFunc g_Func;
230 DdNode * aRes;
231
232 g_Func.dd = dd;
233 g_Func.FileInput = Extra_UtilStrsav(FileNameFin);
234
235 if ( Extra_ReadFile( &g_Func ) == 0 )
236 {
237 printf( "\nSomething did not work out while reading the input file for verification\n");
238 Extra_Dissolve( &g_Func );
239 return;
240 }
241
242 aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] ); Cudd_Ref( aRes );
243
244 if ( aRes != aFunc )
245 printf( "\nFinal verification FAILED!\n");
246 else
247 printf( "\nFinal verification okay!\n");
248
249 Cudd_RecursiveDeref( dd, aRes );
250
251 // delocate
252 Extra_Dissolve( &g_Func );
253 }
254 printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
255 ///////////////////////////////////////////////////////////////////
256 */
257
258 // verify the results
259 if ( fCheck )
260 {
261 char Command[300];
262 sprintf( Command, "cec %s %s", FileNameIni, FileNameFin );
263 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
264 }
265
266 Cudd_RecursiveDeref( dd, aFunc );
267
268 // release the names
269 for ( i = 0; i < nNames; i++ )
270 ABC_FREE( pNames[i] );
271
272
273 //fprintf( pTable, "\n" );
274 //fclose( pTable );
275
276 return 1;
277 }
278
279 #if 0
280
281 /**Function*************************************************************
282
283 Synopsis []
284
285 Description []
286
287 SideEffects []
288
289 SeeAlso []
290
291 ***********************************************************************/
292 void Experiment2( BFunc * pFunc )
293 {
294 int i, x, RetValue;
295 int nVars = pFunc->nInputs;
296 int nOuts = pFunc->nOutputs;
297 DdManager * dd = pFunc->dd;
298 long clk1;
299
300 // int nVarsEnc; // the number of additional variables to encode outputs
301 // DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
302
303 int nNames; // the total number of all inputs
304 char * pNames[MAXINPUTS]; // the temporary storage for the input (and output encoding) names
305
306 DdNode * aFunc; // the encoded 0-1 BDD containing all the outputs
307
308 char FileNameIni[100];
309 char FileNameFin[100];
310 char Buffer[100];
311
312 DdManager * DdNew;
313
314 //pTable = fopen( "stats.txt", "a+" );
315 //fprintf( pTable, "%s ", pFunc->FileGeneric );
316 //fprintf( pTable, "%d ", nVars );
317 //fprintf( pTable, "%d ", nOuts );
318
319
320 // assign the file names
321 strcpy( FileNameIni, pFunc->FileGeneric );
322 strcat( FileNameIni, "_ENC.blif" );
323
324 strcpy( FileNameFin, pFunc->FileGeneric );
325 strcat( FileNameFin, "_LUT.blif" );
326
327 // derive the single-output function IN THE NEW MANAGER
328 clk1 = Abc_Clock();
329 // aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( aFunc );
330 aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew ); Cudd_Ref( aFunc );
331 printf( "Single-output function derivation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
332 // s_RemappingTime = Abc_Clock() - clk1;
333
334 // dispose of the multiple-output function
335 Extra_Dissolve( pFunc );
336
337 // reorder the single output function
338 printf( "\nReordering variables in the new manager...\n");
339 clk1 = Abc_Clock();
340 printf( "Node count before = %d\n", Cudd_DagSize( aFunc ) );
341 // Cudd_ReduceHeap(DdNew, CUDD_REORDER_SIFT,1);
342 Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
343 // Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
344 printf( "Node count after = %d\n", Cudd_DagSize( aFunc ) );
345 printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
346 printf( "\n" );
347
348 //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
349 //fprintf( pTable, "%d ", Extra_ProfileWidthMax(DdNew, aFunc) );
350
351
352 // create the names to be used with the new manager
353 nNames = DdNew->size;
354 for ( x = 0; x < nNames; x++ )
355 {
356 sprintf( Buffer, "v%02d", x );
357 pNames[x] = Extra_UtilStrsav( Buffer );
358 }
359
360
361
362 // write the single-output function into BLIF for verification
363 clk1 = Abc_Clock();
364 WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni );
365 printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
366
367
368 ///////////////////////////////////////////////////////////////////
369 // verification of single output function
370 clk1 = Abc_Clock();
371 {
372 BFunc g_Func;
373 DdNode * aRes;
374
375 g_Func.dd = DdNew;
376 g_Func.FileInput = Extra_UtilStrsav(FileNameIni);
377
378 if ( Extra_ReadFile( &g_Func ) == 0 )
379 {
380 printf( "\nSomething did not work out while reading the input file for verification\n");
381 Extra_Dissolve( &g_Func );
382 return;
383 }
384
385 aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] ); Cudd_Ref( aRes );
386
387 if ( aRes != aFunc )
388 printf( "\nVerification FAILED!\n");
389 else
390 printf( "\nVerification okay!\n");
391
392 Cudd_RecursiveDeref( DdNew, aRes );
393
394 // delocate
395 Extra_Dissolve( &g_Func );
396 }
397 printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
398 ///////////////////////////////////////////////////////////////////
399
400
401 CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 );
402
403 /*
404 ///////////////////////////////////////////////////////////////////
405 // verification of the decomposed LUT network
406 clk1 = Abc_Clock();
407 {
408 BFunc g_Func;
409 DdNode * aRes;
410
411 g_Func.dd = DdNew;
412 g_Func.FileInput = Extra_UtilStrsav(FileNameFin);
413
414 if ( Extra_ReadFile( &g_Func ) == 0 )
415 {
416 printf( "\nSomething did not work out while reading the input file for verification\n");
417 Extra_Dissolve( &g_Func );
418 return;
419 }
420
421 aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] ); Cudd_Ref( aRes );
422
423 if ( aRes != aFunc )
424 printf( "\nFinal verification FAILED!\n");
425 else
426 printf( "\nFinal verification okay!\n");
427
428 Cudd_RecursiveDeref( DdNew, aRes );
429
430 // delocate
431 Extra_Dissolve( &g_Func );
432 }
433 printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
434 ///////////////////////////////////////////////////////////////////
435 */
436
437
438 Cudd_RecursiveDeref( DdNew, aFunc );
439
440 // release the names
441 for ( i = 0; i < nNames; i++ )
442 ABC_FREE( pNames[i] );
443
444
445
446 /////////////////////////////////////////////////////////////////////
447 // check for remaining references in the package
448 RetValue = Cudd_CheckZeroRef( DdNew );
449 printf( "\nThe number of referenced nodes in the new manager = %d\n", RetValue );
450 Cudd_Quit( DdNew );
451
452 //fprintf( pTable, "\n" );
453 //fclose( pTable );
454
455 }
456
457 #endif
458
459 ////////////////////////////////////////////////////////////////////////
460 /// SINGLE OUTPUT FUNCTION ///
461 ////////////////////////////////////////////////////////////////////////
462
463 // the bit count for the first 256 integer numbers
464 //static unsigned char BitCount8[256] = {
465 // 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
466 // 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
467 // 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
468 // 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
469 // 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
470 // 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
471 // 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
472 // 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
473 //};
474
475 /////////////////////////////////////////////////////////////
476 static int s_SuppSize[MAXOUTPUTS];
CompareSupports(int * ptrX,int * ptrY)477 int CompareSupports( int *ptrX, int *ptrY )
478 {
479 return ( s_SuppSize[*ptrY] - s_SuppSize[*ptrX] );
480 }
481 /////////////////////////////////////////////////////////////
482
483
484 /////////////////////////////////////////////////////////////
485 static int s_MintOnes[MAXOUTPUTS];
CompareMinterms(int * ptrX,int * ptrY)486 int CompareMinterms( int *ptrX, int *ptrY )
487 {
488 return ( s_MintOnes[*ptrY] - s_MintOnes[*ptrX] );
489 }
490 /////////////////////////////////////////////////////////////
491
GrayCode(int BinCode)492 int GrayCode ( int BinCode )
493 {
494 return BinCode ^ ( BinCode >> 1 );
495 }
496
497 /**Function*************************************************************
498
499 Synopsis []
500
501 Description []
502
503 SideEffects []
504
505 SeeAlso []
506
507 ***********************************************************************/
GetSingleOutputFunction(DdManager * dd,DdNode ** pbOuts,int nOuts,DdNode ** pbVarsEnc,int nVarsEnc,int fVerbose)508 DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose )
509 {
510 int i;
511 DdNode * bResult, * aResult;
512 DdNode * bCube, * bTemp, * bProd;
513
514 int Order[MAXOUTPUTS];
515 // int OrderMint[MAXOUTPUTS];
516
517 // sort the output according to their support size
518 for ( i = 0; i < nOuts; i++ )
519 {
520 s_SuppSize[i] = Cudd_SupportSize( dd, pbOuts[i] );
521 // s_MintOnes[i] = BitCount8[i];
522 Order[i] = i;
523 // OrderMint[i] = i;
524 }
525
526 // order the outputs
527 qsort( (void*)Order, (size_t)nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareSupports );
528 // order the outputs
529 // qsort( (void*)OrderMint, (size_t)nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareMinterms );
530
531
532 bResult = b0; Cudd_Ref( bResult );
533 for ( i = 0; i < nOuts; i++ )
534 {
535 // bCube = Cudd_bddBitsToCube( dd, OrderMint[i], nVarsEnc, pbVarsEnc ); Cudd_Ref( bCube );
536 // bProd = Cudd_bddAnd( dd, bCube, pbOuts[Order[nOuts-1-i]] ); Cudd_Ref( bProd );
537 bCube = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc, 1 ); Cudd_Ref( bCube );
538 bProd = Cudd_bddAnd( dd, bCube, pbOuts[Order[i]] ); Cudd_Ref( bProd );
539 Cudd_RecursiveDeref( dd, bCube );
540
541 bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult );
542 Cudd_RecursiveDeref( dd, bTemp );
543 Cudd_RecursiveDeref( dd, bProd );
544 }
545
546 // convert to the ADD
547 if ( fVerbose )
548 printf( "Single BDD size = %6d nodes\n", Cudd_DagSize(bResult) );
549 aResult = Cudd_BddToAdd( dd, bResult ); Cudd_Ref( aResult );
550 Cudd_RecursiveDeref( dd, bResult );
551 if ( fVerbose )
552 printf( "MTBDD = %6d nodes\n", Cudd_DagSize(aResult) );
553 Cudd_Deref( aResult );
554 return aResult;
555 }
556 /*
557 DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc )
558 {
559 int i;
560 DdNode * bResult, * aResult;
561 DdNode * bCube, * bTemp, * bProd;
562
563 bResult = b0; Cudd_Ref( bResult );
564 for ( i = 0; i < nOuts; i++ )
565 {
566 // bCube = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc ); Cudd_Ref( bCube );
567 bCube = Extra_bddBitsToCube( dd, nOuts-1-i, nVarsEnc, pbVarsEnc ); Cudd_Ref( bCube );
568 bProd = Cudd_bddAnd( dd, bCube, pbOuts[i] ); Cudd_Ref( bProd );
569 Cudd_RecursiveDeref( dd, bCube );
570
571 bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult );
572 Cudd_RecursiveDeref( dd, bTemp );
573 Cudd_RecursiveDeref( dd, bProd );
574 }
575
576 // conver to the ADD
577 aResult = Cudd_BddToAdd( dd, bResult ); Cudd_Ref( aResult );
578 Cudd_RecursiveDeref( dd, bResult );
579
580 Cudd_Deref( aResult );
581 return aResult;
582 }
583 */
584
585
586 ////////////////////////////////////////////////////////////////////////
587 /// INPUT REMAPPING ///
588 ////////////////////////////////////////////////////////////////////////
589
590
591 /**Function*************************************************************
592
593 Synopsis []
594
595 Description []
596
597 SideEffects []
598
599 SeeAlso []
600
601 ***********************************************************************/
GetSingleOutputFunctionRemapped(DdManager * dd,DdNode ** pOutputs,int nOuts,DdNode ** pbVarsEnc,int nVarsEnc)602 DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc )
603 // returns the ADD of the remapped function
604 {
605 static int Permute[MAXINPUTS];
606 static DdNode * pRemapped[MAXOUTPUTS];
607
608 DdNode * bSupp, * bTemp;
609 int i, Counter;
610 DdNode * bFunc;
611 DdNode * aFunc;
612
613 Cudd_AutodynDisable(dd);
614
615 // perform the remapping
616 for ( i = 0; i < nOuts; i++ )
617 {
618 // get support
619 bSupp = Cudd_Support( dd, pOutputs[i] ); Cudd_Ref( bSupp );
620
621 // create the variable map
622 Counter = 0;
623 for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
624 Permute[bTemp->index] = Counter++;
625
626 // transfer the BDD and remap it
627 pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute ); Cudd_Ref( pRemapped[i] );
628
629 // remove support
630 Cudd_RecursiveDeref( dd, bSupp );
631 }
632
633 // perform the encoding
634 bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( bFunc );
635
636 // convert to ADD
637 aFunc = Cudd_BddToAdd( dd, bFunc ); Cudd_Ref( aFunc );
638 Cudd_RecursiveDeref( dd, bFunc );
639
640 // deref the intermediate results
641 for ( i = 0; i < nOuts; i++ )
642 Cudd_RecursiveDeref( dd, pRemapped[i] );
643
644 Cudd_Deref( aFunc );
645 return aFunc;
646 }
647
648
649 /**Function*************************************************************
650
651 Synopsis []
652
653 Description []
654
655 SideEffects []
656
657 SeeAlso []
658
659 ***********************************************************************/
GetSingleOutputFunctionRemappedNewDD(DdManager * dd,DdNode ** pOutputs,int nOuts,DdManager ** DdNew)660 DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew )
661 // returns the ADD of the remapped function
662 {
663 static int Permute[MAXINPUTS];
664 static DdNode * pRemapped[MAXOUTPUTS];
665
666 static DdNode * pbVarsEnc[MAXINPUTS];
667 int nVarsEnc;
668
669 DdManager * ddnew;
670
671 DdNode * bSupp, * bTemp;
672 int i, v, Counter;
673 DdNode * bFunc;
674
675 // these are in the new manager
676 DdNode * bFuncNew;
677 DdNode * aFuncNew;
678
679 int nVarsMax = 0;
680
681 // perform the remapping and write the DDs into the new manager
682 for ( i = 0; i < nOuts; i++ )
683 {
684 // get support
685 bSupp = Cudd_Support( dd, pOutputs[i] ); Cudd_Ref( bSupp );
686
687 // create the variable map
688 // to remap the DD into the upper part of the manager
689 Counter = 0;
690 for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
691 Permute[bTemp->index] = dd->invperm[Counter++];
692
693 // transfer the BDD and remap it
694 pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute ); Cudd_Ref( pRemapped[i] );
695
696 // remove support
697 Cudd_RecursiveDeref( dd, bSupp );
698
699
700 // determine the largest support size
701 if ( nVarsMax < Counter )
702 nVarsMax = Counter;
703 }
704
705 // select the encoding variables to follow immediately after the original variables
706 nVarsEnc = Abc_Base2Log(nOuts);
707 /*
708 for ( v = 0; v < nVarsEnc; v++ )
709 if ( nVarsMax + v < dd->size )
710 pbVarsEnc[v] = dd->var[ dd->invperm[nVarsMax+v] ];
711 else
712 pbVarsEnc[v] = Cudd_bddNewVar( dd );
713 */
714 // create the new variables on top of the manager
715 for ( v = 0; v < nVarsEnc; v++ )
716 pbVarsEnc[v] = Cudd_bddNewVarAtLevel( dd, v );
717
718 //fprintf( pTable, "%d ", Cudd_SharingSize( pRemapped, nOuts ) );
719 //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pRemapped, nOuts) );
720
721
722 // perform the encoding
723 bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( bFunc );
724
725
726 // find the cross-manager permutation
727 // the variable from the level v in the old manager
728 // should become a variable number v in the new manager
729 for ( v = 0; v < nVarsMax + nVarsEnc; v++ )
730 Permute[dd->invperm[v]] = v;
731
732
733 ///////////////////////////////////////////////////////////////////////////////
734 // start the new manager
735 ddnew = Cudd_Init( nVarsMax + nVarsEnc, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
736 // Cudd_AutodynDisable(ddnew);
737 Cudd_AutodynEnable(dd, CUDD_REORDER_SYMM_SIFT);
738
739 // transfer it to the new manager
740 bFuncNew = Cudd_bddTransferPermute( dd, ddnew, bFunc, Permute ); Cudd_Ref( bFuncNew );
741 ///////////////////////////////////////////////////////////////////////////////
742
743
744 // deref the intermediate results in the old manager
745 Cudd_RecursiveDeref( dd, bFunc );
746 for ( i = 0; i < nOuts; i++ )
747 Cudd_RecursiveDeref( dd, pRemapped[i] );
748
749
750 ///////////////////////////////////////////////////////////////////////////////
751 // convert to ADD in the new manager
752 aFuncNew = Cudd_BddToAdd( ddnew, bFuncNew ); Cudd_Ref( aFuncNew );
753 Cudd_RecursiveDeref( ddnew, bFuncNew );
754
755 // return the manager
756 *DdNew = ddnew;
757 ///////////////////////////////////////////////////////////////////////////////
758
759 Cudd_Deref( aFuncNew );
760 return aFuncNew;
761 }
762
763 ////////////////////////////////////////////////////////////////////////
764 /// BLIF WRITING FUNCTIONS ///
765 ////////////////////////////////////////////////////////////////////////
766
767 void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
768
769
770 /**Function*************************************************************
771
772 Synopsis []
773
774 Description []
775
776 SideEffects []
777
778 SeeAlso []
779
780 ***********************************************************************/
WriteSingleOutputFunctionBlif(DdManager * dd,DdNode * aFunc,char ** pNames,int nNames,char * FileName)781 void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName )
782 {
783 int i;
784 FILE * pFile;
785
786 // start the file
787 pFile = fopen( FileName, "w" );
788 fprintf( pFile, ".model %s\n", FileName );
789
790 fprintf( pFile, ".inputs" );
791 for ( i = 0; i < nNames; i++ )
792 fprintf( pFile, " %s", pNames[i] );
793 fprintf( pFile, "\n" );
794 fprintf( pFile, ".outputs F" );
795 fprintf( pFile, "\n" );
796
797 // write the DD into the file
798 WriteDDintoBLIFfile( pFile, aFunc, "F", "", pNames );
799
800 fprintf( pFile, ".end\n" );
801 fclose( pFile );
802 }
803
804 /**Function*************************************************************
805
806 Synopsis []
807
808 Description []
809
810 SideEffects []
811
812 SeeAlso []
813
814 ***********************************************************************/
WriteDDintoBLIFfile(FILE * pFile,DdNode * Func,char * OutputName,char * Prefix,char ** InputNames)815 void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames )
816 // writes the main part of the BLIF file
817 // Func is a BDD or a 0-1 ADD to be written
818 // OutputName is the name of the output
819 // Prefix is attached to each intermendiate signal to make it unique
820 // InputNames are the names of the input signals
821 // (some part of the code is borrowed from Cudd_DumpDot())
822 {
823 int i;
824 st__table * visited;
825 st__generator * gen = NULL;
826 long refAddr, diff, mask;
827 DdNode * Node, * Else, * ElseR, * Then;
828
829 /* Initialize symbol table for visited nodes. */
830 visited = st__init_table( st__ptrcmp, st__ptrhash );
831
832 /* Collect all the nodes of this DD in the symbol table. */
833 cuddCollectNodes( Cudd_Regular(Func), visited );
834
835 /* Find how many most significant hex digits are identical
836 ** in the addresses of all the nodes. Build a mask based
837 ** on this knowledge, so that digits that carry no information
838 ** will not be printed. This is done in two steps.
839 ** 1. We scan the symbol table to find the bits that differ
840 ** in at least 2 addresses.
841 ** 2. We choose one of the possible masks. There are 8 possible
842 ** masks for 32-bit integer, and 16 possible masks for 64-bit
843 ** integers.
844 */
845
846 /* Find the bits that are different. */
847 refAddr = ( long )Cudd_Regular(Func);
848 diff = 0;
849 gen = st__init_gen( visited );
850 while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
851 {
852 diff |= refAddr ^ ( long ) Node;
853 }
854 st__free_gen( gen );
855 gen = NULL;
856
857 /* Choose the mask. */
858 for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 )
859 {
860 mask = ( 1 << i ) - 1;
861 if ( diff <= mask )
862 break;
863 }
864
865
866 // write the buffer for the output
867 fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(Func) ) / sizeof(DdNode), OutputName );
868 fprintf( pFile, "%s 1\n", (Cudd_IsComplement(Func))? "0": "1" );
869
870
871 gen = st__init_gen( visited );
872 while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
873 {
874 if ( Node->index == CUDD_MAXINDEX )
875 {
876 // write the terminal node
877 fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
878 fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" );
879 continue;
880 }
881
882 Else = cuddE(Node);
883 ElseR = Cudd_Regular(Else);
884 Then = cuddT(Node);
885
886 assert( InputNames[Node->index] );
887 if ( Else == ElseR )
888 { // no inverter
889 fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index],
890 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
891 Prefix, ( mask & (long)Then ) / sizeof(DdNode),
892 Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
893 fprintf( pFile, "01- 1\n" );
894 fprintf( pFile, "1-1 1\n" );
895 }
896 else
897 { // inverter
898 int * pSlot;
899 fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index],
900 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
901 Prefix, ( mask & (long)Then ) / sizeof(DdNode),
902 Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
903 fprintf( pFile, "01- 1\n" );
904 fprintf( pFile, "1-1 1\n" );
905
906 // if the inverter is written, skip
907 if ( ! st__find( visited, (char *)ElseR, (char ***)&pSlot ) )
908 assert( 0 );
909 if ( *pSlot )
910 continue;
911 *pSlot = 1;
912
913 fprintf( pFile, ".names %s%lx %s%lx_i\n",
914 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
915 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode) );
916 fprintf( pFile, "0 1\n" );
917 }
918 }
919 st__free_gen( gen );
920 gen = NULL;
921 st__free_table( visited );
922 }
923
924
925
926
927 static DdManager * s_ddmin;
928
929 /**Function*************************************************************
930
931 Synopsis []
932
933 Description []
934
935 SideEffects []
936
937 SeeAlso []
938
939 ***********************************************************************/
WriteDDintoBLIFfileReorder(DdManager * dd,FILE * pFile,DdNode * Func,char * OutputName,char * Prefix,char ** InputNames)940 void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames )
941 // writes the main part of the BLIF file
942 // Func is a BDD or a 0-1 ADD to be written
943 // OutputName is the name of the output
944 // Prefix is attached to each intermendiate signal to make it unique
945 // InputNames are the names of the input signals
946 // (some part of the code is borrowed from Cudd_DumpDot())
947 {
948 int i;
949 st__table * visited;
950 st__generator * gen = NULL;
951 long refAddr, diff, mask;
952 DdNode * Node, * Else, * ElseR, * Then;
953
954
955 ///////////////////////////////////////////////////////////////
956 DdNode * bFmin;
957 abctime clk1;
958
959 if ( s_ddmin == NULL )
960 s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
961
962 clk1 = Abc_Clock();
963 bFmin = Cudd_bddTransfer( dd, s_ddmin, Func ); Cudd_Ref( bFmin );
964
965 // reorder
966 printf( "Nodes before = %d. ", Cudd_DagSize(bFmin) );
967 Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
968 // Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT_CONV,1);
969 printf( "Nodes after = %d. \n", Cudd_DagSize(bFmin) );
970 ///////////////////////////////////////////////////////////////
971
972
973
974 /* Initialize symbol table for visited nodes. */
975 visited = st__init_table( st__ptrcmp, st__ptrhash );
976
977 /* Collect all the nodes of this DD in the symbol table. */
978 cuddCollectNodes( Cudd_Regular(bFmin), visited );
979
980 /* Find how many most significant hex digits are identical
981 ** in the addresses of all the nodes. Build a mask based
982 ** on this knowledge, so that digits that carry no information
983 ** will not be printed. This is done in two steps.
984 ** 1. We scan the symbol table to find the bits that differ
985 ** in at least 2 addresses.
986 ** 2. We choose one of the possible masks. There are 8 possible
987 ** masks for 32-bit integer, and 16 possible masks for 64-bit
988 ** integers.
989 */
990
991 /* Find the bits that are different. */
992 refAddr = ( long )Cudd_Regular(bFmin);
993 diff = 0;
994 gen = st__init_gen( visited );
995 while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
996 {
997 diff |= refAddr ^ ( long ) Node;
998 }
999 st__free_gen( gen );
1000 gen = NULL;
1001
1002 /* Choose the mask. */
1003 for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 )
1004 {
1005 mask = ( 1 << i ) - 1;
1006 if ( diff <= mask )
1007 break;
1008 }
1009
1010
1011 // write the buffer for the output
1012 fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(bFmin) ) / sizeof(DdNode), OutputName );
1013 fprintf( pFile, "%s 1\n", (Cudd_IsComplement(bFmin))? "0": "1" );
1014
1015
1016 gen = st__init_gen( visited );
1017 while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
1018 {
1019 if ( Node->index == CUDD_MAXINDEX )
1020 {
1021 // write the terminal node
1022 fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
1023 fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" );
1024 continue;
1025 }
1026
1027 Else = cuddE(Node);
1028 ElseR = Cudd_Regular(Else);
1029 Then = cuddT(Node);
1030
1031 assert( InputNames[Node->index] );
1032 if ( Else == ElseR )
1033 { // no inverter
1034 fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index],
1035 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
1036 Prefix, ( mask & (long)Then ) / sizeof(DdNode),
1037 Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
1038 fprintf( pFile, "01- 1\n" );
1039 fprintf( pFile, "1-1 1\n" );
1040 }
1041 else
1042 { // inverter
1043 fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index],
1044 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
1045 Prefix, ( mask & (long)Then ) / sizeof(DdNode),
1046 Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
1047 fprintf( pFile, "01- 1\n" );
1048 fprintf( pFile, "1-1 1\n" );
1049
1050 fprintf( pFile, ".names %s%lx %s%lx_i\n",
1051 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
1052 Prefix, ( mask & (long)ElseR ) / sizeof(DdNode) );
1053 fprintf( pFile, "0 1\n" );
1054 }
1055 }
1056 st__free_gen( gen );
1057 gen = NULL;
1058 st__free_table( visited );
1059
1060
1061 //////////////////////////////////////////////////
1062 Cudd_RecursiveDeref( s_ddmin, bFmin );
1063 //////////////////////////////////////////////////
1064 }
1065
1066
1067
1068
1069 ////////////////////////////////////////////////////////////////////////
1070 /// TRANSFER WITH MAPPING ///
1071 ////////////////////////////////////////////////////////////////////////
1072 static DdNode * cuddBddTransferPermuteRecur
1073 ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute ));
1074
1075 static DdNode * cuddBddTransferPermute
1076 ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute));
1077
1078 /**Function********************************************************************
1079
1080 Synopsis [Convert a BDD from a manager to another one.]
1081
1082 Description [Convert a BDD from a manager to another one. The orders of the
1083 variables in the two managers may be different. Returns a
1084 pointer to the BDD in the destination manager if successful; NULL
1085 otherwise. The i-th entry in the array Permute tells what is the index
1086 of the i-th variable from the old manager in the new manager.]
1087
1088 SideEffects [None]
1089
1090 SeeAlso []
1091
1092 ******************************************************************************/
1093 DdNode *
Cudd_bddTransferPermute(DdManager * ddSource,DdManager * ddDestination,DdNode * f,int * Permute)1094 Cudd_bddTransferPermute( DdManager * ddSource,
1095 DdManager * ddDestination, DdNode * f, int * Permute )
1096 {
1097 DdNode *res;
1098 do
1099 {
1100 ddDestination->reordered = 0;
1101 res = cuddBddTransferPermute( ddSource, ddDestination, f, Permute );
1102 }
1103 while ( ddDestination->reordered == 1 );
1104 return ( res );
1105
1106 } /* end of Cudd_bddTransferPermute */
1107
1108
1109 /*---------------------------------------------------------------------------*/
1110 /* Definition of internal functions */
1111 /*---------------------------------------------------------------------------*/
1112
1113
1114 /**Function********************************************************************
1115
1116 Synopsis [Convert a BDD from a manager to another one.]
1117
1118 Description [Convert a BDD from a manager to another one. Returns a
1119 pointer to the BDD in the destination manager if successful; NULL
1120 otherwise.]
1121
1122 SideEffects [None]
1123
1124 SeeAlso [Cudd_bddTransferPermute]
1125
1126 ******************************************************************************/
1127 DdNode *
cuddBddTransferPermute(DdManager * ddS,DdManager * ddD,DdNode * f,int * Permute)1128 cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute )
1129 {
1130 DdNode *res;
1131 st__table *table = NULL;
1132 st__generator *gen = NULL;
1133 DdNode *key, *value;
1134
1135 table = st__init_table( st__ptrcmp, st__ptrhash );
1136 if ( table == NULL )
1137 goto failure;
1138 res = cuddBddTransferPermuteRecur( ddS, ddD, f, table, Permute );
1139 if ( res != NULL )
1140 cuddRef( res );
1141
1142 /* Dereference all elements in the table and dispose of the table.
1143 ** This must be done also if res is NULL to avoid leaks in case of
1144 ** reordering. */
1145 gen = st__init_gen( table );
1146 if ( gen == NULL )
1147 goto failure;
1148 while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
1149 {
1150 Cudd_RecursiveDeref( ddD, value );
1151 }
1152 st__free_gen( gen );
1153 gen = NULL;
1154 st__free_table( table );
1155 table = NULL;
1156
1157 if ( res != NULL )
1158 cuddDeref( res );
1159 return ( res );
1160
1161 failure:
1162 if ( table != NULL )
1163 st__free_table( table );
1164 if ( gen != NULL )
1165 st__free_gen( gen );
1166 return ( NULL );
1167
1168 } /* end of cuddBddTransferPermute */
1169
1170
1171 /**Function********************************************************************
1172
1173 Synopsis [Performs the recursive step of Cudd_bddTransferPermute.]
1174
1175 Description [Performs the recursive step of Cudd_bddTransferPermute.
1176 Returns a pointer to the result if successful; NULL otherwise.]
1177
1178 SideEffects [None]
1179
1180 SeeAlso [cuddBddTransferPermute]
1181
1182 ******************************************************************************/
1183 static DdNode *
cuddBddTransferPermuteRecur(DdManager * ddS,DdManager * ddD,DdNode * f,st__table * table,int * Permute)1184 cuddBddTransferPermuteRecur( DdManager * ddS,
1185 DdManager * ddD, DdNode * f, st__table * table, int * Permute )
1186 {
1187 DdNode *ft, *fe, *t, *e, *var, *res;
1188 DdNode *one, *zero;
1189 int index;
1190 int comple = 0;
1191
1192 statLine( ddD );
1193 one = DD_ONE( ddD );
1194 comple = Cudd_IsComplement( f );
1195
1196 /* Trivial cases. */
1197 if ( Cudd_IsConstant( f ) )
1198 return ( Cudd_NotCond( one, comple ) );
1199
1200 /* Make canonical to increase the utilization of the cache. */
1201 f = Cudd_NotCond( f, comple );
1202 /* Now f is a regular pointer to a non-constant node. */
1203
1204 /* Check the cache. */
1205 if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) )
1206 return ( Cudd_NotCond( res, comple ) );
1207
1208 /* Recursive step. */
1209 index = Permute[f->index];
1210 ft = cuddT( f );
1211 fe = cuddE( f );
1212
1213 t = cuddBddTransferPermuteRecur( ddS, ddD, ft, table, Permute );
1214 if ( t == NULL )
1215 {
1216 return ( NULL );
1217 }
1218 cuddRef( t );
1219
1220 e = cuddBddTransferPermuteRecur( ddS, ddD, fe, table, Permute );
1221 if ( e == NULL )
1222 {
1223 Cudd_RecursiveDeref( ddD, t );
1224 return ( NULL );
1225 }
1226 cuddRef( e );
1227
1228 zero = Cudd_Not( one );
1229 var = cuddUniqueInter( ddD, index, one, zero );
1230 if ( var == NULL )
1231 {
1232 Cudd_RecursiveDeref( ddD, t );
1233 Cudd_RecursiveDeref( ddD, e );
1234 return ( NULL );
1235 }
1236 res = cuddBddIteRecur( ddD, var, t, e );
1237 if ( res == NULL )
1238 {
1239 Cudd_RecursiveDeref( ddD, t );
1240 Cudd_RecursiveDeref( ddD, e );
1241 return ( NULL );
1242 }
1243 cuddRef( res );
1244 Cudd_RecursiveDeref( ddD, t );
1245 Cudd_RecursiveDeref( ddD, e );
1246
1247 if ( st__add_direct( table, ( char * ) f, ( char * ) res ) ==
1248 st__OUT_OF_MEM )
1249 {
1250 Cudd_RecursiveDeref( ddD, res );
1251 return ( NULL );
1252 }
1253 return ( Cudd_NotCond( res, comple ) );
1254
1255 } /* end of cuddBddTransferPermuteRecur */
1256
1257 ////////////////////////////////////////////////////////////////////////
1258 /// END OF FILE ///
1259 ////////////////////////////////////////////////////////////////////////
1260
1261
1262
1263
1264 ABC_NAMESPACE_IMPL_END
1265
1266