| /**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 "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_ObjCompareByData( 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_ManCiNum(pAig) ); |
| vPermCos = Vec_IntAlloc( Aig_ManCoNum(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_ObjCompareByData ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) |
| Vec_IntPush( vPermCos, Aig_ObjCioId(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_ManCi(pAig, Entry); |
| pObj->pData = Aig_ObjCreateCi(pNew); |
| Aig_ObjSetTravIdCurrent( pAig, pObj ); |
| } |
| // traverse from the POs |
| Vec_IntForEachEntry( vPermCo, Entry, i ) |
| { |
| pObj = Aig_ManCo(pAig, Entry); |
| Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); |
| } |
| // create POs |
| Vec_IntForEachEntry( vPermCo, Entry, i ) |
| { |
| pObj = Aig_ManCo(pAig, Entry); |
| Aig_ObjCreateCo( 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_ManCiNum(pAig1) == Aig_ManCiNum(pAig2) ); |
| assert( Aig_ManCoNum(pAig1) == Aig_ManCoNum(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_ManForEachCi( pAig2, pObj, i ) |
| pObj->pData = Aig_ManCi( 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_ManCoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManCo(pAig2, 0)) != Aig_ObjChild0(Aig_ManCo(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_ObjIsCo(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_ManCiNum(pAig1) != Aig_ManCiNum(pAig2) ) |
| return NULL; |
| if ( Aig_ManCoNum(pAig1) != Aig_ManCoNum(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_ManCiNum(pAig1) ); |
| if ( vPerm2_ ) |
| assert( Vec_IntSize(vPerm2_) == Aig_ManCiNum(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_ManCiNum(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_ManCoNum(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, Vec_Ptr_t ** pvPosEquivs, 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; |
| abctime clk = Abc_Clock(); |
| abctime clkDup = 0, clkAig = 0, clkIso = 0, clk2; |
| *pvPosEquivs = NULL; |
| |
| // derive AIG for each PO |
| nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig); |
| vBuffers = Vec_PtrAlloc( nPos ); |
| for ( i = 0; i < nPos; i++ ) |
| { |
| if ( i % 100 == 0 ) |
| printf( "%6d finished...\r", i ); |
| |
| clk2 = Abc_Clock(); |
| pPart = Saig_ManDupCones( pAig, &i, 1 ); |
| clkDup += Abc_Clock() - clk2; |
| |
| clk2 = Abc_Clock(); |
| pTemp = Saig_ManDupIsoCanonical( pPart, 0 ); |
| clkIso += Abc_Clock() - clk2; |
| |
| clk2 = Abc_Clock(); |
| vStr = Ioa_WriteAigerIntoMemoryStr( pTemp ); |
| clkAig += Abc_Clock() - clk2; |
| |
| 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, "Duplicate time", clkDup ); |
| Abc_PrintTime( 1, "Isomorph time", clkIso ); |
| Abc_PrintTime( 1, "AIGER time", clkAig ); |
| } |
| |
| // sort the infos |
| clk = Abc_Clock(); |
| Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr ); |
| |
| // create classes |
| clk = Abc_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", Abc_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 ); |
| } |
| */ |
| |
| // canonicize order |
| Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) |
| Vec_IntSort( vLevel, 0 ); |
| Vec_VecSortByFirstInt( (Vec_Vec_t *)vClasses, 0 ); |
| |
| // 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 ); |
| *pvPosEquivs = vClasses; |
| return pPart; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) |
| { |
| Vec_Int_t * vPerm; |
| abctime clk = Abc_Clock(); |
| vPerm = Saig_ManFindIsoPerm( pAig, fVerbose ); |
| Vec_IntFree( vPerm ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| return NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) |
| { |
| Aig_Man_t * pPart; |
| abctime clk = Abc_Clock(); |
| pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose ); |
| printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| if ( fVerbose && *pvPosEquivs && Saig_ManPoNum(pAig) != Vec_PtrSize(*pvPosEquivs) ) |
| { |
| printf( "Nontrivial classes:\n" ); |
| Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 ); |
| } |
| // Aig_ManStopP( &pPart ); |
| return pPart; |
| } |
| |
| ABC_NAMESPACE_IMPL_END |
| |
| #include "base/abc/abc.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| /**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, NULL ); |
| 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 |
| |
