diff options
Diffstat (limited to 'src/bdd')
88 files changed, 2817 insertions, 174 deletions
diff --git a/src/bdd/cas/cas.h b/src/bdd/cas/cas.h new file mode 100644 index 00000000..fcc9f890 --- /dev/null +++ b/src/bdd/cas/cas.h @@ -0,0 +1,62 @@ +/**CFile**************************************************************** + + FileName [cas.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cas.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CAS_H__ +#define __CAS_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define MAXINPUTS 1024 +#define MAXOUTPUTS 1024 + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== zzz.c ==========================================================*/ + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + 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 <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 /// +//////////////////////////////////////////////////////////////////////// + + + + diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c new file mode 100644 index 00000000..a1eb5f36 --- /dev/null +++ b/src/bdd/cas/casDec.c @@ -0,0 +1,508 @@ +/**CFile**************************************************************** + + FileName [casDec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.] + + Synopsis [BDD-based decomposition with encoding.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Spring 2002.] + + Revision [$Id: casDec.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <string.h> +#include <stdlib.h> +#include <time.h> + +#include "extra.h" +#include "cas.h" + +//////////////////////////////////////////////////////////////////////// +/// type definitions /// +//////////////////////////////////////////////////////////////////////// + +typedef struct +{ + int nIns; // the number of LUT variables + int nInsP; // the number of inputs coming from the previous LUT + int nCols; // the number of columns in this LUT + int nMulti; // the column multiplicity, [log2(nCols)] + int nSimple; // the number of outputs implemented as direct connections to inputs of the previous block + int Level; // the starting level in the ADD in this LUT + +// DdNode ** pbVarsIn[32]; // the BDDs of the elementary input variables +// DdNode ** pbVarsOut[32]; // the BDDs of the elementary output variables + +// char * pNamesIn[32]; // the names of input variables +// char * pNamesOut[32]; // the names of output variables + + DdNode ** pbCols; // the array of columns represented by BDDs + DdNode ** pbCodes; // the array of codes (in terms of pbVarsOut) + DdNode ** paNodes; // the array of starting ADD nodes on the next level (also referenced) + + DdNode * bRelation; // the relation after encoding + + // the relation depends on the three groups of variables: + // (1) variables on top represent the outputs of the previous cascade + // (2) variables in the middle represent the primary inputs + // (3) variables below (CVars) represent the codes + // + // the replacement is done after computing the relation +} LUT; + + +//////////////////////////////////////////////////////////////////////// +/// static functions /// +//////////////////////////////////////////////////////////////////////// + +// the LUT-2-BLIF writing function +void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName ); + +// the function to write a DD (BDD or ADD) as a network of MUXES +extern void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames ); +extern void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames ); + +//////////////////////////////////////////////////////////////////////// +/// static varibles /// +//////////////////////////////////////////////////////////////////////// + +static int s_LutSize = 15; +static int s_nFuncVars; + +long s_EncodingTime; + +long s_EncSearchTime; +long s_EncComputeTime; + +//////////////////////////////////// +// temporary output variables +//FILE * pTable; +//long s_ReadingTime; +//long s_RemappingTime; +//////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// debugging macros /// +//////////////////////////////////////////////////////////////////////// + +#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 /// +//////////////////////////////////////////////////////////////////////// + +int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose ) +// aFunc is a 0-1 ADD for the given function +// pNames (nNames) are the input variable names +// FileName is the name of the output file for the LUT network +// dynamic variable reordering should be disabled when this function is running +{ + static LUT * pLuts[MAXINPUTS]; // the LUT cascade + static int Profile[MAXINPUTS]; // the profile filled in with the info about the BDD width + static int Permute[MAXINPUTS]; // the array to store a temporary permutation of variables + + LUT * p; // the current LUT + int i, v; + + DdNode * bCVars[32]; // these are variables for the codes + + int nVarsRem; // the number of remaining variables + int PrevMulti; // column multiplicity on the previous level + int fLastLut; // flag to signal the last LUT + int nLuts; + int nLutsTotal = 0; + int nLutOutputs = 0; + int nLutOutputsOrig = 0; + + long clk1; + + s_LutSize = nLutSize; + + s_nFuncVars = nNames; + + // get the profile + clk1 = clock(); + Extra_ProfileWidth( dd, aFunc, Profile, -1 ); + + +// for ( v = 0; v < nNames; v++ ) +// printf( "Level = %2d, Width = %2d\n", v+1, Profile[v] ); + + +//printf( "\n" ); + + // mark-up the LUTs + // assuming that the manager has exactly nNames vars (new vars have not been introduced yet) + nVarsRem = nNames; // the number of remaining variables + PrevMulti = 0; // column multiplicity on the previous level + fLastLut = 0; + nLuts = 0; + do + { + p = (LUT*) malloc( sizeof(LUT) ); + memset( p, 0, sizeof(LUT) ); + + if ( nVarsRem + PrevMulti <= s_LutSize ) // this is the last LUT + { + p->nIns = nVarsRem + PrevMulti; + p->nInsP = PrevMulti; + p->nCols = 2; + p->nMulti = 1; + p->Level = nNames-nVarsRem; + + nVarsRem = 0; + PrevMulti = 1; + + fLastLut = 1; + } + else // this is not the last LUT + { + p->nIns = s_LutSize; + p->nInsP = PrevMulti; + p->nCols = Profile[nNames-(nVarsRem-(s_LutSize-PrevMulti))]; + p->nMulti = Extra_Base2Log(p->nCols); + p->Level = nNames-nVarsRem; + + nVarsRem = nVarsRem-(s_LutSize-PrevMulti); + PrevMulti = p->nMulti; + } + + if ( p->nMulti >= s_LutSize ) + { + printf( "The LUT size is too small\n" ); + return 0; + } + + nLutOutputsOrig += p->nMulti; + + +//if ( fVerbose ) +//printf( "Stage %2d: In = %3d, InP = %3d, Cols = %5d, Multi = %2d, Level = %2d\n", +// nLuts+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->Level ); + + + // there should be as many columns, codes, and nodes, as there are columns on this level + p->pbCols = (DdNode **) malloc( p->nCols * sizeof(DdNode *) ); + p->pbCodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) ); + p->paNodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) ); + + pLuts[nLuts] = p; + nLuts++; + } + while ( !fLastLut ); + + +//if ( fVerbose ) +//printf( "The number of cascades = %d\n", nLuts ); + + +//fprintf( pTable, "%d ", nLuts ); + + + // add the new variables at the bottom + for ( i = 0; i < s_LutSize; i++ ) + bCVars[i] = Cudd_bddNewVar(dd); + + // for each LUT - assign the LUT and encode the columns + s_EncodingTime = 0; + for ( i = 0; i < nLuts; i++ ) + { + int RetValue; + DdNode * bVars[32]; + int nVars; + DdNode * bVarsInCube; + DdNode * bVarsCCube; + DdNode * bVarsCube; + int CutLevel; + + p = pLuts[i]; + + // compute the columns of this LUT starting from the given set of nodes with the given codes + // (these codes have been remapped to depend on the topmost variables in the manager) + // for the first LUT, start with the constant 1 BDD + CutLevel = p->Level + p->nIns - p->nInsP; + if ( i == 0 ) + RetValue = Extra_bddNodePathsUnderCutArray( + dd, &aFunc, &(b1), 1, + p->paNodes, p->pbCols, CutLevel ); + else + RetValue = Extra_bddNodePathsUnderCutArray( + dd, pLuts[i-1]->paNodes, pLuts[i-1]->pbCodes, pLuts[i-1]->nCols, + p->paNodes, p->pbCols, CutLevel ); + assert( RetValue == p->nCols ); + // at this point, we have filled out p->paNodes[] and p->pbCols[] of this LUT + // pLuts[i-1]->paNodes depended on normal vars + // pLuts[i-1]->pbCodes depended on the topmost variables + // the resulting p->paNodes depend on normal ADD nodes + // the resulting p->pbCols depend on normal vars and topmost variables in the manager + + // perform the encoding + + // create the cube of these variables + // collect the topmost variables of the manager + nVars = p->nInsP; + for ( v = 0; v < nVars; v++ ) + bVars[v] = dd->vars[ dd->invperm[v] ]; + bVarsCCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 ); Cudd_Ref( bVarsCCube ); + + // collect the primary input variables involved in this LUT + nVars = p->nIns - p->nInsP; + for ( v = 0; v < nVars; v++ ) + bVars[v] = dd->vars[ dd->invperm[p->Level+v] ]; + bVarsInCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 ); Cudd_Ref( bVarsInCube ); + + // get the cube + bVarsCube = Cudd_bddAnd( dd, bVarsInCube, bVarsCCube ); Cudd_Ref( bVarsCube ); + Cudd_RecursiveDeref( dd, bVarsInCube ); + Cudd_RecursiveDeref( dd, bVarsCCube ); + + // get the encoding relation + if ( i == nLuts -1 ) + { + DdNode * bVar; + assert( p->nMulti == 1 ); + assert( p->nCols == 2 ); + assert( Cudd_IsConstant( p->paNodes[0] ) ); + assert( Cudd_IsConstant( p->paNodes[1] ) ); + + bVar = ( p->paNodes[0] == a1 )? bCVars[0]: Cudd_Not( bCVars[0] ); + p->bRelation = Cudd_bddIte( dd, bVar, p->pbCols[0], p->pbCols[1] ); Cudd_Ref( p->bRelation ); + } + else + { + long clk2 = clock(); +// p->bRelation = PerformTheEncoding( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple ); Cudd_Ref( p->bRelation ); + p->bRelation = Extra_bddEncodingNonStrict( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple ); Cudd_Ref( p->bRelation ); + s_EncodingTime += clock() - clk2; + } + + // update the number of LUT outputs + nLutOutputs += (p->nMulti - p->nSimple); + nLutsTotal += p->nMulti; + +//if ( fVerbose ) +//printf( "Stage %2d: Simple = %d\n", i+1, p->nSimple ); + +if ( fVerbose ) +printf( "Stage %3d: In = %3d InP = %3d Cols = %5d Multi = %2d Simple = %2d Level = %3d\n", + i+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->nSimple, p->Level ); + + // get the codes from the relation (these are not necessarily cubes) + { + int c; + for ( c = 0; c < p->nCols; c++ ) + { + p->pbCodes[c] = Cudd_bddAndAbstract( dd, p->bRelation, p->pbCols[c], bVarsCube ); Cudd_Ref( p->pbCodes[c] ); + } + } + + Cudd_RecursiveDeref( dd, bVarsCube ); + + // remap the codes to depend on the topmost varibles of the manager + // useful as a preparation for the next step + { + DdNode ** pbTemp; + int k, v; + + pbTemp = (DdNode **) malloc( p->nCols * sizeof(DdNode *) ); + + // create the identical permutation + for ( v = 0; v < dd->size; v++ ) + Permute[v] = v; + + // use the topmost variables of the manager + // to represent the previous level codes + for ( v = 0; v < p->nMulti; v++ ) + Permute[bCVars[v]->index] = dd->invperm[v]; + + Extra_bddPermuteArray( dd, p->pbCodes, pbTemp, p->nCols, Permute ); + // the array pbTemp comes already referenced + + // deref the old codes and assign the new ones + for ( k = 0; k < p->nCols; k++ ) + { + Cudd_RecursiveDeref( dd, p->pbCodes[k] ); + p->pbCodes[k] = pbTemp[k]; + } + free( pbTemp ); + } + } + if ( fVerbose ) + printf( "LUTs: Total = %5d. Final = %5d. Simple = %5d. (%6.2f %%) ", + nLutsTotal, nLutOutputs, nLutsTotal-nLutOutputs, 100.0*(nLutsTotal-nLutOutputs)/nLutsTotal ); + if ( fVerbose ) + printf( "Memory = %6.2f Mb\n", 1.0*nLutOutputs*(1<<nLutSize)/(1<<20) ); +// printf( "\n" ); + +//fprintf( pTable, "%d ", nLutOutputsOrig ); +//fprintf( pTable, "%d ", nLutOutputs ); + + if ( fVerbose ) + { + printf( "Pure decomposition time = %.2f sec\n", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) ); + printf( "Encoding time = %.2f sec\n", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) ); +// printf( "Encoding search time = %.2f sec\n", (float)(s_EncSearchTime)/(float)(CLOCKS_PER_SEC) ); +// printf( "Encoding compute time = %.2f sec\n", (float)(s_EncComputeTime)/(float)(CLOCKS_PER_SEC) ); + } + + +//fprintf( pTable, "%.2f ", (float)(s_ReadingTime)/(float)(CLOCKS_PER_SEC) ); +//fprintf( pTable, "%.2f ", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) ); +//fprintf( pTable, "%.2f ", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) ); +//fprintf( pTable, "%.2f ", (float)(s_RemappingTime)/(float)(CLOCKS_PER_SEC) ); + + + // write LUTs into the BLIF file + clk1 = clock(); + if ( fCheck ) + { + 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 + WriteLUTSintoBLIFfile( pFile, dd, pLuts, nLuts, bCVars, pNames, nNames, FileName ); + + fprintf( pFile, ".end\n" ); + fclose( pFile ); + if ( fVerbose ) + printf( "Output file writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) ); + } + + + // updo the LUT cascade + for ( i = 0; i < nLuts; i++ ) + { + p = pLuts[i]; + for ( v = 0; v < p->nCols; v++ ) + { + Cudd_RecursiveDeref( dd, p->pbCols[v] ); + Cudd_RecursiveDeref( dd, p->pbCodes[v] ); + Cudd_RecursiveDeref( dd, p->paNodes[v] ); + } + Cudd_RecursiveDeref( dd, p->bRelation ); + + free( p->pbCols ); + free( p->pbCodes ); + free( p->paNodes ); + free( p ); + } + + return 1; +} + +void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName ) +{ + int i, v, o; + static char * pNamesLocalIn[MAXINPUTS]; + static char * pNamesLocalOut[MAXINPUTS]; + static char Buffer[100]; + DdNode * bCube, * bCof, * bFunc; + LUT * p; + + // go through all the LUTs + for ( i = 0; i < nLuts; i++ ) + { + // get the pointer to the LUT + p = pLuts[i]; + + if ( i == nLuts -1 ) + { + assert( p->nMulti == 1 ); + } + + + fprintf( pFile, "#----------------- LUT #%d ----------------------\n", i ); + + + // fill in the names for the current LUT + + // write the outputs of the previous LUT + if ( i != 0 ) + for ( v = 0; v < p->nInsP; v++ ) + { + sprintf( Buffer, "LUT%02d_%02d", i-1, v ); + pNamesLocalIn[dd->invperm[v]] = Extra_UtilStrsav( Buffer ); + } + // write the primary inputs of the current LUT + for ( v = 0; v < p->nIns - p->nInsP; v++ ) + pNamesLocalIn[dd->invperm[p->Level+v]] = Extra_UtilStrsav( pNames[dd->invperm[p->Level+v]] ); + // write the outputs of the current LUT + for ( v = 0; v < p->nMulti; v++ ) + { + sprintf( Buffer, "LUT%02d_%02d", i, v ); + if ( i != nLuts - 1 ) + pNamesLocalOut[v] = Extra_UtilStrsav( Buffer ); + else + pNamesLocalOut[v] = Extra_UtilStrsav( "F" ); + } + + + // write LUT outputs + + // get the prefix + sprintf( Buffer, "L%02d_", i ); + + // get the cube of encoding variables + bCube = Extra_bddBitsToCube( dd, (1<<p->nMulti)-1, p->nMulti, bCVars, 1 ); Cudd_Ref( bCube ); + + // write each output of the LUT + for ( o = 0; o < p->nMulti; o++ ) + { + // get the cofactor of this output + bCof = Cudd_Cofactor( dd, p->bRelation, bCVars[o] ); Cudd_Ref( bCof ); + // quantify the remaining variables to get the function + bFunc = Cudd_bddExistAbstract( dd, bCof, bCube ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bCof ); + + // write BLIF + sprintf( Buffer, "L%02d_%02d_", i, o ); + +// WriteDDintoBLIFfileReorder( dd, pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn ); + // does not work well; the advantage is marginal (30%), the run time is huge... + + WriteDDintoBLIFfile( pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn ); + Cudd_RecursiveDeref( dd, bFunc ); + } + Cudd_RecursiveDeref( dd, bCube ); + + // clean up the previous local names + for ( v = 0; v < dd->size; v++ ) + { + if ( pNamesLocalIn[v] ) + free( pNamesLocalIn[v] ); + pNamesLocalIn[v] = NULL; + } + for ( v = 0; v < p->nMulti; v++ ) + free( pNamesLocalOut[v] ); + } +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + + + diff --git a/src/bdd/cas/module.make b/src/bdd/cas/module.make new file mode 100644 index 00000000..7830e47f --- /dev/null +++ b/src/bdd/cas/module.make @@ -0,0 +1,3 @@ +SRC += src/bdd/cas/casCore.c \ + src/bdd/cas/casDec.c + diff --git a/src/bdd/cudd/cuddAPI.c b/src/bdd/cudd/cuddAPI.c index 2acde7cd..a16b82cf 100644 --- a/src/bdd/cudd/cuddAPI.c +++ b/src/bdd/cudd/cuddAPI.c @@ -164,7 +164,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddAddAbs.c b/src/bdd/cudd/cuddAddAbs.c index 27039908..b256ad0f 100644 --- a/src/bdd/cudd/cuddAddAbs.c +++ b/src/bdd/cudd/cuddAddAbs.c @@ -32,7 +32,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddAddApply.c b/src/bdd/cudd/cuddAddApply.c index 67649913..60c06de6 100644 --- a/src/bdd/cudd/cuddAddApply.c +++ b/src/bdd/cudd/cuddAddApply.c @@ -42,7 +42,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddAddFind.c b/src/bdd/cudd/cuddAddFind.c index 3399527a..0469b014 100644 --- a/src/bdd/cudd/cuddAddFind.c +++ b/src/bdd/cudd/cuddAddFind.c @@ -27,7 +27,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddAddInv.c b/src/bdd/cudd/cuddAddInv.c index cb6dbfbe..fc4a340b 100644 --- a/src/bdd/cudd/cuddAddInv.c +++ b/src/bdd/cudd/cuddAddInv.c @@ -24,7 +24,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c index 77c4d18a..71f8070f 100644 --- a/src/bdd/cudd/cuddAddIte.c +++ b/src/bdd/cudd/cuddAddIte.c @@ -33,7 +33,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddAddNeg.c b/src/bdd/cudd/cuddAddNeg.c index 2420df64..bdb08ddc 100644 --- a/src/bdd/cudd/cuddAddNeg.c +++ b/src/bdd/cudd/cuddAddNeg.c @@ -26,7 +26,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c index 980ee215..c6a67e34 100644 --- a/src/bdd/cudd/cuddAddWalsh.c +++ b/src/bdd/cudd/cuddAddWalsh.c @@ -26,7 +26,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c index 3a6ce85f..5ec47beb 100644 --- a/src/bdd/cudd/cuddAndAbs.c +++ b/src/bdd/cudd/cuddAndAbs.c @@ -24,7 +24,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddAnneal.c b/src/bdd/cudd/cuddAnneal.c index dfc81e86..3d8b56b9 100644 --- a/src/bdd/cudd/cuddAnneal.c +++ b/src/bdd/cudd/cuddAnneal.c @@ -35,7 +35,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddApa.c b/src/bdd/cudd/cuddApa.c index 805a4dde..47ab51e8 100644 --- a/src/bdd/cudd/cuddApa.c +++ b/src/bdd/cudd/cuddApa.c @@ -28,7 +28,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddApprox.c b/src/bdd/cudd/cuddApprox.c index eb6813ff..debcf48b 100644 --- a/src/bdd/cudd/cuddApprox.c +++ b/src/bdd/cudd/cuddApprox.c @@ -51,7 +51,7 @@ #else #define DBL_MAX_EXP 1024 #endif -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c index 20a8f15a..9552464e 100644 --- a/src/bdd/cudd/cuddBddAbs.c +++ b/src/bdd/cudd/cuddBddAbs.c @@ -35,7 +35,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c index 47395ec7..c99324a8 100644 --- a/src/bdd/cudd/cuddBddCorr.c +++ b/src/bdd/cudd/cuddBddCorr.c @@ -30,7 +30,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c index fe0c6500..b44e40de 100644 --- a/src/bdd/cudd/cuddBddIte.c +++ b/src/bdd/cudd/cuddBddIte.c @@ -44,7 +44,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c index e7e5c89f..ccc0893f 100644 --- a/src/bdd/cudd/cuddBridge.c +++ b/src/bdd/cudd/cuddBridge.c @@ -44,7 +44,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddCache.c b/src/bdd/cudd/cuddCache.c index 6598948a..d9e40921 100644 --- a/src/bdd/cudd/cuddCache.c +++ b/src/bdd/cudd/cuddCache.c @@ -36,7 +36,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddCheck.c b/src/bdd/cudd/cuddCheck.c index 3db08dd6..aec8246d 100644 --- a/src/bdd/cudd/cuddCheck.c +++ b/src/bdd/cudd/cuddCheck.c @@ -34,7 +34,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c index 3c728a56..4da296ef 100644 --- a/src/bdd/cudd/cuddClip.c +++ b/src/bdd/cudd/cuddClip.c @@ -33,7 +33,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddCof.c b/src/bdd/cudd/cuddCof.c index 0dfeff6c..f79e3f91 100644 --- a/src/bdd/cudd/cuddCof.c +++ b/src/bdd/cudd/cuddCof.c @@ -29,7 +29,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c index 11c6cb7b..8c858051 100644 --- a/src/bdd/cudd/cuddCompose.c +++ b/src/bdd/cudd/cuddCompose.c @@ -55,7 +55,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c index d9c28482..4fde7392 100644 --- a/src/bdd/cudd/cuddDecomp.c +++ b/src/bdd/cudd/cuddDecomp.c @@ -34,7 +34,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddEssent.c b/src/bdd/cudd/cuddEssent.c index 7bd48c5a..db4b8b49 100644 --- a/src/bdd/cudd/cuddEssent.c +++ b/src/bdd/cudd/cuddEssent.c @@ -25,7 +25,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c index 6a81406b..6852be68 100644 --- a/src/bdd/cudd/cuddExact.c +++ b/src/bdd/cudd/cuddExact.c @@ -40,7 +40,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c index d7b9645b..d148be42 100644 --- a/src/bdd/cudd/cuddExport.c +++ b/src/bdd/cudd/cuddExport.c @@ -35,7 +35,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c index 59ae55d7..142ee27e 100644 --- a/src/bdd/cudd/cuddGenCof.c +++ b/src/bdd/cudd/cuddGenCof.c @@ -46,7 +46,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddGenetic.c b/src/bdd/cudd/cuddGenetic.c index 8341dcbd..9fe03dad 100644 --- a/src/bdd/cudd/cuddGenetic.c +++ b/src/bdd/cudd/cuddGenetic.c @@ -53,7 +53,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c index f84f7881..81c05d2c 100644 --- a/src/bdd/cudd/cuddGroup.c +++ b/src/bdd/cudd/cuddGroup.c @@ -49,7 +49,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddHarwell.c b/src/bdd/cudd/cuddHarwell.c index 10746186..063f1922 100644 --- a/src/bdd/cudd/cuddHarwell.c +++ b/src/bdd/cudd/cuddHarwell.c @@ -21,7 +21,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddInit.c b/src/bdd/cudd/cuddInit.c index aec8d286..8e06a425 100644 --- a/src/bdd/cudd/cuddInit.c +++ b/src/bdd/cudd/cuddInit.c @@ -29,7 +29,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #define CUDD_MAIN #include "cuddInt.h" #undef CUDD_MAIN diff --git a/src/bdd/cudd/cuddInteract.c b/src/bdd/cudd/cuddInteract.c index 5a4ec79a..96613639 100644 --- a/src/bdd/cudd/cuddInteract.c +++ b/src/bdd/cudd/cuddInteract.c @@ -47,7 +47,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c index 72fbd48a..8bd37ba0 100644 --- a/src/bdd/cudd/cuddLCache.c +++ b/src/bdd/cudd/cuddLCache.c @@ -45,7 +45,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddLevelQ.c b/src/bdd/cudd/cuddLevelQ.c index c4c621e7..3cc8e8d8 100644 --- a/src/bdd/cudd/cuddLevelQ.c +++ b/src/bdd/cudd/cuddLevelQ.c @@ -50,7 +50,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c index cec7c255..7f6b3678 100644 --- a/src/bdd/cudd/cuddLinear.c +++ b/src/bdd/cudd/cuddLinear.c @@ -34,7 +34,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddLiteral.c b/src/bdd/cudd/cuddLiteral.c index 69594486..43740690 100644 --- a/src/bdd/cudd/cuddLiteral.c +++ b/src/bdd/cudd/cuddLiteral.c @@ -25,7 +25,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c index b10975ec..345e7921 100644 --- a/src/bdd/cudd/cuddMatMult.c +++ b/src/bdd/cudd/cuddMatMult.c @@ -29,7 +29,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c index bb0b83d3..788fc712 100644 --- a/src/bdd/cudd/cuddPriority.c +++ b/src/bdd/cudd/cuddPriority.c @@ -43,7 +43,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddRead.c b/src/bdd/cudd/cuddRead.c index eea4c7f3..2c4a86d8 100644 --- a/src/bdd/cudd/cuddRead.c +++ b/src/bdd/cudd/cuddRead.c @@ -23,7 +23,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddRef.c b/src/bdd/cudd/cuddRef.c index af08d048..a9241f3d 100644 --- a/src/bdd/cudd/cuddRef.c +++ b/src/bdd/cudd/cuddRef.c @@ -38,7 +38,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c index e2b3470b..1387196f 100644 --- a/src/bdd/cudd/cuddReorder.c +++ b/src/bdd/cudd/cuddReorder.c @@ -45,7 +45,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c index dde33a5b..1755a1c1 100644 --- a/src/bdd/cudd/cuddSat.c +++ b/src/bdd/cudd/cuddSat.c @@ -42,7 +42,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddSign.c b/src/bdd/cudd/cuddSign.c index 62477e7f..fcaa65c4 100644 --- a/src/bdd/cudd/cuddSign.c +++ b/src/bdd/cudd/cuddSign.c @@ -25,7 +25,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c index 058e0c08..d9c4a2e7 100644 --- a/src/bdd/cudd/cuddSolve.c +++ b/src/bdd/cudd/cuddSolve.c @@ -28,7 +28,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddSplit.c b/src/bdd/cudd/cuddSplit.c index af7d6372..e21ea7cb 100644 --- a/src/bdd/cudd/cuddSplit.c +++ b/src/bdd/cudd/cuddSplit.c @@ -32,7 +32,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddSubsetHB.c b/src/bdd/cudd/cuddSubsetHB.c index 43aaf744..24d41ce5 100644 --- a/src/bdd/cudd/cuddSubsetHB.c +++ b/src/bdd/cudd/cuddSubsetHB.c @@ -46,7 +46,7 @@ #else #define DBL_MAX_EXP 1024 #endif -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c index 0f7209dd..55ee3470 100644 --- a/src/bdd/cudd/cuddSubsetSP.c +++ b/src/bdd/cudd/cuddSubsetSP.c @@ -41,7 +41,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c index 7b2013e4..e5488b17 100644 --- a/src/bdd/cudd/cuddSymmetry.c +++ b/src/bdd/cudd/cuddSymmetry.c @@ -38,7 +38,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c index b118b76a..7f14aed1 100644 --- a/src/bdd/cudd/cuddTable.c +++ b/src/bdd/cudd/cuddTable.c @@ -54,7 +54,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c index c366d534..d5fa18e2 100644 --- a/src/bdd/cudd/cuddUtil.c +++ b/src/bdd/cudd/cuddUtil.c @@ -76,7 +76,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddWindow.c b/src/bdd/cudd/cuddWindow.c index 3e6d5686..9ceb79b2 100644 --- a/src/bdd/cudd/cuddWindow.c +++ b/src/bdd/cudd/cuddWindow.c @@ -31,7 +31,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddCount.c b/src/bdd/cudd/cuddZddCount.c index 29cf0c14..6c6ec1df 100644 --- a/src/bdd/cudd/cuddZddCount.c +++ b/src/bdd/cudd/cuddZddCount.c @@ -34,7 +34,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddFuncs.c b/src/bdd/cudd/cuddZddFuncs.c index f938e1de..9dc27a95 100644 --- a/src/bdd/cudd/cuddZddFuncs.c +++ b/src/bdd/cudd/cuddZddFuncs.c @@ -48,7 +48,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c index 35f28881..621fa43f 100644 --- a/src/bdd/cudd/cuddZddGroup.c +++ b/src/bdd/cudd/cuddZddGroup.c @@ -40,7 +40,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddIsop.c b/src/bdd/cudd/cuddZddIsop.c index 0918461c..f4b057ea 100644 --- a/src/bdd/cudd/cuddZddIsop.c +++ b/src/bdd/cudd/cuddZddIsop.c @@ -34,7 +34,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddLin.c b/src/bdd/cudd/cuddZddLin.c index 9369bb05..ef2cd298 100644 --- a/src/bdd/cudd/cuddZddLin.c +++ b/src/bdd/cudd/cuddZddLin.c @@ -32,7 +32,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddMisc.c b/src/bdd/cudd/cuddZddMisc.c index d55bb768..6a4ddd09 100644 --- a/src/bdd/cudd/cuddZddMisc.c +++ b/src/bdd/cudd/cuddZddMisc.c @@ -33,7 +33,7 @@ ******************************************************************************/ #include <math.h> -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddPort.c b/src/bdd/cudd/cuddZddPort.c index 1700ab2b..6d4a3236 100644 --- a/src/bdd/cudd/cuddZddPort.c +++ b/src/bdd/cudd/cuddZddPort.c @@ -32,7 +32,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c index e14ae2ad..e2da37f2 100644 --- a/src/bdd/cudd/cuddZddReord.c +++ b/src/bdd/cudd/cuddZddReord.c @@ -46,7 +46,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddSetop.c b/src/bdd/cudd/cuddZddSetop.c index cf05210f..f1bd72f3 100644 --- a/src/bdd/cudd/cuddZddSetop.c +++ b/src/bdd/cudd/cuddZddSetop.c @@ -46,7 +46,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c index c9ffaab4..54019892 100644 --- a/src/bdd/cudd/cuddZddSymm.c +++ b/src/bdd/cudd/cuddZddSymm.c @@ -40,7 +40,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c index 0795f123..616d16d4 100644 --- a/src/bdd/cudd/cuddZddUtil.c +++ b/src/bdd/cudd/cuddZddUtil.c @@ -35,7 +35,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/cudd/testcudd.c b/src/bdd/cudd/testcudd.c index 451bb190..d8affadc 100644 --- a/src/bdd/cudd/testcudd.c +++ b/src/bdd/cudd/testcudd.c @@ -23,7 +23,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "cuddInt.h" diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 5396bacd..b73b81ab 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -28,8 +28,12 @@ #ifndef __DSD_H__ #define __DSD_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// -/// TYPEDEF DEFITIONS /// +/// TYPEDEF DEFINITIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Dsd_Manager_t_ Dsd_Manager_t; @@ -55,14 +59,14 @@ enum Dsd_Type_t_ { }; //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// // complementation and testing for pointers for decomposition entries -#define Dsd_IsComplement(p) (((int)((long) (p) & 01))) -#define Dsd_Regular(p) ((Dsd_Node_t *)((unsigned)(p) & ~01)) -#define Dsd_Not(p) ((Dsd_Node_t *)((long)(p) ^ 01)) -#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((long)(p) ^ (c))) +#define Dsd_IsComplement(p) (((int)((unsigned long) (p) & 01))) +#define Dsd_Regular(p) ((Dsd_Node_t *)((unsigned long)(p) & ~01)) +#define Dsd_Not(p) ((Dsd_Node_t *)((unsigned long)(p) ^ 01)) +#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((unsigned long)(p) ^ (c))) //////////////////////////////////////////////////////////////////////// /// ITERATORS /// @@ -76,7 +80,7 @@ enum Dsd_Type_t_ { Index++ ) //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /*=== dsdApi.c =======================================================*/ @@ -91,6 +95,7 @@ extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ); extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ); extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ); +extern Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ); /*=== dsdMan.c =======================================================*/ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ); extern void Dsd_ManagerStop( Dsd_Manager_t * dMan ); @@ -100,6 +105,7 @@ extern Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc /*=== dsdTree.c =======================================================*/ extern void Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax ); extern void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax ); +extern int Dsd_TreeGetAigCost( Dsd_Node_t * pNode ); extern int Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * dMan ); extern int Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot ); extern int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan ); @@ -108,11 +114,16 @@ extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, in extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes ); extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ); extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output ); +extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif
\ No newline at end of file diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c index daf3080f..d1c90e23 100644 --- a/src/bdd/dsd/dsdApi.c +++ b/src/bdd/dsd/dsdApi.c @@ -23,7 +23,7 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -89,6 +89,7 @@ void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; } ***********************************************************************/ Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ) { return pMan->pRoots[i]; } Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } +Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ) { return pMan->pConst1; } DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ) { return pMan->dd; } //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c index 608aa2e3..58b824d2 100644 --- a/src/bdd/dsd/dsdCheck.c +++ b/src/bdd/dsd/dsdCheck.c @@ -43,7 +43,7 @@ static Dds_Cache_t * pCache; static int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function******************************************************************** @@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries ) /**Function******************************************************************** - Synopsis [Delocates the local cache.] + Synopsis [Deallocates the local cache.] Description [] diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 5008c24e..62ce7e99 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -23,7 +23,7 @@ #include "dsd.h" //////////////////////////////////////////////////////////////////////// -/// TYPEDEF DEFITIONS /// +/// TYPEDEF DEFINITIONS /// //////////////////////////////////////////////////////////////////////// typedef unsigned char byte; @@ -42,6 +42,7 @@ struct Dsd_Manager_t_ int nRootsAlloc;// the number of primary outputs Dsd_Node_t ** pInputs; // the primary input nodes Dsd_Node_t ** pRoots; // the primary output nodes + Dsd_Node_t * pConst1; // the constant node int fVerbose; // the verbosity level }; @@ -58,7 +59,7 @@ struct Dsd_Node_t_ }; //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// #define MAXINPUTS 1000 @@ -82,9 +83,9 @@ extern void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode ); extern void Dsd_TreeUnmark( Dsd_Manager_t * dMan ); extern DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif
\ No newline at end of file diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c index 4529e75a..6e43f0f4 100644 --- a/src/bdd/dsd/dsdMan.c +++ b/src/bdd/dsd/dsdMan.c @@ -73,6 +73,7 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ) pNode->G = b1; Cudd_Ref( pNode->G ); pNode->S = b1; Cudd_Ref( pNode->S ); st_insert( dMan->Table, (char*)b1, (char*)pNode ); + dMan->pConst1 = pNode; Dsd_CheckCacheAllocate( 5000 ); return dMan; diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c index 08c029e1..543ad387 100644 --- a/src/bdd/dsd/dsdProc.c +++ b/src/bdd/dsd/dsdProc.c @@ -1255,7 +1255,7 @@ EXIT: s_CacheEntries++; -#if 0 +/* if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 ) { // write the function, for which verification does not work @@ -1277,7 +1277,7 @@ EXIT: cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask ); Cudd_RecursiveDerefZdd( dd, zNewFunc ); } -#endif +*/ } diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index 7905cbdd..2855d68d 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/src/bdd/dsd/dsdTree.c @@ -29,7 +29,7 @@ static int Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode ); static int Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars ); static void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes ); static void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fCcmp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames ); - +static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter ); //////////////////////////////////////////////////////////////////////// /// STATIC VARIABLES /// @@ -243,6 +243,58 @@ void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur ) /**Function************************************************************* + Synopsis [Counts AIG nodes needed to implement this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode ) +{ + int i, Counter = 0; + + assert( pNode ); + assert( !Dsd_IsComplement( pNode ) ); + assert( pNode->nVisits >= 0 ); + + if ( pNode->nDecs < 2 ) + return 0; + + // we don't want the two-input gates to count for non-decomposable blocks + if ( pNode->Type == DSD_NODE_OR ) + Counter += pNode->nDecs - 1; + else if ( pNode->Type == DSD_NODE_EXOR ) + Counter += 3*(pNode->nDecs - 1); + else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 ) + Counter += 3; + + // call recursively + for ( i = 0; i < pNode->nDecs; i++ ) + Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts AIG nodes needed to implement this node.] + + Description [Assumes that the only primes of the DSD tree are MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsd_TreeGetAigCost( Dsd_Node_t * pNode ) +{ + return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) ); +} + +/**Function************************************************************* + Synopsis [Counts non-terminal nodes of the DSD tree.] Description [Nonterminal nodes include all the nodes with the @@ -631,27 +683,21 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); Extra_PrintSymbols( pFile, ' ', nOffset, 0 ); - fprintf( pFile, "%s: ", pOutputName ); + if ( !fComp ) + fprintf( pFile, "%s = ", pOutputName ); + else + fprintf( pFile, "NOT(%s) = ", pOutputName ); pInputNums = ALLOC( int, pNode->nDecs ); if ( pNode->Type == DSD_NODE_CONST1 ) { - if ( fComp ) - fprintf( pFile, " Constant 0.\n" ); - else - fprintf( pFile, " Constant 1.\n" ); + fprintf( pFile, " Constant 1.\n" ); } else if ( pNode->Type == DSD_NODE_BUF ) { - if ( fComp ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( fShortNames ) - fprintf( pFile, "%d", pNode->S->index ); + fprintf( pFile, "%d", 'a' + pNode->S->index ); else fprintf( pFile, "%s", pInputNames[pNode->S->index] ); - if ( fComp ) - fprintf( pFile, ")" ); fprintf( pFile, "\n" ); } else if ( pNode->Type == DSD_NODE_PRIME ) @@ -664,25 +710,25 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp fCompNew = (int)( pInput != pNode->pDecs[i] ); if ( i ) fprintf( pFile, "," ); + if ( fCompNew ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( pInput->Type == DSD_NODE_BUF ) { pInputNums[i] = 0; - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( fShortNames ) fprintf( pFile, "%d", pInput->S->index ); else fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - if ( fCompNew ) - fprintf( pFile, ")" ); } else { pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); + fprintf( pFile, "<%d>", pInputNums[i] ); } + if ( fCompNew ) + fprintf( pFile, ")" ); } fprintf( pFile, " )\n" ); // call recursively for the following blocks @@ -690,43 +736,39 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp if ( pInputNums[i] ) { pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); + Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); } } else if ( pNode->Type == DSD_NODE_OR ) { // print the line - if ( fComp ) - fprintf( pFile, "AND(" ); - else - fprintf( pFile, "OR(" ); + fprintf( pFile, "OR(" ); for ( i = 0; i < pNode->nDecs; i++ ) { pInput = Dsd_Regular( pNode->pDecs[i] ); fCompNew = (int)( pInput != pNode->pDecs[i] ); if ( i ) fprintf( pFile, "," ); + if ( fCompNew ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( pInput->Type == DSD_NODE_BUF ) { pInputNums[i] = 0; - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( fShortNames ) - fprintf( pFile, "%d", pInput->S->index ); + fprintf( pFile, "%c", 'a' + pInput->S->index ); else fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - if ( fCompNew ) - fprintf( pFile, ")" ); } else { pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); + fprintf( pFile, "<%d>", pInputNums[i] ); } + if ( fCompNew ) + fprintf( pFile, ")" ); } fprintf( pFile, " )\n" ); // call recursively for the following blocks @@ -734,43 +776,208 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp if ( pInputNums[i] ) { pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fComp ^ fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); + Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); } } else if ( pNode->Type == DSD_NODE_EXOR ) { // print the line - if ( fComp ) - fprintf( pFile, "NEXOR(" ); - else - fprintf( pFile, "EXOR(" ); + fprintf( pFile, "EXOR(" ); for ( i = 0; i < pNode->nDecs; i++ ) { pInput = Dsd_Regular( pNode->pDecs[i] ); fCompNew = (int)( pInput != pNode->pDecs[i] ); if ( i ) fprintf( pFile, "," ); + if ( fCompNew ) + fprintf( pFile, " NOT(" ); + else + fprintf( pFile, " " ); if ( pInput->Type == DSD_NODE_BUF ) { pInputNums[i] = 0; - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); if ( fShortNames ) - fprintf( pFile, "%d", pInput->S->index ); + fprintf( pFile, "%c", 'a' + pInput->S->index ); else fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - if ( fCompNew ) - fprintf( pFile, ")" ); + } + else + { + pInputNums[i] = (*pSigCounter)++; + fprintf( pFile, "<%d>", pInputNums[i] ); + } + if ( fCompNew ) + fprintf( pFile, ")" ); + } + fprintf( pFile, " )\n" ); + // call recursively for the following blocks + for ( i = 0; i < pNode->nDecs; i++ ) + if ( pInputNums[i] ) + { + pInput = Dsd_Regular( pNode->pDecs[i] ); + sprintf( Buffer, "<%d>", pInputNums[i] ); + Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); + } + } + free( pInputNums ); +} + +/**Function************************************************************* + + Synopsis [Prints the decompostion tree into file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ) +{ + Dsd_Node_t * pNodeR; + int SigCounter = 1; + pNodeR = Dsd_Regular(pNode); + Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter ); +} + +/**Function************************************************************* + + Synopsis [Prints one node of the decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter ) +{ + char Buffer[100]; + Dsd_Node_t * pInput; + int * pInputNums; + int fCompNew, i; + + assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || + pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); + + Extra_PrintSymbols( pFile, ' ', nOffset, 0 ); + if ( !fComp ) + fprintf( pFile, "%s = ", pOutputName ); + else + fprintf( pFile, "NOT(%s) = ", pOutputName ); + pInputNums = ALLOC( int, pNode->nDecs ); + if ( pNode->Type == DSD_NODE_CONST1 ) + { + fprintf( pFile, " Constant 1.\n" ); + } + else if ( pNode->Type == DSD_NODE_BUF ) + { + fprintf( pFile, " " ); + fprintf( pFile, "%c", 'a' + pNode->S->index ); + fprintf( pFile, "\n" ); + } + else if ( pNode->Type == DSD_NODE_PRIME ) + { + // print the line + fprintf( pFile, "PRIME(" ); + for ( i = 0; i < pNode->nDecs; i++ ) + { + pInput = Dsd_Regular( pNode->pDecs[i] ); + fCompNew = (int)( pInput != pNode->pDecs[i] ); + assert( fCompNew == 0 ); + if ( i ) + fprintf( pFile, "," ); + if ( pInput->Type == DSD_NODE_BUF ) + { + pInputNums[i] = 0; + fprintf( pFile, " %c", 'a' + pInput->S->index ); + } + else + { + pInputNums[i] = (*pSigCounter)++; + fprintf( pFile, " <%d>", pInputNums[i] ); + } + if ( fCompNew ) + fprintf( pFile, "\'" ); + } + fprintf( pFile, " )\n" ); +/* + fprintf( pFile, " ) " ); + { + DdNode * bLocal; + bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd ); Cudd_Ref( bLocal ); + Extra_bddPrint( dd, bLocal ); + Cudd_RecursiveDeref( dd, bLocal ); + } +*/ + // call recursively for the following blocks + for ( i = 0; i < pNode->nDecs; i++ ) + if ( pInputNums[i] ) + { + pInput = Dsd_Regular( pNode->pDecs[i] ); + sprintf( Buffer, "<%d>", pInputNums[i] ); + Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); + } + } + else if ( pNode->Type == DSD_NODE_OR ) + { + // print the line + fprintf( pFile, "OR(" ); + for ( i = 0; i < pNode->nDecs; i++ ) + { + pInput = Dsd_Regular( pNode->pDecs[i] ); + fCompNew = (int)( pInput != pNode->pDecs[i] ); + if ( i ) + fprintf( pFile, "," ); + if ( pInput->Type == DSD_NODE_BUF ) + { + pInputNums[i] = 0; + fprintf( pFile, " %c", 'a' + pInput->S->index ); + } + else + { + pInputNums[i] = (*pSigCounter)++; + fprintf( pFile, " <%d>", pInputNums[i] ); + } + if ( fCompNew ) + fprintf( pFile, "\'" ); + } + fprintf( pFile, " )\n" ); + // call recursively for the following blocks + for ( i = 0; i < pNode->nDecs; i++ ) + if ( pInputNums[i] ) + { + pInput = Dsd_Regular( pNode->pDecs[i] ); + sprintf( Buffer, "<%d>", pInputNums[i] ); + Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); + } + } + else if ( pNode->Type == DSD_NODE_EXOR ) + { + // print the line + fprintf( pFile, "EXOR(" ); + for ( i = 0; i < pNode->nDecs; i++ ) + { + pInput = Dsd_Regular( pNode->pDecs[i] ); + fCompNew = (int)( pInput != pNode->pDecs[i] ); + assert( fCompNew == 0 ); + if ( i ) + fprintf( pFile, "," ); + if ( pInput->Type == DSD_NODE_BUF ) + { + pInputNums[i] = 0; + fprintf( pFile, " %c", 'a' + pInput->S->index ); } else { pInputNums[i] = (*pSigCounter)++; fprintf( pFile, " <%d>", pInputNums[i] ); } + if ( fCompNew ) + fprintf( pFile, "\'" ); } fprintf( pFile, " )\n" ); // call recursively for the following blocks @@ -778,9 +985,8 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp if ( pInputNums[i] ) { pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); + Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); } } free( pInputNums ); diff --git a/src/bdd/epd/epd.c b/src/bdd/epd/epd.c index a843b986..a80240bc 100644 --- a/src/bdd/epd/epd.c +++ b/src/bdd/epd/epd.c @@ -25,7 +25,7 @@ #include <stdlib.h> #include <string.h> #include <math.h> -#include "util.h" +#include "util_hack.h" #include "epd.h" diff --git a/src/bdd/mtr/mtrBasic.c b/src/bdd/mtr/mtrBasic.c index 2aec8d6b..94105282 100644 --- a/src/bdd/mtr/mtrBasic.c +++ b/src/bdd/mtr/mtrBasic.c @@ -33,7 +33,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "mtrInt.h" diff --git a/src/bdd/mtr/mtrGroup.c b/src/bdd/mtr/mtrGroup.c index ae9c5c2f..363b776b 100644 --- a/src/bdd/mtr/mtrGroup.c +++ b/src/bdd/mtr/mtrGroup.c @@ -33,7 +33,7 @@ ******************************************************************************/ -#include "util.h" +#include "util_hack.h" #include "mtrInt.h" /*---------------------------------------------------------------------------*/ diff --git a/src/bdd/parse/module.make b/src/bdd/parse/module.make index ea535e6e..4f590f01 100644 --- a/src/bdd/parse/module.make +++ b/src/bdd/parse/module.make @@ -1,2 +1,3 @@ SRC += src/bdd/parse/parseCore.c \ + src/bdd/parse/parseEqn.c \ src/bdd/parse/parseStack.c diff --git a/src/bdd/parse/parse.h b/src/bdd/parse/parse.h index 8364e782..4923fbdd 100644 --- a/src/bdd/parse/parse.h +++ b/src/bdd/parse/parse.h @@ -36,18 +36,19 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /*=== parseCore.c =============================================================*/ extern DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormula, int nVars, int nRanks, char * ppVarNames[], DdManager * dd, DdNode * pbVars[] ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c index d60687a3..21a37070 100644 --- a/src/bdd/parse/parseCore.c +++ b/src/bdd/parse/parseCore.c @@ -89,7 +89,7 @@ static DdNode * Parse_ParserPerformTopOp( DdManager * dd, Parse_StackFn_t * pStackFn, int Oper ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* diff --git a/src/bdd/parse/parseEqn.c b/src/bdd/parse/parseEqn.c new file mode 100644 index 00000000..02d83966 --- /dev/null +++ b/src/bdd/parse/parseEqn.c @@ -0,0 +1,349 @@ +/**CFile**************************************************************** + + FileNameIn [parseEqn.c] + + PackageName [ABC: Logic synthesis and verification system.] + + Synopsis [Boolean formula parser.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - December 18, 2006.] + + Revision [$Id: parseEqn.c,v 1.0 2006/12/18 00:00:00 alanmi Exp $] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#include "parseInt.h" +#include "vec.h" +#include "hop.h" + +// the list of operation symbols to be used in expressions +#define PARSE_EQN_SYM_OPEN '(' // opening paranthesis +#define PARSE_EQN_SYM_CLOSE ')' // closing paranthesis +#define PARSE_EQN_SYM_CONST0 '0' // constant 0 +#define PARSE_EQN_SYM_CONST1 '1' // constant 1 +#define PARSE_EQN_SYM_NEG '!' // negation before the variable +#define PARSE_EQN_SYM_AND '*' // logic AND +#define PARSE_EQN_SYM_OR '+' // logic OR + +// the list of opcodes (also specifying operation precedence) +#define PARSE_EQN_OPER_NEG 10 // negation +#define PARSE_EQN_OPER_AND 9 // logic AND +#define PARSE_EQN_OPER_OR 7 // logic OR +#define PARSE_EQN_OPER_MARK 1 // OpStack token standing for an opening paranthesis + +// these are values of the internal Flag +#define PARSE_EQN_FLAG_START 1 // after the opening parenthesis +#define PARSE_EQN_FLAG_VAR 2 // after operation is received +#define PARSE_EQN_FLAG_OPER 3 // after operation symbol is received +#define PARSE_EQN_FLAG_ERROR 4 // when error is detected + +#define PARSE_EQN_STACKSIZE 1000 + +static Hop_Obj_t * Parse_ParserPerformTopOp( Hop_Man_t * pMan, Parse_StackFn_t * pStackFn, int Oper ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the AIG corresponding to the equation.] + + Description [Takes the stream to output messages, the formula, the vector + of variable names and the AIG manager.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVarNames, Hop_Man_t * pMan ) +{ + char * pFormula; + Parse_StackFn_t * pStackFn; + Parse_StackOp_t * pStackOp; + Hop_Obj_t * gFunc; + char * pTemp, * pName; + int nParans, fFound, Flag; + int Oper, Oper1, Oper2; + int i, v; + + // make sure that the number of opening and closing parantheses is the same + nParans = 0; + for ( pTemp = pFormInit; *pTemp; pTemp++ ) + if ( *pTemp == '(' ) + nParans++; + else if ( *pTemp == ')' ) + nParans--; + if ( nParans != 0 ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): Different number of opening and closing parantheses ().\n" ); + return NULL; + } + + // copy the formula + pFormula = ALLOC( char, strlen(pFormInit) + 3 ); + sprintf( pFormula, "(%s)", pFormInit ); + + // start the stacks + pStackFn = Parse_StackFnStart( PARSE_EQN_STACKSIZE ); + pStackOp = Parse_StackOpStart( PARSE_EQN_STACKSIZE ); + + Flag = PARSE_EQN_FLAG_START; + for ( pTemp = pFormula; *pTemp; pTemp++ ) + { + switch ( *pTemp ) + { + // skip all spaces, tabs, and end-of-lines + case ' ': + case '\t': + case '\r': + case '\n': + continue; + case PARSE_EQN_SYM_CONST0: + Parse_StackFnPush( pStackFn, Hop_ManConst0(pMan) ); // Cudd_Ref( b0 ); + if ( Flag == PARSE_EQN_FLAG_VAR ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 0.\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + Flag = PARSE_EQN_FLAG_VAR; + break; + case PARSE_EQN_SYM_CONST1: + Parse_StackFnPush( pStackFn, Hop_ManConst1(pMan) ); // Cudd_Ref( b1 ); + if ( Flag == PARSE_EQN_FLAG_VAR ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 1.\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + Flag = PARSE_EQN_FLAG_VAR; + break; + case PARSE_EQN_SYM_NEG: + if ( Flag == PARSE_EQN_FLAG_VAR ) + {// if NEGBEF follows a variable, AND is assumed + Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND ); + Flag = PARSE_EQN_FLAG_OPER; + } + Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_NEG ); + break; + case PARSE_EQN_SYM_AND: + case PARSE_EQN_SYM_OR: + if ( Flag != PARSE_EQN_FLAG_VAR ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): There is no variable before AND, EXOR, or OR.\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + if ( *pTemp == PARSE_EQN_SYM_AND ) + Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND ); + else //if ( *pTemp == PARSE_EQN_SYM_OR ) + Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_OR ); + Flag = PARSE_EQN_FLAG_OPER; + break; + case PARSE_EQN_SYM_OPEN: + if ( Flag == PARSE_EQN_FLAG_VAR ) + { +// Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND ); + fprintf( pOutput, "Parse_FormulaParserEqn(): An opening paranthesis follows a var without operation sign.\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_MARK ); + // after an opening bracket, it feels like starting over again + Flag = PARSE_EQN_FLAG_START; + break; + case PARSE_EQN_SYM_CLOSE: + if ( !Parse_StackOpIsEmpty( pStackOp ) ) + { + while ( 1 ) + { + if ( Parse_StackOpIsEmpty( pStackOp ) ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening paranthesis\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + Oper = Parse_StackOpPop( pStackOp ); + if ( Oper == PARSE_EQN_OPER_MARK ) + break; + + // perform the given operation + if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper ) == NULL ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" ); + free( pFormula ); + return NULL; + } + } + } + else + { + fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening paranthesis\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + if ( Flag != PARSE_EQN_FLAG_ERROR ) + Flag = PARSE_EQN_FLAG_VAR; + break; + + + default: + // scan the next name + for ( i = 0; pTemp[i] && + pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' && + pTemp[i] != PARSE_EQN_SYM_AND && pTemp[i] != PARSE_EQN_SYM_OR && pTemp[i] != PARSE_EQN_SYM_CLOSE; i++ ) + { + if ( pTemp[i] == PARSE_EQN_SYM_NEG || pTemp[i] == PARSE_EQN_SYM_OPEN ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): The negation sign or an opening paranthesis inside the variable name.\n" ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + } + // variable name is found + fFound = 0; + Vec_PtrForEachEntry( vVarNames, pName, v ) + if ( strncmp(pTemp, pName, i) == 0 && strlen(pName) == (unsigned)i ) + { + pTemp += i-1; + fFound = 1; + break; + } + if ( !fFound ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + if ( Flag == PARSE_EQN_FLAG_VAR ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): The variable name \"%s\" follows another var without operation sign.\n", pTemp ); + Flag = PARSE_EQN_FLAG_ERROR; + break; + } + Parse_StackFnPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] ); + Flag = PARSE_EQN_FLAG_VAR; + break; + } + + if ( Flag == PARSE_EQN_FLAG_ERROR ) + break; // error exit + else if ( Flag == PARSE_EQN_FLAG_START ) + continue; // go on parsing + else if ( Flag == PARSE_EQN_FLAG_VAR ) + while ( 1 ) + { // check if there are negations in the OpStack + if ( Parse_StackOpIsEmpty(pStackOp) ) + break; + Oper = Parse_StackOpPop( pStackOp ); + if ( Oper != PARSE_EQN_OPER_NEG ) + { + Parse_StackOpPush( pStackOp, Oper ); + break; + } + else + { + Parse_StackFnPush( pStackFn, Hop_Not(Parse_StackFnPop(pStackFn)) ); + } + } + else // if ( Flag == PARSE_EQN_FLAG_OPER ) + while ( 1 ) + { // execute all the operations in the OpStack + // with precedence higher or equal than the last one + Oper1 = Parse_StackOpPop( pStackOp ); // the last operation + if ( Parse_StackOpIsEmpty(pStackOp) ) + { // if it is the only operation, push it back + Parse_StackOpPush( pStackOp, Oper1 ); + break; + } + Oper2 = Parse_StackOpPop( pStackOp ); // the operation before the last one + if ( Oper2 >= Oper1 ) + { // if Oper2 precedence is higher or equal, execute it + if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper2 ) == NULL ) + { + fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" ); + free( pFormula ); + return NULL; + } + Parse_StackOpPush( pStackOp, Oper1 ); // push the last operation back + } + else + { // if Oper2 precedence is lower, push them back and done + Parse_StackOpPush( pStackOp, Oper2 ); + Parse_StackOpPush( pStackOp, Oper1 ); + break; + } + } + } + + if ( Flag != PARSE_EQN_FLAG_ERROR ) + { + if ( !Parse_StackFnIsEmpty(pStackFn) ) + { + gFunc = Parse_StackFnPop(pStackFn); + if ( Parse_StackFnIsEmpty(pStackFn) ) + if ( Parse_StackOpIsEmpty(pStackOp) ) + { + Parse_StackFnFree(pStackFn); + Parse_StackOpFree(pStackOp); +// Cudd_Deref( gFunc ); + free( pFormula ); + return gFunc; + } + else + fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the operation stack\n" ); + else + fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the function stack\n" ); + } + else + fprintf( pOutput, "Parse_FormulaParserEqn(): The input string is empty\n" ); + } + free( pFormula ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs the operation on the top entries in the stack.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Parse_ParserPerformTopOp( Hop_Man_t * pMan, Parse_StackFn_t * pStackFn, int Oper ) +{ + Hop_Obj_t * gArg1, * gArg2, * gFunc; + // perform the given operation + gArg2 = Parse_StackFnPop( pStackFn ); + gArg1 = Parse_StackFnPop( pStackFn ); + if ( Oper == PARSE_EQN_OPER_AND ) + gFunc = Hop_And( pMan, gArg1, gArg2 ); + else if ( Oper == PARSE_EQN_OPER_OR ) + gFunc = Hop_Or( pMan, gArg1, gArg2 ); + else + return NULL; +// Cudd_Ref( gFunc ); +// Cudd_RecursiveDeref( dd, gArg1 ); +// Cudd_RecursiveDeref( dd, gArg2 ); + Parse_StackFnPush( pStackFn, gFunc ); + return gFunc; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/parse/parseInt.h b/src/bdd/parse/parseInt.h index 6e6c49b0..17f48375 100644 --- a/src/bdd/parse/parseInt.h +++ b/src/bdd/parse/parseInt.h @@ -47,18 +47,18 @@ typedef struct ParseStackOpStruct Parse_StackOp_t; // the operation stack //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /*=== parseStack.c =============================================================*/ extern Parse_StackFn_t * Parse_StackFnStart ( int nDepth ); extern bool Parse_StackFnIsEmpty( Parse_StackFn_t * p ); -extern void Parse_StackFnPush ( Parse_StackFn_t * p, DdNode * bFunc ); -extern DdNode * Parse_StackFnPop ( Parse_StackFn_t * p ); +extern void Parse_StackFnPush ( Parse_StackFn_t * p, void * bFunc ); +extern void * Parse_StackFnPop ( Parse_StackFn_t * p ); extern void Parse_StackFnFree ( Parse_StackFn_t * p ); extern Parse_StackOp_t * Parse_StackOpStart ( int nDepth ); @@ -67,7 +67,8 @@ extern void Parse_StackOpPush ( Parse_StackOp_t * p, int Oper ); extern int Parse_StackOpPop ( Parse_StackOp_t * p ); extern void Parse_StackOpFree ( Parse_StackOp_t * p ); +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif diff --git a/src/bdd/parse/parseStack.c b/src/bdd/parse/parseStack.c index 8329070e..cd7cd7e3 100644 --- a/src/bdd/parse/parseStack.c +++ b/src/bdd/parse/parseStack.c @@ -24,7 +24,7 @@ struct ParseStackFnStruct { - DdNode ** pData; // the array of elements + void ** pData; // the array of elements int Top; // the index int Size; // the stack size }; @@ -37,7 +37,7 @@ struct ParseStackOpStruct }; //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -56,7 +56,7 @@ Parse_StackFn_t * Parse_StackFnStart( int nDepth ) Parse_StackFn_t * p; p = ALLOC( Parse_StackFn_t, 1 ); memset( p, 0, sizeof(Parse_StackFn_t) ); - p->pData = ALLOC( DdNode *, nDepth ); + p->pData = ALLOC( void *, nDepth ); p->Size = nDepth; return p; } @@ -88,7 +88,7 @@ bool Parse_StackFnIsEmpty( Parse_StackFn_t * p ) SeeAlso [] ***********************************************************************/ -void Parse_StackFnPush( Parse_StackFn_t * p, DdNode * bFunc ) +void Parse_StackFnPush( Parse_StackFn_t * p, void * bFunc ) { if ( p->Top >= p->Size ) { @@ -109,7 +109,7 @@ void Parse_StackFnPush( Parse_StackFn_t * p, DdNode * bFunc ) SeeAlso [] ***********************************************************************/ -DdNode * Parse_StackFnPop( Parse_StackFn_t * p ) +void * Parse_StackFnPop( Parse_StackFn_t * p ) { if ( p->Top == 0 ) { diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make index 7eb41e0e..3a636980 100644 --- a/src/bdd/reo/module.make +++ b/src/bdd/reo/module.make @@ -1,6 +1,7 @@ SRC += src/bdd/reo/reoApi.c \ src/bdd/reo/reoCore.c \ src/bdd/reo/reoProfile.c \ + src/bdd/reo/reoShuffle.c \ src/bdd/reo/reoSift.c \ src/bdd/reo/reoSwap.c \ src/bdd/reo/reoTransfer.c \ diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h index 7e4be855..1a31242a 100644 --- a/src/bdd/reo/reo.h +++ b/src/bdd/reo/reo.h @@ -19,10 +19,16 @@ #ifndef __REO_H__ #define __REO_H__ +#ifdef __cplusplus +extern "C" { +#endif + #include <stdio.h> #include <stdlib.h> #include "extra.h" +//#pragma warning( disable : 4514 ) + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -87,9 +93,9 @@ struct _reo_plane struct _reo_hash { int Sign; // signature of the current cache operation - unsigned Arg1; // the first argument - unsigned Arg2; // the second argument - unsigned Arg3; // the second argument + reo_unit * Arg1; // the first argument + reo_unit * Arg2; // the second argument + reo_unit * Arg3; // the third argument }; struct _reo_man @@ -166,8 +172,8 @@ struct _reo_man // used to manipulate units #define Unit_Regular(u) ((reo_unit *)((unsigned long)(u) & ~01)) -#define Unit_Not(u) ((reo_unit *)((long)(u) ^ 01)) -#define Unit_NotCond(u,c) ((reo_unit *)((long)(u) ^ (c))) +#define Unit_Not(u) ((reo_unit *)((unsigned long)(u) ^ 01)) +#define Unit_NotCond(u,c) ((reo_unit *)((unsigned long)(u) ^ (c))) #define Unit_IsConstant(u) ((int)((u)->lev == REO_CONST_LEVEL)) //////////////////////////////////////////////////////////////////////// @@ -215,8 +221,12 @@ extern DdNode * Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermut extern int Extra_bddReorderTest( DdManager * dd, DdNode * bF ); extern int Extra_addReorderTest( DdManager * dd, DdNode * aF ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - -#endif diff --git a/src/bdd/reo/reoProfile.c b/src/bdd/reo/reoProfile.c index b38575f0..84a0bc19 100644 --- a/src/bdd/reo/reoProfile.c +++ b/src/bdd/reo/reoProfile.c @@ -330,7 +330,7 @@ void reoProfileWidthPrint( reo_man * p ) WidthMax = p->pPlanes[i].statsWidth; TotalWidth += p->pPlanes[i].statsWidth; } - assert( p->nWidthCur = TotalWidth ); + assert( p->nWidthCur == TotalWidth ); printf( "WIDTH: " ); printf( "Maximum = %5d. ", WidthMax ); printf( "Total = %7d. ", p->nWidthCur ); diff --git a/src/bdd/reo/reoShuffle.c b/src/bdd/reo/reoShuffle.c new file mode 100644 index 00000000..8dab67a4 --- /dev/null +++ b/src/bdd/reo/reoShuffle.c @@ -0,0 +1,224 @@ +/**CFile**************************************************************** + + FileName [reoShuffle.c] + + PackageName [REO: A specialized DD reordering engine.] + + Synopsis [Implementation of the two-variable swap.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 15, 2002.] + + Revision [$Id: reoShuffle.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "reo.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure is similar to Cudd_ShuffleHeap() and Cudd_bddPermute().] + + Description [The first argument is the REO manager. The 2nd/3d + arguments are the function and its CUDD manager. The last argument + is the permutation to be implemented. The i-th entry of the permutation + array contains the index of the variable that should be brought to the + i-th level. The size of the array should be equal or greater to + the number of variables currently in use (that is, the size of CUDD + manager and the size of REO manager).] + + SideEffects [Note that the resulting BDD is not referenced.] + + SeeAlso [] + +***********************************************************************/ +DdNode * reoShuffle( reo_man * p, DdManager * dd, DdNode * bFunc, int * pPerm, int * pPermInv ) +{ + DdNode * bFuncRes = NULL; + int i, k, v; + + if ( Cudd_IsConstant(bFunc) ) + return bFunc; + + // set the initial parameters + p->dd = dd; + p->nSupp = Cudd_SupportSize( dd, bFunc ); + p->nTops = 1; +// p->nNodesBeg = Cudd_DagSize( bFunc ); + + // set the starting permutation + for ( i = 0; i < p->nSupp; i++ ) + { + p->pOrderInt[i] = i; + p->pMapToPlanes[ dd->invperm[i] ] = i; + p->pMapToDdVarsFinal[i] = dd->invperm[i]; + } + + // set the initial parameters + p->nUnitsUsed = 0; + p->nNodesCur = 0; + p->fThisIsAdd = 0; + p->Signature++; + + // transfer the function from the CUDD package into REO's internal data structure + p->pTops[0] = reoTransferNodesToUnits_rec( p, bFunc ); +// assert( p->nNodesBeg == p->nNodesCur ); + + // reorder one variable at a time + for ( i = 0; i < p->nSupp; i++ ) + { + if ( p->pOrderInt[i] == pPerm[i] ) + continue; + // find where is variable number pPerm[i] + for ( k = i + 1; k < p->nSupp; k++ ) + if ( pPerm[i] == p->pOrderInt[k] ) + break; + if ( k == p->nSupp ) + { + printf( "reoShuffle() Error: Cannot find a variable.\n" ); + goto finish; + } + // move the variable up + for ( v = k - 1; v >= i; v-- ) + { + reoReorderSwapAdjacentVars( p, v, 1 ); + // check if the number of nodes is not too large + if ( p->nNodesCur > 10000 ) + { + printf( "reoShuffle() Error: BDD size is too large.\n" ); + goto finish; + } + } + assert( p->pOrderInt[i] == pPerm[i] ); + } + + // set the initial parameters + p->nRefNodes = 0; + p->nNodesCur = 0; + p->Signature++; + // transfer the BDDs from REO's internal data structure to CUDD + bFuncRes = reoTransferUnitsToNodes_rec( p, p->pTops[0] ); Cudd_Ref( bFuncRes ); + // undo the DDs referenced for storing in the cache + for ( i = 0; i < p->nRefNodes; i++ ) + Cudd_RecursiveDeref( dd, p->pRefNodes[i] ); + + // verify zero refs of the terminal nodes +// assert( reoRecursiveDeref( p->pTops[0] ) ); +// assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) ); + + // perform verification + if ( p->fVerify ) + { + DdNode * bFuncPerm; + bFuncPerm = Cudd_bddPermute( dd, bFunc, pPermInv ); Cudd_Ref( bFuncPerm ); + if ( bFuncPerm != bFuncRes ) + { + printf( "REO: Internal verification has failed!\n" ); + fflush( stdout ); + } + Cudd_RecursiveDeref( dd, bFuncPerm ); + } + + // recycle the data structure + for ( i = 0; i <= p->nSupp; i++ ) + reoUnitsRecycleUnitList( p, p->pPlanes + i ); + +finish : + if ( bFuncRes ) + Cudd_Deref( bFuncRes ); + return bFuncRes; +} + + + +/**Function************************************************************* + + Synopsis [Reorders the DD using REO and CUDD.] + + Description [This function can be used to test the performance of the reordering package.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func ) +{ +// extern int runtime1, runtime2; + + DdNode * Temp, * bRemap; + int nSuppSize, OffSet, Num, i, clk; + int pOrder[1000], pOrderInv[1000]; + assert( dd->size < 1000 ); + + srand( 0x12341234 ); + nSuppSize = Cudd_SupportSize( dd, Func ); + if ( nSuppSize < 2 ) + return; + + for ( i = 0; i < nSuppSize; i++ ) + pOrder[i] = i; + for ( i = 0; i < 120; i++ ) + { + OffSet = rand() % (nSuppSize - 1); + Num = pOrder[OffSet]; + pOrder[OffSet] = pOrder[OffSet+1]; + pOrder[OffSet+1] = Num; + } + for ( i = 0; i < nSuppSize; i++ ) + pOrderInv[pOrder[i]] = i; + +/* + printf( "Permutation: " ); + for ( i = 0; i < nSuppSize; i++ ) + printf( "%d ", pOrder[i] ); + printf( "\n" ); + printf( "Inverse permutation: " ); + for ( i = 0; i < nSuppSize; i++ ) + printf( "%d ", pOrderInv[i] ); + printf( "\n" ); +*/ + + // create permutation +// Extra_ReorderSetVerification( pReo, 1 ); + bRemap = Extra_bddRemapUp( dd, Func ); Cudd_Ref( bRemap ); + +clk = clock(); + Temp = reoShuffle( pReo, dd, bRemap, pOrder, pOrderInv ); Cudd_Ref( Temp ); +//runtime1 += clock() - clk; + +//printf( "Initial = %d. Final = %d.\n", Cudd_DagSize(bRemap), Cudd_DagSize(Temp) ); + + { + DdNode * bFuncPerm; +clk = clock(); + bFuncPerm = Cudd_bddPermute( dd, bRemap, pOrderInv ); Cudd_Ref( bFuncPerm ); +//runtime2 += clock() - clk; + if ( bFuncPerm != Temp ) + { + printf( "REO: Internal verification has failed!\n" ); + fflush( stdout ); + } + Cudd_RecursiveDeref( dd, bFuncPerm ); + } + + Cudd_RecursiveDeref( dd, Temp ); + Cudd_RecursiveDeref( dd, bRemap ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c index cb730d8e..4afa650c 100644 --- a/src/bdd/reo/reoSwap.c +++ b/src/bdd/reo/reoSwap.c @@ -271,9 +271,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp ) HKey = (HKey+1) % p->nTableSize ); assert( p->HTable[HKey].Sign != p->Signature ); p->HTable[HKey].Sign = p->Signature; - p->HTable[HKey].Arg1 = (unsigned)pUnitE; - p->HTable[HKey].Arg2 = (unsigned)pUnitT; - p->HTable[HKey].Arg3 = (unsigned)pUnit; + p->HTable[HKey].Arg1 = pUnitE; + p->HTable[HKey].Arg2 = pUnitT; + p->HTable[HKey].Arg3 = pUnit; nNodesUpMovedDown++; @@ -512,10 +512,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp ) for ( HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ) - if ( p->HTable[HKey].Arg1 == (unsigned)pNew1E && p->HTable[HKey].Arg2 == (unsigned)pNew1T ) + if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T ) { // the entry is present // assign this entry - pNewPlane20 = (reo_unit *)p->HTable[HKey].Arg3; + pNewPlane20 = p->HTable[HKey].Arg3; assert( pNewPlane20->lev == lev1 ); fFound = 1; p->HashSuccess++; @@ -549,9 +549,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp ) // add this entry to cache assert( p->HTable[HKey].Sign != p->Signature ); p->HTable[HKey].Sign = p->Signature; - p->HTable[HKey].Arg1 = (unsigned)pNew1E; - p->HTable[HKey].Arg2 = (unsigned)pNew1T; - p->HTable[HKey].Arg3 = (unsigned)pNewPlane20; + p->HTable[HKey].Arg1 = pNew1E; + p->HTable[HKey].Arg2 = pNew1T; + p->HTable[HKey].Arg3 = pNewPlane20; nNodesUnrefAdded++; @@ -637,10 +637,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp ) for ( HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ) - if ( p->HTable[HKey].Arg1 == (unsigned)pNew2E && p->HTable[HKey].Arg2 == (unsigned)pNew2T ) + if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T ) { // the entry is present // assign this entry - pNewPlane21 = (reo_unit *)p->HTable[HKey].Arg3; + pNewPlane21 = p->HTable[HKey].Arg3; assert( pNewPlane21->lev == lev1 ); fFound = 1; p->HashSuccess++; @@ -675,9 +675,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp ) // add this entry to cache assert( p->HTable[HKey].Sign != p->Signature ); p->HTable[HKey].Sign = p->Signature; - p->HTable[HKey].Arg1 = (unsigned)pNew2E; - p->HTable[HKey].Arg2 = (unsigned)pNew2T; - p->HTable[HKey].Arg3 = (unsigned)pNewPlane21; + p->HTable[HKey].Arg1 = pNew2E; + p->HTable[HKey].Arg2 = pNew2T; + p->HTable[HKey].Arg3 = pNewPlane21; nNodesUnrefAdded++; diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c index 752cd3d7..65d31d01 100644 --- a/src/bdd/reo/reoTransfer.c +++ b/src/bdd/reo/reoTransfer.c @@ -51,9 +51,9 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F ) { // search cache - use linear probing for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ) - if ( p->HTable[HKey].Arg1 == (unsigned)F ) + if ( p->HTable[HKey].Arg1 == (reo_unit *)F ) { - pUnit = (reo_unit*) p->HTable[HKey].Arg2; + pUnit = p->HTable[HKey].Arg2; assert( pUnit ); // increment the edge counter pUnit->n++; @@ -93,8 +93,8 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F ) // might have been used. Make sure that its signature is different. for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ); p->HTable[HKey].Sign = p->Signature; - p->HTable[HKey].Arg1 = (unsigned)F; - p->HTable[HKey].Arg2 = (unsigned)pUnit; + p->HTable[HKey].Arg1 = (reo_unit *)F; + p->HTable[HKey].Arg2 = pUnit; } // increment the counter of nodes @@ -126,7 +126,7 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit ) if ( pUnit->n != 1 ) { for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ) - if ( p->HTable[HKey].Arg1 == (unsigned)pUnit ) + if ( p->HTable[HKey].Arg1 == pUnit ) { bRes = (DdNode*) p->HTable[HKey].Arg2; assert( bRes ); @@ -179,8 +179,8 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit ) // might have been used. Make sure that its signature is different. for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize ); p->HTable[HKey].Sign = p->Signature; - p->HTable[HKey].Arg1 = (unsigned)pUnit; - p->HTable[HKey].Arg2 = (unsigned)bRes; + p->HTable[HKey].Arg1 = pUnit; + p->HTable[HKey].Arg2 = (reo_unit *)bRes; // add the DD to the referenced DD list in order to be able to store it in cache p->pRefNodes[p->nRefNodes++] = bRes; Cudd_Ref( bRes ); |