kliveness.c File Reference

#include <stdio.h>
#include "base/main/main.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include <string.h>
#include "base/main/mainInt.h"
#include "proof/pdr/pdr.h"
#include <time.h>

Include dependency graph for kliveness.c:

Go to the source code of this file.

Macros
#define	SIMPLE_kCS   0
#define	kCS_WITH_SAFETY_INVARIANTS   1
#define	kCS_WITH_DISCOVER_MONOTONE_SIGNALS   2
#define	kCS_WITH_SAFETY_AND_DCS_INVARIANTS   3
#define	kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS   4

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///.
Abc_Ntk_t *	Abc_NtkFromAigPhase (Aig_Man_t *pMan)
	DECLARATIONS ///.
Abc_Ntk_t *	Abc_NtkMakeOnePo (Abc_Ntk_t *pNtk, int Output, int nRange)
void	Aig_ManDumpBlif (Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
Aig_Man_t *	generateWorkingAig (Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live)
Aig_Man_t *	generateWorkingAigWithDSC (Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers)
Vec_Ptr_t *	findDisjunctiveMonotoneSignals (Abc_Ntk_t *pNtk)
Vec_Int_t *	createSingletonIntVector (int i)
Aig_Man_t *	generateDisjunctiveTester (Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK)
Aig_Man_t *	generateGeneralDisjunctiveTester (Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK)
Aig_Obj_t *	readLiveSignal_0 (Aig_Man_t *pAig, int liveIndex_0)
Aig_Obj_t *	readLiveSignal_k (Aig_Man_t *pAig, int liveIndex_k)
Aig_Man_t *	introduceAbsorberLogic (Aig_Man_t *pAig, int *pLiveIndex_0, int *pLiveIndex_k, int nonFirstIteration)
void	modifyAigToApplySafetyInvar (Aig_Man_t *pAig, int csTarget, int safetyInvarPO)
int	flipConePdr (Aig_Man_t *pAig, int directive, int targetCSPropertyIndex, int safetyInvariantPOIndex, int absorberCount)
int	collectSafetyInvariantPOIndex (Abc_Ntk_t *pNtk)
Vec_Ptr_t *	collectUserGivenDisjunctiveMonotoneSignals (Abc_Ntk_t *pNtk)
void	deallocateMasterBarrierDisjunctInt (Vec_Ptr_t *vMasterBarrierDisjunctsArg)
void	deallocateMasterBarrierDisjunctVecPtrVecInt (Vec_Ptr_t *vMasterBarrierDisjunctsArg)
Vec_Ptr_t *	getVecOfVecFairness (FILE *fp)
int	Abc_CommandCS_kLiveness (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandNChooseK (Abc_Frame_t *pAbc, int argc, char **argv)

Macro Definition Documentation

kCS_WITH_DISCOVER_MONOTONE_SIGNALS

#define kCS_WITH_DISCOVER_MONOTONE_SIGNALS   2

Definition at line 59 of file kliveness.c.

kCS_WITH_SAFETY_AND_DCS_INVARIANTS

#define kCS_WITH_SAFETY_AND_DCS_INVARIANTS   3

Definition at line 60 of file kliveness.c.

kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS

#define kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS   4

Definition at line 61 of file kliveness.c.

kCS_WITH_SAFETY_INVARIANTS

#define kCS_WITH_SAFETY_INVARIANTS   1

Definition at line 58 of file kliveness.c.

SIMPLE_kCS

#define SIMPLE_kCS   0

Definition at line 57 of file kliveness.c.

Function Documentation

Abc_CommandCS_kLiveness()

int Abc_CommandCS_kLiveness	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

Definition at line 525 of file kliveness.c.

{
        Abc_Ntk_t * pNtk, * pNtkTemp;
    Aig_Man_t * pAig, *pAigCS, *pAigCSNew;
    int absorberCount;
    int absorberLimit = 500;
    int RetValue;
    int liveIndex_0 = -1, liveIndex_k = -1;
    int fVerbose = 1;
    int directive = -1;
    int c;
    int safetyInvariantPO = -1;
    abctime beginTime, endTime;
    double time_spent;
    Vec_Ptr_t *vMasterBarrierDisjuncts = NULL;
    Aig_Man_t *pWorkingAig;
    //FILE *fp;
 
    pNtk = Abc_FrameReadNtk(pAbc);
 
    //fp = fopen("propFile.txt", "r");
    //if( fp )
    //    getVecOfVecFairness(fp);
    //exit(0);
 
    /*************************************************
    Extraction of Command Line Argument    
    *************************************************/
    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = SIMPLE_kCS;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
        {
            switch( c )
            {
            case 'c':
                directive = kCS_WITH_SAFETY_INVARIANTS; 
                break;
            case 'm':
                directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; 
                break;
            case 'C':
                directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
                break;
            case 'g':
                directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
                break;
            case 'h':
                goto usage;
                break;
            default:
                goto usage;
            }
        }
    }
    /*************************************************
    Extraction of Command Line Argument Ends    
    *************************************************/
 
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkTemp = pNtk;
    }
 
    if( directive == kCS_WITH_SAFETY_INVARIANTS )
    {
        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
        assert( safetyInvariantPO != -1 );
    }
 
    if(directive == kCS_WITH_DISCOVER_MONOTONE_SIGNALS)
    {
        beginTime = Abc_Clock();
        vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
        endTime = Abc_Clock();
        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
        printf("pre-processing time = %f\n",time_spent); 
        return 0;
    }
 
    if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS)
    {
        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
        assert( safetyInvariantPO != -1 );
 
        beginTime = Abc_Clock();
        vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
        endTime = Abc_Clock();
        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
        printf("pre-processing time = %f\n",time_spent); 
 
        assert( vMasterBarrierDisjuncts != NULL );
        assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
    }
 
    if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
    {
        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
        assert( safetyInvariantPO != -1 );
 
        beginTime = Abc_Clock();
        vMasterBarrierDisjuncts = collectUserGivenDisjunctiveMonotoneSignals( pNtk );
        endTime = Abc_Clock();
        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
        printf("pre-processing time = %f\n",time_spent); 
 
        assert( vMasterBarrierDisjuncts != NULL );
        assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
    }
 
    if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
    {
        assert( vMasterBarrierDisjuncts != NULL );
        pWorkingAig = generateWorkingAigWithDSC( pAig, pNtk, &liveIndex_0, vMasterBarrierDisjuncts );
        pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
    }
    else
    {
        pWorkingAig = generateWorkingAig( pAig, pNtk, &liveIndex_0 );
        pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
    }
 
    Aig_ManStop(pWorkingAig);
 
    for( absorberCount=1; absorberCount<absorberLimit; absorberCount++ )
    {
        //printf( "\nindex of the liveness output = %d\n", liveIndex_k );
        RetValue = flipConePdr( pAigCS, directive, liveIndex_k, safetyInvariantPO, absorberCount );
 
        if ( RetValue == 1 )
        {
                Abc_Print( 1, "k = %d, Property proved\n", absorberCount );
            break;
        }
            else if ( RetValue == 0 )
        {
            if( fVerbose )
            {
                Abc_Print( 1, "k = %d, Property DISPROVED\n", absorberCount );
            }
        }
            else if ( RetValue == -1 )
        {
                Abc_Print( 1, "Property UNDECIDED with k = %d.\n", absorberCount );
        }
            else
                assert( 0 );
 
        pAigCSNew = introduceAbsorberLogic(pAigCS, &liveIndex_0, &liveIndex_k, absorberCount);
        Aig_ManStop(pAigCS);
        pAigCS = pAigCSNew;
    }
 
    Aig_ManStop(pAigCS);
    Aig_ManStop(pAig);
 
    if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
    {
        deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
    }
    else
    {
        //if(vMasterBarrierDisjuncts)
        //    Vec_PtrFree(vMasterBarrierDisjuncts);
        //deallocateMasterBarrierDisjunctVecPtrVecInt(vMasterBarrierDisjuncts);
        deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
    }
    return 0;
 
    usage:
        fprintf( stdout, "usage: kcs [-cmgCh]\n" );
            fprintf( stdout, "\timplements Claessen-Sorensson's k-Liveness algorithm\n" );
        fprintf( stdout, "\t-c : verification with constraints, looks for POs prefixed with csSafetyInvar_\n");
        fprintf( stdout, "\t-m : discovers monotone signals\n");
            fprintf( stdout, "\t-g : verification with user-supplied barriers, looks for POs prefixed with csLevel1Stabil_\n");
        fprintf( stdout, "\t-C : verification with discovered monotone signals\n");
        fprintf( stdout, "\t-h : print usage\n");
            return 1;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_CommandNChooseK()

