abc/src/proof/live/liveness.c

/**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 "base/main/main.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include <string.h>
#include "base/main/mainInt.h"

ABC_NAMESPACE_IMPL_START

#define PROPAGATE_NAMES
#define MULTIPLE_LTL_FORMULA
#define ALLOW_SAFETY_PROPERTIES

#define FULL_BIERE_MODE 0
#define IGNORE_LIVENESS_KEEP_SAFETY_MODE 1
#define IGNORE_SAFETY_KEEP_LIVENESS_MODE 2
#define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE 3
#define FULL_BIERE_ONE_LOOP_MODE 4
//#define DUPLICATE_CKT_DEBUG

extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
//char *strdup(const char *string);

//******************************************
//external functions defined in ltl_parser.c
//******************************************
typedef struct ltlNode_t ltlNode;
extern ltlNode *readLtlFormula( char *formula );
extern void traverseAbstractSyntaxTree( ltlNode *node );
extern ltlNode *parseFormulaCreateAST( char *inputFormula );
extern int isWellFormed( ltlNode *topNode );
extern int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode );
extern void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode );
extern int checkAllBoolHaveAIGPointer( ltlNode *topASTNode );
extern void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap );
extern void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo );
extern Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode );
extern Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode );
extern void traverseAbstractSyntaxTree_postFix( ltlNode *node );
//**********************************
//external function declaration ends
//**********************************

 
/*******************************************************************
LAYOUT OF PI VECTOR:

+------------------------------------------------------------------------------------------------------------------------------------+
| TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) |
+------------------------------------------------------------------------------------------------------------------------------------+
<------------True PI----------------->|<----------------------------LO--------------------------------------------------------------->

LAYOUT OF PO VECTOR:

+-----------------------------------------------------------------------------------------------------------+
| SOLE PO (1) | ORIGINAL LI (k) | SAVED LI (1) | SHADOW_ORIGINAL LI (k) | LIVENESS LI (l) | FAIRNESS LI (f) |
+-----------------------------------------------------------------------------------------------------------+
<--True PO--->|<--------------------------------------LI---------------------------------------------------->

********************************************************************/


static int nodeName_starts_with( Abc_Obj_t *pNode, const char *prefix )
{
    if( strstr( Abc_ObjName( pNode ), prefix ) == Abc_ObjName( pNode ) )
        return 1;
    else
        return 0;
}

void printVecPtrOfString( Vec_Ptr_t *vec )
{
    int i;

    for( i=0; i< Vec_PtrSize( vec ); i++ )
    {
        printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) );
    }
}

int getPoIndex( Aig_Man_t *pAig, Aig_Obj_t *pPivot )
{
    int i;
    Aig_Obj_t *pObj;

    Saig_ManForEachPo( pAig, pObj, i )
    {
        if( pObj == pPivot )
            return i;
    }
    return -1;
}

char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot )
{
    Aig_Obj_t *pObjOld, *pObj;
    Abc_Obj_t *pNode;
    int index;

    assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
    Aig_ManForEachCi( pAigNew, pObj, index )
        if( pObj == pObjPivot )
            break;
    assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
    if( index == Saig_ManPiNum( pAigNew ) - 1 )
        return "SAVE_BIERE";
    else
    {
        pObjOld = Aig_ManCi( pAigOld, index );
        pNode = Abc_NtkPi( pNtkOld, index );
        assert( pObjOld->pData == pObjPivot );
        return Abc_ObjName( pNode );
    }
}

char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot, Vec_Ptr_t *vLive, Vec_Ptr_t * vFair )
{
    Aig_Obj_t *pObjOld, *pObj;
    Abc_Obj_t *pNode;
    int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i;
    char *dummyStr = (char *)malloc( sizeof(char) * 50 );

    assert( Saig_ObjIsLo( pAigNew, pObjPivot ) );
    Saig_ManForEachLo( pAigNew, pObj, index )
        if( pObj == pObjPivot )
            break;
    if( index < originalLatchNum )
    {
        oldIndex = Saig_ManPiNum( pAigOld ) + index;
        pObjOld = Aig_ManCi( pAigOld, oldIndex );
        pNode = Abc_NtkCi( pNtkOld, oldIndex );
        assert( pObjOld->pData == pObjPivot );
        return Abc_ObjName( pNode );
    }
    else if( index == originalLatchNum )
        return "SAVED_LO";
    else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
    {
        oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
        pObjOld = Aig_ManCi( pAigOld, oldIndex );
        pNode = Abc_NtkCi( pNtkOld, oldIndex );
        sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
        return dummyStr;
    }
    else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) )
    {
        oldIndex = index - 2 * originalLatchNum - 1;
        strMatch = 0;
        dummyStr[0] = '\0';
        Saig_ManForEachPo( pAigOld, pObj, i )
        {
            pNode = Abc_NtkPo( pNtkOld, i );
            //if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
            if(    nodeName_starts_with( pNode, "assert_fair" ) )
            {
                if( strMatch == oldIndex )
                {
                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
                    //return dummyStr;
                    break;
                }
                else
                    strMatch++;
            }
        }
        assert( dummyStr[0] != '\0' );
        return dummyStr;
    }
    else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) )
    {
        oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive );
        strMatch = 0;
        dummyStr[0] = '\0';
        Saig_ManForEachPo( pAigOld, pObj, i )
        {
            pNode = Abc_NtkPo( pNtkOld, i );
            //if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
            if(    nodeName_starts_with( pNode, "assume_fair" ) )
            {
                if( strMatch == oldIndex )
                {
                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
                    //return dummyStr;
                    break;
                }
                else
                    strMatch++;
            }
        }
        assert( dummyStr[0] != '\0' );
        return dummyStr;
    }
    else
        return "UNKNOWN";
}

