From 2696cf05e568f7a928f32b01534d106bf626ef8a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 13 Mar 2007 08:01:00 -0700 Subject: [PATCH] Version abc70313 --- abc.dsp | 4 + abc.rc | 26 +- src/aig/hop/hop.h | 14 +- src/aig/hop/hopMan.c | 1 + src/aig/hop/hopObj.c | 48 +++- src/base/abc/abc.h | 12 +- src/base/abc/abcAig.c | 9 + src/base/abc/abcFunc.c | 2 +- src/base/abc/abcHie.c | 2 +- src/base/abc/abcNames.c | 6 +- src/base/abc/abcNtk.c | 3 + src/base/abc/abcObj.c | 3 + src/base/abc/abcUtil.c | 7 +- src/base/abci/abc.c | 244 ++++++++++++++-- src/base/abci/abcBalance.c | 7 + src/base/abci/abcGen.c | 144 ++++++++++ src/base/abci/abcHaig.c | 506 +++++++++++++++++++++++++++++++++ src/base/abci/abcOdc.c | 4 +- src/base/abci/abcPrint.c | 19 +- src/base/abci/abcResub.c | 2 + src/base/abci/abcStrash.c | 2 +- src/base/abci/abcVerify.c | 10 +- src/base/abci/module.make | 1 + src/base/io/io.c | 1 + src/base/io/ioReadBench.c | 32 ++- src/base/io/ioReadBlifMv.c | 2 + src/base/ver/verCore.c | 28 +- src/base/ver/verCore.zip | Bin 13275 -> 14163 bytes src/map/if/ifCore.c | 3 + src/map/if/ifSeq.c | 26 +- src/map/if/ifUtil.c | 12 +- src/misc/extra/extraUtilFile.c | 2 + src/opt/res/res.h | 1 + src/opt/res/resCore.c | 14 +- src/opt/res/resDivs.c | 7 + src/opt/res/resFilter.c | 211 ++++++++++++-- src/opt/res/resInt.h | 4 +- 37 files changed, 1320 insertions(+), 99 deletions(-) create mode 100644 src/base/abci/abcHaig.c diff --git a/abc.dsp b/abc.dsp index ca5ad3008..ed7ae4e4e 100644 --- a/abc.dsp +++ b/abc.dsp @@ -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 diff --git a/abc.rc b/abc.rc index c0ef46f3b..33bc0c96a 100644 --- a/abc.rc +++ b/abc.rc @@ -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 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 ce4cdfde2..341245992 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 18b8618b3..4fa52fbd8 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 037203fb0..c4430abdc 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 063f8b154..3a2789276 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 287e44215..1d09548b3 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 f1101f19e..03f41f3b8 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 9e9d921ba..56333a366 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 a649fe431..91964dfac 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 e0773e3f5..bed5d399c 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 02d13963f..6167979c8 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 5f82b4b59..965e611e2 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 fbe81f483..4aa137338 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 ] [-S ] [-avwh]\n" ); - fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" ); - fprintf( pErr, "\t-W : 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 ] [-L ] [-C ] [-S ] [-avwh]\n" ); + fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" ); + fprintf( pErr, "\t-W : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); + fprintf( pErr, "\t-L : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-C : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands ); fprintf( pErr, "\t-S : 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] \n" ); + fprintf( pErr, "usage: gen [-N] [-asmfvh] \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 : output file name\n"); @@ -7487,6 +7532,158 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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 [] @@ -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 819974bf8..f55dc4352 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 5d74bda52..bfb413745 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 000000000..87fada223 --- /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 42b8826c7..d6e59328e 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 33f336dec..ad8eec6ab 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 1938db7cf..243548fab 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 45fc90896..00a94bec0 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 05bd021dc..b7a7d4b97 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 3bec3840e..71a47ec0a 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 68b2dbd20..cc907eb2e 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 bd01f9140..2730ba69b 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 dc72c5918..18578cbb0 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 3bbbe8515..cc9e569a8 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 index 481f7e6a7f2895f4f48b737d17b2ea9e25651234..45574008d7ff10e1920265551f2622903f2d8d5d 100644 GIT binary patch literal 14163 zcmV-ZH>}7|O9KQH00ICA0O?F-HjtR2YTq^h07ZBK00{s90Cr_^LvM0rE@SO|Yg61v zvgr4TnExPikB4r%!9eWUyK9Eo3mAKe#lW%g?nKxQhv-&=hHj~kqy}?6>~BArSr64q zQmN@~<2m+j#L!Zy9$8uW&a7uop6tJjN70je{`>KVAAbk}?CCfhM*;kMe;sA}X%?;b zKeCr^Z}TD=v)Au;_x7I$N9je}5AxfjxQy~R55i;+z*q4w?uSL3Ch!VBS?3*`hW)GX zf(`KgpU`fUUIddc%cE>vj*+Aj>Oe%Zf_lB@J1HlRksVLXc26yLww5B8$$DjG$%ypI=Q5e57o z&T~E3T;Es^-WFk2M1x=r2DzB#MX>qTUa+;X@nn^#34)S&rl2;PWK-59;a3eEvPdzWz^~^heV{6s*8p)-PAoC*wFZ zpM-HjkAD2&*_{4SPeH}M7YF-CyKi>S4o{BX2DSf0Pji|R_7xPjlZepin&V;~UnJou z|M3TWGl+&kluXCL7s8n!_~*f!Pj3%jeL6llJ_vS#jh_Da@c8uInepu8-I@LH@c6`f z_U7P~@#J5JZw`L^;STZp(_5O?8BFR^v0XL!3&7gCslVDiJNUGF{KA+zJwAD3KKa#t zwD<0%`REw>vz|FRb38jfITOo!1v6I`mltp{`}F2@n0zXNC-gT_13H79pnn-=@OUEV zRWH~*?|(Xq&#CnUJA@xWcU$&$oyG&Tn{?9AMwnDLewjrPkc80tgTthVGT5-158|W< z$`4+rgXt*pZqCrbXwE=zTwJlA@JG+WodAB|U)5djj&8!+ys_)*4i1yJh&?7(Gld+F z;XOLQ-3L5L24OZZx`98c;8Y@EApWc$!UO)Vv9h|$z4Wu+WX&h=VRf(jX_7?! zqNekc^WWH$+J1J6BJ5v6lPI@4qR-@qYNzEqvItgx8h0EE5{H@O0%Znu9i?;X=qN1u zmz@eIOVAug#nGYT*@@>Uhsm|i7&;tvn(`(Zr`OTjDM&7#&%$$yT3FiNdqnBY4Cp132=d)rj(rF>zY~!qc z`~hcjF-kuTUxyQ5oX8xv17xq4AcVsI&%?nZY$w<%lRRnid(&hvg0uaJ_?q&7aKdi( z;}2gL59D|%{}GH|rr9_gZIh@2qenr4fCv7Le-G(pkVFONqEY|TX^|0}@ZU9HPreHh zvDU*iKow+R=p&?8_E|d{{5>&0pAi z^5o?->7&3u2Q5icQb-~(w3ruB-p}F*(=R@P$r`~OGjup?V`WxEN` z9I1xxl#^0kzlp*@ggV|1lW+$OF}&!AemT$)f9@83M$^f|KcXHgiadc5sZX=?B8&1|MdyRh zMHYS%Z}!5B^`$r8E{`%hK&a+u2c>L6cq`va+PO1wTJ}-6JV$xPKY-ulV2ZK-G-KBr4X@a;-ads!IZt6T?Fa!(dpF zf0M5$6Vz04PA`PWMPx{k!ITy>`GB=xKa`i{YIc;RsZ?JT?D+ZkQf}_w(+RGe4u?j* z;349kn5sqI`1@c-yqciAvS;@S1%BhjTjOQl22wJIe4Dxz%Su z`vb(z+#Z9hlw%7jEPG!xE&eu6pO-;LKS-udwXF&Jle6?HlE?{%G2UjYU?`JCCDx47 zK{P^B9&I!XqSEah7j>u8#$=S9LeXDE1w#8R$XXrV4yT?Xmi$%%_(+C z9lZvihZn9zmd8nXc&EWr+vKSr4syAVOp73n(KR8Zjluh`V)+L4Na|~06{jHzMy7py zGhikI5-vfJ<-g9+5Tp>=M{YwA1CcFhs{{3!_D?{eZfU4K(t2IGNV5az`5-B>Te&bn zlCK%O@*cOW#BOvR#-Ews93~f|IJqE&xNN~s@XHvEI-D6iE1lBTsPsd#;|HU-NwX_d z&|xJRVp0NNGcliL%emQ4KLwBYNc2D*rUt8dA7|<0D7ubDuw|Ruet3VT%#+RhGR%Wv z2q%9)6BjQZ=j$sBf~DPOLFeJ_JEL(ino3uLE%lA7%QD)Jb zL->=^5sDCtf-ys*fVm>^YzhI28N!e#km)d)j?cfL9d#U(s;xztmRc%jTWoiE?z_Ue zr$7S@mB`vIfQu;{dMF8kux0=?c$`0ngZ?4GldhOr=ocdy5=WvDFe~B(D6rUjbrTnt z=2RL-4?5KP@t`Z`VGufPR+=<(1YaK0Fr89Q?YgFp#2yX+r}jl?NWtYflRD>uX;CuB zHHLA1%MHAlu;_&F?j|@Nfo2SRP&9nt8mbU@6%92RoMg zzpZsD7`IRp-WBl(jt{7p9b9(Ut!qhkGj{0$)6Qh$yQf*^2d}Z^)>iNcs z^NcAYDP*I=S0KM^?0$3R?l)IVH038@(Kx!FCf89`=x933(lOJ81YV-&5iJHOAnYIp zbju>(#%U5gU`!SMT@izT>#X4hHtLeOvb5Z(!f&-fk7<)QmII6gK^4*@y#V3G$U?ru zIbgs96k-5yh>?CkGj1{I04D?CcMR-nJoa0;v`GY zN6|PK#}}7Ha8CRV&;alz;zQ+#28_Fdi8#SFo395;cFbjEpgd)V0;5|(z`v9TN zq>Hp~ zK==#>sk%A|5Z8uQxr-cxf}xfc6jTCN%v5^3L~DR~Z&fZ%upi}ZchyioN?$50bw3>w z8LoDA$T|AVk4E4P5goSMpu@rE3B^$c{ZX15xMyL8;q98&_Lm;6IGId~{8>t-zx-Ji zUBo#|A%AuggP8Fw#%RpE*$ZiTw%$z!EK*7LVHu`EV2Y;z1f#Tt}t!5l_q=`6m(!j8{j%r^(G zdC+LP6!rK;udoBCqGK_$&jvvbPd_ zXn8&zM>3U&M>qx397Ob(1?g9T@QZD`qG8&qs!eO5#6WFFTnoCphs>d=g}7p_Fja=W zHEC7VW1zy1E13b`QRogL* z?J~VP8Zt3&wQ$&&z^pg;>85VSL`*+sk7u#cf6t<9Y~VkOx;3LsF!fP7JlSd5;~U4o zv2Blv9z_<8h#9SXtu%w!T;mse$uu`>%-A`avd-PXfN~oX^D6x5% zAKcY0H=WmV)7HzC3CfKhsF|P~E*`7BvyXH}Nw+MU3Uh7|_me0ZL<1w9$dR3^5f{^H zy->UL5iv%_Z*rQFNF!zSE!3pa;Qjb{^6^_SXtR|uFxN#DF@BGq!jI&2eqR1K%GE^1 zX@VdD+9XWS`0xpR0vP**HQx!=^l&_)YQ#gf*j#FI3O9|&1tGRLdf^gE@T98>ECEU^ zjN5i=`j?aLu(rSa68xnb{1j|_9uCVUY&ooj_HK!8l|L?e9wul!&fDN;iJU%|*#iAs ztx#%4rR7t>NEFjEdiWUrybSY8-O`QC^H1Z50xq2h%LUCEyc7m?!p>h%TmaO=zqiKVus=s z67^vRFQO#MLM&eJ1f=@J@Fe~tx+NKJ#-pL-B*0(*&G1Hn^q_8e2ylXHxtyQG-37f}IX5(a2+|R$PS7CF z-f+ea#~~Kl=~Jb!0_8O&14bz(qqrzU6uvOuKVcsMLFIp;XYu)}@!;dC#y{}+)2Hg` zdLlLBjTwE^!Y_HAfr15#B_jx69%cm0*B|Maw6Q=g3n6f~YvQWJwkiEQU)2WZ9aU|Q zxkV1&Y}v4O$MpHzn^d<^?b9UNZrGf|eJWu8an*L>N&wu|i5ya{P|gh-UP#B{Fsnyd ziq#69NI6H5fdsqG`2t`AP0Q7wP0(Ty?P|jjDD`IsppiRVd{aA zo8Ny|e!pL>^8qk9h_~h9`AoE0#4jmFpW_>)QSe|Q%g{VOx^1slS%Iyi6aB@Ho^Gl` z@P0HBW2h(w+0Y>G;Lbd#iG{epQM?XE23>GWMdbhnd!IYP{NWMA-l+yTs&ckB=MI$0@D67Jo;;iMAU=C43#&i2brp3 zWhO{b6|Z6#LMxjcl$d8?UFMCQE#S5w$;C+S;a{+)ZJ zJA4hAkB-Ckbedo4pzQ@6GBZ8tZYaZ9adRHucf<_V0MMlm?W?97lx1nE=sK@fP6Rz1 z49cJaqUX#HeZ;6d5c~B9EBX7^Xm;1K)=HUq9*rSY=_nR9V8y`hhLQn7$ryZvk zz=7=rNAVc{BbbX&4-H3Ao4QKN30H6wu;Hon8KqTrn+u#&o?jD-L-Q6(`)p_jp z=)N&Dp0+XtIj}GU4`(8eA^9^Z4zS@6Rf5xc3Sq4pMesMq$e#Jz4T7dYh8()cXJV~K&rfcjnAcu;eCYZthL$YVZ-0SN5_V8-c9FbkayuE}7Dj+|&YT&4aZwx4)iAzH)iFv^eQ3dLg}QN$Hb?a299aYsy>86S5} z&2mUl!R3u1EQ=s2%nX8BDU!#X<5xBiW~jQ06JyCaC6*GDuq+_oJWS#g^$dBr*{<7@ zumF#<>gM_HX*i0D+dxmun1!{YY3^rIo0SJUtMdS+Q4K@_Q?lxxcaT@_EDwaHc=EF) zo-~uyWhIM{Vjh8vH82!&#@gDF?yVN-;Z{9EBx8W~u;R&x_R?*J*%G|%-*xyy?7Zoy zZ#}hbFV=_31y&+K2wQmRn*K9!Q=P44kR8g%ucta&OCUSSwJsyPlg#15&~7YKHltTw z9;S4t1xLl!s`0e~^*qu3Hxu zqA#R_NGJ?#^@RgqsR+V{qcVIKpTCRG-a~pqnt>2xwwCP` z$5|;qYa>XPvDJ73M?Qi1U>JiTN6A!Z?UGP9o!xmvN=v~FxrTBJpE$1+w6*w-GmuwPs3=k{DR7E3c>h2(7&1+NH{9Vx|u zZPkT}OXwj&EQY%m4Bte9X|WP~2t_)(`j%F8N+mShDrAy1s#mhla4$+=luXs(yLv)U%!;@;|jHqRQR zU?x857p-MLPHgd4)z_sd8(D7-6lD-$CFF|9v7^w@;_=l0=M52$-@VV?+9Bh7d-(z7 zp$#8a9_JrcP-;Jqlo{jJ)&!r-d2gM&3s8)&;{hNXOWfczt`4S-%n7X`*ettRT!uQP z(e;6(`XS}To80Fgl10m59X*marz;nkvIy?`;K!M|B3wk!c|7PM_Li5dNM6Zsg`x8)G|Z~ zYb{MjVFM*-=>@HM{duMFxFV=vH#o7-?>zLQ68H0;*3DvrI&0gupqV;(cxlQ= zP&wuI^F_f$d>ti$=|HJ9ZFKAlHDr6d9U?43^c5QSd$!h>ndFh6qaAP26o#s5;~6uU zRhk2zZD|ES{On_;!wXZ{9l?59fwK;5X}8W~w)G^gFw)>S!A{Whv03d<>wuR}t5RpH zqj#J}rzREEc?s!PHybG-=8yAAg|%+_U)O#_4s_QI!!q zWO%i@1u!FC7+$l0VG4?M6#(*i z>d^k)JtFztG)%K{I|^=hO+%)6l@e|8!XsmSc1W#>+mW1=*EEs0Y=VyNe0O|u)0O=YBdrV zN{t=OM~tcOCWDS;N2$Q;u2RvzW?m<6Y7WjDuUVaB^PbeNHM9EFcUlLZ)45NqfzB*! z6RT%*T#HyuaGZTD$7#{gpMQnxg1&VX(@(WTYd^MTkJxRoQme$5r*TrggCE=XQaE=( z7YIjRUG2OmlYR;NH>v!)%X#U+V$PJ|@mtsc9_`8;R_nn#IQJh`vS4k@0%3_8ac>rP zfX!F$laQOzo$(rk3OtX-J&P@r@6Bd~+m&LDwLe8>+ax9NCKrKFr-%8o(-RqgTgnOx z%1Hmp1_4|8a2o>3!-+?V#RK54#mH_T9A(7}%D>ACfU}&-Scp?44it-sd^0M-`?P2A?IFTC_Qg!z;X! zFN?}pcx5s|m7r*N9vP32Ts3!21>+$hl>p?$(!nm(9(Px6dFgDJ?>n+XDRfp97D-9(m+^W9gRY7FEog zvCIEvq07&nD1~zN@pJTDYoXi!UbW`STUMh0YXAc7z!Ajl4$0&#*^OdFZaXfM8<*>t}vC&eibH{vhca<608DCPJ) z199jsgE&-~mmdIepi=E3p=ut&h=;#JXwbszK@lEglbqH6!4Xk*g-iLy93o3~iF~7& z>$^+U_oz%%BsVlQA@o4IQs}945lAtgfTm`kr)3;_YEs0?fYKjlJ#0d+BFCv$6REKCCM?)6Qs& z&Gx2PZ-X^se{X9y!O@#*_9m}2Hg5+NHEZgP&$93)3Anvr$n?g;{1pbzs@AOwX<=3L z#Pjs?Vr-aZxK4;eiO^mQeU$o%(|WhZE$0muJhr7eTv^>AK6frYFrXP3)y!f~QHA=I zcLFAhvaBK`ycA14$I7b0wuGpwz{5Cd*hU4mml4Ceqfy%L1e<@h_HjR*+@gM`Abr<3 zEe#gb5c@7O;i>vfN43g54ZH-@R>rf?e# zI|!~;*KoXZMSWAj@h4+1l{^{&f}Wh5CGpH=Io7Fz5sPi0``dn)2z=jZvMXC1I}@cn zZPv3TD^{GXb)S>8taQZ&EA}!f_EcAKa?Hhz?aaRMu82plnecf>F$7rM*IV`4TJ~l` zjS5xBn+|jSVI$F!Go)KoTd1n#P3_yIDp#+9F}nUIlcmK1fwi?5ZaII&xZQK91)WH*1q( zSb1-xFJ8<@WBln%Ev<1Gim41JiMFsqq13+cD$b~G5{@z%fJAqzEz)^fmD^DFbki?^ z#;Q58Q3WyEJmf4W=q~tW4`p6!F3YI30M6`X#5{A8xmi+H-YT!5uK+&f(p|A!x~sZe zI(Ur*sT}Ea9=YHR*7%0vM?4+&@c?)R<=b_%oH;FJ?y4(_JaubxyuBO%H5KYwcm!I& z$$rAU;gh&H$6c@HG5NusxN-yJf)VYv3r(!aZB$pp2s2~`#q>OOLj z;Qjb{^0DUF*AUo`-c^%q)V4_y5#`S-e)K2X=|oHJL!pv$qm(VEWdm9Ccs)PLdDlk1tWYAEjysE<>I!F=)jr`H zc~NCda@zr1si}T}7xya+!i+fn;TQQxIt zqSgdAqrh+zg`fCaRORk}K*WjaRfc;f^og92|7qF&$k!Y7x72GcVb4 zs5YUe-?z*sbd|57CW2K4f9k=iu7FY$)|Ka7{Deo87 z!)K=_N`+Y739S4e>|dV79Rc{BfNZR?RI{cJHtCk(lS=fV(Q)eCFEF-4Sgnq<@5mA@|e%-{Q5f;wq3#_BSX1q*gO1x7A!up3~r6+cQFU4S| z8XhXa5h0AC#H@McNGR*GeF)D@VVgsij%i1KRfe>Xn2q?uowp{!OJ>+(SG zQPBrxTMU)xazKG$3V#M`GO>~`kBa!LaT-8tLa!pqDX&fEqT_JBiLN7nd4m(cpp#Wb zH_nxxx$PvjZhKxxN7Jmuu=c2;Aq(m$<(2@n+cQWDica-QRfWtENLP|VyPi)XC3ZWF z#4cYh1u;QL!z{zHRX|U}7E90!vKdznT_TgRFVN>TV}=^ z{dyILaNAQ?>Wr>6Ep)P!Mkyf4EH?!J+zC{YC6*NdKYIimA-+l*YGg`aS5zCZPM)r% zqy`8nFh<-=AtDWxrMpXU$oKp*2_-7gE1F*JzsU2b2s3BVHGGVlY#n@Cq zM~?ZM7m8Z^uMS6>-94(JI=_qe2vb4OE>$N&N;MIL)nmDreqoT-SyY7ux=wVVZ=O=s zyd)}<+O-wB+X~z>2-~{!q=2-Pn(p*`Xm+X5WmO7F+|PY+wN z{L*Mu&+#=5ubWZ+(EMHmeSGKk-?{yFZvXYTz1zM#)aq#}H-cpp)A0~kyW`fa`Ecol zGh>bRns*h$*IoBbn>8&Rmt3|G><)`yl%`jCFp96-TaVk0n;e!&k;tt&kMr&vaKU*n z-K%|2Qs7J`slKKLR4>P zZh5f9#T(#>$RyG51Hi`c?%@<|&%fg5H@)#L=X+W6sC1VDbp9ERrje4M z&XSz4Wc>8vlDvs@J#{*mj%uB=yx0{0Kfb_(<=5;BQCh!Bq_>Bn4UytK8@S3!zbA@4 z^|%_;NZmO|4)de1=wAxb32+%p;(8nTy5QkqzbKd>EF3H(N7F0G8@#IAipwT0t;8MVH8OyC{Aeh#{yq z({k^6w80gaV}^LtK&^f+#jPKF;UX;Q<}xlK3lJP<#jt1Tzj(8b&6)08r2)luEhXS; zG?L_5p|EsG#yFhhEc!#-Z4zfPVj_RQg#^_&Dg_~Fsqb)+%_Le2#iDQWicqRv8B*m( z$G5fMp-dszs5npYDvG&~Zabes5dtcRxj_;6%InI!&5OGjoIIa8?ln?Cwr%a|ICYyFp4+)dmNpHWQ?@RA3ky(Ve9;|8A=uKPBEZQMS-S!)92Py z&ncf`y_QxoBL3@ilzr{0txNF9)l)S}+*yk3D?)imlGExnprsS_3o(A@@jy8(>G^Mj z^dyr{;Aq3MFjrX5bBdHfBJ>S&T^CV5yxJ48FM&C+_>3s}jJx&ugbu>SATykGCC9DmDH_4=kqIU(u zkDbz)l*@_t)P`KE%-%p4y-z8|OVu6wZg7Yx(qtuZ(uYxEndLyW@`2MvT$KRPr4QLDejtnw!79>bBKXVpPlq3)hp8ROAR1C4gN7mqoz^qkRbB8Lw1);jD!@%Zb&t@iG}gtm9q435c32lnaC0)g9mN8(