int Abc_CommandNChooseK	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

Definition at line 718 of file kliveness.c.

{
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkCombStabil;
    Aig_Man_t * pAig, *pAigCombStabil;
    int directive = -1;
    int c;
    int parameterizedCombK;
 
    pNtk = Abc_FrameReadNtk(pAbc);
 
 
    /*************************************************
    Extraction of Command Line Argument    
    *************************************************/
    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = SIMPLE_kCS;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
        {
            switch( c )
            {
            case 'c':
                directive = kCS_WITH_SAFETY_INVARIANTS; 
                break;
            case 'm':
                directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; 
                break;
            case 'C':
                directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
                break;
            case 'g':
                directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
                break;
            case 'h':
                goto usage;
                break;
            default:
                goto usage;
            }
        }
    }
    /*************************************************
    Extraction of Command Line Argument Ends    
    *************************************************/
 
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkTemp = pNtk;
    }
 
/**********************Code for generation of nCk outputs**/
    //combCount = countCombination(1000, 3);
    //pAigCombStabil = generateDisjunctiveTester( pNtk, pAig, 7, 2 );
    printf("Enter parameterizedCombK = " );
    if( scanf("%d", &parameterizedCombK) != 1 )
    {
        printf("\nFailed to read integer!\n");
        return 0;
    }
    printf("\n");
 
    pAigCombStabil = generateGeneralDisjunctiveTester( pNtk, pAig, parameterizedCombK );
    Aig_ManPrintStats(pAigCombStabil);
    pNtkCombStabil = Abc_NtkFromAigPhase( pAigCombStabil );
    pNtkCombStabil->pName = Abc_UtilStrsav( pAigCombStabil->pName );
    if ( !Abc_NtkCheck( pNtkCombStabil ) )
            fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkCombStabil );
 
    Aig_ManStop( pAigCombStabil );
    Aig_ManStop( pAig );
 
    return 1;
    //printf("\ncombCount = %d\n", combCount);
    //exit(0);
/**********************************************************/
 
    usage:
        fprintf( stdout, "usage: nck [-cmgCh]\n" );
            fprintf( stdout, "\tgenerates combinatorial signals for stabilization\n" );
        fprintf( stdout, "\t-h : print usage\n");
            return 1;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFromAigPhase()

Abc_Ntk_t * Abc_NtkFromAigPhase ( Aig_Man_t * pMan )

extern

DECLARATIONS ///.

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [This procedure should be called after seq sweeping, which changes the number of registers.]

SideEffects []

SeeAlso []

Definition at line 595 of file abcDar.c.

{
    Vec_Ptr_t * vNodes; 
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew;
    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
    int i; 
    assert( pMan->nAsserts == 0 );
    // perform strashing
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pNtkNew->nConstrs = pMan->nConstrs;
    pNtkNew->nBarBufs = pMan->nBarBufs;
    // duplicate the name and the spec
//    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
//    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
    // create PIs
    Aig_ManForEachPiSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePi( pNtkNew );
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        pObj->pData = pObjNew;
    }
    // create POs
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePo( pNtkNew );
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        pObj->pData = pObjNew;
    }
    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
    // create as many latches as there are registers in the manager
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
        Abc_LatchSetInit0( pObjNew );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
    }
    // rebuild the AIG
    vNodes = Aig_ManDfs( pMan, 1 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        else
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
    Vec_PtrFree( vNodes );
    // connect the PO nodes
    Aig_ManForEachCo( pMan, pObj, i )
    {
        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
    }
 
    Abc_NtkAddDummyPiNames( pNtkNew );
    Abc_NtkAddDummyPoNames( pNtkNew );
    Abc_NtkAddDummyBoxNames( pNtkNew );
 
    // check the resulting AIG
    if ( !Abc_NtkCheck( pNtkNew ) )
        Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
    return pNtkNew;
}

