diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraClaus.c | 6 | ||||
-rw-r--r-- | src/aig/fra/fraHot.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 6 | ||||
-rw-r--r-- | src/base/abc/abcDfs.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 39 | ||||
-rw-r--r-- | src/base/abci/abcGen.c | 42 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 1 | ||||
-rw-r--r-- | src/base/cmd/cmd.c | 254 | ||||
-rw-r--r-- | src/base/io/ioReadBlif.c | 15 | ||||
-rw-r--r-- | src/base/io/ioReadBlifMv.c | 29 | ||||
-rw-r--r-- | src/misc/vec/vecPtr.h | 18 | ||||
-rw-r--r-- | src/opt/mfs/mfs.h | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsCore.c | 20 | ||||
-rw-r--r-- | src/opt/mfs/mfsInt.h | 8 | ||||
-rw-r--r-- | src/opt/mfs/mfsMan.c | 17 | ||||
-rw-r--r-- | src/opt/mfs/mfsResub.c | 307 |
17 files changed, 672 insertions, 98 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 339fd810..64268358 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -39,7 +39,7 @@ extern "C" { #include "aig.h" #include "dar.h" #include "satSolver.h" -//#include "bar.h" +#include "ioa.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index a35e1169..8e3a03e1 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -1530,7 +1530,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p ) extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); Aig_Man_t * pNew; Aig_Obj_t * pClause, * pLiteral; - char Buffer[500]; + char Buffer[500], * pName; int * pStart, * pVar2Id; int Beg, End, i, k; // create mapping from SAT vars to node IDs @@ -1561,7 +1561,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p ) free( pVar2Id ); Aig_ManCleanup( pNew ); // write the manager into a file - sprintf( Buffer, "%s_care.aig", p->pAig->pName ); + pName = Ioa_FileNameGeneric(p->pAig->pName); + sprintf( Buffer, "%s_care.aig", pName ); + free( pName ); printf( "Care clauses are written into file \"%s\".\n", Buffer ); Ioa_WriteAiger( pNew, Buffer, 0, 1 ); Aig_ManStop( pNew ); diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index 4a3f9b03..8796f827 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -130,7 +130,7 @@ int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * p ***********************************************************************/ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ) { - int fSkipConstEqu = 1; + int fSkipConstEqu = 0; Vec_Int_t * vOneHots; Aig_Obj_t * pObj1, * pObj2; int i, k; diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 07044b52..ea17706c 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -471,12 +471,14 @@ clk2 = clock(); if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) ) { extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); - char Buffer[500]; + char Buffer[500], * pStart; Aig_Man_t * pNew; pManAigNew = Aig_ManDup( pManAig, 1 ); // pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots ); pNew = Fra_OneHotCreateExdc( p, p->vOneHots ); - sprintf( Buffer, "%s_care.aig", p->pManAig->pName ); + pStart = Ioa_FileNameGeneric(p->pManAig->pName); + sprintf( Buffer, "%s_care.aig", pStart ); + free( pStart ); printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer ); Ioa_WriteAiger( pNew, Buffer, 0, 1 ); Aig_ManStop( pNew ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index de517705..c882672b 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -1025,7 +1025,7 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk ) return LevelsMax; } - + /**Function************************************************************* Synopsis [Recursively detects combinational loops.] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 266f8075..4b872aa3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3130,7 +3130,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nWindow = 62; pPars->nCands = 5; pPars->nSimWords = 4; - pPars->nGrowthLevel = 0; + pPars->nGrowthLevel = 1; pPars->fArea = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; @@ -3225,7 +3225,7 @@ usage: fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands ); fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords ); - fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); @@ -3264,13 +3264,15 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nDepthMax = 20; pPars->nDivMax = 200; pPars->nWinSizeMax = 300; - pPars->nGrowthLevel = 0; + pPars->nGrowthLevel = 1; pPars->fResub = 1; pPars->fArea = 0; + pPars->fMoreEffort = 0; + pPars->fSwapEdge = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLravwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLraesvwh" ) ) != EOF ) { switch ( c ) { @@ -3335,6 +3337,12 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fArea ^= 1; break; + case 'e': + pPars->fMoreEffort ^= 1; + break; + case 's': + pPars->fSwapEdge ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -3368,15 +3376,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: mfs [-WFDML <num>] [-arvh]\n" ); + fprintf( pErr, "usage: mfs [-WFDML <num>] [-raesvh]\n" ); fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" ); fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax ); fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax ); fprintf( pErr, "\t-M <num> : the max size of window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); - fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); - fprintf( pErr, "\t-a : toggle minimizing area or edges [default = %s]\n", pPars->fArea? "area": "edges" ); + fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); fprintf( pErr, "\t-r : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" ); + fprintf( pErr, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); + fprintf( pErr, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" ); + fprintf( pErr, "\t-s : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -6208,12 +6218,14 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSorter; int fMesh; int fFpga; + int fOneHot; int fVerbose; char * FileName; extern void Abc_GenAdder( char * pFileName, int nVars ); extern void Abc_GenSorter( char * pFileName, int nVars ); extern void Abc_GenMesh( char * pFileName, int nVars ); extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars ); + extern void Abc_GenOneHot( char * pFileName, int nVars ); pNtk = Abc_FrameReadNtk(pAbc); @@ -6226,9 +6238,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) fSorter = 0; fMesh = 0; fFpga = 0; + fOneHot = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftvh" ) ) != EOF ) { switch ( c ) { @@ -6255,6 +6268,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': fFpga ^= 1; break; + case 't': + fOneHot ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6282,18 +6298,21 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_GenFpga( FileName, 4, 3, 10 ); // Abc_GenFpga( FileName, 2, 2, 3 ); // Abc_GenFpga( FileName, 3, 2, 5 ); + else if ( fOneHot ) + Abc_GenOneHot( FileName, nVars ); else printf( "Type of circuit is not specified.\n" ); return 0; usage: - fprintf( pErr, "usage: gen [-N] [-asmfvh] <file>\n" ); + fprintf( pErr, "usage: gen [-N num] [-asmftvh] <file>\n" ); fprintf( pErr, "\t generates simple circuits\n" ); fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars ); fprintf( pErr, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" ); fprintf( pErr, "\t-s : generate a sorter [default = %s]\n", fSorter? "yes": "no" ); fprintf( pErr, "\t-m : generate a mesh [default = %s]\n", fMesh? "yes": "no" ); fprintf( pErr, "\t-f : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" ); + fprintf( pErr, "\t-t : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t<file> : output file name\n"); @@ -6634,7 +6653,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); - extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); +// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); // extern void Abc_NtkDarTestBlif( char * pFileName ); diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c index bfb41374..0b66c476 100644 --- a/src/base/abci/abcGen.c +++ b/src/base/abci/abcGen.c @@ -504,6 +504,48 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars ) fclose( pFile ); } +/**Function************************************************************* + + Synopsis [Generates structure of L K-LUTs implementing an N-var function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_GenOneHot( char * pFileName, int nVars ) +{ + FILE * pFile; + int i, k, Counter, nDigitsIn, nDigitsOut; + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# One-hotness condition for %d vars generated by ABC on %s\n", nVars, Extra_TimeStamp() ); + fprintf( pFile, ".model 1hot_%dvars\n", nVars ); + fprintf( pFile, ".inputs" ); + nDigitsIn = Extra_Base10Log( nVars ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " i%0*d", nDigitsIn, i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".outputs" ); + nDigitsOut = Extra_Base10Log( nVars * (nVars - 1) / 2 ); + for ( i = 0; i < nVars * (nVars - 1) / 2; i++ ) + fprintf( pFile, " o%0*d", nDigitsOut, i ); + fprintf( pFile, "\n" ); + Counter = 0; + for ( i = 0; i < nVars; i++ ) + for ( k = i+1; k < nVars; k++ ) + { + fprintf( pFile, ".names i%0*d i%0*d o%0*d\n", nDigitsIn, i, nDigitsIn, k, nDigitsOut, Counter ); + fprintf( pFile, "11 0\n" ); + Counter++; + } + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 257d930f..a054a474 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -1130,6 +1130,7 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ) pNode = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pNode, pMiter ); Abc_ObjAssignName( pNode, "miter", NULL ); + Abc_NtkOrderCisCos( pNtk ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 2dc03d5c..8640b7a8 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -46,6 +46,7 @@ static int CmdCommandRecall ( Abc_Frame_t * pAbc, int argc, char ** argv static int CmdCommandEmpty ( Abc_Frame_t * pAbc, int argc, char ** argv ); #ifdef WIN32 static int CmdCommandLs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int CmdCommandScrGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); #endif static int CmdCommandSis ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandMvsis ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -86,6 +87,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "empty", CmdCommandEmpty, 0); #ifdef WIN32 Cmd_CommandAdd( pAbc, "Basic", "ls", CmdCommandLs, 0 ); + Cmd_CommandAdd( pAbc, "Basic", "scrgen", CmdCommandScrGen, 0 ); #endif Cmd_CommandAdd( pAbc, "Various", "sis", CmdCommandSis, 1); @@ -1068,17 +1070,6 @@ usage: #ifdef WIN32 -/**Function************************************************************* - - Synopsis [Command to print the contents of the current directory (Windows).] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ #include <io.h> // these structures are defined in <io.h> but are for some reason invisible @@ -1097,6 +1088,20 @@ extern long _findfirst( char *filespec, struct _finddata_t *fileinfo ); extern int _findnext( long handle, struct _finddata_t *fileinfo ); extern int _findclose( long handle ); +extern char * _getcwd( char * buffer, int maxlen ); +extern int _chdir( const char *dirname ); + +/**Function************************************************************* + + Synopsis [Command to print the contents of the current directory (Windows).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv ) { struct _finddata_t c_file; @@ -1181,15 +1186,238 @@ int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "Usage: ls [-l] [-b]\n" ); + fprintf( pAbc->Err, "usage: ls [-l] [-b]\n" ); fprintf( pAbc->Err, " print the file names in the current directory\n" ); fprintf( pAbc->Err, " -l : print in the long format [default = short]\n" ); fprintf( pAbc->Err, " -b : print only .mv files [default = all]\n" ); return 1; } -#endif +/**Function************************************************************* + + Synopsis [Generates the script for running ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + struct _finddata_t c_file; + long hFile; + FILE * pFile = NULL; + char * pFileStr = "test.s"; + char * pDirStr = NULL; + char * pComStr = "ps"; + char * pWriteStr = NULL; + char Buffer[1000], Line[2000]; + int nFileNameMax, nFileNameCur; + int Counter = 0; + int fUseCurrent; + char c; + + fUseCurrent = 0; + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "FDCWch") ) != EOF ) + { + switch (c) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pAbc->Err, "Command line switch \"-F\" should be followed by a string.\n" ); + goto usage; + } + pFileStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( pAbc->Err, "Command line switch \"-D\" should be followed by a string.\n" ); + goto usage; + } + pDirStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pAbc->Err, "Command line switch \"-C\" should be followed by a string.\n" ); + goto usage; + } + pComStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + fprintf( pAbc->Err, "Command line switch \"-W\" should be followed by a string.\n" ); + goto usage; + } + pWriteStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'c': + fUseCurrent ^= 1; + break; + default: + goto usage; + } + } + +// printf( "File = %s.\n", pFileStr ); +// printf( "Dir = %s.\n", pDirStr ); +// printf( "Com = %s.\n", pComStr ); + if ( pDirStr == NULL ) + fUseCurrent = 1; + + if ( _getcwd( Buffer, 1000 ) == NULL ) + { + printf( "Cannot get the current directory.\n" ); + return 0; + } + if ( fUseCurrent ) + pFile = fopen( pFileStr, "w" ); + if ( pDirStr ) + { + if ( _chdir(pDirStr) ) + { + printf( "Cannot change to directory: %s\n", pDirStr ); + return 0; + } + } + if ( !fUseCurrent ) + pFile = fopen( pFileStr, "w" ); + if ( pFile == NULL ) + { + printf( "Cannot open file %s.\n", pFileStr ); + if ( pDirStr && _chdir(Buffer) ) + { + printf( "Cannot change to the current directory: %s\n", Buffer ); + return 0; + } + return 0; + } + + // find the first file in the directory + if( (hFile = _findfirst( "*.*", &c_file )) == -1L ) + { + if ( pDirStr ) + printf( "No files in the current directory.\n" ); + else + printf( "No files in directory: %s\n", pDirStr ); + if ( pDirStr && _chdir(Buffer) ) + { + printf( "Cannot change to the current directory: %s\n", Buffer ); + return 0; + } + } + + // get the longest file name + { + nFileNameMax = 0; + do + { + // skip script and txt files + nFileNameCur = strlen(c_file.name); + if ( c_file.name[nFileNameCur-1] == '.' ) + continue; + if ( nFileNameCur > 2 && + c_file.name[nFileNameCur-1] == 's' && + c_file.name[nFileNameCur-2] == '.' ) + continue; + if ( nFileNameCur > 4 && + c_file.name[nFileNameCur-1] == 't' && + c_file.name[nFileNameCur-2] == 'x' && + c_file.name[nFileNameCur-3] == 't' && + c_file.name[nFileNameCur-4] == '.' ) + continue; + if ( nFileNameMax < nFileNameCur ) + nFileNameMax = nFileNameCur; + } + while( _findnext( hFile, &c_file ) == 0 ); + _findclose( hFile ); + } + + // print the script file + { + if( (hFile = _findfirst( "*.*", &c_file )) == -1L ) + { + if ( pDirStr ) + printf( "No files in the current directory.\n" ); + else + printf( "No files in directory: %s\n", pDirStr ); + } + fprintf( pFile, "# Script file produced by ABC on %s\n", Extra_TimeStamp() ); + fprintf( pFile, "# Command line was: scrgen -F %s -D %s -C \"%s\"%s%s\n", + pFileStr, pDirStr, pComStr, pWriteStr?" -W ":"", pWriteStr?pWriteStr:"" ); + do + { + // skip script and txt files + nFileNameCur = strlen(c_file.name); + if ( c_file.name[nFileNameCur-1] == '.' ) + continue; + if ( nFileNameCur > 2 && + c_file.name[nFileNameCur-1] == 's' && + c_file.name[nFileNameCur-2] == '.' ) + continue; + if ( nFileNameCur > 4 && + c_file.name[nFileNameCur-1] == 't' && + c_file.name[nFileNameCur-2] == 'x' && + c_file.name[nFileNameCur-3] == 't' && + c_file.name[nFileNameCur-4] == '.' ) + continue; + sprintf( Line, "r %s%s%-*s ; %s", pDirStr?pDirStr:"", pDirStr?"/":"", nFileNameMax, c_file.name, pComStr ); + for ( c = (int)strlen(Line)-1; c >= 0; c-- ) + if ( Line[c] == '\\' ) + Line[c] = '/'; + fprintf( pFile, "%s", Line ); + if ( pWriteStr ) + { + sprintf( Line, " ; w %s/%-*s", pWriteStr, nFileNameMax, c_file.name ); + for ( c = (int)strlen(Line)-1; c >= 0; c-- ) + if ( Line[c] == '\\' ) + Line[c] = '/'; + fprintf( pFile, "%s", Line ); + } + fprintf( pFile, "\n", Line ); + } + while( _findnext( hFile, &c_file ) == 0 ); + _findclose( hFile ); + } + fclose( pFile ); + if ( pDirStr && _chdir(Buffer) ) + { + printf( "Cannot change to the current directory: %s\n", Buffer ); + return 0; + } + + // report + if ( fUseCurrent ) + printf( "Script file \"%s\" was saved in the current directory.\n", pFileStr ); + else + printf( "Script file \"%s\" was saved in directory: %s\n", pFileStr, pDirStr ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: scrgen -F <str> -D <str> -C <str> -W <str> -ch\n" ); + fprintf( pAbc->Err, "\t generates script for running ABC\n" ); + fprintf( pAbc->Err, "\t-F str : the name of the script file [default = \"test.s\"]\n" ); + fprintf( pAbc->Err, "\t-D str : the directory to read files from [default = current]\n" ); + fprintf( pAbc->Err, "\t-C str : the sequence of commands to run [default = \"ps\"]\n" ); + fprintf( pAbc->Err, "\t-W str : the directory to write the resulting files [default = no writing]\n" ); + fprintf( pAbc->Err, "\t-c : toggle placing file in current/target dir [default = %s]\n", fUseCurrent? "current": "target" ); + fprintf( pAbc->Err, "\t-h : print the command usage\n\n"); + fprintf( pAbc->Err, "\tExample : scrgen -F test1.s -D a/in -C \"ps; st; ps\" -W a/out\n" ); + return 1; +} +#endif + #ifdef WIN32 #define unlink _unlink diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index d0750178..ffa25c7f 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -218,7 +218,20 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p ) p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 ); // read the model name if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 ) - pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] ); + { + char * pToken, * pPivot; + if ( Vec_PtrSize(p->vTokens) != 2 ) + { + p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0); + sprintf( p->sError, "The .model line does not have exactly two entries." ); + Io_ReadBlifPrintErrorMessage( p ); + return NULL; + } + for ( pPivot = pToken = Vec_PtrEntry(p->vTokens, 1); *pToken; pToken++ ) + if ( *pToken == '/' || *pToken == '\\' ) + pPivot = pToken+1; + pNtk->pName = Extra_UtilStrsav( pPivot ); + } else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) { printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 97f2fbf3..8a1fe309 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -90,7 +90,7 @@ static Io_MvMod_t * Io_MvModAlloc(); static void Io_MvModFree( Io_MvMod_t * p ); static char * Io_MvLoadFile( char * pFileName ); static void Io_MvReadPreparse( Io_MvMan_t * p ); -static void Io_MvReadInterfaces( Io_MvMan_t * p ); +static int Io_MvReadInterfaces( Io_MvMan_t * p ); static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p ); static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine ); static int Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine ); @@ -128,7 +128,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) FILE * pFile; Io_MvMan_t * p; Abc_Ntk_t * pNtk; - Abc_Lib_t * pDesign; + Abc_Lib_t * pDesign = NULL; char * pDesignName; int RetValue, i; @@ -161,10 +161,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) p->pDesign->pManFunc = NULL; // prepare the file for parsing Io_MvReadPreparse( p ); - // parse interfaces of each network - Io_MvReadInterfaces( p ); - // construct the network - pDesign = Io_MvParse( p ); + // parse interfaces of each network and construct the network + if ( Io_MvReadInterfaces( p ) ) + pDesign = Io_MvParse( p ); if ( p->sError[0] ) fprintf( stdout, "%s\n", p->sError ); Io_MvFree( p ); @@ -646,7 +645,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p ) SeeAlso [] ***********************************************************************/ -static void Io_MvReadInterfaces( Io_MvMan_t * p ) +static int Io_MvReadInterfaces( Io_MvMan_t * p ) { Io_MvMod_t * pMod; char * pLine; @@ -656,22 +655,23 @@ static void Io_MvReadInterfaces( Io_MvMan_t * p ) { // parse the model if ( !Io_MvParseLineModel( pMod, pMod->pName ) ) - return; + return 0; // add model to the design if ( !Abc_LibAddModel( p->pDesign, pMod->pNtk ) ) { sprintf( p->sError, "Line %d: Model %s is defined twice.", Io_MvGetLine(p, pMod->pName), pMod->pName ); - return; + return 0; } // parse the inputs Vec_PtrForEachEntry( pMod->vInputs, pLine, k ) if ( !Io_MvParseLineInputs( pMod, pLine ) ) - return; + return 0; // parse the outputs Vec_PtrForEachEntry( pMod->vOutputs, pLine, k ) if ( !Io_MvParseLineOutputs( pMod, pLine ) ) - return; + return 0; } + return 1; } @@ -767,7 +767,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p ) static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; - char * pToken; + char * pToken, * pPivot; Io_MvSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry( vTokens, 0 ); assert( !strcmp(pToken, "model") ); @@ -782,7 +782,10 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine ) p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLIFMV, 1 ); else p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 ); - p->pNtk->pName = Extra_UtilStrsav( Vec_PtrEntry(vTokens, 1) ); + for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ ) + if ( *pToken == '/' || *pToken == '\\' ) + pPivot = pToken+1; + p->pNtk->pName = Extra_UtilStrsav( pPivot ); return 1; } diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 9595bc72..df06168c 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -705,6 +705,24 @@ static inline void Vec_PtrCleanSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords /**Function************************************************************* + Synopsis [Cleans simulation info of each entry beginning with iWord.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_PtrFillSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords ) +{ + int i; + for ( i = 0; i < vInfo->nSize; i++ ) + memset( (char*)Vec_PtrEntry(vInfo,i) + 4*iWord, 0xFF, 4*(nWords-iWord) ); +} + +/**Function************************************************************* + Synopsis [Resizes the array of simulation info.] Description [Doubles the number of objects for which siminfo is allocated.] diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index 9fc6a253..cb2da431 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -49,6 +49,8 @@ struct Mfs_Par_t_ int nGrowthLevel; // the maximum allowed growth in level int fResub; // performs resubstitution int fArea; // performs optimization for area + int fMoreEffort; // performs high-affort minimization + int fSwapEdge; // performs edge swapping int fDelay; // performs optimization for delay int fVerbose; // enable basic stats int fVeryVerbose; // enable detailed stats diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 332a6ad9..aed0abe5 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -74,10 +74,14 @@ clk = clock(); return 1; } // solve the SAT problem - if ( p->pPars->fArea ) - Abc_NtkMfsResubArea( p, pNode ); + if ( p->pPars->fSwapEdge ) + Abc_NtkMfsEdgeSwapEval( p, pNode ); else - Abc_NtkMfsResubEdge( p, pNode ); + { + Abc_NtkMfsResubNode( p, pNode ); + if ( p->pPars->fMoreEffort ) + Abc_NtkMfsResubNode2( p, pNode ); + } p->timeSat += clock() - clk; return 1; } @@ -140,12 +144,13 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; - int i, clk = clock(); + int i, nFaninMax, clk = clock(); int nTotalNodesBeg = Abc_NtkNodeNum(pNtk); int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk); assert( Abc_NtkIsLogic(pNtk) ); - if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX ) + nFaninMax = Abc_NtkGetFaninMax(pNtk); + if ( nFaninMax > MFS_FANIN_MAX ) { printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX ); return 1; @@ -162,7 +167,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) // start the manager p = Mfs_ManAlloc( pPars ); - p->pNtk = pNtk; + p->pNtk = pNtk; + p->nFaninMax = nFaninMax; if ( pNtk->pExcare ) { Abc_Ntk_t * pTemp; @@ -170,7 +176,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) p->pCare = Abc_NtkToDar( pTemp, 0 ); Abc_NtkDelete( pTemp ); } - if ( pPars->fVerbose ) +// if ( pPars->fVerbose ) { if ( p->pCare != NULL ) printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 54826bc1..ddd16407 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -49,6 +49,7 @@ struct Mfs_Man_t_ Mfs_Par_t * pPars; Abc_Ntk_t * pNtk; Aig_Man_t * pCare; + int nFaninMax; // intermeditate data for the node Vec_Ptr_t * vRoots; // the roots of the window Vec_Ptr_t * vSupp; // the support of the window @@ -78,7 +79,6 @@ struct Mfs_Man_t_ // performance statistics int nNodesTried; int nNodesResub; - int nNodesGained; int nMintsCare; int nMintsTotal; int nNodesBad; @@ -119,8 +119,10 @@ extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ); extern void Mfs_ManStop( Mfs_Man_t * p ); extern void Mfs_ManClean( Mfs_Man_t * p ); /*=== mfsResub.c ==========================================================*/ -extern int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ); -extern int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p ); +extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsSat.c ==========================================================*/ extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsStrash.c ==========================================================*/ diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 67981d5a..519b855d 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -85,12 +85,12 @@ void Mfs_ManClean( Mfs_Man_t * p ) if ( p->vDivs ) Vec_PtrFree( p->vDivs ); p->pAigWin = NULL; - p->pCnf = NULL; - p->pSat = NULL; - p->vRoots = NULL; - p->vSupp = NULL; - p->vNodes = NULL; - p->vDivs = NULL; + p->pCnf = NULL; + p->pSat = NULL; + p->vRoots = NULL; + p->vSupp = NULL; + p->vNodes = NULL; + p->vDivs = NULL; } /**Function************************************************************* @@ -117,6 +117,11 @@ void Mfs_ManPrint( Mfs_Man_t * p ) printf( "\n" ); printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls ); + if ( p->pPars->fSwapEdge ) + printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", + p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) ); + else + Abc_NtkMfsPrintResubStats( p ); } else { diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index ae1132f2..1e9da4d2 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -57,6 +57,35 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani /**Function************************************************************* + Synopsis [Prints resub candidate stats.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p ) +{ + Abc_Obj_t * pFanin, * pNode; + int i, k, nAreaCrits = 0, nAreaExpanse = 0; + int nFaninMax = Abc_NtkGetFaninMax(p->pNtk); + Abc_NtkForEachNode( p->pNtk, pNode, i ) + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + nAreaCrits++; + nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax); + } + } + printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", + nAreaCrits, nAreaExpanse ); +} + +/**Function************************************************************* + Synopsis [Tries resubstitution.] Description [Returns 1 if it is feasible, or 0 if c-ex is found.] @@ -68,7 +97,7 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani ***********************************************************************/ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) { - unsigned * pData, * pDataTot; + unsigned * pData; int RetValue, iVar, i; p->nSatCalls++; RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); @@ -77,17 +106,16 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) return 1; p->nSatCexes++; // store the counter-example - pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ ); - assert( pData[0] == 0 ); Vec_IntForEachEntry( p->vProjVars, iVar, i ) { - if ( sat_solver_var_value( p->pSat, iVar ) ) - Aig_InfoSetBit( pData, i ); + pData = Vec_PtrEntry( p->vDivCexes, i ); + if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! + { + assert( Aig_InfoHasBit(pData, p->nCexes) ); + Aig_InfoXorBit( pData, p->nCexes ); + } } - // AND the result with the previous ones - pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); - for ( i = 0; i < p->nDivWords; i++ ) - pDataTot[i] &= pData[i]; + p->nCexes++; return 0; } @@ -102,22 +130,19 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) SeeAlso [] ***********************************************************************/ -int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove ) +int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate ) { int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; unsigned * pData; int pCands[MFS_FANIN_MAX]; - int iVar, i, nCands, clk; + int iVar, i, nCands, nWords, w, clk; Abc_Obj_t * pFanin; Hop_Obj_t * pFunc; assert( iFanin >= 0 ); // clean simulation info - Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); - pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); - memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords ); + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); p->nCexes = 0; - if ( fVeryVerbose ) { printf( "\n" ); @@ -143,7 +168,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f if ( fVeryVerbose ) printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); p->nNodesResub++; -// p->nNodesGained += Abc_NodeMffcLabel(pNode); + if ( fSkipUpdate ) + return 1; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); @@ -156,11 +182,6 @@ p->timeInt += clock() - clk; if ( fOnlyRemove ) return 0; - // shift variables by 1 - for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) - p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; - p->vFanins->nSize++; - if ( fVeryVerbose ) { for ( i = 0; i < 8; i++ ) @@ -180,37 +201,52 @@ p->timeInt += clock() - clk; if ( fVeryVerbose ) { printf( "%3d: %2d ", p->nCexes, iVar ); - pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 ); -// Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) ); for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) - printf( "%d", Aig_InfoHasBit(pData, i) ); + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } printf( "\n" ); } // find the next divisor to try - pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) - if ( Aig_InfoHasBit( pData, iVar ) ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( w = 0; w < nWords; w++ ) + if ( pData[w] != ~0 ) + break; + if ( w == nWords ) break; + } if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) return 0; + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) ) { if ( fVeryVerbose ) printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); p->nNodesResub++; -// p->nNodesGained += Abc_NodeMffcLabel(pNode); + if ( fSkipUpdate ) + return 1; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 ); - // update the network -// Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + // shift fanins by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) ); + // update the network Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); p->timeInt += clock() - clk; return 1; } + if ( p->nCexes >= p->pPars->nDivMax ) + break; } return 0; } @@ -226,16 +262,155 @@ p->timeInt += clock() - clk; SeeAlso [] ***********************************************************************/ -int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ) +int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 ) { + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData, * pData2; + int pCands[MFS_FANIN_MAX]; + int iVar, iVar2, i, w, nCands, clk, nWords, fBreak; Abc_Obj_t * pFanin; - int i; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + assert( iFanin2 >= 0 || iFanin2 == -1 ); + + // clean simulation info + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); + p->nCexes = 0; + if ( fVeryVerbose ) + { + printf( "\n" ); + printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), + iFanin, iFanin2, Abc_ObjFaninNum(pNode), + Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( i == iFanin || i == iFanin2 ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 ); + p->nNodesResub++; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fVeryVerbose ) + { + for ( i = 0; i < 11; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ ) + if ( i == iFanin || i == iFanin2 ) + printf( "*" ); + else + printf( "%c", 'a' + i ); + printf( "\n" ); + } + iVar = iVar2 = -1; + while ( 1 ) + { + if ( fVeryVerbose ) { - if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) ) - return 1; + printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } + printf( "\n" ); + } + + // find the next divisor to try + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); + fBreak = 0; + for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( iVar2 = 0; iVar2 < iVar; iVar2++ ) + { + pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 ); + for ( w = 0; w < nWords; w++ ) + if ( (pData[w] | pData2[w]) != ~0 ) + break; + if ( w == nWords ) + { + fBreak = 1; + break; + } + } + if ( fBreak ) + break; + } + if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) + return 0; + + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 ); + p->nNodesResub++; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 ); + // shift fanins by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; + // shift fanins by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; + Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) ); + Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) ); + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; } + if ( p->nCexes >= p->pPars->nDivMax ) + break; + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Evaluates the possibility of replacing given edge by another edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i; + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 ); return 0; } @@ -250,25 +425,81 @@ int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode ) +int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Abc_Obj_t * pFanin; int i; + // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) { - if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) ) + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) return 1; } + // try removing redundant edges + if ( !p->pPars->fArea ) + { + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) + return 1; + } + } + if ( Abc_ObjFaninNum(pNode) == p->nFaninMax ) + return 0; + // try replacing area critical fanins while adding two new fanins Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) { - if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) ) + if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) return 1; } return 0; } +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin, * pFanin2; + int i, k; +/* + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } +*/ + if ( Abc_ObjFaninNum(pNode) < 2 ) + return 0; + // try replacing one area critical fanin and one other fanin while adding two new fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + // consider second fanin to remove at the same time + Abc_ObjForEachFanin( pNode, pFanin2, k ) + { + if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) ) + return 1; + } + } + } + return 0; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |