pdrTsim2.c File Reference

#include "pdrInt.h"
#include "aig/gia/giaAig.h"

Include dependency graph for pdrTsim2.c:

Go to the source code of this file.

Classes
struct	Txs_Man_t_
	DECLARATIONS ///. More...

Functions
Txs_Man_t *	Txs_ManStart (Pdr_Man_t *pMan, Aig_Man_t *pAig, Vec_Int_t *vPrio)
	FUNCTION DEFINITIONS ///.
void	Txs_ManStop (Txs_Man_t *p)
void	Txs_ManCollectCone_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes)
void	Txs_ManCollectCone (Gia_Man_t *p, Vec_Int_t *vCoObjs, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes)
void	Txs_ManForwardPass (Gia_Man_t *p, Vec_Int_t *vPrio, Vec_Int_t *vCiObjs, Vec_Int_t *vCiVals, Vec_Int_t *vNodes, Vec_Int_t *vCoObjs, Vec_Int_t *vCoVals)
void	Txs_ManBackwardPass (Gia_Man_t *p, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes, Vec_Int_t *vPiLits, Vec_Int_t *vFfLits)
void	Txs_ManSelectJustPath (Gia_Man_t *p, Vec_Int_t *vNodes, Vec_Int_t *vCoObjs, Vec_Int_t *vRes)
void	Txs_ManCollectJustPis (Gia_Man_t *p, Vec_Int_t *vCiObjs, Vec_Int_t *vPiLits)
void	Txs_ManInitPrio (Gia_Man_t *p, Vec_Int_t *vCiObjs)
void	Txs_ManPropagatePrio (Gia_Man_t *p, Vec_Int_t *vNodes, Vec_Int_t *vPrio)
int	Txs_ManFindMinId (Gia_Man_t *p, Vec_Int_t *vCoObjs, Vec_Int_t *vPrio)
void	Txs_ManFindCiReduction (Gia_Man_t *p, Vec_Int_t *vPrio, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes, Vec_Int_t *vCoObjs, Vec_Int_t *vPiLits, Vec_Int_t *vFfLits, Vec_Int_t *vTemp)
void	Txs_ManPrintFlopLits (Vec_Int_t *vFfLits, Vec_Int_t *vPrio)
void	Txs_ManVerify (Gia_Man_t *p, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes, Vec_Int_t *vPiLits, Vec_Int_t *vFfLits, Vec_Int_t *vCoObjs, Vec_Int_t *vCoVals)
Pdr_Set_t *	Txs_ManTernarySim (Txs_Man_t *p, int k, Pdr_Set_t *pCube)

Function Documentation

Txs_ManBackwardPass()

void Txs_ManBackwardPass	(	Gia_Man_t *	p,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vPiLits,
		Vec_Int_t *	vFfLits )

Definition at line 217 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj, * pFan0, * pFan1; int i, value0, value1;
    Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
    {
        if ( !pObj->fMark1 )
            continue;
        pObj->fMark1 = 0;
        pFan0 = Gia_ObjFanin0(pObj);
        pFan1 = Gia_ObjFanin1(pObj);
        if ( pObj->fMark0 )
        {
            pFan0->fMark1 = 1;
            pFan1->fMark1 = 1;
            continue;
        }
        value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
        value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
        assert( !value0 || !value1 );
        if ( value0 )
            pFan1->fMark1 = 1;
        else if ( value1 )
            pFan0->fMark1 = 1;
        else // if ( !value0 && !value1 )
        {
            if ( pFan0->fMark1 || pFan1->fMark1 )
                continue;
            if ( Gia_ObjIsPi(p, pFan0) )
                pFan0->fMark1 = 1;
            else if ( Gia_ObjIsPi(p, pFan1) )
                pFan1->fMark1 = 1;
            else if ( Gia_ObjIsAnd(pFan0) && Txs_ObjIsJust(p, pFan0) )
                pFan0->fMark1 = 1;
            else if ( Gia_ObjIsAnd(pFan1) && Txs_ObjIsJust(p, pFan1) )
                pFan1->fMark1 = 1;
            else
            {
                if ( pFan0->Value >= pFan1->Value )
                    pFan0->fMark1 = 1;
                else
                    pFan1->fMark1 = 1;
            }
        }
    }
    Vec_IntClear( vPiLits );
    Vec_IntClear( vFfLits );
    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
    {
        if ( !pObj->fMark1 )
            continue;
        if ( Gia_ObjIsPi(p, pObj) )
            Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj),                 !pObj->fMark0) );
        else
            Vec_IntPush( vFfLits, Abc_Var2Lit(Gia_ObjCioId(pObj)-Gia_ManPiNum(p), !pObj->fMark0) );
    }
    assert( Vec_IntSize(vFfLits) > 0 );
}

