#include <stdio.h>
#include "base/main/main.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include <string.h>

Macros
#define	PROPAGATE_NAMES

Functions
Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///. More...

Abc_Ntk_t *	Abc_NtkFromAigPhase (Aig_Man_t *pMan)

static void	printVecPtrOfString (Vec_Ptr_t *vec)

static int	getPoIndex (Aig_Man_t pAig, Aig_Obj_t pPivot)

static char *	retrieveTruePiName (Abc_Ntk_t pNtkOld, Aig_Man_t pAigOld, Aig_Man_t pAigNew, Aig_Obj_t pObjPivot)

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)

static int	Aig_ManCiCleanupBiere (Aig_Man_t *p)

static int	Aig_ManCoCleanupBiere (Aig_Man_t *p)

static Aig_Man_t *	LivenessToSafetyTransformationSim (Abc_Ntk_t pNtk, Aig_Man_t p, Vec_Ptr_t vLive, Vec_Ptr_t vFair)

static Aig_Man_t *	LivenessToSafetyTransformationOneStepLoopSim (Abc_Ntk_t pNtk, Aig_Man_t p, Vec_Ptr_t vLive, Vec_Ptr_t vFair)

static Vec_Ptr_t *	populateLivenessVector (Abc_Ntk_t pNtk, Aig_Man_t pAig)

static Vec_Ptr_t *	populateFairnessVector (Abc_Ntk_t pNtk, Aig_Man_t pAig)

static void	updateNewNetworkNameManager (Abc_Ntk_t pNtk, Aig_Man_t pAig, Vec_Ptr_t vPiNames, Vec_Ptr_t vLoNames)

int	Abc_CommandAbcLivenessToSafetySim (Abc_Frame_t pAbc, int argc, char *argv)

Variables
Vec_Ptr_t *	vecPis

Vec_Ptr_t *	vecPiNames

Vec_Ptr_t *	vecLos

Vec_Ptr_t *	vecLoNames

Macro Definition Documentation

#define PROPAGATE_NAMES

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

]

Definition at line 30 of file liveness_sim.c.

Function Documentation

int Abc_CommandAbcLivenessToSafetySim	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv
	)

