saigDup.c File Reference

#include "saig.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Saig_ManDupOrpos (Aig_Man_t *pAig)
	DECLARATIONS ///. More...
Aig_Man_t *	Saig_ManCreateEquivMiter (Aig_Man_t *pAig, Vec_Int_t *vPairs)
Aig_Man_t *	Saig_ManTrimPis (Aig_Man_t *p)
Aig_Obj_t *	Saig_ManAbstractionDfs_rec (Aig_Man_t *pNew, Aig_Obj_t *pObj)
Aig_Man_t *	Saig_ManDupAbstraction (Aig_Man_t *p, Vec_Int_t *vFlops)
int	Saig_ManVerifyCex (Aig_Man_t *pAig, Abc_Cex_t *p)
int	Saig_ManVerifyCexNoClear (Aig_Man_t *pAig, Abc_Cex_t *p)
Vec_Int_t *	Saig_ManReturnFailingState (Aig_Man_t *pAig, Abc_Cex_t *p, int fNextOne)
Abc_Cex_t *	Saig_ManExtendCex (Aig_Man_t *pAig, Abc_Cex_t *p)
int	Saig_ManFindFailedPoCex (Aig_Man_t *pAig, Abc_Cex_t *p)
Aig_Man_t *	Saig_ManDupWithPhase (Aig_Man_t *pAig, Vec_Int_t *vInit)
void	Saig_ManDupCones_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Ptr_t *vRoots)
Aig_Man_t *	Saig_ManDupCones (Aig_Man_t *pAig, int *pPos, int nPos)

Function Documentation

Aig_Obj_t* Saig_ManAbstractionDfs_rec	(	Aig_Man_t *	pNew,
		Aig_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Duplicates the AIG manager recursively.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file saigDup.c.

{
    if ( pObj->pData )
        return (Aig_Obj_t *)pObj->pData;
    Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
    Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
}

Aig_Man_t* Saig_ManCreateEquivMiter	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vPairs
	)

Function*************************************************************

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pObj2, * pMiter;
    int i;
    if ( pAig->nConstrs > 0 )
    {
        printf( "The AIG manager should have no constraints.\n" );
        return NULL;
    }
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create POs
    assert( Vec_IntSize(vPairs) % 2 == 0 );
    Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
    {
        pObj2  = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
        pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
        pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

Aig_Man_t* Saig_ManDupAbstraction	(	Aig_Man_t *	p,
		Vec_Int_t *	vFlops
	)

Function*************************************************************

Synopsis [Performs abstraction of the AIG to preserve the included flops.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file saigDup.c.

{ 
    Aig_Man_t * pNew;//, * pTemp;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, Entry;
    Aig_ManCleanData( p );
    // start the new manager
    pNew = Aig_ManStart( 5000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    // map the constant node
    Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
    // label included flops
    Vec_IntForEachEntry( vFlops, Entry, i )
    {
        pObjLi = Saig_ManLi( p, Entry );
        assert( pObjLi->fMarkA == 0 );
        pObjLi->fMarkA = 1;
        pObjLo = Saig_ManLo( p, Entry );
        assert( pObjLo->fMarkA == 0 );
        pObjLo->fMarkA = 1;
    }
    // create variables for PIs
    assert( p->vCiNumsOrig == NULL );
    pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
    Aig_ManForEachCi( p, pObj, i )
        if ( !pObj->fMarkA )
        {
            pObj->pData = Aig_ObjCreateCi( pNew );
            Vec_IntPush( pNew->vCiNumsOrig, i );
        }
    // create variables for LOs
    Aig_ManForEachCi( p, pObj, i )
        if ( pObj->fMarkA )
        {
            pObj->fMarkA = 0;
            pObj->pData = Aig_ObjCreateCi( pNew );
            Vec_IntPush( pNew->vCiNumsOrig, i );
        }
    // add internal nodes 
//    Aig_ManForEachNode( p, pObj, i )
//        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create POs
    Saig_ManForEachPo( p, pObj, i )
    {
        Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    // create LIs
    Aig_ManForEachCo( p, pObj, i )
        if ( pObj->fMarkA )
        {
            pObj->fMarkA = 0;
            Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
            Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
        }
    Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
    Aig_ManSeqCleanup( pNew );
    // remove PIs without fanout
//    pNew = Saig_ManTrimPis( pTemp = pNew );
//    Aig_ManStop( pTemp );
    return pNew;
}

Aig_Man_t* Saig_ManDupCones	(	Aig_Man_t *	pAig,
		int *	pPos,
		int	nPos
	)

Definition at line 543 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
    Aig_Obj_t * pObj;
    int i;

    // collect initial POs
    vLeaves = Vec_PtrAlloc( 100 );
    vNodes = Vec_PtrAlloc( 100 );
    vRoots = Vec_PtrAlloc( 100 );
    for ( i = 0; i < nPos; i++ )
        Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );

    // mark internal nodes
    Aig_ManIncrementTravId( pAig );
    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );

    // start the new manager
    pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create PIs
    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // create LOs
    Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
        Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
    // create internal nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create COs
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // finalize
    Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
    Vec_PtrFree( vLeaves );
    Vec_PtrFree( vNodes );
    Vec_PtrFree( vRoots );
    return pAigNew;

}

void Saig_ManDupCones_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vNodes,
		Vec_Ptr_t *	vRoots
	)

