From d9760b04a80adbb44a203aeb614ab6576171aa9b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 9 Feb 2008 08:01:00 -0800 Subject: Version abc80209 --- src/aig/aig/aig.h | 3 ++- src/aig/aig/aigPart.c | 36 ++++++++++++++++++++++++++++++++++- src/aig/fra/fraClaus.c | 4 ++-- src/base/abci/abcDar.c | 50 ++++++++++++++++++++++++++++++------------------- src/opt/mfs/mfsCore.c | 1 + src/opt/mfs/mfsInt.h | 1 + src/opt/mfs/mfsMan.c | 2 ++ src/opt/mfs/mfsStrash.c | 23 ++++++++++++++++++++++- 8 files changed, 96 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index cd810b5e..1124c2fb 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -517,7 +517,8 @@ extern void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId ); extern void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId ); extern void Aig_ObjOrderAdvance( Aig_Man_t * p ); /*=== aigPart.c =========================================================*/ -extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan ); +extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * p ); +extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps ); extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index e2100b57..edf51a2e 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -258,7 +258,7 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p ) Synopsis [Computes supports of the POs in the multi-output AIG.] Description [Returns the array of integer arrays containing indices - of the primary inputs.] + of the primary inputsf or each primary output.] SideEffects [Adds the integer PO number at end of each array.] @@ -344,6 +344,40 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan ) return vSupports; } +/**Function************************************************************* + + Synopsis [Computes the set of outputs for each input.] + + Description [Returns the array of integer arrays containing indices + of the primary outputsf for each primary input.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p ) +{ + Vec_Ptr_t * vSupps, * vSuppsInv; + Vec_Int_t * vSupp; + int i, k, iIn, iOut; + // get structural supports for each output + vSupps = Aig_ManSupports( p ); + // start the inverse supports + vSuppsInv = Vec_PtrAlloc( Aig_ManPiNum(p) ); + for ( i = 0; i < Aig_ManPiNum(p); i++ ) + Vec_PtrPush( vSuppsInv, Vec_IntAlloc(8) ); + // transforms the supports into the inverse supports + Vec_PtrForEachEntry( vSupps, vSupp, i ) + { + iOut = Vec_IntPop( vSupp ); + Vec_IntForEachEntry( vSupp, iIn, k ) + Vec_IntPush( Vec_PtrEntry(vSuppsInv, iIn), iOut ); + } + Vec_VecFree( (Vec_Vec_t *)vSupps ); + return vSuppsInv; +} + /**Function************************************************************* Synopsis [Start char-bases support representation.] diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index 8e3a03e1..d95515d5 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -515,7 +515,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) nCountConst = nCountImps = 0; CostMax = p->nSimWords * 32; - +/* // add the property { Aig_Obj_t * pObj; @@ -528,7 +528,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) nCountConst++; // printf( "Added the target property to the set of clauses to be inductively checked.\n" ); } - +*/ pSeq->nWordsPref = p->nSimWordsPref; Aig_ManForEachLoSeq( p->pAig, pObj1, i ) diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 72606dcf..d703cfc4 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -95,8 +95,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) if ( fRegisters ) { pMan->nRegs = Abc_NtkLatchNum(pNtk); -// pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); - pMan->vFlopNums = NULL; + pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); +// pMan->vFlopNums = NULL; } // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); @@ -154,6 +154,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_Obj_t * pObjNew; Aig_Obj_t * pObj; int i; + assert( pMan->nAsserts == 0 ); // assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); // perform strashing pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); @@ -203,11 +204,12 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) { - Vec_Ptr_t * vNodes; + Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObjNew, * pLatch; Aig_Obj_t * pObj, * pObjLo, * pObjLi; - int i, iNodeId; + int i, iNodeId, nDigits; + assert( pMan->nAsserts == 0 ); // assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); // perform strashing pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); @@ -237,19 +239,6 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_ObjAddFanin( pObjLo->pData, pObjNew ); Abc_LatchSetInit0( pObjNew ); } - if ( pMan->vFlopNums == NULL ) - Abc_NtkAddDummyBoxNames( pNtkNew ); - else - { - assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) ); - Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) - { - pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) ); - Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL ); - Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL ); - Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL ); - } - } // rebuild the AIG vNodes = Aig_ManDfs( pMan ); Vec_PtrForEachEntry( vNodes, pObj, i ) @@ -261,8 +250,8 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) // connect the PO nodes Aig_ManForEachPo( pMan, pObj, i ) { - if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) - break; +// if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts ) +// break; iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO ); if ( iNodeId >= 0 ) pObjNew = Abc_NtkObj( pNtkNew, iNodeId ); @@ -270,6 +259,29 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew ); } + if ( pMan->vFlopNums == NULL ) + Abc_NtkAddDummyBoxNames( pNtkNew ); + else + { + assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) ); + nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) ); + Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) + { + pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) ); + iNodeId = Nm_ManFindIdByName( pNtkNew->pManName, Abc_ObjName(Abc_ObjFanout0(pLatch)), ABC_OBJ_PO ); + if ( iNodeId >= 0 ) + { + Abc_ObjAssignName( pObjNew, Abc_ObjNameDummy("l", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjNameDummy("li", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjNameDummy("lo", i, nDigits), NULL ); +//printf( "happening %s -> %s\n", Abc_ObjName(Abc_ObjFanin0(pObjNew)), Abc_ObjName(Abc_ObjFanout0(pObjNew)) ); + continue; + } + Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL ); + } + } // if there are assertions, add them if ( pMan->nAsserts > 0 ) Aig_ManForEachAssert( pMan, pObj, i ) diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index aed0abe5..082b35d4 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -175,6 +175,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 ); p->pCare = Abc_NtkToDar( pTemp, 0 ); Abc_NtkDelete( pTemp ); + p->vSuppsInv = Aig_ManSupportsInverse( p->pCare ); } // if ( pPars->fVerbose ) { diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index ddd16407..e51e0bba 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -49,6 +49,7 @@ struct Mfs_Man_t_ Mfs_Par_t * pPars; Abc_Ntk_t * pNtk; Aig_Man_t * pCare; + Vec_Ptr_t * vSuppsInv; int nFaninMax; // intermeditate data for the node Vec_Ptr_t * vRoots; // the roots of the window diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 519b855d..768e5295 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -155,6 +155,8 @@ void Mfs_ManStop( Mfs_Man_t * p ) Mfs_ManPrint( p ); if ( p->pCare ) Aig_ManStop( p->pCare ); + if ( p->vSuppsInv ) + Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv ); Mfs_ManClean( p ); Int_ManFree( p->pMan ); Vec_IntFree( p->vMem ); diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c index 8e945045..a3475752 100644 --- a/src/opt/mfs/mfsStrash.c +++ b/src/opt/mfs/mfsStrash.c @@ -179,7 +179,8 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) Aig_Man_t * pMan; Abc_Obj_t * pFanin; Aig_Obj_t * pObjAig, * pPi, * pPo; - int i; + Vec_Int_t * vOuts; + int i, k, iOut; // start the new manager pMan = Aig_ManStart( 1000 ); // construct the root node's AIG cone @@ -197,6 +198,25 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) pPi->pData = pFanin->pCopy; } // construct the constraints + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + vOuts = Vec_PtrEntry( p->vSuppsInv, (int)pFanin->pData ); + Vec_IntForEachEntry( vOuts, iOut, k ) + { + pPo = Aig_ManPo( p->pCare, iOut ); + if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) ) + continue; + Aig_ObjSetTravIdCurrent( p->pCare, pPo ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) ) + continue; + pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + Aig_ObjCreatePo( pMan, pObjAig ); + } + } +/* Aig_ManForEachPo( p->pCare, pPo, i ) { // assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) ); @@ -208,6 +228,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); Aig_ObjCreatePo( pMan, pObjAig ); } +*/ } if ( p->pPars->fResub ) { -- cgit v1.2.3