Here is the caller graph for this function:

Abc_NtkMakeOnePo()

Abc_Ntk_t * Abc_NtkMakeOnePo ( Abc_Ntk_t * pNtkInit, int Output, int nRange )

extern

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

Synopsis [Removes all POs, except one.]

Description []

SideEffects []

SeeAlso []

Definition at line 1857 of file abcNtk.c.

{
    Abc_Ntk_t * pNtk;
    Vec_Ptr_t * vPosLeft;
    Vec_Ptr_t * vCosLeft;
    Abc_Obj_t * pNodePo;
    int i;
    assert( !Abc_NtkIsNetlist(pNtkInit) );
    assert( Abc_NtkHasOnlyLatchBoxes(pNtkInit) );
    if ( Output < 0 || Output >= Abc_NtkPoNum(pNtkInit) )
    {
        printf( "PO index is incorrect.\n" );
        return NULL;
    }
 
    pNtk = Abc_NtkDup( pNtkInit );
    if ( Abc_NtkPoNum(pNtk) == 1 )
        return pNtk;
 
    if ( nRange < 1 )
        nRange = 1;
 
    // filter POs
    vPosLeft = Vec_PtrAlloc( nRange );
    Abc_NtkForEachPo( pNtk, pNodePo, i )
        if ( i < Output || i >= Output + nRange )
            Abc_NtkDeleteObjPo( pNodePo );
        else
            Vec_PtrPush( vPosLeft, pNodePo );
    // filter COs
    vCosLeft = Vec_PtrDup( vPosLeft );
    for ( i = Abc_NtkPoNum(pNtk); i < Abc_NtkCoNum(pNtk); i++ )
        Vec_PtrPush( vCosLeft, Abc_NtkCo(pNtk, i) );
    // update arrays
    Vec_PtrFree( pNtk->vPos );  pNtk->vPos = vPosLeft;
    Vec_PtrFree( pNtk->vCos );  pNtk->vCos = vCosLeft;
 
    // clean the network
    if ( Abc_NtkIsStrash(pNtk) )
    {
        Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
        if ( Abc_NtkLatchNum(pNtk) ) printf( "Run sequential cleanup (\"scl\") to get rid of dangling logic.\n" );
    }
    else
    {
        if ( Abc_NtkLatchNum(pNtk) ) printf( "Run sequential cleanup (\"st; scl\") to get rid of dangling logic.\n" );
    }
 
    if ( !Abc_NtkCheck( pNtk ) )
        fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" );
    return pNtk;
}

Here is the call graph for this function:

Abc_NtkToDar()

ABC_NAMESPACE_IMPL_START Aig_Man_t * Abc_NtkToDar ( Abc_Ntk_t * pNtk, int fExors, int fRegisters )

extern

DECLARATIONS ///.

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

FileName [kliveness.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [Main implementation module of the algorithm k-Liveness ] [invented by Koen Claessen, Niklas Sorensson. Implements] [the code for 'kcs'. 'kcs' pre-processes based on switch] [and then runs the (absorber circuit >> pdr) loop ]

Author [Sayak Ray]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 31, 2012.]

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [Assumes that registers are ordered after PIs/POs.]

SideEffects []

SeeAlso []

Definition at line 237 of file abcDar.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Man_t * pMan;
    Aig_Obj_t * pObjNew;
    Abc_Obj_t * pObj;
    int i, nNodes, nDontCares;
    // make sure the latches follow PIs/POs
    if ( fRegisters ) 
    { 
        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
        Abc_NtkForEachCi( pNtk, pObj, i )
            if ( i < Abc_NtkPiNum(pNtk) )
            {
                assert( Abc_ObjIsPi(pObj) );
                if ( !Abc_ObjIsPi(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBo(pObj) );
        Abc_NtkForEachCo( pNtk, pObj, i )
            if ( i < Abc_NtkPoNum(pNtk) )
            {
                assert( Abc_ObjIsPo(pObj) );
                if ( !Abc_ObjIsPo(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBi(pObj) );
        // print warning about initial values
        nDontCares = 0;
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInitDc(pObj) )
            {
                Abc_LatchSetInit0(pObj);
                nDontCares++;
            }
        if ( nDontCares )
        {
            Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
            Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
            Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
            Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
        }
    }
    // create the manager
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
    pMan->fCatchExor = fExors;
    pMan->nConstrs = pNtk->nConstrs;
    pMan->nBarBufs = pNtk->nBarBufs;
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
    // transfer the pointers to the basic nodes
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
        // initialize logic level of the CIs
        ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
    }
 
    // complement the 1-values registers
    if ( fRegisters ) {
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInit1(pObj) )
                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
    }
    // perform the conversion of the internal nodes (assumes DFS ordering)
//    pMan->fAddStrash = 1;
    vNodes = Abc_NtkDfs( pNtk, 0 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
//    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
//        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
    }
    Vec_PtrFree( vNodes );
    pMan->fAddStrash = 0;
    // create the POs
    Abc_NtkForEachCo( pNtk, pObj, i )
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
    // complement the 1-valued registers
    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
    if ( fRegisters )
        Aig_ManForEachLiSeq( pMan, pObjNew, i )
            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
    // remove dangling nodes
    nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
    if ( !fExors && nNodes )
        Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
    // save the number of registers
    if ( fRegisters )
    {
        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
//        pMan->vFlopNums = NULL;
//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
        if ( pNtk->vOnehots )
            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
    }
    if ( !Aig_ManCheck( pMan ) )
    {
        Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
        Aig_ManStop( pMan );
        return NULL;
    }
    return pMan;
}

Here is the caller graph for this function:

Aig_ManDumpBlif()

void Aig_ManDumpBlif ( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )

extern

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

Synopsis [Writes the AIG into a BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 746 of file aigUtil.c.

{
    FILE * pFile;
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
    int i, nDigits, Counter = 0;
    if ( Aig_ManCoNum(p) == 0 )
    {
        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
        return;
    }
    // check if constant is used
    Aig_ManForEachCo( p, pObj, i )
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
            pConst1 = Aig_ManConst1(p);
    // collect nodes in the DFS order
    vNodes = Aig_ManDfs( p, 1 );
    // assign IDs to objects
    Aig_ManConst1(p)->iData = Counter++;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Counter++;
    Aig_ManForEachCo( p, pObj, i )
        pObj->iData = Counter++;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        pObj->iData = Counter++;
    nDigits = Abc_Base10Log( Counter );
    // write the file 
    pFile = fopen( pFileName, "w" );
    fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
//    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
    fprintf( pFile, ".model %s\n", p->pName );
    // write PIs
    fprintf( pFile, ".inputs" );
    Aig_ManForEachPiSeq( p, pObj, i )
        if ( vPiNames )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) );
        else
            fprintf( pFile, " n%0*d", nDigits, pObj->iData );
    fprintf( pFile, "\n" );
    // write POs
    fprintf( pFile, ".outputs" );
    Aig_ManForEachPoSeq( p, pObj, i )
        if ( vPoNames )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) );
        else
            fprintf( pFile, " n%0*d", nDigits, pObj->iData );
    fprintf( pFile, "\n" );
    // write latches
    if ( Aig_ManRegNum(p) )
    {
        fprintf( pFile, "\n" );
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        {
            fprintf( pFile, ".latch" );
            if ( vPoNames )
                fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i) );
            else
                fprintf( pFile, " n%0*d", nDigits, pObjLi->iData );
            if ( vPiNames )
                fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i) );
            else
                fprintf( pFile, " n%0*d", nDigits, pObjLo->iData );
            fprintf( pFile, " 0\n" );
        }
        fprintf( pFile, "\n" );
    } 
    // write nodes
    if ( pConst1 )
        fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
    Aig_ManSetCioIds( p );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        fprintf( pFile, ".names" );
        if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
        else
            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
        if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) );
        else
            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
        fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
        fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
    }
    // write POs
    Aig_ManForEachCo( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
        else
            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
        if ( vPoNames )
            fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) );
        else
            fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
        fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
    }
    Aig_ManCleanCioIds( p );
    fprintf( pFile, ".end\n\n" );
    fclose( pFile );
    Vec_PtrFree( vNodes );
}

Here is the caller graph for this function:

collectSafetyInvariantPOIndex()

int collectSafetyInvariantPOIndex

(

Abc_Ntk_t *

pNtk

)

Definition at line 425 of file kliveness.c.

{
    Abc_Obj_t *pObj;
    int i;
 
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
        if( strstr( Abc_ObjName( pObj ), "csSafetyInvar_" ) != NULL )
            return i;
    }        
 
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

collectUserGivenDisjunctiveMonotoneSignals()

Vec_Ptr_t * collectUserGivenDisjunctiveMonotoneSignals

(

Abc_Ntk_t *

pNtk

)

Definition at line 439 of file kliveness.c.

{
    Abc_Obj_t *pObj;
    int i;
    Vec_Ptr_t *monotoneVector;
    Vec_Int_t *newIntVector;
 
    monotoneVector = Vec_PtrAlloc(0);    
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
        if( strstr( Abc_ObjName( pObj ), "csLevel1Stabil_" ) != NULL )
        {
            newIntVector = createSingletonIntVector(i);
            Vec_PtrPush(monotoneVector, newIntVector);
        }
    }
 
    if( Vec_PtrSize(monotoneVector) > 0 )
        return monotoneVector;
    else
        return NULL;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

createSingletonIntVector()

Vec_Int_t * createSingletonIntVector ( int i )

extern

Definition at line 380 of file disjunctiveMonotone.c.

{
    Vec_Int_t *myVec = Vec_IntAlloc(1);
    
    Vec_IntPush(myVec, iElem);
    return myVec;
}

Here is the caller graph for this function:

deallocateMasterBarrierDisjunctInt()

void deallocateMasterBarrierDisjunctInt

(

Vec_Ptr_t *

vMasterBarrierDisjunctsArg

)

Definition at line 463 of file kliveness.c.

{
    Vec_Int_t *vInt;
    int i;
 
    if(vMasterBarrierDisjunctsArg)
    {
        Vec_PtrForEachEntry(Vec_Int_t *, vMasterBarrierDisjunctsArg, vInt, i)
        {    
            Vec_IntFree(vInt);
        }
        Vec_PtrFree(vMasterBarrierDisjunctsArg);
    }
}

Here is the caller graph for this function:

deallocateMasterBarrierDisjunctVecPtrVecInt()

void deallocateMasterBarrierDisjunctVecPtrVecInt

(

Vec_Ptr_t *

vMasterBarrierDisjunctsArg

)

Definition at line 478 of file kliveness.c.

{
    Vec_Int_t *vInt;
    Vec_Ptr_t *vPtr;
    int i, j, k, iElem;
 
    if(vMasterBarrierDisjunctsArg)
    {
        Vec_PtrForEachEntry(Vec_Ptr_t *, vMasterBarrierDisjunctsArg, vPtr, i)
        {    
            assert(vPtr);
            Vec_PtrForEachEntry( Vec_Int_t *, vPtr, vInt, j )
            {
                //Vec_IntFree(vInt);
                Vec_IntForEachEntry( vInt, iElem, k )
                    printf("%d - ", iElem);
                //printf("Chung Chang j = %d\n", j);
            }
            Vec_PtrFree(vPtr);
        }
        Vec_PtrFree(vMasterBarrierDisjunctsArg);
    }
}

findDisjunctiveMonotoneSignals()

Vec_Ptr_t * findDisjunctiveMonotoneSignals ( Abc_Ntk_t * pNtk )

extern

Definition at line 596 of file disjunctiveMonotone.c.

