From 0c6505a26a537dc911b6566f82d759521e527c08 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Jan 2008 20:01:00 -0800 Subject: Version abc80130_2 --- src/bdd/cas/casCore.c | 1263 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1263 insertions(+) create mode 100644 src/bdd/cas/casCore.c (limited to 'src/bdd/cas/casCore.c') diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c new file mode 100644 index 00000000..579235b1 --- /dev/null +++ b/src/bdd/cas/casCore.c @@ -0,0 +1,1263 @@ +/**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 + +#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 /// +//////////////////////////////////////////////////////////////////////// + + + + -- cgit v1.2.3