/**CFile****************************************************************

  FileName    [liveness_sim.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_sim.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>

ABC_NAMESPACE_IMPL_START


#define PROPAGATE_NAMES
//#define DUPLICATE_CKT_DEBUG

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


/*******************************************************************
LAYOUT OF PI VECTOR:
 
+------------------------------------------------------------------------------------------------------------------------------------+
| TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) |
+------------------------------------------------------------------------------------------------------------------------------------+
<------------True PI----------------->|<----------------------------LO--------------------------------------------------------------->

LAYOUT OF PO VECTOR:

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

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

static 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) );
    }
}

static 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;
}

static 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 );
    }
}

static 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;
        Saig_ManForEachPo( pAigOld, pObj, i )
        {
            pNode = Abc_NtkPo( pNtkOld, i );
            if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
            {
                if( strMatch == oldIndex )
                {
                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
                    return dummyStr;
                }
                else
                    strMatch++;
            }
        }
    }
    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;
        Saig_ManForEachPo( pAigOld, pObj, i )
        {
            pNode = Abc_NtkPo( pNtkOld, i );
            if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
            {
                if( strMatch == oldIndex )
                {
                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
                    return dummyStr;
                }
                else
                    strMatch++;
            }
        }
    }
    else
        return "UNKNOWN";
    return NULL;
}

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


static 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);
}


static 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);
}

static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
{
    Aig_Man_t * pNew;
    int i, nRegCount;
    Aig_Obj_t * pObjSavePi;
    Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSaveOrSaved, *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput;
    Aig_Obj_t *pDriverImage;
    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 ) );

#ifdef DUPLICATE_CKT_DEBUG
    printf("\nCode is compiled in DEBUG mode, the input-output behavior will be the same as the original circuit\n");
    printf("Press any key to continue...");
    scanf("%c", &c);
#endif

    //****************************************************************
    // 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
    //****************************************************************
#ifndef DUPLICATE_CKT_DEBUG
    pObjSavePi = Aig_ObjCreateCi( pNew );
    nodeName = Abc_UtilStrsav("SAVE_BIERE"),
    Vec_PtrPush( vecPiNames, nodeName );
#endif
        
    //****************************************************************
    // 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
    //****************************************************************
#ifndef DUPLICATE_CKT_DEBUG
    loCreated++;
    pObjSavedLo = Aig_ObjCreateCi( pNew );
    Vec_PtrPush( vecLos, pObjSavedLo );
    nodeName = Abc_UtilStrsav("SAVED_LO");
    Vec_PtrPush( vecLoNames, nodeName );
#endif

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
#ifndef DUPLICATE_CKT_DEBUG
    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) );
    }

    //********************************************************************
    // 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
    //********************************************************************
#ifndef DUPLICATE_CKT_DEBUG
    pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
#endif

    //********************************************************************
    // DEBUG: To recreate the same circuit, at least from the input and output
    // behavior, we need to copy the original PO
    //********************************************************************
#ifdef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPo( p, pObj, i )
    {
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
#endif

    // 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++;
    }

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

    pObjAndAcc = NULL;

    // 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, pObjSavePi, (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 );
        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, pObjSavedLo, 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("\nCircuit without any liveness property\n");
    else
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
        {
            //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
            //Aig_ObjPrint( pNew, pObj );
            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, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), 
                                                Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
            nRegCount++;
            loCreated++; liCreated++;
            
            if( pObjAndAcc == NULL )
                pObjAndAcc = pObjShadowLo;
            else
            {
                pObjAndAccDummy = pObjAndAcc;
                pObjAndAcc = Aig_And( pNew, pObjShadowLo, 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("\nCircuit without any fairness property\n");
    else
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
        {
            fairLatch++;
            //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
            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, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), 
                                    Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
            nRegCount++;
            loCreated++; liCreated++;
            
            if( pObjAndAcc == NULL )
                pObjAndAcc = pObjShadowLo;
            else
            {
                pObjAndAccDummy = pObjAndAcc;
                pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAccDummy );
            }
        }
    }

    if( pObjAndAcc != NULL )
        pObjFair = pObjAndAcc;
    else
        pObjFair = Aig_ManConst1( pNew );
    
    //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
    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 ) );
    
#ifndef DUPLICATE_CKT_DEBUG
    assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
    assert( Saig_ManPoNum( pNew ) == 1 );
    assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
    assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
#endif

    return pNew;
}


static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
{
    Aig_Man_t * pNew;
    int i, nRegCount;
    Aig_Obj_t * pObjSavePi;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput;
    Aig_Obj_t *pDriverImage;
    Aig_Obj_t *pObjCorrespondingLi;


    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 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 = 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
    //****************************************************************
    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) );
    }

    //********************************************************************
    // 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
    //********************************************************************

    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++;
#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
    //****************************************************************************************************

    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("\nCircuit 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("\nCircuit 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->vCis ), pNew->nRegs );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );

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


static 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 )
        {
            Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
            liveCounter++;
        }
    printf("\nNumber of liveness property found = %d\n", liveCounter);
    return vLive;
}

static 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 )
        {
            Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
            fairCounter++;
        }
    printf("\nNumber of fairness property found = %d\n", fairCounter);
    return vFair;
}

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

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

    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 );
    }
    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 );
    }
}


int Abc_CommandAbcLivenessToSafetySim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
    Aig_Man_t * pAig, *pAigNew;
    int c;
    Vec_Ptr_t * vLive, * vFair;
                
    pNtk = Abc_FrameReadNtk(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);

    if ( pNtk == NULL )
    {
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }

    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("\nThe 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 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkOld = pNtk;
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
    }

#if 0
    Aig_ManPrintStats( pAig );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAig ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAig ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAig ) - Saig_ManPiNum( pAig ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAig ) - Saig_ManPoNum( pAig ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAig ) );
    printf("\n*******************************************************\n");
#endif

    c = Extra_UtilGetopt( argc, argv, "1" );
    if( c == '1' )
        pAigNew = LivenessToSafetyTransformationOneStepLoopSim( pNtk, pAig, vLive, vFair );
    else
        pAigNew = LivenessToSafetyTransformationSim( pNtk, pAig, vLive, vFair );
    
#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 );

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

    //Saig_ManForEachPi( pAigNew, pObj, i )
    //    printf("Name of %d-th Pi = %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) );

    //Saig_ManForEachLo( pAigNew, pObj, i )
    //    printf("Name of %d-th Lo = %s\n", i, retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) );

    //printVecPtrOfString( vecPiNames );
    //printVecPtrOfString( vecLoNames );

#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;

}
ABC_NAMESPACE_IMPL_END