iEJjFb z!XIW6AEXicsGeaNuz6CQ<&qr2NwJP!=6cFRP!>lP14+sohwG9gs>zn$MAtxnSS$Bw z+no|vWf7}bS9>{cPPF5Zn|KJFypnec72l@X-DWY3QyU$XbxOpIy^AJBw3=Lt3P}|1 zC^V>=vnbf|nlcY~530Wv1%Gh?MM#tWTxlBv|L9h zr!e!m>s6MNZd<<;REv$}-=AbgjVEW_OT}3m7s6esISUA3yrON4MJQSET`W4kX(cs*vsf0?X%Ogw8%-Q)qY;K7C@B#{b`12_3(0v_cUY9VO-z`NnW2XY z>ti_&!TGI=_1!aybv#Q-Nh)I$St*xghd}CJ%A#?49XYcq+UCms3veN7)FpoF=}hrX zD@w#D!`Fyt{6h-7{H9umz+3MSsSs@&?H1O^Krfq|BI1TI!LCopuJdiy`vjz(y?*z)>0gC;TLstm2j;c)h%`SNB?G_TLzk zNx;le7uVVStZo`P&QmN*t7knq6Nl7gS6#%Rfkuq5ZCBZ~dVEwizXt<7bCrx?7o^oy znJKTSOQJbcmrl+A9RdU08nQFyArmi|yCi|r!xS^padj&OXt3StA!x!<@&*nF3dZ&!oXs4QP#1TRzDdC%hazQ1!x& z!_PquoRrE5s<~?4iW2xb{0v|wVPLipxaMGB7y|oOl!oCAdPw&{MF7A3oox==lLN`nj{5x2x# z#!(h#mvJAEgeNCF&b9mmo-xgG4-6FVIWD5M_O3hkj5up0kJq;Tl!JEWN=C55XgqTr ztWk&$18`R?-*|Omtyjk)!(*kv>27@pL?rH8A6m^6D;b=?$A2F18KZoyPp5)&zW2wp+X@j;keVD%1Oxh2=GX7L~czm!(9FP5aKUF~4p zty1YQ5o{bZu>_Py)Qo#Fd=Azmf0#LSHI4_bMbBj$zSvGkUv^e!yYOXe4F(MVYc|?4 z#WswwVUjiUe8y#0V1*Jk>CiSf?m65+b15|@`}e$*z_BJ#p8=gKJTL)81gq3W1&HMg z?sEr$<$H;;y7Ja{6=A=wyC$8o4L`B8eYi|qekuKC%Bt5@Dr@uJFAam4U;E7H@xU=5 zEPy5_#Uw6QFfiZK2+-4Z%sR@p+?!HWkejv?tHvhTnsPN9BuUA&q4M1hX989^;+XT74vFMU%`ijCCG zy3Y!tms7y*901XGhNF_!Am<@A53xWXI}I~eTdCC$tE*LU^RFl=CM7NAkl{WbRVgmZ zeCWnuhs|3C{aCfdwWwhBR;fW(T{F?X4OM>jbFiiI9lKPTsn#1(Vom8A*E*plm$w+8w=y!cBdNPnR0r~6x#qFMcHh1a;n=;j>$h^ zG2flqavA&^%61cj{;UnwR7TP{{~1cP*SG}jaEJP|Qr3mkNPMynnxZLOft3!m&>`Bo zW7TC!0V9+6Q;oDRN-=6FZM+tvntW)lvFi3-aej8=+r`D9svlL%r#|9P|At>CDi#NlF7L|~V0dZ< z7&_zk%m6x(am+z_w=85n`J*6nx*%jenGZ4p2d}Fe)PU+IUj@}q8c{uMMD;Sp^y{KJ zhQFXa(9F;zh2|MEsX8%#?-s@Fa5@4kAz)K4*CaGkz2rfftQKp1(4N*G{3&53QO7|s zPsGuo@RagodH`n%GQTW9=P! zEz0|du(@_^5_EK;UleKalA{xon_#*we9gdtNyz%wIofyFO;BQ;W_hur6D%-xw4%+M z+P;m7!z3@P}Xl@TZBA z7|cKe2>P$kX8K{a7rdfTqQSvTWMH*^gm^xuf7DZjG5X;6MR4+xMfWxQ6FtpoPWZq7 z0Z>Z;0u%rg00ICA0O?F-HjtR2YTq^h07ZBK00{s9000000096X000000001XWpYDr da%C=KP)h{{000000RRC2Hvj+t1~&iz00845Z$kh8 literal 13275 zcmV<1GbGGVO9KQH00ICA08p)1Hf^xepJy`w0PtS{00{s90Cr_^LvM0rE@SO|Yf~FZ zvgr4TnE%k`9uJZ&FcA0d-8IAP0gSzz#lW@k?nKxQMnPh#vuM5l zk-dC-n-|fTy?(#DxBomiN-yGmkl!Z7Wt7Kx5GI2FzKVx&KP=)jfmis+I`7~#>|cc! zY=HOwfOezwBAA3(9%butj3k|4S2%%Fe3b`z1bv31U^oh|(<~3tVUQQuv|mi|Dep&g zusba-(=4EW?{`OG617QT%{ke0W}&9<5A3}`2O8~uoq=l(I~p*eY^;ZDB%Ba zp6kKp`o?KZ&v5MAvbSed2fjaX5G$ND%g}v5yUE z{%qsV&o=)OY-~KI{|6z=avTQ-pC`e8P)|?h^Y0n<^}phzKbj7rUGIJ*!{ZB{nIklc(hwvllZp+@T(|DkFlTJFu2orzfmsu16NeCN%aF`TP1{+rKL7WtU z`rvgsn2w^x%^5ma%^3)ei!1gM{^*r(Cx9RLm%r=X(M@=p*LLmi;4q1cxWVKqrjX+? zyhjJP`+z6OAj}3O9A=UWv>8-&l+LN6qp;{- zc05p)pgE3;qeI8DlZK-lCf7~IFyUy@lsC~hy^h{aL2~(g7M_==MQI!2WE3Y6Z6h{> z0T1&R(GZ>uI&K^afL(++2xCBC`NOqe1TcvSXA#I;iTL_7KAw&{yk$4|{df5y)nCA; zcfMJ{>JM{{qhekXBJc-JN}CmbeV8LY(4Rk2d*b znvKKJHpyBrdK4tM^B`d0-$QyCBvHZHc+~%NT4V$Y{C5oi%6CB|H+r~+Z3ST*`UvS2 zexC=O*KhZNA`On-?sY)~*j|pb`SRWIKFXOObG|%0KCBiw=PzwOdGd0a^ikuOgPLY& zNhA_kYSfD;?`QFZDL5b5mTCW}k9ZIr42Q5oIW?hY5eNWz$`qeDt0MCd=Oh9fq;H!& zo50c8Jvuts*C=Bz*d(fm@5j+N$5RZPdZP!T{{KYjup?V`WxELwJ*fxps7YzB-$dac zLM3yDiC6`k_wnv%l=eHSz3ea^1|9vgot@zL-O&*)M{EcuANW`eb22R^(;}c@@?rqQ zOPj)JmR@90p2NF?&qWq~5)bymj6;=u)6=H-Dk^YxZ(;2nH6df^*Esb&;A^8p&KI@` zs;b@)M(JO@Od2*knTUoU9XlGrsqGWhB*HO>PzDS}@p%?zw`5lcNi3wdMby7cQqXyB zMGFO&7wk(MjN=d^#;%P~?ct9jKGu%JH&?4y5ip8#-ucT6dP5jOV|dXK{qo&J#JpSh z;ZG+I|LiwVzKo;Iuod+#(O6%TZJICGp$aK;X6B0C3i7a59k%hU^Xf zhW!o}y5We#4}ZgT@~!mf7^T)`w7y3o;&A^m>R<7{-+`VSjY-a}yG0_Qk9$vFg;N(q5TtXC-ct;z) zL{ZII(Eb2Dv$w~h9BOPqXl3t1$+-G7pli+H4z&!sINyiX?KvVT`xgDj3RS zk;0mBI*3MShs2jRmk6&83SlJ#h7T_yb`+E7GyH)=XgEtl>gN)K7d(y~rR$2eOu*tF zl!Yt&cMc5Y%Kij&r2cp!KJ5i7W3t1ofL^D4{>AJmpJV`mA)Ch9FZn^1r5Sv?A0|m! z07`~~-~;dJ!%8rSGuZd|I$B>b=4{~gDRxO6y$0SDUbq&i@LhX&XTa0gg{e5ba=DLe zdn1m~wIOAUac69E+DFbhU`7NI%0RQ^zs}J#q*1R&ZqpH4R$27b@u|=30kjb6mWJvh z0X126njJvT2T76LitUhe?wYMJ?{N)0cB9}h{>%imhLvQv`w4)}##WjwXAwXB6g(1^1AL$lQ-O)RkF#`g6kSIn zI4hgm&2aThny~P~NMXxVW^ZQagIkq1KNFT{#bn&>6Eb%o#`Uz9`dq;}uMgqZ`d)M7%2=8gPt0$9bWPBK$LD5yBb0MmcrwR!Ni^S>$tY80gdt zo;?%Dyh2OkvV-87>@*o1Q(3rhS9x20&W#zu4{jhsx54q*-_dPwbolm+`4P~N{b}!L zcmMBuC%^WD6rgFx+eW8?aSJ=)yCNRJ@d2H!V@*(f@OBdQOR8Bo7;w1~jrYn*XK3BK z0|r?KOxY4`)lCBQ`+=MBz?FQCxKgLTs`8NOZa0I~pc`&SlZ2^n)*bcZJSSEskEE)_ zX!y$Jht>0q73Ue#M$*WJ@TAEvYrEf^x%!S`5Y!<} z(hCq?j5XvtoC5|-vM2`thZy?@G-LPhRY{v81t|fnBFoxNnNC-zam2?!{Z#Y7{WaU@ zZh75?w^J731tr(!qo(tE_te=`vkF>zH1~M8Z4M+3Iw0`K9C8M0imsu8goyhKh=Yvh z5{-@LDeM#lyy?Cn^yNom*s6Rz*q>&2Dn_?KKJ8!1zQQabxi|y{dlL=TgA01W_dB0f}(h;Tl|qn9hp;?AfAsm#HKQ)w3a@E!MS za3AL07Wes^*^wW{{Eqw!Mt%+^K_&+7v4n0Kf=*8(rv=ZRlrag1$VBsU@z5v z0&g$eT!FR{)gPK&cWTsECZw>TjSHMMU?3ti8yI!-feYMtz)V?4)Uvb zB2>l*=9LZ=2!zjIkm{?G0C8=o&&A^)6b!YDC>;e{F;nTK60HH|y;Zq5!G5&2-BnBd zP!391>V7&VGVFJD$T>EdAC15pB06lhL5G9S6N;=1`lB?raIb_JmWOIy+poM*aWa_} z`LmQvfBCa4x`=a_LjLR~1~KDVjPaQbJcp(5k9U&+i|}FONW8I3g}@X~0SHK&0lF^Z zcReLBB_GzlF*aJNDx-cY1QbhE#eaed8lee1@Sl?(7Q3#epBR%=0!nF6wgqz-l_j_| z9Ts+c4r9JKc-3@3M65ZCh`BgTha@bX%YL4?0NcQ=tw!1jHfr$FeNeLq6Ty&PD5-M! z=d$kPfbiQ8&Spl44Q-hi)%5UW^BeZ$P18|7&vV#cn~w{E{`|(>d-t;GxXE0%_qfIW zCi8^!af=%hOZ7#T#yd9L`(I=&SnGmWz0;36|j4cl~qA*Ho79fs$?wI3#C$!`tE zk*RX+2LdtL8LQ;t37Vb4Y1+f^lMYKx+ac|bM?#}khflea%>6M}g1TMih3+%MgW(yf zLnjlBRF<5|(__a~vC@@1fLMTM4| z2_;RIfnAli5`AcSJ{?Cgw}(eK1=Acv^q2*=`#|`mY`dai+N!E`YoSy@V@F&Iy1R$W zVW@?;Vy-ZG!`14vD*qU$@S{r)KrvX3pnqouvMtK|+S2rD>(<;zbDRz$k*e1Xeu14+ zNqm3@<}1G))7mcEyJH{|^HvLojSb9dgP&>Yc1*u0dREtMx+d)MAe9gY_YjiB>8Pxkqbg>arD9^ zl;BBM7gz$6SQxkMR`f3?-C=Ei`6c*sH~1;o_&gk{CTuyZh4F5QZk0bSdLAZdJkHzT zr$WvqnArmTT&+-QMy2Ib!AKO-GkW+K{=5wHOViSg&GS#=hypI12+IY{3cM5sb;8bH zP+SD*oqqfrY;OIzWOyeq$aY7ic0z*fus(i9EdQMv@&>d=Z9c_CGFYhVM5%l5g?-sva;b z9M->hm_xnt)1%bQfSQSDP3+iuvL!+kuk|F~Lq;z|JARf!x@uF%d6 z8(v7q;xOw+S&G#fo=7=bJKal^6G|l76r#U9v6+$QIcjy{gZ*iyQRJg2xhO9A1NMVN z;%pQpTncoOYSwgZ^P`P`fIv6l=qfmevvCs&lOrZnc4%yYN{OERhz1j-O zIy%u`{OIYXJ_PT_ATgGTVv!94@(%9IgPK@~3mnDkaAeU1$5eCvhF`^{1>CXkD^do%6RQ5SvQKve9S67 z#=*}F$KcPWPknwnhMn<8g4c$Iu>8^H>I~xj-@89 zVtMnD%I?zBj!JKp2?a#f_bA=u{pQBT#z&Dd&=bVoX=LdIaGH9-Q9Q=~2+A*XH_MCD zrclvxVhJ48Wq6)@M)^{Jf%zor$HO=pIEjR^Ct-OR?svzT9ff&OK_v`bc?V%6m1XwJ zO94!y8bgeqxQ_M{+nAr2UbgMX0u%Lf`e6R zXZP^bdv&nEq|74(AZZ6&jln=Ad~x-%+%3 zc}b26;5=Nw8Ij~0o5z{obMSPw!72RPJv7Cly8{sXN#^Czn+CWvG-PSWfmIuLtP#2M z$l2gIz?QdCiyZ4|gw;2S;BSnPK|5q*`MKGa$T2sb1;0>#e`P<`Sm#fJ&FAc|HTL{z zsj8JGHxZE+b~lotXaJI-Z~< zQjw*DhD|FO!0upE?Q~pVFa@Zd*FYwj9h7nr*lZf)da>X&bA-w=4^oBFE|p+eh@5CS z{Fu!}>}KM%N3@37VF(_{6`DC;qKGTl*^!X3;tprF(=qOxn&pr}cGdkFEW|%5?C}0d zDUt_;<5y)M%uvP_C&n^o6qXW{ux20MJj}2Z#RhpT*sj~mzW{5I?t}U7X*i0D+rZ44 zn1!{YA?;^Uo3#f!tMdS+RjNY*Q?lxxcaT@_EDwaXc=B^eJgFzE%gW>+#XJHTYhWqn zjJ35T-CHekw@bwak&FS_!-^*(+Do??W=rt4e^ucRvGcm4zV)R$n*(mWm*J zI4Z+;@%g*>{B4QP24Z}dpTEn`4^w^?q~6$Qpcx23W^37Aahw(PSsOuG1wP~T82JR| zgYgEI93}IVjXOQzbav+v#w-Olk8{FnkjY zrhTo~Qu3A{6;|C&>pBwRQ(OP{|NKeOmM=Py!EQfu#e_XwX6=xBm+L6SDm9Ivs@Gr^ zU5HT{^H6+bcT}&j+LT_w%d9hCL`ImQP0fbqp{f+Y1=~h3PkQt=lSoj^bA|Ib0zayB zM|nM?(2`0)O~?}`w<^BDEjia~3-!fpcUIfPTijb6Fy>jI6wJg&n?-9`kP}<{RrPgg z%0||k14S7`Sf<1c zEpGXALzo(i%PgHH^K*rWd| zySLhOy5a6rT}KfSvOCJvy8T4##so(+v1S91)v)jxpq}nH@()sF1@*)*Zs|dc0>^z( zj5W~WJyyg$du*x|_%#sFwP;YIu2e|Dc=O)K z5~oyf=Z=>$4JqmG!)lYQtvS`L{Tq$W<08cIna|;JMDp*-Ok2oRI4ov#T2xE6mClO> z=X*9EhhKzf&{xmVSu>}}J#Z)zT{GNiW9fCn;rsjD;JqWlQdZ?GSJCEBUc8sT%_G9^c%&wE46tp(qN55=#dH=ra}uL zM1j{Y&3Zdi1j+ZYUO>a6#56@g)M*;y-(4jiDr2WxPgNmGSO{r43O$sdntkXCL}Yl$ z`jX!mr`5bzuxA5Y!(V`T5VX=<%X1*S%vw+2`fU;RuU;nR?~_TR2{QU@Uc}g#R4hTY zaxx*MizldE$;;|5;_E00Y!5)CZr&+h*C5;D-2-6}qO;4oJ+igJ$5>~Ao?^VCQCM31 z)*oi^@!GSVZ5ibyni+VM#|Cq;9noe+`K%6XX}8Mev-KqQSQ&7fU?-^i*si5#bij*q z`SdY=_=(eMQm11%ueki`b`LE^`f={nxT>cAbqyfo0WJkee>)kR-vbcZ1R$7K3N@`Q zf?x5_BB5svvP4=yHrE*=^eJPl#{$$Z7jD-Xfligli-x`1fT13GP!qolMfK;PP%u z(9i4U<0dDk$(~fR;_Vq&G3gKua5#^~aX%eR$H`ZKqgGpJlwQPrDL83Rabh9f_36b> zx(L*Yz*ibOnywgA-%SRck{!i^*Ilh%e8s#@-c%f%H;ra>lFfTkzgEoZ*QV1t_?*st zVl{MTVVmfm(QzeW)xmN0wH&8K$9(=3E~EL@Rm^6pC7P?THG9PFB9&StzC4W+^$vb) z-%H`#1zjKe9KG#0NEsacbh#G711@|+&#&rVNd z0I8A{7L-!`l??)A>BDUZP=^zb6mw|fuf@o2ARJ}I49dUD3xKnn%`PCQ48NIKEFPZZ zeDTc+*iN#v4^SZLjpJIw;;l|0dgKrdEyc;Z8GQ;ae7|U~X+PLY1I!ZXVi=kX*HQP6y*5A(a5+&W=|I3aZP(itI_on)DG)riHdw z_X+iW$=0fwx&rjj19~uTh9lrxPbwm;;vZ{ONO{{ypX*x#_PIpt0|kCA@Q6+T2fksFt-IX<9`l3{(9t*^Npoj zqFa>Vat7c2i^bkPd!ki(*~ib(cWuNT|7*20U*6J>0;~ZDxC2KNvOA_&yULwQ41SNX z(Tv|*`g;6w6n%b+@=C{w_h(mW7#KC7?egMRQYK@DGpm_)*4g4KKgBD&7itr$t>|F#B#dZfrN+OFuU=8{1Fd!>Vd2 z?Tp6QY;TGMBUm%`_qK7*7`?e>Z}LiG^LF4Vx>9X?mX#w(!0iP?rZ*nuuP}I4w{BfX z3#+Clo~NG|W5cw=bwV6Ug!W?Sqts8F*1J7!Ij^zcu`M;>$_nT3xpVP>0nJJYW)^#j zDl{)w6EOMumQ^!Ls8mO631L^k4AxPB?F9R3r$Lxy;Vn*DX;``L+GFD(4jvty?01Zl-Ls;ad1IJ5?h3cku%qB= zbqxnR*AzG%9RJ(eOf3~efS@NQSCV;VvmKlC!HUMV5dLjHOa#X7)LE8G9XoS<8(OVr z%eSkxUe}zZWu@HJ7_yg9b;e(b$T1f;x-%2UyCNRJZo=ms%@$DVzS^+Y*0?ttZp_Qb zSH_|xr}?%h8Q`&u2tc^I)fVYLt?EnYd%D>y;ign% zW5WlrvN_3FLC;;`syvi^$+oN;)&e-Q*Uf5}jLXfKvecBi6x{=S%DuZ{xp!Apxp(jy zD=<0I?;0dO*I4gss{Qc%@y7$;FO;9xF>>sT6uYagsA|-$OlofAFsLZW*206(0!|G* z47@a$BUOOCS=Xu}HI(P(mMz`@Nh`9(%gNpj4Z$*WH%?2xyJw96y_5%)(iG+abS7(?QeKDvXQ*bOJH`i!ie3VK^4p( z@OR22166RbM^XYCY7M`=qKR$uCY^Fo#x+rt5r*o*=WA<~;zNTY(DEp|MTw@DA1^{$ zn2|Cx0L{aY9OgnM8j^|{axq_$ao0x3@KtCbMQ0Xe#pMH^RY`5?uJ>6V+{&OUpRt*@ z{(jXYm?q!chmSDq&c+6pQ}(58oTcs6zky|a-QwIX%T_d=6t@m5iws?>Ev329r0Ati zrOhaJL8a>oS30XQ>A`mG!}uD9=v9R2`4;T0^4TUTuWe+WBRa1ogTAMX-GYO*q$&%S zrI$-Y8uCCf|FqaoS;nCXOcS{1H<~k)HQid37dq4gDYj*5ZGsx_<1m|7pxD=Ou+7ys zQWH7&2Pl!SP>JH})J6Ei1)D84>SO7VX8WvC9*b1KC?GQz_Tk2yQ8iD+#j_}4T&Cj* z{nA3qUcNav=(wHdT{A)qyLIy~*>b2ip{L)stVx(4UqwZk-y z#Oxb!-{;(|&e(qE+MMoxsWu!v5uH+!2893CPAeQ?=`-V3V#2 zRMXtp>wl5mGPS6V31NBolA_^(R}>5NmJOAc%{x#EE!rnyLPUS zGtS4Yf9S#seQf(z#fYx3b-^fC{uyQ%dGb8K!UQq7b^8$)M??_-_;nMHMp&evFR+e+ zNb%-{De+Dn2{3i+wfwM#=+x!fvBd$&O}e z&GFirADLM6KBe2`rKEuwxZrnGaiL1u3RTp$li0f5@b)U2W+jHTM-}q|dC*hTmH@Qd zGsqGYo$8ma3fUu&t|WzaGjd-_?B#&{a;a!3hzUX(W*L?U0(u%Iw;Yky;4NM;iJpNV zf~5&`q@u9Y1Q649lN+@}5Wj8(Gdn$`WWCT=1ib}euDj-!4vY{2^n`Og&Rb_-Zqe8l zreJ5OCcdcV&f%dlf1HC#GGJ}X%y?s7D(?_(d-_V9k%_jAPL?fD0+P%q(g47HCyFew z@N@XtBj5<}Ra#LaTLQbHI&@X?bR{LVKuCcU;uZiArKK(1UG_k}=Y{*Vh^|JF$a4Qh zJiRAGmqlanG1j)lOj!hmc`#-d&7=O4yp%CF{+F(7ISt- z?0%`d`K7(e;KcHz5t<9-zFQZQ;e(DG^S4GQTH=3II9l)V(G}JC-O@#v3WBy$od_xQ zAbM8&;$HfNMOtT36&C0`F@?T)N>%fcsBCK2R_JakaL*uYo6?g8QYAIrnYpLz0-4KH z`DL)aAXOb0q|C?B%um&( zC$HJb4#8NCN1y6lGsi4qa+EuZ{=A{N<-rygZ-6HvlSIQ8EH4_WPamk$|3x(1!zq?M z|C*oQ_Qt!M@2b9xa+d>i{t=F*k(S)cl47tt_w?eDyoq#|Z915aDxI^uun+)0zQAP9 z*X#>X#@r{;mxrPak>WiY*k`5R6NPnpTn(zF?i?hC`B7N(F9m68%)~@^8x>SffEsJF zRb}#{+$jOb*odllSpUF6KIb$XfI}FJ2cUF*_ufL zD5;K?Gsc~YErVcqdLxnLcERsuAcmmcOx51?XoEeNV~2QDK&^T&#SII5;UX;Q<}xm# z5+FFvieb;vfAVIXGH1GTm0=UxwUmIX(MXbKjl$A}1mkd$v*-_Tk3^iwh>83G7j4ty zs5FG6rM|;O){|%>6pOyeJ)u-R6;joVj&B>mLzzafQE{GPVXL{2?s6J}CIonhxkVBA z%Bu=$&5OHOoWiKX)`VSDMYWZZIH+N3qAufeJyB-uI#MEd6_0V-J!Ije67eZzDDW+m zBERRVWOFY5?e;SVIVV9Os?sKm@p=vEqB@6*CW~((ye%#dF4G&Jf*^brFIaTd|VtCwr%b|ICYyFp4+)TO6H+WQ;5o zntS9t!lm=eW++v_JI#PT6~%4tO`ls+J*Rw%wJuu8i1@G5(e|~gw^rbjtEakuxU&@5 zSA_CH8mHB3Kuag;7h?R*B=M+uJ5o9iGrtQ|tRXye* ze!+?i$>W9;_^M~)n$*0-=dcj@(8B*Yadr#O7f%GUjlPv~zWW%+ zdYmR~>S%uKxa7WiN>~{NZ<9$8MehoRA3LQpDVG!PsSLT+nZ1QDW}i}wm#RDVUE>hb zq)9JvGKbM(ndLy0@`2Mv>`Q>Cb6}L`qQ@zV`PfcErz4>26|*c5dCl3dyDc0ydh&$j z9L3JMRc@1VA$a(J=X@hf)N!rx`FITGx?LSuPfaVbspGI1RL$b4x%s z;d(NXiX5S$1+a_YvM9J2bA}Lw1);jD!@%ZlkoeiG}gt z^_}!^5c32lnaC0)g9mN8Gbn^nV?{`6!XH*9K1d_>Q9Z-5QS+oa%OyF4lVTme%=MIs zpe&9o7LusjU8|BL{A8=yMAtxnSX2A7?M?~wS;Rc+YA@%_iFQ146Az)2dwHi&@yk@Z zTQ8<@YGb0ZNr||zchSU%R+Af1A&JHvrJ(bzh&i+#whztjdT~>i4bOcqTk5(OT~eA^ zk*vtk7JrswW_L$9lE-sYuA+C0&rVZi zk&{rX{9Lu;@jo@q*)cQR6nf}SLzzHm^QBuXoXAvd`uw+1UcMQ%1yub7sVycUt<_vG z#LuO?voBRo57Xql+{H#2W|wX@+U_ z@N$ZG;$qHWT;K=exCkj~bbV!+p@$mlV>u7O`K^of-7|`HJWEPRDq|E`DVJr3K$>96 zqH%g1IkPI-=F0vPa3QMIC4TFfO!3YrO2jC`*NABRLkhh7R#1n)TkR0>h_b5i+uWaK{I9dLAi-))i=zaj%$Q87^hnK4JA>QB5_xf8tCk4h zs0{xTeiBSpaZ3^S!yrlSwao0lu_%*(nWLPnv-?@yG;*A$SkKkWdU7TX>C5(AVqkzq zjIdoUPFw2nk!pSq272Zy8N)83s;V-ht^-S=IaHU?p{rxQa9ux;98hQJ4+2?U(kx6< zl!4J3&cY1$LeVenbAu}4zUCtKRb;}|DAje!bpzeHnU3vOvHhxcbCtVNeTrq>qhQvZ6TB6AS8M%iE_#^r_&8JG zeE3WnoNvI=IF;p-?kcabUz!(o9DWXR;G|SeP|sESR+PZk;b#Cd2?Mi*z|{u>!w}fN zrc8X>QEsj>n9V}n_=Rj79zV}!jieA|1=B`-nC24k^-@mDZczY)h24Zgd(GO;&XaP6 zK%@)D2UxNUuLJ>(i2=jIg5QY3V~w#LBJyCJ4%2SItdElvFt8`ttgu#&(*a1JtkMZf zYdSr|fubC=G1dbpaJOX2RSNnr&T@ErjMu^#xl+)I---^cICmz^}qN<~Z^dXwAr zBt3+T(&0~Cak4V2jR+N7|EfZuR$Pm-S@iG;*oNMR#k=u>HW~I=+ z>%17mOpKXM?q^{)@3qkKUd^ZqPd@COtE7fJLc!OloI%3xyCViW07D1uYAB- zg{}uEQX`B%HSyvW=ac#bMc;AXkET2DP(}a{nK|JRx7r0&x1dSSA!{%1KEuJ;BX?pO z48yN53n!BZdgjs*_x_DykPZ1g0J?8d%%|FbXnw=*1`vw_VU_pgvKOA(_ClvQ&bEh% z074GZyJaEs$sYxo(*+^($$XF*ICxbWPz|b|d=*qbsYUg)7S)x>`0JuNXlWxXSz`xW zkxufA6$Nu*{@yK$+u?KsSVF+2Uam=Krt&9)G+8ay`k(-&siL7db&g=7E>`GP$rOrW!wymVQk+lH#?6aMf215ir= z0u%rg00ICA08p)1Hf^xepJy`w0PtS{00{s9000000096X000000001XWpYDra%C=K ZP)h{{000000RRC2Hvj+tjxzuN005(I&=>#! diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 60ddcbe17..c36642bc7 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 e6528233d..8d1de8c1a 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 4fdb4d31d..f4ffa4c10 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 e2f0bcd43..6b130e7e0 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 3c963e994..3c3431bfe 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 ad99829af..1d0711f65 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 382944286..cc75b90f7 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 afbbbe428..f2ca41d3e 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, pFanin2, k ) + 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 ); } } 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) ); + // 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( 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 10e312b3b..5aae46cc0 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 );