{
    Aig_Man_t *pAig;
    Vec_Int_t *vCandidateMonotoneSignals;
    Vec_Int_t *vKnownMonotoneSignals;
    //Vec_Int_t *vKnownMonotoneSignalsRoundTwo;
    //Vec_Int_t *vOldConsequentVector;
    //Vec_Int_t *vRemainingConsecVector;
    int i;
    int iElem;
    int pendingSignalIndex;
    Abc_Ntk_t *pNtkTemp;
    int hintSingalBeginningMarker;
    int hintSingalEndMarker;
    struct aigPoIndices *aigPoIndicesInstance;
    //struct monotoneVectorsStruct *monotoneVectorsInstance;
    struct antecedentConsequentVectorsStruct *anteConsecInstance;
    //Aig_Obj_t *safetyDriverNew;
    Vec_Int_t *newIntVec;
    Vec_Ptr_t *levelOneMonotne, *levelTwoMonotne;
    //Vec_Ptr_t *levelThreeMonotne;
 
    Vec_Ptr_t *vMasterDisjunctions;
 
    extern int findPendingSignal(Abc_Ntk_t *pNtk);
    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);    
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 
    //system("rm monotone.dat");
    
    /*******************************************/    
    //Finding the PO index of the pending signal 
    /*******************************************/    
    pendingSignalIndex = findPendingSignal(pNtk);
    if( pendingSignalIndex == -1 )
    {
        printf("\nNo Pending Signal Found\n");
        return NULL;
    }
    //else
        //printf("Po[%d] = %s\n", pendingSignalIndex, Abc_ObjName( Abc_NtkPo(pNtk, pendingSignalIndex) ) );
 
    /*******************************************/    
    //Finding the PO indices of all hint signals
    /*******************************************/    
    vCandidateMonotoneSignals = findHintOutputs(pNtk);
    if( vCandidateMonotoneSignals == NULL )
        return NULL;
    else
    {
        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
        hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
        hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
    }
 
    /**********************************************/
    //Allocating "struct" with necessary parameters
    /**********************************************/
    aigPoIndicesInstance = allocAigPoIndices();
    aigPoIndicesInstance->attrPendingSignalIndex = pendingSignalIndex;
    aigPoIndicesInstance->attrHintSingalBeginningMarker = hintSingalBeginningMarker;
    aigPoIndicesInstance->attrHintSingalEndMarker = hintSingalEndMarker;
    aigPoIndicesInstance->attrSafetyInvarIndex = collectSafetyInvariantPOIndex(pNtk);
 
    /****************************************************/
    //Allocating "struct" with necessary monotone vectors
    /****************************************************/
    anteConsecInstance = allocAntecedentConsequentVectorsStruct();
    anteConsecInstance->attrAntecedents = NULL;
    anteConsecInstance->attrConsequentCandidates = vCandidateMonotoneSignals;
 
    /*******************************************/    
    //Generate AIG from Ntk
    /*******************************************/    
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkTemp = pNtk;
    }
 
    /*******************************************/    
    //finding LEVEL 1 monotone signals
    /*******************************************/    
    //printf("Calling target function outside loop\n");
    vKnownMonotoneSignals = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
    levelOneMonotne = Vec_PtrAlloc(0);
    Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
    {
        newIntVec = createSingletonIntVector( iElem );
        Vec_PtrPush( levelOneMonotne, newIntVec );
        //printf("Monotone Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
    }
    //printAllIntVectors( levelOneMonotne, pNtk, "monotone.dat" );
 
    vMasterDisjunctions = Vec_PtrAlloc( Vec_PtrSize( levelOneMonotne ));
    appendVecToMasterVecInt(vMasterDisjunctions, levelOneMonotne );
 
    /*******************************************/    
    //finding LEVEL >1 monotone signals
    /*******************************************/    
    #if 0
    if( vKnownMonotoneSignals )
    {
        Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
        {
            printf("\n**************************************************************\n");
            printf("Exploring Second Layer : Reference Po[%d] = %s", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ));
            printf("\n**************************************************************\n");
            anteConsecInstance->attrAntecedents = createSingletonIntVector( iElem );
            vOldConsequentVector = anteConsecInstance->attrConsequentCandidates;
            vRemainingConsecVector = updateAnteConseVectors(anteConsecInstance);
            if( anteConsecInstance->attrConsequentCandidates != vRemainingConsecVector )
            {
                anteConsecInstance->attrConsequentCandidates = vRemainingConsecVector;
            }
            vKnownMonotoneSignalsRoundTwo = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
            Vec_IntForEachEntry( vKnownMonotoneSignalsRoundTwo, iElemTwo, iTwo )
            {
                printf("Monotone Po[%d] = %s, (%d, %d)\n", iElemTwo, Abc_ObjName( Abc_NtkPo(pNtk, iElemTwo) ), iElem, iElemTwo );
            }
            Vec_IntFree(vKnownMonotoneSignalsRoundTwo);
            Vec_IntFree(anteConsecInstance->attrAntecedents);
            if(anteConsecInstance->attrConsequentCandidates != vOldConsequentVector)
            {
                Vec_IntFree(anteConsecInstance->attrConsequentCandidates);
                anteConsecInstance->attrConsequentCandidates = vOldConsequentVector;
            }
        }
    }
    #endif 
 
#if 1
    levelTwoMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelOneMonotne );
    //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
    appendVecToMasterVecInt(vMasterDisjunctions, levelTwoMonotne );
#endif
 
    //levelThreeMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelTwoMonotne );
    //printAllIntVectors( levelThreeMonotne );
    //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
    //appendVecToMasterVecInt(vMasterDisjunctions, levelThreeMonotne );
 
    deallocAigPoIndices(aigPoIndicesInstance);
    deallocAntecedentConsequentVectorsStruct(anteConsecInstance);
    //deallocPointersToMonotoneVectors(monotoneVectorsInstance);
 
    deallocateVecOfIntVec( levelOneMonotne );
    deallocateVecOfIntVec( levelTwoMonotne );
 
    Aig_ManStop(pAig);
    Vec_IntFree(vKnownMonotoneSignals);
 
    return vMasterDisjunctions;
}

Here is the call graph for this function:

Here is the caller graph for this function:

flipConePdr()

int flipConePdr	(	Aig_Man_t *	pAig,
		int	directive,
		int	targetCSPropertyIndex,
		int	safetyInvariantPOIndex,
		int	absorberCount )

Definition at line 341 of file kliveness.c.

