diff options
Diffstat (limited to 'src/proof/live/monotone.c')
-rw-r--r-- | src/proof/live/monotone.c | 507 |
1 files changed, 507 insertions, 0 deletions
diff --git a/src/proof/live/monotone.c b/src/proof/live/monotone.c new file mode 100644 index 00000000..c8b08ed3 --- /dev/null +++ b/src/proof/live/monotone.c @@ -0,0 +1,507 @@ +/**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 |