luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc70127

This commit is contained in:
Alan Mishchenko 2007-01-27 08:01:00 -08:00
parent 1c26e2d297
commit 12578e622f
13 changed files with 1434 additions and 94 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abc.dsp
View File

@ -278,6 +278,10 @@ SOURCE=.\src\base\abci\abcNtbdd.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcOdc.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcOrder.c
# End Source File
# Begin Source File
@ -1670,6 +1674,10 @@ SOURCE=.\src\opt\res\resFilter.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\res\resInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\res\resSat.c
# End Source File
# Begin Source File

3
src/base/abc/abc.h
View File

@ -237,7 +237,8 @@ static inline int Abc_TruthWordNum( int nVars ) { return nV
static inline int Abc_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Abc_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Abc_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Abc_InfoRandom() { return ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); } // #define RAND_MAX 0x7fff
static inline unsigned Abc_InfoRandomWord() { return ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); } // #define RAND_MAX 0x7fff
static inline void Abc_InfoRandom( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = Abc_InfoRandomWord(); }
static inline void Abc_InfoClear( unsigned * p, int nWords ) { memset( p, 0, sizeof(unsigned) * nWords ); }
static inline void Abc_InfoFill( unsigned * p, int nWords ) { memset( p, 0xff, sizeof(unsigned) * nWords );}
static inline void Abc_InfoNot( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i]; }

94
src/base/abc/abcUtil.c
View File

