/**CFile**************************************************************** FileName [casCore.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.] Synopsis [Entrance into the implementation.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - Spring 2002.] Revision [$Id: casCore.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $] ***********************************************************************/ #include #include #include #include "base/main/main.h" #include "base/cmd/cmd.h" #include "misc/extra/extraBdd.h" #include "cas.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// static functions /// //////////////////////////////////////////////////////////////////////// DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose ); DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc ); DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew ); extern int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose ); void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName ); DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ); //////////////////////////////////////////////////////////////////////// /// static varibles /// //////////////////////////////////////////////////////////////////////// //static FILE * pTable = NULL; //static long s_RemappingTime = 0; //////////////////////////////////////////////////////////////////////// /// debugging macros /// //////////////////////////////////////////////////////////////////////// #define PRD(p) printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 ) #define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" ) #define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" ) #define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" ) //////////////////////////////////////////////////////////////////////// /// EXTERNAL FUNCTIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose ) { int i; int nVars = nInputs; int nOuts = nOutputs; abctime clk1; int nVarsEnc; // the number of additional variables to encode outputs DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars int nNames; // the total number of all inputs char * pNames[MAXINPUTS]; // the temporary storage for the input (and output encoding) names DdNode * aFunc; // the encoded 0-1 BDD containing all the outputs char FileNameIni[100]; char FileNameFin[100]; char Buffer[100]; //pTable = fopen( "stats.txt", "a+" ); //fprintf( pTable, "%s ", pFileGeneric ); //fprintf( pTable, "%d ", nVars ); //fprintf( pTable, "%d ", nOuts ); // assign the file names strcpy( FileNameIni, pFileGeneric ); strcat( FileNameIni, "_ENC.blif" ); strcpy( FileNameFin, pFileGeneric ); strcat( FileNameFin, "_LUT.blif" ); // create the variables to encode the outputs nVarsEnc = Abc_Base2Log( nOuts ); for ( i = 0; i < nVarsEnc; i++ ) pbVarsEnc[i] = Cudd_bddNewVarAtLevel( dd, i ); // store the input names nNames = nVars + nVarsEnc; for ( i = 0; i < nVars; i++ ) { // pNames[i] = Extra_UtilStrsav( pFunc->pInputNames[i] ); sprintf( Buffer, "pi%03d", i ); pNames[i] = Extra_UtilStrsav( Buffer ); } // set the encoding variable name for ( ; i < nNames; i++ ) { sprintf( Buffer, "OutEnc_%02d", i-nVars ); pNames[i] = Extra_UtilStrsav( Buffer ); } // print the variable order // printf( "\n" ); // printf( "Variable order is: " ); // for ( i = 0; i < dd->size; i++ ) // printf( " %d", dd->invperm[i] ); // printf( "\n" ); // derive the single-output function clk1 = Abc_Clock(); aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose ); Cudd_Ref( aFunc ); // aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( aFunc ); // if ( fVerbose ) // printf( "Single-output function computation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); //fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) ); //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) ); // dispose of the multiple-output function // Extra_Dissolve( pFunc ); // reorder the single output function // if ( fVerbose ) // printf( "Reordering variables...\n"); clk1 = Abc_Clock(); // if ( fVerbose ) // printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) ); // Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1); Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1); Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1); // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1); // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1); // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1); // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1); if ( fVerbose ) printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) ); if ( fVerbose ) printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); // printf( "\n" ); // printf( "Variable order is: " ); // for ( i = 0; i < dd->size; i++ ) // printf( " %d", dd->invperm[i] ); // printf( "\n" ); //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) ); //fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) ); // write the single-output function into BLIF for verification clk1 = Abc_Clock(); if ( fCheck ) WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni ); // if ( fVerbose ) // printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); /* /////////////////////////////////////////////////////////////////// // verification of single output function clk1 = Abc_Clock(); { BFunc g_Func; DdNode * aRes; g_Func.dd = dd; g_Func.FileInput = Extra_UtilStrsav(FileNameIni); if ( Extra_ReadFile( &g_Func ) == 0 ) { printf( "\nSomething did not work out while reading the input file for verification\n"); Extra_Dissolve( &g_Func ); return; } aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] ); Cudd_Ref( aRes ); if ( aRes != aFunc ) printf( "\nVerification FAILED!\n"); else printf( "\nVerification okay!\n"); Cudd_RecursiveDeref( dd, aRes ); // delocate Extra_Dissolve( &g_Func ); } printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); /////////////////////////////////////////////////////////////////// */ if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) ) return 0; /* /////////////////////////////////////////////////////////////////// // verification of the decomposed LUT network clk1 = Abc_Clock(); { BFunc g_Func; DdNode * aRes; g_Func.dd = dd; g_Func.FileInput = Extra_UtilStrsav(FileNameFin); if ( Extra_ReadFile( &g_Func ) == 0 ) { printf( "\nSomething did not work out while reading the input file for verification\n"); Extra_Dissolve( &g_Func ); return; } aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] ); Cudd_Ref( aRes ); if ( aRes != aFunc ) printf( "\nFinal verification FAILED!\n"); else printf( "\nFinal verification okay!\n"); Cudd_RecursiveDeref( dd, aRes ); // delocate Extra_Dissolve( &g_Func ); } printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); /////////////////////////////////////////////////////////////////// */ // verify the results if ( fCheck ) { char Command[200]; sprintf( Command, "cec %s %s", FileNameIni, FileNameFin ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ); } Cudd_RecursiveDeref( dd, aFunc ); // release the names for ( i = 0; i < nNames; i++ ) ABC_FREE( pNames[i] ); //fprintf( pTable, "\n" ); //fclose( pTable ); return 1; } #if 0 /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Experiment2( BFunc * pFunc ) { int i, x, RetValue; int nVars = pFunc->nInputs; int nOuts = pFunc->nOutputs; DdManager * dd = pFunc->dd; long clk1; // int nVarsEnc; // the number of additional variables to encode outputs // DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars int nNames; // the total number of all inputs char * pNames[MAXINPUTS]; // the temporary storage for the input (and output encoding) names DdNode * aFunc; // the encoded 0-1 BDD containing all the outputs char FileNameIni[100]; char FileNameFin[100]; char Buffer[100]; DdManager * DdNew; //pTable = fopen( "stats.txt", "a+" ); //fprintf( pTable, "%s ", pFunc->FileGeneric ); //fprintf( pTable, "%d ", nVars ); //fprintf( pTable, "%d ", nOuts ); // assign the file names strcpy( FileNameIni, pFunc->FileGeneric ); strcat( FileNameIni, "_ENC.blif" ); strcpy( FileNameFin, pFunc->FileGeneric ); strcat( FileNameFin, "_LUT.blif" ); // derive the single-output function IN THE NEW MANAGER clk1 = Abc_Clock(); // aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( aFunc ); aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew ); Cudd_Ref( aFunc ); printf( "Single-output function derivation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); // s_RemappingTime = Abc_Clock() - clk1; // dispose of the multiple-output function Extra_Dissolve( pFunc ); // reorder the single output function printf( "\nReordering variables in the new manager...\n"); clk1 = Abc_Clock(); printf( "Node count before = %d\n", Cudd_DagSize( aFunc ) ); // Cudd_ReduceHeap(DdNew, CUDD_REORDER_SIFT,1); Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1); // Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1); printf( "Node count after = %d\n", Cudd_DagSize( aFunc ) ); printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); printf( "\n" ); //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) ); //fprintf( pTable, "%d ", Extra_ProfileWidthMax(DdNew, aFunc) ); // create the names to be used with the new manager nNames = DdNew->size; for ( x = 0; x < nNames; x++ ) { sprintf( Buffer, "v%02d", x ); pNames[x] = Extra_UtilStrsav( Buffer ); } // write the single-output function into BLIF for verification clk1 = Abc_Clock(); WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni ); printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); /////////////////////////////////////////////////////////////////// // verification of single output function clk1 = Abc_Clock(); { BFunc g_Func; DdNode * aRes; g_Func.dd = DdNew; g_Func.FileInput = Extra_UtilStrsav(FileNameIni); if ( Extra_ReadFile( &g_Func ) == 0 ) { printf( "\nSomething did not work out while reading the input file for verification\n"); Extra_Dissolve( &g_Func ); return; } aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] ); Cudd_Ref( aRes ); if ( aRes != aFunc ) printf( "\nVerification FAILED!\n"); else printf( "\nVerification okay!\n"); Cudd_RecursiveDeref( DdNew, aRes ); // delocate Extra_Dissolve( &g_Func ); } printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); /////////////////////////////////////////////////////////////////// CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 ); /* /////////////////////////////////////////////////////////////////// // verification of the decomposed LUT network clk1 = Abc_Clock(); { BFunc g_Func; DdNode * aRes; g_Func.dd = DdNew; g_Func.FileInput = Extra_UtilStrsav(FileNameFin); if ( Extra_ReadFile( &g_Func ) == 0 ) { printf( "\nSomething did not work out while reading the input file for verification\n"); Extra_Dissolve( &g_Func ); return; } aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] ); Cudd_Ref( aRes ); if ( aRes != aFunc ) printf( "\nFinal verification FAILED!\n"); else printf( "\nFinal verification okay!\n"); Cudd_RecursiveDeref( DdNew, aRes ); // delocate Extra_Dissolve( &g_Func ); } printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); /////////////////////////////////////////////////////////////////// */ Cudd_RecursiveDeref( DdNew, aFunc ); // release the names for ( i = 0; i < nNames; i++ ) ABC_FREE( pNames[i] ); ///////////////////////////////////////////////////////////////////// // check for remaining references in the package RetValue = Cudd_CheckZeroRef( DdNew ); printf( "\nThe number of referenced nodes in the new manager = %d\n", RetValue ); Cudd_Quit( DdNew ); //fprintf( pTable, "\n" ); //fclose( pTable ); } #endif //////////////////////////////////////////////////////////////////////// /// SINGLE OUTPUT FUNCTION /// //////////////////////////////////////////////////////////////////////// // the bit count for the first 256 integer numbers //static unsigned char BitCount8[256] = { // 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, // 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, // 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, // 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, // 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, // 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, // 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, // 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 //}; ///////////////////////////////////////////////////////////// static int s_SuppSize[MAXOUTPUTS]; int CompareSupports( int *ptrX, int *ptrY ) { return ( s_SuppSize[*ptrY] - s_SuppSize[*ptrX] ); } ///////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////// static int s_MintOnes[MAXOUTPUTS]; int CompareMinterms( int *ptrX, int *ptrY ) { return ( s_MintOnes[*ptrY] - s_MintOnes[*ptrX] ); } ///////////////////////////////////////////////////////////// int GrayCode ( int BinCode ) { return BinCode ^ ( BinCode >> 1 ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose ) { int i; DdNode * bResult, * aResult; DdNode * bCube, * bTemp, * bProd; int Order[MAXOUTPUTS]; // int OrderMint[MAXOUTPUTS]; // sort the output according to their support size for ( i = 0; i < nOuts; i++ ) { s_SuppSize[i] = Cudd_SupportSize( dd, pbOuts[i] ); // s_MintOnes[i] = BitCount8[i]; Order[i] = i; // OrderMint[i] = i; } // order the outputs qsort( (void*)Order, nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareSupports ); // order the outputs // qsort( (void*)OrderMint, nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareMinterms ); bResult = b0; Cudd_Ref( bResult ); for ( i = 0; i < nOuts; i++ ) { // bCube = Cudd_bddBitsToCube( dd, OrderMint[i], nVarsEnc, pbVarsEnc ); Cudd_Ref( bCube ); // bProd = Cudd_bddAnd( dd, bCube, pbOuts[Order[nOuts-1-i]] ); Cudd_Ref( bProd ); bCube = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc, 1 ); Cudd_Ref( bCube ); bProd = Cudd_bddAnd( dd, bCube, pbOuts[Order[i]] ); Cudd_Ref( bProd ); Cudd_RecursiveDeref( dd, bCube ); bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bProd ); } // convert to the ADD if ( fVerbose ) printf( "Single BDD size = %6d nodes\n", Cudd_DagSize(bResult) ); aResult = Cudd_BddToAdd( dd, bResult ); Cudd_Ref( aResult ); Cudd_RecursiveDeref( dd, bResult ); if ( fVerbose ) printf( "MTBDD = %6d nodes\n", Cudd_DagSize(aResult) ); Cudd_Deref( aResult ); return aResult; } /* DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc ) { int i; DdNode * bResult, * aResult; DdNode * bCube, * bTemp, * bProd; bResult = b0; Cudd_Ref( bResult ); for ( i = 0; i < nOuts; i++ ) { // bCube = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc ); Cudd_Ref( bCube ); bCube = Extra_bddBitsToCube( dd, nOuts-1-i, nVarsEnc, pbVarsEnc ); Cudd_Ref( bCube ); bProd = Cudd_bddAnd( dd, bCube, pbOuts[i] ); Cudd_Ref( bProd ); Cudd_RecursiveDeref( dd, bCube ); bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bProd ); } // conver to the ADD aResult = Cudd_BddToAdd( dd, bResult ); Cudd_Ref( aResult ); Cudd_RecursiveDeref( dd, bResult ); Cudd_Deref( aResult ); return aResult; } */ //////////////////////////////////////////////////////////////////////// /// INPUT REMAPPING /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc ) // returns the ADD of the remapped function { static int Permute[MAXINPUTS]; static DdNode * pRemapped[MAXOUTPUTS]; DdNode * bSupp, * bTemp; int i, Counter; DdNode * bFunc; DdNode * aFunc; Cudd_AutodynDisable(dd); // perform the remapping for ( i = 0; i < nOuts; i++ ) { // get support bSupp = Cudd_Support( dd, pOutputs[i] ); Cudd_Ref( bSupp ); // create the variable map Counter = 0; for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) ) Permute[bTemp->index] = Counter++; // transfer the BDD and remap it pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute ); Cudd_Ref( pRemapped[i] ); // remove support Cudd_RecursiveDeref( dd, bSupp ); } // perform the encoding bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( bFunc ); // convert to ADD aFunc = Cudd_BddToAdd( dd, bFunc ); Cudd_Ref( aFunc ); Cudd_RecursiveDeref( dd, bFunc ); // deref the intermediate results for ( i = 0; i < nOuts; i++ ) Cudd_RecursiveDeref( dd, pRemapped[i] ); Cudd_Deref( aFunc ); return aFunc; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew ) // returns the ADD of the remapped function { static int Permute[MAXINPUTS]; static DdNode * pRemapped[MAXOUTPUTS]; static DdNode * pbVarsEnc[MAXINPUTS]; int nVarsEnc; DdManager * ddnew; DdNode * bSupp, * bTemp; int i, v, Counter; DdNode * bFunc; // these are in the new manager DdNode * bFuncNew; DdNode * aFuncNew; int nVarsMax = 0; // perform the remapping and write the DDs into the new manager for ( i = 0; i < nOuts; i++ ) { // get support bSupp = Cudd_Support( dd, pOutputs[i] ); Cudd_Ref( bSupp ); // create the variable map // to remap the DD into the upper part of the manager Counter = 0; for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) ) Permute[bTemp->index] = dd->invperm[Counter++]; // transfer the BDD and remap it pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute ); Cudd_Ref( pRemapped[i] ); // remove support Cudd_RecursiveDeref( dd, bSupp ); // determine the largest support size if ( nVarsMax < Counter ) nVarsMax = Counter; } // select the encoding variables to follow immediately after the original variables nVarsEnc = Abc_Base2Log(nOuts); /* for ( v = 0; v < nVarsEnc; v++ ) if ( nVarsMax + v < dd->size ) pbVarsEnc[v] = dd->var[ dd->invperm[nVarsMax+v] ]; else pbVarsEnc[v] = Cudd_bddNewVar( dd ); */ // create the new variables on top of the manager for ( v = 0; v < nVarsEnc; v++ ) pbVarsEnc[v] = Cudd_bddNewVarAtLevel( dd, v ); //fprintf( pTable, "%d ", Cudd_SharingSize( pRemapped, nOuts ) ); //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pRemapped, nOuts) ); // perform the encoding bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( bFunc ); // find the cross-manager permutation // the variable from the level v in the old manager // should become a variable number v in the new manager for ( v = 0; v < nVarsMax + nVarsEnc; v++ ) Permute[dd->invperm[v]] = v; /////////////////////////////////////////////////////////////////////////////// // start the new manager ddnew = Cudd_Init( nVarsMax + nVarsEnc, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); // Cudd_AutodynDisable(ddnew); Cudd_AutodynEnable(dd, CUDD_REORDER_SYMM_SIFT); // transfer it to the new manager bFuncNew = Cudd_bddTransferPermute( dd, ddnew, bFunc, Permute ); Cudd_Ref( bFuncNew ); /////////////////////////////////////////////////////////////////////////////// // deref the intermediate results in the old manager Cudd_RecursiveDeref( dd, bFunc ); for ( i = 0; i < nOuts; i++ ) Cudd_RecursiveDeref( dd, pRemapped[i] ); /////////////////////////////////////////////////////////////////////////////// // convert to ADD in the new manager aFuncNew = Cudd_BddToAdd( ddnew, bFuncNew ); Cudd_Ref( aFuncNew ); Cudd_RecursiveDeref( ddnew, bFuncNew ); // return the manager *DdNew = ddnew; /////////////////////////////////////////////////////////////////////////////// Cudd_Deref( aFuncNew ); return aFuncNew; } //////////////////////////////////////////////////////////////////////// /// BLIF WRITING FUNCTIONS /// //////////////////////////////////////////////////////////////////////// void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames ); /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName ) { int i; FILE * pFile; // start the file pFile = fopen( FileName, "w" ); fprintf( pFile, ".model %s\n", FileName ); fprintf( pFile, ".inputs" ); for ( i = 0; i < nNames; i++ ) fprintf( pFile, " %s", pNames[i] ); fprintf( pFile, "\n" ); fprintf( pFile, ".outputs F" ); fprintf( pFile, "\n" ); // write the DD into the file WriteDDintoBLIFfile( pFile, aFunc, "F", "", pNames ); fprintf( pFile, ".end\n" ); fclose( pFile ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames ) // writes the main part of the BLIF file // Func is a BDD or a 0-1 ADD to be written // OutputName is the name of the output // Prefix is attached to each intermendiate signal to make it unique // InputNames are the names of the input signals // (some part of the code is borrowed from Cudd_DumpDot()) { int i; st__table * visited; st__generator * gen = NULL; long refAddr, diff, mask; DdNode * Node, * Else, * ElseR, * Then; /* Initialize symbol table for visited nodes. */ visited = st__init_table( st__ptrcmp, st__ptrhash ); /* Collect all the nodes of this DD in the symbol table. */ cuddCollectNodes( Cudd_Regular(Func), visited ); /* Find how many most significant hex digits are identical ** in the addresses of all the nodes. Build a mask based ** on this knowledge, so that digits that carry no information ** will not be printed. This is done in two steps. ** 1. We scan the symbol table to find the bits that differ ** in at least 2 addresses. ** 2. We choose one of the possible masks. There are 8 possible ** masks for 32-bit integer, and 16 possible masks for 64-bit ** integers. */ /* Find the bits that are different. */ refAddr = ( long )Cudd_Regular(Func); diff = 0; gen = st__init_gen( visited ); while ( st__gen( gen, ( const char ** ) &Node, NULL ) ) { diff |= refAddr ^ ( long ) Node; } st__free_gen( gen ); gen = NULL; /* Choose the mask. */ for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 ) { mask = ( 1 << i ) - 1; if ( diff <= mask ) break; } // write the buffer for the output fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(Func) ) / sizeof(DdNode), OutputName ); fprintf( pFile, "%s 1\n", (Cudd_IsComplement(Func))? "0": "1" ); gen = st__init_gen( visited ); while ( st__gen( gen, ( const char ** ) &Node, NULL ) ) { if ( Node->index == CUDD_MAXINDEX ) { // write the terminal node fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) ); fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" ); continue; } Else = cuddE(Node); ElseR = Cudd_Regular(Else); Then = cuddT(Node); assert( InputNames[Node->index] ); if ( Else == ElseR ) { // no inverter fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index], Prefix, ( mask & (long)ElseR ) / sizeof(DdNode), Prefix, ( mask & (long)Then ) / sizeof(DdNode), Prefix, ( mask & (long)Node ) / sizeof(DdNode) ); fprintf( pFile, "01- 1\n" ); fprintf( pFile, "1-1 1\n" ); } else { // inverter int * pSlot; fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index], Prefix, ( mask & (long)ElseR ) / sizeof(DdNode), Prefix, ( mask & (long)Then ) / sizeof(DdNode), Prefix, ( mask & (long)Node ) / sizeof(DdNode) ); fprintf( pFile, "01- 1\n" ); fprintf( pFile, "1-1 1\n" ); // if the inverter is written, skip if ( ! st__find( visited, (char *)ElseR, (char ***)&pSlot ) ) assert( 0 ); if ( *pSlot ) continue; *pSlot = 1; fprintf( pFile, ".names %s%lx %s%lx_i\n", Prefix, ( mask & (long)ElseR ) / sizeof(DdNode), Prefix, ( mask & (long)ElseR ) / sizeof(DdNode) ); fprintf( pFile, "0 1\n" ); } } st__free_gen( gen ); gen = NULL; st__free_table( visited ); } static DdManager * s_ddmin; /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames ) // writes the main part of the BLIF file // Func is a BDD or a 0-1 ADD to be written // OutputName is the name of the output // Prefix is attached to each intermendiate signal to make it unique // InputNames are the names of the input signals // (some part of the code is borrowed from Cudd_DumpDot()) { int i; st__table * visited; st__generator * gen = NULL; long refAddr, diff, mask; DdNode * Node, * Else, * ElseR, * Then; /////////////////////////////////////////////////////////////// DdNode * bFmin; abctime clk1; if ( s_ddmin == NULL ) s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); clk1 = Abc_Clock(); bFmin = Cudd_bddTransfer( dd, s_ddmin, Func ); Cudd_Ref( bFmin ); // reorder printf( "Nodes before = %d. ", Cudd_DagSize(bFmin) ); Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1); // Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT_CONV,1); printf( "Nodes after = %d. \n", Cudd_DagSize(bFmin) ); /////////////////////////////////////////////////////////////// /* Initialize symbol table for visited nodes. */ visited = st__init_table( st__ptrcmp, st__ptrhash ); /* Collect all the nodes of this DD in the symbol table. */ cuddCollectNodes( Cudd_Regular(bFmin), visited ); /* Find how many most significant hex digits are identical ** in the addresses of all the nodes. Build a mask based ** on this knowledge, so that digits that carry no information ** will not be printed. This is done in two steps. ** 1. We scan the symbol table to find the bits that differ ** in at least 2 addresses. ** 2. We choose one of the possible masks. There are 8 possible ** masks for 32-bit integer, and 16 possible masks for 64-bit ** integers. */ /* Find the bits that are different. */ refAddr = ( long )Cudd_Regular(bFmin); diff = 0; gen = st__init_gen( visited ); while ( st__gen( gen, ( const char ** ) &Node, NULL ) ) { diff |= refAddr ^ ( long ) Node; } st__free_gen( gen ); gen = NULL; /* Choose the mask. */ for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 ) { mask = ( 1 << i ) - 1; if ( diff <= mask ) break; } // write the buffer for the output fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(bFmin) ) / sizeof(DdNode), OutputName ); fprintf( pFile, "%s 1\n", (Cudd_IsComplement(bFmin))? "0": "1" ); gen = st__init_gen( visited ); while ( st__gen( gen, ( const char ** ) &Node, NULL ) ) { if ( Node->index == CUDD_MAXINDEX ) { // write the terminal node fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) ); fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" ); continue; } Else = cuddE(Node); ElseR = Cudd_Regular(Else); Then = cuddT(Node); assert( InputNames[Node->index] ); if ( Else == ElseR ) { // no inverter fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index], Prefix, ( mask & (long)ElseR ) / sizeof(DdNode), Prefix, ( mask & (long)Then ) / sizeof(DdNode), Prefix, ( mask & (long)Node ) / sizeof(DdNode) ); fprintf( pFile, "01- 1\n" ); fprintf( pFile, "1-1 1\n" ); } else { // inverter fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index], Prefix, ( mask & (long)ElseR ) / sizeof(DdNode), Prefix, ( mask & (long)Then ) / sizeof(DdNode), Prefix, ( mask & (long)Node ) / sizeof(DdNode) ); fprintf( pFile, "01- 1\n" ); fprintf( pFile, "1-1 1\n" ); fprintf( pFile, ".names %s%lx %s%lx_i\n", Prefix, ( mask & (long)ElseR ) / sizeof(DdNode), Prefix, ( mask & (long)ElseR ) / sizeof(DdNode) ); fprintf( pFile, "0 1\n" ); } } st__free_gen( gen ); gen = NULL; st__free_table( visited ); ////////////////////////////////////////////////// Cudd_RecursiveDeref( s_ddmin, bFmin ); ////////////////////////////////////////////////// } //////////////////////////////////////////////////////////////////////// /// TRANSFER WITH MAPPING /// //////////////////////////////////////////////////////////////////////// static DdNode * cuddBddTransferPermuteRecur ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute )); static DdNode * cuddBddTransferPermute ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute)); /**Function******************************************************************** Synopsis [Convert a BDD from a manager to another one.] Description [Convert a BDD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise. The i-th entry in the array Permute tells what is the index of the i-th variable from the old manager in the new manager.] SideEffects [None] SeeAlso [] ******************************************************************************/ DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ) { DdNode *res; do { ddDestination->reordered = 0; res = cuddBddTransferPermute( ddSource, ddDestination, f, Permute ); } while ( ddDestination->reordered == 1 ); return ( res ); } /* end of Cudd_bddTransferPermute */ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Convert a BDD from a manager to another one.] Description [Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.] SideEffects [None] SeeAlso [Cudd_bddTransferPermute] ******************************************************************************/ DdNode * cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ) { DdNode *res; st__table *table = NULL; st__generator *gen = NULL; DdNode *key, *value; table = st__init_table( st__ptrcmp, st__ptrhash ); if ( table == NULL ) goto failure; res = cuddBddTransferPermuteRecur( ddS, ddD, f, table, Permute ); if ( res != NULL ) cuddRef( res ); /* Dereference all elements in the table and dispose of the table. ** This must be done also if res is NULL to avoid leaks in case of ** reordering. */ gen = st__init_gen( table ); if ( gen == NULL ) goto failure; while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) ) { Cudd_RecursiveDeref( ddD, value ); } st__free_gen( gen ); gen = NULL; st__free_table( table ); table = NULL; if ( res != NULL ) cuddDeref( res ); return ( res ); failure: if ( table != NULL ) st__free_table( table ); if ( gen != NULL ) st__free_gen( gen ); return ( NULL ); } /* end of cuddBddTransferPermute */ /**Function******************************************************************** Synopsis [Performs the recursive step of Cudd_bddTransferPermute.] Description [Performs the recursive step of Cudd_bddTransferPermute. Returns a pointer to the result if successful; NULL otherwise.] SideEffects [None] SeeAlso [cuddBddTransferPermute] ******************************************************************************/ static DdNode * cuddBddTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute ) { DdNode *ft, *fe, *t, *e, *var, *res; DdNode *one, *zero; int index; int comple = 0; statLine( ddD ); one = DD_ONE( ddD ); comple = Cudd_IsComplement( f ); /* Trivial cases. */ if ( Cudd_IsConstant( f ) ) return ( Cudd_NotCond( one, comple ) ); /* Make canonical to increase the utilization of the cache. */ f = Cudd_NotCond( f, comple ); /* Now f is a regular pointer to a non-constant node. */ /* Check the cache. */ if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) ) return ( Cudd_NotCond( res, comple ) ); /* Recursive step. */ index = Permute[f->index]; ft = cuddT( f ); fe = cuddE( f ); t = cuddBddTransferPermuteRecur( ddS, ddD, ft, table, Permute ); if ( t == NULL ) { return ( NULL ); } cuddRef( t ); e = cuddBddTransferPermuteRecur( ddS, ddD, fe, table, Permute ); if ( e == NULL ) { Cudd_RecursiveDeref( ddD, t ); return ( NULL ); } cuddRef( e ); zero = Cudd_Not( one ); var = cuddUniqueInter( ddD, index, one, zero ); if ( var == NULL ) { Cudd_RecursiveDeref( ddD, t ); Cudd_RecursiveDeref( ddD, e ); return ( NULL ); } res = cuddBddIteRecur( ddD, var, t, e ); if ( res == NULL ) { Cudd_RecursiveDeref( ddD, t ); Cudd_RecursiveDeref( ddD, e ); return ( NULL ); } cuddRef( res ); Cudd_RecursiveDeref( ddD, t ); Cudd_RecursiveDeref( ddD, e ); if ( st__add_direct( table, ( char * ) f, ( char * ) res ) == st__OUT_OF_MEM ) { Cudd_RecursiveDeref( ddD, res ); return ( NULL ); } return ( Cudd_NotCond( res, comple ) ); } /* end of cuddBddTransferPermuteRecur */ //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END