/**CFile**************************************************************** FileName [liveness.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Liveness property checking.] Synopsis [Main implementation module.] Author [Sayak Ray] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - January 1, 2009.] Revision [$Id: liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $] ***********************************************************************/ #include #include "base/main/main.h" #include "aig/aig/aig.h" #include "aig/saig/saig.h" #include #include "base/main/mainInt.h" ABC_NAMESPACE_IMPL_START #define PROPAGATE_NAMES #define MULTIPLE_LTL_FORMULA #define ALLOW_SAFETY_PROPERTIES #define FULL_BIERE_MODE 0 #define IGNORE_LIVENESS_KEEP_SAFETY_MODE 1 #define IGNORE_SAFETY_KEEP_LIVENESS_MODE 2 #define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE 3 #define FULL_BIERE_ONE_LOOP_MODE 4 //#define DUPLICATE_CKT_DEBUG extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); //char *strdup(const char *string); //****************************************** //external functions defined in ltl_parser.c //****************************************** typedef struct ltlNode_t ltlNode; extern ltlNode *readLtlFormula( char *formula ); extern void traverseAbstractSyntaxTree( ltlNode *node ); extern ltlNode *parseFormulaCreateAST( char *inputFormula ); extern int isWellFormed( ltlNode *topNode ); extern int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode ); extern void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode ); extern int checkAllBoolHaveAIGPointer( ltlNode *topASTNode ); extern void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap ); extern void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo ); extern Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode ); extern Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode ); extern void traverseAbstractSyntaxTree_postFix( ltlNode *node ); //********************************** //external function declaration ends //********************************** /******************************************************************* LAYOUT OF PI VECTOR: +------------------------------------------------------------------------------------------------------------------------------------+ | TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) | +------------------------------------------------------------------------------------------------------------------------------------+ <------------True PI----------------->|<----------------------------LO---------------------------------------------------------------> LAYOUT OF PO VECTOR: +-----------------------------------------------------------------------------------------------------------+ | SOLE PO (1) | ORIGINAL LI (k) | SAVED LI (1) | SHADOW_ORIGINAL LI (k) | LIVENESS LI (l) | FAIRNESS LI (f) | +-----------------------------------------------------------------------------------------------------------+ <--True PO--->|<--------------------------------------LI----------------------------------------------------> ********************************************************************/ static int nodeName_starts_with( Abc_Obj_t *pNode, const char *prefix ) { if( strstr( Abc_ObjName( pNode ), prefix ) == Abc_ObjName( pNode ) ) return 1; else return 0; } void printVecPtrOfString( Vec_Ptr_t *vec ) { int i; for( i=0; i< Vec_PtrSize( vec ); i++ ) { printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) ); } } int getPoIndex( Aig_Man_t *pAig, Aig_Obj_t *pPivot ) { int i; Aig_Obj_t *pObj; Saig_ManForEachPo( pAig, pObj, i ) { if( pObj == pPivot ) return i; } return -1; } char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot ) { Aig_Obj_t *pObjOld, *pObj; Abc_Obj_t *pNode; int index; assert( Saig_ObjIsPi( pAigNew, pObjPivot ) ); Aig_ManForEachCi( pAigNew, pObj, index ) if( pObj == pObjPivot ) break; assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); if( index == Saig_ManPiNum( pAigNew ) - 1 ) return "SAVE_BIERE"; else { pObjOld = Aig_ManCi( pAigOld, index ); pNode = Abc_NtkPi( pNtkOld, index ); assert( pObjOld->pData == pObjPivot ); return Abc_ObjName( pNode ); } } char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot, Vec_Ptr_t *vLive, Vec_Ptr_t * vFair ) { Aig_Obj_t *pObjOld, *pObj; Abc_Obj_t *pNode; int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i; char *dummyStr = (char *)malloc( sizeof(char) * 50 ); assert( Saig_ObjIsLo( pAigNew, pObjPivot ) ); Saig_ManForEachLo( pAigNew, pObj, index ) if( pObj == pObjPivot ) break; if( index < originalLatchNum ) { oldIndex = Saig_ManPiNum( pAigOld ) + index; pObjOld = Aig_ManCi( pAigOld, oldIndex ); pNode = Abc_NtkCi( pNtkOld, oldIndex ); assert( pObjOld->pData == pObjPivot ); return Abc_ObjName( pNode ); } else if( index == originalLatchNum ) return "SAVED_LO"; else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 ) { oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1; pObjOld = Aig_ManCi( pAigOld, oldIndex ); pNode = Abc_NtkCi( pNtkOld, oldIndex ); sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW"); return dummyStr; } else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) ) { oldIndex = index - 2 * originalLatchNum - 1; strMatch = 0; dummyStr[0] = '\0'; Saig_ManForEachPo( pAigOld, pObj, i ) { pNode = Abc_NtkPo( pNtkOld, i ); //if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL ) if( nodeName_starts_with( pNode, "assert_fair" ) ) { if( strMatch == oldIndex ) { sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS"); //return dummyStr; break; } else strMatch++; } } assert( dummyStr[0] != '\0' ); return dummyStr; } else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ) { oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive ); strMatch = 0; dummyStr[0] = '\0'; Saig_ManForEachPo( pAigOld, pObj, i ) { pNode = Abc_NtkPo( pNtkOld, i ); //if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL ) if( nodeName_starts_with( pNode, "assume_fair" ) ) { if( strMatch == oldIndex ) { sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS"); //return dummyStr; break; } else strMatch++; } } assert( dummyStr[0] != '\0' ); return dummyStr; } else return "UNKNOWN"; } Vec_Ptr_t *vecPis, *vecPiNames; Vec_Ptr_t *vecLos, *vecLoNames; int Aig_ManCiCleanupBiere( Aig_Man_t * p ) { int nPisOld = Aig_ManCiNum(p); p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis ); if ( Aig_ManRegNum(p) ) p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p); return nPisOld - Aig_ManCiNum(p); } int Aig_ManCoCleanupBiere( Aig_Man_t * p ) { int nPosOld = Aig_ManCoNum(p); p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos ); if ( Aig_ManRegNum(p) ) p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p); return nPosOld - Aig_ManCoNum(p); } Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety ) { Aig_Man_t * pNew; int i, nRegCount; Aig_Obj_t * pObjSavePi = NULL; Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL; Aig_Obj_t *pObj, *pMatch; Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality; Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver; Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc; Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate; Aig_Obj_t *pObjSafetyPropertyOutput = NULL; Aig_Obj_t *pObjOriginalSafetyPropertyOutput; Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety; char *nodeName; int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0; vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); //**************************************************************** // 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 //**************************************************************** pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) ); pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 ); sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s"); pNew->pSpec = NULL; //**************************************************************** // Step 2: map constant nodes //**************************************************************** pObj = Aig_ManConst1( p ); pObj->pData = Aig_ManConst1( pNew ); //**************************************************************** // Step 3: create true PIs //**************************************************************** Saig_ManForEachPi( p, pObj, i ) { piCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 4: create the special Pi corresponding to SAVE //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 5: create register outputs //**************************************************************** Saig_ManForEachLo( p, pObj, i ) { loCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 6: create "saved" register output //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { loCreated++; pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo ); pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) ); } //******************************************************************** // Step 8: create internal nodes //******************************************************************** Aig_ManForEachNode( p, pObj, i ) { pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } //******************************************************************** // Step 8.x : create PO for each safety assertions // NOTE : Here the output is purposely inverted as it will be thrown to // dprove //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) { if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 ) { pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssertSafety = pObjAndAcc; pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssumeSafety = pObjAndAcc; pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else { printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n"); pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); } } //******************************************************************** // Step 9: create the safety property output gate for the liveness properties // discuss with Sat/Alan for an alternative implementation //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); } // create register inputs for the original registers nRegCount = 0; Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } // create register input corresponding to the register "saved" if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { #ifndef DUPLICATE_CKT_DEBUG pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; //Changed on October 13, 2009 //pObjAndAcc = NULL; pObjAndAcc = Aig_ManConst1( pNew ); // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator Saig_ManForEachLo( p, pObj, i ) { pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); pObjXnor = Aig_Not( pObjXor ); pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc ); } // create the AND gate whose output will be the signal "looped" pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc ); // create the master AND gate and corresponding AND and OR logic for the liveness properties pObjAndAcc = Aig_ManConst1( pNew ); if( vLive == NULL || Vec_PtrSize( vLive ) == 0 ) { printf("Circuit without any liveness property\n"); } else { Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i ) { liveLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc ); } } pObjLive = pObjAndAcc; pObjAndAcc = Aig_ManConst1( pNew ); if( vFair == NULL || Vec_PtrSize( vFair ) == 0 ) printf("Circuit without any fairness property\n"); else { Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i ) { fairLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc ); } } pObjFair = pObjAndAcc; //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) ); //Following is the actual Biere translation pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate ); #endif } Aig_ManSetRegNum( pNew, nRegCount ); Aig_ManCiCleanupBiere( pNew ); Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); assert( Aig_ManCheck( pNew ) ); if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); } return pNew; } Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Int_t *vFlops, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety ) { Aig_Man_t * pNew; int i, nRegCount, iEntry; Aig_Obj_t * pObjSavePi = NULL; Aig_Obj_t *pObjSavedLi = NULL, *pObjSavedLo = NULL; Aig_Obj_t *pObj, *pMatch; Aig_Obj_t *pObjSavedLoAndEquality, *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL; Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver; Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc; Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate; Aig_Obj_t *pObjSafetyPropertyOutput = NULL; Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety; char *nodeName; int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;//, piVecIndex = 0; vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecLos = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); //**************************************************************** // 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 //**************************************************************** pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) ); pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 ); sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s"); pNew->pSpec = NULL; //**************************************************************** // Step 2: map constant nodes //**************************************************************** pObj = Aig_ManConst1( p ); pObj->pData = Aig_ManConst1( pNew ); //**************************************************************** // Step 3: create true PIs //**************************************************************** Saig_ManForEachPi( p, pObj, i ) { piCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 4: create the special Pi corresponding to SAVE //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 5: create register outputs //**************************************************************** Saig_ManForEachLo( p, pObj, i ) { loCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 6: create "saved" register output //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { loCreated++; pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo ); pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) ); } //******************************************************************** // Step 8: create internal nodes //******************************************************************** Aig_ManForEachNode( p, pObj, i ) { pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } //******************************************************************** // Step 8.x : create PO for each safety assertions // NOTE : Here the output is purposely inverted as it will be thrown to // dprove //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) { if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 ) { pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssertSafety = pObjAndAcc; pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssumeSafety = pObjAndAcc; Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else { printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n"); Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); } } //******************************************************************** // Step 9: create the safety property output gate for the liveness properties // discuss with Sat/Alan for an alternative implementation //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); } // create register inputs for the original registers nRegCount = 0; Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } // create register input corresponding to the register "saved" if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { #ifndef DUPLICATE_CKT_DEBUG pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; //Changed on October 13, 2009 //pObjAndAcc = NULL; pObjAndAcc = Aig_ManConst1( pNew ); // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator //Saig_ManForEachLo( p, pObj, i ) Saig_ManForEachLo( p, pObj, i ) { printf("Flop[%d] = %s\n", i, Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ); } Vec_IntForEachEntry( vFlops, iEntry, i ) { pObjShadowLo = Aig_ObjCreateCi( pNew ); pObj = Aig_ManLo( p, iEntry ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ) ) + 10 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ), "SHADOW" ); printf("Flop copied [%d] = %s\n", iEntry, nodeName ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); pObjXnor = Aig_Not( pObjXor ); pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc ); } // create the AND gate whose output will be the signal "looped" pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc ); // create the master AND gate and corresponding AND and OR logic for the liveness properties pObjAndAcc = Aig_ManConst1( pNew ); if( vLive == NULL || Vec_PtrSize( vLive ) == 0 ) { printf("Circuit without any liveness property\n"); } else { Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i ) { liveLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc ); } } pObjLive = pObjAndAcc; pObjAndAcc = Aig_ManConst1( pNew ); if( vFair == NULL || Vec_PtrSize( vFair ) == 0 ) printf("Circuit without any fairness property\n"); else { Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i ) { fairLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc ); } } pObjFair = pObjAndAcc; //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) ); //Following is the actual Biere translation pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate ); #endif } Aig_ManSetRegNum( pNew, nRegCount ); Aig_ManCiCleanupBiere( pNew ); Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); assert( Aig_ManCheck( pNew ) ); if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch ); } return pNew; } Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety ) { Aig_Man_t * pNew; int i, nRegCount; Aig_Obj_t * pObjSavePi = NULL; Aig_Obj_t *pObj, *pMatch; Aig_Obj_t *pObjSavedLoAndEquality; Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy; Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate; Aig_Obj_t *pObjSafetyPropertyOutput = NULL; Aig_Obj_t *pDriverImage; Aig_Obj_t *pObjCorrespondingLi; Aig_Obj_t *pArgument; Aig_Obj_t *collectiveAssertSafety, *collectiveAssumeSafety; char *nodeName; int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0; if( Aig_ManRegNum( p ) == 0 ) { printf("The input AIG contains no register, returning the original AIG as it is\n"); return p; } vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); //**************************************************************** // 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 //**************************************************************** pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) ); pNew->pName = Abc_UtilStrsav( "live2safe" ); pNew->pSpec = NULL; //**************************************************************** // Step 2: map constant nodes //**************************************************************** pObj = Aig_ManConst1( p ); pObj->pData = Aig_ManConst1( pNew ); //**************************************************************** // Step 3: create true PIs //**************************************************************** Saig_ManForEachPi( p, pObj, i ) { piCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 4: create the special Pi corresponding to SAVE //**************************************************************** if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE ) { pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 5: create register outputs //**************************************************************** Saig_ManForEachLo( p, pObj, i ) { loCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 6: create "saved" register output //**************************************************************** #if 0 loCreated++; pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); #endif //**************************************************************** // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi //**************************************************************** #if 0 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo ); pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) ); #endif //******************************************************************** // Step 8: create internal nodes //******************************************************************** Aig_ManForEachNode( p, pObj, i ) { pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } #if 0 //******************************************************************** // Step 8.x : create PO for each safety assertions //******************************************************************** Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); } #endif if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) { if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 ) { pObjAndAcc = NULL; Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); if( pObjAndAcc == NULL ) pObjAndAcc = pArgument; else { pObjAndAccDummy = pObjAndAcc; pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy ); } } Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { pObjAndAcc = NULL; Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); if( pObjAndAcc == NULL ) pObjAndAcc = pArgument; else { pObjAndAccDummy = pObjAndAcc; pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy ); } } collectiveAssertSafety = pObjAndAcc; pObjAndAcc = NULL; Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i ) { //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); if( pObjAndAcc == NULL ) pObjAndAcc = pArgument; else { pObjAndAccDummy = pObjAndAcc; pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy ); } } collectiveAssumeSafety = pObjAndAcc; Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else printf("No safety property is specified, hence no safety gate is created\n"); } //******************************************************************** // Step 9: create the safety property output gate // create the safety property output gate, this will be the sole true PO // of the whole circuit, discuss with Sat/Alan for an alternative implementation //******************************************************************** if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE ) { pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); } // create register inputs for the original registers nRegCount = 0; Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) ); Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } #if 0 // create register input corresponding to the register "saved" pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++;7 #endif pObjAndAcc = NULL; //**************************************************************************************************** //For detection of loop of length 1 we do not need any shadow register, we only need equality detector //between Lo_j and Li_j and then a cascade of AND gates //**************************************************************************************************** if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE ) { Saig_ManForEachLo( p, pObj, i ) { pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj ); pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) ); pObjXnor = Aig_Not( pObjXor ); if( pObjAndAcc == NULL ) pObjAndAcc = pObjXnor; else { pObjAndAccDummy = pObjAndAcc; pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy ); } } // create the AND gate whose output will be the signal "looped" pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc ); // create the master AND gate and corresponding AND and OR logic for the liveness properties pObjAndAcc = NULL; if( vLive == NULL || Vec_PtrSize( vLive ) == 0 ) printf("Circuit without any liveness property\n"); else { Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i ) { pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); if( pObjAndAcc == NULL ) pObjAndAcc = pDriverImage; else { pObjAndAccDummy = pObjAndAcc; pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy ); } } } if( pObjAndAcc != NULL ) pObjLive = pObjAndAcc; else pObjLive = Aig_ManConst1( pNew ); // create the master AND gate and corresponding AND and OR logic for the fairness properties pObjAndAcc = NULL; if( vFair == NULL || Vec_PtrSize( vFair ) == 0 ) printf("Circuit without any fairness property\n"); else { Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i ) { pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); if( pObjAndAcc == NULL ) pObjAndAcc = pDriverImage; else { pObjAndAccDummy = pObjAndAcc; pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy ); } } } if( pObjAndAcc != NULL ) pObjFair = pObjAndAcc; else pObjFair = Aig_ManConst1( pNew ); pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate ); } Aig_ManSetRegNum( pNew, nRegCount ); //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs ); Aig_ManCiCleanupBiere( pNew ); Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); assert( Aig_ManCheck( pNew ) ); return pNew; } Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) { Abc_Obj_t * pNode; int i, liveCounter = 0; Vec_Ptr_t * vLive; vLive = Vec_PtrAlloc( 100 ); Abc_NtkForEachPo( pNtk, pNode, i ) //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL ) if( nodeName_starts_with( pNode, "assert_fair" ) ) { Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) ); liveCounter++; } printf("Number of liveness property found = %d\n", liveCounter); return vLive; } Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) { Abc_Obj_t * pNode; int i, fairCounter = 0; Vec_Ptr_t * vFair; vFair = Vec_PtrAlloc( 100 ); Abc_NtkForEachPo( pNtk, pNode, i ) //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL ) if( nodeName_starts_with( pNode, "assume_fair" ) ) { Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) ); fairCounter++; } printf("Number of fairness property found = %d\n", fairCounter); return vFair; } Vec_Ptr_t * populateSafetyAssertionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) { Abc_Obj_t * pNode; int i, assertSafetyCounter = 0; Vec_Ptr_t * vAssertSafety; vAssertSafety = Vec_PtrAlloc( 100 ); Abc_NtkForEachPo( pNtk, pNode, i ) //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL ) if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" )) { Vec_PtrPush( vAssertSafety, Aig_ManCo( pAig, i ) ); assertSafetyCounter++; } printf("Number of safety property found = %d\n", assertSafetyCounter); return vAssertSafety; } Vec_Ptr_t * populateSafetyAssumptionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) { Abc_Obj_t * pNode; int i, assumeSafetyCounter = 0; Vec_Ptr_t * vAssumeSafety; vAssumeSafety = Vec_PtrAlloc( 100 ); Abc_NtkForEachPo( pNtk, pNode, i ) //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL ) if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" )) { Vec_PtrPush( vAssumeSafety, Aig_ManCo( pAig, i ) ); assumeSafetyCounter++; } printf("Number of assume_safety property found = %d\n", assumeSafetyCounter); return vAssumeSafety; } void updateNewNetworkNameManager( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames ) { 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; //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId); 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; //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId); Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL ); } } Abc_NtkForEachPo(pNtk, pNode, i) { Abc_ObjAssignName(pNode, "assert_safety_", Abc_ObjName(pNode) ); } // 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 ); } int Abc_CommandAbcLivenessToSafety( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld; Aig_Man_t * pAig, *pAigNew = NULL; int c; Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety; int directive = -1; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); if( argc == 1 ) { assert( directive == -1 ); directive = FULL_BIERE_MODE; } else { Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF ) { switch( c ) { case '1': if( directive == -1 ) directive = FULL_BIERE_ONE_LOOP_MODE; else { assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE ); if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE; else directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE; } break; case 's': if( directive == -1 ) directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE; else { if( directive != FULL_BIERE_ONE_LOOP_MODE ) goto usage; assert(directive == FULL_BIERE_ONE_LOOP_MODE); directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE; } break; case 'l': if( directive == -1 ) directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE; else { if( directive != FULL_BIERE_ONE_LOOP_MODE ) goto usage; assert(directive == FULL_BIERE_ONE_LOOP_MODE); directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE; } break; case 'h': goto usage; default: goto usage; } } } if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } switch( directive ) { case FULL_BIERE_MODE: //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 ) //{ // printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n"); // return 1; //} //else //{ pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n"); break; //} case FULL_BIERE_ONE_LOOP_MODE: //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 ) //{ // printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n"); // return 1; //} //else //{ pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n"); break; //} case IGNORE_LIVENESS_KEEP_SAFETY_MODE: //if( Vec_PtrSize(vAssertSafety) == 0 ) //{ // printf("Input circuit has NO safety property, original network is not disturbed\n"); // return 1; //} //else //{ pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n"); break; //} case IGNORE_SAFETY_KEEP_LIVENESS_MODE: //if( Vec_PtrSize(vLive) == 0 ) //{ // printf("Input circuit has NO liveness property, original network is not disturbed\n"); // return 1; //} //else //{ pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n"); break; //} case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE: //if( Vec_PtrSize(vLive) == 0 ) //{ // printf("Input circuit has NO liveness property, original network is not disturbed\n"); // return 1; //} //else //{ pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n"); break; //} } #if 0 if( argc == 1 ) { pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n"); } else { Extra_UtilGetoptReset(); c = Extra_UtilGetopt( argc, argv, "1lsh" ); if( c == '1' ) { if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); } else if( c == 'l' ) { if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n"); } else if( c == 's' ) { if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n"); } else if( c == 'h' ) goto usage; else goto usage; } #endif #if 0 Aig_ManPrintStats( pAigNew ); printf("\nDetail statistics*************************************\n"); printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew )); printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew )); printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew )); printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew )); printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) ); printf("\n*******************************************************\n"); #endif pNtkNew = Abc_NtkFromAigPhase( pAigNew ); pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames ); Abc_FrameSetCurrentNetwork( pAbc, pNtkNew ); #if 0 #ifndef DUPLICATE_CKT_DEBUG Saig_ManForEachPi( pAigNew, pObj, i ) assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 ); //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) ); Saig_ManForEachLo( pAigNew, pObj, i ) assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 ); #endif #endif return 0; usage: fprintf( stdout, "usage: l2s [-1lsh]\n" ); fprintf( stdout, "\t performs Armin Biere's live-to-safe transformation\n" ); fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n"); fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n"); fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n"); fprintf( stdout, "\t-h : print command usage\n"); return 1; } Vec_Int_t * prepareFlopVector( Aig_Man_t * pAig, int vectorLength ) { Vec_Int_t *vFlops; int i; vFlops = Vec_IntAlloc( vectorLength ); for( i=0; ipName = Abc_UtilStrsav( pAigNew->pName ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames ); Abc_FrameSetCurrentNetwork( pAbc, pNtkNew ); #if 0 #ifndef DUPLICATE_CKT_DEBUG Saig_ManForEachPi( pAigNew, pObj, i ) assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 ); //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) ); Saig_ManForEachLo( pAigNew, pObj, i ) assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 ); #endif #endif return 0; usage: fprintf( stdout, "usage: l2s [-1lsh]\n" ); fprintf( stdout, "\t performs Armin Biere's live-to-safe transformation\n" ); fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n"); fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n"); fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n"); fprintf( stdout, "\t-h : print command usage\n"); return 1; } Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety, int *numLtlProcessed, Vec_Ptr_t *ltlBuffer ) { Aig_Man_t * pNew; int i, ii, iii, nRegCount; Aig_Obj_t * pObjSavePi = NULL; Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL; Aig_Obj_t *pObj, *pMatch; Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality; Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver; Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc; Aig_Obj_t *pObjLive, *pObjSafetyGate; Aig_Obj_t *pObjSafetyPropertyOutput; Aig_Obj_t *pObjOriginalSafetyPropertyOutput; Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety; Aig_Obj_t *pNegatedSafetyConjunction = NULL; Aig_Obj_t *pObjSafetyAndLiveToSafety; char *nodeName, *pFormula; int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0;//, piVecIndex = 0, fairLatch = 0; Vec_Ptr_t *vSignal, *vTopASTNodeArray = NULL; ltlNode *pEnrtyGLOBALLY; ltlNode *topNodeOfAST, *tempTopASTNode; Vec_Vec_t *vAigGFMap; Vec_Ptr_t *vSignalMemory, *vGFFlopMemory, *vPoForLtlProps = NULL; Vec_Ptr_t *vecInputLtlFormulae; vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1); vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) ); //**************************************************************** //step0: Parsing the LTL formula //**************************************************************** //Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pFormula, i ) // printf("\ninput LTL formula [%d] = %s\n", i, pFormula ); #ifdef MULTIPLE_LTL_FORMULA //*************************************************************************** //Reading input LTL formulae from Ntk data-structure and creating //AST for them, Steps involved: // parsing -> AST creation -> well-formedness check -> signal name check //*************************************************************************** //resetting numLtlProcessed *numLtlProcessed = 0; if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { //if( ltlBuffer ) vecInputLtlFormulae = ltlBuffer; //vecInputLtlFormulae = pNtk->vLtlProperties; if( vecInputLtlFormulae ) { vTopASTNodeArray = Vec_PtrAlloc( Vec_PtrSize( vecInputLtlFormulae ) ); printf("\n"); Vec_PtrForEachEntry( char *, vecInputLtlFormulae, pFormula, i ) { tempTopASTNode = parseFormulaCreateAST( pFormula ); //traverseAbstractSyntaxTree_postFix( tempTopASTNode ); if( tempTopASTNode ) { printf("Formula %d: AST is created, ", i+1); if( isWellFormed( tempTopASTNode ) ) printf("Well-formedness check PASSED, "); else { printf("Well-formedness check FAILED!!\n"); printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 ); //do memory management to free the created AST continue; } if( checkSignalNameExistence( pNtk, tempTopASTNode ) ) printf("Signal check PASSED\n"); else { printf("Signal check FAILED!!"); printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 ); //do memory management to free the created AST continue; } Vec_PtrPush( vTopASTNodeArray, tempTopASTNode ); (*numLtlProcessed)++; } else printf("\nNo AST has been created for formula %d, no extra logic will be added\n", i+1 ); } } printf("\n"); if( Vec_PtrSize( vTopASTNodeArray ) == 0 ) { //printf("\nNo AST has been created for any formula; hence the circuit is left untouched\n"); printf("\nCurrently aborting, need to take care when Vec_PtrSize( vTopASTNodeArray ) == 0\n"); exit(0); } } //**************************************************************** // 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 //**************************************************************** pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) ); pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l3s") + 1 ); sprintf(pNew->pName, "%s_%s", pNtk->pName, "l3s"); pNew->pSpec = NULL; //**************************************************************** // Step 2: map constant nodes //**************************************************************** pObj = Aig_ManConst1( p ); pObj->pData = Aig_ManConst1( pNew ); //**************************************************************** // Step 3: create true PIs //**************************************************************** Saig_ManForEachPi( p, pObj, i ) { piCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 4: create the special Pi corresponding to SAVE //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } //**************************************************************** // Step 5: create register outputs //**************************************************************** Saig_ManForEachLo( p, pObj, i ) { loCopied++; pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 6: create "saved" register output //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { loCreated++; pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); } //**************************************************************** // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo ); pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) ); } //******************************************************************** // Step 8: create internal nodes //******************************************************************** Aig_ManForEachNode( p, pObj, i ) { pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } //******************************************************************** // Step 8.x : create PO for each safety assertions // NOTE : Here the output is purposely inverted as it will be thrown to // dprove //******************************************************************** assert( pNegatedSafetyConjunction == NULL ); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE) { if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 ) { pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } pNegatedSafetyConjunction = Aig_Not(pObjAndAcc); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssertSafety = pObjAndAcc; pObjAndAcc = Aig_ManConst1( pNew ); Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i ) { pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssumeSafety = pObjAndAcc; pNegatedSafetyConjunction = Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else { printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n"); pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) ); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); } } assert( pNegatedSafetyConjunction != NULL ); //******************************************************************** // Step 9: create the safety property output gate for the liveness properties // discuss with Sat/Alan for an alternative implementation //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { vPoForLtlProps = Vec_PtrAlloc( Vec_PtrSize( vTopASTNodeArray ) ); if( Vec_PtrSize( vTopASTNodeArray ) ) { //no effective AST for any input LTL property //must do something graceful } for( i=0; ipData ); Vec_PtrPush( vPoForLtlProps, pObjSafetyPropertyOutput ); } } //************************************************************************************* // Step 10: Placeholder PO's were created for Liveness property outputs in the // last step. FYI, # of new liveness property outputs = # of LTL properties in the circuit // It is time for creation of loop LI's and other stuff // Now creating register inputs for the original flops //************************************************************************************* nRegCount = 0; Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } //************************************************************************************* // Step 11: create register input corresponding to the register "saved" //************************************************************************************* if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { #ifndef DUPLICATE_CKT_DEBUG pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; pObjAndAcc = Aig_ManConst1( pNew ); //************************************************************************************* // Step 11: create the family of shadow registers, then create the cascade of Xnor // and And gates for the comparator //************************************************************************************* Saig_ManForEachLo( p, pObj, i ) { //printf("\nKEMON RENDY = %s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i )) ); //top|route0_target0_queue_with_credit0_queue0 //top|route0_master0_queue2 // if( strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0 // || strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 ) { pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 ); sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" ); Vec_PtrPush( vecLoNames, nodeName ); #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); pObjXnor = Aig_Not( pObjXor ); pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc ); } } // create the AND gate whose output will be the signal "looped" pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc ); // create the master AND gate and corresponding AND and OR logic for the liveness properties //************************************************************************************* // Step 11: logic for LTL properties:- (looped & ~theta) where theta is the input ltl // property // Description of some data-structure: //------------------------------------------------------------------------------------- // Name | Type | Purpose //------------------------------------------------------------------------------------- // vSignalMemory | Vec_Ptr_t * | A vector across all ASTs of the LTL properties // | | It remembers if OR+Latch for GF node has already been // | | created for a particular signal. // | | // vGFFlopMemory | Vec_Ptr_t * | A vector across all ASTs of the LTL properties // | | remembers if OR+Latch of a GF node has already been created // | | // vSignal | Vec_Ptr_t * | vector for each AST; contains pointers from GF nodes // | | to AIG signals // | | // vAigGFMap | Vec_Vec_t * | vAigGFMap[ index ] = vector of GF nodes pointing to // | | the same AIG node; "index" is the index of that // | | AIG node in the vector vSignal //************************************************************************************* vSignalMemory = Vec_PtrAlloc(10); vGFFlopMemory = Vec_PtrAlloc(10); Vec_PtrForEachEntry( ltlNode *, vTopASTNodeArray, topNodeOfAST, iii ) { vSignal = Vec_PtrAlloc( 10 ); vAigGFMap = Vec_VecAlloc( 10 ); //************************************************************************************* //Step 11a: for the current AST, find out the leaf level Boolean signal pointers from // the NEW aig. //************************************************************************************* populateBoolWithAigNodePtr( pNtk, p, pNew, topNodeOfAST ); assert( checkAllBoolHaveAIGPointer( topNodeOfAST ) ); //************************************************************************************* //Step 11b: for each GF node, compute the pointer in AIG that it should point to // In particular, if the subtree below GF is some Boolean crown (including the case // of simple negation, create new logic and populate the AIG pointer in GF node // accordingly //************************************************************************************* populateAigPointerUnitGF( pNew, topNodeOfAST, vSignal, vAigGFMap ); //************************************************************************************* //Step 11c: everything below GF are computed. Now, it is time to create logic for individual // GF nodes (i.e. the OR gate and the latch and the Boolean crown of the AST //************************************************************************************* Vec_PtrForEachEntry( Aig_Obj_t *, vSignal, pObj, i ) { //********************************************************* // Step 11c.1: if the OR+Latch of the particular signal is // not already created, create it. It may have already been // created from another property, so check it before creation //********************************************************* if( Vec_PtrFind( vSignalMemory, pObj ) == -1 ) { liveLatch++; pDriverImage = pObj; pObjShadowLo = Aig_ObjCreateCi( pNew ); pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; Vec_PtrPush( vSignalMemory, pObj ); Vec_PtrPush( vGFFlopMemory, pObjShadowLo ); #if 1 #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); //nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 ); //sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" ); nodeName = (char *)malloc( 20 ); sprintf( nodeName, "n%d__%s", Aig_ObjId(pObjShadowLo), "GF_flop" ); Vec_PtrPush( vecLoNames, nodeName ); #endif #endif } else pObjShadowLo = (Aig_Obj_t *)Vec_PtrEntry( vGFFlopMemory, Vec_PtrFind( vSignalMemory, pObj ) ); Vec_VecForEachEntryLevel( ltlNode *, vAigGFMap, pEnrtyGLOBALLY, ii, i ) setAIGNodePtrOfGloballyNode( pEnrtyGLOBALLY, pObjShadowLo); //#ifdef PROPAGATE_NAMES // Vec_PtrPush( vecLos, pObjShadowLo ); // nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 ); // sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" ); // Vec_PtrPush( vecLoNames, nodeName ); //#endif } //********************************************************* //Step 11c.2: creating the Boolean crown //********************************************************* buildLogicFromLTLNode( pNew, topNodeOfAST ); //********************************************************* //Step 11c.3: creating logic for (looped & ~theta) and patching // it with the proper PO //Note: if ALLOW_SAFETY_PROPERTIES is defined then the final AND //gate is a conjunction of safety & liveness, i.e. SAFETY & (looped => theta) //since ABC convention demands a NOT gate at the end, the property logic //becomes !( SAFETY & (looped => theta) ) = !SAFETY + (looped & !theta) //********************************************************* pObjLive = retriveAIGPointerFromLTLNode( topNodeOfAST ); pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_Not(pObjLive) ); #ifdef ALLOW_SAFETY_PROPERTIES printf("liveness output is conjoined with safety assertions\n"); pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction ); pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety ); #else pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii ); Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate ); #endif //refreshing vSignal and vAigGFMap arrays Vec_PtrFree( vSignal ); Vec_VecFree( vAigGFMap ); } #endif } #endif Aig_ManSetRegNum( pNew, nRegCount ); Aig_ManCiCleanupBiere( pNew ); Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); assert( Aig_ManCheck( pNew ) ); if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); } return pNew; } int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld; Aig_Man_t * pAig, *pAigNew = NULL; int c; Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety; int directive = -1; // char *ltfFormulaString = NULL; int numOfLtlPropOutput;//, LTL_FLAG = 0; Vec_Ptr_t *ltlBuffer; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); if( argc == 1 ) { assert( directive == -1 ); directive = FULL_BIERE_MODE; } else { Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "1slhf" ) ) != EOF ) { switch( c ) { case '1': if( directive == -1 ) directive = FULL_BIERE_ONE_LOOP_MODE; else { assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE ); if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE; else directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE; } break; case 's': if( directive == -1 ) directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE; else { if( directive != FULL_BIERE_ONE_LOOP_MODE ) goto usage; assert(directive == FULL_BIERE_ONE_LOOP_MODE); directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE; } break; case 'l': if( directive == -1 ) directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE; else { if( directive != FULL_BIERE_ONE_LOOP_MODE ) goto usage; assert(directive == FULL_BIERE_ONE_LOOP_MODE); directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE; } break; case 'f': //assert( argc >= 3 ); //vecLtlFormula = Vec_PtrAlloc( argc - 2 ); //if( argc >= 3 ) //{ // for( t=3; t<=argc; t++ ) // { // printf("argv[%d] = %s\n", t-1, argv[t-1]); // Vec_PtrPush( vecLtlFormula, argv[t-1] ); // } //} //printf("argv[argc] = %s\n", argv[argc-1]); //ltfFormulaString = argv[2]; //LTL_FLAG = 1; printf("\nILLEGAL FLAG: aborting....\n"); exit(0); break; case 'h': goto usage; default: goto usage; } } } if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } if( pAbc->vLTLProperties_global != NULL ) ltlBuffer = pAbc->vLTLProperties_global; else ltlBuffer = NULL; switch( directive ) { case FULL_BIERE_MODE: pAigNew = LivenessToSafetyTransformationWithLTL( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t%d POs - one for safety and %d for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput+1, numOfLtlPropOutput); break; case FULL_BIERE_ONE_LOOP_MODE: pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n"); break; case IGNORE_LIVENESS_KEEP_SAFETY_MODE: pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer ); assert( numOfLtlPropOutput == 0 ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n"); break; case IGNORE_SAFETY_KEEP_LIVENESS_MODE: pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("A new circuit is produced with\n\t%d PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput); break; case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE: pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n"); break; } #if 0 if( argc == 1 ) { pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n"); } else { Extra_UtilGetoptReset(); c = Extra_UtilGetopt( argc, argv, "1lsh" ); if( c == '1' ) { if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); } else if( c == 'l' ) { if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n"); } else if( c == 's' ) { if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } if( !Abc_NtkIsStrash( pNtk ) ) { printf("The input network was not strashed, strashing....\n"); pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 ); pNtkOld = pNtkTemp; pAig = Abc_NtkToDar( pNtkTemp, 0, 1 ); vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } else { pAig = Abc_NtkToDar( pNtk, 0, 1 ); pNtkOld = pNtk; vLive = populateLivenessVector( pNtk, pAig ); vFair = populateFairnessVector( pNtk, pAig ); vAssertSafety = populateSafetyAssertionVector( pNtk, pAig ); vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig ); } pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety ); if( Aig_ManRegNum(pAigNew) != 0 ) printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n"); } else if( c == 'h' ) goto usage; else goto usage; } #endif #if 0 Aig_ManPrintStats( pAigNew ); printf("\nDetail statistics*************************************\n"); printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew )); printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew )); printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew )); printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew )); printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) ); printf("\n*******************************************************\n"); #endif pNtkNew = Abc_NtkFromAigPhase( pAigNew ); pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames ); Abc_FrameSetCurrentNetwork( pAbc, pNtkNew ); #if 0 #ifndef DUPLICATE_CKT_DEBUG Saig_ManForEachPi( pAigNew, pObj, i ) assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 ); //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) ); Saig_ManForEachLo( pAigNew, pObj, i ) assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 ); #endif #endif return 0; usage: fprintf( stdout, "usage: l3s [-1lsh]\n" ); fprintf( stdout, "\t performs Armin Biere's live-to-safe transformation\n" ); fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n"); fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n"); fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n"); fprintf( stdout, "\t-h : print command usage\n"); return 1; } ABC_NAMESPACE_IMPL_END