Vec_Ptr_t *vecPis, *vecPiNames;
Vec_Ptr_t *vecLos, *vecLoNames;


int Aig_ManCiCleanupBiere( Aig_Man_t * p )
{
    int nPisOld = Aig_ManCiNum(p);
    
    p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis );
    if ( Aig_ManRegNum(p) )
        p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
    
    return nPisOld - Aig_ManCiNum(p);
}


int Aig_ManCoCleanupBiere( Aig_Man_t * p )
{
    int nPosOld = Aig_ManCoNum(p);

    p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos );
    if ( Aig_ManRegNum(p) )
        p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
    return nPosOld - Aig_ManCoNum(p);
}

Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
                                           Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
{
    Aig_Man_t * pNew;
    int i, nRegCount;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
    Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;
    
    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
    pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
    sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
    pNew->pSpec = NULL;
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );

    //****************************************************************
    // Step 3: create true PIs
    //****************************************************************
    Saig_ManForEachPi( p, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecPis, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
        Vec_PtrPush( vecPiNames, nodeName );
    }

    //****************************************************************
    // Step 4: create the special Pi corresponding to SAVE
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSavePi = Aig_ObjCreateCi( pNew );
        nodeName = "SAVE_BIERE",
        Vec_PtrPush( vecPiNames, nodeName );
    }
        
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
    Saig_ManForEachLo( p, pObj, i )
    {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecLos, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 6: create "saved" register output
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        loCreated++;
        pObjSavedLo = Aig_ObjCreateCi( pNew );
        Vec_PtrPush( vecLos, pObjSavedLo );
        nodeName = "SAVED_LO";
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
        pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
    }

    //********************************************************************
    // Step 8: create internal nodes
    //********************************************************************
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }

    
    //********************************************************************
    // Step 8.x : create PO for each safety assertions
    // NOTE : Here the output is purposely inverted as it will be thrown to 
    // dprove
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
    {
        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
        }
        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssertSafety = pObjAndAcc;

            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssumeSafety = pObjAndAcc;
            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
        }
        else
        {
            printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
        }
    }

    //********************************************************************
    // Step 9: create the safety property output gate for the liveness properties
    // discuss with Sat/Alan for an alternative implementation
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
    }

    // create register inputs for the original registers
    nRegCount = 0;
    
    Saig_ManForEachLo( p, pObj, i )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
        nRegCount++;
        liCopied++;
    }

    // create register input corresponding to the register "saved"
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        #ifndef DUPLICATE_CKT_DEBUG
            pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
            nRegCount++;
            liCreated++;

            //Changed on October 13, 2009
            //pObjAndAcc = NULL;
            pObjAndAcc = Aig_ManConst1( pNew );

    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
            Saig_ManForEachLo( p, pObj, i )
            {
                pObjShadowLo = Aig_ObjCreateCi( pNew );

                #ifdef PROPAGATE_NAMES
                    Vec_PtrPush( vecLos, pObjShadowLo );
                    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
                    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
                    
                    Vec_PtrPush( vecLoNames, nodeName );
                #endif

                pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                nRegCount++;
                loCreated++; liCreated++;
        
                pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjXnor = Aig_Not( pObjXor );
                
                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
            }

            // create the AND gate whose output will be the signal "looped"
            pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );

            // create the master AND gate and corresponding AND and OR logic for the liveness properties
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
            {
                printf("Circuit without any liveness property\n");
            }
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
                {
                    liveLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjLive = pObjAndAcc;
                
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
                printf("Circuit without any fairness property\n");
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
                {
                    fairLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjFair = pObjAndAcc;
                
            //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
            //Following is the actual Biere translation
            pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );

            Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
        #endif
    }

    Aig_ManSetRegNum( pNew, nRegCount );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );
    
    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
            assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
    }

    return pNew;
}





Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Int_t *vFlops, 
                                           Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
{
    Aig_Man_t * pNew;
    int i, nRegCount, iEntry;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObjSavedLi = NULL, *pObjSavedLo = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSavedLoAndEquality, *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;//, piVecIndex = 0;
    
    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
    pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
    sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
    pNew->pSpec = NULL;
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );

    //****************************************************************
    // Step 3: create true PIs
    //****************************************************************
    Saig_ManForEachPi( p, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecPis, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
        Vec_PtrPush( vecPiNames, nodeName );
    }

    //****************************************************************
    // Step 4: create the special Pi corresponding to SAVE
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSavePi = Aig_ObjCreateCi( pNew );
        nodeName = "SAVE_BIERE",
        Vec_PtrPush( vecPiNames, nodeName );
    }
        
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
    Saig_ManForEachLo( p, pObj, i )
    {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecLos, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 6: create "saved" register output
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        loCreated++;
        pObjSavedLo = Aig_ObjCreateCi( pNew );
        Vec_PtrPush( vecLos, pObjSavedLo );
        nodeName = "SAVED_LO";
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
        pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
    }

    //********************************************************************
    // Step 8: create internal nodes
    //********************************************************************
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }

    
    //********************************************************************
    // Step 8.x : create PO for each safety assertions
    // NOTE : Here the output is purposely inverted as it will be thrown to 
    // dprove
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
    {
        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
        }
        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssertSafety = pObjAndAcc;

            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssumeSafety = pObjAndAcc;
            Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
        }
        else
        {
            printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
            Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
        }
    }

    //********************************************************************
    // Step 9: create the safety property output gate for the liveness properties
    // discuss with Sat/Alan for an alternative implementation
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
    }

    // create register inputs for the original registers
    nRegCount = 0;
    
    Saig_ManForEachLo( p, pObj, i )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
        nRegCount++;
        liCopied++;
    }

    // create register input corresponding to the register "saved"
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        #ifndef DUPLICATE_CKT_DEBUG
            pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
            nRegCount++;
            liCreated++;

            //Changed on October 13, 2009
            //pObjAndAcc = NULL;
            pObjAndAcc = Aig_ManConst1( pNew );

    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
            //Saig_ManForEachLo( p, pObj, i )
            Saig_ManForEachLo( p, pObj, i )
            {
                printf("Flop[%d] = %s\n", i, Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) );
            }
            Vec_IntForEachEntry( vFlops, iEntry, i )
            {
                pObjShadowLo = Aig_ObjCreateCi( pNew );
                pObj = Aig_ManLo( p, iEntry );

                #ifdef PROPAGATE_NAMES
                    Vec_PtrPush( vecLos, pObjShadowLo );
                    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ) ) + 10 );
                    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ), "SHADOW" );
                    printf("Flop copied [%d] = %s\n", iEntry, nodeName );
                    Vec_PtrPush( vecLoNames, nodeName );
                #endif

                pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                nRegCount++;
                loCreated++; liCreated++;
        
                pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjXnor = Aig_Not( pObjXor );
                
                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
            }

            // create the AND gate whose output will be the signal "looped"
            pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );

            // create the master AND gate and corresponding AND and OR logic for the liveness properties
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
            {
                printf("Circuit without any liveness property\n");
            }
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
                {
                    liveLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjLive = pObjAndAcc;
                
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
                printf("Circuit without any fairness property\n");
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
                {
                    fairLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjFair = pObjAndAcc;
                
            //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
            //Following is the actual Biere translation
            pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );

            Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
        #endif
    }

    Aig_ManSetRegNum( pNew, nRegCount );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );
    
    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
            assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
    }

    return pNew;
}



Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
                                                      Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
{
    Aig_Man_t * pNew;
    int i, nRegCount;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
    Aig_Obj_t *pDriverImage;
    Aig_Obj_t *pObjCorrespondingLi;
    Aig_Obj_t *pArgument;
    Aig_Obj_t *collectiveAssertSafety, *collectiveAssumeSafety;

    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0;

    if( Aig_ManRegNum( p ) == 0 )
    {
        printf("The input AIG contains no register, returning the original AIG as it is\n");
        return p;
    }

    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( "live2safe" );
    pNew->pSpec = NULL;
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );

    //****************************************************************
    // Step 3: create true PIs
    //****************************************************************
    Saig_ManForEachPi( p, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecPis, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
        Vec_PtrPush( vecPiNames, nodeName );
    }

    //****************************************************************
    // Step 4: create the special Pi corresponding to SAVE
    //****************************************************************
    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
    {
        pObjSavePi = Aig_ObjCreateCi( pNew );
        nodeName = "SAVE_BIERE",
        Vec_PtrPush( vecPiNames, nodeName );
    }
            
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
    Saig_ManForEachLo( p, pObj, i )
    {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecLos, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 6: create "saved" register output
    //****************************************************************

#if 0
    loCreated++;
    pObjSavedLo = Aig_ObjCreateCi( pNew );
    Vec_PtrPush( vecLos, pObjSavedLo );
    nodeName = "SAVED_LO";
    Vec_PtrPush( vecLoNames, nodeName );
#endif

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
#if 0
    pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
    pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
#endif

    //********************************************************************
    // Step 8: create internal nodes
    //********************************************************************
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }

