diff options
Diffstat (limited to 'src/aig/saig/saigIso.c')
| -rw-r--r-- | src/aig/saig/saigIso.c | 597 |
1 files changed, 597 insertions, 0 deletions
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c new file mode 100644 index 00000000..1001f153 --- /dev/null +++ b/src/aig/saig/saigIso.c @@ -0,0 +1,597 @@ +/**CFile**************************************************************** + + FileName [saigIso.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Sequential cleanup.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "src/aig/ioa/ioa.h" +#include "saig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Find the canonical permutation of the COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis ) +{ + extern int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ); + Vec_Int_t * vPermCos; + Aig_Obj_t * pObj, * pFanin; + int i, Entry, Diff; + assert( Vec_IntSize(vPermCis) == Aig_ManPiNum(pAig) ); + vPermCos = Vec_IntAlloc( Aig_ManPoNum(pAig) ); + if ( Saig_ManPoNum(pAig) == 1 ) + Vec_IntPush( vPermCos, 0 ); + else + { + Vec_Ptr_t * vRoots = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + Saig_ManForEachPo( pAig, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + assert( Aig_ObjIsConst1(pFanin) || pFanin->iData > 0 ); + pObj->iData = Abc_Var2Lit( pFanin->iData, Aig_ObjFaninC0(pObj) ); + Vec_PtrPush( vRoots, pObj ); + } + Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareAigObjByData ); + Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) + Vec_IntPush( vPermCos, Aig_ObjPioNum(pObj) ); + Vec_PtrFree( vRoots ); + } + // add flop outputs + Diff = Saig_ManPoNum(pAig) - Saig_ManPiNum(pAig); + Vec_IntForEachEntryStart( vPermCis, Entry, i, Saig_ManPiNum(pAig) ) + Vec_IntPush( vPermCos, Entry + Diff ); + return vPermCos; +} + +/**Function************************************************************* + + Synopsis [Performs canonical duplication of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManDupIsoCanonical_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + assert( Aig_ObjIsNode(pObj) ); + if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) || !Aig_ObjIsNode(Aig_ObjFanin1(pObj)) ) + { + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + } + else + { + assert( Aig_ObjFanin0(pObj)->iData != Aig_ObjFanin1(pObj)->iData ); + if ( Aig_ObjFanin0(pObj)->iData < Aig_ObjFanin1(pObj)->iData ) + { + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + } + else + { + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + } + } + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Performs canonical duplication of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + Vec_Int_t * vPerm, * vPermCo; + int i, Entry; + // derive permutations + vPerm = Saig_ManFindIsoPerm( pAig, fVerbose ); + vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm ); + // create the new manager + pNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); + pNew->pName = Abc_UtilStrsav( pAig->pName ); + Aig_ManIncrementTravId( pAig ); + // create constant + pObj = Aig_ManConst1(pAig); + pObj->pData = Aig_ManConst1(pNew); + Aig_ObjSetTravIdCurrent( pAig, pObj ); + // create PIs + Vec_IntForEachEntry( vPerm, Entry, i ) + { + pObj = Aig_ManPi(pAig, Entry); + pObj->pData = Aig_ObjCreatePi(pNew); + Aig_ObjSetTravIdCurrent( pAig, pObj ); + } + // traverse from the POs + Vec_IntForEachEntry( vPermCo, Entry, i ) + { + pObj = Aig_ManPo(pAig, Entry); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + } + // create POs + Vec_IntForEachEntry( vPermCo, Entry, i ) + { + pObj = Aig_ManPo(pAig, Entry); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) ); + Vec_IntFreeP( &vPerm ); + Vec_IntFreeP( &vPermCo ); + return pNew; +} + + + + + +/**Function************************************************************* + + Synopsis [Checks structural equivalence of AIG1 and AIG2.] + + Description [Returns 1 if AIG1 and AIG2 are structurally equivalent + under this mapping.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose ) +{ + Aig_Obj_t * pObj, * pFanin0, * pFanin1; + int i; + assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) ); + assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) ); + assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) ); + assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) ); + Aig_ManCleanData( pAig1 ); + // map const and PI nodes + Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1); + Aig_ManForEachPi( pAig2, pObj, i ) + pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) ); + // try internal nodes + Aig_ManForEachNode( pAig2, pObj, i ) + { + pFanin0 = Aig_ObjChild0Copy( pObj ); + pFanin1 = Aig_ObjChild1Copy( pObj ); + pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 ); + if ( pObj->pData == NULL ) + { + if ( fVerbose ) + printf( "Structural equivalence failed at node %d.\n", i ); + return 0; + } + } + // make sure the first PO points to the same node + if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) ) + { + if ( fVerbose ) + printf( "Structural equivalence failed at primary output 0.\n" ); + return 0; + } + return 1; +} + +//static int s_Counter; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ManNegEdgeNum( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + if ( pAig->nComplEdges > 0 ) + return pAig->nComplEdges; + Aig_ManForEachObj( pAig, pObj, i ) + if ( Aig_ObjIsNode(pObj) ) + { + Counter += Aig_ObjFaninC0(pObj); + Counter += Aig_ObjFaninC1(pObj); + } + else if ( Aig_ObjIsPo(pObj) ) + Counter += Aig_ObjFaninC0(pObj); + return (pAig->nComplEdges = Counter); +} + +/**Function************************************************************* + + Synopsis [Finds mapping of CIs of AIG2 into those of AIG1.] + + Description [Returns the mapping of CIs of the two AIGs, or NULL + if there is no mapping.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose ) +{ + Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2; + int i, Entry; + if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) ) + return NULL; + if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) ) + return NULL; + if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) ) + return NULL; + if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) ) + return NULL; + if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) ) + return NULL; +// if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) ) +// return NULL; +// s_Counter++; + + if ( fVerbose ) + printf( "AIG1:\n" ); + vPerm1 = vPerm1_ ? vPerm1_ : Saig_ManFindIsoPerm( pAig1, fVerbose ); + if ( fVerbose ) + printf( "AIG1:\n" ); + vPerm2 = vPerm2_ ? vPerm2_ : Saig_ManFindIsoPerm( pAig2, fVerbose ); + if ( vPerm1_ ) + assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) ); + if ( vPerm2_ ) + assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) ); + // find canonical permutation + // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2 + vInvPerm2 = Vec_IntInvert( vPerm2, -1 ); + Vec_IntForEachEntry( vInvPerm2, Entry, i ) + { + assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) ); + Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) ); + } + if ( vPerm1_ == NULL ) + Vec_IntFree( vPerm1 ); + if ( vPerm2_ == NULL ) + Vec_IntFree( vPerm2 ); + // check if they are indeed equivalent + if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) ) + Vec_IntFreeP( &vInvPerm2 ); + return vInvPerm2; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose ) +{ + int fVeryVerbose = 0; + Vec_Ptr_t * vParts, * vPerms, * vAigs; + Vec_Int_t * vPos, * vMap; + Aig_Man_t * pPart, * pTemp; + int i, k, nPos; + + // derive AIG for each PO + nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); + vParts = Vec_PtrAlloc( nPos ); + vPerms = Vec_PtrAlloc( nPos ); + for ( i = 0; i < nPos; i++ ) + { + pPart = Saig_ManDupCones( pAig, &i, 1 ); + vMap = Saig_ManFindIsoPerm( pPart, fVeryVerbose ); + Vec_PtrPush( vParts, pPart ); + Vec_PtrPush( vPerms, vMap ); + } +// s_Counter = 0; + + // check AIGs for each PO + vAigs = Vec_PtrAlloc( 1000 ); + vPos = Vec_IntAlloc( 1000 ); + Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i ) + { + if ( fVeryVerbose ) + { + printf( "AIG %4d : ", i ); + Aig_ManPrintStats( pPart ); + } + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k ) + { + if ( fVeryVerbose ) + printf( "Comparing AIG %4d and AIG %4d. ", Vec_IntEntry(vPos,k), i ); + vMap = Iso_ManFindMapping( pTemp, pPart, + (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)), + (Vec_Int_t *)Vec_PtrEntry(vPerms, i), + fVeryVerbose ); + if ( vMap != NULL ) + { + if ( fVeryVerbose ) + printf( "Found match\n" ); + if ( fVerbose ) + printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i ); + Vec_IntFree( vMap ); + break; + } + if ( fVeryVerbose ) + printf( "No match.\n" ); + } + if ( k == Vec_PtrSize(vAigs) ) + { + Vec_PtrPush( vAigs, pPart ); + Vec_IntPush( vPos, i ); + } + } + // delete AIGs + Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i ) + Aig_ManStop( pPart ); + Vec_PtrFree( vParts ); + Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i ) + Vec_IntFree( vMap ); + Vec_PtrFree( vPerms ); + // derive the resulting AIG + pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) ); + Vec_PtrFree( vAigs ); + Vec_IntFree( vPos ); + +// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); + return pPart; +} + +/**Function************************************************************* + + Synopsis [Takes multi-output sequential AIG.] + + Description [Returns candidate equivalence classes of POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) +{ + return Vec_StrCompareVec( *p1, *p2 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) +{ + int fVeryVerbose = 0; + Aig_Man_t * pPart, * pTemp; + Vec_Ptr_t * vBuffers, * vClasses; + Vec_Int_t * vLevel, * vRemain; + Vec_Str_t * vStr, * vPrev; + int i, nPos, nUnique = 0, clk = clock(); + + // derive AIG for each PO + nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); + vBuffers = Vec_PtrAlloc( nPos ); + for ( i = 0; i < nPos; i++ ) + { +// if ( i % 100 == 0 ) +// printf( "%d finished...\n", i ); + pPart = Saig_ManDupCones( pAig, &i, 1 ); + pTemp = Saig_ManDupIsoCanonical( pPart, 0 ); + vStr = Ioa_WriteAigerIntoMemoryStr( pTemp ); + Vec_PtrPush( vBuffers, vStr ); + Aig_ManStop( pTemp ); + Aig_ManStop( pPart ); + // remember the output number in nCap (attention: hack!) + vStr->nCap = i; + } +// s_Counter = 0; + if ( fVerbose ) + Abc_PrintTime( 1, "Isomorph time", clock() - clk ); + + // sort the infos + clk = clock(); + Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr ); + + // create classes + clk = clock(); + vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + // start the first class + Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) ); + vPrev = (Vec_Str_t *)Vec_PtrEntry( vBuffers, 0 ); + Vec_IntPush( vLevel, vPrev->nCap ); + // consider other classes + Vec_PtrForEachEntryStart( Vec_Str_t *, vBuffers, vStr, i, 1 ) + { + if ( Vec_StrCompareVec(vPrev, vStr) ) + Vec_PtrPush( vClasses, Vec_IntAlloc(4) ); + vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses ); + Vec_IntPush( vLevel, vStr->nCap ); + vPrev = vStr; + } + Vec_VecFree( (Vec_Vec_t *)vBuffers ); + + if ( fVerbose ) + Abc_PrintTime( 1, "Sorting time", clock() - clk ); +// Abc_PrintTime( 1, "Traversal time", time_Trav ); + + // report the results +// Vec_VecPrintInt( (Vec_Vec_t *)vClasses ); +// printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); + if ( fVerbose ) + { + Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) + if ( Vec_IntSize(vLevel) > 1 ) + printf( "%d ", Vec_IntSize(vLevel) ); + else + nUnique++; + printf( " Unique = %d\n", nUnique ); + } + + // collect the first ones + vRemain = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) + Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) ); + + // derive the resulting AIG + pPart = Saig_ManDupCones( pAig, Vec_IntArray(vRemain), Vec_IntSize(vRemain) ); + Vec_IntFree( vRemain ); + +// return (Vec_Vec_t *)vClasses; + Vec_VecFree( (Vec_Vec_t *)vClasses ); + +// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); + return pPart; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) +{ + Vec_Int_t * vPerm; + int clk = clock(); + vPerm = Saig_ManFindIsoPerm( pAig, fVerbose ); + Vec_IntFree( vPerm ); + Abc_PrintTime( 1, "Time", clock() - clk ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose ) +{ + Aig_Man_t * pPart; + int clk = clock(); + pPart = Iso_ManFilterPos( pAig, fVerbose ); + printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); + Abc_PrintTime( 1, "Time", clock() - clk ); +// Aig_ManStop( pPart ); + return pPart; +} + + +#include "src/base/abc/abc.h" + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManTest888( Aig_Man_t * pAig1, int fVerbose ) +{ + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + Abc_Ntk_t * pNtk; + Aig_Man_t * pAig2; + Vec_Int_t * vMap; + + pNtk = Abc_NtkFromAigPhase( pAig1 ); + Abc_NtkPermute( pNtk, 1, 0, 1 ); + pAig2 = Abc_NtkToDar( pNtk, 0, 1 ); + Abc_NtkDelete( pNtk ); + + vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose ); + Aig_ManStop( pAig2 ); + + if ( vMap != NULL ) + { + printf( "Mapping of AIGs is found.\n" ); + if ( fVerbose ) + Vec_IntPrint( vMap ); + } + else + printf( "Mapping of AIGs is NOT found.\n" ); + Vec_IntFreeP( &vMap ); + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |