summaryrefslogtreecommitdiffstats
path: root/src/aig/live/liveness.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/live/liveness.c')
-rw-r--r--src/aig/live/liveness.c2575
1 files changed, 2575 insertions, 0 deletions
diff --git a/src/aig/live/liveness.c b/src/aig/live/liveness.c
new file mode 100644
index 00000000..e0511556
--- /dev/null
+++ b/src/aig/live/liveness.c
@@ -0,0 +1,2575 @@
+/**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 <stdio.h>
+#include "main.h"
+#include "aig.h"
+#include "saig.h"
+#include <string.h>
+#include "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_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;
+}
+
+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;
+ 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, *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, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
+ Vec_Ptr_t *vSignal, *vTopASTNodeArray;
+ ltlNode *pEnrtyGLOBALLY;
+ ltlNode *topNodeOfAST, *tempTopASTNode;
+ Vec_Vec_t *vAigGFMap;
+ Vec_Ptr_t *vSignalMemory, *vGFFlopMemory, *vPoForLtlProps;
+ 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_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
+ //********************************************************************
+ 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_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;
+ pNegatedSafetyConjunction = Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety );
+ if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
+ 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");
+ pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) );
+ if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
+ pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( 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; i<Vec_PtrSize( vTopASTNodeArray ); i++ )
+ {
+ pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+ 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_ObjCreatePo( 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_ObjCreatePo( 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_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
+
+ //*************************************************************************************
+ // 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_ObjCreatePi( pNew );
+ pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
+ pObjShadowLi = Aig_ObjCreatePo( 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 = 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_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;
+}
+
+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;
+ int c;
+ Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
+ int directive = -1;
+ char *ltfFormulaString = NULL;
+ int LTL_FLAG = 0, numOfLtlPropOutput;
+ 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 = 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: 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