Integration of the liveness property prover developed by Sayak Ray.

1 files changed, 549 insertions, 0 deletions

diff --git a/src/proof/live/arenaViolation.c b/src/proof/live/arenaViolation.c
new file mode 100644
index 00000000..8f78630b
--- /dev/null
+++ b/src/proof/live/arenaViolation.c
@@ -0,0 +1,549 @@
+/**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