Skip to content

A
abc
Commit 39bc4842 by Alan Mishchenko
Options

Version abc70706

parent 0c1e87bc
Showing with 918 additions and 592 deletions
abc.dsp
...@@ -1902,10 +1902,6 @@ SOURCE=.\src\opt\res\resStrash.c ...@@ -1902,10 +1902,6 @@ SOURCE=.\src\opt\res\resStrash.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\opt\res\resUpdate.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\res\resWin.c SOURCE=.\src\opt\res\resWin.c
# End Source File # End Source File
# End Group # End Group
......
abc.rc
...@@ -143,14 +143,6 @@ alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar ...@@ -143,14 +143,6 @@ alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar
alias chnew "st; haig_start; resyn2; haig_use" alias chnew "st; haig_start; resyn2; haig_use"
alias chnewrs "st; haig_start; resyn2rs; haig_use" alias chnewrs "st; haig_start; resyn2rs; haig_use"
alias t0 "read_dsd a*(b+(c*d)+e); clp -r; print_dsd"
alias t1 "read_dsd a*(b+(c*d)); clp -r; print_dsd"
alias t2 "read_dsd 56BA(a,b,c,d); clp -r; print_dsd"
alias t3 "read_dsd 56BA(a,b*c,e,d); clp -r; print_dsd"
alias t4 "read_dsd 56BA(a,b*c,e+d,f); clp -r; print_dsd"
alias t5 "read_dsd 56BA(a,CA(b,c,d),e,f); clp -r; print_dsd"
alias t6 "read_dsd f*CA(b,c,d)*CA(e,a,g); clp -r; print_dsd"
alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps" alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
alias trec "rec_start; r c.blif; st; rec_add; rec_use" alias trec "rec_start; r c.blif; st; rec_add; rec_use"
alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use" alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
...@@ -166,12 +158,10 @@ alias tst4 "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4 ...@@ -166,12 +158,10 @@ alias tst4 "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4
alias tst4n "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec" alias tst4n "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec"
alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec" alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec"
alias bug "r pj1_if3.blif; lp"
alias table "r lutexp.baf; test"
#alias t "r c.blif; st; wc c.cnf" #alias t "r c.blif; st; wc c.cnf"
#alias t "r test/dsdmap6.blif; lutpack -vw; cec" #alias t "r test/dsdmap6.blif; lutpack -vw; cec"
alias t "r i10_if4.blif; lp" alias t "r i10_if4.blif; lp"
alias t1 "r pj1_if4.blif; lp"
alias t2 "r pj1_if6.blif; lp"
src/base/abc/abc.h
...@@ -354,6 +354,7 @@ static inline Hop_Obj_t * Abc_ObjEquiv( Abc_Obj_t * pObj ) { return pO ...@@ -354,6 +354,7 @@ static inline Hop_Obj_t * Abc_ObjEquiv( Abc_Obj_t * pObj ) { return pO
static inline Abc_Obj_t * Abc_ObjCopyCond( Abc_Obj_t * pObj ) { return Abc_ObjRegular(pObj)->pCopy? Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)) : NULL; } static inline Abc_Obj_t * Abc_ObjCopyCond( Abc_Obj_t * pObj ) { return Abc_ObjRegular(pObj)->pCopy? Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)) : NULL; }
// setting data members of the network // setting data members of the network
static inline void Abc_ObjSetLevel( Abc_Obj_t * pObj, int Level ) { pObj->Level = Level; }
static inline void Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy ) { pObj->pCopy = pCopy; } static inline void Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy ) { pObj->pCopy = pCopy; }
static inline void Abc_ObjSetData( Abc_Obj_t * pObj, void * pData ) { pObj->pData = pData; } static inline void Abc_ObjSetData( Abc_Obj_t * pObj, void * pData ) { pObj->pData = pData; }
...@@ -852,11 +853,16 @@ extern void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk ); ...@@ -852,11 +853,16 @@ extern void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
extern float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk ); extern float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
extern Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk ); extern Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
extern float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk ); extern float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
extern void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk ); extern int Abc_ObjLevelNew( Abc_Obj_t * pObj );
extern int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj );
extern int Abc_ObjRequiredLevel( Abc_Obj_t * pObj );
extern int Abc_ObjReverseLevel( Abc_Obj_t * pObj );
extern void Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
extern void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease );
extern void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk ); extern void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
extern void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR ); extern void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
extern int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj ); extern void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
extern int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj ); extern void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
/*=== abcUtil.c ==========================================================*/ /*=== abcUtil.c ==========================================================*/
extern void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan ); extern void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan );
extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ); extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
......
src/base/abc/abcAig.c
...@@ -923,7 +923,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i ...@@ -923,7 +923,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
{ {
assert( pFanout->fMarkB == 0 ); assert( pFanout->fMarkB == 0 );
pFanout->fMarkB = 1; pFanout->fMarkB = 1;
Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout ); Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanout), pFanout );
} }
} }
...@@ -1094,7 +1094,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan ) ...@@ -1094,7 +1094,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
if ( pNode == NULL ) if ( pNode == NULL )
continue; continue;
assert( Abc_ObjIsNode(pNode) ); assert( Abc_ObjIsNode(pNode) );
assert( Abc_NodeReadReverseLevel(pNode) == i ); assert( Abc_ObjReverseLevel(pNode) == i );
// clean the mark // clean the mark
assert( pNode->fMarkB == 1 ); assert( pNode->fMarkB == 1 );
pNode->fMarkB = 0; pNode->fMarkB = 0;
...@@ -1106,17 +1106,17 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan ) ...@@ -1106,17 +1106,17 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
// get the new reverse level of this fanin // get the new reverse level of this fanin
LevelNew = 0; LevelNew = 0;
Abc_ObjForEachFanout( pFanin, pFanout, j ) Abc_ObjForEachFanout( pFanin, pFanout, j )
if ( LevelNew < Abc_NodeReadReverseLevel(pFanout) ) if ( LevelNew < Abc_ObjReverseLevel(pFanout) )
LevelNew = Abc_NodeReadReverseLevel(pFanout); LevelNew = Abc_ObjReverseLevel(pFanout);
LevelNew += 1; LevelNew += 1;
assert( LevelNew > i ); assert( LevelNew > i );
if ( Abc_NodeReadReverseLevel(pFanin) == LevelNew ) // no change if ( Abc_ObjReverseLevel(pFanin) == LevelNew ) // no change
continue; continue;
// if the fanin is present in the data structure, pull it out // if the fanin is present in the data structure, pull it out
if ( pFanin->fMarkB ) if ( pFanin->fMarkB )
Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin ); Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin );
// update the reverse level // update the reverse level
Abc_NodeSetReverseLevel( pFanin, LevelNew ); Abc_ObjSetReverseLevel( pFanin, LevelNew );
// add the fanin to the data structure to update its fanins // add the fanin to the data structure to update its fanins
assert( pFanin->fMarkB == 0 ); assert( pFanin->fMarkB == 0 );
pFanin->fMarkB = 1; pFanin->fMarkB = 1;
...@@ -1173,7 +1173,7 @@ void Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode ) ...@@ -1173,7 +1173,7 @@ void Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
Abc_Obj_t * pTemp; Abc_Obj_t * pTemp;
int m; int m;
assert( pNode->fMarkB ); assert( pNode->fMarkB );
vVecTemp = Vec_VecEntry( vStruct, Abc_NodeReadReverseLevel(pNode) ); vVecTemp = Vec_VecEntry( vStruct, Abc_ObjReverseLevel(pNode) );
Vec_PtrForEachEntry( vVecTemp, pTemp, m ) Vec_PtrForEachEntry( vVecTemp, pTemp, m )
{ {
if ( pTemp != pNode ) if ( pTemp != pNode )
......
src/base/abc/abcObj.c
...@@ -447,7 +447,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) ...@@ -447,7 +447,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
if ( Num >= 0 ) if ( Num >= 0 )
return Abc_NtkObj( pNtk, Num ); return Abc_NtkObj( pNtk, Num );
// find the internal node // find the internal node
if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' ) if ( pName[0] != 'n' )
{ {
printf( "Name \"%s\" is not found among CO or node names (internal names often look as \"n<num>\").\n", pName ); printf( "Name \"%s\" is not found among CO or node names (internal names often look as \"n<num>\").\n", pName );
return NULL; return NULL;
......
src/base/abci/abc.c
...@@ -2805,7 +2805,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2805,7 +2805,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
pPars->nWindow = 62; pPars->nWindow = 62;
pPars->nGrowthLevel = 3; pPars->nGrowthLevel = 1;
pPars->nCands = 5; pPars->nCands = 5;
pPars->nSimWords = 4; pPars->nSimWords = 4;
pPars->fArea = 0; pPars->fArea = 0;
...@@ -2936,13 +2936,14 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2936,13 +2936,14 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure
pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC
pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars)
pPars->nGrowthLevel = 9; // (L) the maximum number of increased levels pPars->nGrowthLevel = 1; // (L) the maximum number of increased levels
pPars->fSatur = 1; pPars->fSatur = 1;
pPars->fZeroCost = 0; pPars->fZeroCost = 0;
pPars->fVerbose = 1; pPars->fFirst = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0; pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -2996,6 +2997,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2996,6 +2997,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'z': case 'z':
pPars->fZeroCost ^= 1; pPars->fZeroCost ^= 1;
break; break;
case 'f':
pPars->fFirst ^= 1;
break;
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
...@@ -3029,7 +3033,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -3029,7 +3033,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szvwh]\n" ); fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfvwh]\n" );
fprintf( pErr, "\t performs \"rewriting\" for LUT networks\n" ); fprintf( pErr, "\t performs \"rewriting\" for LUT networks\n" );
fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
...@@ -3037,6 +3041,7 @@ usage: ...@@ -3037,6 +3041,7 @@ usage:
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 largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "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" ); fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
......
src/base/abci/abcBalance.c
...@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, ...@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective,
// compute the required times // compute the required times
if ( fSelective ) if ( fSelective )
{ {
Abc_NtkStartReverseLevels( pNtk ); Abc_NtkStartReverseLevels( pNtk, 0 );
Abc_NtkMarkCriticalNodes( pNtk ); Abc_NtkMarkCriticalNodes( pNtk );
} }
// perform balancing // perform balancing
...@@ -600,7 +600,7 @@ void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ) ...@@ -600,7 +600,7 @@ void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk )
Abc_Obj_t * pNode; Abc_Obj_t * pNode;
int i, Counter = 0; int i, Counter = 0;
Abc_NtkForEachNode( pNtk, pNode, i ) Abc_NtkForEachNode( pNtk, pNode, i )
if ( Abc_NodeReadRequiredLevel(pNode) - pNode->Level <= 1 ) if ( Abc_ObjRequiredLevel(pNode) - pNode->Level <= 1 )
pNode->fMarkA = 1, Counter++; pNode->fMarkA = 1, Counter++;
printf( "The number of nodes on the critical paths = %6d (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) ); printf( "The number of nodes on the critical paths = %6d (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) );
} }
......
src/base/abci/abcIf.c
...@@ -263,10 +263,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t ...@@ -263,10 +263,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
} }
// set the level of the new node // set the level of the new node
{ pNodeNew->Level = Abc_ObjLevelNew( pNodeNew );
extern int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
pNodeNew->Level = Res_UpdateNetworkLevelNew( pNodeNew );
}
// derive the function of this node // derive the function of this node
if ( pIfMan->pPars->fTruth ) if ( pIfMan->pPars->fTruth )
{ {
......
src/base/abci/abcRefactor.c
...@@ -100,7 +100,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool ...@@ -100,7 +100,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut ); pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut );
// compute the reverse levels if level update is requested // compute the reverse levels if level update is requested
if ( fUpdateLevel ) if ( fUpdateLevel )
Abc_NtkStartReverseLevels( pNtk ); Abc_NtkStartReverseLevels( pNtk, 0 );
// resynthesize each node once // resynthesize each node once
nNodes = Abc_NtkObjNumMax(pNtk); nNodes = Abc_NtkObjNumMax(pNtk);
...@@ -187,7 +187,7 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * ...@@ -187,7 +187,7 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
char * pSop; char * pSop;
int Required; int Required;
Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY; Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
p->nNodesConsidered++; p->nNodesConsidered++;
......
src/base/abci/abcRestruct.c
...@@ -114,7 +114,7 @@ int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool f ...@@ -114,7 +114,7 @@ int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool f
// compute the reverse levels if level update is requested // compute the reverse levels if level update is requested
if ( fUpdateLevel ) if ( fUpdateLevel )
Abc_NtkStartReverseLevels( pNtk ); Abc_NtkStartReverseLevels( pNtk, 0 );
// start the restructuring manager // start the restructuring manager
pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose ); pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose );
...@@ -324,7 +324,7 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C ...@@ -324,7 +324,7 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C
p->nCutsConsidered++; p->nCutsConsidered++;
// get the required time for the node // get the required time for the node
Required = p->fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY; Required = p->fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
// collect the leaves of the cut // collect the leaves of the cut
Vec_PtrClear( p->vLeaves ); Vec_PtrClear( p->vLeaves );
......
src/base/abci/abcResub.c
...@@ -159,7 +159,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve ...@@ -159,7 +159,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
// compute the reverse levels if level update is requested // compute the reverse levels if level update is requested
if ( fUpdateLevel ) if ( fUpdateLevel )
Abc_NtkStartReverseLevels( pNtk ); Abc_NtkStartReverseLevels( pNtk, 0 );
if ( Abc_NtkLatchNum(pNtk) ) if ( Abc_NtkLatchNum(pNtk) )
Abc_NtkForEachLatch(pNtk, pNode, i) Abc_NtkForEachLatch(pNtk, pNode, i)
...@@ -1617,7 +1617,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * ...@@ -1617,7 +1617,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
int Required; int Required;
int clk; int clk;
Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY; Required = fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
assert( nSteps >= 0 ); assert( nSteps >= 0 );
assert( nSteps <= 3 ); assert( nSteps <= 3 );
......
src/base/abci/abcRewrite.c
...@@ -83,7 +83,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb ...@@ -83,7 +83,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
return 0; return 0;
// compute the reverse levels if level update is requested // compute the reverse levels if level update is requested
if ( fUpdateLevel ) if ( fUpdateLevel )
Abc_NtkStartReverseLevels( pNtk ); Abc_NtkStartReverseLevels( pNtk, 0 );
// start the cut manager // start the cut manager
clk = clock(); clk = clock();
pManCut = Abc_NtkStartCutManForRewrite( pNtk ); pManCut = Abc_NtkStartCutManForRewrite( pNtk );
......
src/base/abci/abcTiming.c
...@@ -630,39 +630,133 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode ) ...@@ -630,39 +630,133 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prepares the AIG for the comptuation of required levels.] Synopsis [Computes the level of the node using its fanin levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ObjLevelNew( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanin;
int i, Level = 0;
Abc_ObjForEachFanin( pObj, pFanin, i )
Level = ABC_MAX( Level, Abc_ObjLevel(pFanin) );
return Level + 1;
}
/**Function*************************************************************
Synopsis [Computes the reverse level of the node using its fanout levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanout;
int i, LevelCur, Level = 0;
Abc_ObjForEachFanout( pObj, pFanout, i )
{
LevelCur = Abc_ObjReverseLevel( pFanout );
Level = ABC_MAX( Level, LevelCur );
}
return Level + 1;
}
/**Function*************************************************************
Synopsis [Returns required level of the node.]
Description [Converts the reverse levels of the node into its required
level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ObjRequiredLevel( Abc_Obj_t * pObj )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
assert( pNtk->vLevelsR );
return pNtk->LevelMax + 1 - Abc_ObjReverseLevel(pObj);
}
/**Function*************************************************************
Synopsis [Returns the reverse level of the node.]
Description [The reverse level is the level of the node in reverse
topological order, starting from the COs.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ObjReverseLevel( Abc_Obj_t * pObj )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
assert( pNtk->vLevelsR );
Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
}
/**Function*************************************************************
Synopsis [Sets the reverse level of the node.]
Description [The reverse level is the level of the node in reverse
topological order, starting from the COs.]
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
assert( pNtk->vLevelsR );
Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
}
/**Function*************************************************************
Synopsis [Prepares for the computation of required levels.]
Description [This procedure should be called before the required times Description [This procedure should be called before the required times
are used. It starts internal data structures, which records the level are used. It starts internal data structures, which records the level
from the COs of the AIG nodes in reverse topologogical order.] from the COs of the network nodes in reverse topologogical order.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk ) void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease )
{ {
Vec_Ptr_t * vNodes; Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pFanout; Abc_Obj_t * pObj;
int i, k, nLevelsCur; int i;
// assert( Abc_NtkIsStrash(pNtk) );
// remember the maximum number of direct levels // remember the maximum number of direct levels
// pNtk->LevelMax = Abc_AigLevel(pNtk); pNtk->LevelMax = Abc_NtkLevel(pNtk) + nMaxLevelIncrease;
pNtk->LevelMax = Abc_NtkLevel(pNtk);
// start the reverse levels // start the reverse levels
pNtk->vLevelsR = Vec_IntAlloc( 0 ); pNtk->vLevelsR = Vec_IntAlloc( 0 );
Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 ); Vec_IntFill( pNtk->vLevelsR, 1 + Abc_NtkObjNumMax(pNtk), 0 );
// compute levels in reverse topological order // compute levels in reverse topological order
vNodes = Abc_NtkDfsReverse( pNtk ); vNodes = Abc_NtkDfsReverse( pNtk );
Vec_PtrForEachEntry( vNodes, pObj, i ) Vec_PtrForEachEntry( vNodes, pObj, i )
{ Abc_ObjSetReverseLevel( pObj, Abc_ObjReverseLevelNew(pObj) );
nLevelsCur = 0;
Abc_ObjForEachFanout( pObj, pFanout, k )
if ( nLevelsCur < Vec_IntEntry(pNtk->vLevelsR, pFanout->Id) )
nLevelsCur = Vec_IntEntry(pNtk->vLevelsR, pFanout->Id);
Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, nLevelsCur + 1 );
}
Vec_PtrFree( vNodes ); Vec_PtrFree( vNodes );
} }
...@@ -688,64 +782,116 @@ void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk ) ...@@ -688,64 +782,116 @@ void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Sets the reverse level of the node.] Synopsis [Incrementally updates level of the nodes.]
Description [The reverse level is the level of the node in reverse Description []
topological order, starting from the COs.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR ) void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{ {
Abc_Ntk_t * pNtk = pObj->pNtk; Abc_Obj_t * pFanout, * pTemp;
assert( Abc_NtkIsStrash(pNtk) ); int LevelOld, Lev, k, m;
assert( pNtk->vLevelsR ); // check if level has changed
Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 ); LevelOld = Abc_ObjLevel(pObjNew);
Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR ); if ( LevelOld == Abc_ObjLevelNew(pObjNew) )
return;
// start the data structure for level update
// we cannot fail to visit a node when using this structure because the
// nodes are stored by their _old_ levels, which are assumed to be correct
Vec_VecClear( vLevels );
Vec_VecPush( vLevels, LevelOld, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
{
pTemp->fMarkA = 0;
assert( Abc_ObjLevel(pTemp) == Lev );
Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) );
// if the level did not change, to need to check the fanout levels
if ( Abc_ObjLevel(pTemp) == Lev )
continue;
// schedule fanout for level update
Abc_ObjForEachFanout( pTemp, pFanout, m )
{
if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
{
Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout );
pFanout->fMarkA = 1;
}
}
}
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns the reverse level of the node.] Synopsis [Incrementally updates level of the nodes.]
Description [The reverse level is the level of the node in reverse Description []
topological order, starting from the COs.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj ) void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{ {
Abc_Ntk_t * pNtk = pObj->pNtk; Abc_Obj_t * pFanin, * pTemp;
assert( Abc_NtkIsStrash(pNtk) ); int LevelOld, Lev, k, m;
assert( pNtk->vLevelsR ); // check if level has changed
Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 ); LevelOld = Abc_ObjReverseLevel(pObjNew);
return Vec_IntEntry(pNtk->vLevelsR, pObj->Id); if ( LevelOld == Abc_ObjReverseLevelNew(pObjNew) )
return;
// start the data structure for level update
// we cannot fail to visit a node when using this structure because the
// nodes are stored by their _old_ levels, which are assumed to be correct
Vec_VecClear( vLevels );
Vec_VecPush( vLevels, LevelOld, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
{
pTemp->fMarkA = 0;
LevelOld = Abc_ObjReverseLevel(pTemp);
assert( LevelOld == Lev );
Abc_ObjSetReverseLevel( pTemp, Abc_ObjReverseLevelNew(pTemp) );
// if the level did not change, to need to check the fanout levels
if ( Abc_ObjReverseLevel(pTemp) == Lev )
continue;
// schedule fanins for level update
Abc_ObjForEachFanin( pTemp, pFanin, m )
{
if ( !Abc_ObjIsCi(pFanin) && !pFanin->fMarkA )
{
Vec_VecPush( vLevels, Abc_ObjReverseLevel(pFanin), pFanin );
pFanin->fMarkA = 1;
}
}
}
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns required level of the node.] Synopsis [Replaces the node and incrementally updates levels.]
Description [Converts the reverse levels of the node into its required Description []
level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj ) void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{ {
Abc_Ntk_t * pNtk = pObj->pNtk; // replace the old node by the new node
assert( Abc_NtkIsStrash(pNtk) ); pObjNew->Level = pObj->Level;
assert( pNtk->vLevelsR ); Abc_ObjReplace( pObj, pObjNew );
return pNtk->LevelMax + 1 - Vec_IntEntry(pNtk->vLevelsR, pObj->Id); // update the level of the node
Abc_NtkUpdateLevel( pObjNew, vLevels );
Abc_NtkUpdateReverseLevel( pObjNew, vLevels );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcVerify.c
...@@ -705,7 +705,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode ...@@ -705,7 +705,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
nErrors = 0; nErrors = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
nErrors += (int)( pValues1[i] != pValues2[i] ); nErrors += (int)( pValues1[i] != pValues2[i] );
printf( "Verification failed for %d outputs: ", nErrors ); printf( "Verification failed for at least %d outputs: ", nErrors );
// print the first 3 outputs // print the first 3 outputs
nPrinted = 0; nPrinted = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
...@@ -860,7 +860,7 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM ...@@ -860,7 +860,7 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
return; return;
} }
printf( "Verification failed for %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 ); printf( "Verification failed for at least %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
// print the first 3 outputs // print the first 3 outputs
nPrinted = 0; nPrinted = 0;
Abc_NtkForEachPo( pNtk1, pObj1, o ) Abc_NtkForEachPo( pNtk1, pObj1, o )
......
src/base/cmd/cmdHist.c
...@@ -43,7 +43,7 @@ ...@@ -43,7 +43,7 @@
***********************************************************************/ ***********************************************************************/
void Cmd_HistoryAddCommand( Abc_Frame_t * p, char * command ) void Cmd_HistoryAddCommand( Abc_Frame_t * p, char * command )
{ {
char Buffer[500]; static char Buffer[MAX_STR];
strcpy( Buffer, command ); strcpy( Buffer, command );
if ( command[strlen(command)-1] != '\n' ) if ( command[strlen(command)-1] != '\n' )
strcat( Buffer, "\n" ); strcat( Buffer, "\n" );
......
src/misc/vec/vecVec.h
...@@ -77,6 +77,9 @@ struct Vec_Vec_t_ ...@@ -77,6 +77,9 @@ struct Vec_Vec_t_
#define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k ) \ #define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k ) \
for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \ for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \
Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryReverseStart( vGlob, pEntry, i, k, LevelStart ) \
for ( i = LevelStart; i >= 0; i-- ) \
Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
......
src/opt/kit/kit.h
...@@ -121,7 +121,7 @@ struct Kit_DsdNtk_t_ ...@@ -121,7 +121,7 @@ struct Kit_DsdNtk_t_
unsigned char Root; // the root of the tree unsigned char Root; // the root of the tree
unsigned * pMem; // memory for the truth tables (memory manager?) unsigned * pMem; // memory for the truth tables (memory manager?)
unsigned * pSupps; // supports of the nodes unsigned * pSupps; // supports of the nodes
Kit_DsdObj_t * pNodes[0]; // the nodes Kit_DsdObj_t** pNodes; // the nodes
}; };
// DSD manager // DSD manager
...@@ -260,7 +260,15 @@ static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars ) ...@@ -260,7 +260,15 @@ static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
int w; int w;
for ( w = 0; w < Kit_TruthWordNum(nVars); w++ ) for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
if ( pIn[w] ) if ( pIn[w] )
return Kit_WordFindFirstBit(pIn[w]); return 32*w + Kit_WordFindFirstBit(pIn[w]);
return -1;
}
static inline int Kit_TruthFindFirstZero( unsigned * pIn, int nVars )
{
int w;
for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
if ( ~pIn[w] )
return 32*w + Kit_WordFindFirstBit(~pIn[w]);
return -1; return -1;
} }
static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars ) static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
...@@ -444,12 +452,18 @@ extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars ...@@ -444,12 +452,18 @@ extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars
extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph ); extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop ); extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
/*=== kitDsd.c ==========================================================*/ /*=== kitDsd.c ==========================================================*/
extern Kit_DsdMan_t * Kit_DsdManAlloc( int nVars );
extern void Kit_DsdManFree( Kit_DsdMan_t * p );
extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize ); extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk ); extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes ); extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
extern void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk ); extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk ); extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ); extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
extern void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk ); extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk ); extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
extern void Kit_DsdGetSupports( Kit_DsdNtk_t * p ); extern void Kit_DsdGetSupports( Kit_DsdNtk_t * p );
...@@ -510,10 +524,12 @@ extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, i ...@@ -510,10 +524,12 @@ extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, i
extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar ); extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin ); extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
extern int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore ); extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux ); extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
extern unsigned Kit_TruthHash( unsigned * pIn, int nWords ); extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore ); extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
extern char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
#ifdef __cplusplus #ifdef __cplusplus
} }
......
src/opt/kit/kitDsd.c
...@@ -91,6 +91,11 @@ Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans ) ...@@ -91,6 +91,11 @@ Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
pObj->nFans = nFans; pObj->nFans = nFans;
pObj->Offset = Kit_DsdObjOffset( nFans ); pObj->Offset = Kit_DsdObjOffset( nFans );
// add the object // add the object
if ( pNtk->nNodes == pNtk->nNodesAlloc )
{
pNtk->nNodesAlloc *= 2;
pNtk->pNodes = REALLOC( Kit_DsdObj_t *, pNtk->pNodes, pNtk->nNodesAlloc );
}
assert( pNtk->nNodes < pNtk->nNodesAlloc ); assert( pNtk->nNodes < pNtk->nNodesAlloc );
pNtk->pNodes[pNtk->nNodes++] = pObj; pNtk->pNodes[pNtk->nNodes++] = pObj;
return pObj; return pObj;
...@@ -126,10 +131,9 @@ void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj ) ...@@ -126,10 +131,9 @@ void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars ) Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
{ {
Kit_DsdNtk_t * pNtk; Kit_DsdNtk_t * pNtk;
int nSize = sizeof(Kit_DsdNtk_t) + sizeof(void *) * nVars; pNtk = ALLOC( Kit_DsdNtk_t, 1 );
// allocate the network memset( pNtk, 0, sizeof(Kit_DsdNtk_t) );
pNtk = (Kit_DsdNtk_t *)ALLOC( char, nSize ); pNtk->pNodes = ALLOC( Kit_DsdObj_t *, nVars );
memset( pNtk, 0, nSize );
pNtk->nVars = nVars; pNtk->nVars = nVars;
pNtk->nNodesAlloc = nVars; pNtk->nNodesAlloc = nVars;
pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) ); pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
...@@ -154,6 +158,7 @@ void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk ) ...@@ -154,6 +158,7 @@ void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
Kit_DsdNtkForEachObj( pNtk, pObj, i ) Kit_DsdNtkForEachObj( pNtk, pObj, i )
free( pObj ); free( pObj );
FREE( pNtk->pSupps ); FREE( pNtk->pSupps );
free( pNtk->pNodes );
free( pNtk->pMem ); free( pNtk->pMem );
free( pNtk ); free( pNtk );
} }
...@@ -275,7 +280,27 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk ) ...@@ -275,7 +280,27 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
{ {
Kit_DsdNtk_t * pTemp; Kit_DsdNtk_t * pTemp;
pTemp = Kit_DsdExpand( pNtk ); pTemp = Kit_DsdExpand( pNtk );
Kit_DsdPrint( stdout, pNtk ); Kit_DsdPrint( stdout, pTemp );
Kit_DsdNtkFree( pTemp );
}
/**Function*************************************************************
Synopsis [Print the DSD formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
{
Kit_DsdNtk_t * pTemp;
pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
Kit_DsdVerify( pTemp, pTruth, nVars );
Kit_DsdPrintExpanded( pTemp );
Kit_DsdNtkFree( pTemp ); Kit_DsdNtkFree( pTemp );
} }
...@@ -290,11 +315,11 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk ) ...@@ -290,11 +315,11 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id ) unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
{ {
Kit_DsdObj_t * pObj; Kit_DsdObj_t * pObj;
unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16]; unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
unsigned i, m, iLit, nMints, fCompl; unsigned i, m, iLit, nMints, fCompl, fPartial = 0;
// get the node with this ID // get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id ); pObj = Kit_DsdNtkObj( pNtk, Id );
...@@ -304,6 +329,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -304,6 +329,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
if ( pObj == NULL ) if ( pObj == NULL )
{ {
assert( Id < pNtk->nVars ); assert( Id < pNtk->nVars );
assert( !uSupp || uSupp != (uSupp & ~(1<<Id)) );
return pTruthRes; return pTruthRes;
} }
...@@ -320,7 +346,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -320,7 +346,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
{ {
assert( pObj->nFans == 1 ); assert( pObj->nFans == 1 );
iLit = pObj->pFans[0]; iLit = pObj->pFans[0];
pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) ); assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
if ( Kit_DsdLitIsCompl(iLit) ) if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars ); Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
else else
...@@ -329,8 +356,22 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -329,8 +356,22 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
} }
// collect the truth tables of the fanins // collect the truth tables of the fanins
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) if ( uSupp )
pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) ); {
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
else
{
pTruthFans[i] = NULL;
fPartial = 1;
}
}
else
{
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
}
// create the truth table // create the truth table
// simple gates // simple gates
...@@ -338,7 +379,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -338,7 +379,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
{ {
Kit_TruthFill( pTruthRes, pNtk->nVars ); Kit_TruthFill( pTruthRes, pNtk->nVars );
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); if ( pTruthFans[i] )
Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
return pTruthRes; return pTruthRes;
} }
if ( pObj->Type == KIT_DSD_XOR ) if ( pObj->Type == KIT_DSD_XOR )
...@@ -347,8 +389,11 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -347,8 +389,11 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
fCompl = 0; fCompl = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{ {
Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); if ( pTruthFans[i] )
fCompl ^= Kit_DsdLitIsCompl(iLit); {
Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
fCompl ^= Kit_DsdLitIsCompl(iLit);
}
} }
if ( fCompl ) if ( fCompl )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
...@@ -356,6 +401,16 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -356,6 +401,16 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
} }
assert( pObj->Type == KIT_DSD_PRIME ); assert( pObj->Type == KIT_DSD_PRIME );
if ( uSupp && fPartial )
{
// find the only non-empty component
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
if ( pTruthFans[i] )
break;
assert( i < pObj->nFans );
return pTruthFans[i];
}
// get the truth table of the prime node // get the truth table of the prime node
pTruthPrime = Kit_DsdObjTruth( pObj ); pTruthPrime = Kit_DsdObjTruth( pObj );
// get storage for the temporary minterm // get storage for the temporary minterm
...@@ -387,16 +442,19 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i ...@@ -387,16 +442,19 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk ) unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
{ {
unsigned * pTruthRes; unsigned * pTruthRes;
int i; int i;
// assign elementary truth ables // if support is specified, request that supports are available
if ( uSupp )
Kit_DsdGetSupports( pNtk );
// assign elementary truth tables
assert( pNtk->nVars <= p->nVars ); assert( pNtk->nVars <= p->nVars );
for ( i = 0; i < (int)pNtk->nVars; i++ ) for ( i = 0; i < (int)pNtk->nVars; i++ )
Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars ); Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node // compute truth table for each node
pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) ); pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
// complement the truth table if needed // complement the truth table if needed
if ( Kit_DsdLitIsCompl(pNtk->Root) ) if ( Kit_DsdLitIsCompl(pNtk->Root) )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
...@@ -419,13 +477,30 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes ) ...@@ -419,13 +477,30 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
Kit_DsdMan_t * p; Kit_DsdMan_t * p;
unsigned * pTruth; unsigned * pTruth;
p = Kit_DsdManAlloc( pNtk->nVars ); p = Kit_DsdManAlloc( pNtk->nVars );
pTruth = Kit_DsdTruthCompute( p, pNtk ); pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
Kit_DsdManFree( p ); Kit_DsdManFree( p );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
{
unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
}
/**Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.] Synopsis [Counts the number of blocks of the given number of inputs.]
Description [] Description []
...@@ -1085,7 +1160,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 ) ...@@ -1085,7 +1160,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar ) void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux )
{ {
Kit_DsdObj_t * pRes, * pRes0, * pRes1; Kit_DsdObj_t * pRes, * pRes0, * pRes1;
int nWords = Kit_TruthWordNum(pObj->nFans); int nWords = Kit_TruthWordNum(pObj->nFans);
...@@ -1168,11 +1243,10 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS ...@@ -1168,11 +1243,10 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++; pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++; pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
// call recursively // call recursively
Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 ); Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 ); Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
return; return;
} }
//Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
// create the new node // create the new node
pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 ); pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
...@@ -1214,7 +1288,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS ...@@ -1214,7 +1288,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
assert( 0 ); assert( 0 );
// decompose the remainder // decompose the remainder
assert( Kit_DsdObjTruth(pObj) == pTruth ); assert( Kit_DsdObjTruth(pObj) == pTruth );
Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1 ); Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1, nDecMux );
return; return;
} }
pObj->fMark = 1; pObj->fMark = 1;
...@@ -1234,7 +1308,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS ...@@ -1234,7 +1308,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
if ( uSupp0 == 0 || uSupp1 == 0 ) if ( uSupp0 == 0 || uSupp1 == 0 )
{ {
pObj->fMark = 0; pObj->fMark = 0;
Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar ); Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
return; return;
} }
assert( uSupp0 && uSupp1 ); assert( uSupp0 && uSupp1 );
...@@ -1275,7 +1349,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS ...@@ -1275,7 +1349,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
if ( fEquals[1][0] && fEquals[1][1] ) if ( fEquals[1][0] && fEquals[1][1] )
pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]); pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
// decompose the remainder // decompose the remainder
Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar ); Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
return; return;
} }
} }
...@@ -1339,10 +1413,36 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS ...@@ -1339,10 +1413,36 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k ); Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
} }
// decompose the remainder // decompose the remainder
Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar ); Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
return; return;
} }
} }
/*
// if all decomposition methods failed and we are still above the limit, perform MUX-decomposition
if ( nDecMux > 0 && (int)pObj->nFans > nDecMux )
{
int iBestVar = Kit_TruthBestCofVar( pTruth, pObj->nFans, pCofs2[0], pCofs2[1] );
uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
// perform MUX decomposition
pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
for ( k = 0; k < pObj->nFans; k++ )
pRes0->pFans[k] = pRes1->pFans[k] = pObj->pFans[k];
Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
// update the current one
assert( pObj->Type == KIT_DSD_PRIME );
pTruth[0] = 0xCACACACA;
pObj->nFans = 3;
pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
pObj->pFans[2] = pObj->pFans[iBestVar];
// call recursively
Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
}
*/
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1356,7 +1456,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS ...@@ -1356,7 +1456,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) Kit_DsdNtk_t * Kit_DsdDecomposeInt( unsigned * pTruth, int nVars, int nDecMux )
{ {
Kit_DsdNtk_t * pNtk; Kit_DsdNtk_t * pNtk;
Kit_DsdObj_t * pObj; Kit_DsdObj_t * pObj;
...@@ -1389,7 +1489,7 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) ...@@ -1389,7 +1489,7 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
pObj->pFans[0] = Kit_DsdVar2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) ); pObj->pFans[0] = Kit_DsdVar2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
return pNtk; return pNtk;
} }
Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root ); Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root, nDecMux );
return pNtk; return pNtk;
} }
...@@ -1404,6 +1504,38 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) ...@@ -1404,6 +1504,38 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
{
return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
}
/**Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description [Uses MUXes to break-down large prime nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux )
{
return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
}
/**Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit ) int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
{ {
Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp; Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
...@@ -1489,7 +1621,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize ) ...@@ -1489,7 +1621,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
// recompute the truth table // recompute the truth table
p = Kit_DsdManAlloc( nVars ); p = Kit_DsdManAlloc( nVars );
pTruthC = Kit_DsdTruthCompute( p, pNtk ); pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" ); printf( "Verification failed.\n" );
Kit_DsdManFree( p ); Kit_DsdManFree( p );
...@@ -1509,37 +1641,15 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize ) ...@@ -1509,37 +1641,15 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize ) void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
{ {
// Kit_DsdMan_t * p; Kit_DsdMan_t * p;
Kit_DsdNtk_t * pNtk;//, * pTemp; unsigned * pTruthC;
// unsigned * pTruthC;
// int Result;
// decompose the function
pNtk = Kit_DsdDecompose( pTruth, nVars );
// pNtk = Kit_DsdExpand( pTemp = pNtk );
// Kit_DsdNtkFree( pTemp );
// Result = Kit_DsdCountLuts( pNtk, nLutSize );
// printf( "\n" );
// Kit_DsdPrint( stdout, pNtk );
// printf( "Eval = %d.\n", Result );
/*
// recompute the truth table
p = Kit_DsdManAlloc( nVars ); p = Kit_DsdManAlloc( nVars );
pTruthC = Kit_DsdTruthCompute( p, pNtk ); pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" ); printf( "Verification failed.\n" );
Kit_DsdManFree( p ); Kit_DsdManFree( p );
*/
// Kit_DsdNtkFree( pNtk );
// return Result;
return pNtk;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1578,7 +1688,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars ) ...@@ -1578,7 +1688,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
// recompute the truth table // recompute the truth table
p = Kit_DsdManAlloc( nVars ); p = Kit_DsdManAlloc( nVars );
pTruthC = Kit_DsdTruthCompute( p, pNtk ); pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
// Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" ); // Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
// Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" ); // Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
...@@ -1648,7 +1758,7 @@ void Kit_DsdPrecompute4Vars() ...@@ -1648,7 +1758,7 @@ void Kit_DsdPrecompute4Vars()
*/ */
p = Kit_DsdManAlloc( 4 ); p = Kit_DsdManAlloc( 4 );
pTruthC = Kit_DsdTruthCompute( p, pNtk ); pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) ) if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
printf( "Verification failed.\n" ); printf( "Verification failed.\n" );
Kit_DsdManFree( p ); Kit_DsdManFree( p );
......
src/opt/kit/kitGraph.c
...@@ -354,9 +354,10 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor ...@@ -354,9 +354,10 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
Kit_Graph_t * pGraph; Kit_Graph_t * pGraph;
int RetValue; int RetValue;
// derive SOP // derive SOP
RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); // tried 1 and found not useful in "renode" RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
if ( RetValue == -1 ) if ( RetValue == -1 )
return NULL; return NULL;
// printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
assert( RetValue == 0 || RetValue == 1 ); assert( RetValue == 0 || RetValue == 1 );
// derive factored form // derive factored form
pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory ); pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
......
src/opt/kit/kitTruth.c
...@@ -1061,6 +1061,48 @@ int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin ) ...@@ -1061,6 +1061,48 @@ int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Find the best cofactoring variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
{
int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
return -1;
// iterate through variables
iBestVar = -1;
nSuppSizeMin = KIT_INFINITY;
for ( i = 0; i < nVars; i++ )
{
// cofactor the functiona and get support sizes
Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
// compare this variable with other variables
if ( nSuppSizeMin > nSuppSizeCur )
{
nSuppSizeMin = nSuppSizeCur;
iBestVar = i;
}
}
assert( iBestVar != -1 );
// cofactor w.r.t. this variable
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
return iBestVar;
}
/**Function*************************************************************
Synopsis [Counts the number of 1's in each cofactor.] Synopsis [Counts the number of 1's in each cofactor.]
Description [The resulting numbers are stored in the array of shorts, Description [The resulting numbers are stored in the array of shorts,
...@@ -1566,6 +1608,31 @@ void Kit_TruthCountMintermsPrecomp() ...@@ -1566,6 +1608,31 @@ void Kit_TruthCountMintermsPrecomp()
} }
} }
/**Function*************************************************************
Synopsis [Dumps truth table into a file.]
Description [Generates script file for reading into ABC.]
SideEffects []
SeeAlso []
***********************************************************************/
char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
{
static char pFileName[100];
FILE * pFile;
sprintf( pFileName, "s%03d", nFile );
pFile = fopen( pFileName, "w" );
fprintf( pFile, "rt " );
Extra_PrintHexadecimal( pFile, pTruth, nVars );
fprintf( pFile, "; bdd; sop; ps\n" );
fclose( pFile );
return pFileName;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/opt/lpk/lpk.h
...@@ -47,6 +47,7 @@ struct Lpk_Par_t_ ...@@ -47,6 +47,7 @@ struct Lpk_Par_t_
int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis
int fSatur; // iterate till saturation int fSatur; // iterate till saturation
int fZeroCost; // accept zero-cost replacements int fZeroCost; // accept zero-cost replacements
int fFirst; // use root node and first cut only
int fVerbose; // the verbosiness flag int fVerbose; // the verbosiness flag
int fVeryVerbose; // additional verbose info printout int fVeryVerbose; // additional verbose info printout
// internal parameters // internal parameters
......
src/opt/lpk/lpkCore.c
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
Revision [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] Revision [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
#include "lpkInt.h" #include "lpkInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -30,6 +30,54 @@ ...@@ -30,6 +30,54 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_IfManStart( Lpk_Man_t * p )
{
If_Par_t * pPars;
assert( p->pIfMan == NULL );
// set defaults
pPars = ALLOC( If_Par_t, 1 );
memset( pPars, 0, sizeof(If_Par_t) );
// user-controlable paramters
pPars->nLutSize = p->pPars->nLutSize;
pPars->nCutsMax = 16;
pPars->nFlowIters = 0; // 1
pPars->nAreaIters = 0; // 1
pPars->DelayTarget = -1;
pPars->fPreprocess = 0;
pPars->fArea = 1;
pPars->fFancy = 0;
pPars->fExpRed = 0; //
pPars->fLatchPaths = 0;
pPars->fSeqMap = 0;
pPars->fVerbose = 0;
// internal parameters
pPars->fTruth = 1;
pPars->fUsePerm = 0;
pPars->nLatches = 0;
pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
pPars->pTimesArr = NULL;
pPars->pTimesArr = NULL;
pPars->fUseBdds = 0;
pPars->fUseSops = 0;
pPars->fUseCnfs = 0;
pPars->fUseMv = 0;
// start the mapping manager and set its parameters
p->pIfMan = If_ManStart( pPars );
If_ManSetupSetAll( p->pIfMan, 1000 );
p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
}
/**Function*************************************************************
Synopsis [Returns 1 if at least one entry has changed.] Synopsis [Returns 1 if at least one entry has changed.]
Description [] Description []
...@@ -63,6 +111,112 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode ) ...@@ -63,6 +111,112 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
{
extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
Kit_DsdObj_t * pRoot;
If_Obj_t * pDriver, * ppLeaves[16];
Abc_Obj_t * pLeaf, * pObjNew;
int nGain, i, clk;
// int nOldShared;
// check special cases
pRoot = Kit_DsdNtkRoot( pNtk );
if ( pRoot->Type == KIT_DSD_CONST1 )
{
if ( Kit_DsdLitIsCompl(pNtk->Root) )
pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
else
pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
return 1;
}
if ( pRoot->Type == KIT_DSD_VAR )
{
pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
return 1;
}
assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
// start the mapping manager
if ( p->pIfMan == NULL )
Lpk_IfManStart( p );
// prepare the mapping manager
If_ManRestart( p->pIfMan );
// create the PI variables
for ( i = 0; i < p->pPars->nVarsMax; i++ )
ppLeaves[i] = If_ManCreateCi( p->pIfMan );
// set the arrival times
Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
// prepare the PI cuts
If_ManSetupCiCutSets( p->pIfMan );
// create the internal nodes
p->fCalledOnce = 0;
p->nCalledSRed = 0;
pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
if ( pDriver == NULL )
return 0;
// create the PO node
If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
// perform mapping
p->pIfMan->pPars->fAreaOnly = 1;
clk = clock();
If_ManPerformMappingComb( p->pIfMan );
p->timeMap += clock() - clk;
// compute the gain in area
nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
if ( p->pPars->fVeryVerbose )
printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d. SReds = %d.\n",
pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level, p->nCalledSRed );
// quit if there is no gain
if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
return 0;
// quit if depth increases too much
if ( (int)p->pIfMan->RequiredGlo > Abc_ObjRequiredLevel(p->pObj) )
return 0;
// perform replacement
p->nGainTotal += nGain;
p->nChanges++;
if ( p->nCalledSRed )
p->nBenefited++;
// prepare the mapping manager
If_ManCleanNodeCopy( p->pIfMan );
If_ManCleanCutData( p->pIfMan );
// set the PIs of the cut
Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
// get the area of mapping
pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
// perform replacement
Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
return 1;
}
/**Function*************************************************************
Synopsis [Performs resynthesis for one node.] Synopsis [Performs resynthesis for one node.]
Description [] Description []
...@@ -74,13 +228,13 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode ) ...@@ -74,13 +228,13 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
***********************************************************************/ ***********************************************************************/
int Lpk_ResynthesizeNode( Lpk_Man_t * p ) int Lpk_ResynthesizeNode( Lpk_Man_t * p )
{ {
static int Count = 0;
char * pFileName;
Kit_DsdNtk_t * pDsdNtk; Kit_DsdNtk_t * pDsdNtk;
Lpk_Cut_t * pCut; Lpk_Cut_t * pCut;
unsigned * pTruth; unsigned * pTruth;
void * pDsd = NULL; void * pDsd = NULL;
int i, RetValue, clk; int i, nSuppSize, RetValue, clk;
Lpk_Cut_t * pCutMax;
// compute the cuts // compute the cuts
clk = clock(); clk = clock();
...@@ -91,17 +245,6 @@ p->timeCuts += clock() - clk; ...@@ -91,17 +245,6 @@ p->timeCuts += clock() - clk;
} }
p->timeCuts += clock() - clk; p->timeCuts += clock() - clk;
// find the max volume cut
pCutMax = NULL;
for ( i = 0; i < p->nEvals; i++ )
{
pCut = p->pCuts + p->pEvals[i];
if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
pCutMax = pCut;
}
assert( pCutMax != NULL );
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
// try the good cuts // try the good cuts
...@@ -111,20 +254,34 @@ p->timeCuts += clock() - clk; ...@@ -111,20 +254,34 @@ p->timeCuts += clock() - clk;
{ {
// get the cut // get the cut
pCut = p->pCuts + p->pEvals[i]; pCut = p->pCuts + p->pEvals[i];
if ( p->pPars->fFirst && i == 1 )
break;
if ( pCut != pCutMax ) if ( p->pObj->Id == 8835 )
continue; {
int x = 0;
}
// compute the truth table // compute the truth table
clk = clock(); clk = clock();
pTruth = Lpk_CutTruth( p, pCut ); pTruth = Lpk_CutTruth( p, pCut );
nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
p->timeTruth += clock() - clk; p->timeTruth += clock() - clk;
clk = clock(); pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves );
pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize ); // Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves );
p->timeEval += clock() - clk; // skip 16-input non-DSD because ISOP will not work
if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 )
{
Kit_DsdNtkFree( pDsdNtk );
continue;
}
if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work // if DSD has nodes that require splitting to fit them into LUTs
// we can skip those cuts that cannot lead to improvement
// (a full DSD network requires V = Nmin * (K-1) + 1 for improvement)
if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > p->pPars->nLutSize &&
nSuppSize >= ((int)pCut->nNodes - (int)pCut->nNodesDup - 1) * (p->pPars->nLutSize - 1) + 1 )
{ {
Kit_DsdNtkFree( pDsdNtk ); Kit_DsdNtkFree( pDsdNtk );
continue; continue;
...@@ -133,15 +290,18 @@ p->timeEval += clock() - clk; ...@@ -133,15 +290,18 @@ p->timeEval += clock() - clk;
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
{ {
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
Kit_DsdPrint( stdout, pDsdNtk ); Kit_DsdPrint( stdout, pDsdNtk );
// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
printf( "Saved truth table in file \"%s\".\n", pFileName );
} }
// update the network // update the network
clk = clock(); clk = clock();
RetValue = Lpk_CutExplore( p, pCut, pDsdNtk ); RetValue = Lpk_ExploreCut( p, pCut, pDsdNtk );
p->timeEval += clock() - clk;
Kit_DsdNtkFree( pDsdNtk ); Kit_DsdNtkFree( pDsdNtk );
p->timeMap += clock() - clk;
if ( RetValue ) if ( RetValue )
break; break;
} }
...@@ -187,16 +347,28 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) ...@@ -187,16 +347,28 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax ); pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
} }
// convert logic to AIGs
Abc_NtkToAig( pNtk ); // convert into the AIG
if ( !Abc_NtkToAig(pNtk) )
{
fprintf( stdout, "Converting to BDD has failed.\n" );
return 0;
}
assert( Abc_NtkHasAig(pNtk) );
// set the number of levels
Abc_NtkLevel( pNtk );
Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// start the manager // start the manager
p = Lpk_ManStart( pPars ); p = Lpk_ManStart( pPars );
p->pNtk = pNtk; p->pNtk = pNtk;
p->nNodesTotal = Abc_NtkNodeNum(pNtk); p->nNodesTotal = Abc_NtkNodeNum(pNtk);
p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes p->vLevels = Vec_VecStart( pNtk->LevelMax );
if ( p->pPars->fSatur ) if ( p->pPars->fSatur )
p->vVisited = Vec_VecStart( 0 ); p->vVisited = Vec_VecStart( 0 );
if ( pPars->fVerbose )
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
// iterate over the network // iterate over the network
nNodesPrev = p->nNodesTotal; nNodesPrev = p->nNodesTotal;
...@@ -213,8 +385,11 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) ...@@ -213,8 +385,11 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
Abc_NtkForEachNode( pNtk, pObj, i ) Abc_NtkForEachNode( pNtk, pObj, i )
{ {
// skip all except the final node // skip all except the final node
// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) ) if ( pPars->fFirst )
// continue; {
if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
continue;
}
if ( i >= nNodes ) if ( i >= nNodes )
break; break;
...@@ -227,8 +402,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) ...@@ -227,8 +402,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
p->pObj = pObj; p->pObj = pObj;
Lpk_ResynthesizeNode( p ); Lpk_ResynthesizeNode( p );
if ( p->nChanges == 3 ) // if ( p->nChanges == 3 )
break; // break;
} }
if ( !pPars->fVeryVerbose ) if ( !pPars->fVeryVerbose )
Extra_ProgressBarStop( pProgress ); Extra_ProgressBarStop( pProgress );
...@@ -241,19 +416,30 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) ...@@ -241,19 +416,30 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
if ( !p->pPars->fSatur ) if ( !p->pPars->fSatur )
break; break;
break; if ( pPars->fFirst )
break;
} }
Abc_NtkStopReverseLevels( pNtk );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n", p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter ); printf( "Reduction in nodes = %5d. (%.2f %%) ",
printf( "Non_DSD blocks: " ); p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal );
printf( "Reduction in edges = %5d. (%.2f %%) ",
p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
printf( "\n" );
printf( "Nodes = %5d (%3d) Cuts = %5d (%4d) Changes = %5d Iter = %2d Benefit = %d.\n",
p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, Iter, p->nBenefited );
printf( "Non-DSD:" );
for ( i = 3; i <= pPars->nVarsMax; i++ ) for ( i = 3; i <= pPars->nVarsMax; i++ )
if ( p->nBlocks[i] ) if ( p->nBlocks[i] )
printf( "%d=%d ", i, p->nBlocks[i] ); printf( " %d=%d", i, p->nBlocks[i] );
printf( "\n" ); printf( "\n" );
p->timeTotal = clock() - clk; p->timeTotal = clock() - clk;
p->timeEval = p->timeEval - p->timeMap;
p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap; p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
PRTP( "Cuts ", p->timeCuts, p->timeTotal ); PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Truth ", p->timeTruth, p->timeTotal ); PRTP( "Truth ", p->timeTruth, p->timeTotal );
......
src/opt/lpk/lpkCut.c
...@@ -545,11 +545,11 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) ...@@ -545,11 +545,11 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
pCut = p->pCuts + i; pCut = p->pCuts + i;
if ( pCut->nLeaves < 2 ) if ( pCut->nLeaves < 2 )
continue; continue;
// compute the number of LUTs neede to implement this cut // compute the minimum number of LUTs needed to implement this cut
// V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0] // V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 );
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax; pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
if ( pCut->Weight <= 1.0 ) if ( pCut->Weight <= 1.001 )
continue; continue;
pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut ); pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
if ( pCut->fHasDsd ) if ( pCut->fHasDsd )
...@@ -566,7 +566,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) ...@@ -566,7 +566,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
{ {
pCut = p->pCuts + p->pEvals[i]; pCut = p->pCuts + p->pEvals[i];
pCut2 = p->pCuts + p->pEvals[i+1]; pCut2 = p->pCuts + p->pEvals[i+1];
if ( pCut->Weight >= pCut2->Weight ) if ( pCut->Weight >= pCut2->Weight - 0.001 )
continue; continue;
Temp = p->pEvals[i]; Temp = p->pEvals[i];
p->pEvals[i] = p->pEvals[i+1]; p->pEvals[i] = p->pEvals[i+1];
...@@ -574,6 +574,14 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) ...@@ -574,6 +574,14 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
fChanges = 1; fChanges = 1;
} }
} while ( fChanges ); } while ( fChanges );
/*
for ( i = 0; i < p->nEvals; i++ )
{
pCut = p->pCuts + p->pEvals[i];
printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
}
printf( "\n" );
*/
return 1; return 1;
} }
......
src/opt/lpk/lpkInt.h
...@@ -87,6 +87,7 @@ struct Lpk_Man_t_ ...@@ -87,6 +87,7 @@ struct Lpk_Man_t_
// temporary variables // temporary variables
int fCofactoring; // working in the cofactoring mode int fCofactoring; // working in the cofactoring mode
int fCalledOnce; // limits the depth of MUX cofactoring int fCalledOnce; // limits the depth of MUX cofactoring
int nCalledSRed; // the number of called to SRed
int pRefs[LPK_SIZE_MAX]; // fanin reference counters int pRefs[LPK_SIZE_MAX]; // fanin reference counters
int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves
// truth table representation // truth table representation
...@@ -94,6 +95,7 @@ struct Lpk_Man_t_ ...@@ -94,6 +95,7 @@ struct Lpk_Man_t_
Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
// variable sets // variable sets
Vec_Int_t * vSets[8]; Vec_Int_t * vSets[8];
Kit_DsdMan_t * pDsdMan;
// statistics // statistics
int nNodesTotal; // total number of nodes int nNodesTotal; // total number of nodes
int nNodesOver; // nodes with cuts over the limit int nNodesOver; // nodes with cuts over the limit
...@@ -101,6 +103,9 @@ struct Lpk_Man_t_ ...@@ -101,6 +103,9 @@ struct Lpk_Man_t_
int nCutsUseful; // useful cuts int nCutsUseful; // useful cuts
int nGainTotal; // the gain in LUTs int nGainTotal; // the gain in LUTs
int nChanges; // the number of changed nodes int nChanges; // the number of changed nodes
int nBenefited; // the number of gainful that benefited from decomposition
int nTotalNets;
int nTotalNets2;
// counter of non-DSD blocks // counter of non-DSD blocks
int nBlocks[17]; int nBlocks[17];
// rutime // rutime
...@@ -138,7 +143,6 @@ extern int Lpk_NodeCuts( Lpk_Man_t * p ); ...@@ -138,7 +143,6 @@ extern int Lpk_NodeCuts( Lpk_Man_t * p );
extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ); extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars );
extern void Lpk_ManStop( Lpk_Man_t * p ); extern void Lpk_ManStop( Lpk_Man_t * p );
/*=== lpkMap.c =========================================================*/ /*=== lpkMap.c =========================================================*/
extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult ); extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
/*=== lpkMulti.c =======================================================*/ /*=== lpkMulti.c =======================================================*/
......
src/opt/lpk/lpkMan.c
...@@ -54,6 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) ...@@ -54,6 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
p->vCover = Vec_IntAlloc( 1 << 12 ); p->vCover = Vec_IntAlloc( 1 << 12 );
for ( i = 0; i < 8; i++ ) for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100); p->vSets[i] = Vec_IntAlloc(100);
p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
return p; return p;
} }
...@@ -71,6 +72,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) ...@@ -71,6 +72,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
void Lpk_ManStop( Lpk_Man_t * p ) void Lpk_ManStop( Lpk_Man_t * p )
{ {
int i; int i;
Kit_DsdManFree( p->pDsdMan );
for ( i = 0; i < 8; i++ ) for ( i = 0; i < 8; i++ )
Vec_IntFree(p->vSets[i]); Vec_IntFree(p->vSets[i]);
if ( p->pIfMan ) if ( p->pIfMan )
......
src/opt/lpk/lpkMap.c
...@@ -24,62 +24,12 @@ ...@@ -24,62 +24,12 @@
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_IfManStart( Lpk_Man_t * p )
{
If_Par_t * pPars;
assert( p->pIfMan == NULL );
// set defaults
pPars = ALLOC( If_Par_t, 1 );
memset( pPars, 0, sizeof(If_Par_t) );
// user-controlable paramters
pPars->nLutSize = p->pPars->nLutSize;
pPars->nCutsMax = 16;
pPars->nFlowIters = 0; // 1
pPars->nAreaIters = 0; // 1
pPars->DelayTarget = -1;
pPars->fPreprocess = 0;
pPars->fArea = 1;
pPars->fFancy = 0;
pPars->fExpRed = 0; //
pPars->fLatchPaths = 0;
pPars->fSeqMap = 0;
pPars->fVerbose = 0;
// internal parameters
pPars->fTruth = 0;
pPars->fUsePerm = 0;
pPars->nLatches = 0;
pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
pPars->pTimesArr = NULL;
pPars->pTimesArr = NULL;
pPars->fUseBdds = 0;
pPars->fUseSops = 0;
pPars->fUseCnfs = 0;
pPars->fUseMv = 0;
// start the mapping manager and set its parameters
p->pIfMan = If_ManStart( pPars );
If_ManSetupSetAll( p->pIfMan, 1000 );
p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
}
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.] Synopsis [Transforms the decomposition graph into the AIG.]
Description [] Description []
...@@ -154,122 +104,10 @@ If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t * ...@@ -154,122 +104,10 @@ If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t *
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
{
extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
Kit_DsdObj_t * pRoot;
If_Obj_t * pDriver, * ppLeaves[16];
Abc_Obj_t * pLeaf, * pObjNew;
int nGain, i;
// int nOldShared;
// check special cases
pRoot = Kit_DsdNtkRoot( pNtk );
if ( pRoot->Type == KIT_DSD_CONST1 )
{
if ( Kit_DsdLitIsCompl(pNtk->Root) )
pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
else
pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
// perform replacement
pObjNew->Level = p->pObj->Level;
Abc_ObjReplace( p->pObj, pObjNew );
Res_UpdateNetworkLevel( pObjNew, p->vLevels );
p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
return 1;
}
if ( pRoot->Type == KIT_DSD_VAR )
{
pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
// perform replacement
pObjNew->Level = p->pObj->Level;
Abc_ObjReplace( p->pObj, pObjNew );
Res_UpdateNetworkLevel( pObjNew, p->vLevels );
p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
return 1;
}
assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
// start the mapping manager
if ( p->pIfMan == NULL )
Lpk_IfManStart( p );
// prepare the mapping manager
If_ManRestart( p->pIfMan );
// create the PI variables
for ( i = 0; i < p->pPars->nVarsMax; i++ )
ppLeaves[i] = If_ManCreateCi( p->pIfMan );
// set the arrival times
Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
// prepare the PI cuts
If_ManSetupCiCutSets( p->pIfMan );
// create the internal nodes
p->fCalledOnce = 0;
pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
if ( pDriver == NULL )
return 0;
// create the PO node
If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
// perform mapping
p->pIfMan->pPars->fAreaOnly = 1;
If_ManPerformMappingComb( p->pIfMan );
// compute the gain in area
nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
if ( p->pPars->fVeryVerbose )
printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n",
pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
// quit if there is no gain
if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
return 0;
// quit if depth increases too much
if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
return 0;
// perform replacement
p->nGainTotal += nGain;
p->nChanges++;
// prepare the mapping manager
If_ManCleanNodeCopy( p->pIfMan );
If_ManCleanCutData( p->pIfMan );
// set the PIs of the cut
Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
// get the area of mapping
pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
// perform replacement
pObjNew->Level = p->pObj->Level;
Abc_ObjReplace( p->pObj, pObjNew );
Res_UpdateNetworkLevel( pObjNew, p->vLevels );
return 1;
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult ) If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
{ {
Kit_DsdObj_t * pObj; Kit_DsdObj_t * pObj;
If_Obj_t * pObjNew, * pFansNew[16]; If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
unsigned i, iLitFanin; unsigned i, iLitFanin;
assert( iLit >= 0 ); assert( iLit >= 0 );
...@@ -325,20 +163,38 @@ If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLe ...@@ -325,20 +163,38 @@ If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLe
if ( pFansNew[i] == NULL ) if ( pFansNew[i] == NULL )
return NULL; return NULL;
} }
/* /*
if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize ) if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
{ {
pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
} }
*/ */
/*
if ( (int)pObj->nFans > p->pPars->nLutSize )
{
pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
// if ( pObjNew2 )
// return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
}
*/
// find best cofactoring variable // find best cofactoring variable
if ( pObj->nFans > 3 && !p->fCalledOnce ) if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); {
pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
else if ( pObjNew2 )
pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
}
pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
// add choice
if ( pObjNew && pObjNew2 )
{
If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
}
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
} }
......
src/opt/lpk/lpkMux.c
...@@ -39,18 +39,12 @@ ...@@ -39,18 +39,12 @@
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars ) int Lpk_MapTreeBestCofVar( Lpk_Man_t * p, unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
{ {
// Kit_DsdNtk_t * ppNtks[2], * pTemp;
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin; int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
// iterate through variables // iterate through variables
iBestVar = -1; iBestVar = -1;
nSuppSizeMin = ABC_INFINITY; nSuppSizeMin = KIT_INFINITY;
// nPrimeSizeMin = ABC_INFINITY;
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
{ {
// cofactor the functiona and get support sizes // cofactor the functiona and get support sizes
...@@ -59,44 +53,22 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars ) ...@@ -59,44 +53,22 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars ); nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars ); nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1; nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
/* // skip cofactoring that goes above the limit
// check the size of the largest prime components if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize )
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); continue;
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
// compute the largest non-decomp block
nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
printf( "Evaluating variable %c:\n", 'a'+i );
// Kit_DsdPrintExpanded( ppNtks[0] );
// Kit_DsdPrintExpanded( ppNtks[1] );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
Kit_DsdNtkFree( pTemp );
Kit_DsdPrint( stdout, ppNtks[0] );
Kit_DsdPrint( stdout, ppNtks[1] );
// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
// free the networks
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
*/
// compare this variable with other variables // compare this variable with other variables
if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) ) if ( nSuppSizeMin > nSuppSizeCur )
{ {
nSuppSizeMin = nSuppSizeCur; nSuppSizeMin = nSuppSizeCur;
// nPrimeSizeMin = nPrimeSizeCur;
iBestVar = i; iBestVar = i;
} }
} }
printf( "\n" ); // cofactor w.r.t. this variable
assert( iBestVar != -1 ); if ( iBestVar != -1 )
{
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
}
return iBestVar; return iBestVar;
} }
...@@ -113,18 +85,17 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars ) ...@@ -113,18 +85,17 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
***********************************************************************/ ***********************************************************************/
If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{ {
If_Obj_t * pObj0, * pObj1;
Kit_DsdNtk_t * ppNtks[2];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
If_Obj_t * pObj0, * pObj1;
Kit_DsdNtk_t * ppNtks[2];
int iBestVar; int iBestVar;
assert( nVars > 3 ); assert( nVars > 3 );
p->fCalledOnce = 1; p->fCalledOnce = 1;
// cofactor w.r.t. the best variable // cofactor w.r.t. the best variable
iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars ); iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar ); if ( iBestVar == -1 )
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar ); return NULL;
// decompose the functions // decompose the functions
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
...@@ -158,7 +129,7 @@ If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_O ...@@ -158,7 +129,7 @@ If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_O
***********************************************************************/ ***********************************************************************/
If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{ {
Kit_DsdNtk_t * pNtkDec, * pNtkComp; Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
If_Obj_t * pObjNew; If_Obj_t * pObjNew;
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
...@@ -172,80 +143,96 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I ...@@ -172,80 +143,96 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I
unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 ); unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 );
unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 ); unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 );
unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 ); unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 );
int TrueMint0, TrueMint1; int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i; int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
// determine if supp-red decomposition exists // determine if supp-red decomposition exists
uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused ); uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
if ( uSubsets == 0 ) if ( uSubsets == 0 )
return NULL; return NULL;
p->nCalledSRed++;
// get the bound sets
uSubset0 = uSubsets & 0xFFFF;
uSubset1 = uSubsets >> 16;
// get the cofactors // get the cofactors
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar ); Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar ); Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
// find any true assignments of the cofactors
TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars ); // get the bound sets
TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars ); uSubset0 = uSubsets & 0xFFFF;
uSubset1 = uSubsets >> 16;
// compute the decomposed functions
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
//Kit_DsdPrintFromTruth( pDec0, nVars );
//Kit_DsdPrintFromTruth( pDec1, nVars );
// get the decomposed function
Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
// find any true assignments of the decomposed functions
TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
assert( TrueMint0 >= 0 && TrueMint1 >= 0 ); assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
// find any false assignments of the decomposed functions
FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
// cofactor the cofactors according to these minterms // cofactor the cofactors according to these minterms
Kit_TruthCopy( pDec0, pCof0, nVars ); Kit_TruthCopy( pCo00, pCof0, nVars );
Kit_TruthCopy( pDec1, pCof1, nVars ); Kit_TruthCopy( pCo01, pCof0, nVars );
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
if ( !(uSubset0 & (1 << i)) ) if ( uSubset0 & (1 << i) )
{ {
if ( FalseMint0 & (1 << i) )
Kit_TruthCofactor1( pCo00, nVars, i );
else
Kit_TruthCofactor0( pCo00, nVars, i );
if ( TrueMint0 & (1 << i) ) if ( TrueMint0 & (1 << i) )
Kit_TruthCofactor1( pDec0, nVars, i ); Kit_TruthCofactor1( pCo01, nVars, i );
else else
Kit_TruthCofactor0( pDec0, nVars, i ); Kit_TruthCofactor0( pCo01, nVars, i );
} }
Kit_TruthCopy( pCo10, pCof1, nVars );
Kit_TruthCopy( pCo11, pCof1, nVars );
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
if ( !(uSubset1 & (1 << i)) ) if ( uSubset1 & (1 << i) )
{ {
if ( FalseMint1 & (1 << i) )
Kit_TruthCofactor1( pCo10, nVars, i );
else
Kit_TruthCofactor0( pCo10, nVars, i );
if ( TrueMint1 & (1 << i) ) if ( TrueMint1 & (1 << i) )
Kit_TruthCofactor1( pDec1, nVars, i ); Kit_TruthCofactor1( pCo11, nVars, i );
else else
Kit_TruthCofactor0( pDec1, nVars, i ); Kit_TruthCofactor0( pCo11, nVars, i );
} }
// get the decomposed function
Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
// derive the remainders
Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
// quantify bound set variables
for ( i = 0; i < nVars; i++ )
if ( uSubset0 & (1 << i) )
{
Kit_TruthExist( pCo00, nVars, i );
Kit_TruthExist( pCo01, nVars, i );
}
for ( i = 0; i < nVars; i++ )
if ( uSubset1 & (1 << i) )
{
Kit_TruthExist( pCo10, nVars, i );
Kit_TruthExist( pCo11, nVars, i );
}
// derive the functions by composing them with the new variable (iVarReused) // derive the functions by composing them with the new variable (iVarReused)
Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused ); Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused ); Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
//Kit_DsdPrintFromTruth( pCo0, nVars );
//Kit_DsdPrintFromTruth( pCo1, nVars );
// derive the composition function // derive the composition function
Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar ); Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
// process the decomposed function // process the decomposed function
pNtkDec = Kit_DsdDecompose( pDec, nVars ); pNtkDec = Kit_DsdDecompose( pDec, nVars );
Kit_DsdPrint( stdout, pNtkDec );
ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
Kit_DsdNtkFree( pNtkDec );
// process the composition function
pNtkComp = Kit_DsdDecompose( pCo, nVars ); pNtkComp = Kit_DsdDecompose( pCo, nVars );
Kit_DsdPrint( stdout, pNtkComp ); //Kit_DsdPrint( stdout, pNtkDec );
//Kit_DsdPrint( stdout, pNtkComp );
//printf( "cofactored variable %c\n", 'a' + iVar );
//printf( "reused variable %c\n", 'a' + iVarReused );
ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL ); pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
Kit_DsdNtkFree( pNtkDec );
Kit_DsdNtkFree( pNtkComp ); Kit_DsdNtkFree( pNtkComp );
return pObjNew; return pObjNew;
} }
......
src/opt/lpk/lpkSets.c
...@@ -104,7 +104,8 @@ unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets ) ...@@ -104,7 +104,8 @@ unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
***********************************************************************/ ***********************************************************************/
unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets ) unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
{ {
unsigned uSupport, Entry, i; unsigned uSupport, Entry;
int Number, i;
assert( p->nVars <= 16 ); assert( p->nVars <= 16 );
Vec_IntClear( vSets ); Vec_IntClear( vSets );
Vec_IntPush( vSets, 0 ); Vec_IntPush( vSets, 0 );
...@@ -120,8 +121,11 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets ) ...@@ -120,8 +121,11 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
assert( (uSupport & 0xFFFF0000) == 0 ); assert( (uSupport & 0xFFFF0000) == 0 );
Vec_IntPush( vSets, uSupport ); Vec_IntPush( vSets, uSupport );
// set the remaining variables // set the remaining variables
Vec_IntForEachEntry( vSets, Entry, i ) Vec_IntForEachEntry( vSets, Number, i )
{
Entry = Number;
Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) ); Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
}
return uSupport; return uSupport;
} }
...@@ -157,10 +161,14 @@ void Lpk_PrintSetOne( int uSupport ) ...@@ -157,10 +161,14 @@ void Lpk_PrintSetOne( int uSupport )
***********************************************************************/ ***********************************************************************/
void Lpk_PrintSets( Vec_Int_t * vSets ) void Lpk_PrintSets( Vec_Int_t * vSets )
{ {
unsigned uSupport, i; unsigned uSupport;
int Number, i;
printf( "Subsets(%d): ", Vec_IntSize(vSets) ); printf( "Subsets(%d): ", Vec_IntSize(vSets) );
Vec_IntForEachEntry( vSets, uSupport, i ) Vec_IntForEachEntry( vSets, Number, i )
{
uSupport = Number;
Lpk_PrintSetOne( uSupport ); Lpk_PrintSetOne( uSupport );
}
printf( "\n" ); printf( "\n" );
} }
...@@ -237,7 +245,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo ...@@ -237,7 +245,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
} }
} }
// check if there are non-overlapping // find the minimum overlap
nMinOver = 1000; nMinOver = 1000;
for ( s = 0; s < nUsed; s++ ) for ( s = 0; s < nUsed; s++ )
if ( nMinOver > Over[Used[s]] ) if ( nMinOver > Over[Used[s]] )
...@@ -267,7 +275,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo ...@@ -267,7 +275,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
// get the number of overlapping vars // get the number of overlapping vars
pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) ); pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
// get the support reduction // get the support reduction
pEntry->SRed = pEntry->Size - 1 - pEntry->Over; pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
assert( pEntry->SRed > 0 ); assert( pEntry->SRed > 0 );
} }
} }
...@@ -318,13 +326,21 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i ...@@ -318,13 +326,21 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
Vec_Int_t * vSets1 = p->vSets[1]; Vec_Int_t * vSets1 = p->vSets[1];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int nSets, i, SizeMax; int nSets, i, SizeMax;//, SRedMax;
unsigned Entry; unsigned Entry;
int fVerbose = p->pPars->fVeryVerbose;
// int fVerbose = 0;
// collect decomposable subsets for each pair of cofactors // collect decomposable subsets for each pair of cofactors
if ( fVerbose )
{
printf( "\nExploring support-reducing bound-sets of function:\n" );
Kit_DsdPrintFromTruth( pTruth, nVars );
}
nSets = 0; nSets = 0;
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
{ {
if ( fVerbose )
printf( "Evaluating variable %c:\n", 'a'+i ); printf( "Evaluating variable %c:\n", 'a'+i );
// evaluate the cofactor pair // evaluate the cofactor pair
Kit_TruthCofactor0New( pCof0, pTruth, nVars, i ); Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
...@@ -334,13 +350,17 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i ...@@ -334,13 +350,17 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp ); ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp ); ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[0] ); Kit_DsdPrint( stdout, ppNtks[0] );
if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[1] ); Kit_DsdPrint( stdout, ppNtks[1] );
// compute subsets // compute subsets
Lpk_ComputeSets( ppNtks[0], vSets0 ); Lpk_ComputeSets( ppNtks[0], vSets0 );
Lpk_ComputeSets( ppNtks[1], vSets1 ); Lpk_ComputeSets( ppNtks[1], vSets1 );
// print subsets // print subsets
if ( fVerbose )
Lpk_PrintSets( vSets0 ); Lpk_PrintSets( vSets0 );
if ( fVerbose )
Lpk_PrintSets( vSets1 ); Lpk_PrintSets( vSets1 );
// free the networks // free the networks
Kit_DsdNtkFree( ppNtks[0] ); Kit_DsdNtkFree( ppNtks[0] );
...@@ -350,7 +370,9 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i ...@@ -350,7 +370,9 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
} }
// print the results // print the results
if ( fVerbose )
printf( "\n" ); printf( "\n" );
if ( fVerbose )
for ( i = 0; i < nSets; i++ ) for ( i = 0; i < nSets; i++ )
Lpk_MapSuppPrintSet( pStore + i, i ); Lpk_MapSuppPrintSet( pStore + i, i );
...@@ -368,14 +390,33 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i ...@@ -368,14 +390,33 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
SizeMax = pSet->Size; SizeMax = pSet->Size;
} }
} }
/*
// if the best is not choosen, select the one with largest reduction
SRedMax = 0;
if ( pSetBest == NULL )
{
for ( i = 0; i < nSets; i++ )
{
pSet = pStore + i;
if ( SRedMax < pSet->SRed )
{
pSetBest = pSet;
SRedMax = pSet->SRed;
}
}
}
*/
if ( pSetBest == NULL ) if ( pSetBest == NULL )
{ {
if ( fVerbose )
printf( "Could not select a subset.\n" ); printf( "Could not select a subset.\n" );
return 0; return 0;
} }
else else
{ {
if ( fVerbose )
printf( "Selected the following subset:\n" ); printf( "Selected the following subset:\n" );
if ( fVerbose )
Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore ); Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
} }
......
src/opt/res/module.make
...@@ -4,5 +4,4 @@ SRC += src/opt/res/resCore.c \ ...@@ -4,5 +4,4 @@ SRC += src/opt/res/resCore.c \
src/opt/res/resSat.c \ src/opt/res/resSat.c \
src/opt/res/resSim.c \ src/opt/res/resSim.c \
src/opt/res/resStrash.c \ src/opt/res/resStrash.c \
src/opt/res/resUpdate.c \
src/opt/res/resWin.c src/opt/res/resWin.c
src/opt/res/resCore.c
...@@ -102,9 +102,9 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars ) ...@@ -102,9 +102,9 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
p->pSim = Res_SimAlloc( pPars->nSimWords ); p->pSim = Res_SimAlloc( pPars->nSimWords );
p->pMan = Int_ManAlloc( 512 ); p->pMan = Int_ManAlloc( 512 );
p->vMem = Vec_IntAlloc( 0 ); p->vMem = Vec_IntAlloc( 0 );
p->vResubs = Vec_VecStart( pPars->nCands ); p->vResubs = Vec_VecStart( pPars->nCands );
p->vResubsW = Vec_VecStart( pPars->nCands ); p->vResubsW = Vec_VecStart( pPars->nCands );
p->vLevels = Vec_VecStart( 32 ); p->vLevels = Vec_VecStart( 32 );
return p; return p;
} }
...@@ -123,6 +123,14 @@ void Res_ManFree( Res_Man_t * p ) ...@@ -123,6 +123,14 @@ void Res_ManFree( Res_Man_t * p )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
{ {
printf( "Reduction in nodes = %5d. (%.2f %%) ",
p->nTotalNodes-p->nTotalNodes2,
100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
printf( "Reduction in edges = %5d. (%.2f %%) ",
p->nTotalNets-p->nTotalNets2,
100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
printf( "\n" );
printf( "Winds = %d. ", p->nWins ); printf( "Winds = %d. ", p->nWins );
printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins ); printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins ); printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
...@@ -134,13 +142,6 @@ void Res_ManFree( Res_Man_t * p ) ...@@ -134,13 +142,6 @@ void Res_ManFree( Res_Man_t * p )
printf( "Cands = %d. ", p->nCandSets ); printf( "Cands = %d. ", p->nCandSets );
printf( "Proved = %d.", p->nProvedSets ); printf( "Proved = %d.", p->nProvedSets );
printf( "\n" ); printf( "\n" );
printf( "Reduction in nodes = %d. (%.2f %%) ",
p->nTotalNodes-p->nTotalNodes2,
100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
printf( "Reduction in nets = %d. (%.2f %%) ",
p->nTotalNets-p->nTotalNets2,
100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
printf( "\n" );
PRTP( "Windowing ", p->timeWin, p->timeTotal ); PRTP( "Windowing ", p->timeWin, p->timeTotal );
PRTP( "Divisors ", p->timeDiv, p->timeTotal ); PRTP( "Divisors ", p->timeDiv, p->timeTotal );
...@@ -153,7 +154,7 @@ void Res_ManFree( Res_Man_t * p ) ...@@ -153,7 +154,7 @@ void Res_ManFree( Res_Man_t * p )
PRTP( " simul ", p->timeSatSim, p->timeTotal ); PRTP( " simul ", p->timeSatSim, p->timeTotal );
PRTP( "Interpol ", p->timeInt, p->timeTotal ); PRTP( "Interpol ", p->timeInt, p->timeTotal );
PRTP( "Undating ", p->timeUpd, p->timeTotal ); PRTP( "Undating ", p->timeUpd, p->timeTotal );
PRT( "TOTAL ", p->timeTotal ); PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
} }
Res_WinFree( p->pWin ); Res_WinFree( p->pWin );
if ( p->pAig ) Abc_NtkDelete( p->pAig ); if ( p->pAig ) Abc_NtkDelete( p->pAig );
...@@ -169,6 +170,31 @@ void Res_ManFree( Res_Man_t * p ) ...@@ -169,6 +170,31 @@ void Res_ManFree( Res_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pObjNew, * pFanin;
int k;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
// update the level of the node
Abc_NtkUpdate( pObj, pObjNew, vLevels );
}
/**Function*************************************************************
Synopsis [Entrace into the resynthesis package.] Synopsis [Entrace into the resynthesis package.]
Description [] Description []
...@@ -210,6 +236,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ) ...@@ -210,6 +236,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
// set the number of levels // set the number of levels
Abc_NtkLevel( pNtk ); Abc_NtkLevel( pNtk );
Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// try resynthesizing nodes in the topological order // try resynthesizing nodes in the topological order
nNodesOld = Abc_NtkObjNumMax(pNtk); nNodesOld = Abc_NtkObjNumMax(pNtk);
...@@ -239,10 +266,10 @@ p->timeWin += clock() - clk; ...@@ -239,10 +266,10 @@ p->timeWin += clock() - clk;
Vec_PtrSize(p->pWin->vNodes), Vec_PtrSize(p->pWin->vNodes),
Vec_PtrSize(p->pWin->vRoots) ); Vec_PtrSize(p->pWin->vRoots) );
} }
// collect the divisors // collect the divisors
clk = clock(); clk = clock();
Res_WinDivisors( p->pWin, pObj->Level + pPars->nGrowthLevel - 1 ); Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
p->timeDiv += clock() - clk; p->timeDiv += clock() - clk;
p->nWins++; p->nWins++;
...@@ -359,6 +386,7 @@ p->timeUpd += clock() - clk; ...@@ -359,6 +386,7 @@ p->timeUpd += clock() - clk;
// printf( "\n" ); // printf( "\n" );
} }
Extra_ProgressBarStop( pProgress ); Extra_ProgressBarStop( pProgress );
Abc_NtkStopReverseLevels( pNtk );
p->timeSatSim += p->pSim->timeSat; p->timeSatSim += p->pSim->timeSat;
p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim; p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
......
src/opt/res/resUpdate.c deleted 100644 → 0
/**CFile****************************************************************
FileName [resUpdate.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resynthesis package.]
Synopsis [Updates the network after changes.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [$Id: resUpdate.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "resInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the level of the node using its fanin levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanin;
int i, Level = 0;
Abc_ObjForEachFanin( pObj, pFanin, i )
Level = ABC_MAX( Level, (int)pFanin->Level );
return Level + 1;
}
/**Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pFanout, * pTemp;
int Lev, k, m;
// check if level has changed
if ( (int)pObjNew->Level == Res_UpdateNetworkLevelNew(pObjNew) )
return;
// start the data structure for level update
Vec_VecClear( vLevels );
Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level )
{
pTemp->fMarkA = 0;
pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
// if the level did not change, to need to check the fanout levels
if ( (int)pTemp->Level == Lev )
continue;
// schedule fanout for level update
Abc_ObjForEachFanout( pTemp, pFanout, m )
if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
{
Vec_VecPush( vLevels, pFanout->Level, pFanout );
pFanout->fMarkA = 1;
}
}
}
/**Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pObjNew, * pFanin;
int k;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
pObjNew->Level = pObj->Level;
Abc_ObjReplace( pObj, pObjNew );
// update the level of the node
Res_UpdateNetworkLevel( pObjNew, vLevels );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/rwr/rwrEva.c
...@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int ...@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
p->nNodesConsidered++; p->nNodesConsidered++;
// get the required times // get the required times
Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY; Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
// get the node's cuts // get the node's cuts
clk = clock(); clk = clock();
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment