abc/src/proof/live/arenaViolation.c - third_party/vtr-verilog-to-routing - Git at Google

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

   FileName    [arenaViolation.c]

   SystemName  [ABC: Logic synthesis and verification system.]

   PackageName [Liveness property checking.]

   Synopsis    [module for addition of arena violator detector
         induced by stabilizing constraints]

   Author      [Sayak Ray]

   Affiliation [UC Berkeley]

   Date        [Ver. 1.0. Started - October 31, 2012.]

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

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

 //#define DISJUNCTIVE_CONSTRAINT_ENABLE_MODE
 #define BARRIER_MONOTONE_TEST

 ABC_NAMESPACE_IMPL_START

 Vec_Ptr_t * createArenaLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers )
 {
     Vec_Ptr_t *vArenaLO;
     int barrierCount;
     Aig_Obj_t *pObj;
     int i;

     if( vBarriers == NULL )
         return NULL;

     barrierCount = Vec_PtrSize(vBarriers);
     if( barrierCount <= 0 )
         return NULL;

     vArenaLO = Vec_PtrAlloc(barrierCount);
     for( i=0; i<barrierCount; i++ )
     {
         pObj = Aig_ObjCreateCi( pAigNew );
         Vec_PtrPush( vArenaLO, pObj );
     }

     return vArenaLO;
 }

 Vec_Ptr_t * createArenaLi( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal )
 {
     Vec_Ptr_t *vArenaLi;
     int barrierCount;
     int i;
     Aig_Obj_t *pObj, *pObjDriver;

     if( vBarriers == NULL )
         return NULL;

     barrierCount = Vec_PtrSize(vBarriers);
     if( barrierCount <= 0 )
         return NULL;

     vArenaLi = Vec_PtrAlloc(barrierCount);
     for( i=0; i<barrierCount; i++ )
     {
         pObjDriver = (Aig_Obj_t *)Vec_PtrEntry( vArenaSignal, i );
         pObj = Aig_ObjCreateCo( pAigNew, pObjDriver );
         Vec_PtrPush( vArenaLi, pObj );
     }

     return vArenaLi;
 }

 Vec_Ptr_t *createMonotoneBarrierLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers )
 {
     Vec_Ptr_t *vMonotoneLO;
     int barrierCount;
     Aig_Obj_t *pObj;
     int i;

     if( vBarriers == NULL )
         return NULL;

     barrierCount = Vec_PtrSize(vBarriers);
     if( barrierCount <= 0 )
         return NULL;

     vMonotoneLO = Vec_PtrAlloc(barrierCount);
     for( i=0; i<barrierCount; i++ )
     {
         pObj = Aig_ObjCreateCi( pAigNew );
         Vec_PtrPush( vMonotoneLO, pObj );
     }

     return vMonotoneLO;
 }

 Aig_Obj_t *driverToPoNew( Aig_Man_t *pAig, Aig_Obj_t *pObjPo )
 {
     Aig_Obj_t *poDriverOld;
     Aig_Obj_t *poDriverNew;

     //Aig_ObjPrint( pAig, pObjPo );
     //printf("\n");

     assert( Aig_ObjIsCo(pObjPo) );
     poDriverOld = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
     assert( !Aig_ObjIsCo(poDriverOld) );
     poDriverNew = !Aig_IsComplement(poDriverOld)?
             (Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData) :
             Aig_Not((Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData));
     //assert( !Aig_ObjIsCo(poDriverNew) );
     return poDriverNew;
 }

 Vec_Ptr_t *collectBarrierDisjunctions(Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
 {
     int barrierCount, i, j, jElem;
     Vec_Int_t *vIthBarrier;
     Aig_Obj_t *pObjBarrier, *pObjCurr, *pObjTargetPoOld;
     Vec_Ptr_t *vNewBarrierSignals;

     if( vBarriers == NULL )
         return NULL;
     barrierCount = Vec_PtrSize( vBarriers );
     if( barrierCount <= 0 )
         return NULL;

     vNewBarrierSignals = Vec_PtrAlloc( barrierCount );

     for( i=0; i<barrierCount; i++ )
     {
         vIthBarrier = (Vec_Int_t *)Vec_PtrEntry( vBarriers, i );
         assert( Vec_IntSize( vIthBarrier ) >= 1 );
         pObjBarrier = Aig_Not(Aig_ManConst1(pAigNew));
         Vec_IntForEachEntry( vIthBarrier, jElem, j )
         {
             pObjTargetPoOld = Aig_ManCo( pAigOld, jElem );
             //Aig_ObjPrint( pAigOld, pObjTargetPoOld );
             //printf("\n");
             pObjCurr = driverToPoNew( pAigOld, pObjTargetPoOld );
             pObjBarrier = Aig_Or( pAigNew, pObjCurr, pObjBarrier );
         }
         assert( pObjBarrier );
         Vec_PtrPush(vNewBarrierSignals, pObjBarrier);
     }
     assert( Vec_PtrSize( vNewBarrierSignals ) == barrierCount );

     return vNewBarrierSignals;
 }

 Aig_Obj_t *Aig_Xor( Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2 )
 {
     return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) );
 }

 Aig_Obj_t *createArenaViolation(
         Aig_Man_t *pAigOld,
         Aig_Man_t *pAigNew,
         Aig_Obj_t *pWindowBegins,
         Aig_Obj_t *pWithinWindow,
         Vec_Ptr_t *vMasterBarriers,
         Vec_Ptr_t *vBarrierLo,
         Vec_Ptr_t *vBarrierLiDriver,
         Vec_Ptr_t *vMonotoneDisjunctionNodes
         )
 {
     Aig_Obj_t *pWindowBeginsLocal = pWindowBegins;
     Aig_Obj_t *pWithinWindowLocal = pWithinWindow;
     int i;
     Aig_Obj_t *pObj, *pObjAnd1, *pObjOr1, *pObjAnd2, *pObjBarrierLo, *pObjBarrierSwitch, *pObjArenaViolation;
     Vec_Ptr_t *vBarrierSignals;

     assert( vBarrierLiDriver != NULL );
     assert( vMonotoneDisjunctionNodes != NULL );

     pObjArenaViolation = Aig_Not(Aig_ManConst1( pAigNew ));

     vBarrierSignals = collectBarrierDisjunctions(pAigOld, pAigNew, vMasterBarriers);
     assert( vBarrierSignals != NULL );

     assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == 0 );
     Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
         Vec_PtrPush( vMonotoneDisjunctionNodes, pObj );
     assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == Vec_PtrSize( vMasterBarriers ) );

     Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
     {
         //pObjNew = driverToPoNew( pAigOld, pObj );
         pObjAnd1 = Aig_And(pAigNew, pObj, pWindowBeginsLocal);
         pObjBarrierLo = (Aig_Obj_t *)Vec_PtrEntry( vBarrierLo, i );
         pObjOr1 = Aig_Or(pAigNew, pObjAnd1, pObjBarrierLo);
         Vec_PtrPush( vBarrierLiDriver, pObjOr1 );

         pObjBarrierSwitch = Aig_Xor( pAigNew, pObj, pObjBarrierLo );
         pObjAnd2 = Aig_And( pAigNew, pObjBarrierSwitch, pWithinWindowLocal );
         pObjArenaViolation = Aig_Or( pAigNew, pObjAnd2, pObjArenaViolation );
     }

     Vec_PtrFree(vBarrierSignals);
     return pObjArenaViolation;
 }

 Aig_Obj_t *createConstrained0LiveConeWithDSC( Aig_Man_t *pNewAig, Vec_Ptr_t *signalList )
 {
     Aig_Obj_t *pConsequent, *pConsequentCopy, *pAntecedent, *p0LiveCone, *pObj;
     int i, numSigAntecedent;

     numSigAntecedent = Vec_PtrSize( signalList ) - 1;

     pAntecedent = Aig_ManConst1( pNewAig );
     pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent );
     pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) );

     for(i=0; i<numSigAntecedent; i++ )
     {
         pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i );
         assert( Aig_Regular(pObj)->pData );
         pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) );
     }

     p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy );

     return p0LiveCone;
 }

 Vec_Ptr_t *collectCSSignalsWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
 {
     int i;
     Aig_Obj_t *pObj, *pConsequent = NULL;
     Vec_Ptr_t *vNodeArray;

     vNodeArray = Vec_PtrAlloc(1);

     Saig_ManForEachPo( pAig, pObj, i )
     {
         if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL )
             Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) );
         else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL )
             pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
     }
     assert( pConsequent );
     Vec_PtrPush( vNodeArray, pConsequent );
     return vNodeArray;
 }

 int collectWindowBeginSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
 {
     int i;
     Aig_Obj_t *pObj;

     Saig_ManForEachPo( pAig, pObj, i )
     {
         if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "windowBegins_" ) != NULL )
         {
             return i;
         }
     }

     return -1;
 }

 int collectWithinWindowSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
 {
     int i;
     Aig_Obj_t *pObj;

     Saig_ManForEachPo( pAig, pObj, i )
     {
         if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "withinWindow_" ) != NULL )
             return i;
     }

     return -1;
 }

 int collectPendingSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
 {
     int i;
     Aig_Obj_t *pObj;

     Saig_ManForEachPo( pAig, pObj, i )
     {
         if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "pendingSignal" ) != NULL )
             return i;
     }

     return -1;
 }

 Aig_Obj_t *createAndGateForMonotonicityVerification(
                 Aig_Man_t *pNewAig,
                 Vec_Ptr_t *vDisjunctionSignals,
                 Vec_Ptr_t *vDisjunctionLo,
                 Aig_Obj_t *pendingLo,
                 Aig_Obj_t *pendingSignal
                 )
 {
     Aig_Obj_t *pObjBigAnd, *pObj, *pObjLo, *pObjImply;
     Aig_Obj_t *pObjPendingAndPendingLo;
     int i;

     pObjBigAnd = Aig_ManConst1( pNewAig );
     pObjPendingAndPendingLo = Aig_And( pNewAig, pendingLo, pendingSignal );
     Vec_PtrForEachEntry( Aig_Obj_t *, vDisjunctionSignals, pObj, i )
     {
         pObjLo = (Aig_Obj_t *)Vec_PtrEntry( vDisjunctionLo, i );
         pObjImply = Aig_Or( pNewAig, Aig_Not(Aig_And( pNewAig, pObjPendingAndPendingLo, pObjLo)),
                     pObj );
         pObjBigAnd = Aig_And( pNewAig, pObjBigAnd, pObjImply );
     }
     return pObjBigAnd;
 }

 Aig_Man_t *createNewAigWith0LivePoWithDSC( Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers )
 {
     Aig_Man_t *pNewAig;
     Aig_Obj_t *pObj, *pObjNewPoDriver;
     int i;
     int loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0;
     Aig_Obj_t *pObjWindowBeginsNew, *pObjWithinWindowNew, *pObjArenaViolation, *pObjTarget, *pObjArenaViolationLiDriver;
     Aig_Obj_t *pObjNewPoDriverArenaViolated, *pObjArenaViolationLo;
     Vec_Ptr_t *vBarrierLo, *vBarrierLiDriver, *vBarrierLi;
     Vec_Ptr_t *vMonotoneNodes;

 #ifdef BARRIER_MONOTONE_TEST
     Aig_Obj_t *pObjPendingSignal;
     Aig_Obj_t *pObjPendingFlopLo;
     Vec_Ptr_t *vMonotoneBarrierLo;
     Aig_Obj_t *pObjPendingAndPendingSignal, *pObjMonotoneAnd, *pObjCurrMonotoneLo;
 #endif

     //assert( Vec_PtrSize( signalList ) > 1 );

     //****************************************************************
     // 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
     //****************************************************************
     pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
     pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_0Live") + 1 );
     sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live");
         pNewAig->pSpec = NULL;

     //****************************************************************
     // Step 2: map constant nodes
     //****************************************************************
         pObj = Aig_ManConst1( pAig );
         pObj->pData = Aig_ManConst1( pNewAig );

     //****************************************************************
         // Step 3: create true PIs
     //****************************************************************
         Saig_ManForEachPi( pAig, pObj, i )
     {
         pObj->pData = Aig_ObjCreateCi( pNewAig );
     }

     //****************************************************************
     // Step 4: create register outputs
     //****************************************************************
         Saig_ManForEachLo( pAig, pObj, i )
         {
         loCopied++;
         pObj->pData = Aig_ObjCreateCi( pNewAig );
         }

     //****************************************************************
     // Step 4.a: create register outputs for the barrier flops
     //****************************************************************
     vBarrierLo = createArenaLO( pNewAig, vBarriers );
     loCreated = Vec_PtrSize(vBarrierLo);

     //****************************************************************
     // Step 4.b: create register output for arenaViolationFlop
     //****************************************************************
     pObjArenaViolationLo = Aig_ObjCreateCi( pNewAig );
     loCreated++;

 #ifdef BARRIER_MONOTONE_TEST
     //****************************************************************
     // Step 4.c: create register output for pendingFlop
     //****************************************************************
     pObjPendingFlopLo = Aig_ObjCreateCi( pNewAig );
     loCreated++;

     //****************************************************************
     // Step 4.d: create register outputs for the barrier flops
     // for asserting monotonicity
     //****************************************************************
     vMonotoneBarrierLo = createMonotoneBarrierLO( pNewAig, vBarriers );
     loCreated = loCreated + Vec_PtrSize(vMonotoneBarrierLo);
 #endif

     //********************************************************************
     // Step 5: create internal nodes
     //********************************************************************
         Aig_ManForEachNode( pAig, pObj, i )
     {
         pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     }

     //********************************************************************
     // Step 5.a: create internal nodes corresponding to arenaViolation
     //********************************************************************
     pObjTarget = Aig_ManCo( pAig, windowBeginIndex );
     pObjWindowBeginsNew = driverToPoNew( pAig, pObjTarget );

     pObjTarget = Aig_ManCo( pAig, withinWindowIndex );
     pObjWithinWindowNew = driverToPoNew( pAig, pObjTarget );

     vBarrierLiDriver = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
     vMonotoneNodes = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );

     pObjArenaViolation = createArenaViolation( pAig, pNewAig,
                 pObjWindowBeginsNew, pObjWithinWindowNew,
                 vBarriers, vBarrierLo, vBarrierLiDriver, vMonotoneNodes );
     assert( Vec_PtrSize(vMonotoneNodes) == Vec_PtrSize(vBarriers) );

 #ifdef ARENA_VIOLATION_CONSTRAINT

 #endif

     pObjArenaViolationLiDriver = Aig_Or( pNewAig, pObjArenaViolation, pObjArenaViolationLo );

 #ifdef BARRIER_MONOTONE_TEST
     //********************************************************************
     // Step 5.b: Create internal nodes for monotone testing
     //********************************************************************

     pObjTarget = Aig_ManCo( pAig, pendingSignalIndex );
     pObjPendingSignal = driverToPoNew( pAig, pObjTarget );

     pObjPendingAndPendingSignal = Aig_And( pNewAig, pObjPendingSignal, pObjPendingFlopLo );
     pObjMonotoneAnd = Aig_ManConst1( pNewAig );
     Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
     {
         pObjCurrMonotoneLo = (Aig_Obj_t *)Vec_PtrEntry(vMonotoneBarrierLo, i);
         pObjMonotoneAnd = Aig_And( pNewAig, pObjMonotoneAnd,
             Aig_Or( pNewAig,
             Aig_Not(Aig_And(pNewAig, pObjPendingAndPendingSignal, pObjCurrMonotoneLo)),
             pObj ) );
     }
 #endif

     //********************************************************************
     // Step 6: create primary outputs
     //********************************************************************

     Saig_ManForEachPo( pAig, pObj, i )
     {
         pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
     }

     pObjNewPoDriver = createConstrained0LiveConeWithDSC( pNewAig, signalList );
     pObjNewPoDriverArenaViolated = Aig_Or( pNewAig, pObjNewPoDriver, pObjArenaViolationLo );
 #ifdef BARRIER_MONOTONE_TEST
     pObjNewPoDriverArenaViolated = Aig_And( pNewAig, pObjNewPoDriverArenaViolated, pObjMonotoneAnd );
 #endif
     Aig_ObjCreateCo( pNewAig, pObjNewPoDriverArenaViolated );

     *index0Live = i;

     //********************************************************************
     // Step 7: create register inputs
     //********************************************************************

     Saig_ManForEachLi( pAig, pObj, i )
     {
         liCopied++;
         pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
     }

     //********************************************************************
     // Step 7.a: create register inputs for barrier flops
     //********************************************************************
     assert( Vec_PtrSize(vBarrierLiDriver) == Vec_PtrSize(vBarriers) );
     vBarrierLi = createArenaLi( pNewAig, vBarriers, vBarrierLiDriver );
     liCreated = Vec_PtrSize( vBarrierLi );

     //********************************************************************
     // Step 7.b: create register inputs for arenaViolation flop
     //********************************************************************
     Aig_ObjCreateCo( pNewAig, pObjArenaViolationLiDriver );
     liCreated++;

 #ifdef BARRIER_MONOTONE_TEST
     //****************************************************************
     // Step 7.c: create register input for pendingFlop
     //****************************************************************
     Aig_ObjCreateCo( pNewAig, pObjPendingSignal);
     liCreated++;

     //********************************************************************
     // Step 7.d: create register inputs for the barrier flops
     // for asserting monotonicity
     //********************************************************************
     Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
     {
         Aig_ObjCreateCo( pNewAig, pObj );
         liCreated++;
     }
 #endif

     assert(loCopied + loCreated == liCopied + liCreated);
     //next step should be changed
     Aig_ManSetRegNum( pNewAig, loCopied + loCreated );
     Aig_ManCleanup( pNewAig );

     assert( Aig_ManCheck( pNewAig ) );

     Vec_PtrFree(vBarrierLo);
     Vec_PtrFree(vMonotoneBarrierLo);
     Vec_PtrFree(vBarrierLiDriver);
     Vec_PtrFree(vBarrierLi);
     Vec_PtrFree(vMonotoneNodes);

     return pNewAig;
 }

 Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers )
 {
     Vec_Ptr_t *vSignalVector;
     Aig_Man_t *pAigNew;
     int pObjWithinWindow;
     int pObjWindowBegin;
     int pObjPendingSignal;

     vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );

     pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
     pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
     pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );

     pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
     Vec_PtrFree(vSignalVector);

     return pAigNew;
 }

 ABC_NAMESPACE_IMPL_END
	/CFile**************************************************************

	FileName [arenaViolation.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [Liveness property checking.]

	Synopsis [module for addition of arena violator detector
	induced by stabilizing constraints]

	Author [Sayak Ray]

	Affiliation [UC Berkeley]

	Date [Ver. 1.0. Started - October 31, 2012.]

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

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

	//#define DISJUNCTIVE_CONSTRAINT_ENABLE_MODE
	#define BARRIER_MONOTONE_TEST

	ABC_NAMESPACE_IMPL_START

	Vec_Ptr_t * createArenaLO( Aig_Man_t pAigNew, Vec_Ptr_t vBarriers )
	{
	Vec_Ptr_t *vArenaLO;
	int barrierCount;
	Aig_Obj_t *pObj;
	int i;

	if( vBarriers == NULL )
	return NULL;

	barrierCount = Vec_PtrSize(vBarriers);
	if( barrierCount <= 0 )
	return NULL;

	vArenaLO = Vec_PtrAlloc(barrierCount);
	for( i=0; i<barrierCount; i++ )
	{
	pObj = Aig_ObjCreateCi( pAigNew );
	Vec_PtrPush( vArenaLO, pObj );
	}

	return vArenaLO;
	}

	Vec_Ptr_t * createArenaLi( Aig_Man_t pAigNew, Vec_Ptr_t vBarriers, Vec_Ptr_t *vArenaSignal )
	{
	Vec_Ptr_t *vArenaLi;
	int barrierCount;
	int i;
	Aig_Obj_t pObj, pObjDriver;

	if( vBarriers == NULL )
	return NULL;

	barrierCount = Vec_PtrSize(vBarriers);
	if( barrierCount <= 0 )
	return NULL;

	vArenaLi = Vec_PtrAlloc(barrierCount);
	for( i=0; i<barrierCount; i++ )
	{
	pObjDriver = (Aig_Obj_t *)Vec_PtrEntry( vArenaSignal, i );
	pObj = Aig_ObjCreateCo( pAigNew, pObjDriver );
	Vec_PtrPush( vArenaLi, pObj );
	}

	return vArenaLi;
	}

	Vec_Ptr_t createMonotoneBarrierLO( Aig_Man_t pAigNew, Vec_Ptr_t *vBarriers )
	{
	Vec_Ptr_t *vMonotoneLO;
	int barrierCount;
	Aig_Obj_t *pObj;
	int i;

	if( vBarriers == NULL )
	return NULL;

	barrierCount = Vec_PtrSize(vBarriers);
	if( barrierCount <= 0 )
	return NULL;

	vMonotoneLO = Vec_PtrAlloc(barrierCount);
	for( i=0; i<barrierCount; i++ )
	{
	pObj = Aig_ObjCreateCi( pAigNew );
	Vec_PtrPush( vMonotoneLO, pObj );
	}

	return vMonotoneLO;
	}

	Aig_Obj_t driverToPoNew( Aig_Man_t pAig, Aig_Obj_t *pObjPo )
	{
	Aig_Obj_t *poDriverOld;
	Aig_Obj_t *poDriverNew;

	//Aig_ObjPrint( pAig, pObjPo );
	//printf("\n");

	assert( Aig_ObjIsCo(pObjPo) );
	poDriverOld = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
	assert( !Aig_ObjIsCo(poDriverOld) );
	poDriverNew = !Aig_IsComplement(poDriverOld)?
	(Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData) :
	Aig_Not((Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData));
	//assert( !Aig_ObjIsCo(poDriverNew) );
	return poDriverNew;
	}

	Vec_Ptr_t collectBarrierDisjunctions(Aig_Man_t pAigOld, Aig_Man_t pAigNew, Vec_Ptr_t vBarriers)
	{
	int barrierCount, i, j, jElem;
	Vec_Int_t *vIthBarrier;
	Aig_Obj_t pObjBarrier, pObjCurr, *pObjTargetPoOld;
	Vec_Ptr_t *vNewBarrierSignals;

	if( vBarriers == NULL )
	return NULL;
	barrierCount = Vec_PtrSize( vBarriers );
	if( barrierCount <= 0 )
	return NULL;

	vNewBarrierSignals = Vec_PtrAlloc( barrierCount );

	for( i=0; i<barrierCount; i++ )
	{
	vIthBarrier = (Vec_Int_t *)Vec_PtrEntry( vBarriers, i );
	assert( Vec_IntSize( vIthBarrier ) >= 1 );
	pObjBarrier = Aig_Not(Aig_ManConst1(pAigNew));
	Vec_IntForEachEntry( vIthBarrier, jElem, j )
	{
	pObjTargetPoOld = Aig_ManCo( pAigOld, jElem );
	//Aig_ObjPrint( pAigOld, pObjTargetPoOld );
	//printf("\n");
	pObjCurr = driverToPoNew( pAigOld, pObjTargetPoOld );
	pObjBarrier = Aig_Or( pAigNew, pObjCurr, pObjBarrier );
	}
	assert( pObjBarrier );
	Vec_PtrPush(vNewBarrierSignals, pObjBarrier);
	}
	assert( Vec_PtrSize( vNewBarrierSignals ) == barrierCount );

	return vNewBarrierSignals;
	}

	Aig_Obj_t Aig_Xor( Aig_Man_t pAig, Aig_Obj_t pObj1, Aig_Obj_t pObj2 )
	{
	return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) );
	}

	Aig_Obj_t *createArenaViolation(
	Aig_Man_t *pAigOld,
	Aig_Man_t *pAigNew,
	Aig_Obj_t *pWindowBegins,
	Aig_Obj_t *pWithinWindow,
	Vec_Ptr_t *vMasterBarriers,
	Vec_Ptr_t *vBarrierLo,
	Vec_Ptr_t *vBarrierLiDriver,
	Vec_Ptr_t *vMonotoneDisjunctionNodes
	)
	{
	Aig_Obj_t *pWindowBeginsLocal = pWindowBegins;
	Aig_Obj_t *pWithinWindowLocal = pWithinWindow;
	int i;
	Aig_Obj_t pObj, pObjAnd1, pObjOr1, pObjAnd2, pObjBarrierLo, pObjBarrierSwitch, *pObjArenaViolation;
	Vec_Ptr_t *vBarrierSignals;

	assert( vBarrierLiDriver != NULL );
	assert( vMonotoneDisjunctionNodes != NULL );

	pObjArenaViolation = Aig_Not(Aig_ManConst1( pAigNew ));

	vBarrierSignals = collectBarrierDisjunctions(pAigOld, pAigNew, vMasterBarriers);
	assert( vBarrierSignals != NULL );

	assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == 0 );
	Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
	Vec_PtrPush( vMonotoneDisjunctionNodes, pObj );
	assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == Vec_PtrSize( vMasterBarriers ) );

	Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
	{
	//pObjNew = driverToPoNew( pAigOld, pObj );
	pObjAnd1 = Aig_And(pAigNew, pObj, pWindowBeginsLocal);
	pObjBarrierLo = (Aig_Obj_t *)Vec_PtrEntry( vBarrierLo, i );
	pObjOr1 = Aig_Or(pAigNew, pObjAnd1, pObjBarrierLo);
	Vec_PtrPush( vBarrierLiDriver, pObjOr1 );

	pObjBarrierSwitch = Aig_Xor( pAigNew, pObj, pObjBarrierLo );
	pObjAnd2 = Aig_And( pAigNew, pObjBarrierSwitch, pWithinWindowLocal );
	pObjArenaViolation = Aig_Or( pAigNew, pObjAnd2, pObjArenaViolation );
	}

	Vec_PtrFree(vBarrierSignals);
	return pObjArenaViolation;
	}

	Aig_Obj_t createConstrained0LiveConeWithDSC( Aig_Man_t pNewAig, Vec_Ptr_t *signalList )
	{
	Aig_Obj_t pConsequent, pConsequentCopy, pAntecedent, p0LiveCone, *pObj;
	int i, numSigAntecedent;

	numSigAntecedent = Vec_PtrSize( signalList ) - 1;

	pAntecedent = Aig_ManConst1( pNewAig );
	pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent );
	pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) );

	for(i=0; i<numSigAntecedent; i++ )
	{
	pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i );
	assert( Aig_Regular(pObj)->pData );
	pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) );
	}

	p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy );

	return p0LiveCone;
	}

	Vec_Ptr_t collectCSSignalsWithDSC( Abc_Ntk_t pNtk, Aig_Man_t *pAig )
	{
	int i;
	Aig_Obj_t pObj, pConsequent = NULL;
	Vec_Ptr_t *vNodeArray;

	vNodeArray = Vec_PtrAlloc(1);

	Saig_ManForEachPo( pAig, pObj, i )
	{
	if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL )
	Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) );
	else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL )
	pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
	}
	assert( pConsequent );
	Vec_PtrPush( vNodeArray, pConsequent );
	return vNodeArray;
	}

	int collectWindowBeginSignalWithDSC( Abc_Ntk_t pNtk, Aig_Man_t pAig )
	{
	int i;
	Aig_Obj_t *pObj;

	Saig_ManForEachPo( pAig, pObj, i )
	{
	if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "windowBegins_" ) != NULL )
	{
	return i;
	}
	}

	return -1;
	}

	int collectWithinWindowSignalWithDSC( Abc_Ntk_t pNtk, Aig_Man_t pAig )
	{
	int i;
	Aig_Obj_t *pObj;

	Saig_ManForEachPo( pAig, pObj, i )
	{
	if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "withinWindow_" ) != NULL )
	return i;
	}

	return -1;
	}

	int collectPendingSignalWithDSC( Abc_Ntk_t pNtk, Aig_Man_t pAig )
	{
	int i;
	Aig_Obj_t *pObj;

	Saig_ManForEachPo( pAig, pObj, i )
	{
	if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "pendingSignal" ) != NULL )
	return i;
	}

	return -1;
	}

	Aig_Obj_t *createAndGateForMonotonicityVerification(
	Aig_Man_t *pNewAig,
	Vec_Ptr_t *vDisjunctionSignals,
	Vec_Ptr_t *vDisjunctionLo,
	Aig_Obj_t *pendingLo,
	Aig_Obj_t *pendingSignal
	)
	{
	Aig_Obj_t pObjBigAnd, pObj, pObjLo, pObjImply;
	Aig_Obj_t *pObjPendingAndPendingLo;
	int i;

	pObjBigAnd = Aig_ManConst1( pNewAig );
	pObjPendingAndPendingLo = Aig_And( pNewAig, pendingLo, pendingSignal );
	Vec_PtrForEachEntry( Aig_Obj_t *, vDisjunctionSignals, pObj, i )
	{
	pObjLo = (Aig_Obj_t *)Vec_PtrEntry( vDisjunctionLo, i );
	pObjImply = Aig_Or( pNewAig, Aig_Not(Aig_And( pNewAig, pObjPendingAndPendingLo, pObjLo)),
	pObj );
	pObjBigAnd = Aig_And( pNewAig, pObjBigAnd, pObjImply );
	}
	return pObjBigAnd;
	}

	Aig_Man_t createNewAigWith0LivePoWithDSC( Aig_Man_t pAig, Vec_Ptr_t signalList, int index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers )
	{
	Aig_Man_t *pNewAig;
	Aig_Obj_t pObj, pObjNewPoDriver;
	int i;
	int loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0;
	Aig_Obj_t pObjWindowBeginsNew, pObjWithinWindowNew, pObjArenaViolation, pObjTarget, *pObjArenaViolationLiDriver;
	Aig_Obj_t pObjNewPoDriverArenaViolated, pObjArenaViolationLo;
	Vec_Ptr_t vBarrierLo, vBarrierLiDriver, *vBarrierLi;
	Vec_Ptr_t *vMonotoneNodes;

	#ifdef BARRIER_MONOTONE_TEST
	Aig_Obj_t *pObjPendingSignal;
	Aig_Obj_t *pObjPendingFlopLo;
	Vec_Ptr_t *vMonotoneBarrierLo;
	Aig_Obj_t pObjPendingAndPendingSignal, pObjMonotoneAnd, *pObjCurrMonotoneLo;
	#endif

	//assert( Vec_PtrSize( signalList ) > 1 );

	//****************************************************************
	// 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
	//****************************************************************
	pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
	pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_0Live") + 1 );
	sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live");
	pNewAig->pSpec = NULL;

	//****************************************************************
	// Step 2: map constant nodes
	//****************************************************************
	pObj = Aig_ManConst1( pAig );
	pObj->pData = Aig_ManConst1( pNewAig );

	//****************************************************************
	// Step 3: create true PIs
	//****************************************************************
	Saig_ManForEachPi( pAig, pObj, i )
	{
	pObj->pData = Aig_ObjCreateCi( pNewAig );
	}

	//****************************************************************
	// Step 4: create register outputs
	//****************************************************************
	Saig_ManForEachLo( pAig, pObj, i )
	{
	loCopied++;
	pObj->pData = Aig_ObjCreateCi( pNewAig );
	}

	//****************************************************************
	// Step 4.a: create register outputs for the barrier flops
	//****************************************************************
	vBarrierLo = createArenaLO( pNewAig, vBarriers );
	loCreated = Vec_PtrSize(vBarrierLo);

	//****************************************************************
	// Step 4.b: create register output for arenaViolationFlop
	//****************************************************************
	pObjArenaViolationLo = Aig_ObjCreateCi( pNewAig );
	loCreated++;

	#ifdef BARRIER_MONOTONE_TEST
	//****************************************************************
	// Step 4.c: create register output for pendingFlop
	//****************************************************************
	pObjPendingFlopLo = Aig_ObjCreateCi( pNewAig );
	loCreated++;

	//****************************************************************
	// Step 4.d: create register outputs for the barrier flops
	// for asserting monotonicity
	//****************************************************************
	vMonotoneBarrierLo = createMonotoneBarrierLO( pNewAig, vBarriers );
	loCreated = loCreated + Vec_PtrSize(vMonotoneBarrierLo);
	#endif

	//********************************************************************
	// Step 5: create internal nodes
	//********************************************************************
	Aig_ManForEachNode( pAig, pObj, i )
	{
	pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
	}

	//********************************************************************
	// Step 5.a: create internal nodes corresponding to arenaViolation
	//********************************************************************
	pObjTarget = Aig_ManCo( pAig, windowBeginIndex );
	pObjWindowBeginsNew = driverToPoNew( pAig, pObjTarget );

	pObjTarget = Aig_ManCo( pAig, withinWindowIndex );
	pObjWithinWindowNew = driverToPoNew( pAig, pObjTarget );

	vBarrierLiDriver = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
	vMonotoneNodes = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );

	pObjArenaViolation = createArenaViolation( pAig, pNewAig,
	pObjWindowBeginsNew, pObjWithinWindowNew,
	vBarriers, vBarrierLo, vBarrierLiDriver, vMonotoneNodes );
	assert( Vec_PtrSize(vMonotoneNodes) == Vec_PtrSize(vBarriers) );

	#ifdef ARENA_VIOLATION_CONSTRAINT

	#endif

	pObjArenaViolationLiDriver = Aig_Or( pNewAig, pObjArenaViolation, pObjArenaViolationLo );

	#ifdef BARRIER_MONOTONE_TEST
	//********************************************************************
	// Step 5.b: Create internal nodes for monotone testing
	//********************************************************************

	pObjTarget = Aig_ManCo( pAig, pendingSignalIndex );
	pObjPendingSignal = driverToPoNew( pAig, pObjTarget );

	pObjPendingAndPendingSignal = Aig_And( pNewAig, pObjPendingSignal, pObjPendingFlopLo );
	pObjMonotoneAnd = Aig_ManConst1( pNewAig );
	Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
	{
	pObjCurrMonotoneLo = (Aig_Obj_t *)Vec_PtrEntry(vMonotoneBarrierLo, i);
	pObjMonotoneAnd = Aig_And( pNewAig, pObjMonotoneAnd,
	Aig_Or( pNewAig,
	Aig_Not(Aig_And(pNewAig, pObjPendingAndPendingSignal, pObjCurrMonotoneLo)),
	pObj ) );
	}
	#endif

	//********************************************************************
	// Step 6: create primary outputs
	//********************************************************************

	Saig_ManForEachPo( pAig, pObj, i )
	{
	pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
	}

	pObjNewPoDriver = createConstrained0LiveConeWithDSC( pNewAig, signalList );
	pObjNewPoDriverArenaViolated = Aig_Or( pNewAig, pObjNewPoDriver, pObjArenaViolationLo );
	#ifdef BARRIER_MONOTONE_TEST
	pObjNewPoDriverArenaViolated = Aig_And( pNewAig, pObjNewPoDriverArenaViolated, pObjMonotoneAnd );
	#endif
	Aig_ObjCreateCo( pNewAig, pObjNewPoDriverArenaViolated );

	*index0Live = i;

	//********************************************************************
	// Step 7: create register inputs
	//********************************************************************

	Saig_ManForEachLi( pAig, pObj, i )
	{
	liCopied++;
	pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
	}

	//********************************************************************
	// Step 7.a: create register inputs for barrier flops
	//********************************************************************
	assert( Vec_PtrSize(vBarrierLiDriver) == Vec_PtrSize(vBarriers) );
	vBarrierLi = createArenaLi( pNewAig, vBarriers, vBarrierLiDriver );
	liCreated = Vec_PtrSize( vBarrierLi );

	//********************************************************************
	// Step 7.b: create register inputs for arenaViolation flop
	//********************************************************************
	Aig_ObjCreateCo( pNewAig, pObjArenaViolationLiDriver );
	liCreated++;

	#ifdef BARRIER_MONOTONE_TEST
	//****************************************************************
	// Step 7.c: create register input for pendingFlop
	//****************************************************************
	Aig_ObjCreateCo( pNewAig, pObjPendingSignal);
	liCreated++;

	//********************************************************************
	// Step 7.d: create register inputs for the barrier flops
	// for asserting monotonicity
	//********************************************************************
	Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
	{
	Aig_ObjCreateCo( pNewAig, pObj );
	liCreated++;
	}
	#endif

	assert(loCopied + loCreated == liCopied + liCreated);
	//next step should be changed
	Aig_ManSetRegNum( pNewAig, loCopied + loCreated );
	Aig_ManCleanup( pNewAig );

	assert( Aig_ManCheck( pNewAig ) );

	Vec_PtrFree(vBarrierLo);
	Vec_PtrFree(vMonotoneBarrierLo);
	Vec_PtrFree(vBarrierLiDriver);
	Vec_PtrFree(vBarrierLi);
	Vec_PtrFree(vMonotoneNodes);

	return pNewAig;
	}

	Aig_Man_t generateWorkingAigWithDSC( Aig_Man_t pAig, Abc_Ntk_t pNtk, int pIndex0Live, Vec_Ptr_t *vMasterBarriers )
	{
	Vec_Ptr_t *vSignalVector;
	Aig_Man_t *pAigNew;
	int pObjWithinWindow;
	int pObjWindowBegin;
	int pObjPendingSignal;

	vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );

	pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
	pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
	pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );

	pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
	Vec_PtrFree(vSignalVector);

	return pAigNew;
	}

	ABC_NAMESPACE_IMPL_END