{
    int RetValue, i;
    Aig_Obj_t *pObjTargetPo;
    Aig_Man_t *pAigDupl;
    Pdr_Par_t Pars, * pPars = &Pars;
    Abc_Cex_t * pCex = NULL;
 
    char *fileName;
    
    fileName = (char *)malloc(sizeof(char) * 50);
    sprintf(fileName, "%s_%d.%s", "kLive", absorberCount, "blif" );
 
    if( directive == kCS_WITH_SAFETY_INVARIANTS || directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS )
    {
        assert( safetyInvariantPOIndex != -1 );
        modifyAigToApplySafetyInvar(pAig, targetCSPropertyIndex, safetyInvariantPOIndex);
    }
 
    pAigDupl = pAig;
    pAig = Aig_ManDupSimple( pAigDupl );
 
    for( i=0; i<Saig_ManPoNum(pAig); i++ )
    {
        pObjTargetPo = Aig_ManCo( pAig, i );
        Aig_ObjChild0Flip( pObjTargetPo );
    }
 
    Pdr_ManSetDefaultParams( pPars );
    pPars->fVerbose = 1;
    pPars->fNotVerbose = 1;
    pPars->fSolveAll = 1;
    pAig->vSeqModelVec = NULL;
 
    Aig_ManCleanup( pAig );
    assert( Aig_ManCheck( pAig ) );
 
    Pdr_ManSolve( pAig, pPars );    
 
    if( pAig->vSeqModelVec )
    {
        pCex = (Abc_Cex_t *)Vec_PtrEntry( pAig->vSeqModelVec, targetCSPropertyIndex );
        if( pCex == NULL )
        {
            RetValue = 1;
        }
        else
            RetValue = 0;
    }
    else
    {
        RetValue = -1;
        exit(0);
    }
 
    free(fileName);
 
    for( i=0; i<Saig_ManPoNum(pAig); i++ )
    {
        pObjTargetPo = Aig_ManCo( pAig, i );
        Aig_ObjChild0Flip( pObjTargetPo );
    }
    
    Aig_ManStop( pAig );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

generateDisjunctiveTester()

Aig_Man_t * generateDisjunctiveTester ( Abc_Ntk_t * pNtk, Aig_Man_t * pAig, int combN, int combK )

extern

Definition at line 148 of file combination.c.

{
    //AIG creation related data structure
    Aig_Man_t *pNewAig;
    int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
    //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
    int i, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
    int combN_internal, combK_internal; //, targetPoIndex;
    long longI, lCombinationCount;
    //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
    Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
    Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
    Vec_Int_t *vCandidateMonotoneSignals;
 
    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
    
    //Knuth's Data Strcuture
    //Vec_Int_t *vC_KNUTH;
    //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
 
    //Collecting target HINT signals
    vCandidateMonotoneSignals = findHintOutputs(pNtk);
    if( vCandidateMonotoneSignals == NULL )
    {
        printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
        combN_internal = 0;
    }
    else
    {
        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
        hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
        hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
        combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
    }
 
    //combK_internal = combK;
 
    //Knuth's Data Structure Initialization
    //vC_KNUTH = Vec_IntAlloc(combK_internal+3);
    //for(i_KNUTH=-1; i_KNUTH<combK_internal; i_KNUTH++)
    //    Vec_IntPush( vC_KNUTH, i_KNUTH );
    //Vec_IntPush( vC_KNUTH, combN_internal );
    //Vec_IntPush( vC_KNUTH, 0 );
 
    //Standard AIG duplication begins
    //Standard AIG Manager Creation
    pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
    pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
        pNewAig->pSpec = NULL;
 
    //Standard Mapping of Constant Nodes
    pObj = Aig_ManConst1( pAig );
        pObj->pData = Aig_ManConst1( pNewAig );
 
    //Standard AIG PI duplication
    Saig_ManForEachPi( pAig, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
    }
 
    //Standard AIG LO duplication
    Saig_ManForEachLo( pAig, pObj, i )
        {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
        }
 
    //nCk LO creation
    lCombinationCount = 0;
    for(combK_internal=1; combK_internal<=combK; combK_internal++)
        lCombinationCount += countCombination( combN_internal, combK_internal );
    assert( lCombinationCount > 0 );
    vLO_nCk = Vec_PtrAlloc(lCombinationCount);
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        loCreated++;
        pObj = Aig_ObjCreateCi(pNewAig);
        Vec_PtrPush( vLO_nCk, pObj );
    }
 
    //Standard Node duplication
    Aig_ManForEachNode( pAig, pObj, i )
    {
        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }
    
    //nCk specific logic creation (i.e. nCk number of OR gates)
    vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
 
    
 
    //while(1)
    //{
    //    //visit combination
    //    //printf("Comb-%3d : ", ++combCounter_KNUTH);
    //    pObjMonoCand = Aig_Not(Aig_ManConst1(pNewAig));
    //    for( i_KNUTH=combK_internal; i_KNUTH>0; i_KNUTH--)
    //    {
    //        //printf("vC[%d] = %d ", i_KNUTH, Vec_IntEntry(vC_KNUTH, i_KNUTH));
    //        targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntEntry(vC_KNUTH, i_KNUTH));
    //        pObj = Aig_ObjChild0Copy(Aig_ManCo( pAig, targetPoIndex ));
    //        pObjMonoCand = Aig_Or( pNewAig, pObj, pObjMonoCand );
    //    }
    //    Vec_PtrPush(vDisj_nCk, pObjMonoCand );
    //    //printf("\n");
 
    //    j_KNUTH = 1;
    //    while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
    //    {
    //        Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
    //        j_KNUTH = j_KNUTH + 1;
    //    }
    //    if( j_KNUTH > combK_internal ) break;
    //    Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
    //}
    for( combK_internal=1; combK_internal<=combK; combK_internal++ )
        generateCombinatorialStabil( pNewAig, pAig, vCandidateMonotoneSignals,
                vDisj_nCk, combN_internal, combK_internal );
 
 
    //creation of implication logic
    vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
        pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
 
        pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
        Vec_PtrPush(vPODriver_nCk, pObj);
    }
    
    //Standard PO duplication
    Saig_ManForEachPo( pAig, pObj, i )
    {
        poCopied++;
        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
    }
 
    //nCk specific PO creation
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
    }
 
    //Standard LI duplication
    Saig_ManForEachLi( pAig, pObj, i )
    {
        liCopied++;
        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
    }
 
    //nCk specific LI creation
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        liCreated++;
        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
    }
 
    //clean-up, book-keeping
    assert( liCopied + liCreated == loCopied + loCreated );    
    nRegCount = loCopied + loCreated;
 
    Aig_ManSetRegNum( pNewAig, nRegCount );
    Aig_ManCleanup( pNewAig );
    assert( Aig_ManCheck( pNewAig ) );
    
    //Vec_IntFree(vC_KNUTH);    
    return pNewAig;
}