Definition at line 754 of file liveness_sim.c.

 {
     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_Ntk_t* Abc_NtkFromAigPhase ( Aig_Man_t * pMan )

Function*************************************************************

Synopsis [Converts the network from the AIG manager into ABC.]

Description [This procedure should be called after seq sweeping, which changes the number of registers.]

SideEffects []

SeeAlso []

Definition at line 590 of file abcDar.c.

 {
     Vec_Ptr_t * vNodes; 
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObjNew;
     Aig_Obj_t * pObj, * pObjLo, * pObjLi;
     int i; 
     assert( pMan->nAsserts == 0 );
     // perform strashing
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->nConstrs = pMan->nConstrs;
     pNtkNew->nBarBufs = pMan->nBarBufs;
     // duplicate the name and the spec
 //    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
 //    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     // create PIs
     Aig_ManForEachPiSeq( pMan, pObj, i )
     {
         pObjNew = Abc_NtkCreatePi( pNtkNew );
 //        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
         pObj->pData = pObjNew;
     }
     // create POs
     Aig_ManForEachPoSeq( pMan, pObj, i )
     {
         pObjNew = Abc_NtkCreatePo( pNtkNew );
 //        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
         pObj->pData = pObjNew;
     }
     assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
     assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
     // create as many latches as there are registers in the manager
     Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
     {
         pObjNew = Abc_NtkCreateLatch( pNtkNew );
         pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
         pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
         Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
         Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
         Abc_LatchSetInit0( pObjNew );
 //        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
 //        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
     }
     // rebuild the AIG
     vNodes = Aig_ManDfs( pMan, 1 );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         if ( Aig_ObjIsBuf(pObj) )
             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         else
             pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachCo( pMan, pObj, i )
     {
         pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
     }
 
     Abc_NtkAddDummyPiNames( pNtkNew );
     Abc_NtkAddDummyPoNames( pNtkNew );
     Abc_NtkAddDummyBoxNames( pNtkNew );
 
     // check the resulting AIG
     if ( !Abc_NtkCheck( pNtkNew ) )
         Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
     return pNtkNew;
 }

Aig_Man_t* Abc_NtkToDar	(	Abc_Ntk_t *	pNtk,
		int	fExors,
		int	fRegisters
	)

DECLARATIONS ///.

Function*************************************************************

Synopsis [Converts the network from the AIG manager into ABC.]

Description [Assumes that registers are ordered after PIs/POs.]

SideEffects []

SeeAlso []

Definition at line 233 of file abcDar.c.

 {
     Vec_Ptr_t * vNodes;
     Aig_Man_t * pMan;
     Aig_Obj_t * pObjNew;
     Abc_Obj_t * pObj;
     int i, nNodes, nDontCares;
     // make sure the latches follow PIs/POs
     if ( fRegisters ) 
     { 
         assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
         Abc_NtkForEachCi( pNtk, pObj, i )
             if ( i < Abc_NtkPiNum(pNtk) )
             {
                 assert( Abc_ObjIsPi(pObj) );
                 if ( !Abc_ObjIsPi(pObj) )
                     Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
             }
             else
                 assert( Abc_ObjIsBo(pObj) );
         Abc_NtkForEachCo( pNtk, pObj, i )
             if ( i < Abc_NtkPoNum(pNtk) )
             {
                 assert( Abc_ObjIsPo(pObj) );
                 if ( !Abc_ObjIsPo(pObj) )
                     Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
             }
             else
                 assert( Abc_ObjIsBi(pObj) );
         // print warning about initial values
         nDontCares = 0;
         Abc_NtkForEachLatch( pNtk, pObj, i )
             if ( Abc_LatchIsInitDc(pObj) )
             {
                 Abc_LatchSetInit0(pObj);
                 nDontCares++;
             }
         if ( nDontCares )
         {
             Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
             Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
             Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
             Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
         }
     }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     pMan->fCatchExor = fExors;
     pMan->nConstrs = pNtk->nConstrs;
     pMan->nBarBufs = pNtk->nBarBufs;
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
     pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
     {
         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
         // initialize logic level of the CIs
         ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
     }
     // complement the 1-values registers
     if ( fRegisters ) {
         Abc_NtkForEachLatch( pNtk, pObj, i )
             if ( Abc_LatchIsInit1(pObj) )
                 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
     }
     // perform the conversion of the internal nodes (assumes DFS ordering)
 //    pMan->fAddStrash = 1;
     vNodes = Abc_NtkDfs( pNtk, 0 );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
 //    Abc_NtkForEachNode( pNtk, pObj, i )
     {
         pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
 //        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
     }
     Vec_PtrFree( vNodes );
     pMan->fAddStrash = 0;
     // create the POs
     Abc_NtkForEachCo( pNtk, pObj, i )
         Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
     // complement the 1-valued registers
     Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
     if ( fRegisters )
         Aig_ManForEachLiSeq( pMan, pObjNew, i )
             if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                 pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
     // remove dangling nodes
     nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
     if ( !fExors && nNodes )
         Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
 //Aig_ManDumpVerilog( pMan, "test.v" );
     // save the number of registers
     if ( fRegisters )
     {
         Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
         pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
 //        pMan->vFlopNums = NULL;
 //        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
         if ( pNtk->vOnehots )
             pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
     }
     if ( !Aig_ManCheck( pMan ) )
     {
         Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
         Aig_ManStop( pMan );
         return NULL;
     }
     return pMan;
 }

static int Aig_ManCiCleanupBiere ( Aig_Man_t * p )

static

Definition at line 176 of file liveness_sim.c.

 {
     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 )

static

Definition at line 188 of file liveness_sim.c.

 {
     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 int getPoIndex	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pPivot
	)

static

Definition at line 65 of file liveness_sim.c.

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

static Aig_Man_t* LivenessToSafetyTransformationOneStepLoopSim	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	p,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair
	)

static

Definition at line 480 of file liveness_sim.c.

 {
     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 Aig_Man_t* LivenessToSafetyTransformationSim	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	p,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair
	)

static

Definition at line 198 of file liveness_sim.c.

 {
     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 Vec_Ptr_t* populateFairnessVector	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig
	)

static

Definition at line 715 of file liveness_sim.c.

 {
     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 Vec_Ptr_t* populateLivenessVector	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig
	)

static

Definition at line 698 of file liveness_sim.c.

 {
     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 void printVecPtrOfString ( Vec_Ptr_t * vec )

static

Definition at line 55 of file liveness_sim.c.

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

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
	)

static

Definition at line 100 of file liveness_sim.c.

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

static char* retrieveTruePiName	(	Abc_Ntk_t *	pNtkOld,
		Aig_Man_t *	pAigOld,
		Aig_Man_t *	pAigNew,
		Aig_Obj_t *	pObjPivot
	)

static

Definition at line 78 of file liveness_sim.c.

 {
     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 void updateNewNetworkNameManager	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig,
		Vec_Ptr_t *	vPiNames,
		Vec_Ptr_t *	vLoNames
	)

static

Definition at line 732 of file liveness_sim.c.

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

Variable Documentation

Vec_Ptr_t * vecLoNames

Definition at line 219 of file liveness.c.

Vec_Ptr_t* vecLos

Definition at line 219 of file liveness.c.

Vec_Ptr_t * vecPiNames

Definition at line 218 of file liveness.c.

Vec_Ptr_t* vecPis

Definition at line 218 of file liveness.c.

Macros

Functions

Variables

Macro Definition Documentation

Function Documentation

Variable Documentation