#if 0
    //********************************************************************
    // Step 8.x : create PO for each safety assertions
    //********************************************************************
    Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
    {
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
    }
#endif

    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
    {
        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
        {
            pObjAndAcc = NULL;
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pArgument;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                }
            }
            Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
        }
        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
        {
            pObjAndAcc = NULL;
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pArgument;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                }
            }
            collectiveAssertSafety = pObjAndAcc;
            pObjAndAcc = NULL;
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
            {
                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pArgument;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                }
            }
            collectiveAssumeSafety = pObjAndAcc;
            Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
        }
        else
            printf("No safety property is specified, hence no safety gate is created\n");
    }

    //********************************************************************
    // Step 9: create the safety property output gate
    // create the safety property output gate, this will be the sole true PO 
    // of the whole circuit, discuss with Sat/Alan for an alternative implementation
    //********************************************************************

    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
    {
        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
    }

    // create register inputs for the original registers
    nRegCount = 0;
    
    Saig_ManForEachLo( p, pObj, i )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
        nRegCount++;
        liCopied++;
    }

#if 0
    // create register input corresponding to the register "saved"
    pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
    nRegCount++;
    liCreated++;7
#endif

    pObjAndAcc = NULL;

    //****************************************************************************************************
    //For detection of loop of length 1 we do not need any shadow register, we only need equality detector
    //between Lo_j and Li_j and then a cascade of AND gates
    //****************************************************************************************************

    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
    {
        Saig_ManForEachLo( p, pObj, i )
        {
            pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj );
        
            pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData,  Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) );
            pObjXnor = Aig_Not( pObjXor );
        
            if( pObjAndAcc == NULL )
                pObjAndAcc = pObjXnor;
            else
            {
                pObjAndAccDummy = pObjAndAcc;
                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
            }
        }

        // create the AND gate whose output will be the signal "looped"
        pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc );
    
        // create the master AND gate and corresponding AND and OR logic for the liveness properties
        pObjAndAcc = NULL;
        if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
            printf("Circuit without any liveness property\n");
        else
        {
            Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
            {
                pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pDriverImage;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
                }
            }
        }

        if( pObjAndAcc != NULL )
            pObjLive = pObjAndAcc;
        else
            pObjLive = Aig_ManConst1( pNew );
    
        // create the master AND gate and corresponding AND and OR logic for the fairness properties
        pObjAndAcc = NULL;
        if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
            printf("Circuit without any fairness property\n");
        else
        {
            Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
            {
                pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pDriverImage;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
                }
            }
        }

        if( pObjAndAcc != NULL )
            pObjFair = pObjAndAcc;
        else
            pObjFair = Aig_ManConst1( pNew );
    
        pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
    
        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
    }

    Aig_ManSetRegNum( pNew, nRegCount );

    //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );

    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    return pNew;
}



Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
    Abc_Obj_t * pNode;
    int i, liveCounter = 0;
    Vec_Ptr_t * vLive;

    vLive = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
        if( nodeName_starts_with( pNode, "assert_fair" ) )
        {
            Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
            liveCounter++;
        }
    printf("Number of liveness property found = %d\n", liveCounter);
    return vLive;
}

Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
    Abc_Obj_t * pNode;
    int i, fairCounter = 0;
    Vec_Ptr_t * vFair;

    vFair = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
        if( nodeName_starts_with( pNode, "assume_fair" ) )
        {
            Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
            fairCounter++;
        }
    printf("Number of fairness property found = %d\n", fairCounter);
    return vFair;
}

Vec_Ptr_t * populateSafetyAssertionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
    Abc_Obj_t * pNode;
    int i, assertSafetyCounter = 0;
    Vec_Ptr_t * vAssertSafety;

    vAssertSafety = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
        if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" ))
        {
            Vec_PtrPush( vAssertSafety, Aig_ManCo( pAig, i ) );
            assertSafetyCounter++;
        }
    printf("Number of safety property found = %d\n", assertSafetyCounter);
    return vAssertSafety;
}

Vec_Ptr_t * populateSafetyAssumptionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
{
    Abc_Obj_t * pNode;
    int i, assumeSafetyCounter = 0;
    Vec_Ptr_t * vAssumeSafety;

    vAssumeSafety = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
        if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" ))
        {
            Vec_PtrPush( vAssumeSafety, Aig_ManCo( pAig, i ) );
            assumeSafetyCounter++;
        }
    printf("Number of assume_safety property found = %d\n", assumeSafetyCounter);
    return vAssumeSafety;
}

void updateNewNetworkNameManager( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames )
{
    Aig_Obj_t *pObj;
    Abc_Obj_t *pNode;
    int i, ntkObjId;

    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );

    if( vPiNames )
    {
        Saig_ManForEachPi( pAig, pObj, i )
        {
            ntkObjId = Abc_NtkCi( pNtk, i )->Id;
            //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId);  
            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
        }
    }
    if( vLoNames )
    {
        Saig_ManForEachLo( pAig, pObj, i )
        {
            ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
            //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId);  
            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
        }
    }

    Abc_NtkForEachPo(pNtk, pNode, i)
    {
        Abc_ObjAssignName(pNode, "assert_safety_", Abc_ObjName(pNode) );
    }

    // assign latch input names
    Abc_NtkForEachLatch(pNtk, pNode, i)
        if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL )
            Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL );
}


int Abc_CommandAbcLivenessToSafety( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
    Aig_Man_t * pAig, *pAigNew = NULL;
    int c;
    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
    int directive = -1;
                
    pNtk = Abc_FrameReadNtk(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);

    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = FULL_BIERE_MODE;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF )
        {
            switch( c )
            {
            case '1': 
                if( directive == -1 )
                    directive = FULL_BIERE_ONE_LOOP_MODE;
                else
                {
                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                    else
                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 's':
                if( directive == -1 )
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 'l':
                if( directive == -1 )
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                }
                break;
            case 'h':
                goto usage;
            default:
                goto usage;
            }
        }
    }

    if ( pNtk == NULL )
    {
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pNtkOld = pNtkTemp;
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkOld = pNtk;
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }

    switch( directive )
    {
    case FULL_BIERE_MODE:
        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
        //{
        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
            break;
        //}
    case FULL_BIERE_ONE_LOOP_MODE:
        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
        //{
        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        //}
    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
        //if( Vec_PtrSize(vAssertSafety) == 0 )
        //{    
        //    printf("Input circuit has NO safety property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        //}
    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
        //if( Vec_PtrSize(vLive) == 0 )
        //{    
        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
            break;
        //}
    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
        //if( Vec_PtrSize(vLive) == 0 )
        //{
        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
            break;
        //}
    }

#if 0
    if( argc == 1 )
    {
        pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        if( Aig_ManRegNum(pAigNew) != 0 )
            printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
    }
    else 
    {
        Extra_UtilGetoptReset();
        c = Extra_UtilGetopt( argc, argv, "1lsh" );
        if( c == '1' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        }
        else if( c == 'l' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
        }
        else if( c == 's' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
        }
        else if( c == 'h' )
            goto usage;
        else
            goto usage;
    }
#endif
    
#if 0
    Aig_ManPrintStats( pAigNew );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
    printf("\n*******************************************************\n");
#endif

    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
    pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
    
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    
    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );

#if 0
#ifndef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPi( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );

    Saig_ManForEachLo( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
#endif    
#endif
        
    return 0;

usage:
    fprintf( stdout, "usage: l2s [-1lsh]\n" );
    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
    fprintf( stdout, "\t-h : print command usage\n");
    return 1;
}