Here is the call graph for this function:

generateGeneralDisjunctiveTester()

Aig_Man_t * generateGeneralDisjunctiveTester ( Abc_Ntk_t * pNtk, Aig_Man_t * pAig, int combK )

extern

Definition at line 321 of file combination.c.

{
    //AIG creation related data structure
    Aig_Man_t *pNewAig;
    int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
    //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
    int i, nRegCount;
    int combN_internal, combK_internal; //, targetPoIndex;
    long longI, lCombinationCount;
    //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
    Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
    Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
 
    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
    
    //Knuth's Data Strcuture
    //Vec_Int_t *vC_KNUTH;
    //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
 
    //Collecting target HINT signals
    //vCandidateMonotoneSignals = findHintOutputs(pNtk);
    //if( vCandidateMonotoneSignals == NULL )
    //{
    //    printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
    //    combN_internal = 0;
    //}
    //else
    //{
        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
    //    hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
    //    hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
    //    combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
    //}
 
    combN_internal = Aig_ManRegNum(pAig);
 
    pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
    pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
        pNewAig->pSpec = NULL;
 
    //Standard Mapping of Constant Nodes
    pObj = Aig_ManConst1( pAig );
        pObj->pData = Aig_ManConst1( pNewAig );
 
    //Standard AIG PI duplication
    Saig_ManForEachPi( pAig, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
    }
 
    //Standard AIG LO duplication
    Saig_ManForEachLo( pAig, pObj, i )
        {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
        }
 
    //nCk LO creation
    lCombinationCount = 0;
    for(combK_internal=1; combK_internal<=combK; combK_internal++)
        lCombinationCount += countCombination( combN_internal, combK_internal );
    assert( lCombinationCount > 0 );
    vLO_nCk = Vec_PtrAlloc(lCombinationCount);
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        loCreated++;
        pObj = Aig_ObjCreateCi(pNewAig);
        Vec_PtrPush( vLO_nCk, pObj );
    }
 
    //Standard Node duplication
    Aig_ManForEachNode( pAig, pObj, i )
    {
        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }
    
    //nCk specific logic creation (i.e. nCk number of OR gates)
    vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
 
    for( combK_internal=1; combK_internal<=combK; combK_internal++ )
    {
        generateCombinatorialStabilExhaust( pNewAig, pAig,
                vDisj_nCk, combN_internal, combK_internal );
    }
 
 
    //creation of implication logic
    vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
        pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
 
        pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
        Vec_PtrPush(vPODriver_nCk, pObj);
    }
    
    //Standard PO duplication
    Saig_ManForEachPo( pAig, pObj, i )
    {
        poCopied++;
        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
    }
 
    //nCk specific PO creation
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
    }
 
    //Standard LI duplication
    Saig_ManForEachLi( pAig, pObj, i )
    {
        liCopied++;
        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
    }
 
    //nCk specific LI creation
    for( longI = 0; longI < lCombinationCount; longI++ )
    {
        liCreated++;
        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
    }
 
    //clean-up, book-keeping
    assert( liCopied + liCreated == loCopied + loCreated );    
    nRegCount = loCopied + loCreated;
 
    Aig_ManSetRegNum( pNewAig, nRegCount );
    Aig_ManCleanup( pNewAig );
    assert( Aig_ManCheck( pNewAig ) );
    
    Vec_PtrFree(vLO_nCk);
    Vec_PtrFree(vPODriver_nCk);
    Vec_PtrFree(vDisj_nCk);
    //Vec_IntFree(vC_KNUTH);    
    return pNewAig;
}

Here is the call graph for this function:

Here is the caller graph for this function:

generateWorkingAig()

Aig_Man_t * generateWorkingAig ( Aig_Man_t * pAig, Abc_Ntk_t * pNtk, int * pIndex0Live )

extern

Definition at line 163 of file kLiveConstraints.c.

{
    Vec_Ptr_t *vSignalVector;
    Aig_Man_t *pAigNew;
 
    vSignalVector = collectCSSignals( pNtk, pAig );    
    assert(vSignalVector);
    pAigNew = createNewAigWith0LivePo( pAig, vSignalVector, pIndex0Live );
    Vec_PtrFree(vSignalVector);
 
    return pAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

generateWorkingAigWithDSC()

Aig_Man_t * generateWorkingAigWithDSC ( Aig_Man_t * pAig, Abc_Ntk_t * pNtk, int * pIndex0Live, Vec_Ptr_t * vMasterBarriers )

extern

Definition at line 529 of file arenaViolation.c.

{
    Vec_Ptr_t *vSignalVector;
    Aig_Man_t *pAigNew;
    int pObjWithinWindow;
    int pObjWindowBegin;
    int pObjPendingSignal;
 
    vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );    
 
    pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
    pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
    pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );
 
    pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
    Vec_PtrFree(vSignalVector);
 
    return pAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

getVecOfVecFairness()

Vec_Ptr_t * getVecOfVecFairness

(

FILE *

fp

)

Definition at line 502 of file kliveness.c.

{
    Vec_Ptr_t *masterVector = Vec_PtrAlloc(0);
    //Vec_Ptr_t *currSignalVector;
    char stringBuffer[100];
    //int i;
    
    while(fgets(stringBuffer, 50, fp))
    {
        if(strstr(stringBuffer, ":"))
        {
 
        }
        else
        {
                
        }
    }
 
    return masterVector;
}

Here is the call graph for this function:

introduceAbsorberLogic()

