| /**CFile**************************************************************** |
| |
| FileName [saigMiter.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Computes sequential miter of two sequential AIGs.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigMiter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "proof/fra/fra.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks the status of the miter.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p ) |
| { |
| Sec_MtrStatus_t Status; |
| Aig_Obj_t * pObj, * pChild; |
| int i; |
| memset( &Status, 0, sizeof(Sec_MtrStatus_t) ); |
| Status.iOut = -1; |
| Status.nInputs = Saig_ManPiNum( p ); |
| Status.nNodes = Aig_ManNodeNum( p ); |
| Status.nOutputs = Saig_ManPoNum(p); |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| pChild = Aig_ObjChild0(pObj); |
| // check if the output is constant 0 |
| if ( pChild == Aig_ManConst0(p) ) |
| Status.nUnsat++; |
| // check if the output is constant 1 |
| else if ( pChild == Aig_ManConst1(p) ) |
| { |
| Status.nSat++; |
| if ( Status.iOut == -1 ) |
| Status.iOut = i; |
| } |
| // check if the output is a primary input |
| else if ( Saig_ObjIsPi(p, Aig_Regular(pChild)) ) |
| { |
| Status.nSat++; |
| if ( Status.iOut == -1 ) |
| Status.iOut = i; |
| } |
| // check if the output is 1 for the 0000 pattern |
| else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) |
| { |
| Status.nSat++; |
| if ( Status.iOut == -1 ) |
| Status.iOut = i; |
| } |
| else |
| Status.nUndec++; |
| } |
| return Status; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates sequential miter.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj; |
| int i; |
| assert( Saig_ManRegNum(p0) > 0 || Saig_ManRegNum(p1) > 0 ); |
| assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) ); |
| assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) ); |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); |
| pNew->pName = Abc_UtilStrsav( "miter" ); |
| Aig_ManCleanData( p0 ); |
| Aig_ManCleanData( p1 ); |
| // map constant nodes |
| Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); |
| Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); |
| // map primary inputs |
| Saig_ManForEachPi( p0, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| Saig_ManForEachPi( p1, pObj, i ) |
| pObj->pData = Aig_ManCi( pNew, i ); |
| // map register outputs |
| Saig_ManForEachLo( p0, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| Saig_ManForEachLo( p1, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| // map internal nodes |
| Aig_ManForEachNode( p0, pObj, i ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| Aig_ManForEachNode( p1, pObj, i ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // create primary outputs |
| Saig_ManForEachPo( p0, pObj, i ) |
| { |
| if ( Oper == 0 ) // XOR |
| pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) ); |
| else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1) |
| pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) ); |
| else |
| assert( 0 ); |
| Aig_ObjCreateCo( pNew, pObj ); |
| } |
| // create register inputs |
| Saig_ManForEachLi( p0, pObj, i ) |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| Saig_ManForEachLi( p1, pObj, i ) |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| // cleanup |
| Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) ); |
| // Aig_ManCleanup( pNew ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates combinational miter.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj; |
| int i; |
| assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) ); |
| assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) ); |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); |
| pNew->pName = Abc_UtilStrsav( "miter" ); |
| // map constant nodes |
| Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); |
| Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); |
| // map primary inputs and register outputs |
| Aig_ManForEachCi( p0, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| Aig_ManForEachCi( p1, pObj, i ) |
| pObj->pData = Aig_ManCi( pNew, i ); |
| // map internal nodes |
| Aig_ManForEachNode( p0, pObj, i ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| Aig_ManForEachNode( p1, pObj, i ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // create primary outputs |
| Aig_ManForEachCo( p0, pObj, i ) |
| { |
| if ( Oper == 0 ) // XOR |
| pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) ); |
| else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1) |
| pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) ); |
| else |
| assert( 0 ); |
| Aig_ObjCreateCo( pNew, pObj ); |
| } |
| // cleanup |
| Aig_ManSetRegNum( pNew, 0 ); |
| Aig_ManCleanup( pNew ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives dual-rail AIG.] |
| |
| Description [Orders nodes as follows: PIs, ANDs, POs.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_AndDualRail( Aig_Man_t * pNew, Aig_Obj_t * pObj, Aig_Obj_t ** ppData, Aig_Obj_t ** ppNext ) |
| { |
| Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj); |
| Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj); |
| Aig_Obj_t * p0Data = Aig_ObjFaninC0(pObj)? pFanin0->pNext : (Aig_Obj_t *)pFanin0->pData; |
| Aig_Obj_t * p0Next = Aig_ObjFaninC0(pObj)? (Aig_Obj_t *)pFanin0->pData : pFanin0->pNext; |
| Aig_Obj_t * p1Data = Aig_ObjFaninC1(pObj)? pFanin1->pNext : (Aig_Obj_t *)pFanin1->pData; |
| Aig_Obj_t * p1Next = Aig_ObjFaninC1(pObj)? (Aig_Obj_t *)pFanin1->pData : pFanin1->pNext; |
| *ppData = Aig_Or( pNew, |
| Aig_And(pNew, p0Data, Aig_Not(p0Next)), |
| Aig_And(pNew, p1Data, Aig_Not(p1Next)) ); |
| *ppNext = Aig_And( pNew, |
| Aig_And(pNew, Aig_Not(p0Data), p0Next), |
| Aig_And(pNew, Aig_Not(p1Data), p1Next) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives dual-rail AIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter ) |
| { |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pObj, * pMiter; |
| int i; |
| Aig_ManCleanData( p ); |
| Aig_ManCleanNext( p ); |
| // create the new manager |
| pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| // create the PIs |
| Aig_ManConst1(p)->pData = Aig_ManConst0(pNew); |
| Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew); |
| Aig_ManForEachCi( p, pObj, i ) |
| { |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| pObj->pNext = Aig_ObjCreateCi( pNew ); |
| } |
| // duplicate internal nodes |
| Aig_ManForEachNode( p, pObj, i ) |
| Saig_AndDualRail( pNew, pObj, (Aig_Obj_t **)&pObj->pData, &pObj->pNext ); |
| // add the POs |
| if ( fMiter ) |
| { |
| pMiter = Aig_ManConst1(pNew); |
| Saig_ManForEachLo( p, pObj, i ) |
| { |
| pMiter = Aig_And( pNew, pMiter, |
| Aig_Or(pNew, (Aig_Obj_t *)pObj->pData, pObj->pNext) ); |
| } |
| Aig_ObjCreateCo( pNew, pMiter ); |
| Saig_ManForEachLi( p, pObj, i ) |
| { |
| if ( !Aig_ObjFaninC0(pObj) ) |
| { |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); |
| Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext ); |
| } |
| else |
| { |
| Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext ); |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); |
| } |
| } |
| } |
| else |
| { |
| Aig_ManForEachCo( p, pObj, i ) |
| { |
| if ( !Aig_ObjFaninC0(pObj) ) |
| { |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); |
| Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext ); |
| } |
| else |
| { |
| Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext ); |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); |
| } |
| } |
| } |
| Aig_ManSetRegNum( pNew, 2*Aig_ManRegNum(p) ); |
| Aig_ManCleanData( p ); |
| Aig_ManCleanNext( p ); |
| Aig_ManCleanup( pNew ); |
| // check the resulting network |
| if ( !Aig_ManCheck(pNew) ) |
| printf( "Aig_ManDupSimple(): The check has failed.\n" ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Create combinational timeframes by unrolling sequential circuits.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) |
| { |
| Aig_Man_t * p, * pAig; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo; |
| int i, f; |
| // assert( nFrames > 1 ); |
| assert( Saig_ManPiNum(pBot) == Saig_ManPiNum(pTop) ); |
| assert( Saig_ManPoNum(pBot) == Saig_ManPoNum(pTop) ); |
| assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) ); |
| assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 ); |
| // start timeframes |
| p = Aig_ManStart( nFrames * Abc_MaxInt(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); |
| p->pName = Abc_UtilStrsav( "frames" ); |
| // create variables for register outputs |
| pAig = pBot; |
| Saig_ManForEachLo( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( p ); |
| // add timeframes |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| // create PI nodes for this frame |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1( p ); |
| Saig_ManForEachPi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( p ); |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| if ( f == nFrames - 1 ) |
| { |
| // create POs for this frame |
| Aig_ManForEachCo( pAig, pObj, i ) |
| Aig_ObjCreateCo( p, Aig_ObjChild0Copy(pObj) ); |
| break; |
| } |
| // create POs for this frame |
| Saig_ManForEachPo( pAig, pObj, i ) |
| Aig_ObjCreateCo( p, Aig_ObjChild0Copy(pObj) ); |
| // save register inputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjChild0Copy(pObj); |
| // transfer to register outputs |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) |
| pObjLo->pData = pObjLi->pData; |
| if ( f == 0 ) |
| { |
| // transfer from pOld to pNew |
| Saig_ManForEachLo( pAig, pObj, i ) |
| Saig_ManLo(pTop, i)->pData = pObj->pData; |
| pAig = pTop; |
| } |
| } |
| Aig_ManCleanup( p ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG while creating POs from the set.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet ) |
| { |
| Aig_Man_t * pNew, * pCopy; |
| Aig_Obj_t * pObj; |
| int i; |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); |
| Aig_ManForEachCi( p, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| Aig_ManForEachNode( p, pObj, i ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // Saig_ManForEachPo( p, pObj, i ) |
| // pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i ) |
| Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) ); |
| Saig_ManForEachLi( p, pObj, i ) |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) ); |
| // cleanup and return a copy |
| Aig_ManSeqCleanup( pNew ); |
| pCopy = Aig_ManDupSimpleDfs( pNew ); |
| Aig_ManStop( pNew ); |
| return pCopy; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG while creating POs from the set.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) |
| { |
| Aig_Man_t * pNew, * pCopy; |
| Aig_Obj_t * pObj; |
| int i; |
| Aig_ManCleanData( p ); |
| pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); |
| Saig_ManForEachPi( p, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| if ( iPart == 0 ) |
| { |
| Saig_ManForEachLo( p, pObj, i ) |
| if ( i < Saig_ManRegNum(p)/2 ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| } |
| else |
| { |
| Saig_ManForEachLo( p, pObj, i ) |
| if ( i >= Saig_ManRegNum(p)/2 ) |
| pObj->pData = Aig_ObjCreateCi( pNew ); |
| } |
| Aig_ManForEachNode( p, pObj, i ) |
| if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData ) |
| pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // Saig_ManForEachPo( p, pObj, i ) |
| // pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i ) |
| { |
| assert( Aig_Regular(pObj)->pData != NULL ); |
| Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) ); |
| } |
| if ( iPart == 0 ) |
| { |
| Saig_ManForEachLi( p, pObj, i ) |
| if ( i < Saig_ManRegNum(p)/2 ) |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| } |
| else |
| { |
| Saig_ManForEachLi( p, pObj, i ) |
| if ( i >= Saig_ManRegNum(p)/2 ) |
| pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| } |
| Aig_ManSetRegNum( pNew, Saig_ManRegNum(p)/2 ); |
| // cleanup and return a copy |
| // Aig_ManSeqCleanup( pNew ); |
| Aig_ManCleanup( pNew ); |
| pCopy = Aig_ManDupSimpleDfs( pNew ); |
| Aig_ManStop( pNew ); |
| return pCopy; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG to have constant-0 initial state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) |
| { |
| Vec_Ptr_t * vSet0, * vSet1; |
| Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1; |
| int i, Counter = 0; |
| assert( Saig_ManRegNum(p) % 2 == 0 ); |
| vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| pFanin = Aig_ObjFanin0(pObj); |
| if ( Aig_ObjIsConst1( pFanin ) ) |
| { |
| if ( !Aig_ObjFaninC0(pObj) ) |
| printf( "The output number %d of the miter is constant 1.\n", i ); |
| Counter++; |
| continue; |
| } |
| if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) ) |
| { |
| printf( "The miter cannot be demitered.\n" ); |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| return 0; |
| } |
| if ( Aig_ObjFaninC0(pObj) ) |
| pObj0 = Aig_Not(pObj0); |
| |
| // printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id ); |
| if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) |
| { |
| Vec_PtrPush( vSet0, pObj0 ); |
| Vec_PtrPush( vSet1, pObj1 ); |
| } |
| else |
| { |
| Vec_PtrPush( vSet0, pObj1 ); |
| Vec_PtrPush( vSet1, pObj0 ); |
| } |
| } |
| // printf( "Miter has %d constant outputs.\n", Counter ); |
| // printf( "\n" ); |
| if ( ppAig0 ) |
| { |
| *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); |
| ABC_FREE( (*ppAig0)->pName ); |
| (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); |
| } |
| if ( ppAig1 ) |
| { |
| *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); |
| ABC_FREE( (*ppAig1)->pName ); |
| (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); |
| } |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if PO can be demitered.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManDemiterMarkPos( Aig_Man_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int i; |
| Aig_ManCleanMarkAB( p ); |
| Saig_ManForEachLo( p, pObj, i ) |
| if ( i < Saig_ManRegNum(p)/2 ) |
| pObj->fMarkA = 1; |
| else |
| pObj->fMarkB = 1; |
| Aig_ManForEachNode( p, pObj, i ) |
| { |
| pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; |
| pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB | Aig_ObjFanin1(pObj)->fMarkB; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if PO can be demitered.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiterCheckPo( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t ** ppPo0, Aig_Obj_t ** ppPo1 ) |
| { |
| Aig_Obj_t * pFanin, * pObj0, * pObj1, * pObjR0, * pObjR1; |
| assert( Saig_ObjIsPo(p, pObj) ); |
| pFanin = Aig_ObjFanin0( pObj ); |
| if ( Aig_ObjIsConst1(pFanin) ) |
| { |
| if ( !Aig_ObjFaninC0(pObj) ) |
| return 0; |
| *ppPo0 = Aig_ManConst0(p); |
| *ppPo1 = Aig_ManConst0(p); |
| return 1; |
| } |
| if ( !Aig_ObjIsNode(pFanin) ) |
| return 0; |
| if ( !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) ) |
| return 0; |
| if ( Aig_ObjFaninC0(pObj) ) |
| pObj0 = Aig_Not(pObj0); |
| // make sure they can reach only one |
| pObjR0 = Aig_Regular(pObj0); |
| pObjR1 = Aig_Regular(pObj1); |
| if ( (pObjR0->fMarkA && pObjR0->fMarkB) || (pObjR1->fMarkA && pObjR1->fMarkB) || |
| (pObjR0->fMarkA && pObjR1->fMarkA) || (pObjR0->fMarkB && pObjR1->fMarkB) ) |
| return 0; |
| |
| if ( pObjR1->fMarkA && !pObjR0->fMarkA ) |
| { |
| *ppPo0 = pObj1; |
| *ppPo1 = pObj0; |
| } |
| else if ( pObjR0->fMarkA && !pObjR1->fMarkA ) |
| { |
| *ppPo0 = pObj0; |
| *ppPo1 = pObj1; |
| } |
| else |
| { |
| /* |
| printf( "%d", pObjR0->fMarkA ); |
| printf( "%d", pObjR0->fMarkB ); |
| printf( ":" ); |
| printf( "%d", pObjR1->fMarkA ); |
| printf( "%d", pObjR1->fMarkB ); |
| printf( " " ); |
| */ |
| if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) |
| { |
| *ppPo0 = pObj0; |
| *ppPo1 = pObj1; |
| } |
| else |
| { |
| *ppPo0 = pObj1; |
| *ppPo1 = pObj0; |
| } |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if AIG can be demitered.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) |
| { |
| Vec_Ptr_t * vSet0, * vSet1; |
| Aig_Obj_t * pObj, * pObj0, * pObj1; |
| int i; |
| if ( Aig_ManRegNum(p) == 0 || (Aig_ManRegNum(p) & 1) ) |
| return 0; |
| Saig_ManDemiterMarkPos( p ); |
| vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| if ( !Saig_ManDemiterCheckPo( p, pObj, &pObj0, &pObj1 ) ) |
| { |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| Aig_ManCleanMarkAB( p ); |
| return 0; |
| } |
| Vec_PtrPush( vSet0, pObj0 ); |
| Vec_PtrPush( vSet1, pObj1 ); |
| } |
| // create new AIG |
| *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); |
| ABC_FREE( (*ppAig0)->pName ); |
| (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); |
| // create new AIGs |
| *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); |
| ABC_FREE( (*ppAig1)->pName ); |
| (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); |
| // cleanup |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| Aig_ManCleanMarkAB( p ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if AIG can be demitered.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiterDual( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) |
| { |
| Aig_Man_t * pTemp; |
| Aig_Obj_t * pObj; |
| int i, k; |
| |
| if ( p->pFanData ) |
| Aig_ManFanoutStop( p ); |
| |
| k = 0; |
| pTemp = Aig_ManDupSimple( p ); |
| Saig_ManForEachPo( pTemp, pObj, i ) |
| { |
| if ( i & 1 ) |
| Aig_ObjDeletePo( pTemp, pObj ); |
| else |
| Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); |
| } |
| Saig_ManForEachLi( pTemp, pObj, i ) |
| Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); |
| Vec_PtrShrink( pTemp->vCos, k ); |
| pTemp->nTruePos = k - Saig_ManRegNum(pTemp); |
| Aig_ManSeqCleanup( pTemp ); |
| *ppAig0 = Aig_ManDupSimple( pTemp ); |
| Aig_ManStop( pTemp ); |
| |
| k = 0; |
| pTemp = Aig_ManDupSimple( p ); |
| Saig_ManForEachPo( pTemp, pObj, i ) |
| { |
| if ( i & 1 ) |
| Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); |
| else |
| Aig_ObjDeletePo( pTemp, pObj ); |
| } |
| Saig_ManForEachLi( pTemp, pObj, i ) |
| Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); |
| Vec_PtrShrink( pTemp->vCos, k ); |
| pTemp->nTruePos = k - Saig_ManRegNum(pTemp); |
| Aig_ManSeqCleanup( pTemp ); |
| *ppAig1 = Aig_ManDupSimple( pTemp ); |
| Aig_ManStop( pTemp ); |
| |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG to have constant-0 initial state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiterSimpleDiff_old( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) |
| { |
| Vec_Ptr_t * vSet0, * vSet1; |
| Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1; |
| int i, Counter = 0; |
| // assert( Saig_ManRegNum(p) % 2 == 0 ); |
| vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| pFanin = Aig_ObjFanin0(pObj); |
| if ( Aig_ObjIsConst1( pFanin ) ) |
| { |
| if ( !Aig_ObjFaninC0(pObj) ) |
| printf( "The output number %d of the miter is constant 1.\n", i ); |
| Counter++; |
| continue; |
| } |
| if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) ) |
| { |
| /* |
| printf( "The miter cannot be demitered.\n" ); |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| return 0; |
| */ |
| printf( "The output number %d cannot be demitered.\n", i ); |
| continue; |
| } |
| if ( Aig_ObjFaninC0(pObj) ) |
| pObj0 = Aig_Not(pObj0); |
| |
| // printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id ); |
| if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) |
| { |
| Vec_PtrPush( vSet0, pObj0 ); |
| Vec_PtrPush( vSet1, pObj1 ); |
| } |
| else |
| { |
| Vec_PtrPush( vSet0, pObj1 ); |
| Vec_PtrPush( vSet1, pObj0 ); |
| } |
| } |
| // printf( "Miter has %d constant outputs.\n", Counter ); |
| // printf( "\n" ); |
| if ( ppAig0 ) |
| { |
| *ppAig0 = Aig_ManDupNodesAll( p, vSet0 ); |
| ABC_FREE( (*ppAig0)->pName ); |
| (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); |
| } |
| if ( ppAig1 ) |
| { |
| *ppAig1 = Aig_ManDupNodesAll( p, vSet1 ); |
| ABC_FREE( (*ppAig1)->pName ); |
| (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); |
| } |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Labels logic reachable from the node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManDemiterLabel_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int Value ) |
| { |
| if ( Aig_ObjIsTravIdCurrent(p, pObj) ) |
| return; |
| Aig_ObjSetTravIdCurrent(p, pObj); |
| if ( Value ) |
| pObj->fMarkB = 1; |
| else |
| pObj->fMarkA = 1; |
| if ( Saig_ObjIsPi(p, pObj) ) |
| return; |
| if ( Saig_ObjIsLo(p, pObj) ) |
| { |
| Saig_ManDemiterLabel_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p, pObj) ), Value ); |
| return; |
| } |
| assert( Aig_ObjIsNode(pObj) ); |
| Saig_ManDemiterLabel_rec( p, Aig_ObjFanin0(pObj), Value ); |
| Saig_ManDemiterLabel_rec( p, Aig_ObjFanin1(pObj), Value ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the first labeled register encountered during traversal.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Saig_ManGetLabeledRegister_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) |
| { |
| Aig_Obj_t * pResult; |
| if ( Aig_ObjIsTravIdCurrent(p, pObj) ) |
| return NULL; |
| Aig_ObjSetTravIdCurrent(p, pObj); |
| if ( Saig_ObjIsPi(p, pObj) ) |
| return NULL; |
| if ( Saig_ObjIsLo(p, pObj) ) |
| { |
| if ( pObj->fMarkA || pObj->fMarkB ) |
| return pObj; |
| return Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p, pObj) ) ); |
| } |
| assert( Aig_ObjIsNode(pObj) ); |
| pResult = Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin0(pObj) ); |
| if ( pResult ) |
| return pResult; |
| return Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin1(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG to have constant-0 initial state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) |
| { |
| Vec_Ptr_t * vPairs, * vSet0, * vSet1; |
| Aig_Obj_t * pObj, * pObj0, * pObj1, * pFlop0, * pFlop1; |
| int i, Counter; |
| assert( Saig_ManRegNum(p) > 0 ); |
| Aig_ManSetCioIds( p ); |
| // check if demitering is possible |
| vPairs = Vec_PtrAlloc( 2 * Saig_ManPoNum(p) ); |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| if ( !Aig_ObjRecognizeExor( Aig_ObjFanin0(pObj), &pObj0, &pObj1 ) ) |
| { |
| Vec_PtrFree( vPairs ); |
| return 0; |
| } |
| Vec_PtrPush( vPairs, pObj0 ); |
| Vec_PtrPush( vPairs, pObj1 ); |
| } |
| // start array of outputs |
| vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); |
| // get the first pair of outputs |
| pObj0 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, 0 ); |
| pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, 1 ); |
| // label registers reachable from the outputs |
| Aig_ManIncrementTravId( p ); |
| Saig_ManDemiterLabel_rec( p, Aig_Regular(pObj0), 0 ); |
| Vec_PtrPush( vSet0, pObj0 ); |
| Aig_ManIncrementTravId( p ); |
| Saig_ManDemiterLabel_rec( p, Aig_Regular(pObj1), 1 ); |
| Vec_PtrPush( vSet1, pObj1 ); |
| // find where each output belongs |
| for ( i = 2; i < Vec_PtrSize(vPairs); i += 2 ) |
| { |
| pObj0 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, i ); |
| pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, i+1 ); |
| |
| Aig_ManIncrementTravId( p ); |
| pFlop0 = Saig_ManGetLabeledRegister_rec( p, Aig_Regular(pObj0) ); |
| |
| Aig_ManIncrementTravId( p ); |
| pFlop1 = Saig_ManGetLabeledRegister_rec( p, Aig_Regular(pObj1) ); |
| |
| if ( (pFlop0->fMarkA && pFlop0->fMarkB) || (pFlop1->fMarkA && pFlop1->fMarkB) || |
| (pFlop0->fMarkA && pFlop1->fMarkA) || (pFlop0->fMarkB && pFlop1->fMarkB) ) |
| printf( "Ouput pair %4d: Difficult case...\n", i/2 ); |
| |
| if ( pFlop0->fMarkB ) |
| { |
| Saig_ManDemiterLabel_rec( p, pObj0, 1 ); |
| Vec_PtrPush( vSet0, pObj0 ); |
| } |
| else // if ( pFlop0->fMarkA ) or none |
| { |
| Saig_ManDemiterLabel_rec( p, pObj0, 0 ); |
| Vec_PtrPush( vSet1, pObj0 ); |
| } |
| |
| if ( pFlop1->fMarkB ) |
| { |
| Saig_ManDemiterLabel_rec( p, pObj1, 1 ); |
| Vec_PtrPush( vSet0, pObj1 ); |
| } |
| else // if ( pFlop1->fMarkA ) or none |
| { |
| Saig_ManDemiterLabel_rec( p, pObj1, 0 ); |
| Vec_PtrPush( vSet1, pObj1 ); |
| } |
| } |
| // check if there are any flops in common |
| Counter = 0; |
| Saig_ManForEachLo( p, pObj, i ) |
| if ( pObj->fMarkA && pObj->fMarkB ) |
| Counter++; |
| if ( Counter > 0 ) |
| printf( "The miters contains %d flops reachable from both AIGs.\n", Counter ); |
| |
| // produce two miters |
| if ( ppAig0 ) |
| { |
| assert( 0 ); |
| *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready |
| ABC_FREE( (*ppAig0)->pName ); |
| (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); |
| } |
| if ( ppAig1 ) |
| { |
| assert( 0 ); |
| *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready |
| ABC_FREE( (*ppAig1)->pName ); |
| (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); |
| } |
| Vec_PtrFree( vSet0 ); |
| Vec_PtrFree( vSet1 ); |
| Vec_PtrFree( vPairs ); |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Create specialized miter by unrolling two circuits.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames ) |
| { |
| Aig_Man_t * pFrames0, * pFrames1, * pMiter; |
| // assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) ); |
| pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames ); |
| pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames ); |
| pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 ); |
| Aig_ManStop( pFrames0 ); |
| Aig_ManStop( pFrames1 ); |
| return pMiter; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Resimulates counter-example and returns the failed output number.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ) |
| { |
| Aig_Obj_t * pObj; |
| int i, RetValue = -1; |
| *pnOutputs = 0; |
| Aig_ManConst1(p)->fMarkA = 1; |
| Aig_ManForEachCi( p, pObj, i ) |
| pObj->fMarkA = pModel[i]; |
| Aig_ManForEachNode( p, pObj, i ) |
| pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) & |
| ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) ); |
| Aig_ManForEachCo( p, pObj, i ) |
| pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj); |
| Aig_ManForEachCo( p, pObj, i ) |
| if ( pObj->fMarkA ) |
| { |
| if ( RetValue == -1 ) |
| RetValue = i; |
| (*pnOutputs)++; |
| } |
| Aig_ManCleanMarkA(p); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces SEC to CEC for the special case of seq synthesis.] |
| |
| Description [The first circuit (pPart0) should be circuit before synthesis. |
| The second circuit (pPart1) should be circuit after synthesis.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose ) |
| { |
| // extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); |
| int iOut, nOuts; |
| Aig_Man_t * pMiterCec; |
| int RetValue; |
| abctime clkTotal = Abc_Clock(); |
| if ( fVerbose ) |
| { |
| Aig_ManPrintStats( pPart0 ); |
| Aig_ManPrintStats( pPart1 ); |
| } |
| // Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL ); |
| // Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL ); |
| // assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) ); |
| /* |
| if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) ) |
| { |
| printf( "Warning: The design after synthesis is smaller!\n" ); |
| printf( "This warning may indicate that the order of designs is changed.\n" ); |
| printf( "The solver expects the original design as first argument and\n" ); |
| printf( "the modified design as the second argument in \"absec\".\n" ); |
| } |
| */ |
| // create two-level miter |
| pMiterCec = Saig_ManCreateMiterTwo( pPart0, pPart1, nFrames ); |
| if ( fVerbose ) |
| { |
| Aig_ManPrintStats( pMiterCec ); |
| // Aig_ManDumpBlif( pMiterCec, "miter01.blif", NULL, NULL ); |
| // printf( "The new miter is written into file \"%s\".\n", "miter01.blif" ); |
| } |
| // run CEC on this miter |
| RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose ); |
| // transfer model if given |
| // if ( pNtk2 == NULL ) |
| // pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL; |
| // report the miter |
| if ( RetValue == 1 ) |
| { |
| printf( "Networks are equivalent. " ); |
| ABC_PRT( "Time", Abc_Clock() - clkTotal ); |
| } |
| else if ( RetValue == 0 ) |
| { |
| printf( "Networks are NOT EQUIVALENT. " ); |
| ABC_PRT( "Time", Abc_Clock() - clkTotal ); |
| if ( pMiterCec->pData == NULL ) |
| printf( "Counter-example is not available.\n" ); |
| else |
| { |
| iOut = Ssw_SecCexResimulate( pMiterCec, (int *)pMiterCec->pData, &nOuts ); |
| if ( iOut == -1 ) |
| printf( "Counter-example verification has failed.\n" ); |
| else |
| { |
| if ( iOut < Saig_ManPoNum(pPart0) * nFrames ) |
| printf( "Primary output %d has failed in frame %d.\n", |
| iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) ); |
| else |
| printf( "Flop input %d has failed in the last frame.\n", |
| iOut - Saig_ManPoNum(pPart0) * nFrames ); |
| printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts ); |
| } |
| } |
| } |
| else |
| { |
| printf( "Networks are UNDECIDED. " ); |
| ABC_PRT( "Time", Abc_Clock() - clkTotal ); |
| } |
| fflush( stdout ); |
| Aig_ManStop( pMiterCec ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces SEC to CEC for the special case of seq synthesis.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose ) |
| { |
| Aig_Man_t * pPart0, * pPart1; |
| int RetValue; |
| if ( fVerbose ) |
| printf( "Performing sequential verification using combinational A/B miter.\n" ); |
| // consider the case when a miter is given |
| if ( p1 == NULL ) |
| { |
| if ( fVerbose ) |
| { |
| Aig_ManPrintStats( p0 ); |
| } |
| // demiter the miter |
| if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) ) |
| { |
| printf( "Demitering has failed.\n" ); |
| return -1; |
| } |
| if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) ) |
| { |
| Aig_ManStop( pPart0 ); |
| Aig_ManStop( pPart1 ); |
| printf( "After demitering AIGs have different number of flops. Quitting.\n" ); |
| return -1; |
| } |
| } |
| else |
| { |
| pPart0 = Aig_ManDupSimple( p0 ); |
| pPart1 = Aig_ManDupSimple( p1 ); |
| } |
| if ( fVerbose ) |
| { |
| // Aig_ManPrintStats( pPart0 ); |
| // Aig_ManPrintStats( pPart1 ); |
| if ( p1 == NULL ) |
| { |
| // Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); |
| // Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); |
| // printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); |
| } |
| } |
| assert( Aig_ManRegNum(pPart0) > 0 ); |
| assert( Aig_ManRegNum(pPart1) > 0 ); |
| assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) ); |
| assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) ); |
| assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) ); |
| RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose ); |
| if ( RetValue != 1 && Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) ) |
| RetValue = Ssw_SecSpecial( pPart1, pPart0, nFrames, fVerbose ); |
| Aig_ManStop( pPart0 ); |
| Aig_ManStop( pPart1 ); |
| return RetValue; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs demitering of the network.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManDemiterNew( Aig_Man_t * pMan ) |
| { |
| Vec_Ptr_t * vSuper, * vSupp0, * vSupp1; |
| Aig_Obj_t * pObj, * pTemp, * pFan0, * pFan1; |
| int i, k; |
| vSuper = Vec_PtrAlloc( 100 ); |
| Saig_ManForEachPo( pMan, pObj, i ) |
| { |
| if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs ) |
| break; |
| printf( "Output %3d : ", i ); |
| if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) |
| { |
| if ( !Aig_ObjFaninC0(pObj) ) |
| printf( "Const1\n" ); |
| else |
| printf( "Const0\n" ); |
| continue; |
| } |
| if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) ) |
| { |
| printf( "Terminal\n" ); |
| continue; |
| } |
| // check AND |
| if ( !Aig_ObjFaninC0(pObj) ) |
| { |
| printf( "AND " ); |
| if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) ) |
| printf( " Yes" ); |
| else |
| printf( " No" ); |
| printf( "\n" ); |
| continue; |
| } |
| // check OR |
| Aig_ObjCollectSuper( Aig_ObjFanin0(pObj), vSuper ); |
| printf( "OR with %d inputs ", Vec_PtrSize(vSuper) ); |
| if ( Vec_PtrSize(vSuper) == 2 ) |
| { |
| if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) ) |
| { |
| printf( " Yes" ); |
| printf( "\n" ); |
| |
| vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k ) |
| if ( Saig_ObjIsLo(pMan, pTemp) ) |
| printf( " %d", Aig_ObjCioId(pTemp) ); |
| printf( "\n" ); |
| Vec_PtrFree( vSupp0 ); |
| |
| vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k ) |
| if ( Saig_ObjIsLo(pMan, pTemp) ) |
| printf( " %d", Aig_ObjCioId(pTemp) ); |
| printf( "\n" ); |
| Vec_PtrFree( vSupp1 ); |
| } |
| else |
| printf( " No" ); |
| printf( "\n" ); |
| continue; |
| } |
| /* |
| Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k ) |
| if ( Aig_ObjRecognizeExor(Aig_Regular(pTemp), &pFan0, &pFan1) ) |
| { |
| printf( " Yes" ); |
| if ( Aig_IsComplement(pTemp) ) |
| pFan0 = Aig_Not(pFan0); |
| } |
| else |
| printf( " No" ); |
| */ |
| printf( "\n" ); |
| } |
| Vec_PtrFree( vSuper ); |
| return 1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
