monotone.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"

Go to the source code of this file.

Data Structures
struct	aigPoIndices
struct	monotoneVectorsStruct

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///. More...
struct aigPoIndices *	allocAigPoIndices ()
void	deallocAigPoIndices (struct aigPoIndices *toBeDeletedAigPoIndices)
struct monotoneVectorsStruct *	allocPointersToMonotoneVectors ()
void	deallocPointersToMonotoneVectors (struct monotoneVectorsStruct *toBeDeleted)
Vec_Int_t *	findHintOutputs (Abc_Ntk_t *pNtk)
int	findPendingSignal (Abc_Ntk_t *pNtk)
int	checkSanityOfKnownMonotone (Vec_Int_t *vKnownMonotone, Vec_Int_t *vCandMonotone, Vec_Int_t *vHintMonotone)
Aig_Man_t *	createMonotoneTester (Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg, int *startMonotonePropPo)
Vec_Int_t *	findNewMonotone (Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg)
Vec_Int_t *	findRemainingMonotoneCandidates (Vec_Int_t *vKnownMonotone, Vec_Int_t *vHintMonotone)
Vec_Int_t *	findMonotoneSignals (Abc_Ntk_t *pNtk)

Function Documentation

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

DECLARATIONS ///.

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

FileName [kLiveConstraints.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [Constraint analysis module for the k-Liveness algorithm invented by Koen Classen, Niklas Sorensson.]

Author [Sayak Ray]

Affiliation [UC Berkeley]

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

Revision [

Id:

liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp

]

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 233 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;
}

struct aigPoIndices* allocAigPoIndices

(

)

Definition at line 43 of file monotone.c.

{
    struct aigPoIndices *newAigPoIndices;

    newAigPoIndices = (struct aigPoIndices *)malloc(sizeof (struct aigPoIndices));
    newAigPoIndices->attrPendingSignalIndex = -1;
    newAigPoIndices->attrHintSingalBeginningMarker = -1;
    newAigPoIndices->attrHintSingalEndMarker = -1;
    newAigPoIndices->attrSafetyInvarIndex = -1;

    assert( newAigPoIndices != NULL );
    return newAigPoIndices;
}

struct monotoneVectorsStruct* allocPointersToMonotoneVectors

(

)

Definition at line 70 of file monotone.c.

{
    struct monotoneVectorsStruct *newPointersToMonotoneVectors;

    newPointersToMonotoneVectors = (struct monotoneVectorsStruct *)malloc(sizeof (struct monotoneVectorsStruct));

    newPointersToMonotoneVectors->attrKnownMonotone = NULL;
    newPointersToMonotoneVectors->attrCandMonotone = NULL;
    newPointersToMonotoneVectors->attrHintMonotone = NULL;
        
    assert( newPointersToMonotoneVectors != NULL );
    return newPointersToMonotoneVectors;
}

int checkSanityOfKnownMonotone	(	Vec_Int_t *	vKnownMonotone,
		Vec_Int_t *	vCandMonotone,
		Vec_Int_t *	vHintMonotone
	)

Definition at line 129 of file monotone.c.

{
    int iElem, i;

    Vec_IntForEachEntry( vKnownMonotone, iElem, i )
        printf("%d ", iElem);
    printf("\n");
    Vec_IntForEachEntry( vCandMonotone, iElem, i )
        printf("%d ", iElem);
    printf("\n");
    Vec_IntForEachEntry( vHintMonotone, iElem, i )
        printf("%d ", iElem);
    printf("\n");
    return 1;
}

Aig_Man_t* createMonotoneTester	(	Aig_Man_t *	pAig,
		struct aigPoIndices *	aigPoIndicesArg,
		struct monotoneVectorsStruct *	monotoneVectorArg,
		int *	startMonotonePropPo
	)

Definition at line 145 of file monotone.c.

{
    Aig_Man_t *pNewAig;
    int iElem, i, nRegCount, oldPoNum, poSerialNum, iElemHint;
    int piCopied = 0, liCopied = 0, liCreated = 0, loCopied = 0, loCreated = 0;
    int poCopied = 0, poCreated = 0;
    Aig_Obj_t *pObj, *pObjPo, *pObjDriver, *pObjDriverNew, *pObjPendingDriverNew, *pObjPendingAndNextPending;
    Aig_Obj_t *pPendingFlop, *pHintSignalLo, *pHintMonotoneFlop, *pObjTemp1, *pObjTemp2, *pObjKnownMonotoneAnd;
    Vec_Ptr_t *vHintMonotoneLocalDriverNew;
    Vec_Ptr_t *vHintMonotoneLocalFlopOutput;
    Vec_Ptr_t *vHintMonotoneLocalProp;

    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
    int hintSingalBeginningMarkerLocal = aigPoIndicesArg->attrHintSingalBeginningMarker;
    //int hintSingalEndMarkerLocal = aigPoIndicesArg->attrHintSingalEndMarker;

    Vec_Int_t *vKnownMonotoneLocal = monotoneVectorArg->attrKnownMonotone;
    Vec_Int_t *vCandMonotoneLocal = monotoneVectorArg->attrCandMonotone;
    Vec_Int_t *vHintMonotoneLocal = monotoneVectorArg->attrHintMonotone;
    
    //****************************************************************
    // 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("_monotone") + 1 );
    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "_monotone");
        pNewAig->pSpec = NULL;

    //****************************************************************
    // 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 PENDING flop 
    //****************************************************************
    loCreated++;
    pPendingFlop = Aig_ObjCreateCi( pNewAig );

    //****************************************************************
    // Step 6.a: create "D" register output for HINT_MONOTONE flop 
    //****************************************************************
    vHintMonotoneLocalFlopOutput = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
    Vec_IntForEachEntry( vHintMonotoneLocal, iElem, i )
    {
        loCreated++;
        pHintMonotoneFlop = Aig_ObjCreateCi( pNewAig );
        Vec_PtrPush( vHintMonotoneLocalFlopOutput, pHintMonotoneFlop );
    }

    nRegCount = loCreated + loCopied;
    printf("\nnRegCount = %d\n", nRegCount);

    //********************************************************************
    // Step 7: create internal nodes
    //********************************************************************
        Aig_ManForEachNode( pAig, pObj, i )
    {
        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }
    
    //********************************************************************
    // Step 8: mapping appropriate new flop drivers 
    //********************************************************************

    pObjPo = Aig_ManCo( pAig, pendingSignalIndexLocal );
    pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
    pObjPendingDriverNew = !Aig_IsComplement(pObjDriver)? 
                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));

    pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingDriverNew, pPendingFlop );

    oldPoNum = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
    pObjKnownMonotoneAnd = Aig_ManConst1( pNewAig );
    #if 1
    if( vKnownMonotoneLocal )
    {
        assert( checkSanityOfKnownMonotone( vKnownMonotoneLocal, vCandMonotoneLocal, vHintMonotoneLocal ) );

        Vec_IntForEachEntry( vKnownMonotoneLocal, iElemHint, i )
        {
            iElem = (iElemHint - hintSingalBeginningMarkerLocal) + 1 + pendingSignalIndexLocal;
            printf("\nProcessing knownMonotone = %d\n", iElem);
            pObjPo = Aig_ManCo( pAig, iElem );
            pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
            pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
                    (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
                    Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
            pHintSignalLo = (Aig_Obj_t *)Vec_PtrEntry(vHintMonotoneLocalFlopOutput, iElem - oldPoNum);
            pObjTemp1 = Aig_Or( pNewAig, Aig_And(pNewAig, pObjDriverNew, pHintSignalLo), 
                        Aig_And(pNewAig, Aig_Not(pObjDriverNew), Aig_Not(pHintSignalLo)) );
            
            pObjKnownMonotoneAnd = Aig_And( pNewAig, pObjKnownMonotoneAnd, pObjTemp1 );
        }
        pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingAndNextPending, pObjKnownMonotoneAnd );
    }
    #endif

    vHintMonotoneLocalDriverNew = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
    vHintMonotoneLocalProp = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
    Vec_IntForEachEntry( vHintMonotoneLocal, iElem, i )
    {
        pObjPo = Aig_ManCo( pAig, iElem );
        pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
        pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));

        if( vKnownMonotoneLocal != NULL && Vec_IntFind( vKnownMonotoneLocal, iElem ) != -1 )
        {
            Vec_PtrPush(vHintMonotoneLocalDriverNew, pObjDriverNew);
        }
        else
        {
            poSerialNum = Vec_IntFind( vHintMonotoneLocal, iElem );
            pHintSignalLo = (Aig_Obj_t *)Vec_PtrEntry(vHintMonotoneLocalFlopOutput, poSerialNum );
            pObjTemp1 = Aig_And( pNewAig, pObjPendingAndNextPending, pHintSignalLo);
            pObjTemp2 = Aig_Or( pNewAig, Aig_Not(pObjTemp1), pObjDriverNew );
            //pObjTemp2 = Aig_Or( pNewAig, Aig_Not(pObjTemp1), Aig_ManConst1( pNewAig ));
            //pObjTemp2 = Aig_ManConst1( pNewAig );
            Vec_PtrPush(vHintMonotoneLocalDriverNew, pObjDriverNew);
            Vec_PtrPush(vHintMonotoneLocalProp, pObjTemp2); 
        }
    }

    //********************************************************************
    // Step 9: create primary outputs 
    //********************************************************************
    Saig_ManForEachPo( pAig, pObj, i )
    {
        poCopied++;
        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
    }

    *startMonotonePropPo = i;
    Vec_PtrForEachEntry( Aig_Obj_t *, vHintMonotoneLocalProp, pObj, i )
    {
        poCreated++;
        pObjPo = Aig_ObjCreateCo( pNewAig, pObj ); 
    }

    //********************************************************************
    // Step 9: create latch inputs 
    //********************************************************************

    Saig_ManForEachLi( pAig, pObj, i )
    {
        liCopied++;
        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
    }
    
    //********************************************************************
    // Step 9.a: create latch input for PENDING_FLOP
    //********************************************************************

    liCreated++;
    Aig_ObjCreateCo( pNewAig, pObjPendingDriverNew );

    //********************************************************************
    // Step 9.b: create latch input for MONOTONE_FLOP
    //********************************************************************

    Vec_PtrForEachEntry( Aig_Obj_t *, vHintMonotoneLocalDriverNew, pObj, i )
    {
        liCreated++;
        Aig_ObjCreateCo( pNewAig, pObj );
    }

    printf("\npoCopied = %d, poCreated = %d\n", poCopied, poCreated);
    printf("\nliCreated++ = %d\n", liCreated );
    Aig_ManSetRegNum( pNewAig, nRegCount );
    Aig_ManCleanup( pNewAig );
    
    assert( Aig_ManCheck( pNewAig ) );
    assert( loCopied + loCreated == liCopied + liCreated );

    printf("\nSaig_ManPoNum = %d\n", Saig_ManPoNum(pNewAig));
    return pNewAig;
}

void deallocAigPoIndices

(

struct aigPoIndices *

toBeDeletedAigPoIndices

)

Definition at line 57 of file monotone.c.

{
    assert(toBeDeletedAigPoIndices != NULL );
    free(toBeDeletedAigPoIndices);
}

void deallocPointersToMonotoneVectors

(

struct monotoneVectorsStruct *

toBeDeleted

)

Definition at line 84 of file monotone.c.

{
    assert( toBeDeleted != NULL );
    free( toBeDeleted );
}

Vec_Int_t* findHintOutputs

(

Abc_Ntk_t *

pNtk

)

Definition at line 90 of file monotone.c.

{
    int i, numElementPush = 0;
    Abc_Obj_t *pNode;
    Vec_Int_t *vHintPoIntdex;

    vHintPoIntdex = Vec_IntAlloc(0);
    Abc_NtkForEachPo( pNtk, pNode, i )
    {
        if( strstr( Abc_ObjName( pNode ), "hint_" ) != NULL )
        {
            Vec_IntPush( vHintPoIntdex, i );
            numElementPush++;
        }
    }   
    
    if( numElementPush == 0 )
        return NULL;
    else
        return vHintPoIntdex;
}

Vec_Int_t* findMonotoneSignals

(

Abc_Ntk_t *

pNtk

)

Definition at line 413 of file monotone.c.

{
    Aig_Man_t *pAig;
    Vec_Int_t *vCandidateMonotoneSignals;
    Vec_Int_t *vKnownMonotoneSignals;
    //Vec_Int_t *vKnownMonotoneSignalsNew;
    //Vec_Int_t *vRemainingCanMonotone;
    int i, iElem;
    int pendingSignalIndex;
    Abc_Ntk_t *pNtkTemp;
    int hintSingalBeginningMarker;
    int hintSingalEndMarker;
    struct aigPoIndices *aigPoIndicesInstance;
    struct monotoneVectorsStruct *monotoneVectorsInstance;
    
    /*******************************************/   
    //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;

    /****************************************************/
    //Allocating "struct" with necessary monotone vectors
    /****************************************************/
    monotoneVectorsInstance = allocPointersToMonotoneVectors();
    monotoneVectorsInstance->attrCandMonotone = vCandidateMonotoneSignals;
    monotoneVectorsInstance->attrHintMonotone = 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
    /*******************************************/   
    vKnownMonotoneSignals = findNewMonotone( pAig, aigPoIndicesInstance, monotoneVectorsInstance );
    monotoneVectorsInstance->attrKnownMonotone = vKnownMonotoneSignals;

    /*******************************************/   
    //finding LEVEL >1 monotone signals
    /*******************************************/   
    #if 0
    if( vKnownMonotoneSignals )
    {
        printf("\nsize = %d\n", Vec_IntSize(vKnownMonotoneSignals) );
        vRemainingCanMonotone = findRemainingMonotoneCandidates(vKnownMonotoneSignals, vCandidateMonotoneSignals);
        monotoneVectorsInstance->attrCandMonotone = vRemainingCanMonotone; 
        vKnownMonotoneSignalsNew = findNewMonotone( pAig, aigPoIndicesInstance, monotoneVectorsInstance );
    }
    #endif 

    deallocAigPoIndices(aigPoIndicesInstance);
    deallocPointersToMonotoneVectors(monotoneVectorsInstance);
    return NULL;
}

Vec_Int_t* findNewMonotone	(	Aig_Man_t *	pAig,
		struct aigPoIndices *	aigPoIndicesArg,
		struct monotoneVectorsStruct *	monotoneVectorArg
	)

Definition at line 348 of file monotone.c.

{
    Aig_Man_t *pAigNew;
    Aig_Obj_t *pObjTargetPo;
    int poMarker, oldPoNum;
    int i, RetValue;
    Pdr_Par_t Pars, * pPars = &Pars;
    Abc_Cex_t * pCex = NULL;
    Vec_Int_t *vMonotoneIndex;

    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
    int hintSingalBeginningMarkerLocal = aigPoIndicesArg->attrHintSingalBeginningMarker;
    //int hintSingalEndMarkerLocal = aigPoIndicesArg->attrHintSingalEndMarker;

    //Vec_Int_t *vKnownMonotoneLocal = monotoneVectorArg->attrKnownMonotone;
    //Vec_Int_t *vCandMonotoneLocal = monotoneVectorArg->attrCandMonotone;
    //Vec_Int_t *vHintMonotoneLocal = monotoneVectorArg->attrHintMonotone;

    pAigNew = createMonotoneTester(pAig, aigPoIndicesArg, monotoneVectorArg, &poMarker );
    oldPoNum = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);

    vMonotoneIndex = Vec_IntAlloc(0);
    printf("\nSaig_ManPoNum(pAigNew) = %d, poMarker = %d\n", Saig_ManPoNum(pAigNew), poMarker);
    for( i=poMarker; i<Saig_ManPoNum(pAigNew); i++ )
    {
        pObjTargetPo = Aig_ManCo( pAigNew, i );
        Aig_ObjChild0Flip( pObjTargetPo );

        Pdr_ManSetDefaultParams( pPars );
        pCex = NULL;
        pPars->fVerbose = 0;
        //pPars->iOutput = i;
        //RetValue = Pdr_ManSolve( pAigNew, pPars, &pCex ); 
        RetValue = Pdr_ManSolve( pAigNew, pPars );  
        if( RetValue == 1 )
        {
            printf("\ni = %d, RetValue = %d : %s (Frame %d)\n", i - oldPoNum + hintSingalBeginningMarkerLocal, RetValue, "Property Proved", pCex? (pCex)->iFrame : -1 );
            Vec_IntPush( vMonotoneIndex, i - (pendingSignalIndexLocal + 1) + hintSingalBeginningMarkerLocal);
        }
        Aig_ObjChild0Flip( pObjTargetPo );
    }
    
    if( Vec_IntSize( vMonotoneIndex ) > 0 )
        return vMonotoneIndex;
    else
        return NULL;
}

int findPendingSignal

(

Abc_Ntk_t *

pNtk

)

Definition at line 112 of file monotone.c.

{
    int i, pendingSignalIndex = -1;
    Abc_Obj_t *pNode;

    Abc_NtkForEachPo( pNtk, pNode, i )
    {
        if( strstr( Abc_ObjName( pNode ), "pendingSignal" ) != NULL )
        {
            pendingSignalIndex = i;
            break;
        }
    }   
    
    return pendingSignalIndex;
}

Vec_Int_t* findRemainingMonotoneCandidates	(	Vec_Int_t *	vKnownMonotone,
		Vec_Int_t *	vHintMonotone
	)

Definition at line 396 of file monotone.c.

{
    Vec_Int_t *vCandMonotone;
    int iElem, i;

    if( vKnownMonotone == NULL || Vec_IntSize(vKnownMonotone) <= 0 )
        return vHintMonotone;
    vCandMonotone = Vec_IntAlloc(0);
    Vec_IntForEachEntry( vHintMonotone, iElem, i )
    {
        if( Vec_IntFind( vKnownMonotone, iElem ) == -1 )
            Vec_IntPush( vCandMonotone, iElem );
    }
    
    return vCandMonotone;
}