diff options
Diffstat (limited to 'src/aig/live/liveness_old.c')
-rw-r--r-- | src/aig/live/liveness_old.c | 1756 |
1 files changed, 0 insertions, 1756 deletions
diff --git a/src/aig/live/liveness_old.c b/src/aig/live/liveness_old.c deleted file mode 100644 index b3ddb1fc..00000000 --- a/src/aig/live/liveness_old.c +++ /dev/null @@ -1,1756 +0,0 @@ -#include <stdio.h> -#include "main.h" -#include "aig.h" -#include "saig.h" -#include <string.h> - -ABC_NAMESPACE_IMPL_START - - -#define PROPAGATE_NAMES - -#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); - - -/******************************************************************* -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_ManForEachPi( pAigNew, pObj, index ) - if( pObj == pObjPivot ) - break; - assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); - if( index == Saig_ManPiNum( pAigNew ) - 1 ) - return "SAVE_BIERE"; - else - { - pObjOld = Aig_ManPi( 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_ManPi( 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_ManPi( 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_ManPiCleanupBiere( Aig_Man_t * p ) -{ - int k = 0, nPisOld = Aig_ManPiNum(p); - - p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); - if ( Aig_ManRegNum(p) ) - p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); - - return nPisOld - Aig_ManPiNum(p); -} - - -int Aig_ManPoCleanupBiere( Aig_Man_t * p ) -{ - int k = 0, nPosOld = Aig_ManPoNum(p); - - p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); - if ( Aig_ManRegNum(p) ) - p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); - return nPosOld - Aig_ManPoNum(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; - Aig_Obj_t *pObjSavedLo, *pObjSavedLi; - Aig_Obj_t *pObj, *pMatch; - Aig_Obj_t *pObjSaveOrSaved, *pObjSaveAndNotSaved, *pObjSavedLoAndEquality; - Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver; - Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc; - Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate; - Aig_Obj_t *pObjSafetyPropertyOutput; - Aig_Obj_t *pObjOriginalSafetyPropertyOutput; - Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety; - char *nodeName; - int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 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_ObjCreatePi(pNew); - Vec_PtrPush( vecPis, pObj->pData ); - nodeName = Aig_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_ObjCreatePi( pNew ); - nodeName = "SAVE_BIERE", - Vec_PtrPush( vecPiNames, nodeName ); - } - - //**************************************************************** - // Step 5: create register outputs - //**************************************************************** - Saig_ManForEachLo( p, pObj, i ) - { - loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); - Vec_PtrPush( vecLos, pObj->pData ); - nodeName = Aig_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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( 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->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(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; - Aig_Obj_t *pObjSavedLo, *pObjSavedLi; - Aig_Obj_t *pObj, *pMatch; - Aig_Obj_t *pObjSaveOrSaved, *pObjSaveAndNotSaved, *pObjSavedLoAndEquality; - Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver; - Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc; - Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate; - Aig_Obj_t *pObjSafetyPropertyOutput; - Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety; - char *nodeName; - int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 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 ) + 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_ObjCreatePi(pNew); - Vec_PtrPush( vecPis, pObj->pData ); - nodeName = Aig_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_ObjCreatePi( pNew ); - nodeName = "SAVE_BIERE", - Vec_PtrPush( vecPiNames, nodeName ); - } - - //**************************************************************** - // Step 5: create register outputs - //**************************************************************** - Saig_ManForEachLo( p, pObj, i ) - { - loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); - Vec_PtrPush( vecLos, pObj->pData ); - nodeName = Aig_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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( 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->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(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; - 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; - 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 = Aig_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_ObjCreatePi(pNew); - Vec_PtrPush( vecPis, pObj->pData ); - nodeName = Aig_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_ObjCreatePi( pNew ); - nodeName = "SAVE_BIERE", - Vec_PtrPush( vecPiNames, nodeName ); - } - - //**************************************************************** - // Step 5: create register outputs - //**************************************************************** - Saig_ManForEachLo( p, pObj, i ) - { - loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); - Vec_PtrPush( vecLos, pObj->pData ); - nodeName = Aig_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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( 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_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) ); - Aig_ObjCreatePo( 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_ObjCreatePo( 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_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( 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_ManPo( 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_ManPo( 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_ManPo( 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_ManPo( 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; - 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 = Aig_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; i<vectorLength; i++ ) - Vec_IntPush( vFlops, i ); - -#if 0 - Vec_IntPush( vFlops, 19 ); - Vec_IntPush( vFlops, 20 ); - Vec_IntPush( vFlops, 23 ); - Vec_IntPush( vFlops, 24 ); - //Vec_IntPush( vFlops, 2 ); - //Vec_IntPush( vFlops, 3 ); - //Vec_IntPush( vFlops, 4 ); - //Vec_IntPush( vFlops, 5 ); - //Vec_IntPush( vFlops, 8 ); - //Vec_IntPush( vFlops, 9 ); - //Vec_IntPush( vFlops, 10 ); - //Vec_IntPush( vFlops, 11 ); - //Vec_IntPush( vFlops, 0 ); - //Vec_IntPush( vFlops, 0 ); -#endif - - return vFlops; -} - -int Abc_CommandAbcLivenessToSafetyAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld; - Aig_Man_t * pAig, *pAigNew; - int c; - Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety; - int directive = -1; - Vec_Int_t * vFlops; - - 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 ); - } - - vFlops = prepareFlopVector( pAig, Aig_ManRegNum(pAig)%2 == 0? Aig_ManRegNum(pAig)/2 : (Aig_ManRegNum(pAig)-1)/2); - - //vFlops = prepareFlopVector( pAig, 100 ); - - 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 = LivenessToSafetyTransformationAbs( FULL_BIERE_MODE, pNtk, pAig, vFlops, 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 = LivenessToSafetyTransformationAbs( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vFlops, 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 = LivenessToSafetyTransformationAbs( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vFlops, 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; - //} - } - - pNtkNew = Abc_NtkFromAigPhase( pAigNew ); - pNtkNew->pName = Aig_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; -} -ABC_NAMESPACE_IMPL_END - |