src/base/abci/abcCas.c File Reference

#include "abc.h"

Include dependency graph for abcCas.c:

Functions
int	Abc_CascadeExperiment (char pFileGeneric, DdManager dd, DdNode **pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose)
Abc_Ntk_t *	Abc_NtkCascade (Abc_Ntk_t *pNtk, int nLutSize, int fCheck, int fVerbose)

Function Documentation

int Abc_CascadeExperiment	(	char *	pFileGeneric,
		DdManager *	dd,
		DdNode **	pOutputs,
		int	nInputs,
		int	nOutputs,
		int	nLutSize,
		int	fCheck,
		int	fVerbose
	)

CFile****************************************************************

FileName [abcCas.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Decomposition of shared BDDs into LUT cascade.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id: abcCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

EXTERNAL FUNCTIONS ///Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file casCore.c.

00076 {
00077     int i;
00078     int nVars = nInputs;
00079     int nOuts = nOutputs;
00080     long clk1;
00081 
00082     int      nVarsEnc;              // the number of additional variables to encode outputs
00083     DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
00084 
00085     int      nNames;               // the total number of all inputs
00086     char *   pNames[MAXINPUTS];     // the temporary storage for the input (and output encoding) names
00087 
00088     DdNode * aFunc;                 // the encoded 0-1 BDD containing all the outputs
00089 
00090     char FileNameIni[100];
00091     char FileNameFin[100];
00092     char Buffer[100];
00093 
00094     
00095 //pTable = fopen( "stats.txt", "a+" );
00096 //fprintf( pTable, "%s ", pFileGeneric );
00097 //fprintf( pTable, "%d ", nVars );
00098 //fprintf( pTable, "%d ", nOuts );
00099 
00100 
00101     // assign the file names
00102     strcpy( FileNameIni, pFileGeneric );
00103     strcat( FileNameIni, "_ENC.blif" );
00104 
00105     strcpy( FileNameFin, pFileGeneric );
00106     strcat( FileNameFin, "_LUT.blif" );
00107 
00108 
00109     // create the variables to encode the outputs
00110     nVarsEnc = Extra_Base2Log( nOuts );
00111     for ( i = 0; i < nVarsEnc; i++ )
00112         pbVarsEnc[i] = Cudd_bddNewVarAtLevel( dd, i );
00113 
00114 
00115     // store the input names
00116     nNames  = nVars + nVarsEnc;
00117     for ( i = 0; i < nVars; i++ )
00118     {
00119 //      pNames[i] = Extra_UtilStrsav( pFunc->pInputNames[i] );
00120         sprintf( Buffer, "pi%03d", i );
00121         pNames[i] = Extra_UtilStrsav( Buffer );
00122     }
00123     // set the encoding variable name
00124     for ( ; i < nNames; i++ )
00125     {       
00126         sprintf( Buffer, "OutEnc_%02d", i-nVars );
00127         pNames[i] = Extra_UtilStrsav( Buffer );
00128     }
00129 
00130 
00131     // print the variable order
00132 //  printf( "\n" );
00133 //  printf( "Variable order is: " );
00134 //  for ( i = 0; i < dd->size; i++ )
00135 //      printf( " %d", dd->invperm[i] );
00136 //  printf( "\n" );
00137 
00138     // derive the single-output function
00139     clk1 = clock();
00140     aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose );  Cudd_Ref( aFunc );
00141 //  aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
00142 //  if ( fVerbose )
00143 //  printf( "Single-output function computation time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
00144  
00145 //fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) );
00146 //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) );
00147 
00148     // dispose of the multiple-output function
00149 //  Extra_Dissolve( pFunc );
00150  
00151     // reorder the single output function
00152 //    if ( fVerbose )
00153 //  printf( "Reordering variables...\n");
00154     clk1 = clock();
00155 //  if ( fVerbose )
00156 //  printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) );
00157 //  Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1);
00158     Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
00159     Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
00160 //  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
00161 //  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
00162 //  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
00163 //  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
00164     if ( fVerbose )
00165     printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) );
00166     if ( fVerbose )
00167     printf( "Variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
00168 //  printf( "\n" );
00169 //  printf( "Variable order is: " );
00170 //  for ( i = 0; i < dd->size; i++ )
00171 //      printf( " %d", dd->invperm[i] );
00172 //  printf( "\n" );
00173 //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
00174 //fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) );
00175 
00176     // write the single-output function into BLIF for verification
00177     clk1 = clock();
00178     if ( fCheck )
00179     WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
00180 //    if ( fVerbose )
00181 //  printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
00182 
00183 /*
00185     // verification of single output function
00186     clk1 = clock();
00187     {
00188         BFunc g_Func;
00189         DdNode * aRes;
00190 
00191         g_Func.dd = dd;
00192         g_Func.FileInput = Extra_UtilStrsav(FileNameIni);
00193 
00194         if ( Extra_ReadFile( &g_Func ) == 0 )
00195         {
00196             printf( "\nSomething did not work out while reading the input file for verification\n");
00197             Extra_Dissolve( &g_Func );
00198             return;
00199         } 
00200 
00201         aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] );  Cudd_Ref( aRes );
00202 
00203         if ( aRes != aFunc )
00204             printf( "\nVerification FAILED!\n");
00205         else
00206             printf( "\nVerification okay!\n");
00207         
00208         Cudd_RecursiveDeref( dd, aRes );
00209 
00210         // delocate
00211         Extra_Dissolve( &g_Func );
00212     }
00213     printf( "Preliminary verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
00215 */
00216 
00217     if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) )
00218         return 0;
00219 
00220 /*
00222     // verification of the decomposed LUT network
00223     clk1 = clock();
00224     {
00225         BFunc g_Func;
00226         DdNode * aRes;
00227 
00228         g_Func.dd = dd;
00229         g_Func.FileInput = Extra_UtilStrsav(FileNameFin);
00230 
00231         if ( Extra_ReadFile( &g_Func ) == 0 )
00232         {
00233             printf( "\nSomething did not work out while reading the input file for verification\n");
00234             Extra_Dissolve( &g_Func );
00235             return;
00236         } 
00237 
00238         aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] );  Cudd_Ref( aRes );
00239 
00240         if ( aRes != aFunc )
00241             printf( "\nFinal verification FAILED!\n");
00242         else
00243             printf( "\nFinal verification okay!\n");
00244         
00245         Cudd_RecursiveDeref( dd, aRes );
00246  
00247         // delocate 
00248         Extra_Dissolve( &g_Func );
00249     }
00250     printf( "Final verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
00252 */
00253  
00254     // verify the results
00255     if ( fCheck )
00256     {
00257         extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
00258         extern void * Abc_FrameGetGlobalFrame();
00259         char Command[200];
00260         sprintf( Command, "cec %s %s", FileNameIni, FileNameFin );
00261         Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
00262     }
00263 
00264     Cudd_RecursiveDeref( dd, aFunc );
00265 
00266     // release the names
00267     for ( i = 0; i < nNames; i++ )
00268         free( pNames[i] );
00269 
00270 
00271 //fprintf( pTable, "\n" );
00272 //fclose( pTable );
00273 
00274     return 1;
00275 }

