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