| /**CFile**************************************************************** |
| |
| FileName [kliveness.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Liveness property checking.] |
| |
| Synopsis [Main implementation module of the algorithm k-Liveness ] |
| [invented by Koen Claessen, Niklas Sorensson. Implements] |
| [the code for 'kcs'. 'kcs' pre-processes based on switch] |
| [and then runs the (absorber circuit >> pdr) loop ] |
| |
| Author [Sayak Ray] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - October 31, 2012.] |
| |
| ***********************************************************************/ |
| |
| #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> |
| |
| //#define WITHOUT_CONSTRAINTS |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| /***************** Declaration of standard ABC related functions ********************/ |
| extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); |
| extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); |
| extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange ); |
| extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ); |
| /***********************************************************************************/ |
| |
| /***************** Declaration of kLiveness related functions **********************/ |
| //function defined in kLiveConstraints.c |
| extern Aig_Man_t *generateWorkingAig( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live ); |
| |
| //function defined in arenaViolation.c |
| extern Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers ); |
| |
| //function defined in disjunctiveMonotone.c |
| extern Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk ); |
| extern Vec_Int_t *createSingletonIntVector( int i ); |
| /***********************************************************************************/ |
| extern Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK ); |
| extern Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK ); |
| |
| //Definition of some macros pertaining to modes/switches |
| #define SIMPLE_kCS 0 |
| #define kCS_WITH_SAFETY_INVARIANTS 1 |
| #define kCS_WITH_DISCOVER_MONOTONE_SIGNALS 2 |
| #define kCS_WITH_SAFETY_AND_DCS_INVARIANTS 3 |
| #define kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS 4 |
| |
| //unused function |
| #if 0 |
| Aig_Obj_t *readTargetPinSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk) |
| { |
| Aig_Obj_t *pObj; |
| int i; |
| |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "0Liveness_" ) != NULL ) |
| { |
| //return Aig_ObjFanin0(pObj); |
| return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); |
| } |
| } |
| |
| return NULL; |
| } |
| #endif |
| |
| Aig_Obj_t *readLiveSignal_0( Aig_Man_t *pAig, int liveIndex_0 ) |
| { |
| Aig_Obj_t *pObj; |
| |
| pObj = Aig_ManCo( pAig, liveIndex_0 ); |
| return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); |
| } |
| |
| Aig_Obj_t *readLiveSignal_k( Aig_Man_t *pAig, int liveIndex_k ) |
| { |
| Aig_Obj_t *pObj; |
| |
| pObj = Aig_ManCo( pAig, liveIndex_k ); |
| return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); |
| } |
| |
| //unused funtion |
| #if 0 |
| Aig_Obj_t *readTargetPoutSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int nonFirstIteration) |
| { |
| Aig_Obj_t *pObj; |
| int i; |
| |
| if( nonFirstIteration == 0 ) |
| return NULL; |
| else |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "kLiveness_" ) != NULL ) |
| { |
| //return Aig_ObjFanin0(pObj); |
| return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); |
| } |
| } |
| |
| return NULL; |
| } |
| #endif |
| |
| //unused function |
| #if 0 |
| void updateNewNetworkNameManager_kCS( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, |
| Vec_Ptr_t *vLoNames, Vec_Ptr_t *vPoNames, Vec_Ptr_t *vLiNames ) |
| { |
| Aig_Obj_t *pObj; |
| Abc_Obj_t *pNode; |
| int i, ntkObjId; |
| |
| pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) ); |
| |
| if( vPiNames ) |
| { |
| Saig_ManForEachPi( pAig, pObj, i ) |
| { |
| ntkObjId = Abc_NtkCi( pNtk, i )->Id; |
| Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL ); |
| } |
| } |
| if( vLoNames ) |
| { |
| Saig_ManForEachLo( pAig, pObj, i ) |
| { |
| ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id; |
| Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL ); |
| } |
| } |
| |
| if( vPoNames ) |
| { |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| ntkObjId = Abc_NtkCo( pNtk, i )->Id; |
| Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPoNames, i), NULL ); |
| } |
| } |
| |
| if( vLiNames ) |
| { |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| ntkObjId = Abc_NtkCo( pNtk, Saig_ManPoNum( pAig ) + i )->Id; |
| Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLiNames, i), NULL ); |
| } |
| } |
| |
| // assign latch input names |
| Abc_NtkForEachLatch(pNtk, pNode, i) |
| if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL ) |
| Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL ); |
| } |
| #endif |
| |
| Aig_Man_t *introduceAbsorberLogic( Aig_Man_t *pAig, int *pLiveIndex_0, int *pLiveIndex_k, int nonFirstIteration ) |
| { |
| Aig_Man_t *pNewAig; |
| Aig_Obj_t *pObj, *pObjAbsorberLo, *pPInNewArg, *pPOutNewArg; |
| Aig_Obj_t *pPIn = NULL, *pPOut = NULL, *pPOutCo = NULL; |
| Aig_Obj_t *pFirstAbsorberOr, *pSecondAbsorberOr; |
| int i; |
| int piCopied = 0, loCreated = 0, loCopied = 0, liCreated = 0, liCopied = 0; |
| int nRegCount; |
| |
| assert(*pLiveIndex_0 != -1); |
| if(nonFirstIteration == 0) |
| assert( *pLiveIndex_k == -1 ); |
| else |
| assert( *pLiveIndex_k != -1 ); |
| |
| //**************************************************************** |
| // Step1: create the new manager |
| // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)" |
| // nodes, but this selection is arbitrary - need to be justified |
| //**************************************************************** |
| pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) ); |
| pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_kCS") + 1 ); |
| sprintf(pNewAig->pName, "%s_%s", pAig->pName, "kCS"); |
| pNewAig->pSpec = NULL; |
| |
| //**************************************************************** |
| // reading the signal pIn, and pOut |
| //**************************************************************** |
| |
| pPIn = readLiveSignal_0( pAig, *pLiveIndex_0 ); |
| if( *pLiveIndex_k == -1 ) |
| pPOut = NULL; |
| else |
| pPOut = readLiveSignal_k( pAig, *pLiveIndex_k ); |
| |
| //**************************************************************** |
| // Step 2: map constant nodes |
| //**************************************************************** |
| pObj = Aig_ManConst1( pAig ); |
| pObj->pData = Aig_ManConst1( pNewAig ); |
| |
| //**************************************************************** |
| // Step 3: create true PIs |
| //**************************************************************** |
| Saig_ManForEachPi( pAig, pObj, i ) |
| { |
| piCopied++; |
| pObj->pData = Aig_ObjCreateCi(pNewAig); |
| } |
| |
| //**************************************************************** |
| // Step 5: create register outputs |
| //**************************************************************** |
| Saig_ManForEachLo( pAig, pObj, i ) |
| { |
| loCopied++; |
| pObj->pData = Aig_ObjCreateCi(pNewAig); |
| } |
| |
| //**************************************************************** |
| // Step 6: create "D" register output for the ABSORBER logic |
| //**************************************************************** |
| loCreated++; |
| pObjAbsorberLo = Aig_ObjCreateCi( pNewAig ); |
| |
| nRegCount = loCreated + loCopied; |
| |
| //******************************************************************** |
| // Step 7: create internal nodes |
| //******************************************************************** |
| Aig_ManForEachNode( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| } |
| |
| //**************************************************************** |
| // Step 8: create the two OR gates of the OBSERVER logic |
| //**************************************************************** |
| if( nonFirstIteration == 0 ) |
| { |
| assert(pPIn); |
| |
| pPInNewArg = !Aig_IsComplement(pPIn)? |
| (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : |
| Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData)); |
| |
| pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPInNewArg), pObjAbsorberLo ); |
| pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) ); |
| } |
| else |
| { |
| assert( pPOut ); |
| |
| pPInNewArg = !Aig_IsComplement(pPIn)? |
| (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : |
| Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData)); |
| pPOutNewArg = !Aig_IsComplement(pPOut)? |
| (Aig_Obj_t *)((Aig_Regular(pPOut))->pData) : |
| Aig_Not((Aig_Obj_t *)((Aig_Regular(pPOut))->pData)); |
| |
| pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPOutNewArg), pObjAbsorberLo ); |
| pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) ); |
| } |
| |
| //******************************************************************** |
| // Step 9: create primary outputs |
| //******************************************************************** |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); |
| if( i == *pLiveIndex_k ) |
| pPOutCo = (Aig_Obj_t *)(pObj->pData); |
| } |
| |
| //create new po |
| if( nonFirstIteration == 0 ) |
| { |
| assert(pPOutCo == NULL); |
| pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr ); |
| |
| *pLiveIndex_k = i; |
| } |
| else |
| { |
| assert( pPOutCo != NULL ); |
| //pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr ); |
| //*pLiveIndex_k = Saig_ManPoNum(pAig); |
| |
| Aig_ObjPatchFanin0( pNewAig, pPOutCo, pSecondAbsorberOr ); |
| } |
| |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| liCopied++; |
| Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); |
| } |
| |
| //create new li |
| liCreated++; |
| Aig_ObjCreateCo( pNewAig, pFirstAbsorberOr ); |
| |
| Aig_ManSetRegNum( pNewAig, nRegCount ); |
| Aig_ManCleanup( pNewAig ); |
| |
| assert( Aig_ManCheck( pNewAig ) ); |
| |
| assert( *pLiveIndex_k != - 1); |
| return pNewAig; |
| } |
| |
| void modifyAigToApplySafetyInvar(Aig_Man_t *pAig, int csTarget, int safetyInvarPO) |
| { |
| Aig_Obj_t *pObjPOSafetyInvar, *pObjSafetyInvar; |
| Aig_Obj_t *pObjPOCSTarget, *pObjCSTarget; |
| Aig_Obj_t *pObjCSTargetNew; |
| |
| pObjPOSafetyInvar = Aig_ManCo( pAig, safetyInvarPO ); |
| pObjSafetyInvar = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOSafetyInvar), Aig_ObjFaninC0(pObjPOSafetyInvar)); |
| pObjPOCSTarget = Aig_ManCo( pAig, csTarget ); |
| pObjCSTarget = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOCSTarget), Aig_ObjFaninC0(pObjPOCSTarget)); |
| |
| pObjCSTargetNew = Aig_And( pAig, pObjSafetyInvar, pObjCSTarget ); |
| Aig_ObjPatchFanin0( pAig, pObjPOCSTarget, pObjCSTargetNew ); |
| } |
| |
| int flipConePdr( Aig_Man_t *pAig, int directive, int targetCSPropertyIndex, int safetyInvariantPOIndex, int absorberCount ) |
| { |
| int RetValue, i; |
| Aig_Obj_t *pObjTargetPo; |
| Aig_Man_t *pAigDupl; |
| Pdr_Par_t Pars, * pPars = &Pars; |
| Abc_Cex_t * pCex = NULL; |
| |
| char *fileName; |
| |
| fileName = (char *)malloc(sizeof(char) * 50); |
| sprintf(fileName, "%s_%d.%s", "kLive", absorberCount, "blif" ); |
| |
| if( directive == kCS_WITH_SAFETY_INVARIANTS || directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS ) |
| { |
| assert( safetyInvariantPOIndex != -1 ); |
| modifyAigToApplySafetyInvar(pAig, targetCSPropertyIndex, safetyInvariantPOIndex); |
| } |
| |
| pAigDupl = pAig; |
| pAig = Aig_ManDupSimple( pAigDupl ); |
| |
| for( i=0; i<Saig_ManPoNum(pAig); i++ ) |
| { |
| pObjTargetPo = Aig_ManCo( pAig, i ); |
| Aig_ObjChild0Flip( pObjTargetPo ); |
| } |
| |
| Pdr_ManSetDefaultParams( pPars ); |
| pPars->fVerbose = 1; |
| pPars->fNotVerbose = 1; |
| pPars->fSolveAll = 1; |
| pAig->vSeqModelVec = NULL; |
| |
| Aig_ManCleanup( pAig ); |
| assert( Aig_ManCheck( pAig ) ); |
| |
| Pdr_ManSolve( pAig, pPars ); |
| |
| if( pAig->vSeqModelVec ) |
| { |
| pCex = (Abc_Cex_t *)Vec_PtrEntry( pAig->vSeqModelVec, targetCSPropertyIndex ); |
| if( pCex == NULL ) |
| { |
| RetValue = 1; |
| } |
| else |
| RetValue = 0; |
| } |
| else |
| { |
| RetValue = -1; |
| exit(0); |
| } |
| |
| free(fileName); |
| |
| for( i=0; i<Saig_ManPoNum(pAig); i++ ) |
| { |
| pObjTargetPo = Aig_ManCo( pAig, i ); |
| Aig_ObjChild0Flip( pObjTargetPo ); |
| } |
| |
| Aig_ManStop( pAig ); |
| return RetValue; |
| } |
| |
| //unused function |
| #if 0 |
| int read0LiveIndex( Abc_Ntk_t *pNtk ) |
| { |
| Abc_Obj_t *pObj; |
| int i; |
| |
| Abc_NtkForEachPo( pNtk, pObj, i ) |
| { |
| if( strstr( Abc_ObjName( pObj ), "0Liveness_" ) != NULL ) |
| return i; |
| } |
| |
| return -1; |
| } |
| #endif |
| |
| int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk) |
| { |
| Abc_Obj_t *pObj; |
| int i; |
| |
| Abc_NtkForEachPo( pNtk, pObj, i ) |
| { |
| if( strstr( Abc_ObjName( pObj ), "csSafetyInvar_" ) != NULL ) |
| return i; |
| } |
| |
| return -1; |
| } |
| |
| Vec_Ptr_t *collectUserGivenDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk ) |
| { |
| Abc_Obj_t *pObj; |
| int i; |
| Vec_Ptr_t *monotoneVector; |
| Vec_Int_t *newIntVector; |
| |
| monotoneVector = Vec_PtrAlloc(0); |
| Abc_NtkForEachPo( pNtk, pObj, i ) |
| { |
| if( strstr( Abc_ObjName( pObj ), "csLevel1Stabil_" ) != NULL ) |
| { |
| newIntVector = createSingletonIntVector(i); |
| Vec_PtrPush(monotoneVector, newIntVector); |
| } |
| } |
| |
| if( Vec_PtrSize(monotoneVector) > 0 ) |
| return monotoneVector; |
| else |
| return NULL; |
| |
| } |
| |
| void deallocateMasterBarrierDisjunctInt(Vec_Ptr_t *vMasterBarrierDisjunctsArg) |
| { |
| Vec_Int_t *vInt; |
| int i; |
| |
| if(vMasterBarrierDisjunctsArg) |
| { |
| Vec_PtrForEachEntry(Vec_Int_t *, vMasterBarrierDisjunctsArg, vInt, i) |
| { |
| Vec_IntFree(vInt); |
| } |
| Vec_PtrFree(vMasterBarrierDisjunctsArg); |
| } |
| } |
| |
| void deallocateMasterBarrierDisjunctVecPtrVecInt(Vec_Ptr_t *vMasterBarrierDisjunctsArg) |
| { |
| Vec_Int_t *vInt; |
| Vec_Ptr_t *vPtr; |
| int i, j, k, iElem; |
| |
| if(vMasterBarrierDisjunctsArg) |
| { |
| Vec_PtrForEachEntry(Vec_Ptr_t *, vMasterBarrierDisjunctsArg, vPtr, i) |
| { |
| assert(vPtr); |
| Vec_PtrForEachEntry( Vec_Int_t *, vPtr, vInt, j ) |
| { |
| //Vec_IntFree(vInt); |
| Vec_IntForEachEntry( vInt, iElem, k ) |
| printf("%d - ", iElem); |
| //printf("Chung Chang j = %d\n", j); |
| } |
| Vec_PtrFree(vPtr); |
| } |
| Vec_PtrFree(vMasterBarrierDisjunctsArg); |
| } |
| } |
| |
| Vec_Ptr_t *getVecOfVecFairness(FILE *fp) |
| { |
| Vec_Ptr_t *masterVector = Vec_PtrAlloc(0); |
| //Vec_Ptr_t *currSignalVector; |
| char stringBuffer[100]; |
| //int i; |
| |
| while(fgets(stringBuffer, 50, fp)) |
| { |
| if(strstr(stringBuffer, ":")) |
| { |
| |
| } |
| else |
| { |
| |
| } |
| } |
| |
| return masterVector; |
| } |
| |
| |
| int Abc_CommandCS_kLiveness( Abc_Frame_t * pAbc, int argc, char ** argv ) |
| { |
| Abc_Ntk_t * pNtk, * pNtkTemp; |
| Aig_Man_t * pAig, *pAigCS, *pAigCSNew; |
| int absorberCount; |
| int absorberLimit = 500; |
| int RetValue; |
| int liveIndex_0 = -1, liveIndex_k = -1; |
| int fVerbose = 1; |
| int directive = -1; |
| int c; |
| int safetyInvariantPO = -1; |
| abctime beginTime, endTime; |
| double time_spent; |
| Vec_Ptr_t *vMasterBarrierDisjuncts = NULL; |
| Aig_Man_t *pWorkingAig; |
| //FILE *fp; |
| |
| pNtk = Abc_FrameReadNtk(pAbc); |
| |
| //fp = fopen("propFile.txt", "r"); |
| //if( fp ) |
| // getVecOfVecFairness(fp); |
| //exit(0); |
| |
| /************************************************* |
| Extraction of Command Line Argument |
| *************************************************/ |
| if( argc == 1 ) |
| { |
| assert( directive == -1 ); |
| directive = SIMPLE_kCS; |
| } |
| else |
| { |
| Extra_UtilGetoptReset(); |
| while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF ) |
| { |
| switch( c ) |
| { |
| case 'c': |
| directive = kCS_WITH_SAFETY_INVARIANTS; |
| break; |
| case 'm': |
| directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; |
| break; |
| case 'C': |
| directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS; |
| break; |
| case 'g': |
| directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS; |
| break; |
| case 'h': |
| goto usage; |
| break; |
| default: |
| goto usage; |
| } |
| } |
| } |
| /************************************************* |
| Extraction of Command Line Argument Ends |
| *************************************************/ |
| |
| if( !Abc_NtkIsStrash( pNtk ) ) |
| { |
| printf("The input network was not strashed, strashing....\n"); |
| pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); |
| pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); |
| } |
| else |
| { |
| pAig = Abc_NtkToDar( pNtk, 0, 1 ); |
| pNtkTemp = pNtk; |
| } |
| |
| if( directive == kCS_WITH_SAFETY_INVARIANTS ) |
| { |
| safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp); |
| assert( safetyInvariantPO != -1 ); |
| } |
| |
| if(directive == kCS_WITH_DISCOVER_MONOTONE_SIGNALS) |
| { |
| beginTime = Abc_Clock(); |
| vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk ); |
| endTime = Abc_Clock(); |
| time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC; |
| printf("pre-processing time = %f\n",time_spent); |
| return 0; |
| } |
| |
| if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS) |
| { |
| safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp); |
| assert( safetyInvariantPO != -1 ); |
| |
| beginTime = Abc_Clock(); |
| vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk ); |
| endTime = Abc_Clock(); |
| time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC; |
| printf("pre-processing time = %f\n",time_spent); |
| |
| assert( vMasterBarrierDisjuncts != NULL ); |
| assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 ); |
| } |
| |
| if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS) |
| { |
| safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp); |
| assert( safetyInvariantPO != -1 ); |
| |
| beginTime = Abc_Clock(); |
| vMasterBarrierDisjuncts = collectUserGivenDisjunctiveMonotoneSignals( pNtk ); |
| endTime = Abc_Clock(); |
| time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC; |
| printf("pre-processing time = %f\n",time_spent); |
| |
| assert( vMasterBarrierDisjuncts != NULL ); |
| assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 ); |
| } |
| |
| if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS) |
| { |
| assert( vMasterBarrierDisjuncts != NULL ); |
| pWorkingAig = generateWorkingAigWithDSC( pAig, pNtk, &liveIndex_0, vMasterBarrierDisjuncts ); |
| pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0); |
| } |
| else |
| { |
| pWorkingAig = generateWorkingAig( pAig, pNtk, &liveIndex_0 ); |
| pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0); |
| } |
| |
| Aig_ManStop(pWorkingAig); |
| |
| for( absorberCount=1; absorberCount<absorberLimit; absorberCount++ ) |
| { |
| //printf( "\nindex of the liveness output = %d\n", liveIndex_k ); |
| RetValue = flipConePdr( pAigCS, directive, liveIndex_k, safetyInvariantPO, absorberCount ); |
| |
| if ( RetValue == 1 ) |
| { |
| Abc_Print( 1, "k = %d, Property proved\n", absorberCount ); |
| break; |
| } |
| else if ( RetValue == 0 ) |
| { |
| if( fVerbose ) |
| { |
| Abc_Print( 1, "k = %d, Property DISPROVED\n", absorberCount ); |
| } |
| } |
| else if ( RetValue == -1 ) |
| { |
| Abc_Print( 1, "Property UNDECIDED with k = %d.\n", absorberCount ); |
| } |
| else |
| assert( 0 ); |
| |
| pAigCSNew = introduceAbsorberLogic(pAigCS, &liveIndex_0, &liveIndex_k, absorberCount); |
| Aig_ManStop(pAigCS); |
| pAigCS = pAigCSNew; |
| } |
| |
| Aig_ManStop(pAigCS); |
| Aig_ManStop(pAig); |
| |
| if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS) |
| { |
| deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts); |
| } |
| else |
| { |
| //if(vMasterBarrierDisjuncts) |
| // Vec_PtrFree(vMasterBarrierDisjuncts); |
| //deallocateMasterBarrierDisjunctVecPtrVecInt(vMasterBarrierDisjuncts); |
| deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts); |
| } |
| return 0; |
| |
| usage: |
| fprintf( stdout, "usage: kcs [-cmgCh]\n" ); |
| fprintf( stdout, "\timplements Claessen-Sorensson's k-Liveness algorithm\n" ); |
| fprintf( stdout, "\t-c : verification with constraints, looks for POs prefixed with csSafetyInvar_\n"); |
| fprintf( stdout, "\t-m : discovers monotone signals\n"); |
| fprintf( stdout, "\t-g : verification with user-supplied barriers, looks for POs prefixed with csLevel1Stabil_\n"); |
| fprintf( stdout, "\t-C : verification with discovered monotone signals\n"); |
| fprintf( stdout, "\t-h : print usage\n"); |
| return 1; |
| |
| } |
| |
| int Abc_CommandNChooseK( Abc_Frame_t * pAbc, int argc, char ** argv ) |
| { |
| Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkCombStabil; |
| Aig_Man_t * pAig, *pAigCombStabil; |
| int directive = -1; |
| int c; |
| int parameterizedCombK; |
| |
| pNtk = Abc_FrameReadNtk(pAbc); |
| |
| |
| /************************************************* |
| Extraction of Command Line Argument |
| *************************************************/ |
| if( argc == 1 ) |
| { |
| assert( directive == -1 ); |
| directive = SIMPLE_kCS; |
| } |
| else |
| { |
| Extra_UtilGetoptReset(); |
| while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF ) |
| { |
| switch( c ) |
| { |
| case 'c': |
| directive = kCS_WITH_SAFETY_INVARIANTS; |
| break; |
| case 'm': |
| directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; |
| break; |
| case 'C': |
| directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS; |
| break; |
| case 'g': |
| directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS; |
| break; |
| case 'h': |
| goto usage; |
| break; |
| default: |
| goto usage; |
| } |
| } |
| } |
| /************************************************* |
| Extraction of Command Line Argument Ends |
| *************************************************/ |
| |
| if( !Abc_NtkIsStrash( pNtk ) ) |
| { |
| printf("The input network was not strashed, strashing....\n"); |
| pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); |
| pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); |
| } |
| else |
| { |
| pAig = Abc_NtkToDar( pNtk, 0, 1 ); |
| pNtkTemp = pNtk; |
| } |
| |
| /**********************Code for generation of nCk outputs**/ |
| //combCount = countCombination(1000, 3); |
| //pAigCombStabil = generateDisjunctiveTester( pNtk, pAig, 7, 2 ); |
| printf("Enter parameterizedCombK = " ); |
| if( scanf("%d", ¶meterizedCombK) != 1 ) |
| { |
| printf("\nFailed to read integer!\n"); |
| return 0; |
| } |
| printf("\n"); |
| |
| pAigCombStabil = generateGeneralDisjunctiveTester( pNtk, pAig, parameterizedCombK ); |
| Aig_ManPrintStats(pAigCombStabil); |
| pNtkCombStabil = Abc_NtkFromAigPhase( pAigCombStabil ); |
| pNtkCombStabil->pName = Abc_UtilStrsav( pAigCombStabil->pName ); |
| if ( !Abc_NtkCheck( pNtkCombStabil ) ) |
| fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); |
| Abc_FrameSetCurrentNetwork( pAbc, pNtkCombStabil ); |
| |
| Aig_ManStop( pAigCombStabil ); |
| Aig_ManStop( pAig ); |
| |
| return 1; |
| //printf("\ncombCount = %d\n", combCount); |
| //exit(0); |
| /**********************************************************/ |
| |
| usage: |
| fprintf( stdout, "usage: nck [-cmgCh]\n" ); |
| fprintf( stdout, "\tgenerates combinatorial signals for stabilization\n" ); |
| fprintf( stdout, "\t-h : print usage\n"); |
| return 1; |
| |
| } |
| |
| |
| ABC_NAMESPACE_IMPL_END |
