Skip to content

A
abc
Commit 00dc0f3d by Alan Mishchenko
Options

Version abc70406

parent 028138a7
Showing with 831 additions and 249 deletions
abc.rc
...@@ -30,6 +30,7 @@ alias fs fraig_sweep ...@@ -30,6 +30,7 @@ alias fs fraig_sweep
alias fsto fraig_store alias fsto fraig_store
alias fres fraig_restore alias fres fraig_restore
alias ft fraig_trust alias ft fraig_trust
alias lp lutpack
alias pex print_exdc -d alias pex print_exdc -d
alias pf print_factor alias pf print_factor
alias pfan print_fanio alias pfan print_fanio
...@@ -165,3 +166,5 @@ alias trec12 "rec_start -K 12; r i10.blif; st; rec_add; rec_use" ...@@ -165,3 +166,5 @@ alias trec12 "rec_start -K 12; r i10.blif; st; rec_add; rec_use"
alias tst4 "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4.blif; st -r; ps; cec" alias tst4 "r i10_if4.blif; st; ps; r x/rec4_.blif; 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 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"
src/aig/hop/hop.h
...@@ -314,6 +314,7 @@ extern void Hop_TableProfile( Hop_Man_t * p ); ...@@ -314,6 +314,7 @@ extern void Hop_TableProfile( Hop_Man_t * p );
/*=== aigUtil.c =========================================================*/ /*=== aigUtil.c =========================================================*/
extern void Hop_ManIncrementTravId( Hop_Man_t * p ); extern void Hop_ManIncrementTravId( Hop_Man_t * p );
extern void Hop_ManCleanData( Hop_Man_t * p ); extern void Hop_ManCleanData( Hop_Man_t * p );
extern void Hop_ObjCleanData_rec( Hop_Obj_t * pObj );
extern void Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSuper ); extern void Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSuper );
extern int Hop_ObjIsMuxType( Hop_Obj_t * pObj ); extern int Hop_ObjIsMuxType( Hop_Obj_t * pObj );
extern int Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 ); extern int Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 );
......
src/aig/hop/hopUtil.c
...@@ -48,7 +48,7 @@ void Hop_ManIncrementTravId( Hop_Man_t * p ) ...@@ -48,7 +48,7 @@ void Hop_ManIncrementTravId( Hop_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Sets the DFS ordering of the nodes.] Synopsis [Cleans the data pointers for the nodes.]
Description [] Description []
...@@ -73,6 +73,29 @@ void Hop_ManCleanData( Hop_Man_t * p ) ...@@ -73,6 +73,29 @@ void Hop_ManCleanData( Hop_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Recursively cleans the data pointers in the cone of the node.]
Description [Applicable to small AIGs only because no caching is performed.]
SideEffects []
SeeAlso []
***********************************************************************/
void Hop_ObjCleanData_rec( Hop_Obj_t * pObj )
{
assert( !Hop_IsComplement(pObj) );
assert( !Hop_ObjIsPo(pObj) );
if ( Hop_ObjIsAnd(pObj) )
{
Hop_ObjCleanData_rec( Hop_ObjFanin0(pObj) );
Hop_ObjCleanData_rec( Hop_ObjFanin1(pObj) );
}
pObj->pData = NULL;
}
/**Function*************************************************************
Synopsis [Detects multi-input gate rooted at this node.] Synopsis [Detects multi-input gate rooted at this node.]
Description [] Description []
......
src/base/abc/abc.h
...@@ -787,6 +787,7 @@ extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * ...@@ -787,6 +787,7 @@ extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t *
extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSize( Abc_Obj_t * pNode );
extern int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
extern int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
extern void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); extern void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
extern int Abc_NodeDeref_rec( Abc_Obj_t * pNode ); extern int Abc_NodeDeref_rec( Abc_Obj_t * pNode );
......
src/base/abc/abcCheck.c
...@@ -523,7 +523,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) ...@@ -523,7 +523,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
// the node should have a function assigned unless it is an AIG // the node should have a function assigned unless it is an AIG
if ( pNode->pData == NULL ) if ( pNode->pData == NULL )
{ {
fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_ObjName(pNode) ); fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_NtkIsNetlist(pNode->pNtk)? Abc_ObjName(Abc_ObjFanout0(pNode)) : Abc_ObjName(pNode) );
return 0; return 0;
} }
// the netlist and SOP logic network should have SOPs // the netlist and SOP logic network should have SOPs
......
src/base/abc/abcRefs.c
...@@ -94,7 +94,7 @@ int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ) ...@@ -94,7 +94,7 @@ int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NodeMffcLabel( Abc_Obj_t * pNode ) int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode )
{ {
int nConeSize1, nConeSize2; int nConeSize1, nConeSize2;
assert( Abc_NtkIsStrash(pNode->pNtk) ); assert( Abc_NtkIsStrash(pNode->pNtk) );
...@@ -279,6 +279,7 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * ...@@ -279,6 +279,7 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t *
Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 ); Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 );
// collect the internal node // collect the internal node
if ( vCone ) Vec_PtrPush( vCone, pNode ); if ( vCone ) Vec_PtrPush( vCone, pNode );
// printf( "%d ", pNode->Id );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -300,6 +301,7 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu ...@@ -300,6 +301,7 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu
if ( vSupp ) Vec_PtrClear( vSupp ); if ( vSupp ) Vec_PtrClear( vSupp );
Abc_NtkIncrementTravId( pNode->pNtk ); Abc_NtkIncrementTravId( pNode->pNtk );
Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 ); Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
// printf( "\n" );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -389,6 +391,60 @@ Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ) ...@@ -389,6 +391,60 @@ Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode )
return vInside; return vInside;
} }
/**Function*************************************************************
Synopsis [Collects the internal and boundary nodes in the derefed MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NodeMffcLabel_rec( Abc_Obj_t * pNode, int fTopmost )
{
Abc_Obj_t * pFanin;
int i;
// add to the new support nodes
if ( !fTopmost && (Abc_ObjIsCi(pNode) || pNode->vFanouts.nSize > 0) )
return;
// skip visited nodes
if ( Abc_NodeIsTravIdCurrent(pNode) )
return;
Abc_NodeSetTravIdCurrent(pNode);
// recur on the children
Abc_ObjForEachFanin( pNode, pFanin, i )
Abc_NodeMffcLabel_rec( pFanin, 0 );
// collect the internal node
// printf( "%d ", pNode->Id );
}
/**Function*************************************************************
Synopsis [Collects the internal nodes of the MFFC limited by cut.]
Description []
SideEffects [Increments the trav ID and marks visited nodes.]
SeeAlso []
***********************************************************************/
int Abc_NodeMffcLabel( Abc_Obj_t * pNode )
{
int Count1, Count2;
// dereference the node
Count1 = Abc_NodeDeref_rec( pNode );
// collect the nodes inside the MFFC
Abc_NtkIncrementTravId( pNode->pNtk );
Abc_NodeMffcLabel_rec( pNode, 1 );
// reference it back
Count2 = Abc_NodeRef_rec( pNode );
assert( Count1 == Count2 );
return Count1;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
...@@ -63,7 +63,7 @@ static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -63,7 +63,7 @@ static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutjam ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -218,7 +218,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -218,7 +218,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "lutjam", Abc_CommandLutjam, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "lutpack", Abc_CommandLutpack, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
...@@ -328,6 +328,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -328,6 +328,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Abc_NtkPrint256(); // Abc_NtkPrint256();
// Kit_TruthCountMintermsPrecomp(); // Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1536,7 +1537,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -1536,7 +1537,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
// convert it to truth table // convert it to truth table
{ {
Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) ); Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
Vec_Int_t * vMemory = Vec_IntAlloc( 100 ); Vec_Int_t * vMemory = Vec_IntAlloc( 10000 );
unsigned * pTruth; unsigned * pTruth;
if ( !Abc_ObjIsNode(pObj) ) if ( !Abc_ObjIsNode(pObj) )
{ {
...@@ -1548,7 +1549,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -1548,7 +1549,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Currently works only for up to 8 inputs.\n" ); fprintf( pErr, "Currently works only for up to 8 inputs.\n" );
return 1; return 1;
} }
pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 1 ); pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
if ( Hop_IsComplement(pObj->pData) ) if ( Hop_IsComplement(pObj->pData) )
Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) ); Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
...@@ -2889,7 +2890,7 @@ usage: ...@@ -2889,7 +2890,7 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
...@@ -2907,7 +2908,7 @@ int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2907,7 +2908,7 @@ int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
memset( pPars, 0, sizeof(Lut_Par_t) ); memset( pPars, 0, sizeof(Lut_Par_t) );
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 = 1; // (Q) the maximum number of LUTs not in the MFFC pPars->nLutsOver = 2; // (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->fVerbose = 0; pPars->fVerbose = 0;
pPars->fVeryVerbose = 0; pPars->fVeryVerbose = 0;
...@@ -2982,7 +2983,7 @@ int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2982,7 +2983,7 @@ int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: lutjam [-N <num>] [-Q <num>] [-S <num>] [-vwh]\n" ); fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-vwh]\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 );
......
src/base/abci/abcDsdRes.c
...@@ -41,6 +41,7 @@ struct Lut_Cut_t_ ...@@ -41,6 +41,7 @@ struct Lut_Cut_t_
unsigned fMark : 1; // multipurpose mark unsigned fMark : 1; // multipurpose mark
// unsigned uSign[2]; // the signature // unsigned uSign[2]; // the signature
float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better) float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better)
int Gain; // the gain achieved using this cut
int pLeaves[LUT_SIZE_MAX]; // the leaves of the cut int pLeaves[LUT_SIZE_MAX]; // the leaves of the cut
int pNodes[LUT_SIZE_MAX]; // the nodes of the cut int pNodes[LUT_SIZE_MAX]; // the nodes of the cut
}; };
...@@ -53,25 +54,35 @@ struct Lut_Man_t_ ...@@ -53,25 +54,35 @@ struct Lut_Man_t_
Abc_Ntk_t * pNtk; // the network Abc_Ntk_t * pNtk; // the network
Abc_Obj_t * pObj; // the node to resynthesize Abc_Obj_t * pObj; // the node to resynthesize
// cut representation // cut representation
int nMffc; // the size of MFFC of the node
int nCuts; // the total number of cuts int nCuts; // the total number of cuts
int nCutsMax; // the largest possible number of cuts int nCutsMax; // the largest possible number of cuts
int nEvals; // the number of good cuts int nEvals; // the number of good cuts
Lut_Cut_t pCuts[LUT_CUTS_MAX]; // the storage for cuts Lut_Cut_t pCuts[LUT_CUTS_MAX]; // the storage for cuts
int pEvals[LUT_SIZE_MAX]; // the good cuts int pEvals[LUT_CUTS_MAX]; // the good cuts
// temporary variables // temporary variables
int pRefs[LUT_SIZE_MAX]; // fanin reference counters int pRefs[LUT_SIZE_MAX]; // fanin reference counters
int pCands[LUT_SIZE_MAX]; // internal nodes pointing only to the leaves int pCands[LUT_SIZE_MAX]; // internal nodes pointing only to the leaves
// truth table representation // truth table representation
Vec_Ptr_t * vTtElems; // elementary truth tables Vec_Ptr_t * vTtElems; // elementary truth tables
Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
// statistics
int nCutsTotal;
int nGainTotal;
// rutime
int timeCuts;
int timeTruth;
int timeEval;
int timeOther;
int timeTotal;
}; };
static int Abc_LutResynthesizeNode( Lut_Man_t * p );
#define Abc_LutCutForEachLeaf( pNtk, pCut, pObj, i ) \ #define Abc_LutCutForEachLeaf( pNtk, pCut, pObj, i ) \
for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ ) for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
#define Abc_LutCutForEachNode( pNtk, pCut, pObj, i ) \ #define Abc_LutCutForEachNode( pNtk, pCut, pObj, i ) \
for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ ) for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
#define Abc_LutCutForEachNodeReverse( pNtk, pCut, pObj, i ) \
for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -93,14 +104,15 @@ Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars ) ...@@ -93,14 +104,15 @@ Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars )
Lut_Man_t * p; Lut_Man_t * p;
int i; int i;
assert( pPars->nLutsMax <= 16 ); assert( pPars->nLutsMax <= 16 );
assert( pPars->nVarsMax > 0 );
p = ALLOC( Lut_Man_t, 1 ); p = ALLOC( Lut_Man_t, 1 );
memset( p, 0, sizeof(Lut_Man_t) ); memset( p, 0, sizeof(Lut_Man_t) );
p->pPars = pPars; p->pPars = pPars;
p->nCutsMax = LUT_CUTS_MAX; p->nCutsMax = LUT_CUTS_MAX;
for ( i = 0; i < p->nCuts; i++ ) for ( i = 0; i < p->nCuts; i++ )
p->pCuts[i].nLeavesMax = p->pCuts[i].nNodesMax = LUT_SIZE_MAX; p->pCuts[i].nLeavesMax = p->pCuts[i].nNodesMax = LUT_SIZE_MAX;
p->vTtElems = Vec_PtrAllocTruthTables( pPars->nLutsMax ); p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nLutsMax) ); p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
return p; return p;
} }
...@@ -124,51 +136,6 @@ void Abc_LutManStop( Lut_Man_t * p ) ...@@ -124,51 +136,6 @@ void Abc_LutManStop( Lut_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs resynthesis for one network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
{
Lut_Man_t * p;
Abc_Obj_t * pObj;
int i;
assert( Abc_NtkIsLogic(pNtk) );
// convert logic to AIGs
Abc_NtkToAig( pNtk );
// compute the levels
Abc_NtkLevel( pNtk );
// start the manager
p = Abc_LutManStart( pPars );
p->pNtk = pNtk;
// get the number of inputs
p->pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
p->pPars->nVarsMax = p->pPars->nLutsMax * (p->pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
p->pPars->nLutsMax, p->pPars->nLutSize, p->pPars->nLutsOver, p->pPars->nVarsShared, p->pPars->nVarsMax );
// consider all nodes
Abc_NtkForEachNode( pNtk, pObj, i )
{
p->pObj = pObj;
Abc_LutResynthesizeNode( p );
}
Abc_LutManStop( p );
// check the resulting network
if ( !Abc_NtkCheck( pNtk ) )
{
printf( "Abc_LutResynthesize: The network check has failed.\n" );
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if the cut has structural DSD.] Synopsis [Returns 1 if the cut has structural DSD.]
Description [] Description []
...@@ -216,7 +183,7 @@ int Abc_LutNodeCutsCheckDsd( Lut_Man_t * p, Lut_Cut_t * pCut ) ...@@ -216,7 +183,7 @@ int Abc_LutNodeCutsCheckDsd( Lut_Man_t * p, Lut_Cut_t * pCut )
if ( p->pRefs[(int)pFanin->pCopy] > 1 ) if ( p->pRefs[(int)pFanin->pCopy] > 1 )
break; break;
} }
if ( k == Abc_ObjFaninNum(pFanin) ) if ( k == Abc_ObjFaninNum(pObj) )
{ {
RetValue = 1; RetValue = 1;
break; break;
...@@ -316,6 +283,36 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew ...@@ -316,6 +283,36 @@ int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prints the given cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_LutNodePrintCut( Lut_Man_t * p, Lut_Cut_t * pCut )
{
Abc_Obj_t * pObj;
int i;
printf( "LEAVES:\n" );
Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
{
Abc_ObjPrint( stdout, pObj );
}
printf( "NODES:\n" );
Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i )
{
Abc_ObjPrint( stdout, pObj );
assert( Abc_ObjIsNode(pObj) );
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Computes the set of all cuts.] Synopsis [Computes the set of all cuts.]
Description [] Description []
...@@ -335,8 +332,14 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node ) ...@@ -335,8 +332,14 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
if ( pCut->nNodes == LUT_SIZE_MAX ) if ( pCut->nNodes == LUT_SIZE_MAX )
return; return;
// if the node is not in the MFFC, check the limit // if the node is a PI, quit
pObj = Abc_NtkObj( p->pNtk, Node ); pObj = Abc_NtkObj( p->pNtk, Node );
if ( Abc_ObjIsCi(pObj) )
return;
assert( Abc_ObjIsNode(pObj) );
assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
// if the node is not in the MFFC, check the limit
if ( !Abc_NodeIsTravIdCurrent(pObj) ) if ( !Abc_NodeIsTravIdCurrent(pObj) )
{ {
if ( (int)pCut->nNodesMarked == p->pPars->nLutsOver ) if ( (int)pCut->nNodesMarked == p->pPars->nLutsOver )
...@@ -344,8 +347,17 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node ) ...@@ -344,8 +347,17 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
assert( (int)pCut->nNodesMarked < p->pPars->nLutsOver ); assert( (int)pCut->nNodesMarked < p->pPars->nLutsOver );
} }
// create the new set of leaves // initialize the set of leaves to the nodes in the cut
assert( p->nCuts < LUT_CUTS_MAX );
pCutNew = p->pCuts + p->nCuts; pCutNew = p->pCuts + p->nCuts;
/*
if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
{
int x = 0;
printf( "Start:\n" );
Abc_LutNodePrintCut( p, pCut );
}
*/
pCutNew->nLeaves = 0; pCutNew->nLeaves = 0;
for ( i = 0; i < (int)pCut->nLeaves; i++ ) for ( i = 0; i < (int)pCut->nLeaves; i++ )
if ( pCut->pLeaves[i] != Node ) if ( pCut->pLeaves[i] != Node )
...@@ -358,7 +370,7 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node ) ...@@ -358,7 +370,7 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
if ( pCutNew->pLeaves[k] >= pFanin->Id ) if ( pCutNew->pLeaves[k] >= pFanin->Id )
break; break;
if ( pCutNew->pLeaves[k] == pFanin->Id ) if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
continue; continue;
// check if there is room // check if there is room
if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax ) if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
...@@ -371,22 +383,34 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node ) ...@@ -371,22 +383,34 @@ void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
assert( pCutNew->nLeaves <= LUT_SIZE_MAX ); assert( pCutNew->nLeaves <= LUT_SIZE_MAX );
} }
for ( k = 0; k < (int)pCutNew->nLeaves - 1; k++ )
assert( pCutNew->pLeaves[k] < pCutNew->pLeaves[k+1] );
// skip the contained cuts // skip the contained cuts
if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) ) if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
return; return;
// update the set of internal nodes // update the set of internal nodes
assert( pCut->nNodes < LUT_SIZE_MAX ); assert( pCut->nNodes < LUT_SIZE_MAX );
memcpy( pCutNew->pNodes, pCutNew->pNodes, pCut->nNodes * sizeof(int) ); memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
pCutNew->pNodes[ pCut->nNodes++ ] = Node; pCutNew->nNodes = pCut->nNodes;
pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
// add the marked node // add the marked node
pCutNew->nNodesMarked = pCut->nNodesMarked + !Abc_NodeIsTravIdCurrent(pObj); pCutNew->nNodesMarked = pCut->nNodesMarked + !Abc_NodeIsTravIdCurrent(pObj);
/*
if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
{
int x = 0;
printf( "Finish:\n" );
Abc_LutNodePrintCut( p, pCutNew );
}
*/
// add the cut to storage // add the cut to storage
assert( p->nCuts < LUT_CUTS_MAX ); assert( p->nCuts < LUT_CUTS_MAX );
p->nCuts++; p->nCuts++;
assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesMarked );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -407,13 +431,13 @@ int Abc_LutNodeCuts( Lut_Man_t * p ) ...@@ -407,13 +431,13 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
int i, k, Temp, nMffc, fChanges; int i, k, Temp, nMffc, fChanges;
// mark the MFFC of the node with the current trav ID // mark the MFFC of the node with the current trav ID
nMffc = Abc_NodeMffcLabel( p->pObj ); nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
assert( nMffc > 0 ); assert( nMffc > 0 );
if ( nMffc == 1 ) if ( nMffc == 1 )
return 0; return 0;
// initialize the first cut // initialize the first cut
pCut = p->pCuts; pCut = p->pCuts; p->nCuts = 1;
// assign internal nodes // assign internal nodes
pCut->nNodes = 1; pCut->nNodes = 1;
pCut->pNodes[0] = p->pObj->Id; pCut->pNodes[0] = p->pObj->Id;
...@@ -439,10 +463,10 @@ int Abc_LutNodeCuts( Lut_Man_t * p ) ...@@ -439,10 +463,10 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
// perform the cut computation // perform the cut computation
for ( i = 0; i < p->nCuts; i++ ) for ( i = 0; i < p->nCuts; i++ )
{ {
pCut = p->pCuts + p->pEvals[i]; pCut = p->pCuts + i;
if ( pCut->nLeaves == 0 ) if ( pCut->nLeaves == 0 )
continue; continue;
// try to expand each fanin of each cut // try to expand the fanins of this cut
for ( k = 0; k < (int)pCut->nLeaves; k++ ) for ( k = 0; k < (int)pCut->nLeaves; k++ )
{ {
Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] ); Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] );
...@@ -457,10 +481,14 @@ int Abc_LutNodeCuts( Lut_Man_t * p ) ...@@ -457,10 +481,14 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
p->nEvals = 0; p->nEvals = 0;
for ( i = 0; i < p->nCuts; i++ ) for ( i = 0; i < p->nCuts; i++ )
{ {
pCut = p->pCuts + p->pEvals[i]; pCut = p->pCuts + i;
if ( pCut->nLeaves == 0 )
continue;
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesMarked) / p->pPars->nLutsMax; pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesMarked) / p->pPars->nLutsMax;
if ( pCut->Weight <= 1.0 )
continue;
pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut ); pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut );
if ( pCut->nLeaves == 0 || pCut->Weight <= 1.0 || pCut->fHasDsd ) if ( pCut->fHasDsd )
continue; continue;
p->pEvals[p->nEvals++] = i; p->pEvals[p->nEvals++] = i;
} }
...@@ -496,9 +524,77 @@ int Abc_LutNodeCuts( Lut_Man_t * p ) ...@@ -496,9 +524,77 @@ int Abc_LutNodeCuts( Lut_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
unsigned * Abc_LutCutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
{
unsigned * pTruth, * pTruth0, * pTruth1;
assert( !Hop_IsComplement(pObj) );
if ( pObj->pData )
{
assert( ((unsigned)pObj->pData) & 0xffff0000 );
return pObj->pData;
}
// get the plan for a new truth table
pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
if ( Hop_ObjIsConst1(pObj) )
Extra_TruthFill( pTruth, nVars );
else
{
assert( Hop_ObjIsAnd(pObj) );
// compute the truth tables of the fanins
pTruth0 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
pTruth1 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
// creat the truth table of the node
Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
}
pObj->pData = pTruth;
return pTruth;
}
/**Function*************************************************************
Synopsis [Computes the truth able of one cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut ) unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut )
{ {
unsigned * pTruth = NULL; Hop_Man_t * pManHop = p->pNtk->pManFunc;
Hop_Obj_t * pObjHop;
Abc_Obj_t * pObj, * pFanin;
unsigned * pTruth;
int i, k, iCount = 0;
// Abc_LutNodePrintCut( p, pCut );
// initialize the leaves
Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
// construct truth table in the topological order
Abc_LutCutForEachNodeReverse( p->pNtk, pCut, pObj, i )
{
// get the local AIG
pObjHop = Hop_Regular(pObj->pData);
// clean the data field of the nodes in the AIG subgraph
Hop_ObjCleanData_rec( pObjHop );
// set the initial truth tables at the fanins
Abc_ObjForEachFanin( pObj, pFanin, k )
{
assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
}
// compute the truth table of internal nodes
pTruth = Abc_LutCutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
if ( Hop_IsComplement(pObj->pData) )
Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
// set the truth table at the node
pObj->pCopy = (Abc_Obj_t *)pTruth;
}
return pTruth; return pTruth;
} }
...@@ -531,28 +627,121 @@ int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, void * pDsd ) ...@@ -531,28 +627,121 @@ int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, void * pDsd )
***********************************************************************/ ***********************************************************************/
int Abc_LutResynthesizeNode( Lut_Man_t * p ) int Abc_LutResynthesizeNode( Lut_Man_t * p )
{ {
extern void Kit_DsdTest( unsigned * pTruth, int nVars );
extern int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize );
Lut_Cut_t * pCut; Lut_Cut_t * pCut;
unsigned * pTruth; unsigned * pTruth;
void * pDsd; void * pDsd = NULL;
int i; int i, Result, GainBest, Gain;
int clk;
// compute the cuts // compute the cuts
clk = clock();
if ( !Abc_LutNodeCuts( p ) ) if ( !Abc_LutNodeCuts( p ) )
{
p->timeCuts += clock() - clk;
return 0; return 0;
}
p->timeCuts += clock() - clk;
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
// try the good cuts // try the good cuts
p->nCutsTotal += p->nEvals;
GainBest = 0;
for ( i = 0; i < p->nEvals; i++ ) for ( i = 0; i < p->nEvals; i++ )
{ {
// get the cut // get the cut
pCut = p->pCuts + p->pEvals[i]; pCut = p->pCuts + p->pEvals[i];
// compute the truth table // compute the truth table
clk = clock();
pTruth = Abc_LutCutTruth( p, pCut ); pTruth = Abc_LutCutTruth( p, pCut );
// check decomposition p->timeTruth += clock() - clk;
pDsd = /***/ NULL; // evaluate the result of decomposition
clk = clock();
// Kit_DsdTest( pTruth, pCut->nLeaves );
Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
p->timeEval += clock() - clk;
// calculate the gain
Gain = Result < 0 ? 0 : pCut->nNodes - pCut->nNodesMarked - Result;
if ( GainBest < Gain )
GainBest = Gain;
if ( p->pPars->fVeryVerbose )
{
printf( " Cut %2d : Lvs = %2d. Supp = %2d. Vol = %2d. Q = %d. Weight = %4.2f. New = %2d. Gain = %2d.\n",
i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesMarked, pCut->Weight, Result, Gain );
// for ( k = 0; k < pCut->nNodes; k++ )
// printf( "%d(%d) ", pCut->pNodes[k], Abc_NodeIsTravIdCurrent( Abc_NtkObj(p->pNtk, pCut->pNodes[k]) ) );
// printf( "\n" );
}
// pTruth = NULL;
//Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );
// if it is not DSD decomposable, return // if it is not DSD decomposable, return
if ( pDsd == NULL ) if ( pDsd == NULL )
continue; continue;
// update the network // update the network
Abc_LutCutUpdate( p, pCut, pDsd ); Abc_LutCutUpdate( p, pCut, pDsd );
} }
p->nGainTotal += GainBest;
return 1;
}
/**Function*************************************************************
Synopsis [Performs resynthesis for one network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
{
Lut_Man_t * p;
Abc_Obj_t * pObj;
int i, clk = clock();
assert( Abc_NtkIsLogic(pNtk) );
// convert logic to AIGs
Abc_NtkToAig( pNtk );
// compute the levels
Abc_NtkLevel( pNtk );
// get the number of inputs
pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
// start the manager
p = Abc_LutManStart( pPars );
p->pNtk = pNtk;
// consider all nodes
Abc_NtkForEachNode( pNtk, pObj, i )
{
p->pObj = pObj;
Abc_LutResynthesizeNode( p );
}
printf( "Total nodes = %5d. Total cuts = %5d. Total gain = %5d. (%5.2f %%)\n",
Abc_NtkNodeNum(pNtk), p->nCutsTotal, p->nGainTotal, 100.0 * p->nGainTotal / Abc_NtkNodeNum(pNtk) );
p->timeTotal = clock() - clk;
p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval;
PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Truth ", p->timeTruth, p->timeTotal );
PRTP( "Eval ", p->timeEval, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
Abc_LutManStop( p );
// check the resulting network
if ( !Abc_NtkCheck( pNtk ) )
{
printf( "Abc_LutResynthesize: The network check has failed.\n" );
return 0;
}
return 1; return 1;
} }
......
src/base/abci/abcReconv.c
...@@ -712,7 +712,7 @@ Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Pt ...@@ -712,7 +712,7 @@ Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Pt
// mark MFFC // mark MFFC
if ( pRoot ) if ( pRoot )
Abc_NodeMffcLabel( pRoot ); Abc_NodeMffcLabelAig( pRoot );
// go through the levels up // go through the levels up
Vec_PtrClear( p->vNodesTfo ); Vec_PtrClear( p->vNodesTfo );
......
src/base/abci/abcRefactor.c
...@@ -248,7 +248,7 @@ p->timeFact += clock() - clk; ...@@ -248,7 +248,7 @@ p->timeFact += clock() - clk;
pFanin->vFanouts.nSize++; pFanin->vFanouts.nSize++;
// label MFFC with current traversal ID // label MFFC with current traversal ID
Abc_NtkIncrementTravId( pNode->pNtk ); Abc_NtkIncrementTravId( pNode->pNtk );
nNodesSaved = Abc_NodeMffcLabel( pNode ); nNodesSaved = Abc_NodeMffcLabelAig( pNode );
// unmark the fanin boundary and set the fanins as leaves in the form // unmark the fanin boundary and set the fanins as leaves in the form
Vec_PtrForEachEntry( vFanins, pFanin, i ) Vec_PtrForEachEntry( vFanins, pFanin, i )
{ {
......
src/base/abci/abcRestruct.c
...@@ -391,7 +391,7 @@ p->timeDsd += clock() - clk; ...@@ -391,7 +391,7 @@ p->timeDsd += clock() - clk;
pLeaf->vFanouts.nSize++; pLeaf->vFanouts.nSize++;
// label MFFC with current traversal ID // label MFFC with current traversal ID
Abc_NtkIncrementTravId( pRoot->pNtk ); Abc_NtkIncrementTravId( pRoot->pNtk );
nNodesSaved = Abc_NodeMffcLabel( pRoot ); nNodesSaved = Abc_NodeMffcLabelAig( pRoot );
// unmark the fanin boundary and set the fanins as leaves in the form // unmark the fanin boundary and set the fanins as leaves in the form
Vec_PtrForEachEntry( p->vLeaves, pLeaf, i ) Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
pLeaf->vFanouts.nSize--; pLeaf->vFanouts.nSize--;
......
src/base/ver/verCore.c
...@@ -1203,6 +1203,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) ...@@ -1203,6 +1203,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
Vec_PtrPush( pMan->vNames, pEquation ); Vec_PtrPush( pMan->vNames, pEquation );
// get the buffer // get the buffer
pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen()); pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
if ( pFunc == NULL )
{
sprintf( pMan->sError, "Reading assign statement for node %s has failed because the genlib library has no buffer.", Abc_ObjName(pNet) );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
} }
} }
else else
...@@ -1391,6 +1397,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) ...@@ -1391,6 +1397,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
Ver_ParsePrintErrorMessage( pMan ); Ver_ParsePrintErrorMessage( pMan );
return 0; return 0;
} }
Ver_ParseSkipComments( pMan );
// start the node // start the node
pNode = Abc_NtkCreateNode( pNtk ); pNode = Abc_NtkCreateNode( pNtk );
......
src/misc/extra/extra.h
...@@ -530,6 +530,30 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * ...@@ -530,6 +530,30 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned *
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- ) for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(pIn0[w] & pIn1[w]); pOut[w] = ~(pIn0[w] & pIn1[w]);
} }
static inline void Extra_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
{
int w;
if ( fCompl0 && fCompl1 )
{
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(pIn0[w] | pIn1[w]);
}
else if ( fCompl0 && !fCompl1 )
{
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~pIn0[w] & pIn1[w];
}
else if ( !fCompl0 && fCompl1 )
{
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] & ~pIn1[w];
}
else // if ( !fCompl0 && !fCompl1 )
{
for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] & pIn1[w];
}
}
extern unsigned ** Extra_TruthElementary( int nVars ); extern unsigned ** Extra_TruthElementary( int nVars );
extern void Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start ); extern void Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
......
src/opt/kit/kitDsd.c
...@@ -24,9 +24,9 @@ ...@@ -24,9 +24,9 @@
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Dsd_Man_t_ Dsd_Man_t; typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
typedef struct Dsd_Ntk_t_ Dsd_Ntk_t; typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
typedef struct Dsd_Obj_t_ Dsd_Obj_t; typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
// DSD node types // DSD node types
typedef enum { typedef enum {
...@@ -39,7 +39,7 @@ typedef enum { ...@@ -39,7 +39,7 @@ typedef enum {
} Kit_Dsd_t; } Kit_Dsd_t;
// DSD manager // DSD manager
struct Dsd_Man_t_ struct Kit_DsdMan_t_
{ {
int nVars; // the maximum number of variables int nVars; // the maximum number of variables
int nWords; // the number of words in TTs int nWords; // the number of words in TTs
...@@ -48,18 +48,18 @@ struct Dsd_Man_t_ ...@@ -48,18 +48,18 @@ struct Dsd_Man_t_
}; };
// DSD network // DSD network
struct Dsd_Ntk_t_ struct Kit_DsdNtk_t_
{ {
unsigned char nVars; // at most 16 (perhaps 18?) unsigned char nVars; // at most 16 (perhaps 18?)
unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars) unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars)
unsigned char nNodes; // the number of nodes unsigned char nNodes; // the number of nodes
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?)
Dsd_Obj_t * pNodes[0]; // the nodes Kit_DsdObj_t * pNodes[0]; // the nodes
}; };
// DSD node // DSD node
struct Dsd_Obj_t_ struct Kit_DsdObj_t_
{ {
unsigned Id : 6; // the number of this node unsigned Id : 6; // the number of this node
unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
...@@ -70,27 +70,27 @@ struct Dsd_Obj_t_ ...@@ -70,27 +70,27 @@ struct Dsd_Obj_t_
unsigned char pFans[0]; // the fanin literals unsigned char pFans[0]; // the fanin literals
}; };
static inline int Dsd_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Dsd_Lit2Var( int Lit ) { return Lit >> 1; } static inline int Kit_DsdLit2Var( int Lit ) { return Lit >> 1; }
static inline int Dsd_LitIsCompl( int Lit ) { return Lit & 1; } static inline int Kit_DsdLitIsCompl( int Lit ) { return Lit & 1; }
static inline int Dsd_LitNot( int Lit ) { return Lit ^ 1; } static inline int Kit_DsdLitNot( int Lit ) { return Lit ^ 1; }
static inline int Dsd_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } static inline int Kit_DsdLitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Dsd_LitRegular( int Lit ) { return Lit & 0xfe; } static inline int Kit_DsdLitRegular( int Lit ) { return Lit & 0xfe; }
static inline unsigned Dsd_ObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); } static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
static inline unsigned * Dsd_ObjTruth( Dsd_Obj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; } static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
static inline Dsd_Obj_t * Dsd_NtkObj( Dsd_Ntk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; } static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
static inline Dsd_Obj_t * Dsd_NtkRoot( Dsd_Ntk_t * pNtk ) { return Dsd_NtkObj( pNtk, Dsd_Lit2Var(pNtk->Root) ); } static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
#define Dsd_NtkForEachObj( pNtk, pObj, i ) \ #define Kit_DsdNtkForEachObj( pNtk, pObj, i ) \
for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ ) for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
#define Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) \ #define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) \
for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ ) for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
extern unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk ); extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk ); extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ); extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk ); extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -107,11 +107,11 @@ extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk ); ...@@ -107,11 +107,11 @@ extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk );
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Dsd_Man_t * Dsd_ManAlloc( int nVars ) Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
{ {
Dsd_Man_t * p; Kit_DsdMan_t * p;
p = ALLOC( Dsd_Man_t, 1 ); p = ALLOC( Kit_DsdMan_t, 1 );
memset( p, 0, sizeof(Dsd_Man_t) ); memset( p, 0, sizeof(Kit_DsdMan_t) );
p->nVars = nVars; p->nVars = nVars;
p->nWords = Kit_TruthWordNum( p->nVars ); p->nWords = Kit_TruthWordNum( p->nVars );
p->vTtElems = Vec_PtrAllocTruthTables( p->nVars ); p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
...@@ -130,7 +130,7 @@ Dsd_Man_t * Dsd_ManAlloc( int nVars ) ...@@ -130,7 +130,7 @@ Dsd_Man_t * Dsd_ManAlloc( int nVars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Dsd_ManFree( Dsd_Man_t * p ) void Kit_DsdManFree( Kit_DsdMan_t * p )
{ {
Vec_PtrFree( p->vTtElems ); Vec_PtrFree( p->vTtElems );
Vec_PtrFree( p->vTtNodes ); Vec_PtrFree( p->vTtNodes );
...@@ -148,16 +148,16 @@ void Dsd_ManFree( Dsd_Man_t * p ) ...@@ -148,16 +148,16 @@ void Dsd_ManFree( Dsd_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans ) Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
{ {
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
int nSize = sizeof(Dsd_Obj_t) + sizeof(unsigned) * (Dsd_ObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans)); int nSize = sizeof(Kit_DsdObj_t) + sizeof(unsigned) * (Kit_DsdObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
pObj = (Dsd_Obj_t *)ALLOC( char, nSize ); pObj = (Kit_DsdObj_t *)ALLOC( char, nSize );
memset( pObj, 0, nSize ); memset( pObj, 0, nSize );
pObj->Id = pNtk->nVars + pNtk->nNodes; pObj->Id = pNtk->nVars + pNtk->nNodes;
pObj->Type = Type; pObj->Type = Type;
pObj->nFans = nFans; pObj->nFans = nFans;
pObj->Offset = Dsd_ObjOffset( nFans ); pObj->Offset = Kit_DsdObjOffset( nFans );
// add the object // add the object
assert( pNtk->nNodes < pNtk->nNodesAlloc ); assert( pNtk->nNodes < pNtk->nNodesAlloc );
pNtk->pNodes[pNtk->nNodes++] = pObj; pNtk->pNodes[pNtk->nNodes++] = pObj;
...@@ -175,7 +175,7 @@ Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans ) ...@@ -175,7 +175,7 @@ Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj ) void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
{ {
free( pObj ); free( pObj );
} }
...@@ -191,12 +191,12 @@ void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj ) ...@@ -191,12 +191,12 @@ void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Dsd_Ntk_t * Kit_DsdNtkAlloc( int nVars ) Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
{ {
Dsd_Ntk_t * pNtk; Kit_DsdNtk_t * pNtk;
int nSize = sizeof(Dsd_Ntk_t) + sizeof(void *) * nVars; int nSize = sizeof(Kit_DsdNtk_t) + sizeof(void *) * nVars;
// allocate the network // allocate the network
pNtk = (Dsd_Ntk_t *)ALLOC( char, nSize ); pNtk = (Kit_DsdNtk_t *)ALLOC( char, nSize );
memset( pNtk, 0, nSize ); memset( pNtk, 0, nSize );
pNtk->nVars = nVars; pNtk->nVars = nVars;
pNtk->nNodesAlloc = nVars; pNtk->nNodesAlloc = nVars;
...@@ -215,11 +215,11 @@ Dsd_Ntk_t * Kit_DsdNtkAlloc( int nVars ) ...@@ -215,11 +215,11 @@ Dsd_Ntk_t * Kit_DsdNtkAlloc( int nVars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk ) void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
{ {
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
unsigned i; unsigned i;
Dsd_NtkForEachObj( pNtk, pObj, i ) Kit_DsdNtkForEachObj( pNtk, pObj, i )
free( pObj ); free( pObj );
free( pNtk->pMem ); free( pNtk->pMem );
free( pNtk ); free( pNtk );
...@@ -261,13 +261,13 @@ void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans ) ...@@ -261,13 +261,13 @@ void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id ) void Kit_DsdPrint_rec( FILE * pFile, Kit_DsdNtk_t * pNtk, int Id )
{ {
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
unsigned iLit, i; unsigned iLit, i;
char Symbol; char Symbol;
pObj = Dsd_NtkObj( pNtk, Id ); pObj = Kit_DsdNtkObj( pNtk, Id );
if ( pObj == NULL ) if ( pObj == NULL )
{ {
assert( Id < pNtk->nVars ); assert( Id < pNtk->nVars );
...@@ -293,14 +293,14 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id ) ...@@ -293,14 +293,14 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id )
Symbol = ','; Symbol = ',';
if ( pObj->Type == KIT_DSD_PRIME ) if ( pObj->Type == KIT_DSD_PRIME )
Kit_DsdPrintHex( stdout, Dsd_ObjTruth(pObj), pObj->nFans ); Kit_DsdPrintHex( stdout, Kit_DsdObjTruth(pObj), pObj->nFans );
fprintf( pFile, "(" ); fprintf( pFile, "(" );
Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{ {
if ( Dsd_LitIsCompl(iLit) ) if ( Kit_DsdLitIsCompl(iLit) )
fprintf( pFile, "!" ); fprintf( pFile, "!" );
Kit_DsdPrint_rec( pFile, pNtk, Dsd_Lit2Var(iLit) ); Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(iLit) );
if ( i < pObj->nFans - 1 ) if ( i < pObj->nFans - 1 )
fprintf( pFile, "%c", Symbol ); fprintf( pFile, "%c", Symbol );
} }
...@@ -318,12 +318,12 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id ) ...@@ -318,12 +318,12 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk ) void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
{ {
fprintf( pFile, "F = " ); fprintf( pFile, "F = " );
if ( Dsd_LitIsCompl(pNtk->Root) ) if ( Kit_DsdLitIsCompl(pNtk->Root) )
fprintf( pFile, "!" ); fprintf( pFile, "!" );
Kit_DsdPrint_rec( pFile, pNtk, Dsd_Lit2Var(pNtk->Root) ); Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) );
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
} }
...@@ -338,14 +338,14 @@ void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk ) ...@@ -338,14 +338,14 @@ void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id ) unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
{ {
Dsd_Obj_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;
// get the node with this ID // get the node with this ID
pObj = Dsd_NtkObj( pNtk, Id ); pObj = Kit_DsdNtkObj( pNtk, Id );
pTruthRes = Vec_PtrEntry( p->vTtNodes, Id ); pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
// special case: literal of an internal node // special case: literal of an internal node
...@@ -368,8 +368,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id ...@@ -368,8 +368,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
{ {
assert( pObj->nFans == 1 ); assert( pObj->nFans == 1 );
iLit = pObj->pFans[0]; iLit = pObj->pFans[0];
pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Dsd_Lit2Var(iLit) ); pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
if ( Dsd_LitIsCompl(iLit) ) if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars ); Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
else else
Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars ); Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars );
...@@ -377,26 +377,26 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id ...@@ -377,26 +377,26 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
} }
// collect the truth tables of the fanins // collect the truth tables of the fanins
Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Dsd_Lit2Var(iLit) ); pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
// create the truth table // create the truth table
// simple gates // simple gates
if ( pObj->Type == KIT_DSD_AND ) if ( pObj->Type == KIT_DSD_AND )
{ {
Kit_TruthFill( pTruthRes, pNtk->nVars ); Kit_TruthFill( pTruthRes, pNtk->nVars );
Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Dsd_LitIsCompl(iLit) ); 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 )
{ {
Kit_TruthClear( pTruthRes, pNtk->nVars ); Kit_TruthClear( pTruthRes, pNtk->nVars );
fCompl = 0; fCompl = 0;
Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{ {
Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
fCompl ^= Dsd_LitIsCompl(iLit); fCompl ^= Kit_DsdLitIsCompl(iLit);
} }
if ( fCompl ) if ( fCompl )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
...@@ -405,7 +405,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id ...@@ -405,7 +405,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
assert( pObj->Type == KIT_DSD_PRIME ); assert( pObj->Type == KIT_DSD_PRIME );
// get the truth table of the prime node // get the truth table of the prime node
pTruthPrime = Dsd_ObjTruth( pObj ); pTruthPrime = Kit_DsdObjTruth( pObj );
// get storage for the temporary minterm // get storage for the temporary minterm
pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes); pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
...@@ -417,8 +417,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id ...@@ -417,8 +417,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
if ( !Kit_TruthHasBit(pTruthPrime, m) ) if ( !Kit_TruthHasBit(pTruthPrime, m) )
continue; continue;
Kit_TruthFill( pTruthMint, pNtk->nVars ); Kit_TruthFill( pTruthMint, pNtk->nVars );
Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, Dsd_LitIsCompl(iLit) ); Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars ); Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
} }
return pTruthRes; return pTruthRes;
...@@ -435,7 +435,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id ...@@ -435,7 +435,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk ) unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
{ {
unsigned * pTruthRes; unsigned * pTruthRes;
int i; int i;
...@@ -444,13 +444,81 @@ unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk ) ...@@ -444,13 +444,81 @@ unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk )
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, Dsd_Lit2Var(pNtk->Root) ); pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
// complement the truth table if needed // complement the truth table if needed
if ( Dsd_LitIsCompl(pNtk->Root) ) if ( Kit_DsdLitIsCompl(pNtk->Root) )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
return pTruthRes; return pTruthRes;
} }
/**Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCounter )
{
Kit_DsdObj_t * pObj;
unsigned iLit, i, Res0, Res1;
pObj = Kit_DsdNtkObj( pNtk, Id );
if ( pObj == NULL )
return 0;
if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
{
assert( pObj->nFans == 2 );
Res0 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pObj->pFans[0]), pCounter );
Res1 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pObj->pFans[1]), pCounter );
if ( Res0 == 0 && Res1 > 0 )
return Res1 - 1;
if ( Res0 > 0 && Res1 == 0 )
return Res0 - 1;
(*pCounter)++;
return nLutSize - 2;
}
assert( pObj->Type == KIT_DSD_PRIME );
if ( (int)pObj->nFans > nLutSize )
{
*pCounter = 1000;
return 0;
}
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(iLit), pCounter );
(*pCounter)++;
return nLutSize - pObj->nFans;
}
/**Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
{
int Counter = 0;
if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_CONST1 )
return 0;
if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_VAR )
return 0;
Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pNtk->Root), &Counter );
if ( Counter >= 1000 )
return -1;
return Counter;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Expands the node.] Synopsis [Expands the node.]
...@@ -462,19 +530,19 @@ unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk ) ...@@ -462,19 +530,19 @@ unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdExpandCollectAnd_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int * nLitsNew ) void Kit_DsdExpandCollectAnd_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
{ {
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
unsigned i, iLitFanin; unsigned i, iLitFanin;
// check the end of the supergate // check the end of the supergate
pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) ); pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( Dsd_LitIsCompl(iLit) || Dsd_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND ) if ( Kit_DsdLitIsCompl(iLit) || Kit_DsdLit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND )
{ {
piLitsNew[(*nLitsNew)++] = iLit; piLitsNew[(*nLitsNew)++] = iLit;
return; return;
} }
// iterate through the fanins // iterate through the fanins
Dsd_ObjForEachFanin( p, pObj, iLitFanin, i ) Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew ); Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew );
} }
...@@ -489,24 +557,24 @@ void Kit_DsdExpandCollectAnd_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int ...@@ -489,24 +557,24 @@ void Kit_DsdExpandCollectAnd_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdExpandCollectXor_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int * nLitsNew ) void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
{ {
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
unsigned i, iLitFanin; unsigned i, iLitFanin;
// check the end of the supergate // check the end of the supergate
pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) ); pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( Dsd_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR ) if ( Kit_DsdLit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR )
{ {
piLitsNew[(*nLitsNew)++] = iLit; piLitsNew[(*nLitsNew)++] = iLit;
return; return;
} }
// iterate through the fanins // iterate through the fanins
pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) ); pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
Dsd_ObjForEachFanin( p, pObj, iLitFanin, i ) Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew ); Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew );
// if the literal was complemented, pass the complemented attribute somewhere // if the literal was complemented, pass the complemented attribute somewhere
if ( Dsd_LitIsCompl(iLit) ) if ( Kit_DsdLitIsCompl(iLit) )
piLitsNew[0] = Dsd_LitNot( piLitsNew[0] ); piLitsNew[0] = Kit_DsdLitNot( piLitsNew[0] );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -520,61 +588,63 @@ void Kit_DsdExpandCollectXor_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int ...@@ -520,61 +588,63 @@ void Kit_DsdExpandCollectXor_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Kit_DsdExpandNode_rec( Dsd_Ntk_t * pNew, Dsd_Ntk_t * p, int iLit ) int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
{ {
unsigned * pTruth, * pTruthNew; unsigned * pTruth, * pTruthNew;
unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0; unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0;
Dsd_Obj_t * pObj, * pObjNew; Kit_DsdObj_t * pObj, * pObjNew;
// remember the complement // remember the complement
fCompl = Dsd_LitIsCompl(iLit); fCompl = Kit_DsdLitIsCompl(iLit);
iLit = Dsd_LitRegular(iLit); iLit = Kit_DsdLitRegular(iLit);
assert( !Dsd_LitIsCompl(iLit) ); assert( !Kit_DsdLitIsCompl(iLit) );
// consider the case of simple gate // consider the case of simple gate
pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) ); pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return Kit_DsdLitNotCond( iLit, fCompl );
if ( pObj->Type == KIT_DSD_AND ) if ( pObj->Type == KIT_DSD_AND )
{ {
Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew ); Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew );
pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_AND, nLitsNew ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ ) for ( i = 0; i < pObjNew->nFans; i++ )
pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] ); pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
return Dsd_Var2Lit( pObjNew->Id, fCompl ); return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
} }
if ( pObj->Type == KIT_DSD_XOR ) if ( pObj->Type == KIT_DSD_XOR )
{ {
Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew ); Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew );
pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_XOR, nLitsNew ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ ) for ( i = 0; i < pObjNew->nFans; i++ )
{ {
pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Dsd_LitRegular(piLitsNew[i]) ); pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Kit_DsdLitRegular(piLitsNew[i]) );
fCompl ^= Dsd_LitIsCompl(piLitsNew[i]); fCompl ^= Kit_DsdLitIsCompl(piLitsNew[i]);
} }
return Dsd_Var2Lit( pObjNew->Id, fCompl ); return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
} }
assert( pObj->Type == KIT_DSD_PRIME ); assert( pObj->Type == KIT_DSD_PRIME );
// create new PRIME node // create new PRIME node
pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
// copy the truth table // copy the truth table
pTruth = Dsd_ObjTruth( pObj ); pTruth = Kit_DsdObjTruth( pObj );
pTruthNew = Dsd_ObjTruth( pObjNew ); pTruthNew = Kit_DsdObjTruth( pObjNew );
Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans ); Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
// create fanins // create fanins
Dsd_ObjForEachFanin( pNtk, pObj, iLitFanin, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
{ {
pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin ); pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin );
// complement the corresponding inputs of the truth table // complement the corresponding inputs of the truth table
if ( Dsd_LitIsCompl(pObjNew->pFans[i]) ) if ( Kit_DsdLitIsCompl(pObjNew->pFans[i]) )
{ {
pObjNew->pFans[i] = Dsd_LitRegular(pObjNew->pFans[i]); pObjNew->pFans[i] = Kit_DsdLitRegular(pObjNew->pFans[i]);
Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i ); Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
} }
} }
// if the incoming phase is complemented, absorb it into the prime node // if the incoming phase is complemented, absorb it into the prime node
if ( fCompl ) if ( fCompl )
Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans ); Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
return Dsd_Var2Lit( pObjNew->Id, 0 ); return Kit_DsdVar2Lit( pObjNew->Id, 0 );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -588,25 +658,25 @@ int Kit_DsdExpandNode_rec( Dsd_Ntk_t * pNew, Dsd_Ntk_t * p, int iLit ) ...@@ -588,25 +658,25 @@ int Kit_DsdExpandNode_rec( Dsd_Ntk_t * pNew, Dsd_Ntk_t * p, int iLit )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Dsd_Ntk_t * Kit_DsdExpand( Dsd_Ntk_t * p ) Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
{ {
Dsd_Ntk_t * pNew; Kit_DsdNtk_t * pNew;
Dsd_Obj_t * pObjNew; Kit_DsdObj_t * pObjNew;
assert( p->nVars <= 16 ); assert( p->nVars <= 16 );
// create a new network // create a new network
pNew = Kit_DsdNtkAlloc( p->nVars ); pNew = Kit_DsdNtkAlloc( p->nVars );
// consider simple special cases // consider simple special cases
if ( Dsd_NtkRoot(p)->Type == KIT_DSD_CONST1 ) if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
{ {
pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_CONST1, 0 ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
pNew->Root = Dsd_Var2Lit( pObjNew->Id, Dsd_LitIsCompl(p->Root) ); pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
return pNew; return pNew;
} }
if ( Dsd_NtkRoot(p)->Type == KIT_DSD_VAR ) if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
{ {
pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_VAR, 1 ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
pObjNew->pFans[0] = Dsd_NtkRoot(p)->pFans[0]; pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
pNew->Root = Dsd_Var2Lit( pObjNew->Id, Dsd_LitIsCompl(p->Root) ); pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
return pNew; return pNew;
} }
// convert the root node // convert the root node
...@@ -625,21 +695,86 @@ Dsd_Ntk_t * Kit_DsdExpand( Dsd_Ntk_t * p ) ...@@ -625,21 +695,86 @@ Dsd_Ntk_t * Kit_DsdExpand( Dsd_Ntk_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, int Id ) int Kit_DsdFindLargeBox_rec( Kit_DsdNtk_t * pNtk, int Id, int Size )
{ {
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
unsigned iLit, i, RetValue; unsigned iLit, i, RetValue;
pObj = Dsd_NtkObj( pNtk, Id ); pObj = Kit_DsdNtkObj( pNtk, Id );
if ( pObj->nFans > 3 ) if ( pObj == NULL )
return 0;
if ( pObj->Type == KIT_DSD_PRIME && (int)pObj->nFans > Size )
return 1; return 1;
RetValue = 0; RetValue = 0;
Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
RetValue |= Kit_DsdFindLargeBox( pNtk, Dsd_Lit2Var(iLit) ); RetValue |= Kit_DsdFindLargeBox_rec( pNtk, Kit_DsdLit2Var(iLit), Size );
return RetValue; return RetValue;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns 1 if there is a component with more than 3 inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
{
return Kit_DsdFindLargeBox_rec( pNtk, Kit_DsdLit2Var(pNtk->Root), Size );
}
/**Function*************************************************************
Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdRootNodeHasCommonVars( Kit_DsdObj_t * pObj0, Kit_DsdObj_t * pObj1 )
{
unsigned i, k;
for ( i = 0; i < pObj0->nFans; i++ )
{
if ( Kit_DsdLit2Var(pObj0->pFans[i]) >= 4 )
continue;
for ( k = 0; k < pObj1->nFans; k++ )
if ( Kit_DsdLit2Var(pObj0->pFans[i]) == Kit_DsdLit2Var(pObj1->pFans[k]) )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
{
assert( pNtk0->nVars == 4 );
assert( pNtk1->nVars == 4 );
if ( Kit_DsdFindLargeBox(pNtk0, 2) )
return 0;
if ( Kit_DsdFindLargeBox(pNtk1, 2) )
return 0;
return Kit_DsdRootNodeHasCommonVars( Kit_DsdNtkRoot(pNtk0), Kit_DsdNtkRoot(pNtk1) );
}
/**Function*************************************************************
Synopsis [Performs decomposition of the node.] Synopsis [Performs decomposition of the node.]
Description [] Description []
...@@ -649,11 +784,11 @@ int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, int Id ) ...@@ -649,11 +784,11 @@ int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, int Id )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, unsigned char * pPar ) void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar )
{ {
Dsd_Obj_t * pRes, * pRes0, * pRes1; Kit_DsdObj_t * pRes, * pRes0, * pRes1;
int nWords = Kit_TruthWordNum(pObj->nFans); int nWords = Kit_TruthWordNum(pObj->nFans);
unsigned * pTruth = Dsd_ObjTruth(pObj); unsigned * pTruth = Kit_DsdObjTruth(pObj);
unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords }; unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} }; unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
int i, iLit0, iLit1, nFans0, nFans1, nPairs; int i, iLit0, iLit1, nFans0, nFans1, nPairs;
...@@ -682,12 +817,11 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -682,12 +817,11 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
{ {
pObj->Type = KIT_DSD_NONE; pObj->Type = KIT_DSD_NONE;
if ( pTruth[0] == 0x55555555 ) if ( pTruth[0] == 0x55555555 )
pObj->pFans[0] = Dsd_LitNot(pObj->pFans[0]); pObj->pFans[0] = Kit_DsdLitNot(pObj->pFans[0]);
else else
assert( pTruth[0] == 0xAAAAAAAA ); assert( pTruth[0] == 0xAAAAAAAA );
// update the parent pointer // update the parent pointer
// assert( !Dsd_LitIsCompl(*pPar) ); *pPar = Kit_DsdLitNotCond( pObj->pFans[0], Kit_DsdLitIsCompl(*pPar) );
*pPar = Dsd_LitNotCond( pObj->pFans[0], Dsd_LitIsCompl(*pPar) );
return; return;
} }
...@@ -716,22 +850,22 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -716,22 +850,22 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
if ( uSupp0 & uSupp1 ) if ( uSupp0 & uSupp1 )
continue; continue;
// perform MUX decomposition // perform MUX decomposition
pRes0 = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans ); pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
pRes1 = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans ); pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
for ( k = 0; k < pObj->nFans; k++ ) for ( k = 0; k < pObj->nFans; k++ )
{ {
pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127; pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127;
pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127; pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127;
} }
Kit_TruthCopy( Dsd_ObjTruth(pRes0), pCofs2[0], pObj->nFans ); Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
Kit_TruthCopy( Dsd_ObjTruth(pRes1), pCofs2[1], pObj->nFans ); Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
// update the current one // update the current one
assert( pObj->Type == KIT_DSD_PRIME ); assert( pObj->Type == KIT_DSD_PRIME );
pTruth[0] = 0xCACACACA; pTruth[0] = 0xCACACACA;
pObj->nFans = 3; pObj->nFans = 3;
pObj->pFans[2] = pObj->pFans[i];
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++;
pObj->pFans[2] = pObj->pFans[i];
// call recursively // call recursively
Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 ); Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 );
Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 ); Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
...@@ -740,13 +874,13 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -740,13 +874,13 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
//Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" ); //Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
// create the new node // create the new node
pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 ); pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
pRes->nRefs++; pRes->nRefs++;
pRes->nFans = 2; pRes->nFans = 2;
pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i); pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
pRes->pFans[1] = 2*pObj->Id; pRes->pFans[1] = 2*pObj->Id;
// update the parent pointer // update the parent pointer
*pPar = 2 * pRes->Id; *pPar = Kit_DsdLitNotCond( 2 * pRes->Id, Kit_DsdLitIsCompl(*pPar) );
// consider different decompositions // consider different decompositions
if ( fEquals[0][0] ) if ( fEquals[0][0] )
{ {
...@@ -754,20 +888,20 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -754,20 +888,20 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
} }
else if ( fEquals[0][1] ) else if ( fEquals[0][1] )
{ {
pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]); pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans ); Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
} }
else if ( fEquals[1][0] ) else if ( fEquals[1][0] )
{ {
*pPar = Dsd_LitNot(*pPar); *pPar = Kit_DsdLitNot(*pPar);
pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]); pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans ); Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
} }
else if ( fEquals[1][1] ) else if ( fEquals[1][1] )
{ {
*pPar = Dsd_LitNot(*pPar); *pPar = Kit_DsdLitNot(*pPar);
pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]); pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]); pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans ); Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
} }
else if ( fOppos ) else if ( fOppos )
...@@ -778,7 +912,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -778,7 +912,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
else else
assert( 0 ); assert( 0 );
// decompose the remainder // decompose the remainder
assert( Dsd_ObjTruth(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 );
return; return;
} }
...@@ -824,18 +958,21 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -824,18 +958,21 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) ) if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
{ {
// construct the MUX // construct the MUX
pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, 3 ); pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, 3 );
Dsd_ObjTruth(pRes)[0] = 0xCACACACA; Kit_DsdObjTruth(pRes)[0] = 0xCACACACA;
pRes->nRefs++; pRes->nRefs++;
pRes->nFans = 3; pRes->nFans = 3;
pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0); pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0);
pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1); pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1);
pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
// update the node // update the node
if ( fEquals[0][0] && fEquals[0][1] ) // if ( fEquals[0][0] && fEquals[0][1] )
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i ); // Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
else // else
Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i ); // Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
Kit_TruthMux( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
if ( fEquals[1][0] && fEquals[1][1] )
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 );
return; return;
...@@ -862,25 +999,25 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -862,25 +999,25 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
continue; continue;
// decomposition exists // decomposition exists
pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 ); pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
pRes->nRefs++; pRes->nRefs++;
pRes->nFans = 2; pRes->nFans = 2;
pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id; // remains in support pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id; // remains in support
pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i); pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00 if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
{ {
pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]); pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]); pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k ); Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
} }
else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01 else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
{ {
pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]); pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k ); Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
} }
else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10 else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
{ {
pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]); pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k ); Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
} }
else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11 else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
...@@ -918,21 +1055,21 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u ...@@ -918,21 +1055,21 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
{ {
Dsd_Ntk_t * pNtk; Kit_DsdNtk_t * pNtk;
Dsd_Obj_t * pObj; Kit_DsdObj_t * pObj;
unsigned uSupp; unsigned uSupp;
int i, nVarsReal; int i, nVarsReal;
assert( nVars <= 16 ); assert( nVars <= 16 );
pNtk = Kit_DsdNtkAlloc( nVars ); pNtk = Kit_DsdNtkAlloc( nVars );
pNtk->Root = Dsd_Var2Lit( pNtk->nVars, 0 ); pNtk->Root = Kit_DsdVar2Lit( pNtk->nVars, 0 );
// create the first node // create the first node
pObj = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, nVars ); pObj = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
assert( pNtk->pNodes[0] == pObj ); assert( pNtk->pNodes[0] == pObj );
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
pObj->pFans[i] = Dsd_Var2Lit( i, 0 ); pObj->pFans[i] = Kit_DsdVar2Lit( i, 0 );
Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars ); Kit_TruthCopy( Kit_DsdObjTruth(pObj), pTruth, nVars );
uSupp = Kit_TruthSupport( pTruth, nVars ); uSupp = Kit_TruthSupport( pTruth, nVars );
// consider special cases // consider special cases
nVarsReal = Kit_WordCountOnes( uSupp ); nVarsReal = Kit_WordCountOnes( uSupp );
...@@ -941,14 +1078,14 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) ...@@ -941,14 +1078,14 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
pObj->Type = KIT_DSD_CONST1; pObj->Type = KIT_DSD_CONST1;
pObj->nFans = 0; pObj->nFans = 0;
if ( pTruth[0] == 0 ) if ( pTruth[0] == 0 )
pNtk->Root = Dsd_LitNot(pNtk->Root); pNtk->Root = Kit_DsdLitNot(pNtk->Root);
return pNtk; return pNtk;
} }
if ( nVarsReal == 1 ) if ( nVarsReal == 1 )
{ {
pObj->Type = KIT_DSD_VAR; pObj->Type = KIT_DSD_VAR;
pObj->nFans = 1; pObj->nFans = 1;
pObj->pFans[0] = Dsd_Var2Lit( 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 );
...@@ -966,17 +1103,18 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) ...@@ -966,17 +1103,18 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit ) int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
{ {
Dsd_Ntk_t * pNtk0, * pNtk1; Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
// Dsd_Obj_t * pRoot; // Kit_DsdObj_t * pRoot;
unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) }; unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
unsigned i, * pTruth; unsigned i, * pTruth;
int fVerbose = 1; int fVerbose = 0;
int RetValue = 0;
pTruth = pTruthInit; pTruth = pTruthInit;
// pRoot = Dsd_NtkRoot(pNtk); // pRoot = Kit_DsdNtkRoot(pNtk);
// pTruth = Dsd_ObjTruth(pRoot); // pTruth = Kit_DsdObjTruth(pRoot);
// assert( pRoot->nFans == pNtk->nVars ); // assert( pRoot->nFans == pNtk->nVars );
if ( fVerbose ) if ( fVerbose )
...@@ -991,24 +1129,72 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit ) ...@@ -991,24 +1129,72 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
{ {
Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i ); Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i );
pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars ); pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars );
pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
Kit_DsdNtkFree( pTemp );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Cof%d0: ", i ); printf( "Cof%d0: ", i );
Kit_DsdPrint( stdout, pNtk0 ); Kit_DsdPrint( stdout, pNtk0 );
} }
Kit_DsdNtkFree( pNtk0 );
Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i ); Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i );
pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars ); pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars );
pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
Kit_DsdNtkFree( pTemp );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Cof%d1: ", i ); printf( "Cof%d1: ", i );
Kit_DsdPrint( stdout, pNtk1 ); Kit_DsdPrint( stdout, pNtk1 );
} }
if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
RetValue = 1;
Kit_DsdNtkFree( pNtk0 ); Kit_DsdNtkFree( pNtk0 );
Kit_DsdNtkFree( pNtk1 );
} }
if ( fVerbose ) if ( fVerbose )
printf( "\n" ); printf( "\n" );
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
{
Kit_DsdMan_t * p;
Kit_DsdNtk_t * pNtk;
unsigned * pTruthC;
int Result;
// decompose the function
pNtk = Kit_DsdDecompose( pTruth, nVars );
Result = Kit_DsdCountLuts( pNtk, nLutSize );
// printf( "\n" );
// Kit_DsdPrint( stdout, pNtk );
// printf( "Eval = %d.\n", Result );
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
Kit_DsdNtkFree( pNtk );
return Result;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1024,19 +1210,110 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit ) ...@@ -1024,19 +1210,110 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
***********************************************************************/ ***********************************************************************/
void Kit_DsdTest( unsigned * pTruth, int nVars ) void Kit_DsdTest( unsigned * pTruth, int nVars )
{ {
Dsd_Ntk_t * pNtk; Kit_DsdMan_t * p;
unsigned * pTruthC;
Kit_DsdNtk_t * pNtk, * pTemp;
pNtk = Kit_DsdDecompose( pTruth, nVars ); pNtk = Kit_DsdDecompose( pTruth, nVars );
// if ( Kit_DsdFindLargeBox(pNtk, Dsd_Lit2Var(pNtk->Root)) ) // if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) )
// Kit_DsdPrint( stdout, pNtk ); // Kit_DsdPrint( stdout, pNtk );
// if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 ) // if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
printf( "\n" );
Kit_DsdPrint( stdout, pNtk );
pNtk = Kit_DsdExpand( pTemp = pNtk );
Kit_DsdNtkFree( pTemp );
Kit_DsdPrint( stdout, pNtk );
// if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) )
// Kit_DsdTestCofs( pNtk, pTruth );
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
pTruthC = Kit_DsdTruthCompute( p, pNtk );
// Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
// Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
{
// printf( "Verification is okay.\n" );
}
else
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
Kit_DsdTestCofs( pNtk, pTruth );
Kit_DsdNtkFree( pNtk ); Kit_DsdNtkFree( pNtk );
} }
/**Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdPrecompute4Vars()
{
Kit_DsdMan_t * p;
Kit_DsdNtk_t * pNtk, * pTemp;
FILE * pFile;
unsigned uTruth;
unsigned * pTruthC;
char Buffer[256];
int i, RetValue;
int Counter1 = 0, Counter2 = 0;
pFile = fopen( "5npn/npn4.txt", "r" );
for ( i = 0; fgets( Buffer, 100, pFile ); i++ )
{
Buffer[6] = 0;
Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
uTruth = ((uTruth & 0xffff) << 16) | (uTruth & 0xffff);
pNtk = Kit_DsdDecompose( &uTruth, 4 );
pNtk = Kit_DsdExpand( pTemp = pNtk );
Kit_DsdNtkFree( pTemp );
if ( Kit_DsdFindLargeBox(pNtk, 3) )
{
// RetValue = 0;
RetValue = Kit_DsdTestCofs( pNtk, &uTruth );
printf( "\n" );
printf( "%3d : Non-DSD function %s %s\n", i, Buffer + 2, RetValue? "implementable" : "" );
Kit_DsdPrint( stdout, pNtk );
Counter1++;
Counter2 += RetValue;
}
/*
printf( "%3d : Function %s ", i, Buffer + 2 );
if ( !Kit_DsdFindLargeBox(pNtk, 3) )
Kit_DsdPrint( stdout, pNtk );
else
printf( "\n" );
*/
p = Kit_DsdManAlloc( 4 );
pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
Kit_DsdNtkFree( pNtk );
}
fclose( pFile );
printf( "non-DSD = %d implementable = %d\n", Counter1, Counter2 );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/opt/rwr/rwrEva.c
...@@ -129,7 +129,7 @@ clk2 = clock(); ...@@ -129,7 +129,7 @@ clk2 = clock();
// label MFFC with current ID // label MFFC with current ID
Abc_NtkIncrementTravId( pNode->pNtk ); Abc_NtkIncrementTravId( pNode->pNtk );
nNodesSaved = Abc_NodeMffcLabel( pNode ); nNodesSaved = Abc_NodeMffcLabelAig( pNode );
// unmark the fanin boundary // unmark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Abc_ObjRegular(pFanin)->vFanouts.nSize--; Abc_ObjRegular(pFanin)->vFanouts.nSize--;
......
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