@ -1450,6 +1450,100 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk )
pObj->pCopy = pObj->pCopy? Abc_ObjEquiv(pObj->pCopy) : NULL;
}
/**Function*************************************************************
Synopsis [Increaments the cut counter.]
Description [Returns 1 if it becomes equal to the ref counter.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj )
{
pObj->pCopy = (void *)(((int)pObj->pCopy)++);
return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj);
}
/**Function*************************************************************
Synopsis [Computes cross-cut of the circuit.]
Description [Returns 1 if it is the last visit to the node.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkCrossCut_rec( Abc_Obj_t * pObj, int * pnCutSize, int * pnCutSizeMax )
{
Abc_Obj_t * pFanin;
int i, nDecrem = 0;
int fReverse = 0;
if ( Abc_ObjIsCi(pObj) )
return 0;
// if visited, increment visit counter
if ( Abc_NodeIsTravIdCurrent( pObj ) )
return Abc_ObjCrossCutInc( pObj );
Abc_NodeSetTravIdCurrent( pObj );
// visit the fanins
if ( !Abc_ObjIsCi(pObj) )
{
if ( fReverse )
{
Abc_ObjForEachFanin( pObj, pFanin, i )
{
pFanin = Abc_ObjFanin( pObj, Abc_ObjFaninNum(pObj) - 1 - i );
nDecrem += Abc_NtkCrossCut_rec( pFanin, pnCutSize, pnCutSizeMax );
}
}
else
{
Abc_ObjForEachFanin( pObj, pFanin, i )
nDecrem += Abc_NtkCrossCut_rec( pFanin, pnCutSize, pnCutSizeMax );
}
}
// count the node
(*pnCutSize)++;
if ( *pnCutSizeMax < *pnCutSize )
*pnCutSizeMax = *pnCutSize;
(*pnCutSize) -= nDecrem;
return Abc_ObjCrossCutInc( pObj );
}
/**Function*************************************************************
Synopsis [Computes cross-cut of the circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkCrossCut( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int nCutSize = 0, nCutSizeMax = 0;
int i;
Abc_NtkCleanCopy( pNtk );
Abc_NtkIncrementTravId( pNtk );
Abc_NtkForEachCo( pNtk, pObj, i )
{
Abc_NtkCrossCut_rec( pObj, &nCutSize, &nCutSizeMax );
nCutSize--;
}
assert( nCutSize == 0 );
printf( "Max cross cut size = %6d. Ratio = %6.2f %%\n", nCutSizeMax, 100.0 * nCutSizeMax/Abc_NtkObjNum(pNtk) );
return nCutSizeMax;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

39
src/base/abci/abc.c
View File

@ -2999,23 +2999,27 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int nCutsMax;
int nNodesMax;
int nLevelsOdc;
bool fUpdateLevel;
bool fUseZeros;
bool fVerbose;
extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, bool fUpdateLevel, bool fVerbose );
bool fVeryVerbose;
extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nCutsMax = 8;
nCutsMax = 8;
nNodesMax = 1;
nLevelsOdc = 0;
fUpdateLevel = 1;
fUseZeros = 0;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KNlzvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KNFlzvwh" ) ) != EOF )
{
switch ( c )
{
@ -3041,6 +3045,17 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nNodesMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nLevelsOdc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLevelsOdc < 0 )
goto usage;
break;
case 'l':
fUpdateLevel ^= 1;
break;
@ -3050,6 +3065,9 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -3064,7 +3082,12 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( nCutsMax < RS_CUT_MIN || nCutsMax > RS_CUT_MAX )
{
fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX );
fprintf( pErr, "Can only compute cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX );
return 1;
}
if ( nNodesMax < 0 || nNodesMax > 3 )
{
fprintf( pErr, "Can only resubstitute at most 3 nodes.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
@ -3079,7 +3102,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, fUpdateLevel, fVerbose ) )
if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, nLevelsOdc, fUpdateLevel, fVerbose, fVeryVerbose ) )
{
fprintf( pErr, "Refactoring has failed.\n" );
return 1;
@ -3087,13 +3110,15 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: resub [-K num] [-N num] [-lzvh]\n" );
fprintf( pErr, "usage: resub [-K num] [-N num] [-F num] [-lzvwh]\n" );
fprintf( pErr, "\t performs technology-independent restructuring of the AIG\n" );
fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax );
fprintf( pErr, "\t-N num : the max number of nodes to add [default = %d]\n", nNodesMax );
fprintf( pErr, "\t-N num : the max number of nodes to add (0 <= num <= 3) [default = %d]\n", nNodesMax );
fprintf( pErr, "\t-F num : the number of fanout levels for ODC computation [default = %d]\n", nLevelsOdc );
fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle verbose printout of ODC computation [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}

1134
src/base/abci/abcOdc.c Normal file
View File

File diff suppressed because it is too large Load Diff

1
src/base/abci/abcPrint.c
View File

@ -111,6 +111,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
fprintf( pFile, "\n" );
// Abc_NtkCrossCut( pNtk );
// print the statistic into a file
/*

220
src/base/abci/abcResub.c
View File

@ -46,6 +46,8 @@ struct Abc_ManRes_t_
int nWords; // the number of unsigneds for siminfo
Vec_Ptr_t * vSims; // simulation info
unsigned * pInfo; // pointer to simulation info
// observability don't-cares
unsigned * pCareSet;
// internal divisor storage
Vec_Ptr_t * vDivs1UP; // the single-node unate divisors
Vec_Ptr_t * vDivs1UN; // the single-node unate divisors
@ -58,6 +60,7 @@ struct Abc_ManRes_t_
Vec_Ptr_t * vTemp; // temporary array of nodes
// runtime statistics
int timeCut;
int timeTruth;
int timeRes;
int timeDiv;
int timeMffc;
@ -109,6 +112,13 @@ static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required );
static Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax );
static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
// don't-care manager
extern void * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose );
extern void Abc_NtkDontCareClear( void * p );
extern void Abc_NtkDontCareFree( void * p );
extern int Abc_NtkDontCareCompute( void * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -124,11 +134,12 @@ static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves
SeeAlso []
***********************************************************************/
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpdateLevel, bool fVerbose )
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose )
{
ProgressBar * pProgress;
Abc_ManRes_t * pManRes;
Abc_ManCut_t * pManCut;
void * pManOdc = NULL;
Dec_Graph_t * pFForm;
Vec_Ptr_t * vLeaves;
Abc_Obj_t * pNode;
@ -142,6 +153,8 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd
// start the managers
pManCut = Abc_NtkManCutStart( nCutMax, 100000, 100000, 100000 );
pManRes = Abc_ManResubStart( nCutMax, ABC_RS_DIV1_MAX );
if ( nLevelsOdc > 0 )
pManOdc = Abc_NtkDontCareAlloc( nCutMax, nLevelsOdc, fVerbose, fVeryVerbose );
// compute the reverse levels if level update is requested
if ( fUpdateLevel )
@ -181,6 +194,14 @@ pManRes->timeCut += clock() - clk;
if ( vLeaves == NULL )
continue;
*/
// get the don't-cares
if ( pManOdc )
{
clk = clock();
Abc_NtkDontCareClear( pManOdc );
Abc_NtkDontCareCompute( pManOdc, pNode, vLeaves, pManRes->pCareSet );
pManRes->timeTruth += clock() - clk;
}
// evaluate this cut
clk = clock();
@ -216,6 +237,7 @@ pManRes->timeTotal = clock() - clkStart;
// delete the managers
Abc_ManResubStop( pManRes );
Abc_NtkManCutStop( pManCut );
if ( pManOdc ) Abc_NtkDontCareFree( pManOdc );
// clean the data field
Abc_NtkForEachObj( pNtk, pNode, i )
@ -270,11 +292,14 @@ Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
// allocate simulation info
p->nBits = (1 << p->nLeavesMax);
p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32);
p->pInfo = ALLOC( unsigned, p->nWords * p->nDivsMax );
p->pInfo = ALLOC( unsigned, p->nWords * (p->nDivsMax + 1) );
memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax );
p->vSims = Vec_PtrAlloc( p->nDivsMax );
for ( i = 0; i < p->nDivsMax; i++ )
Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords );
// assign the care set
p->pCareSet = p->pInfo + p->nDivsMax * p->nWords;
Abc_InfoFill( p->pCareSet, p->nWords );
// set elementary truth tables
for ( k = 0; k < p->nLeavesMax; k++ )
{
@ -343,7 +368,7 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
printf( "Used double ANDs = %6d. ", p->nUsedNode2And ); PRT( " 1 ", p->timeRes1 );
printf( "Used OR-AND = %6d. ", p->nUsedNode2OrAnd ); PRT( " D ", p->timeResD );
printf( "Used AND-OR = %6d. ", p->nUsedNode2AndOr ); PRT( " 2 ", p->timeRes2 );
printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); PRT( " 3 ", p->timeRes3 );
printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); PRT( "Truth ", p->timeTruth ); //PRT( " 3 ", p->timeRes3 );
printf( "Used AND-2ORs = %6d. ", p->nUsedNode3AndOr ); PRT( "AIG ", p->timeNtk );
printf( "TOTAL = %6d. ", p->nUsedNodeC +
p->nUsedNode0 +
@ -359,7 +384,6 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
printf( "Total leaves = %8d.\n", p->nTotalLeaves );
printf( "Total divisors = %8d.\n", p->nTotalDivs );
printf( "Total gain = %8d.\n", p->nTotalGain );
}
@ -580,36 +604,6 @@ void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, in
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p )
{
Dec_Graph_t * pGraph;
unsigned * upData;
int w;
upData = p->pRoot->pData;
for ( w = 0; w < p->nWords; w++ )
if ( upData[w] )
break;
if ( w != p->nWords )
return NULL;
// get constant node graph
if ( p->pRoot->fPhase )
pGraph = Dec_GraphCreateConst1();
else
pGraph = Dec_GraphCreateConst0();
return pGraph;
}
/**Function*************************************************************
Synopsis []
@ -854,7 +848,8 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
puData = pObj->pData;
// check positive containment
for ( w = 0; w < p->nWords; w++ )
if ( puData[w] & ~puDataR[w] )
// if ( puData[w] & ~puDataR[w] )
if ( puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -863,7 +858,8 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
}
// check negative containment
for ( w = 0; w < p->nWords; w++ )
if ( ~puData[w] & puDataR[w] )
// if ( ~puData[w] & puDataR[w] )
if ( ~puData[w] & puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -913,7 +909,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
{
// get positive unate divisors
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & puData1[w]) & ~puDataR[w] )
// if ( (puData0[w] & puData1[w]) & ~puDataR[w] )
if ( (puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -921,7 +918,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs2UP1, pObj1 );
}
for ( w = 0; w < p->nWords; w++ )
if ( (~puData0[w] & puData1[w]) & ~puDataR[w] )
// if ( (~puData0[w] & puData1[w]) & ~puDataR[w] )
if ( (~puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -929,7 +927,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs2UP1, pObj1 );
}
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] )
// if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] )
if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -937,7 +936,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) );
}
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | puData1[w]) & ~puDataR[w] )
// if ( (puData0[w] | puData1[w]) & ~puDataR[w] )
if ( (puData0[w] | puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -950,7 +950,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
{
// get negative unate divisors
for ( w = 0; w < p->nWords; w++ )
if ( ~(puData0[w] & puData1[w]) & puDataR[w] )
// if ( ~(puData0[w] & puData1[w]) & puDataR[w] )
if ( ~(puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -958,7 +959,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs2UN1, pObj1 );
}
for ( w = 0; w < p->nWords; w++ )
if ( ~(~puData0[w] & puData1[w]) & puDataR[w] )
// if ( ~(~puData0[w] & puData1[w]) & puDataR[w] )
if ( ~(~puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -966,7 +968,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs2UN1, pObj1 );
}
for ( w = 0; w < p->nWords; w++ )
if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] )
// if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] )
if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -974,7 +977,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) );
}
for ( w = 0; w < p->nWords; w++ )
if ( ~(puData0[w] | puData1[w]) & puDataR[w] )
// if ( ~(puData0[w] | puData1[w]) & puDataR[w] )
if ( ~(puData0[w] | puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -991,7 +995,38 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
/**Function*************************************************************
Synopsis [Derives unate/binate divisors.]
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p )
{
Dec_Graph_t * pGraph;
unsigned * upData;
int w;
upData = p->pRoot->pData;
for ( w = 0; w < p->nWords; w++ )
// if ( upData[w] )
if ( upData[w] & p->pCareSet[w] ) // care set
break;
if ( w != p->nWords )
return NULL;
// get constant node graph
if ( p->pRoot->fPhase )
pGraph = Dec_GraphCreateConst1();
else
pGraph = Dec_GraphCreateConst0();
return pGraph;
}
/**Function*************************************************************
Synopsis []
Description []
@ -1010,7 +1045,8 @@ Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p )
{
puData = pObj->pData;
for ( w = 0; w < p->nWords; w++ )
if ( puData[w] != puDataR[w] )
// if ( puData[w] != puDataR[w] )
if ( (puData[w] ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
return Abc_ManResubQuit0( p->pRoot, pObj );
@ -1020,7 +1056,7 @@ Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p )
/**Function*************************************************************
Synopsis [Derives unate/binate divisors.]
Synopsis []
Description []
@ -1043,7 +1079,8 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
{
puData1 = pObj1->pData;
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | puData1[w]) != puDataR[w] )
// if ( (puData0[w] | puData1[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -1060,7 +1097,8 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
{
puData1 = pObj1->pData;
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & puData1[w]) != puDataR[w] )
// if ( (puData0[w] & puData1[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -1074,7 +1112,7 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
/**Function*************************************************************
Synopsis [Derives unate/binate divisors.]
Synopsis []
Description []
@ -1100,7 +1138,8 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
{
puData2 = pObj2->pData;
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -1138,7 +1177,8 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
{
puData2 = pObj2->pData;
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
@ -1170,7 +1210,7 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
/**Function*************************************************************
Synopsis [Derives unate/binate divisors.]
Synopsis []
Description []
@ -1198,25 +1238,29 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
if ( w == p->nWords )
@ -1239,25 +1283,29 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
if ( w == p->nWords )
@ -1272,7 +1320,7 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
/**Function*************************************************************
Synopsis [Derives unate/binate divisors.]
Synopsis []
Description []
@ -1307,85 +1355,101 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required )
{
case 0: // 0000
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 1: // 0001
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 2: // 0010
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 3: // 0011
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 4: // 0100
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 5: // 0101
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 6: // 0110
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 7: // 0111
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 8: // 1000
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 9: // 1001
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
// if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 10: // 1010
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 11: // 1011
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
// if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 12: // 1100
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
break;
case 13: // 1101
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
// if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 14: // 1110
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
// if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 15: // 1111
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
// if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;

1
src/base/abci/module.make
View File

@ -24,6 +24,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcMiter.c \
src/base/abci/abcMulti.c \
src/base/abci/abcNtbdd.c \
src/base/abci/abcOdc.c \
src/base/abci/abcOrder.c \
src/base/abci/abcPrint.c \
src/base/abci/abcProve.c \

10
src/opt/res/resCore.c
View File

@ -200,8 +200,11 @@ p->timeAig += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
printf( "%5d : ", pObj->Id );
printf( "Win = %3d/%4d/%3d ", Vec_PtrSize(p->pWin->vLeaves), Vec_VecSizeSize(p->pWin->vLevels), Vec_PtrSize(p->pWin->vRoots) );
printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
printf( "Win = %3d/%3d/%4d/%3d ",
Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus,
p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels),
Vec_PtrSize(p->pWin->vRoots) );
printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
printf( "D+ = %3d ", p->pWin->nDivsPlus );
printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
@ -242,12 +245,13 @@ p->timeSat += clock() - clk;
// printf( " Sat\n" );
continue;
}
p->nProvedSets++;
// printf( " Unsat\n" );
continue;
// write it into a file
// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
p->nProvedSets++;
// interplate the problem if it was UNSAT
clk = clock();

2
src/opt/res/resDivs.c
View File

@ -60,6 +60,8 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// mark the MFFC of the node (does not increment trav ID)
Res_WinVisitMffc( p );
// what about the fanouts of the leaves!!!
// go through all the legal levels and check if their fanouts can be divisors
p->nDivsPlus = 0;
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )

1
src/opt/res/resInt.h
View File

@ -48,6 +48,7 @@ struct Res_Win_t_
int nLevLeaves; // the level where leaves begin
int nLevDivMax; // the maximum divisor level
int nDivsPlus; // the number of additional divisors
int nLeavesPlus;// the number of additional leaves
Abc_Obj_t * pNode; // the node in the center
// the window data
Vec_Vec_t * vLevels; // nodes by level

13
src/opt/res/resSim.c
View File

@ -141,12 +141,11 @@ void Res_SimSetRandom( Res_Sim_t * p )
{
Abc_Obj_t * pObj;
unsigned * pInfo;
int i, w;
int i;
Abc_NtkForEachPi( p->pAig, pObj, i )
{
pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
for ( w = 0; w < p->nWords; w++ )
pInfo[w] = Abc_InfoRandom();
Abc_InfoRandom( pInfo, p->nWords );
}
}
@ -478,7 +477,7 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
// prepare the manager
Res_SimAdjust( p, pAig );
// collect 0/1 simulation info
for ( Limit = 0; Limit < 100; Limit++ )
for ( Limit = 0; Limit < 10; Limit++ )
{
Res_SimSetRandom( p );
Res_SimPerformRound( p );
@ -489,10 +488,14 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
}
// printf( "%d ", Limit );
// report the last set of patterns
// Res_SimReportOne( p );
Res_SimReportOne( p );
printf( "\n" );
// quit if there is not enough
if ( p->nPats0 < 4 || p->nPats1 < 4 )
{
// Res_SimReportOne( p );
return 0;
}
// create bit-matrix info
if ( p->nPats0 < p->nPats )
Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );

2
src/opt/res/resWin.c
View File

@ -243,6 +243,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
return;
if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
{
p->nLeavesPlus++;
Vec_PtrPush( p->vLeaves, pObj );
pObj->fMarkA = 1;
return;
@ -349,6 +350,7 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax;
p->nLeavesPlus = 0;
p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 );
// collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
Res_WinCollectNodeTfi( p );