Here is the caller graph for this function:

Txs_ManCollectCone()

void Txs_ManCollectCone	(	Gia_Man_t *	p,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes )

Definition at line 123 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj; int i;
//    printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
    Vec_IntClear( vCiObjs );
    Vec_IntClear( vNodes );
    Gia_ManConst0(p)->Value = ~0;
    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
        Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Txs_ManCollectCone_rec()

void Txs_ManCollectCone_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes )

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

Synopsis [Marks the TFI cone and collects CIs and nodes.]

Description [For this procedure to work Value should not be ~0 at the beginning.]

SideEffects []

SeeAlso []

Definition at line 108 of file pdrTsim2.c.

{
    if ( !~pObj->Value )
        return;
    pObj->Value = ~0;
    if ( Gia_ObjIsCi(pObj) )
    {
        Vec_IntPush( vCiObjs, Gia_ObjId(p, pObj) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
    Txs_ManCollectCone_rec( p, Gia_ObjFanin1(pObj), vCiObjs, vNodes );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Txs_ManCollectJustPis()

void Txs_ManCollectJustPis	(	Gia_Man_t *	p,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vPiLits )

Definition at line 324 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj; int i;
    Vec_IntClear( vPiLits );
    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
        if ( pObj->fMark1 && Gia_ObjIsPi(p, pObj) )
            Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj), !pObj->fMark0) );
}

Here is the caller graph for this function:

Txs_ManFindCiReduction()

void Txs_ManFindCiReduction	(	Gia_Man_t *	p,
		Vec_Int_t *	vPrio,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vPiLits,
		Vec_Int_t *	vFfLits,
		Vec_Int_t *	vTemp )

Definition at line 391 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj;
    int iPrioCi;
    // propagate PI influence
    Txs_ManSelectJustPath( p, vNodes, vCoObjs, vTemp );
    Txs_ManCollectJustPis( p, vCiObjs, vPiLits );
//    printf( "%d -> %d  ", Vec_IntSize(vNodes), Vec_IntSize(vTemp) );
    // iteratively detect and remove smallest IDs
    Vec_IntClear( vFfLits );
    Txs_ManInitPrio( p, vCiObjs );
    while ( 1 )
    {
        Txs_ManPropagatePrio( p, vTemp, vPrio );
        iPrioCi = Txs_ManFindMinId( p, vCoObjs, vPrio );
        if ( iPrioCi == -1 )
            break;
        pObj = Gia_ManCi( p, Gia_ManPiNum(p)+iPrioCi );
        Vec_IntPush( vFfLits, Abc_Var2Lit(iPrioCi, !pObj->fMark0) );
        pObj->Value = 0x7FFFFFFF;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Txs_ManFindMinId()

int Txs_ManFindMinId	(	Gia_Man_t *	p,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vPrio )

Definition at line 380 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj; int i, iMinId = -1;
    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
        if ( Gia_ObjFanin0(pObj)->Value != 0x7FFFFFFF )
        {
            if ( iMinId == -1 || Vec_IntEntry(vPrio, iMinId) > Vec_IntEntry(vPrio, Gia_ObjFanin0(pObj)->Value) )
                iMinId = Gia_ObjFanin0(pObj)->Value;
        }
    return iMinId;
}

Here is the caller graph for this function:

Txs_ManForwardPass()

void Txs_ManForwardPass	(	Gia_Man_t *	p,
		Vec_Int_t *	vPrio,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vCiVals,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vCoVals )

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

Synopsis [Propagate values and assign priority.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj, * pFan0, * pFan1; 
    int i, value0, value1;
    pObj = Gia_ManConst0(p);
    pObj->fMark0 = 0;
    pObj->fMark1 = 0;
    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
    {
        pObj->fMark0 = Vec_IntEntry(vCiVals, i);
        pObj->fMark1 = 0;
        pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Vec_IntEntry(vPrio, Gia_ObjCioId(pObj)-Gia_ManPiNum(p));
        assert( ~pObj->Value );
    }
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
    {
        pFan0 = Gia_ObjFanin0(pObj);
        pFan1 = Gia_ObjFanin1(pObj);
        value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
        value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
        pObj->fMark0 = value0 && value1;
        pObj->fMark1 = 0;
        if ( pObj->fMark0 )
            pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
        else if ( value0 )
            pObj->Value = pFan1->Value;
        else if ( value1 )
            pObj->Value = pFan0->Value;
        else // if ( value0 == 0 && value1 == 0 )
            pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
        assert( ~pObj->Value );
    }
    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
    {
        pFan0 = Gia_ObjFanin0(pObj);
        pObj->fMark0 = (pFan0->fMark0 ^ Gia_ObjFaninC0(pObj));
        pFan0->fMark1 = 1;
        assert( (int)pObj->fMark0 == Vec_IntEntry(vCoVals, i) );
    }
}