Function*************************************************************

Synopsis [Copy an AIG structure related to the selected POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 524 of file saigDup.c.

{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsNode(pObj) )
    {
        Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
        Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
        Vec_PtrPush( vNodes, pObj );
    }
    else if ( Aig_ObjIsCo(pObj) )
        Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
    else if ( Saig_ObjIsLo(p, pObj) )
        Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
    else if ( Saig_ObjIsPi(p, pObj) )
        Vec_PtrPush( vLeaves, pObj );
    else assert( 0 );
}

ABC_NAMESPACE_IMPL_START Aig_Man_t* Saig_ManDupOrpos

(

Aig_Man_t *

pAig

)

DECLARATIONS ///.

CFile****************************************************************

FileName [saigDup.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Various duplication procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

saigDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj, * pMiter;
    int i;
    if ( pAig->nConstrs > 0 )
    {
        printf( "The AIG manager should have no constraints.\n" );
        return NULL;
    }
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create PO of the circuit
    pMiter = Aig_ManConst0( pAigNew );
    Saig_ManForEachPo( pAig, pObj, i )
        pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
    Aig_ObjCreateCo( pAigNew, pMiter );
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

Aig_Man_t* Saig_ManDupWithPhase	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vInit
	)

Function*************************************************************

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file saigDup.c.

{
    Aig_Man_t * pAigNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // update the flop variables
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // transfer to register outputs
    Saig_ManForEachPo( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // update the flop variables
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
    // finalize
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

Abc_Cex_t* Saig_ManExtendCex	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p
	)

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file saigDup.c.

{
    Abc_Cex_t * pNew;
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    // create new counter-example
    pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
    pNew->iPo = p->iPo;
    pNew->iFrame = p->iFrame;
    // simulate the AIG
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        ///////// write PI+LO values ////////////
        Aig_ManForEachCi( pAig, pObj, k )
            if ( pObj->fMarkB )
                Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
        /////////////////////////////////////////
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
    Aig_ManCleanMarkB(pAig);
    if ( RetValue == 0 )
        printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
    return pNew;
}

int Saig_ManFindFailedPoCex	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p
	)

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 434 of file saigDup.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    // remember the number of failed output
    RetValue = -1;
    Saig_ManForEachPo( pAig, pObj, i )
        if ( pObj->fMarkB )
        {
            RetValue = i;
            break;
        }
    Aig_ManCleanMarkB(pAig);
    return RetValue;
}

Vec_Int_t* Saig_ManReturnFailingState	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p,
		int	fNextOne
	)

Definition at line 345 of file saigDup.c.

{
    Aig_Obj_t * pObj;
    Vec_Int_t * vState;
    int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
    if ( RetValue == 0 )
    {
        Aig_ManCleanMarkB(pAig);
        printf( "CEX does fail the given sequential miter.\n" );
        return NULL;
    }
    vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    if ( fNextOne )
    {
        Saig_ManForEachLi( pAig, pObj, i )
            Vec_IntPush( vState, pObj->fMarkB );
    }
    else
    {
        Saig_ManForEachLo( pAig, pObj, i )
            Vec_IntPush( vState, pObj->fMarkB );
    }
    Aig_ManCleanMarkB(pAig);
    return vState;
}

Aig_Man_t* Saig_ManTrimPis

(

Aig_Man_t *

p

)

Function*************************************************************

Synopsis [Trims the model by removing PIs without fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file saigDup.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i, fAllPisHaveNoRefs;
    // check the refs of PIs    
    fAllPisHaveNoRefs = 1;
    Saig_ManForEachPi( p, pObj, i )
        if ( pObj->nRefs )
            fAllPisHaveNoRefs = 0;
    // start the new manager
    pNew = Aig_ManStart( Aig_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->nConstrs = p->nConstrs;
    // start mapping of the CI numbers
    pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
    // map const and primary inputs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
        if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) )
        {
            pObj->pData = Aig_ObjCreateCi( pNew );
            Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) );
        }
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    Aig_ManForEachCo( p, pObj, i )
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    return pNew;
}

int Saig_ManVerifyCex	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p
	)

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file saigDup.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
    Aig_ManCleanMarkB(pAig);
    return RetValue;
}

int Saig_ManVerifyCexNoClear	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	p
	)

Function*************************************************************

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file saigDup.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int RetValue, i, k, iBit = 0;
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
    for ( i = 0; i <= p->iFrame; i++ )
    {
        Saig_ManForEachPi( pAig, pObj, k )
            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        if ( i == p->iFrame )
            break;
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == p->nBits );
    RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
    //Aig_ManCleanMarkB(pAig);
    return RetValue;
}