summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/fra/fra.h2
-rw-r--r--src/aig/fra/fraClaus.c6
-rw-r--r--src/aig/fra/fraHot.c2
-rw-r--r--src/aig/fra/fraInd.c6
-rw-r--r--src/base/abc/abcDfs.c2
-rw-r--r--src/base/abci/abc.c39
-rw-r--r--src/base/abci/abcGen.c42
-rw-r--r--src/base/abci/abcMiter.c1
-rw-r--r--src/base/cmd/cmd.c254
-rw-r--r--src/base/io/ioReadBlif.c15
-rw-r--r--src/base/io/ioReadBlifMv.c29
-rw-r--r--src/misc/vec/vecPtr.h18
-rw-r--r--src/opt/mfs/mfs.h2
-rw-r--r--src/opt/mfs/mfsCore.c20
-rw-r--r--src/opt/mfs/mfsInt.h8
-rw-r--r--src/opt/mfs/mfsMan.c17
-rw-r--r--src/opt/mfs/mfsResub.c307
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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-18 06:18:09 +0000