Here is the caller graph for this function:

Txs_ManInitPrio()

void Txs_ManInitPrio	(	Gia_Man_t *	p,
		Vec_Int_t *	vCiObjs )

Definition at line 332 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj; int i;
    Gia_ManConst0(p)->Value = 0x7FFFFFFF;
    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
        pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
}

Here is the caller graph for this function:

Txs_ManPrintFlopLits()

void Txs_ManPrintFlopLits	(	Vec_Int_t *	vFfLits,
		Vec_Int_t *	vPrio )

Definition at line 416 of file pdrTsim2.c.

{
    int i, Entry;
    printf( "%3d : ", Vec_IntSize(vFfLits) );
    Vec_IntForEachEntry( vFfLits, Entry, i )
        printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "+":"-", Abc_Lit2Var(Entry), Vec_IntEntry(vPrio, Abc_Lit2Var(Entry)) );
    printf( "\n" );
}

Txs_ManPropagatePrio()

void Txs_ManPropagatePrio	(	Gia_Man_t *	p,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vPrio )

Definition at line 339 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj, * pFan0, * pFan1;
    int i, value0, value1;
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
    {
        pFan0 = Gia_ObjFanin0(pObj);
        pFan1 = Gia_ObjFanin1(pObj);
        if ( pObj->fMark0 )
        {
//            pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
            if ( pFan0->Value == 0x7FFFFFFF )
                pObj->Value = pFan1->Value;
            else if ( pFan1->Value == 0x7FFFFFFF )
                pObj->Value = pFan0->Value;
            else if ( Vec_IntEntry(vPrio, pFan0->Value) < Vec_IntEntry(vPrio, pFan1->Value) )
                pObj->Value = pFan0->Value;
            else
                pObj->Value = pFan1->Value;
            continue;
        }
        value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
        value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
        assert( !value0 || !value1 );
        if ( value0 )
            pObj->Value = pFan1->Value;
        else if ( value1 )
            pObj->Value = pFan0->Value;
        else // if ( value0 == 0 && value1 == 0 )
        {
//            pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
            if ( pFan0->Value == 0x7FFFFFFF || pFan1->Value == 0x7FFFFFFF )
                pObj->Value = 0x7FFFFFFF;
            else if ( Vec_IntEntry(vPrio, pFan0->Value) >= Vec_IntEntry(vPrio, pFan1->Value) )
                pObj->Value = pFan0->Value;
            else
                pObj->Value = pFan1->Value;
        }
        assert( ~pObj->Value );
    }
}

Here is the caller graph for this function:

Txs_ManSelectJustPath()

void Txs_ManSelectJustPath	(	Gia_Man_t *	p,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vRes )

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

Synopsis [Collects justification path.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj, * pFan0, * pFan1; 
    int i, value0, value1;
    // mark CO drivers
    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
        Gia_ObjFanin0(pObj)->fMark1 = 1;
    // collect just paths
    Vec_IntClear( vRes );
    Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
    {
        if ( !pObj->fMark1 )
            continue;
        pObj->fMark1 = 0;
        Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
        pFan0 = Gia_ObjFanin0(pObj);
        pFan1 = Gia_ObjFanin1(pObj);
        if ( pObj->fMark0 )
        {
            pFan0->fMark1 = 1;
            pFan1->fMark1 = 1;
            continue;
        }
        value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
        value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
        assert( !value0 || !value1 );
        if ( value0 )
            pFan1->fMark1 = 1;
        else if ( value1 )
            pFan0->fMark1 = 1;
        else // if ( !value0 && !value1 )
        {
            pFan0->fMark1 = 1;
            pFan1->fMark1 = 1;
        }
    }
    Vec_IntReverseOrder( vRes );
}

Here is the caller graph for this function:

Txs_ManStart()

Txs_Man_t * Txs_ManStart	(	Pdr_Man_t *	pMan,
		Aig_Man_t *	pAig,
		Vec_Int_t *	vPrio )

FUNCTION DEFINITIONS ///.

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

