diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-03-13 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-03-13 08:01:00 -0700 |
| commit | 2696cf05e568f7a928f32b01534d106bf626ef8a (patch) | |
| tree | c795e6a7c53151faa830a55bfdc082dc67d98e4e | |
| parent | 93c05287f0d8b044e620b41608df906bbad39db5 (diff) | |
| download | abc-2696cf05e568f7a928f32b01534d106bf626ef8a.tar.gz abc-2696cf05e568f7a928f32b01534d106bf626ef8a.tar.bz2 abc-2696cf05e568f7a928f32b01534d106bf626ef8a.zip | |
Version abc70313
37 files changed, 1319 insertions, 98 deletions
@@ -254,6 +254,10 @@ SOURCE=.\src\base\abci\abcGen.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcHaig.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcIf.c # End Source File # Begin Source File @@ -30,7 +30,6 @@ alias fs fraig_sweep alias fsto fraig_store alias fres fraig_restore alias ft fraig_trust -alias ifs if -s alias pex print_exdc -d alias pf print_factor alias pfan print_fanio @@ -68,6 +67,7 @@ alias rs resub alias rsz resub -z alias sa set autoexec ps alias scl scleanup +alias sif if -s alias so source -x alias st strash alias sw sweep @@ -117,13 +117,25 @@ alias fflitmin "compress2rs; ren; sop; ps -f" #alias t "rvl th/lib.v; rvv th/t2.v" #alias t "so c/pure_sat/test.c" #alias t "r c/14/csat_998.bench; st; ps" -alias t0 "r res.blif; aig; mfs" -alias t "r res2.blif; aig; mfs" +#alias t0 "r res.blif; aig; mfs" +#alias t "r res2.blif; aig; mfs" -alias tt "r a/quip_opt/nut_001_opt.blif" -alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif" -alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v" +#alias tt "r a/quip_opt/nut_001_opt.blif" +#alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif" +#alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v" -alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps" +alias t "r c.blif; st; haig_start; resyn; haig_use" +alias tt "r i10.blif; st; haig_start; resyn2; haig_use" +alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps" +alias qs1 "qvar -I 96 -u; ps; qbf -P 96" +alias qs2 "qvar -I 96 -u; qvar -I 97 -u; ps; qbf -P 96" +alias qs3 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; ps; qbf -P 96" +alias qs4 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; ps; qbf -P 96" +alias qs5 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; ps; qbf -P 96" +alias qs6 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; ps; qbf -P 96" +alias qs7 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; ps; qbf -P 96" +alias qs8 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; ps; qbf -P 96" +alias qs9 "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; ps; qbf -P 96" +alias qsA "qvar -I 96 -u; qvar -I 97 -u; qvar -I 98 -u; qvar -I 99 -u; qvar -I 100 -u; qvar -I 101 -u; qvar -I 102 -u; qvar -I 103 -u; qvar -I 104 -u; qvar -I 105 -u; ps; qbf -P 96" diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index ce4cdfde..34124599 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -61,9 +61,10 @@ typedef enum { } Hop_Type_t; // the AIG node -struct Hop_Obj_t_ // 4 words +struct Hop_Obj_t_ // 6 words { void * pData; // misc + Hop_Obj_t * pNext; // strashing table Hop_Obj_t * pFanin0; // fanin Hop_Obj_t * pFanin1; // fanin unsigned long Type : 3; // object type @@ -71,6 +72,7 @@ struct Hop_Obj_t_ // 4 words unsigned long fMarkA : 1; // multipurpose mask unsigned long fMarkB : 1; // multipurpose mask unsigned long nRefs : 26; // reference count (level) + int Id; // unique ID of the node }; // the AIG manager @@ -79,6 +81,7 @@ struct Hop_Man_t_ // AIG nodes Vec_Ptr_t * vPis; // the array of PIs Vec_Ptr_t * vPos; // the array of POs + Vec_Ptr_t * vNodes; // the array of all nodes (optional) Hop_Obj_t * pConst1; // the constant 1 node Hop_Obj_t Ghost; // the ghost node // AIG node counters @@ -181,6 +184,7 @@ static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_ static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond(Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; } static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; } static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); } +static inline int Hop_ObjFaninPhase( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; } static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); } static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin ) { @@ -219,6 +223,12 @@ static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p ) pTemp = p->pListFree; p->pListFree = *((Hop_Obj_t **)pTemp); memset( pTemp, 0, sizeof(Hop_Obj_t) ); + if ( p->vNodes ) + { + assert( p->nCreated == Vec_PtrSize(p->vNodes) ); + Vec_PtrPush( p->vNodes, pTemp ); + } + pTemp->Id = p->nCreated++; return pTemp; } static inline void Hop_ManRecycleMemory( Hop_Man_t * p, Hop_Obj_t * pEntry ) @@ -279,6 +289,8 @@ extern void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_ extern void Hop_ObjDisconnect( Hop_Man_t * p, Hop_Obj_t * pObj ); extern void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj ); extern void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj ); +extern Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj ); +extern void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew ); /*=== aigOper.c =========================================================*/ extern Hop_Obj_t * Hop_IthVar( Hop_Man_t * p, int i ); extern Hop_Obj_t * Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type ); diff --git a/src/aig/hop/hopMan.c b/src/aig/hop/hopMan.c index 18b8618b..4fa52fbd 100644 --- a/src/aig/hop/hopMan.c +++ b/src/aig/hop/hopMan.c @@ -97,6 +97,7 @@ void Hop_ManStop( Hop_Man_t * p ) if ( p->vChunks ) Hop_ManStopMemory( p ); if ( p->vPis ) Vec_PtrFree( p->vPis ); if ( p->vPos ) Vec_PtrFree( p->vPos ); + if ( p->vNodes ) Vec_PtrFree( p->vNodes ); free( p->pTable ); free( p ); } diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c index 037203fb..c4430abd 100644 --- a/src/aig/hop/hopObj.c +++ b/src/aig/hop/hopObj.c @@ -46,7 +46,6 @@ Hop_Obj_t * Hop_ObjCreatePi( Hop_Man_t * p ) pObj->Type = AIG_PI; Vec_PtrPush( p->vPis, pObj ); p->nObjs[AIG_PI]++; - p->nCreated++; return pObj; } @@ -73,9 +72,10 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver ) Hop_ObjRef( Hop_Regular(pDriver) ); else pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) ); + // set the phase +// pObj->fPhase = Hop_ObjFaninPhase(pDriver); // update node counters of the manager p->nObjs[AIG_PO]++; - p->nCreated++; return pObj; } @@ -103,7 +103,7 @@ Hop_Obj_t * Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost ) Hop_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 ); // update node counters of the manager p->nObjs[Hop_ObjType(pObj)]++; - p->nCreated++; + assert( pObj->pData == NULL ); return pObj; } @@ -135,6 +135,8 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj } else pObj->nRefs = Hop_ObjLevelNew( pObj ); + // set the phase +// pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1); // add the node to the structural hash table Hop_TableInsert( p, pObj ); } @@ -221,6 +223,46 @@ void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj ) Hop_ObjDelete_rec( p, pFanin1 ); } +/**Function************************************************************* + + Synopsis [Returns the representative of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj ) +{ + if ( Hop_Regular(pObj)->pData == NULL ) + return Hop_Regular(pObj); + return Hop_ObjRepr( Hop_Regular(pObj)->pData ); +} + +/**Function************************************************************* + + Synopsis [Sets an equivalence relation between the nodes.] + + Description [Makes the representative of pNew point to the representaive of pOld.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew ) +{ + Hop_Obj_t * pOldRepr; + Hop_Obj_t * pNewRepr; + assert( pOld != NULL && pNew != NULL ); + pOldRepr = Hop_ObjRepr(pOld); + pNewRepr = Hop_ObjRepr(pNew); + if ( pNewRepr != pOldRepr ) + pNewRepr->pData = pOldRepr; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 063f8b15..3a278927 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -166,6 +166,7 @@ struct Abc_Obj_t_ // 12 words void * pData; // the network specific data (SOP, BDD, gate, equiv class, etc) Abc_Obj_t * pNext; // the next pointer in the hash table Abc_Obj_t * pCopy; // the copy of this object + Hop_Obj_t * pEquiv; // pointer to the HAIG node }; struct Abc_Ntk_t_ @@ -210,6 +211,7 @@ struct Abc_Ntk_t_ Abc_Ntk_t * pExdc; // the EXDC network (if given) void * pData; // misc Abc_Ntk_t * pCopy; + Hop_Man_t * pHaig; // history AIG // node attributes Vec_Ptr_t * vAttrs; // managers of various node attributes (node functionality, global BDDs, etc) }; @@ -254,6 +256,7 @@ static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; } static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; } static inline int Abc_InfoIsOrOne( unsigned * p, unsigned * q, int nWords ){ int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~(p[i] | q[i]) ) return 0; return 1; } +static inline int Abc_InfoIsOrOne3( unsigned * p, unsigned * q, unsigned * r, int nWords ){ int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~(p[i] | q[i] | r[i]) ) return 0; return 1; } // checking the network type static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; } @@ -347,7 +350,8 @@ static inline Vec_Int_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj ) { return &p static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj ) { return pObj->pCopy; } static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj ) { return pObj->pNtk; } static inline void * Abc_ObjData( Abc_Obj_t * pObj ) { return pObj->pData; } -static inline Abc_Obj_t * Abc_ObjEquiv( Abc_Obj_t * pObj ) { return Abc_ObjRegular(pObj)->pCopy? Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)) : NULL; } +static inline Hop_Obj_t * Abc_ObjEquiv( Abc_Obj_t * pObj ) { return pObj->pEquiv; } +static inline Abc_Obj_t * Abc_ObjCopyCond( Abc_Obj_t * pObj ) { return Abc_ObjRegular(pObj)->pCopy? Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)) : NULL; } // setting data members of the network static inline void Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy ) { pObj->pCopy = pCopy; } @@ -398,6 +402,8 @@ static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj ) { return Ab static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ); } static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) ); } static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) ); } +static inline Hop_Obj_t * Abc_ObjChild0Equiv( Abc_Obj_t * pObj ) { return Hop_NotCond( Abc_ObjFanin0(pObj)->pEquiv, Abc_ObjFaninC0(pObj) ); } +static inline Hop_Obj_t * Abc_ObjChild1Equiv( Abc_Obj_t * pObj ) { return Hop_NotCond( Abc_ObjFanin1(pObj)->pEquiv, Abc_ObjFaninC1(pObj) ); } // checking the AIG node types static inline bool Abc_AigNodeIsConst( Abc_Obj_t * pNode ) { assert(Abc_NtkIsStrash(Abc_ObjRegular(pNode)->pNtk)); return Abc_ObjRegular(pNode)->Type == ABC_OBJ_CONST1; } @@ -615,6 +621,10 @@ extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ); extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect ); extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk ); extern int Abc_NtkToAig( Abc_Ntk_t * pNtk ); +/*=== abcHaig.c ==========================================================*/ +extern int Abc_NtkHaigStart( Abc_Ntk_t * pNtk ); +extern int Abc_NtkHaigStop( Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk ); /*=== abcHie.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 287e4421..1d09548b 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -331,6 +331,9 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) // add the node to the list of updated nodes if ( pMan->vAddedCells ) Vec_PtrPush( pMan->vAddedCells, pAnd ); + // create HAIG + if ( pAnd->pNtk->pHaig ) + pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) ); return pAnd; } @@ -371,6 +374,9 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * // add the node to the list of updated nodes // if ( pMan->vAddedCells ) // Vec_PtrPush( pMan->vAddedCells, pAnd ); + // create HAIG + if ( pAnd->pNtk->pHaig ) + pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) ); return pAnd; } @@ -812,6 +818,9 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool Vec_PtrPush( pMan->vStackReplaceOld, pOld ); Vec_PtrPush( pMan->vStackReplaceNew, pNew ); assert( !Abc_ObjIsComplement(pOld) ); + // create HAIG + if ( pOld->pNtk->pHaig ) + Hop_ObjCreateChoice( pOld->pEquiv, Abc_ObjRegular(pNew)->pEquiv ); // process the replacements while ( Vec_PtrSize(pMan->vStackReplaceOld) ) { diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index f1101f19..03f41f3b 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -52,7 +52,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNode; DdManager * dd; int nFaninsMax, i; - + assert( Abc_NtkHasSop(pNtk) ); // start the functionality manager diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c index 9e9d921b..56333a36 100644 --- a/src/base/abc/abcHie.c +++ b/src/base/abc/abcHie.c @@ -256,7 +256,7 @@ Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk ) pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); // duplicate the name and the spec pNtkNew->pName = Extra_UtilStrsav( pNtk->pName ); -// pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec ); + pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec ); // clean the node copy fields Abc_NtkCleanCopy( pNtk ); diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index a649fe43..91964dfa 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -420,9 +420,9 @@ void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk ) nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachLatch( pNtk, pObj, i ) { - Abc_ObjAssignName( pObj, Abc_ObjNameDummy("L", i, nDigits), NULL ); - Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjNameDummy("Li", i, nDigits), NULL ); - Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjNameDummy("Lo", i, nDigits), NULL ); + Abc_ObjAssignName( pObj, Abc_ObjNameDummy("l", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjNameDummy("li", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjNameDummy("lo", i, nDigits), NULL ); } /* nDigits = Extra_Base10Log( Abc_NtkBlackboxNum(pNtk) ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index e0773e3f..bed5d399 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -792,6 +792,9 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) int LargePiece = (4 << ABC_NUM_STEPS); if ( pNtk == NULL ) return; + // free the HAIG + if ( pNtk->pHaig ) + Abc_NtkHaigStop( pNtk ); // free EXDC Ntk if ( pNtk->pExdc ) Abc_NtkDelete( pNtk->pExdc ); diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 02d13963..6167979c 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -365,6 +365,9 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName } else if ( Abc_ObjIsLatch(pObj) ) // copy the reset value pObjNew->pData = pObj->pData; + // transfer HAIG +// pObjNew->pEquiv = pObj->pEquiv; + // remember the new node in the old node pObj->pCopy = pObjNew; return pObjNew; } diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 5f82b4b5..965e611e 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1452,7 +1452,7 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk ) int i; Abc_NtkForEachObj( pNtk, pObj, i ) if ( !Abc_ObjIsNet(pObj) ) - pObj->pCopy = pObj->pCopy? Abc_ObjEquiv(pObj->pCopy) : NULL; + pObj->pCopy = pObj->pCopy? Abc_ObjCopyCond(pObj->pCopy) : NULL; } @@ -1469,7 +1469,8 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk ) ***********************************************************************/ static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj ) { - pObj->pCopy = (void *)(((int)pObj->pCopy)++); +// pObj->pCopy = (void *)(((int)pObj->pCopy)++); + ((char*)pObj->pCopy)++; return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj); } @@ -1563,7 +1564,7 @@ int Abc_NtkCrossCut( Abc_Ntk_t * pNtk ) void Abc_NtkPrint256() { FILE * pFile; - int i; + unsigned i; pFile = fopen( "4varfs.txt", "w" ); for ( i = 1; i < (1<<16)-1; i++ ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fbe81f48..4aa13733 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -61,7 +61,7 @@ static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandSweep ( 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_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIfs ( 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 ); @@ -85,8 +85,8 @@ static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -123,6 +123,10 @@ static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandHaigStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandHaigStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandHaigUse ( Abc_Frame_t * pAbc, int argc, char ** argv ); + static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -204,7 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "sweep", Abc_CommandSweep, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "ifs", Abc_CommandIfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); @@ -228,8 +232,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); - Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); - Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); + Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); + Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); @@ -266,6 +270,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 ); + Cmd_CommandAdd( pAbc, "Choicing", "haig_start", Abc_CommandHaigStart, 0 ); + Cmd_CommandAdd( pAbc, "Choicing", "haig_stop", Abc_CommandHaigStop, 0 ); + Cmd_CommandAdd( pAbc, "Choicing", "haig_use", Abc_CommandHaigUse, 1 ); + Cmd_CommandAdd( pAbc, "SC mapping", "map", Abc_CommandMap, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Abc_CommandUnmap, 1 ); Cmd_CommandAdd( pAbc, "SC mapping", "attach", Abc_CommandAttach, 1 ); @@ -2641,7 +2649,7 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -2657,13 +2665,14 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults pPars->nWindow = 62; + pPars->nGrowthLevel = 3; pPars->nCands = 5; pPars->nSimWords = 4; pPars->fArea = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WSavwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WSCLavwh" ) ) != EOF ) { switch ( c ) { @@ -2689,6 +2698,28 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nCands = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nCands < 0 || pPars->nCands > ABC_INFINITY ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nGrowthLevel = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) + goto usage; + break; case 'a': pPars->fArea ^= 1; break; @@ -2725,9 +2756,11 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-avwh]\n" ); - fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" ); - fprintf( pErr, "\t-W <NM> : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); + fprintf( pErr, "usage: ifs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" ); + fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" ); + fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); + fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands ); fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords ); fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -5287,11 +5320,13 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAdder; int fSorter; int fMesh; + int fFpga; int fVerbose; char * FileName; extern void Abc_GenAdder( char * pFileName, int nVars ); extern void Abc_GenSorter( char * pFileName, int nVars ); extern void Abc_GenMesh( char * pFileName, int nVars ); + extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars ); pNtk = Abc_FrameReadNtk(pAbc); @@ -5302,9 +5337,11 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) nVars = 8; fAdder = 0; fSorter = 0; + fMesh = 0; + fFpga = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmfvh" ) ) != EOF ) { switch ( c ) { @@ -5328,6 +5365,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMesh ^= 1; break; + case 'f': + fFpga ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -5351,17 +5391,22 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_GenSorter( FileName, nVars ); else if ( fMesh ) Abc_GenMesh( FileName, nVars ); + else if ( fFpga ) + Abc_GenFpga( FileName, 4, 3, 10 ); +// Abc_GenFpga( FileName, 2, 2, 3 ); +// Abc_GenFpga( FileName, 3, 2, 5 ); else printf( "Type of circuit is not specified.\n" ); return 0; usage: - fprintf( pErr, "usage: gen [-N] [-asmvh] <file>\n" ); + fprintf( pErr, "usage: gen [-N] [-asmfvh] <file>\n" ); fprintf( pErr, "\t generates simple circuits\n" ); fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars ); fprintf( pErr, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" ); fprintf( pErr, "\t-s : generate a sorter [default = %s]\n", fSorter? "yes": "no" ); fprintf( pErr, "\t-m : generate a mesh [default = %s]\n", fMesh? "yes": "no" ); + fprintf( pErr, "\t-f : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t<file> : output file name\n"); @@ -7498,6 +7543,158 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandHaigStart( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs; run strashing (\"st\").\n" ); + return 0; + } + Abc_NtkHaigStart( pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: haig_start [-h]\n" ); + fprintf( pErr, "\t starts constructive accumulation of combinational choices\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandHaigStop( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs; run strashing (\"st\").\n" ); + return 0; + } + Abc_NtkHaigStop( pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: haig_stop [-h]\n" ); + fprintf( pErr, "\t cleans the internal storage for combinational choices\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandHaigUse( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs; run strashing (\"st\").\n" ); + return 0; + } + // get the new network + pNtkRes = Abc_NtkHaigUse( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Transforming internal storage into AIG with choices has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: haig_use [-h]\n" ); + fprintf( pErr, "\t transforms internal storage into an AIG with choices\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -8242,7 +8439,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults memset( pPars, 0, sizeof(If_Par_t) ); // user-controlable paramters - pPars->nLutSize = 4; + pPars->nLutSize = -1; pPars->nCutsMax = 8; pPars->nFlowIters = 1; pPars->nAreaIters = 2; @@ -8360,19 +8557,24 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } -/* - if ( pPars->fSeq ) - { - fprintf( pErr, "Sequential mapping is currently being implemented.\n" ); - return 1; - } -*/ + if ( pPars->fSeqMap && pPars->nLatches == 0 ) { fprintf( pErr, "The network has no latches. Use combinational mapping instead of sequential.\n" ); return 1; } + if ( pPars->nLutSize == -1 ) + { + if ( pPars->pLutLib == NULL ) + { + fprintf( pErr, "The LUT library is not given.\n" ); + return 1; + } + // get LUT size from the library + pPars->nLutSize = pPars->pLutLib->LutMax; + } + if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE ) { fprintf( pErr, "Incorrect LUT size (%d).\n", pPars->nLutSize ); diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 819974bf..f55dc435 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -49,6 +49,7 @@ static Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode ); ***********************************************************************/ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel ) { + extern void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ); Abc_Ntk_t * pNtkAig; assert( Abc_NtkIsStrash(pNtk) ); // compute the required times @@ -59,6 +60,9 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, } // perform balancing pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer HAIG + Abc_NtkHaigTranfer( pNtk, pNtkAig ); + // perform balancing Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel ); Abc_NtkFinalize( pNtk, pNtkAig ); // undo the required times @@ -267,6 +271,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ // if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_AigConst1(pNtkNew) ) // printf( "Constant node\n" ); // assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level ); + // update HAIG + if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig ) + Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv ); return pNodeOld->pCopy; } diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c index 5d74bda5..bfb41374 100644 --- a/src/base/abci/abcGen.c +++ b/src/base/abci/abcGen.c @@ -360,6 +360,150 @@ void Abc_GenMesh( char * pFileName, int nVars ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_WriteKLut( FILE * pFile, int nLutSize ) +{ + int i, iVar, iNext, nPars = (1 << nLutSize); + fprintf( pFile, "\n" ); + fprintf( pFile, ".model lut%d\n", nLutSize ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nPars; i++ ) + fprintf( pFile, " p%02d", i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nLutSize; i++ ) + fprintf( pFile, " i%d", i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".outputs o\n" ); + fprintf( pFile, ".names n01 o\n" ); + fprintf( pFile, "1 1\n" ); + // write internal MUXes + iVar = 0; + iNext = 2; + for ( i = 1; i < nPars; i++ ) + { + if ( i == iNext ) + { + iNext *= 2; + iVar++; + } + if ( iVar == nLutSize - 1 ) + fprintf( pFile, ".names i%d p%02d p%02d n%02d\n", iVar, 2*(i-nPars/2), 2*(i-nPars/2)+1, i ); + else + fprintf( pFile, ".names i%d n%02d n%02d n%02d\n", iVar, 2*i, 2*i+1, i ); + fprintf( pFile, "01- 1\n" ); + fprintf( pFile, "1-1 1\n" ); + } + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Generates structure of L K-LUTs implementing an N-var function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars ) +{ + FILE * pFile; + int nVarsLut = (1 << nLutSize); // the number of LUT variables + int nVarsLog = Extra_Base2Log( nVars + nLuts - 1 ); // the number of encoding vars + int nVarsDeg = (1 << nVarsLog); // the number of LUT variables (total) + int nParsLut = nLuts * (1 << nLutSize); // the number of LUT params + int nParsVar = nLuts * nLutSize * nVarsLog; // the number of var params + int i, j, k; + + assert( nVars > 0 ); + + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# Structure with %d %d-LUTs for %d-var function generated by ABC on %s\n", nLuts, nLutSize, nVars, Extra_TimeStamp() ); + fprintf( pFile, ".model struct%dx%d_%d\n", nLuts, nLutSize, nVars ); + + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nParsLut; i++ ) + fprintf( pFile, " pl%02d", i ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nParsVar; i++ ) + fprintf( pFile, " pv%02d", i ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " v%02d", i ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".outputs" ); + fprintf( pFile, " v%02d", nVars + nLuts - 1 ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".names Gnd\n" ); + fprintf( pFile, " 0\n" ); + + // generate LUTs + for ( i = 0; i < nLuts; i++ ) + { + fprintf( pFile, ".subckt lut%d", nLutSize ); + // generate config parameters + for ( k = 0; k < nVarsLut; k++ ) + fprintf( pFile, " p%02d=pl%02d", k, i * nVarsLut + k ); + // generate the inputs + for ( k = 0; k < nLutSize; k++ ) + fprintf( pFile, " i%d=s%02d", k, i * nLutSize + k ); + // generate the output + fprintf( pFile, " o=v%02d", nVars + i ); + fprintf( pFile, "\n" ); + } + + // generate LUT inputs + for ( i = 0; i < nLuts; i++ ) + { + for ( j = 0; j < nLutSize; j++ ) + { + fprintf( pFile, ".subckt lut%d", nVarsLog ); + // generate config parameters + for ( k = 0; k < nVarsDeg; k++ ) + { + if ( k < nVars + nLuts - 1 && k < nVars + i ) + fprintf( pFile, " p%02d=v%02d", k, k ); + else + fprintf( pFile, " p%02d=Gnd", k ); + } + // generate the inputs + for ( k = 0; k < nVarsLog; k++ ) + fprintf( pFile, " i%d=pv%02d", k, (i * nLutSize + j) * nVarsLog + k ); + // generate the output + fprintf( pFile, " o=s%02d", i * nLutSize + j ); + fprintf( pFile, "\n" ); + } + } + + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); + + // generate LUTs + Abc_WriteKLut( pFile, nLutSize ); + if ( nVarsLog != nLutSize ) + Abc_WriteKLut( pFile, nVarsLog ); + fclose( pFile ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c new file mode 100644 index 00000000..87fada22 --- /dev/null +++ b/src/base/abci/abcHaig.c @@ -0,0 +1,506 @@ +/**CFile**************************************************************** + + FileName [abcHaig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Implements history AIG for combinational rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcHaig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start history AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkHaigStart( Abc_Ntk_t * pNtk ) +{ + Hop_Man_t * p; + Abc_Obj_t * pObj, * pTemp; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + // check if the package is already started + if ( pNtk->pHaig ) + { + Abc_NtkHaigStop( pNtk ); + assert( pNtk->pHaig == NULL ); + printf( "Warning: Previous history AIG was removed.\n" ); + } + // make sure the data is clean + Abc_NtkForEachObj( pNtk, pObj, i ) + assert( pObj->pEquiv == NULL ); + // start the HOP package + p = Hop_ManStart(); + p->vNodes = Vec_PtrAlloc( 4096 ); + Vec_PtrPush( p->vNodes, Hop_ManConst1(p) ); + // map the constant node + Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p); + // map the CIs + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pEquiv = Hop_ObjCreatePi(p); + // map the internal nodes + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pEquiv = Hop_And( p, Abc_ObjChild0Equiv(pObj), Abc_ObjChild1Equiv(pObj) ); + // map the choice nodes + if ( Abc_NtkGetChoiceNum( pNtk ) ) + { + // print warning about choice nodes + printf( "Warning: The choice nodes in the original AIG are converted into HAIG.\n" ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + if ( !Abc_AigNodeIsChoice( pObj ) ) + continue; + for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData ) + Hop_ObjCreateChoice( pObj->pEquiv, pTemp->pEquiv ); + } + } + // make sure everything is okay + if ( !Hop_ManCheck(p) ) + { + printf( "Abc_NtkHaigStart: Check for History AIG has failed.\n" ); + Hop_ManStop(p); + return 0; + } + pNtk->pHaig = p; + return 1; +} + +/**Function************************************************************* + + Synopsis [Stops history AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkHaigStop( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + if ( pNtk->pHaig == NULL ) + { + printf( "Warning: History AIG is not allocated.\n" ); + return 1; + } + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->pEquiv = NULL; + Hop_ManStop( pNtk->pHaig ); + pNtk->pHaig = NULL; + return 1; +} + +/**Function************************************************************* + + Synopsis [Transfers the HAIG to the new network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew ) +{ + Abc_Obj_t * pObj; + int i; + if ( pNtkOld->pHaig == NULL ) + return; + // transfer the package + assert( pNtkNew->pHaig == NULL ); + pNtkNew->pHaig = pNtkOld->pHaig; + pNtkOld->pHaig = NULL; + // transfer constant pointer + Abc_AigConst1(pNtkOld)->pCopy->pEquiv = Abc_AigConst1(pNtkOld)->pEquiv; + // transfer the CI pointers + Abc_NtkForEachCi( pNtkOld, pObj, i ) + pObj->pCopy->pEquiv = pObj->pEquiv; +} + + + + +/**Function************************************************************* + + Synopsis [Collects the nodes in the classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkHaigCollectMembers( Hop_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Hop_Obj_t * pObj; + int i; + vNodes = Vec_PtrAlloc( 4098 ); + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + { + if ( pObj->pData == NULL ) + continue; + pObj->pData = Hop_ObjRepr( pObj ); + Vec_PtrPush( vNodes, pObj ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Creates classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkHaigCreateClasses( Vec_Ptr_t * vMembers ) +{ + Vec_Ptr_t * vClasses; + Hop_Obj_t * pObj, * pRepr; + int i; + + // count classes + vClasses = Vec_PtrAlloc( 4098 ); + Vec_PtrForEachEntry( vMembers, pObj, i ) + { + pRepr = pObj->pData; + assert( pRepr->pData == NULL ); + if ( pRepr->fMarkA == 0 ) // new + { + pRepr->fMarkA = 1; + Vec_PtrPush( vClasses, pRepr ); + } + } + + // set representatives as representatives + Vec_PtrForEachEntry( vClasses, pObj, i ) + { + pObj->fMarkA = 0; + pObj->pData = pObj; + } + + // go through the members and update + Vec_PtrForEachEntry( vMembers, pObj, i ) + { + pRepr = pObj->pData; + if ( ((Hop_Obj_t *)pRepr->pData)->Id > pObj->Id ) + pRepr->pData = pObj; + } + + // change representatives of the class + Vec_PtrForEachEntry( vMembers, pObj, i ) + { + pRepr = pObj->pData; + pObj->pData = pRepr->pData; + assert( ((Hop_Obj_t *)pObj->pData)->Id <= pObj->Id ); + } + + // update classes + Vec_PtrForEachEntry( vClasses, pObj, i ) + { + pRepr = pObj->pData; + assert( pRepr->pData == pRepr ); + pRepr->pData = NULL; + Vec_PtrWriteEntry( vClasses, i, pRepr ); + Vec_PtrPush( vMembers, pObj ); + } +/* + Vec_PtrForEachEntry( vMembers, pObj, i ) + { + printf( "ObjId = %4d : ", pObj->Id ); + if ( pObj->pData == NULL ) + { + printf( "NULL" ); + } + else + { + printf( "%4d", ((Hop_Obj_t *)pObj->pData)->Id ); + assert( ((Hop_Obj_t *)pObj->pData)->Id <= pObj->Id ); + } + printf( "\n" ); + } +*/ + return vClasses; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkHaigCheckTfi_rec( Abc_Obj_t * pNode, Abc_Obj_t * pOld ) +{ + if ( pNode == NULL ) + return 0; + if ( pNode == pOld ) + return 1; + // check the trivial cases + if ( Abc_ObjIsPi(pNode) ) + return 0; + assert( Abc_ObjIsNode(pNode) ); + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return 0; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + // check the children + if ( Abc_NtkHaigCheckTfi_rec( Abc_ObjFanin0(pNode), pOld ) ) + return 1; + if ( Abc_NtkHaigCheckTfi_rec( Abc_ObjFanin1(pNode), pOld ) ) + return 1; + // check equivalent nodes + return Abc_NtkHaigCheckTfi_rec( pNode->pData, pOld ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkHaigCheckTfi( Abc_Ntk_t * pNtk, Abc_Obj_t * pOld, Abc_Obj_t * pNew ) +{ + assert( !Abc_ObjIsComplement(pOld) ); + assert( !Abc_ObjIsComplement(pNew) ); + Abc_NtkIncrementTravId(pNtk); + return Abc_NtkHaigCheckTfi_rec( pNew, pOld ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Abc_Obj_t * Hop_ObjReprAbc( Hop_Obj_t * pObj ) +{ + Hop_Obj_t * pRepr; + Abc_Obj_t * pObjAbcThis, * pObjAbcRepr; + assert( pObj->pNext != NULL ); + if ( pObj->pData == NULL ) + return (Abc_Obj_t *)pObj->pNext; + pRepr = pObj->pData; + assert( pRepr->pData == NULL ); + pObjAbcThis = (Abc_Obj_t *)pObj->pNext; + pObjAbcRepr = (Abc_Obj_t *)pRepr->pNext; + assert( !Abc_ObjIsComplement(pObjAbcThis) ); + assert( !Abc_ObjIsComplement(pObjAbcRepr) ); + return Abc_ObjNotCond( pObjAbcRepr, pObjAbcRepr->fPhase ^ pObjAbcThis->fPhase ); +// return (Abc_Obj_t *)pObj->pNext; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Abc_Obj_t * Hop_ObjChild0Abc( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( Hop_ObjReprAbc(Hop_ObjFanin0(pObj)), Hop_ObjFaninC0(pObj) ); } +static inline Abc_Obj_t * Hop_ObjChild1Abc( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( Hop_ObjReprAbc(Hop_ObjFanin1(pObj)), Hop_ObjFaninC1(pObj) ); } + +/**Function************************************************************* + + Synopsis [Stops history AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p ) +{ + Abc_Ntk_t * pNtkAig; + Abc_Obj_t * pObjAbcThis, * pObjAbcRepr; + Abc_Obj_t * pObjOld, * pObjNew; + Hop_Obj_t * pObj; + int i; + + assert( p->nCreated == Vec_PtrSize(p->vNodes) ); + assert( Hop_ManPoNum(p) == 0 ); + + // start the new network + pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + + // transfer new nodes to the PIs of HOP + Hop_ManConst1(p)->pNext = (Hop_Obj_t *)Abc_AigConst1( pNtkAig ); + Hop_ManForEachPi( p, pObj, i ) + pObj->pNext = (Hop_Obj_t *)Abc_NtkPi( pNtkAig, i ); + + // construct new nodes + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + if ( Hop_ObjIsNode(pObj) ) + pObj->pNext = (Hop_Obj_t *)Abc_AigAnd( pNtkAig->pManFunc, Hop_ObjChild0Abc(pObj), Hop_ObjChild1Abc(pObj) ); + + // set the COs + Abc_NtkForEachCo( pNtk, pObjOld, i ) + { + pObjNew = Hop_ObjReprAbc( Abc_ObjFanin0(pObjOld)->pEquiv ); + pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(pObjOld) ); + Abc_ObjAddFanin( pObjOld->pCopy, pObjNew ); + } + + // create choice nodes + Vec_PtrForEachEntry( p->vNodes, pObj, i ) + { + Abc_Obj_t * pTemp; + if ( pObj->pData == NULL ) + continue; + + pObjAbcThis = (Abc_Obj_t *)pObj->pNext; + pObjAbcRepr = (Abc_Obj_t *)((Hop_Obj_t *)pObj->pData)->pNext; + assert( !Abc_ObjIsComplement(pObjAbcThis) ); + assert( !Abc_ObjIsComplement(pObjAbcRepr) ); + + // skip the case when the class is constant 1 + if ( pObjAbcRepr == Abc_AigConst1(pNtkAig) ) + continue; + + // skip the case when pObjAbcThis is part of the class already + for ( pTemp = pObjAbcRepr; pTemp; pTemp = pTemp->pData ) + if ( pTemp == pObjAbcThis ) + break; + if ( pTemp ) + continue; + +// assert( Abc_ObjFanoutNum(pObjAbcThis) == 0 ); + if ( Abc_ObjFanoutNum(pObjAbcThis) > 0 ) + continue; +// assert( pObjAbcThis->pData == NULL ); + if ( pObjAbcThis->pData ) + continue; + + // do not create choices if there is a path from pObjAbcThis to pObjAbcRepr + if ( !Abc_NtkHaigCheckTfi( pNtkAig, pObjAbcRepr, pObjAbcThis ) ) + { + // find the last node in the class + while ( pObjAbcRepr->pData ) + pObjAbcRepr = pObjAbcRepr->pData; + // add the new node at the end of the list + pObjAbcRepr->pData = pObjAbcThis; + } + } + + // finish the new network +// Abc_NtkFinalize( pNtk, pNtkAig ); +// Abc_AigCleanup( pNtkAig->pManFunc ); + // check correctness of the network + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkHaigUse: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Stops history AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkAig; + Vec_Ptr_t * vMembers, * vClasses; + + // check if HAIG is available + assert( Abc_NtkIsStrash(pNtk) ); + if ( pNtk->pHaig == NULL ) + { + printf( "Warning: History AIG is not available.\n" ); + return NULL; + } + // convert HOP package into AIG with choices + + // print HAIG stats +// Hop_ManPrintStats( pNtk->pHaig ); // USES DATA!!! + + // collect members of the classes and make them point to reprs + vMembers = Abc_NtkHaigCollectMembers( pNtk->pHaig ); + printf( "Collected %6d class members.\n", Vec_PtrSize(vMembers) ); + + // create classes + vClasses = Abc_NtkHaigCreateClasses( vMembers ); + printf( "Collected %6d classes. (Ave = %5.2f)\n", Vec_PtrSize(vClasses), + (float)(Vec_PtrSize(vMembers))/Vec_PtrSize(vClasses) ); + Vec_PtrFree( vMembers ); + Vec_PtrFree( vClasses ); + + // traverse in the topological order and create new AIG + pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pNtk->pHaig ); + + // free HAIG + Abc_NtkHaigStop( pNtk ); + return pNtkAig; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c index 42b8826c..d6e59328 100644 --- a/src/base/abci/abcOdc.c +++ b/src/base/abci/abcOdc.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_DC_MAX_NODES (1<<14) +#define ABC_DC_MAX_NODES (1<<15) typedef unsigned short Odc_Lit_t; @@ -416,7 +416,7 @@ void Abc_NtkDontCareWinCollectRoots( Odc_Man_t * p ) SideEffects [] - SeeAlso [] + SeeAlso [] ***********************************************************************/ int Abc_NtkDontCareWinAddMissing_rec( Odc_Man_t * p, Abc_Obj_t * pObj ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 33f336de..ad8eec6a 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -33,6 +33,8 @@ int s_MappingTime = 0; int s_MappingMem = 0; +int s_ResubTime = 0; +int s_ResynTime = 0; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -147,20 +149,27 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pTable, "\n" ); fclose( pTable ); } -*/ +*/ /* // print the statistic into a file { FILE * pTable; - pTable = fopen( "a/fpga_stats.txt", "a+" ); + pTable = fopen( "x/stats_new.txt", "a+" ); fprintf( pTable, "%s ", pNtk->pName ); - fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) ); - fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) ); +// fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) ); +// fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) ); +// fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) ); +// fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) ); +// fprintf( pTable, "%d ", Abc_NtkGetTotalFanins(pNtk) ); +// fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) ); // fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) ); -// fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) ); + fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) ); +// fprintf( pTable, "%.2f", (float)(s_ResynTime)/(float)(CLOCKS_PER_SEC) ); fprintf( pTable, "\n" ); fclose( pTable ); + + s_ResynTime = 0; } */ diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 1938db7c..243548fa 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -118,6 +118,7 @@ extern void Abc_NtkDontCareClear( void * p ); extern void Abc_NtkDontCareFree( void * p ); extern int Abc_NtkDontCareCompute( void * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth ); +extern int s_ResubTime; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -261,6 +262,7 @@ pManRes->timeTotal = clock() - clkStart; printf( "Abc_NtkRefactor: The network check has failed.\n" ); return 0; } +s_ResubTime = clock() - clkStart; return 1; } diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 45fc9089..00a94bec 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) // restrash the nodes (assuming a topological order of the old network) Abc_NtkForEachNode( pNtk, pObj, i ) pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - //l finalize the network + // finalize the network Abc_NtkFinalize( pNtk, pNtkAig ); // print warning about self-feed latches // if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 05bd021d..b7a7d4b9 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -603,10 +603,14 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode Abc_NtkForEachCi( pNtk1, pNode, i ) pNode->pCopy = (void*)i; // print the model - Vec_PtrForEachEntry( vNodes, pNode, i ) + pNode = Vec_PtrEntry( vNodes, 0 ); + if ( Abc_ObjIsCi(pNode) ) { - assert( Abc_ObjIsCi(pNode) ); - printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + assert( Abc_ObjIsCi(pNode) ); + printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] ); + } } printf( "\n" ); Vec_PtrFree( vNodes ); diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 3bec3840..71a47ec0 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcFraig.c \ src/base/abci/abcFxu.c \ src/base/abci/abcGen.c \ + src/base/abci/abcHaig.c \ src/base/abci/abcIf.c \ src/base/abci/abcIvy.c \ src/base/abci/abcLut.c \ diff --git a/src/base/io/io.c b/src/base/io/io.c index 68b2dbd2..cc907eb2 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -877,6 +877,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pFile; int fCheck; int c; + extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ); fCheck = 1; Extra_UtilGetoptReset(); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index bd01f914..2730ba69 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -86,7 +86,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Vec_Str_t * vString; unsigned uTruth[8]; char * pType, ** ppNames, * pString; - int iLine, nNames; + int iLine, nNames, nDigits, fLutsPresent = 0; // allocate the empty network pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) ); @@ -122,6 +122,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) } else if ( strcmp(pType, "LUT") == 0 ) { + fLutsPresent = 1; ppNames = (char **)vTokens->pArray + 3; nNames = vTokens->nSize - 3; // check the number of inputs @@ -142,6 +143,18 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) return NULL; } pString += 2; + // pad the string with zero's if needed + nDigits = (1 << nNames) / 4; + if ( nDigits == 0 ) + nDigits = 1; + if ( strlen(pString) < (unsigned)nDigits ) + { + Vec_StrFill( vString, nDigits - strlen(pString), '0' ); + Vec_StrPrintStr( vString, pString ); + Vec_StrPush( vString, 0 ); + pString = Vec_StrArray( vString ); + } + // read the hex number from the string if ( !Extra_ReadHexadecimal( uTruth, pString, nNames ) ) { printf( "%s: Reading hexadecimal number (%s) has failed.\n", Extra_FileReaderGetFileName(p), pString ); @@ -229,6 +242,23 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) // Io_ReadCreateConst( pNtk, "gnd", 0 ); Abc_NtkFinalizeRead( pNtk ); + + // if LUTs are present, collapse the truth tables into cubes + if ( fLutsPresent ) + { + if ( !Abc_NtkToBdd(pNtk) ) + { + printf( "Io_ReadBenchNetwork(): Converting to BDD has failed.\n" ); + Abc_NtkDelete( pNtk ); + return NULL; + } + if ( !Abc_NtkToSop(pNtk, 0) ) + { + printf( "Io_ReadBenchNetwork(): Converting to SOP has failed.\n" ); + Abc_NtkDelete( pNtk ); + return NULL; + } + } return pNtk; } diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index dc72c591..18578cbb 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -212,6 +212,8 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) Abc_NtkIsAcyclicHierarchy( pNtk ); //Io_WriteBlifMv( pNtk, "_temp_.mv" ); + if ( pNtk->pSpec == NULL ) + pNtk->pSpec = Extra_UtilStrsav( pFileName ); return pNtk; } diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index 3bbbe851..cc9e569a 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -318,7 +318,7 @@ Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName ) Abc_Obj_t * pObj; if ( pObj = Abc_NtkFindNet(pNtk, pName) ) return pObj; - if ( !strcmp( pName, "1\'b0" ) ) + if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) ) return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); if ( !strcmp( pName, "1\'b1" ) ) return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); @@ -749,18 +749,20 @@ int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord ) Vec_PtrClear( pMan->vNames ); for ( i = 0; i < nBits; i++ ) { - if ( pWord[i] != '0' && pWord[i] != '1' ) - { - sprintf( pMan->sError, "Having problem parsing the binary constant." ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') ); + if ( pWord[i] != '0' && pWord[i] != '1' && pWord[i] != 'x' ) + { + sprintf( pMan->sError, "Having problem parsing the binary constant." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + if ( pWord[i] == 'x' ) + Vec_PtrPush( pMan->vNames, (void *)0 ); + else + Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') ); } return 1; } - /**Function************************************************************* Synopsis [Parses one directive.] @@ -1100,7 +1102,7 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) return 0; } - // set individual bits of the constant + // get individual bits of the constant if ( !Ver_ParseConstant( pMan, pWord ) ) return 0; // check that the constant has the same size @@ -1206,7 +1208,11 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) else { // parse the formula - if ( fReduction ) + if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") || !strcmp(pEquation, "1\'bx") ) + pFunc = Hop_ManConst0(pNtk->pManFunc); + else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") ) + pFunc = Hop_ManConst1(pNtk->pManFunc); + else if ( fReduction ) pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); else pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip Binary files differindex 481f7e6a..45574008 100644 --- a/src/base/ver/verCore.zip +++ b/src/base/ver/verCore.zip diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 60ddcbe1..c36642bc 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -24,6 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern int s_MappingTime; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -133,6 +135,7 @@ int If_ManPerformMappingComb( If_Man_t * p ) PRT( "Total time", clock() - clkTotal ); } // printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) ); + s_MappingTime = clock() - clkTotal; return 1; } diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c index e6528233..8d1de8c1 100644 --- a/src/map/if/ifSeq.c +++ b/src/map/if/ifSeq.c @@ -24,6 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern int s_MappingTime; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -186,15 +188,20 @@ int If_ManBinarySearchPeriod( If_Man_t * p ) p->nAttempts++; - // set LValues of of PIs to be 0 and other nodes to be -infinity - // LValues of the PIs are already set to 0 - // undo any previous mapping, except for CIs + // reset initial LValues (PIs to 0; others to -inf) If_ManForEachObj( p, pObj, i ) { if ( If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) ) + { If_ObjSetLValue( pObj, (float)0.0 ); + If_ObjSetArrTime( pObj, (float)0.0 ); + } else + { If_ObjSetLValue( pObj, (float)-IF_INFINITY ); + If_ObjSetArrTime( pObj, (float)-IF_INFINITY ); + } + // undo any previous mapping, except for CIs if ( If_ObjIsAnd(pObj) ) If_ObjCutBest(pObj)->nLeaves = 0; } @@ -368,6 +375,18 @@ int If_ManPerformMappingSeq( If_Man_t * p ) } if ( p->pPars->fVerbose ) { +/* + { + FILE * pTable; + pTable = fopen( "iscas/stats_new.txt", "a+" ); +// fprintf( pTable, "%s ", pNtk->pName ); + fprintf( pTable, "%d ", p->Period ); + // fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) ); +// fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) ); +// fprintf( pTable, "\n" ); + fclose( pTable ); + } +*/ printf( "The best clock period is %3d. ", p->Period ); PRT( "Sequential time", clock() - clkTotal ); } @@ -375,6 +394,7 @@ int If_ManPerformMappingSeq( If_Man_t * p ) // postprocess it using combinational mapping If_ManPerformMappingSeqPost( p ); + s_MappingTime = clock() - clkTotal; return 1; } diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c index 4fdb4d31..f4ffa4c1 100644 --- a/src/map/if/ifUtil.c +++ b/src/map/if/ifUtil.c @@ -143,7 +143,7 @@ float If_ManDelayMax( If_Man_t * p, int fSeq ) void If_ManComputeRequired( If_Man_t * p ) { If_Obj_t * pObj; - int i; + int i, Counter; // compute area, clean required times, collect nodes used in the mapping p->nNets = 0; @@ -154,13 +154,19 @@ void If_ManComputeRequired( If_Man_t * p ) { assert( !p->pPars->fAreaOnly ); // make sure that the required time hold + Counter = 0; If_ManForEachCo( p, pObj, i ) { if ( If_ObjArrTime(If_ObjFanin0(pObj)) > p->pPars->pTimesReq[i] + p->fEpsilon ) - printf( "Required times are violated for output %d (arr = %d; req = %d).\n", - i, (int)If_ObjArrTime(If_ObjFanin0(pObj)), (int)p->pPars->pTimesReq[i] ); + { + Counter++; +// printf( "Required times are violated for output %d (arr = %d; req = %d).\n", +// i, (int)If_ObjArrTime(If_ObjFanin0(pObj)), (int)p->pPars->pTimesReq[i] ); + } If_ObjFanin0(pObj)->Required = p->pPars->pTimesReq[i]; } + if ( Counter ) + printf( "Required times are violated for %d outputs.\n", Counter ); } else { diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c index e2f0bcd4..6b130e7e 100644 --- a/src/misc/extra/extraUtilFile.c +++ b/src/misc/extra/extraUtilFile.c @@ -330,6 +330,8 @@ int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars ) Sign[k] = 0; // read the number from the string nDigits = (1 << nVars) / 4; + if ( nDigits == 0 ) + nDigits = 1; for ( k = 0; k < nDigits; k++ ) { c = nDigits-1-k; diff --git a/src/opt/res/res.h b/src/opt/res/res.h index 3c963e99..3c3431bf 100644 --- a/src/opt/res/res.h +++ b/src/opt/res/res.h @@ -42,6 +42,7 @@ struct Res_Par_t_ { // general parameters int nWindow; // window size + int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis int nSimWords; // the number of simulation words int nCands; // the number of candidates to try int fArea; // performs optimization for area diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index ad99829a..1d0711f6 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -73,6 +73,8 @@ struct Res_Man_t_ extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); +extern int s_ResynTime; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -185,13 +187,14 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars ) Kit_Graph_t * pGraph; Vec_Ptr_t * vFanins; unsigned * puTruth; - int i, k, RetValue, nNodesOld, nFanins; + int i, k, RetValue, nNodesOld, nFanins, nFaninsMax; int clk, clkTotal = clock(); // start the manager p = Res_ManAlloc( pPars ); p->nTotalNets = Abc_NtkGetTotalFanins(pNtk); p->nTotalNodes = Abc_NtkNodeNum(pNtk); + nFaninsMax = Abc_NtkGetFaninMax(pNtk); // perform the network sweep Abc_NtkSweep( pNtk, 0 ); @@ -236,10 +239,10 @@ p->timeWin += clock() - clk; Vec_PtrSize(p->pWin->vNodes), Vec_PtrSize(p->pWin->vRoots) ); } - + // collect the divisors clk = clock(); - Res_WinDivisors( p->pWin, pObj->Level + 2 ); //- 1 ); + Res_WinDivisors( p->pWin, pObj->Level + pPars->nGrowthLevel - 1 ); p->timeDiv += clock() - clk; p->nWins++; @@ -291,9 +294,9 @@ p->timeSim += clock() - clk; // find resub candidates for the node clk = clock(); if ( p->pPars->fArea ) - RetValue = Res_FilterCandidatesArea( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW ); + RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 ); else - RetValue = Res_FilterCandidatesNets( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW ); + RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 ); p->timeCand += clock() - clk; p->nCandSets += RetValue; if ( RetValue == 0 ) @@ -367,6 +370,7 @@ p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim; p->timeTotal = clock() - clkTotal; Res_ManFree( p ); +s_ResynTime += clock() - clkTotal; // check the resulting network if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c index 38294428..cc75b90f 100644 --- a/src/opt/res/resDivs.c +++ b/src/opt/res/resDivs.c @@ -124,6 +124,13 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) p->nDivsPlus++; } } +/* + printf( "Node level = %d. ", Abc_ObjLevel(p->pNode) ); + Vec_PtrForEachEntryStart( p->vDivs, pObj, k, Vec_PtrSize(p->vDivs)-p->nDivsPlus ) + printf( "%d ", Abc_ObjLevel(pObj) ); + printf( "\n" ); +*/ +//printf( "%d ", p->nDivsPlus ); } /**Function************************************************************* diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c index afbbbe42..f2ca41d3 100644 --- a/src/opt/res/resFilter.c +++ b/src/opt/res/resFilter.c @@ -41,13 +41,13 @@ static int Res_FilterCriticalFanin( Abc_Obj_t * pNode ); SideEffects [] SeeAlso [] - + ***********************************************************************/ -int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW ) +int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea ) { - Abc_Obj_t * pFanin, * pFanin2; - unsigned * pInfo; - int Counter, RetValue, i, k; + Abc_Obj_t * pFanin, * pFanin2, * pFaninTemp; + unsigned * pInfo, * pInfoDiv, * pInfoDiv2; + int Counter, RetValue, i, i2, d, d2, iDiv, iDiv2, k; // check that the info the node is one pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); @@ -67,37 +67,159 @@ int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pS return 0; } - // try removing fanins + // try removing each fanin // printf( "Fanins: " ); Counter = 0; Vec_VecClear( vResubs ); Vec_VecClear( vResubsW ); Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) { + if ( fArea && Abc_ObjFanoutNum(pFanin) > 1 ) + continue; + // get simulation info without this fanin pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); if ( RetValue ) { // printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id ); + // collect the nodes + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); + Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) + { + if ( k != i ) + { + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); + Vec_VecPush( vResubsW, Counter, pFaninTemp ); + } + } + Counter++; + if ( Counter == Vec_VecSize(vResubs) ) + return Counter; + } + } + // try replacing each critical fanin by a non-critical fanin + Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) + { + if ( Abc_ObjFanoutNum(pFanin) > 1 ) + continue; + // get simulation info without this fanin + pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); + // go over the set of divisors + for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) + { + pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); + iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); + if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) + continue; // collect the nodes Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); - Abc_ObjForEachFanin( pWin->pNode, pFanin2, k ) + // collect the remaning fanins and the divisor + Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) { if ( k != i ) { Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); - Vec_VecPush( vResubsW, Counter, pFanin2 ); + Vec_VecPush( vResubsW, Counter, pFaninTemp ); } } + // collect the divisor + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); Counter++; + if ( Counter == Vec_VecSize(vResubs) ) + return Counter; + } + } + + // consider the case when two fanins can be added instead of one + if ( Abc_ObjFaninNum(pWin->pNode) < nFaninsMax ) + { + // try to replace each critical fanin by two non-critical fanins + Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) + { + if ( Abc_ObjFanoutNum(pFanin) > 1 ) + continue; + // get simulation info without this fanin + pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) ); + // go over the set of divisors + for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) + { + pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); + iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); + // go through the second divisor + for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ ) + { + pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 ); + iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2); + if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) ) + continue; + // collect the nodes + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); + // collect the remaning fanins and the divisor + Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) + { + if ( k != i ) + { + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); + Vec_VecPush( vResubsW, Counter, pFaninTemp ); + } + } + // collect the divisor + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) ); + Counter++; + if ( Counter == Vec_VecSize(vResubs) ) + return Counter; + } + } + } + } + + // try to replace two nets by one + if ( !fArea ) + { + Abc_ObjForEachFanin( pWin->pNode, pFanin, i ) + { + for ( i2 = i + 1; i2 < Abc_ObjFaninNum(pWin->pNode); i2++ ) + { + pFanin2 = Abc_ObjFanin(pWin->pNode, i2); + // get simulation info without these fanins + pInfo = Res_FilterCollectFaninInfo( pWin, pSim, (~(1 << i)) & (~(1 << i2)) ); + // go over the set of divisors + for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) + { + pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); + iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); + if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) + continue; + // collect the nodes + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); + // collect the remaning fanins and the divisor + Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k ) + { + if ( k != i && k != i2 ) + { + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); + Vec_VecPush( vResubsW, Counter, pFaninTemp ); + } + } + // collect the divisor + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); + Counter++; + if ( Counter == Vec_VecSize(vResubs) ) + return Counter; + } + } } - if ( Counter == Vec_VecSize(vResubs) ) - break; -// printf( "%d", RetValue ); } -// printf( "\n\n" ); return Counter; } @@ -106,18 +228,18 @@ int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pS Synopsis [Finds sets of feasible candidates.] - Description [] + Description [This procedure is a special case of the above.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW ) +int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax ) { Abc_Obj_t * pFanin; - unsigned * pInfo, * pInfo2; - int Counter, RetValue, i, k, iBest; + unsigned * pInfo, * pInfoDiv, * pInfoDiv2; + int Counter, RetValue, d, d2, k, iDiv, iDiv2, iBest; // check that the info the node is one pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); @@ -170,11 +292,14 @@ int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pS } // go through the divisors - for ( i = Abc_ObjFaninNum(pWin->pNode) + 2; i < Abc_NtkPoNum(pAig); i++ ) + for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) { - pInfo2 = Vec_PtrEntry( pSim->vOuts, i ); - if ( !Abc_InfoIsOrOne( pInfo, pInfo2, pSim->nWordsOut ) ) + pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); + iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); + if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) ) continue; +//if ( Abc_ObjLevel(pWin->pNode) <= Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) ) +// printf( "Node level = %d. Divisor level = %d.\n", Abc_ObjLevel(pWin->pNode), Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) ); // collect the nodes Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); @@ -188,13 +313,55 @@ int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pS } } // collect the divisor - Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,i) ); - Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, i-2-Abc_ObjFaninNum(pWin->pNode)) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); Counter++; if ( Counter == Vec_VecSize(vResubs) ) break; } + + if ( Counter > 0 || Abc_ObjFaninNum(pWin->pNode) >= nFaninsMax ) + return Counter; + + // try to find the node pairs + for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ ) + { + pInfoDiv = Vec_PtrEntry( pSim->vOuts, d ); + iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2); + // go through the second divisor + for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ ) + { + pInfoDiv2 = Vec_PtrEntry( pSim->vOuts, d2 ); + iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2); + + if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) ) + continue; + // collect the nodes + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) ); + // collect the remaning fanins and the divisor + Abc_ObjForEachFanin( pWin->pNode, pFanin, k ) + { + if ( k != iBest ) + { + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) ); + Vec_VecPush( vResubsW, Counter, pFanin ); + } + } + // collect the divisor + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) ); + Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) ); + Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) ); + Counter++; + + if ( Counter == Vec_VecSize(vResubs) ) + break; + } + if ( Counter == Vec_VecSize(vResubs) ) + break; + } return Counter; } diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h index 10e312b3..5aae46cc 100644 --- a/src/opt/res/resInt.h +++ b/src/opt/res/resInt.h @@ -105,8 +105,8 @@ extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ); extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit ); extern int Res_WinVisitMffc( Abc_Obj_t * pNode ); /*=== resFilter.c ==========================================================*/ -extern int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW ); -extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW ); +extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea ); +extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax ); /*=== resSat.c ==========================================================*/ extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ); extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet ); |