Abc_Ntk_t* Abc_NtkCascade	(	Abc_Ntk_t *	pNtk,
		int	nLutSize,
		int	fCheck,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file abcCas.c.

00053 00054 00055 00056 00057 00058 00059 00060 00061 00062 00063 00064 00065 00066 00067 00068     { 00069 00070 00071 00072     } 00073 00074 00075 00076 00077 00078 00079 00080 00081 00082 00083     { 00084 00085     } 00086 00087 00088 00089 00090 00091 00092 00093 00094 00095 00096 00097 00098 00099     { 00100 00101 00102 00103     } 00104 00105 }

class="fragment">00052 { DdManager * dd; DdNode ** ppOutputs; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode; char * pFileGeneric; int fBddSizeMax = 500000; int fReorder = 1; int i, clk = clock(); assert( Abc_NtkIsStrash(pNtk) ); // compute the global BDDs if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL ) return NULL; if ( fVerbose ) DdManager * dd = Abc_NtkGlobalBddMan( pNtk ); printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); PRT( "BDD construction time", clock() - clk ); // collect global BDDs dd = Abc_NtkGlobalBddMan( pNtk ); ppOutputs = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) ppOutputs[i] = Abc_ObjGlobalBdd(pNode); // call the decomposition pFileGeneric = Extra_FileNameGeneric( pNtk->pSpec ); if ( !Abc_CascadeExperiment( pFileGeneric, dd, ppOutputs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), nLutSize, fCheck, fVerbose ) ) // the LUT size is too small // for now, duplicate the network pNtkNew = Abc_NtkDup( pNtk ); // cleanup Abc_NtkFreeGlobalBdds( pNtk, 1 ); free( ppOutputs ); free( pFileGeneric ); // if ( pNtk->pExdc ) // pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) printf( "Abc_NtkCollapse: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); return NULL; return pNtkNew;

src/base/abci/abcCas.c File Reference

Functions

Function Documentation