Synopsis [Start and stop the ternary simulation engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file pdrTsim2.c.

{
    Txs_Man_t * p;
//    Aig_Obj_t * pObj;
//    int i;
    assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
    p = ABC_CALLOC( Txs_Man_t, 1 );
    p->pGia    = Gia_ManFromAigSimple(pAig); // user's AIG
//    Aig_ManForEachObj( pAig, pObj, i )
//        assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
    p->vPrio   = vPrio;                // priority of each flop
    p->vCiObjs = Vec_IntAlloc( 100 );  // cone leaves (CI obj IDs)
    p->vCoObjs = Vec_IntAlloc( 100 );  // cone roots (CO obj IDs)
    p->vCiVals = Vec_IntAlloc( 100 );  // cone leaf values (0/1 CI values)
    p->vCoVals = Vec_IntAlloc( 100 );  // cone root values (0/1 CO values)
    p->vNodes  = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
    p->vTemp   = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
    p->vPiLits = Vec_IntAlloc( 100 );  // resulting array of PI literals
    p->vFfLits = Vec_IntAlloc( 100 );  // resulting array of flop literals
    p->pMan    = pMan;                 // calling manager
    return p;
}

Here is the call graph for this function:

Txs_ManStop()

void Txs_ManStop

(

Txs_Man_t *

p

)

Definition at line 82 of file pdrTsim2.c.

{
    Gia_ManStop( p->pGia );
    Vec_IntFree( p->vCiObjs );
    Vec_IntFree( p->vCoObjs );
    Vec_IntFree( p->vCiVals );
    Vec_IntFree( p->vCoVals );
    Vec_IntFree( p->vNodes );
    Vec_IntFree( p->vTemp );
    Vec_IntFree( p->vPiLits );
    Vec_IntFree( p->vFfLits );
    ABC_FREE( p );
}

Here is the call graph for this function:

Txs_ManTernarySim()

Pdr_Set_t * Txs_ManTernarySim	(	Txs_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube )

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

Synopsis [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which, when converted into a clause and applied to the combinational outputs, led to a satisfiable SAT run in frame k (values stored in the SAT solver). If the cube is NULL, it is assumed that the first property output was asserted and failed. The resulting array is a set of flop index literals that asserts the COs. Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]

SideEffects []

SeeAlso []

Definition at line 490 of file pdrTsim2.c.

{
    int fTryNew = 1;
    Pdr_Set_t * pRes;
    Gia_Obj_t * pObj;
    // collect CO objects
    Vec_IntClear( p->vCoObjs );
    if ( pCube == NULL ) // the target is the property output
    {
        pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
        Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
    }
    else // the target is the cube
    {
        int i;
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
            Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
        }
    }
if ( 0 )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
 
    // collect CI objects
    Txs_ManCollectCone( p->pGia, p->vCoObjs, p->vCiObjs, p->vNodes );
    // collect values
    Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
    Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
 
    // perform two passes
    Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals );
    if ( fTryNew )
        Txs_ManFindCiReduction( p->pGia, p->vPrio, p->vCiObjs, p->vNodes, p->vCoObjs, p->vPiLits, p->vFfLits, p->vTemp );
    else
        Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits );
    Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals );
 
    // derive the final set
    pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
    //ZH: Disabled assertion because this invariant doesn't hold with down
    //because of the join operation which can bring in initial states
    //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
    return pRes;
}

Here is the call graph for this function:

Txs_ManVerify()

void Txs_ManVerify	(	Gia_Man_t *	p,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vPiLits,
		Vec_Int_t *	vFfLits,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vCoVals )

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

Synopsis [Verify the result.]

Description []

SideEffects []

SeeAlso []

Definition at line 436 of file pdrTsim2.c.

{
    Gia_Obj_t * pObj;
    int i, iLit;
    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
    Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
        Gia_ObjTerSimSetX( pObj );
    Vec_IntForEachEntry( vPiLits, iLit, i )
    {
        pObj = Gia_ManPi( p, Abc_Lit2Var(iLit) );
        assert( Gia_ObjTerSimGetX(pObj) );
        if ( Abc_LitIsCompl(iLit) )
            Gia_ObjTerSimSet0( pObj );
        else
            Gia_ObjTerSimSet1( pObj );
    }
    Vec_IntForEachEntry( vFfLits, iLit, i )
    {
        pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Abc_Lit2Var(iLit) );
        assert( Gia_ObjTerSimGetX(pObj) );
        if ( Abc_LitIsCompl(iLit) )
            Gia_ObjTerSimSet0( pObj );
        else
            Gia_ObjTerSimSet1( pObj );
    }
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        Gia_ObjTerSimAnd( pObj );
    Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
    {
        Gia_ObjTerSimCo( pObj );
        if ( Vec_IntEntry(vCoVals, i) )
            assert( Gia_ObjTerSimGet1(pObj) );
        else
            assert( Gia_ObjTerSimGet0(pObj) );
    }
}

Here is the caller graph for this function: