abc/src/proof/live/monotone.c - third_party/vtr-verilog-to-routing - Git at Google

 /**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 $]

 ***********************************************************************/

 #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"

 ABC_NAMESPACE_IMPL_START

 extern Aig_Man_t *Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 //extern Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg, int *startMonotonePropPo);

 struct aigPoIndices
 {
     int attrPendingSignalIndex;
     int attrHintSingalBeginningMarker;
     int attrHintSingalEndMarker;
     int attrSafetyInvarIndex;
 };

 struct aigPoIndices *allocAigPoIndices()
 {
     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;
 }

 void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices)
 {
     assert(toBeDeletedAigPoIndices != NULL );
     free(toBeDeletedAigPoIndices);
 }

 struct monotoneVectorsStruct
 {
     Vec_Int_t *attrKnownMonotone;
     Vec_Int_t *attrCandMonotone;
     Vec_Int_t *attrHintMonotone;
 };

 struct monotoneVectorsStruct *allocPointersToMonotoneVectors()
 {
     struct monotoneVectorsStruct *newPointersToMonotoneVectors;

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

     newPointersToMonotoneVectors->attrKnownMonotone = NULL;
     newPointersToMonotoneVectors->attrCandMonotone = NULL;
     newPointersToMonotoneVectors->attrHintMonotone = NULL;

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

 void deallocPointersToMonotoneVectors(struct monotoneVectorsStruct *toBeDeleted)
 {
     assert( toBeDeleted != NULL );
     free( toBeDeleted );
 }

 Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk)
 {
     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;
 }

 int findPendingSignal(Abc_Ntk_t *pNtk)
 {
     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;
 }

 int checkSanityOfKnownMonotone( Vec_Int_t *vKnownMonotone, Vec_Int_t *vCandMonotone, Vec_Int_t *vHintMonotone )
 {
     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)
 {
     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;
 }


 Vec_Int_t *findNewMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg )
 {
     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;
 }

 Vec_Int_t *findRemainingMonotoneCandidates(Vec_Int_t *vKnownMonotone, Vec_Int_t *vHintMonotone)
 {
     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;
 }

 Vec_Int_t *findMonotoneSignals( Abc_Ntk_t *pNtk )
 {
     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;
 }

 ABC_NAMESPACE_IMPL_END
	/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 $]

	***********************************************************************/

	#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"

	ABC_NAMESPACE_IMPL_START

	extern Aig_Man_t Abc_NtkToDar( Abc_Ntk_t pNtk, int fExors, int fRegisters );
	//extern Aig_Man_t createDisjunctiveMonotoneTester(Aig_Man_t pAig, struct aigPoIndices aigPoIndicesArg, struct monotoneVectorsStruct monotoneVectorArg, int *startMonotonePropPo);

	struct aigPoIndices
	{
	int attrPendingSignalIndex;
	int attrHintSingalBeginningMarker;
	int attrHintSingalEndMarker;
	int attrSafetyInvarIndex;
	};

	struct aigPoIndices *allocAigPoIndices()
	{
	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;
	}

	void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices)
	{
	assert(toBeDeletedAigPoIndices != NULL );
	free(toBeDeletedAigPoIndices);
	}

	struct monotoneVectorsStruct
	{
	Vec_Int_t *attrKnownMonotone;
	Vec_Int_t *attrCandMonotone;
	Vec_Int_t *attrHintMonotone;
	};

	struct monotoneVectorsStruct *allocPointersToMonotoneVectors()
	{
	struct monotoneVectorsStruct *newPointersToMonotoneVectors;

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

	newPointersToMonotoneVectors->attrKnownMonotone = NULL;
	newPointersToMonotoneVectors->attrCandMonotone = NULL;
	newPointersToMonotoneVectors->attrHintMonotone = NULL;

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

	void deallocPointersToMonotoneVectors(struct monotoneVectorsStruct *toBeDeleted)
	{
	assert( toBeDeleted != NULL );
	free( toBeDeleted );
	}

	Vec_Int_t findHintOutputs(Abc_Ntk_t pNtk)
	{
	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;
	}

	int findPendingSignal(Abc_Ntk_t *pNtk)
	{
	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;
	}

	int checkSanityOfKnownMonotone( Vec_Int_t vKnownMonotone, Vec_Int_t vCandMonotone, Vec_Int_t *vHintMonotone )
	{
	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)
	{
	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;
	}


	Vec_Int_t findNewMonotone( Aig_Man_t pAig, struct aigPoIndices aigPoIndicesArg, struct monotoneVectorsStruct monotoneVectorArg )
	{
	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;
	}

	Vec_Int_t findRemainingMonotoneCandidates(Vec_Int_t vKnownMonotone, Vec_Int_t *vHintMonotone)
	{
	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;
	}

	Vec_Int_t findMonotoneSignals( Abc_Ntk_t pNtk )
	{
	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;
	}

	ABC_NAMESPACE_IMPL_END