Vec_Int_t * prepareFlopVector( Aig_Man_t * pAig, int vectorLength )
{
    Vec_Int_t *vFlops;
    int i;

    vFlops = Vec_IntAlloc( vectorLength );

    for( i=0; 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 = NULL;
    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 = Abc_UtilStrsav( pAigNew->pName );
    
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    
    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );

#if 0
#ifndef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPi( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );

    Saig_ManForEachLo( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
#endif    
#endif
        
    return 0;

usage:
    fprintf( stdout, "usage: l2s [-1lsh]\n" );
    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
    fprintf( stdout, "\t-h : print command usage\n");
    return 1;
}

Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
                                           Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety,
                                           int *numLtlProcessed, Vec_Ptr_t *ltlBuffer )
{
    Aig_Man_t * pNew;
    int i, ii, iii, nRegCount;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
    Aig_Obj_t *pObjLive, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput;
    Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
    Aig_Obj_t *pNegatedSafetyConjunction = NULL;
    Aig_Obj_t *pObjSafetyAndLiveToSafety;
    char *nodeName, *pFormula;
    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0;//, piVecIndex = 0, fairLatch = 0;
    Vec_Ptr_t *vSignal, *vTopASTNodeArray = NULL;
    ltlNode *pEnrtyGLOBALLY;
    ltlNode *topNodeOfAST, *tempTopASTNode;
    Vec_Vec_t *vAigGFMap;
    Vec_Ptr_t *vSignalMemory, *vGFFlopMemory, *vPoForLtlProps = NULL;
    Vec_Ptr_t *vecInputLtlFormulae;
    
    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    //step0: Parsing the LTL formula
    //****************************************************************
    //Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pFormula, i )
    //    printf("\ninput LTL formula [%d] = %s\n", i, pFormula );


#ifdef MULTIPLE_LTL_FORMULA


    //***************************************************************************
    //Reading input LTL formulae from Ntk data-structure and creating 
    //AST for them, Steps involved: 
    //        parsing -> AST creation -> well-formedness check -> signal name check
    //***************************************************************************

    //resetting numLtlProcessed
    *numLtlProcessed = 0;
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        //if( ltlBuffer )
        vecInputLtlFormulae = ltlBuffer;
        //vecInputLtlFormulae = pNtk->vLtlProperties;
        if( vecInputLtlFormulae )
        {
            vTopASTNodeArray = Vec_PtrAlloc( Vec_PtrSize( vecInputLtlFormulae ) );
            printf("\n");
            Vec_PtrForEachEntry( char *, vecInputLtlFormulae, pFormula, i )
            {
                tempTopASTNode = parseFormulaCreateAST( pFormula );
                //traverseAbstractSyntaxTree_postFix( tempTopASTNode );
                if( tempTopASTNode )
                {
                    printf("Formula %d: AST is created, ", i+1);
                    if( isWellFormed( tempTopASTNode ) )
                        printf("Well-formedness check PASSED, ");
                    else
                    {
                        printf("Well-formedness check FAILED!!\n");
                        printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
                        //do memory management to free the created AST
                        continue;
                    }
                    if( checkSignalNameExistence( pNtk, tempTopASTNode ) )
                        printf("Signal check PASSED\n");
                    else
                    {
                        printf("Signal check FAILED!!");
                        printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
                        //do memory management to free the created AST
                        continue;
                    }
                    Vec_PtrPush( vTopASTNodeArray, tempTopASTNode );
                    (*numLtlProcessed)++;
                }
                else
                    printf("\nNo AST has been created for formula %d, no extra logic will be added\n", i+1 );
            }
        }
        printf("\n");
        if( Vec_PtrSize( vTopASTNodeArray ) == 0 )
        {
            //printf("\nNo AST has been created for any formula; hence the circuit is left untouched\n");
            printf("\nCurrently aborting, need to take care when Vec_PtrSize( vTopASTNodeArray ) == 0\n");
            exit(0);
        }
    }

        //****************************************************************
        // Step1: create the new manager
        // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
        // nodes, but this selection is arbitrary - need to be justified
        //****************************************************************
        pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
        pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l3s") + 1 );
        sprintf(pNew->pName, "%s_%s", pNtk->pName, "l3s");
        pNew->pSpec = NULL;
    
        //****************************************************************
        // Step 2: map constant nodes
        //****************************************************************
        pObj = Aig_ManConst1( p );
        pObj->pData = Aig_ManConst1( pNew );

        //****************************************************************
        // Step 3: create true PIs
        //****************************************************************
        Saig_ManForEachPi( p, pObj, i )
        {
            piCopied++;
            pObj->pData = Aig_ObjCreateCi(pNew);
            Vec_PtrPush( vecPis, pObj->pData );
            nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
            Vec_PtrPush( vecPiNames, nodeName );
        }

        //****************************************************************
        // Step 4: create the special Pi corresponding to SAVE
        //****************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            pObjSavePi = Aig_ObjCreateCi( pNew );
            nodeName = "SAVE_BIERE",
            Vec_PtrPush( vecPiNames, nodeName );
        }
        
        //****************************************************************
        // Step 5: create register outputs
        //****************************************************************
        Saig_ManForEachLo( p, pObj, i )
        {
            loCopied++;
            pObj->pData = Aig_ObjCreateCi(pNew);
            Vec_PtrPush( vecLos, pObj->pData );
            nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
            Vec_PtrPush( vecLoNames, nodeName );
        }

        //****************************************************************
        // Step 6: create "saved" register output
        //****************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            loCreated++;
            pObjSavedLo = Aig_ObjCreateCi( pNew );
            Vec_PtrPush( vecLos, pObjSavedLo );
            nodeName = "SAVED_LO";
            Vec_PtrPush( vecLoNames, nodeName );
        }

        //****************************************************************
        // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
        //****************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
            pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
        }

        //********************************************************************
        // Step 8: create internal nodes
        //********************************************************************
        Aig_ManForEachNode( p, pObj, i )
        {
            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
        }

        
        //********************************************************************
        // Step 8.x : create PO for each safety assertions
        // NOTE : Here the output is purposely inverted as it will be thrown to 
        // dprove
        //********************************************************************
        assert( pNegatedSafetyConjunction == NULL );
        if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE)
        {
            if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
            {
                pObjAndAcc = Aig_ManConst1( pNew );
                Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
                {
                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
                }
                pNegatedSafetyConjunction = Aig_Not(pObjAndAcc);
                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
            }
            else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
            {
                pObjAndAcc = Aig_ManConst1( pNew );
                Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
                {
                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
                }
                collectiveAssertSafety = pObjAndAcc;

                pObjAndAcc = Aig_ManConst1( pNew );
                Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
                {
                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
                }
                collectiveAssumeSafety = pObjAndAcc;
                pNegatedSafetyConjunction =  Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety );
                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
            }
            else
            {
                printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
                pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) );
                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
            }
        }
        assert( pNegatedSafetyConjunction != NULL );

        //********************************************************************
        // Step 9: create the safety property output gate for the liveness properties
        // discuss with Sat/Alan for an alternative implementation
        //********************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            vPoForLtlProps = Vec_PtrAlloc( Vec_PtrSize( vTopASTNodeArray ) );
            if( Vec_PtrSize( vTopASTNodeArray ) )
            {
                //no effective AST for any input LTL property
                //must do something graceful
            }
            for( i=0; i<Vec_PtrSize( vTopASTNodeArray ); i++ )
            {
                pObjSafetyPropertyOutput = Aig_ObjCreateCo( 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_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
            nRegCount++;
            liCopied++;
        }

        //*************************************************************************************
        // Step 11: create register input corresponding to the register "saved"
        //*************************************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            #ifndef DUPLICATE_CKT_DEBUG
                pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
                nRegCount++;
                liCreated++;

                pObjAndAcc = Aig_ManConst1( pNew );

                //*************************************************************************************
                // Step 11: create the family of shadow registers, then create the cascade of Xnor 
                // and And gates for the comparator 
                //*************************************************************************************
                Saig_ManForEachLo( p, pObj, i )
                {
                //printf("\nKEMON RENDY = %s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i )) );
                //top|route0_target0_queue_with_credit0_queue0
                //top|route0_master0_queue2
                //    if( strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0 
                //            || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 )
                    {        
                        pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
                        
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                        pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                        pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                        nRegCount++;
                        loCreated++; liCreated++;
            
                        pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                        pObjXnor = Aig_Not( pObjXor );
                    
                        pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
                    }
                }

                // create the AND gate whose output will be the signal "looped"
                pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );

                // create the master AND gate and corresponding AND and OR logic for the liveness properties
                
                //*************************************************************************************
                // Step 11: logic for LTL properties:- (looped & ~theta) where theta is the input ltl 
                // property
                // Description of some data-structure:
                //-------------------------------------------------------------------------------------
                // Name          | Type            | Purpose
                //-------------------------------------------------------------------------------------
                // vSignalMemory | Vec_Ptr_t *     | A vector across all ASTs of the LTL properties
                //                 |                   | It remembers if OR+Latch for GF node has already been
                //                 |                   | created for a particular signal.
                //               |                 |
                // vGFFlopMemory | Vec_Ptr_t *     | A vector across all ASTs of the LTL properties
                //                 |                 | remembers if OR+Latch of a GF node has already been created
                //                 |                 |
                // vSignal         | Vec_Ptr_t *     | vector for each AST; contains pointers from GF nodes
                //               |                 | to AIG signals
                //                 |                   |
                // vAigGFMap     | Vec_Vec_t *     | vAigGFMap[ index ] = vector of GF nodes pointing to
                //               |                 | the same AIG node; "index" is the index of that
                //               |                 | AIG node in the vector vSignal
                //*************************************************************************************
                
                vSignalMemory = Vec_PtrAlloc(10);
                vGFFlopMemory = Vec_PtrAlloc(10);

                Vec_PtrForEachEntry( ltlNode *, vTopASTNodeArray, topNodeOfAST, iii )
                {
                                    vSignal = Vec_PtrAlloc( 10 );
                                    vAigGFMap = Vec_VecAlloc( 10 );
                                    
                                    //*************************************************************************************
                                    //Step 11a: for the current AST, find out the leaf level Boolean signal pointers from 
                                    // the NEW aig.
                                    //*************************************************************************************
                                    populateBoolWithAigNodePtr( pNtk, p, pNew, topNodeOfAST );
                                    assert( checkAllBoolHaveAIGPointer( topNodeOfAST ) );

                                    //*************************************************************************************
                                    //Step 11b: for each GF node, compute the pointer in AIG that it should point to
                                    // In particular, if the subtree below GF is some Boolean crown (including the case
                                    // of simple negation, create new logic and populate the AIG pointer in GF node
                                    // accordingly
                                    //*************************************************************************************
                                    populateAigPointerUnitGF( pNew, topNodeOfAST, vSignal, vAigGFMap );
                                    
                                    //*************************************************************************************
                                    //Step 11c: everything below GF are computed. Now, it is time to create logic for individual 
                                    // GF nodes (i.e. the OR gate and the latch and the Boolean crown of the AST
                                    //*************************************************************************************
                                    Vec_PtrForEachEntry( Aig_Obj_t *, vSignal, pObj, i )
                                    {
                                        //*********************************************************
                                        // Step 11c.1: if the OR+Latch of the particular signal is
                                        // not already created, create it. It may have already been 
                                        // created from another property, so check it before creation
                                        //*********************************************************
                                        if( Vec_PtrFind( vSignalMemory, pObj ) == -1 )
                                        {
                                            liveLatch++;

                                            pDriverImage = pObj;
                                            pObjShadowLo = Aig_ObjCreateCi( pNew );
                                            pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                                            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );

                                            nRegCount++;
                                            loCreated++; liCreated++;

                                            Vec_PtrPush( vSignalMemory, pObj );
                                            Vec_PtrPush( vGFFlopMemory, pObjShadowLo );

                                            #if 1
                                            #ifdef PROPAGATE_NAMES
                                                Vec_PtrPush( vecLos, pObjShadowLo );
                                                //nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                                                //sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                                                nodeName = (char *)malloc( 20 );
                                                sprintf( nodeName, "n%d__%s", Aig_ObjId(pObjShadowLo), "GF_flop" );
                                                Vec_PtrPush( vecLoNames, nodeName );
                                            #endif
                                            #endif
                                        }
                                        else
                                            pObjShadowLo = (Aig_Obj_t *)Vec_PtrEntry( vGFFlopMemory, Vec_PtrFind( vSignalMemory, pObj ) );
                                                                                
                                        Vec_VecForEachEntryLevel( ltlNode *, vAigGFMap, pEnrtyGLOBALLY, ii, i )
                                            setAIGNodePtrOfGloballyNode( pEnrtyGLOBALLY, pObjShadowLo);
                                            

                                        //#ifdef PROPAGATE_NAMES
                                        //    Vec_PtrPush( vecLos, pObjShadowLo );
                                        //    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                                        //    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                                        //    Vec_PtrPush( vecLoNames, nodeName );
                                        //#endif
                                        
                                    }
                                    
                                    //*********************************************************
                                    //Step 11c.2: creating the Boolean crown
                                    //*********************************************************
                                    buildLogicFromLTLNode( pNew, topNodeOfAST );

                                    //*********************************************************
                                    //Step 11c.3: creating logic for (looped & ~theta) and patching
                                    // it with the proper PO
                                    //Note: if ALLOW_SAFETY_PROPERTIES is defined then the final AND
                                    //gate is a conjunction of safety & liveness, i.e. SAFETY & (looped => theta)
                                    //since ABC convention demands a NOT gate at the end, the property logic 
                                    //becomes !( SAFETY & (looped => theta) ) = !SAFETY + (looped & !theta)
                                    //*********************************************************
                                    pObjLive = retriveAIGPointerFromLTLNode( topNodeOfAST );
                                    pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_Not(pObjLive) );
                                    #ifdef ALLOW_SAFETY_PROPERTIES
                                        printf("liveness output is conjoined with safety assertions\n");
                                        pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction );
                                        pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii );
                                        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety );
                                    #else
                                        pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
                                        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
                                    #endif
                                    //refreshing vSignal and vAigGFMap arrays
                                    Vec_PtrFree( vSignal );
                                    Vec_VecFree( vAigGFMap );
                }
                                
            #endif
        }
#endif

    Aig_ManSetRegNum( pNew, nRegCount );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );
    
    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
            //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
    }


    return pNew;
}

int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
    Aig_Man_t * pAig, *pAigNew = NULL;
    int c;
    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
    int directive = -1;
//    char *ltfFormulaString = NULL;
    int numOfLtlPropOutput;//, LTL_FLAG = 0;
    Vec_Ptr_t *ltlBuffer;
                
    pNtk = Abc_FrameReadNtk(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);

    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = FULL_BIERE_MODE;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "1slhf" ) ) != EOF )
        {
            switch( c )
            {
            case '1': 
                if( directive == -1 )
                    directive = FULL_BIERE_ONE_LOOP_MODE;
                else
                {
                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                    else
                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 's':
                if( directive == -1 )
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 'l':
                if( directive == -1 )
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                }
                break;
            case 'f':
                //assert( argc >= 3 );
                //vecLtlFormula = Vec_PtrAlloc( argc - 2 );
                //if( argc >= 3 )
                //{
                //    for( t=3; t<=argc; t++ )
                //    {
                //        printf("argv[%d] = %s\n", t-1, argv[t-1]);
                //        Vec_PtrPush( vecLtlFormula, argv[t-1] );
                //    }
                //}
                //printf("argv[argc] = %s\n", argv[argc-1]);
                //ltfFormulaString = argv[2];
                
                //LTL_FLAG = 1;
                printf("\nILLEGAL FLAG: aborting....\n");
                exit(0);
                break;
            case 'h':
                goto usage;
            default:
                goto usage;
            }
        }
    }

    if ( pNtk == NULL )
    {
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pNtkOld = pNtkTemp;
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkOld = pNtk;
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }

    if( pAbc->vLTLProperties_global != NULL )
        ltlBuffer = pAbc->vLTLProperties_global;
    else
        ltlBuffer = NULL;

    switch( directive )
    {
    case FULL_BIERE_MODE:
            pAigNew = LivenessToSafetyTransformationWithLTL( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t%d POs - one for safety and %d for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput+1, numOfLtlPropOutput);
            break;
        
    case FULL_BIERE_ONE_LOOP_MODE:
            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        
    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
            pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
            assert( numOfLtlPropOutput == 0 );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        
    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
            pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t%d PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput);
            break;
        
    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
            break;
    }

#if 0
    if( argc == 1 )
    {
        pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        if( Aig_ManRegNum(pAigNew) != 0 )
            printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
    }
    else 
    {
        Extra_UtilGetoptReset();
        c = Extra_UtilGetopt( argc, argv, "1lsh" );
        if( c == '1' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        }
        else if( c == 'l' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
        }
        else if( c == 's' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
        }
        else if( c == 'h' )
            goto usage;
        else
            goto usage;
    }
#endif
    
#if 0
    Aig_ManPrintStats( pAigNew );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
    printf("\n*******************************************************\n");
#endif

    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
    pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
    
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    
    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );

#if 0
#ifndef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPi( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );

    Saig_ManForEachLo( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
#endif    
#endif
        
    return 0;

usage:
    fprintf( stdout, "usage: l3s [-1lsh]\n" );
    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
    fprintf( stdout, "\t-h : print command usage\n");
    return 1;
}


ABC_NAMESPACE_IMPL_END