Aig_Man_t * introduceAbsorberLogic	(	Aig_Man_t *	pAig,
		int *	pLiveIndex_0,
		int *	pLiveIndex_k,
		int	nonFirstIteration )

Definition at line 175 of file kliveness.c.

{
    Aig_Man_t *pNewAig;
    Aig_Obj_t *pObj, *pObjAbsorberLo, *pPInNewArg, *pPOutNewArg;
    Aig_Obj_t *pPIn = NULL, *pPOut = NULL, *pPOutCo = NULL;
    Aig_Obj_t *pFirstAbsorberOr, *pSecondAbsorberOr;
    int i;
    int piCopied = 0, loCreated = 0, loCopied = 0, liCreated = 0, liCopied = 0; 
    int nRegCount;
 
    assert(*pLiveIndex_0 != -1);
    if(nonFirstIteration == 0)
        assert( *pLiveIndex_k == -1 );
    else
        assert( *pLiveIndex_k != -1  );
 
    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
    pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_kCS") + 1 );
    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "kCS");
        pNewAig->pSpec = NULL;
 
    //****************************************************************
    // reading the signal pIn, and pOut
    //****************************************************************
 
    pPIn = readLiveSignal_0( pAig, *pLiveIndex_0 );
    if( *pLiveIndex_k == -1 )
        pPOut = NULL;
    else
        pPOut = readLiveSignal_k( pAig, *pLiveIndex_k );
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
        pObj = Aig_ManConst1( pAig );
        pObj->pData = Aig_ManConst1( pNewAig );
 
    //****************************************************************
        // Step 3: create true PIs
    //****************************************************************
        Saig_ManForEachPi( pAig, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
    }
 
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
        Saig_ManForEachLo( pAig, pObj, i )
        {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNewAig);
        }
 
    //****************************************************************
    // Step 6: create "D" register output for the ABSORBER logic
    //****************************************************************
    loCreated++;
    pObjAbsorberLo = Aig_ObjCreateCi( pNewAig );
 
    nRegCount = loCreated + loCopied;
 
    //********************************************************************
    // Step 7: create internal nodes
    //********************************************************************
        Aig_ManForEachNode( pAig, pObj, i )
    {
        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }
 
    //****************************************************************
    // Step 8: create the two OR gates of the OBSERVER logic
    //****************************************************************
    if( nonFirstIteration == 0 )
    {
        assert(pPIn);
        
        pPInNewArg = !Aig_IsComplement(pPIn)? 
                (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : 
                Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
 
        pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPInNewArg), pObjAbsorberLo );
        pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
    }
    else
    {
        assert( pPOut );
 
        pPInNewArg = !Aig_IsComplement(pPIn)? 
                (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : 
                Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
        pPOutNewArg = !Aig_IsComplement(pPOut)? 
                (Aig_Obj_t *)((Aig_Regular(pPOut))->pData) : 
                Aig_Not((Aig_Obj_t *)((Aig_Regular(pPOut))->pData));
        
        pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPOutNewArg), pObjAbsorberLo );
        pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
    }    
    
    //********************************************************************
    // Step 9: create primary outputs 
    //********************************************************************
    Saig_ManForEachPo( pAig, pObj, i )
    {
        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
        if( i == *pLiveIndex_k )
            pPOutCo = (Aig_Obj_t *)(pObj->pData);
    }
 
    //create new po
    if( nonFirstIteration == 0 )
    {
        assert(pPOutCo == NULL);
        pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );     
 
        *pLiveIndex_k = i;
    }    
    else
    {
        assert( pPOutCo != NULL );
        //pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );     
        //*pLiveIndex_k = Saig_ManPoNum(pAig);
 
        Aig_ObjPatchFanin0( pNewAig, pPOutCo, pSecondAbsorberOr );
    }
 
    Saig_ManForEachLi( pAig, pObj, i )
    {
        liCopied++;
        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
    }
 
    //create new li
    liCreated++;
    Aig_ObjCreateCo( pNewAig, pFirstAbsorberOr );
 
    Aig_ManSetRegNum( pNewAig, nRegCount );
    Aig_ManCleanup( pNewAig );
    
    assert( Aig_ManCheck( pNewAig ) );
 
    assert( *pLiveIndex_k != - 1);
    return pNewAig;
}

Here is the call graph for this function:

Here is the caller graph for this function:

modifyAigToApplySafetyInvar()

void modifyAigToApplySafetyInvar	(	Aig_Man_t *	pAig,
		int	csTarget,
		int	safetyInvarPO )

Definition at line 326 of file kliveness.c.

{
    Aig_Obj_t *pObjPOSafetyInvar, *pObjSafetyInvar;
    Aig_Obj_t *pObjPOCSTarget, *pObjCSTarget;
    Aig_Obj_t *pObjCSTargetNew;
 
    pObjPOSafetyInvar = Aig_ManCo( pAig, safetyInvarPO );
    pObjSafetyInvar =  Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOSafetyInvar), Aig_ObjFaninC0(pObjPOSafetyInvar));    
    pObjPOCSTarget = Aig_ManCo( pAig, csTarget );
    pObjCSTarget = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOCSTarget), Aig_ObjFaninC0(pObjPOCSTarget));    
 
    pObjCSTargetNew = Aig_And( pAig, pObjSafetyInvar, pObjCSTarget );
    Aig_ObjPatchFanin0( pAig, pObjPOCSTarget, pObjCSTargetNew );
}

Here is the call graph for this function:

Here is the caller graph for this function:

readLiveSignal_0()

Aig_Obj_t * readLiveSignal_0	(	Aig_Man_t *	pAig,
		int	liveIndex_0 )

Definition at line 83 of file kliveness.c.

{
    Aig_Obj_t *pObj;
 
    pObj = Aig_ManCo( pAig, liveIndex_0 );
    return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
}

Here is the caller graph for this function:

readLiveSignal_k()

Aig_Obj_t * readLiveSignal_k	(	Aig_Man_t *	pAig,
		int	liveIndex_k )

Definition at line 91 of file kliveness.c.

{
    Aig_Obj_t *pObj;
 
    pObj = Aig_ManCo( pAig, liveIndex_k );
    return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
}

Here is the caller graph for this function: