luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/proof/live/disjunctiveMonotone.c

758 lines
26 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [disjunctiveMonotone.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.]
***********************************************************************/
#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>
ABC_NAMESPACE_IMPL_START
struct aigPoIndices
{
int attrPendingSignalIndex;
int attrHintSingalBeginningMarker;
int attrHintSingalEndMarker;
int attrSafetyInvarIndex;
};
extern struct aigPoIndices *allocAigPoIndices();
extern void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices);
extern int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk);
struct antecedentConsequentVectorsStruct
{
Vec_Int_t *attrAntecedents;
Vec_Int_t *attrConsequentCandidates;
};
struct antecedentConsequentVectorsStruct *allocAntecedentConsequentVectorsStruct()
{
struct antecedentConsequentVectorsStruct *newStructure;
newStructure = (struct antecedentConsequentVectorsStruct *)malloc(sizeof (struct antecedentConsequentVectorsStruct));
newStructure->attrAntecedents = NULL;
newStructure->attrConsequentCandidates = NULL;
assert( newStructure != NULL );
return newStructure;
}
void deallocAntecedentConsequentVectorsStruct(struct antecedentConsequentVectorsStruct *toBeDeleted)
{
assert( toBeDeleted != NULL );
if(toBeDeleted->attrAntecedents)
Vec_IntFree( toBeDeleted->attrAntecedents );
if(toBeDeleted->attrConsequentCandidates)
Vec_IntFree( toBeDeleted->attrConsequentCandidates );
free( toBeDeleted );
}
Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg,
struct antecedentConsequentVectorsStruct *anteConseVectors, int *startMonotonePropPo)
{
Aig_Man_t *pNewAig;
int iElem, i, nRegCount;
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, *pObjConseCandFlop, *pObjSafetyInvariantPoDriver;
//Vec_Ptr_t *vHintMonotoneLocalDriverNew;
Vec_Ptr_t *vConseCandFlopOutput;
//Vec_Ptr_t *vHintMonotoneLocalProp;
Aig_Obj_t *pObjAnteDisjunction, *pObjConsecDriver, *pObjConsecDriverNew, *pObjCandMonotone, *pObjPrevCandMonotone, *pObjMonotonePropDriver;
Vec_Ptr_t *vCandMonotoneProp;
Vec_Ptr_t *vCandMonotoneFlopInput;
int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
Vec_Int_t *vAntecedentsLocal = anteConseVectors->attrAntecedents;
Vec_Int_t *vConsequentCandidatesLocal = anteConseVectors->attrConsequentCandidates;
if( vConsequentCandidatesLocal == NULL )
return NULL; //no candidates for consequent is provided, hence no need to generate a new AIG
//****************************************************************
// 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") + 2 );
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
//****************************************************************
vConseCandFlopOutput = Vec_PtrAlloc(Vec_IntSize(vConsequentCandidatesLocal));
Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
{
loCreated++;
pObjConseCandFlop = Aig_ObjCreateCi( pNewAig );
Vec_PtrPush( vConseCandFlopOutput, pObjConseCandFlop );
}
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: mapping appropriate new flop drivers
//********************************************************************
if( aigPoIndicesArg->attrSafetyInvarIndex != -1 )
{
pObjPo = Aig_ManCo( pAig, aigPoIndicesArg->attrSafetyInvarIndex );
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));
pObjSafetyInvariantPoDriver = pObjDriverNew;
}
else
pObjSafetyInvariantPoDriver = Aig_ManConst1(pNewAig);
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 );
pObjAnteDisjunction = Aig_Not(Aig_ManConst1( pNewAig ));
if( vAntecedentsLocal )
{
Vec_IntForEachEntry( vAntecedentsLocal, 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));
pObjAnteDisjunction = Aig_Or( pNewAig, pObjDriverNew, pObjAnteDisjunction );
}
}
vCandMonotoneProp = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
vCandMonotoneFlopInput = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
{
pObjPo = Aig_ManCo( pAig, iElem );
pObjConsecDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
pObjConsecDriverNew = !Aig_IsComplement(pObjConsecDriver)?
(Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData) :
Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData));
pObjCandMonotone = Aig_Or( pNewAig, pObjConsecDriverNew, pObjAnteDisjunction );
pObjPrevCandMonotone = (Aig_Obj_t *)(Vec_PtrEntry( vConseCandFlopOutput, i ));
pObjMonotonePropDriver = Aig_Or( pNewAig, Aig_Not( Aig_And( pNewAig, pObjPendingAndNextPending, pObjPrevCandMonotone ) ),
pObjCandMonotone );
//Conjunting safety invar
pObjMonotonePropDriver = Aig_And( pNewAig, pObjMonotonePropDriver, pObjSafetyInvariantPoDriver );
Vec_PtrPush( vCandMonotoneFlopInput, pObjCandMonotone );
Vec_PtrPush( vCandMonotoneProp, pObjMonotonePropDriver );
}
//********************************************************************
// 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 *, vCandMonotoneProp, 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 *, vCandMonotoneFlopInput, pObj, i )
{
liCreated++;
Aig_ObjCreateCo( pNewAig, pObj );
}
Aig_ManSetRegNum( pNewAig, nRegCount );
Aig_ManCleanup( pNewAig );
assert( Aig_ManCheck( pNewAig ) );
assert( loCopied + loCreated == liCopied + liCreated );
Vec_PtrFree(vConseCandFlopOutput);
Vec_PtrFree(vCandMonotoneProp);
Vec_PtrFree(vCandMonotoneFlopInput);
return pNewAig;
}
Vec_Int_t *findNewDisjunctiveMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct antecedentConsequentVectorsStruct *anteConseVectors )
{
Aig_Man_t *pAigNew;
Aig_Obj_t *pObjTargetPo;
int poMarker;
//int i, RetValue, poSerialNum;
int i, poSerialNum;
Pdr_Par_t Pars, * pPars = &Pars;
//Abc_Cex_t * pCex = NULL;
Vec_Int_t *vMonotoneIndex;
//char fileName[20];
Abc_Cex_t * cexElem;
int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
pAigNew = createDisjunctiveMonotoneTester(pAig, aigPoIndicesArg, anteConseVectors, &poMarker );
//printf("enter an integer : ");
//waitForInteger = getchar();
//putchar(waitForInteger);
vMonotoneIndex = Vec_IntAlloc(0);
for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
{
pObjTargetPo = Aig_ManCo( pAigNew, i );
Aig_ObjChild0Flip( pObjTargetPo );
}
Pdr_ManSetDefaultParams( pPars );
pPars->fVerbose = 0;
pPars->fNotVerbose = 1;
pPars->fSolveAll = 1;
pAigNew->vSeqModelVec = NULL;
Pdr_ManSolve( pAigNew, pPars );
if( pAigNew->vSeqModelVec )
{
Vec_PtrForEachEntry( Abc_Cex_t *, pAigNew->vSeqModelVec, cexElem, i )
{
if( cexElem == NULL && i >= pendingSignalIndexLocal + 1)
{
poSerialNum = i - (pendingSignalIndexLocal + 1);
Vec_IntPush( vMonotoneIndex, Vec_IntEntry( anteConseVectors->attrConsequentCandidates, poSerialNum ));
}
}
}
for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
{
pObjTargetPo = Aig_ManCo( pAigNew, i );
Aig_ObjChild0Flip( pObjTargetPo );
}
//if(pAigNew->vSeqModelVec)
// Vec_PtrFree(pAigNew->vSeqModelVec);
Aig_ManStop(pAigNew);
if( Vec_IntSize( vMonotoneIndex ) > 0 )
{
return vMonotoneIndex;
}
else
{
Vec_IntFree(vMonotoneIndex);
return NULL;
}
}
Vec_Int_t *updateAnteConseVectors(struct antecedentConsequentVectorsStruct *anteConse )
{
Vec_Int_t *vCandMonotone;
int iElem, i;
//if( vKnownMonotone == NULL || Vec_IntSize(vKnownMonotone) <= 0 )
// return vHintMonotone;
if( anteConse->attrAntecedents == NULL || Vec_IntSize(anteConse->attrAntecedents) <= 0 )
return anteConse->attrConsequentCandidates;
vCandMonotone = Vec_IntAlloc(0);
Vec_IntForEachEntry( anteConse->attrConsequentCandidates, iElem, i )
{
if( Vec_IntFind( anteConse->attrAntecedents, iElem ) == -1 )
Vec_IntPush( vCandMonotone, iElem );
}
return vCandMonotone;
}
Vec_Int_t *vectorDifference(Vec_Int_t *A, Vec_Int_t *B)
{
Vec_Int_t *C;
int iElem, i;
C = Vec_IntAlloc(0);
Vec_IntForEachEntry( A, iElem, i )
{
if( Vec_IntFind( B, iElem ) == -1 )
{
Vec_IntPush( C, iElem );
}
}
return C;
}
Vec_Int_t *createSingletonIntVector( int iElem )
{
Vec_Int_t *myVec = Vec_IntAlloc(1);
Vec_IntPush(myVec, iElem);
return myVec;
}
#if 0
Vec_Ptr_t *generateDisjuntiveMonotone_rec()
{
nextLevelSignals = ;
if level is not exhausted
for all x \in nextLevelSignals
{
append x in currAntecendent
recond it as a monotone predicate
resurse with level - 1
}
}
#endif
#if 0
Vec_Ptr_t *generateDisjuntiveMonotoneLevels(Aig_Man_t *pAig,
struct aigPoIndices *aigPoIndicesInstance,
struct antecedentConsequentVectorsStruct *anteConsecInstanceOrig,
int level )
{
Vec_Int_t *firstLevelMonotone;
Vec_Int_t *currVecInt;
Vec_Ptr_t *hierarchyList;
int iElem, i;
assert( level >= 1 );
firstLevelMonotone = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
if( firstLevelMonotone == NULL || Vec_IntSize(firstLevelMonotone) <= 0 )
return NULL;
hierarchyList = Vec_PtrAlloc(Vec_IntSize(firstLevelMonotone));
Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
{
currVecInt = createSingletonIntVector( iElem );
Vec_PtrPush( hierarchyList, currVecInt );
}
if( level > 1 )
{
Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
{
currVecInt = (Vec_Int_t *)Vec_PtrEntry( hierarchyList, i );
}
}
return hierarchyList;
}
#endif
int Vec_IntPushUniqueLocal( Vec_Int_t * p, int Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
return 1;
Vec_IntPush( p, Entry );
return 0;
}
Vec_Ptr_t *findNextLevelDisjunctiveMonotone(
Aig_Man_t *pAig,
struct aigPoIndices *aigPoIndicesInstance,
struct antecedentConsequentVectorsStruct *anteConsecInstance,
Vec_Ptr_t *previousMonotoneVectors )
{
Vec_Ptr_t *newLevelPtrVec;
Vec_Int_t *vElem, *vNewDisjunctVector, *newDisjunction;
int i, j, iElem;
struct antecedentConsequentVectorsStruct *anteConsecInstanceLocal;
Vec_Int_t *vUnionPrevMonotoneVector, *vDiffVector;
newLevelPtrVec = Vec_PtrAlloc(0);
vUnionPrevMonotoneVector = Vec_IntAlloc(0);
Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
Vec_IntForEachEntry( vElem, iElem, j )
Vec_IntPushUniqueLocal( vUnionPrevMonotoneVector, iElem );
Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
{
anteConsecInstanceLocal = allocAntecedentConsequentVectorsStruct();
anteConsecInstanceLocal->attrAntecedents = Vec_IntDup(vElem);
vDiffVector = vectorDifference( anteConsecInstance->attrConsequentCandidates, vUnionPrevMonotoneVector);
anteConsecInstanceLocal->attrConsequentCandidates = vDiffVector;
assert( vDiffVector );
//printf("Calling target function %d\n", i);
vNewDisjunctVector = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstanceLocal );
if( vNewDisjunctVector )
{
Vec_IntForEachEntry(vNewDisjunctVector, iElem, j)
{
newDisjunction = Vec_IntDup(vElem);
Vec_IntPush( newDisjunction, iElem );
Vec_PtrPush( newLevelPtrVec, newDisjunction );
}
Vec_IntFree(vNewDisjunctVector);
}
deallocAntecedentConsequentVectorsStruct( anteConsecInstanceLocal );
}
Vec_IntFree(vUnionPrevMonotoneVector);
return newLevelPtrVec;
}
void printAllIntVectors(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
{
Vec_Int_t *vElem;
int i, j, iElem;
char *name, *hintSubStr;
FILE *fp;
fp = fopen( fileName, "a" );
Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
{
fprintf(fp, "( ");
Vec_IntForEachEntry( vElem, iElem, j )
{
name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
hintSubStr = strstr( name, "hint");
assert( hintSubStr );
fprintf(fp, "%s", hintSubStr);
if( j < Vec_IntSize(vElem) - 1 )
{
fprintf(fp, " || ");
}
else
{
fprintf(fp, " )\n");
}
}
}
fclose(fp);
}
void printAllIntVectorsStabil(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
{
Vec_Int_t *vElem;
int i, j, iElem;
char *name, *hintSubStr;
FILE *fp;
fp = fopen( fileName, "a" );
Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
{
printf("INT[%d] : ( ", i);
fprintf(fp, "( ");
Vec_IntForEachEntry( vElem, iElem, j )
{
name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
hintSubStr = strstr( name, "csLevel1Stabil");
assert( hintSubStr );
printf("%s", hintSubStr);
fprintf(fp, "%s", hintSubStr);
if( j < Vec_IntSize(vElem) - 1 )
{
printf(" || ");
fprintf(fp, " || ");
}
else
{
printf(" )\n");
fprintf(fp, " )\n");
}
}
//printf(")\n");
}
fclose(fp);
}
void appendVecToMasterVecInt(Vec_Ptr_t *masterVec, Vec_Ptr_t *candVec )
{
int i;
Vec_Int_t *vCand;
Vec_Int_t *vNewIntVec;
assert(masterVec != NULL);
assert(candVec != NULL);
Vec_PtrForEachEntry( Vec_Int_t *, candVec, vCand, i )
{
vNewIntVec = Vec_IntDup(vCand);
Vec_PtrPush(masterVec, vNewIntVec);
}
}
void deallocateVecOfIntVec( Vec_Ptr_t *vecOfIntVec )
{
Vec_Int_t *vInt;
int i;
if( vecOfIntVec )
{
Vec_PtrForEachEntry( Vec_Int_t *, vecOfIntVec, vInt, i )
{
Vec_IntFree( vInt );
}
Vec_PtrFree(vecOfIntVec);
}
}
Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk )
{
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;
}
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink