diff options
Diffstat (limited to 'src/bdd/cas/casCore.c')
-rw-r--r-- | src/bdd/cas/casCore.c | 1263 |
1 files changed, 0 insertions, 1263 deletions
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c deleted file mode 100644 index 579235b1..00000000 --- a/src/bdd/cas/casCore.c +++ /dev/null @@ -1,1263 +0,0 @@ -/**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 <stdio.h> -#include <stdlib.h> -#include <string.h> -#include <time.h> - -#include "extra.h" -#include "cas.h" - -//////////////////////////////////////////////////////////////////////// -/// 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; - 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]; - - -//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 = Extra_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 = 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)(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 = 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)(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 = clock(); - if ( fCheck ) - WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni ); -// if ( fVerbose ) -// printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - -/* - /////////////////////////////////////////////////////////////////// - // verification of single output function - clk1 = 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)(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 = 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)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - /////////////////////////////////////////////////////////////////// -*/ - - // verify the results - if ( fCheck ) - { - extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); - extern void * Abc_FrameGetGlobalFrame(); - 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++ ) - 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 = 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)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); -// s_RemappingTime = 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 = 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)(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 = clock(); - WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni ); - printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - - - /////////////////////////////////////////////////////////////////// - // verification of single output function - clk1 = 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)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - /////////////////////////////////////////////////////////////////// - - - CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 ); - -/* - /////////////////////////////////////////////////////////////////// - // verification of the decomposed LUT network - clk1 = 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)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - /////////////////////////////////////////////////////////////////// -*/ - - - Cudd_RecursiveDeref( DdNew, aFunc ); - - // release the names - for ( i = 0; i < nNames; i++ ) - 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; - int nSuppPrev = -1; - 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; - int nSuppPrev = -1; - 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 = Extra_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, ( 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, ( 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; - int clk1; - - if ( s_ddmin == NULL ) - s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); - - clk1 = 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, ( 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, ( 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, ( 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 /// -//////////////////////////////////////////////////////////////////////// - - - - |