Integration of the liveness property prover developed by Sayak Ray.

8 files changed, 3283 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f555bbf8..bef700d3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -402,6 +402,8 @@ static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, cha
 extern int Abc_CommandAbcLivenessToSafety    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv );
 extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv );
+extern int Abc_CommandCS_kLiveness           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+extern int Abc_CommandNChooseK               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
@@ -894,9 +896,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Abstraction",  "&fla_gla",      Abc_CommandAbc9Fla2Gla,      0 );
     Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_fla",      Abc_CommandAbc9Gla2Fla,      0 );
 
-    Cmd_CommandAdd( pAbc, "Liveness",     "l2s",           Abc_CommandAbcLivenessToSafety,           0 );
-    Cmd_CommandAdd( pAbc, "Liveness",     "l2ssim",        Abc_CommandAbcLivenessToSafetySim,        0 );
-    Cmd_CommandAdd( pAbc, "Liveness",     "l3s",           Abc_CommandAbcLivenessToSafetyWithLTL,    0 );
+    Cmd_CommandAdd( pAbc, "Liveness",     "l2s",           Abc_CommandAbcLivenessToSafety,        0 );
+    Cmd_CommandAdd( pAbc, "Liveness",     "l2ssim",        Abc_CommandAbcLivenessToSafetySim,     0 );
+    Cmd_CommandAdd( pAbc, "Liveness",     "l3s",           Abc_CommandAbcLivenessToSafetyWithLTL, 0 );
+    Cmd_CommandAdd( pAbc, "Liveness",     "kcs",           Abc_CommandCS_kLiveness,               0 );
+    Cmd_CommandAdd( pAbc, "Liveness",     "nck",           Abc_CommandNChooseK,                   0 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
 
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
diff --git a/src/proof/live/combination.c b/src/proof/live/combination.c
new file mode 100644
index 00000000..b7e56713
--- /dev/null
+++ b/src/proof/live/combination.c
@@ -0,0 +1,463 @@
+#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"
+#include <time.h>
+
+ABC_NAMESPACE_IMPL_START
+
+long countCombination(long n, long k)
+{
+    assert( n >= k );
+    if( n == k ) return 1;
+    if( k == 1 ) return n;
+    return countCombination( n-1, k-1 ) + countCombination( n-1, k );
+}    
+
+void listCombination(int n, int t)
+{
+    Vec_Int_t *vC;
+    int i, j, combCounter = 0;
+
+    //Initialization
+    vC = Vec_IntAlloc(t+3);
+    for(i=-1; i<t; i++)
+        Vec_IntPush( vC, i );
+    Vec_IntPush( vC, n );
+    Vec_IntPush( vC, 0 );
+
+    while(1)
+    {
+        //visit combination
+        printf("Comb-%3d : ", ++combCounter);
+        for( i=t; i>0; i--)
+            printf("vC[%d] = %d ", i, Vec_IntEntry(vC, i));
+        printf("\n");
+
+        j = 1;
+        while( Vec_IntEntry( vC, j ) + 1 == Vec_IntEntry( vC, j+1 ) )
+        {
+            //printf("\nGochon = %d, %d\n", Vec_IntEntry( vC, j ) + 1, Vec_IntEntry( vC, j+1 ));
+            Vec_IntWriteEntry( vC, j, j-1 );
+            j = j + 1;
+        }
+        if( j > t ) break;
+        Vec_IntWriteEntry( vC, j, Vec_IntEntry( vC, j ) + 1 );
+    }
+    
+    Vec_IntFree(vC);    
+}
+
+int generateCombinatorialStabil( Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, 
+                Vec_Int_t *vCandidateMonotoneSignals_,
+                Vec_Ptr_t *vDisj_nCk_,
+                int combN, int combK )
+{
+    Aig_Obj_t *pObjMonoCand, *pObj;
+    int targetPoIndex;
+
+    //Knuth's Data Strcuture
+    int totalCombination_KNUTH = 0;
+    Vec_Int_t *vC_KNUTH;
+    int i_KNUTH, j_KNUTH;
+
+    //Knuth's Data Structure Initialization
+    vC_KNUTH = Vec_IntAlloc(combK+3);
+    for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++)
+        Vec_IntPush( vC_KNUTH, i_KNUTH );
+    Vec_IntPush( vC_KNUTH, combN );
+    Vec_IntPush( vC_KNUTH, 0 );
+
+    while(1)
+    {
+        totalCombination_KNUTH++;
+        pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew));
+        for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--)
+        {
+            targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH));
+            pObj = Aig_ObjChild0Copy(Aig_ManCo( pAigOld, targetPoIndex ));
+            pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand );
+        }
+        Vec_PtrPush(vDisj_nCk_, pObjMonoCand );
+
+        j_KNUTH = 1;
+        while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
+        {
+            Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
+            j_KNUTH = j_KNUTH + 1;
+        }
+        if( j_KNUTH > combK ) break;
+        Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
+    }
+
+    Vec_IntFree(vC_KNUTH);
+
+    return totalCombination_KNUTH;
+}
+
+int generateCombinatorialStabilExhaust( Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, 
+                Vec_Ptr_t *vDisj_nCk_,
+                int combN, int combK )
+{
+    Aig_Obj_t *pObjMonoCand, *pObj;
+    int targetPoIndex;
+
+    //Knuth's Data Strcuture
+    int totalCombination_KNUTH = 0;
+    Vec_Int_t *vC_KNUTH;
+    int i_KNUTH, j_KNUTH;
+
+    //Knuth's Data Structure Initialization
+    vC_KNUTH = Vec_IntAlloc(combK+3);
+    for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++)
+        Vec_IntPush( vC_KNUTH, i_KNUTH );
+    Vec_IntPush( vC_KNUTH, combN );
+    Vec_IntPush( vC_KNUTH, 0 );
+
+    while(1)
+    {
+        totalCombination_KNUTH++;
+        pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew));
+        for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--)
+        {
+            //targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH));
+            targetPoIndex = Vec_IntEntry(vC_KNUTH, i_KNUTH);
+            pObj = (Aig_Obj_t *)(Aig_ManLo( pAigOld, targetPoIndex )->pData);
+            pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand );
+        }
+        Vec_PtrPush(vDisj_nCk_, pObjMonoCand );
+
+        j_KNUTH = 1;
+        while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
+        {
+            Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
+            j_KNUTH = j_KNUTH + 1;
+        }
+        if( j_KNUTH > combK ) break;
+        Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
+    }
+
+    Vec_IntFree(vC_KNUTH);
+
+    return totalCombination_KNUTH;
+}
+
+Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK )
+{
+    //AIG creation related data structure
+    Aig_Man_t *pNewAig;
+    int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
+    //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
+    int i, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
+    int combN_internal, combK_internal; //, targetPoIndex;
+    long longI, lCombinationCount;
+    //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
+    Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
+    Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
+    Vec_Int_t *vCandidateMonotoneSignals;
+
+    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
+    
+    //Knuth's Data Strcuture
+    //Vec_Int_t *vC_KNUTH;
+    //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
+
+    //Collecting target HINT signals
+    vCandidateMonotoneSignals = findHintOutputs(pNtk);
+    if( vCandidateMonotoneSignals == NULL )
+    {
+        printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
+        combN_internal = 0;
+    }
+    else
+    {
+        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
+        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
+        hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
+        hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
+        combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
+    }
+
+    //combK_internal = combK;
+
+    //Knuth's Data Structure Initialization
+    //vC_KNUTH = Vec_IntAlloc(combK_internal+3);
+    //for(i_KNUTH=-1; i_KNUTH<combK_internal; i_KNUTH++)
+    //    Vec_IntPush( vC_KNUTH, i_KNUTH );
+    //Vec_IntPush( vC_KNUTH, combN_internal );
+    //Vec_IntPush( vC_KNUTH, 0 );
+
+    //Standard AIG duplication begins
+    //Standard AIG Manager Creation
+    pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
+    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
+        pNewAig->pSpec = NULL;
+
+    //Standard Mapping of Constant Nodes
+    pObj = Aig_ManConst1( pAig );
+        pObj->pData = Aig_ManConst1( pNewAig );
+
+    //Standard AIG PI duplication
+    Saig_ManForEachPi( pAig, pObj, i )
+    {
+        piCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+    }
+
+    //Standard AIG LO duplication
+    Saig_ManForEachLo( pAig, pObj, i )
+        {
+        loCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+        }
+
+    //nCk LO creation
+    lCombinationCount = 0;
+    for(combK_internal=1; combK_internal<=combK; combK_internal++)
+        lCombinationCount += countCombination( combN_internal, combK_internal );
+    assert( lCombinationCount > 0 );
+    vLO_nCk = Vec_PtrAlloc(lCombinationCount);
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        loCreated++;
+        pObj = Aig_ObjCreateCi(pNewAig);
+        Vec_PtrPush( vLO_nCk, pObj );
+    }
+
+    //Standard Node duplication
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    
+    //nCk specific logic creation (i.e. nCk number of OR gates)
+    vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
+
+    
+
+    //while(1)
+    //{
+    //    //visit combination
+    //    //printf("Comb-%3d : ", ++combCounter_KNUTH);
+    //    pObjMonoCand = Aig_Not(Aig_ManConst1(pNewAig));
+    //    for( i_KNUTH=combK_internal; i_KNUTH>0; i_KNUTH--)
+    //    {
+    //        //printf("vC[%d] = %d ", i_KNUTH, Vec_IntEntry(vC_KNUTH, i_KNUTH));
+    //        targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntEntry(vC_KNUTH, i_KNUTH));
+    //        pObj = Aig_ObjChild0Copy(Aig_ManCo( pAig, targetPoIndex ));
+    //        pObjMonoCand = Aig_Or( pNewAig, pObj, pObjMonoCand );
+    //    }
+    //    Vec_PtrPush(vDisj_nCk, pObjMonoCand );
+    //    //printf("\n");
+
+    //    j_KNUTH = 1;
+    //    while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
+    //    {
+    //        Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
+    //        j_KNUTH = j_KNUTH + 1;
+    //    }
+    //    if( j_KNUTH > combK_internal ) break;
+    //    Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
+    //}
+    for( combK_internal=1; combK_internal<=combK; combK_internal++ )
+        generateCombinatorialStabil( pNewAig, pAig, vCandidateMonotoneSignals,
+                vDisj_nCk, combN_internal, combK_internal );
+
+
+    //creation of implication logic
+    vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
+        pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
+
+        pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
+        Vec_PtrPush(vPODriver_nCk, pObj);
+    }
+    
+    //Standard PO duplication
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        poCopied++;
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
+    }
+
+    //nCk specific PO creation
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
+    }
+
+    //Standard LI duplication
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        liCopied++;
+        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
+    }
+
+    //nCk specific LI creation
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        liCreated++;
+        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
+    }
+
+    //clean-up, book-keeping
+    assert( liCopied + liCreated == loCopied + loCreated );    
+    nRegCount = loCopied + loCreated;
+
+    Aig_ManSetRegNum( pNewAig, nRegCount );
+    Aig_ManCleanup( pNewAig );
+    assert( Aig_ManCheck( pNewAig ) );
+    
+    //Vec_IntFree(vC_KNUTH);    
+    return pNewAig;
+}
+
+Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK )
+{
+    //AIG creation related data structure
+    Aig_Man_t *pNewAig;
+    int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
+    //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
+    int i, nRegCount;
+    int combN_internal, combK_internal; //, targetPoIndex;
+    long longI, lCombinationCount;
+    //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
+    Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
+    Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
+
+    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
+    
+    //Knuth's Data Strcuture
+    //Vec_Int_t *vC_KNUTH;
+    //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
+
+    //Collecting target HINT signals
+    //vCandidateMonotoneSignals = findHintOutputs(pNtk);
+    //if( vCandidateMonotoneSignals == NULL )
+    //{
+    //    printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
+    //    combN_internal = 0;
+    //}
+    //else
+    //{
+        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
+        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
+    //    hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
+    //    hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
+    //    combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
+    //}
+
+    combN_internal = Aig_ManRegNum(pAig);
+
+    pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
+    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
+        pNewAig->pSpec = NULL;
+
+    //Standard Mapping of Constant Nodes
+    pObj = Aig_ManConst1( pAig );
+        pObj->pData = Aig_ManConst1( pNewAig );
+
+    //Standard AIG PI duplication
+    Saig_ManForEachPi( pAig, pObj, i )
+    {
+        piCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+    }
+
+    //Standard AIG LO duplication
+    Saig_ManForEachLo( pAig, pObj, i )
+        {
+        loCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+        }
+
+    //nCk LO creation
+    lCombinationCount = 0;
+    for(combK_internal=1; combK_internal<=combK; combK_internal++)
+        lCombinationCount += countCombination( combN_internal, combK_internal );
+    assert( lCombinationCount > 0 );
+    vLO_nCk = Vec_PtrAlloc(lCombinationCount);
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        loCreated++;
+        pObj = Aig_ObjCreateCi(pNewAig);
+        Vec_PtrPush( vLO_nCk, pObj );
+    }
+
+    //Standard Node duplication
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    
+    //nCk specific logic creation (i.e. nCk number of OR gates)
+    vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
+
+    for( combK_internal=1; combK_internal<=combK; combK_internal++ )
+    {
+        generateCombinatorialStabilExhaust( pNewAig, pAig,
+                vDisj_nCk, combN_internal, combK_internal );
+    }
+
+
+    //creation of implication logic
+    vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
+        pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
+
+        pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
+        Vec_PtrPush(vPODriver_nCk, pObj);
+    }
+    
+    //Standard PO duplication
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        poCopied++;
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
+    }
+
+    //nCk specific PO creation
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
+    }
+
+    //Standard LI duplication
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        liCopied++;
+        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
+    }
+
+    //nCk specific LI creation
+    for( longI = 0; longI < lCombinationCount; longI++ )
+    {
+        liCreated++;
+        Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
+    }
+
+    //clean-up, book-keeping
+    assert( liCopied + liCreated == loCopied + loCreated );    
+    nRegCount = loCopied + loCreated;
+
+    Aig_ManSetRegNum( pNewAig, nRegCount );
+    Aig_ManCleanup( pNewAig );
+    assert( Aig_ManCheck( pNewAig ) );
+    
+    Vec_PtrFree(vLO_nCk);
+    Vec_PtrFree(vPODriver_nCk);
+    Vec_PtrFree(vDisj_nCk);
+    //Vec_IntFree(vC_KNUTH);    
+    return pNewAig;
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/proof/live/disjunctiveMonotone.c b/src/proof/live/disjunctiveMonotone.c
new file mode 100644
index 00000000..505af774
--- /dev/null
+++ b/src/proof/live/disjunctiveMonotone.c
@@ -0,0 +1,757 @@
+/**CFile****************************************************************
+
+  FileName    [disjunctiveMonotone.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Liveness property checking.]
+
+  Synopsis    [Constraint analysis module for the k-Liveness algorithm
+        invented by Koen Classen, Niklas Sorensson.]
+
+  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"
+#include <time.h>
+
+ABC_NAMESPACE_IMPL_START
+
+struct aigPoIndices
+{
+    int attrPendingSignalIndex;
+    int attrHintSingalBeginningMarker;
+    int attrHintSingalEndMarker;
+    int attrSafetyInvarIndex;
+};
+
+extern struct aigPoIndices *allocAigPoIndices();
+extern void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices);
+extern int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk);
+
+struct antecedentConsequentVectorsStruct
+{
+    Vec_Int_t *attrAntecedents;
+    Vec_Int_t *attrConsequentCandidates;
+};
+
+struct antecedentConsequentVectorsStruct *allocAntecedentConsequentVectorsStruct()
+{
+    struct antecedentConsequentVectorsStruct *newStructure;
+
+    newStructure = (struct antecedentConsequentVectorsStruct *)malloc(sizeof (struct antecedentConsequentVectorsStruct));
+
+    newStructure->attrAntecedents = NULL;
+    newStructure->attrConsequentCandidates = NULL;
+        
+    assert( newStructure != NULL );
+    return newStructure;
+}
+
+void deallocAntecedentConsequentVectorsStruct(struct antecedentConsequentVectorsStruct *toBeDeleted)
+{
+    assert( toBeDeleted != NULL );
+    if(toBeDeleted->attrAntecedents) 
+        Vec_IntFree( toBeDeleted->attrAntecedents );
+    if(toBeDeleted->attrConsequentCandidates)
+        Vec_IntFree( toBeDeleted->attrConsequentCandidates );
+    free( toBeDeleted );
+}
+
+Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, 
+                    struct antecedentConsequentVectorsStruct *anteConseVectors, int *startMonotonePropPo)
+{
+    Aig_Man_t *pNewAig;
+    int iElem, i, nRegCount;
+    int piCopied = 0, liCopied = 0, liCreated = 0, loCopied = 0, loCreated = 0;
+    int poCopied = 0, poCreated = 0;
+    Aig_Obj_t *pObj, *pObjPo, *pObjDriver, *pObjDriverNew, *pObjPendingDriverNew, *pObjPendingAndNextPending;
+    Aig_Obj_t *pPendingFlop, *pObjConseCandFlop, *pObjSafetyInvariantPoDriver;
+    //Vec_Ptr_t *vHintMonotoneLocalDriverNew;
+    Vec_Ptr_t *vConseCandFlopOutput;
+    //Vec_Ptr_t *vHintMonotoneLocalProp;
+
+    Aig_Obj_t *pObjAnteDisjunction, *pObjConsecDriver, *pObjConsecDriverNew, *pObjCandMonotone, *pObjPrevCandMonotone, *pObjMonotonePropDriver;
+    Vec_Ptr_t *vCandMonotoneProp;
+    Vec_Ptr_t *vCandMonotoneFlopInput;
+
+    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
+
+    Vec_Int_t *vAntecedentsLocal = anteConseVectors->attrAntecedents;
+    Vec_Int_t *vConsequentCandidatesLocal = anteConseVectors->attrConsequentCandidates;
+
+    if( vConsequentCandidatesLocal == NULL )
+        return NULL; //no candidates for consequent is provided, hence no need to generate a new AIG
+
+    
+    //****************************************************************
+    // 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("_monotone") + 2 );
+    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "monotone");
+        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 )
+    {
+        piCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+    }
+
+    //****************************************************************
+    // Step 5: create register outputs
+    //****************************************************************
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+        loCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+        }
+
+    //****************************************************************
+    // Step 6: create "D" register output for PENDING flop 
+    //****************************************************************
+    loCreated++;
+    pPendingFlop = Aig_ObjCreateCi( pNewAig );
+
+    //****************************************************************
+    // Step 6.a: create "D" register output for HINT_MONOTONE flop 
+    //****************************************************************
+    vConseCandFlopOutput = Vec_PtrAlloc(Vec_IntSize(vConsequentCandidatesLocal));
+    Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
+    {
+        loCreated++;
+        pObjConseCandFlop = Aig_ObjCreateCi( pNewAig );
+        Vec_PtrPush( vConseCandFlopOutput, pObjConseCandFlop );
+    }
+
+    nRegCount = loCreated + loCopied;
+
+    //********************************************************************
+    // Step 7: create internal nodes
+    //********************************************************************
+        Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    
+    //********************************************************************
+    // Step 8: mapping appropriate new flop drivers 
+    //********************************************************************
+
+    if( aigPoIndicesArg->attrSafetyInvarIndex != -1 )
+    {
+        pObjPo = Aig_ManCo( pAig, aigPoIndicesArg->attrSafetyInvarIndex );
+        pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+        pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
+                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
+                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
+        pObjSafetyInvariantPoDriver = pObjDriverNew;
+    }
+    else
+        pObjSafetyInvariantPoDriver = Aig_ManConst1(pNewAig);
+
+    pObjPo = Aig_ManCo( pAig, pendingSignalIndexLocal );
+    pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+    pObjPendingDriverNew = !Aig_IsComplement(pObjDriver)? 
+                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
+                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
+
+    pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingDriverNew, pPendingFlop );
+
+    pObjAnteDisjunction = Aig_Not(Aig_ManConst1( pNewAig ));
+    if( vAntecedentsLocal )
+    {
+        Vec_IntForEachEntry( vAntecedentsLocal, iElem, i )
+        {
+            pObjPo = Aig_ManCo( pAig, iElem );
+            pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+            pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
+                    (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
+                    Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
+
+            pObjAnteDisjunction = Aig_Or( pNewAig, pObjDriverNew, pObjAnteDisjunction );
+        }
+    }
+
+    vCandMonotoneProp = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
+    vCandMonotoneFlopInput = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
+    Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
+    {
+        pObjPo = Aig_ManCo( pAig, iElem );
+        pObjConsecDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+        pObjConsecDriverNew = !Aig_IsComplement(pObjConsecDriver)? 
+                    (Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData) : 
+                    Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData));
+
+        pObjCandMonotone = Aig_Or( pNewAig, pObjConsecDriverNew, pObjAnteDisjunction );
+        pObjPrevCandMonotone = (Aig_Obj_t *)(Vec_PtrEntry( vConseCandFlopOutput, i ));
+        pObjMonotonePropDriver = Aig_Or( pNewAig, Aig_Not( Aig_And( pNewAig, pObjPendingAndNextPending, pObjPrevCandMonotone ) ), 
+                        pObjCandMonotone );
+
+        //Conjunting safety invar
+        pObjMonotonePropDriver = Aig_And( pNewAig, pObjMonotonePropDriver, pObjSafetyInvariantPoDriver );
+                        
+        Vec_PtrPush( vCandMonotoneFlopInput, pObjCandMonotone );
+        Vec_PtrPush( vCandMonotoneProp, pObjMonotonePropDriver );
+    }
+
+    //********************************************************************
+    // Step 9: create primary outputs 
+    //********************************************************************
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        poCopied++;
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
+    }
+
+    *startMonotonePropPo = i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vCandMonotoneProp, pObj, i )
+    {
+        poCreated++;
+        pObjPo = Aig_ObjCreateCo( pNewAig, pObj ); 
+    }
+
+    //********************************************************************
+    // Step 9: create latch inputs 
+    //********************************************************************
+
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        liCopied++;
+        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
+    }
+    
+    //********************************************************************
+    // Step 9.a: create latch input for PENDING_FLOP
+    //********************************************************************
+
+    liCreated++;
+    Aig_ObjCreateCo( pNewAig, pObjPendingDriverNew );
+
+    //********************************************************************
+    // Step 9.b: create latch input for MONOTONE_FLOP
+    //********************************************************************
+
+    Vec_PtrForEachEntry( Aig_Obj_t *, vCandMonotoneFlopInput, pObj, i )
+    {
+        liCreated++;
+        Aig_ObjCreateCo( pNewAig, pObj );
+    }
+
+    Aig_ManSetRegNum( pNewAig, nRegCount );
+    Aig_ManCleanup( pNewAig );
+    
+    assert( Aig_ManCheck( pNewAig ) );
+    assert( loCopied + loCreated == liCopied + liCreated );
+
+    Vec_PtrFree(vConseCandFlopOutput);
+    Vec_PtrFree(vCandMonotoneProp);
+    Vec_PtrFree(vCandMonotoneFlopInput);
+    return pNewAig;
+}
+
+Vec_Int_t *findNewDisjunctiveMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct antecedentConsequentVectorsStruct *anteConseVectors )
+{
+    Aig_Man_t *pAigNew;
+    Aig_Obj_t *pObjTargetPo;
+    int poMarker;
+    //int i, RetValue, poSerialNum;
+    int i, poSerialNum;
+    Pdr_Par_t Pars, * pPars = &Pars;
+    //Abc_Cex_t * pCex = NULL;
+    Vec_Int_t *vMonotoneIndex;
+    //char fileName[20];
+    Abc_Cex_t * cexElem;
+
+    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
+
+    pAigNew = createDisjunctiveMonotoneTester(pAig, aigPoIndicesArg, anteConseVectors, &poMarker );
+
+    //printf("enter an integer : ");
+    //waitForInteger = getchar();
+    //putchar(waitForInteger);
+
+    vMonotoneIndex = Vec_IntAlloc(0);
+
+    for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
+    {
+        pObjTargetPo = Aig_ManCo( pAigNew, i );
+        Aig_ObjChild0Flip( pObjTargetPo );
+    }
+
+    Pdr_ManSetDefaultParams( pPars );
+    pPars->fVerbose = 0;
+    pPars->fNotVerbose = 1;
+    pPars->fSolveAll = 1;
+    pAigNew->vSeqModelVec = NULL;
+    Pdr_ManSolve( pAigNew, pPars );    
+
+    if( pAigNew->vSeqModelVec )
+    {
+        Vec_PtrForEachEntry( Abc_Cex_t *, pAigNew->vSeqModelVec, cexElem, i )
+        {
+            if( cexElem == NULL  && i >= pendingSignalIndexLocal + 1)
+            {
+                poSerialNum = i - (pendingSignalIndexLocal + 1);
+                Vec_IntPush( vMonotoneIndex, Vec_IntEntry( anteConseVectors->attrConsequentCandidates, poSerialNum ));
+            }
+        }
+    }
+    for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
+    {
+        pObjTargetPo = Aig_ManCo( pAigNew, i );
+        Aig_ObjChild0Flip( pObjTargetPo );
+    }
+    
+    //if(pAigNew->vSeqModelVec)
+    //    Vec_PtrFree(pAigNew->vSeqModelVec);
+
+    Aig_ManStop(pAigNew);
+    
+    if( Vec_IntSize( vMonotoneIndex ) > 0 )
+    {
+        return vMonotoneIndex;
+    }
+    else
+    {
+        Vec_IntFree(vMonotoneIndex);
+        return NULL;
+    }
+}
+
+Vec_Int_t *updateAnteConseVectors(struct antecedentConsequentVectorsStruct *anteConse )
+{
+    Vec_Int_t *vCandMonotone;
+    int iElem, i;
+
+    //if( vKnownMonotone == NULL || Vec_IntSize(vKnownMonotone) <= 0 )
+    //    return vHintMonotone;
+    if( anteConse->attrAntecedents == NULL  || Vec_IntSize(anteConse->attrAntecedents) <= 0 )
+        return anteConse->attrConsequentCandidates;
+    vCandMonotone = Vec_IntAlloc(0);
+    Vec_IntForEachEntry( anteConse->attrConsequentCandidates, iElem, i )
+    {
+        if( Vec_IntFind( anteConse->attrAntecedents, iElem ) == -1 )
+            Vec_IntPush( vCandMonotone, iElem );
+    }
+    
+    return vCandMonotone;
+}
+
+Vec_Int_t *vectorDifference(Vec_Int_t *A, Vec_Int_t *B)
+{
+    Vec_Int_t *C;
+    int iElem, i;
+
+    C = Vec_IntAlloc(0);
+    Vec_IntForEachEntry( A, iElem, i )
+    {
+        if( Vec_IntFind( B, iElem ) == -1 )
+        {
+            Vec_IntPush( C, iElem );
+        }
+    }
+
+    return C;
+}
+
+Vec_Int_t *createSingletonIntVector( int iElem )
+{
+    Vec_Int_t *myVec = Vec_IntAlloc(1);
+    
+    Vec_IntPush(myVec, iElem);
+    return myVec;
+}
+
+#if 0
+Vec_Ptr_t *generateDisjuntiveMonotone_rec()
+{
+    nextLevelSignals = ;
+    if level is not exhausted
+    for all x \in nextLevelSignals
+    {
+        append x in currAntecendent
+        recond it as a monotone predicate
+        resurse with level - 1 
+    }
+}
+#endif
+
+#if 0
+Vec_Ptr_t *generateDisjuntiveMonotoneLevels(Aig_Man_t *pAig, 
+            struct aigPoIndices *aigPoIndicesInstance, 
+            struct antecedentConsequentVectorsStruct *anteConsecInstanceOrig,
+            int level )
+{
+    Vec_Int_t *firstLevelMonotone;
+    Vec_Int_t *currVecInt;
+    Vec_Ptr_t *hierarchyList;
+    int iElem, i;
+
+    assert( level >= 1 );
+    firstLevelMonotone = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
+    if( firstLevelMonotone == NULL || Vec_IntSize(firstLevelMonotone) <= 0 )
+        return NULL;
+    
+    hierarchyList = Vec_PtrAlloc(Vec_IntSize(firstLevelMonotone));
+    
+    Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
+    {
+        currVecInt = createSingletonIntVector( iElem );
+        Vec_PtrPush( hierarchyList, currVecInt );
+    }
+
+    if( level > 1 )
+    {
+        Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
+        {
+            currVecInt = (Vec_Int_t *)Vec_PtrEntry( hierarchyList, i );
+            
+            
+        }
+    }
+
+    return hierarchyList;
+}
+#endif
+
+int Vec_IntPushUniqueLocal( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_IntPush( p, Entry );
+    return 0;
+}
+
+Vec_Ptr_t *findNextLevelDisjunctiveMonotone( 
+        Aig_Man_t *pAig, 
+        struct aigPoIndices *aigPoIndicesInstance, 
+        struct antecedentConsequentVectorsStruct *anteConsecInstance, 
+        Vec_Ptr_t *previousMonotoneVectors )
+{
+    Vec_Ptr_t *newLevelPtrVec;
+    Vec_Int_t *vElem, *vNewDisjunctVector, *newDisjunction;
+    int i, j, iElem;
+    struct antecedentConsequentVectorsStruct *anteConsecInstanceLocal;
+    Vec_Int_t *vUnionPrevMonotoneVector, *vDiffVector;
+
+    newLevelPtrVec = Vec_PtrAlloc(0);
+    vUnionPrevMonotoneVector = Vec_IntAlloc(0);
+    Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
+        Vec_IntForEachEntry( vElem, iElem, j )
+            Vec_IntPushUniqueLocal( vUnionPrevMonotoneVector, iElem );
+
+    Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
+    {
+        anteConsecInstanceLocal = allocAntecedentConsequentVectorsStruct();
+
+        anteConsecInstanceLocal->attrAntecedents = Vec_IntDup(vElem);    
+        vDiffVector = vectorDifference( anteConsecInstance->attrConsequentCandidates, vUnionPrevMonotoneVector);
+        anteConsecInstanceLocal->attrConsequentCandidates = vDiffVector;
+        assert( vDiffVector );
+
+        //printf("Calling target function %d\n", i);
+        vNewDisjunctVector = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstanceLocal );
+
+        if( vNewDisjunctVector )
+        {
+            Vec_IntForEachEntry(vNewDisjunctVector, iElem, j)
+            {
+                newDisjunction = Vec_IntDup(vElem);
+                Vec_IntPush( newDisjunction, iElem );
+                Vec_PtrPush( newLevelPtrVec, newDisjunction );
+            }
+            Vec_IntFree(vNewDisjunctVector);
+        }
+        deallocAntecedentConsequentVectorsStruct( anteConsecInstanceLocal );
+    }
+
+    Vec_IntFree(vUnionPrevMonotoneVector);
+
+    return newLevelPtrVec;
+}
+
+void printAllIntVectors(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
+{
+    Vec_Int_t *vElem;
+    int i, j, iElem;
+    char *name, *hintSubStr;
+    FILE *fp;
+
+    fp = fopen( fileName, "a" );
+
+    Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
+    {    
+        fprintf(fp, "( ");
+        Vec_IntForEachEntry( vElem, iElem, j )
+        {
+            name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
+            hintSubStr = strstr( name, "hint");
+            assert( hintSubStr );
+            fprintf(fp, "%s", hintSubStr);
+            if( j < Vec_IntSize(vElem) - 1 )
+            {
+                fprintf(fp, " || ");
+            }
+            else
+            {
+                fprintf(fp, " )\n");
+            }
+        }
+    }
+    fclose(fp);
+}
+
+void printAllIntVectorsStabil(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
+{
+    Vec_Int_t *vElem;
+    int i, j, iElem;
+    char *name, *hintSubStr;
+    FILE *fp;
+
+    fp = fopen( fileName, "a" );
+
+    Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
+    {    
+        printf("INT[%d] : ( ", i);
+        fprintf(fp, "( ");
+        Vec_IntForEachEntry( vElem, iElem, j )
+        {
+            name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
+            hintSubStr = strstr( name, "csLevel1Stabil");
+            assert( hintSubStr );
+            printf("%s", hintSubStr);
+            fprintf(fp, "%s", hintSubStr);
+            if( j < Vec_IntSize(vElem) - 1 )
+            {
+                printf(" || ");
+                fprintf(fp, " || ");
+            }
+            else
+            {
+                printf(" )\n");
+                fprintf(fp, " )\n");
+            }
+        }
+        //printf(")\n");
+    }
+    fclose(fp);
+}
+
+
+void appendVecToMasterVecInt(Vec_Ptr_t *masterVec, Vec_Ptr_t *candVec )
+{
+    int i;
+    Vec_Int_t *vCand;
+    Vec_Int_t *vNewIntVec;
+
+    assert(masterVec != NULL);
+    assert(candVec != NULL);
+    Vec_PtrForEachEntry( Vec_Int_t *, candVec, vCand, i )
+    {
+        vNewIntVec = Vec_IntDup(vCand);    
+        Vec_PtrPush(masterVec, vNewIntVec);
+    }
+}
+
+void deallocateVecOfIntVec( Vec_Ptr_t *vecOfIntVec )
+{
+    Vec_Int_t *vInt;
+    int i;
+
+    if( vecOfIntVec )
+    {
+        Vec_PtrForEachEntry( Vec_Int_t *, vecOfIntVec, vInt, i )
+        {
+            Vec_IntFree( vInt );
+        }
+        Vec_PtrFree(vecOfIntVec);
+    }    
+}
+
+Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk )
+{
+    Aig_Man_t *pAig;
+    Vec_Int_t *vCandidateMonotoneSignals;
+    Vec_Int_t *vKnownMonotoneSignals;
+    //Vec_Int_t *vKnownMonotoneSignalsRoundTwo;
+    //Vec_Int_t *vOldConsequentVector;
+    //Vec_Int_t *vRemainingConsecVector;
+    int i;
+    int iElem;
+    int pendingSignalIndex;
+    Abc_Ntk_t *pNtkTemp;
+    int hintSingalBeginningMarker;
+    int hintSingalEndMarker;
+    struct aigPoIndices *aigPoIndicesInstance;
+    //struct monotoneVectorsStruct *monotoneVectorsInstance;
+    struct antecedentConsequentVectorsStruct *anteConsecInstance;
+    //Aig_Obj_t *safetyDriverNew;
+    Vec_Int_t *newIntVec;
+    Vec_Ptr_t *levelOneMonotne, *levelTwoMonotne;
+    //Vec_Ptr_t *levelThreeMonotne;
+
+    Vec_Ptr_t *vMasterDisjunctions;
+
+    extern int findPendingSignal(Abc_Ntk_t *pNtk);
+    extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);    
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+
+    //system("rm monotone.dat");
+    
+    /*******************************************/    
+    //Finding the PO index of the pending signal 
+    /*******************************************/    
+    pendingSignalIndex = findPendingSignal(pNtk);
+    if( pendingSignalIndex == -1 )
+    {
+        printf("\nNo Pending Signal Found\n");
+        return NULL;
+    }
+    //else
+        //printf("Po[%d] = %s\n", pendingSignalIndex, Abc_ObjName( Abc_NtkPo(pNtk, pendingSignalIndex) ) );
+
+    /*******************************************/    
+    //Finding the PO indices of all hint signals
+    /*******************************************/    
+    vCandidateMonotoneSignals = findHintOutputs(pNtk);
+    if( vCandidateMonotoneSignals == NULL )
+        return NULL;
+    else
+    {
+        //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
+        //    printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
+        hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
+        hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
+    }
+
+    /**********************************************/
+    //Allocating "struct" with necessary parameters
+    /**********************************************/
+    aigPoIndicesInstance = allocAigPoIndices();
+    aigPoIndicesInstance->attrPendingSignalIndex = pendingSignalIndex;
+    aigPoIndicesInstance->attrHintSingalBeginningMarker = hintSingalBeginningMarker;
+    aigPoIndicesInstance->attrHintSingalEndMarker = hintSingalEndMarker;
+    aigPoIndicesInstance->attrSafetyInvarIndex = collectSafetyInvariantPOIndex(pNtk);
+
+    /****************************************************/
+    //Allocating "struct" with necessary monotone vectors
+    /****************************************************/
+    anteConsecInstance = allocAntecedentConsequentVectorsStruct();
+    anteConsecInstance->attrAntecedents = NULL;
+    anteConsecInstance->attrConsequentCandidates = vCandidateMonotoneSignals;
+
+    /*******************************************/    
+    //Generate AIG from Ntk
+    /*******************************************/    
+    if( !Abc_NtkIsStrash( pNtk ) )
+    {
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
+        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
+    }
+    else
+    {
+        pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        pNtkTemp = pNtk;
+    }
+
+    /*******************************************/    
+    //finding LEVEL 1 monotone signals
+    /*******************************************/    
+    //printf("Calling target function outside loop\n");
+    vKnownMonotoneSignals = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
+    levelOneMonotne = Vec_PtrAlloc(0);
+    Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
+    {
+        newIntVec = createSingletonIntVector( iElem );
+        Vec_PtrPush( levelOneMonotne, newIntVec );
+        //printf("Monotone Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
+    }
+    //printAllIntVectors( levelOneMonotne, pNtk, "monotone.dat" );
+
+    vMasterDisjunctions = Vec_PtrAlloc( Vec_PtrSize( levelOneMonotne ));
+    appendVecToMasterVecInt(vMasterDisjunctions, levelOneMonotne );
+
+    /*******************************************/    
+    //finding LEVEL >1 monotone signals
+    /*******************************************/    
+    #if 0
+    if( vKnownMonotoneSignals )
+    {
+        Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
+        {
+            printf("\n**************************************************************\n");
+            printf("Exploring Second Layer : Reference Po[%d] = %s", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ));
+            printf("\n**************************************************************\n");
+            anteConsecInstance->attrAntecedents = createSingletonIntVector( iElem );
+            vOldConsequentVector = anteConsecInstance->attrConsequentCandidates;
+            vRemainingConsecVector = updateAnteConseVectors(anteConsecInstance);
+            if( anteConsecInstance->attrConsequentCandidates != vRemainingConsecVector )
+            {
+                anteConsecInstance->attrConsequentCandidates = vRemainingConsecVector;
+            }
+            vKnownMonotoneSignalsRoundTwo = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
+            Vec_IntForEachEntry( vKnownMonotoneSignalsRoundTwo, iElemTwo, iTwo )
+            {
+                printf("Monotone Po[%d] = %s, (%d, %d)\n", iElemTwo, Abc_ObjName( Abc_NtkPo(pNtk, iElemTwo) ), iElem, iElemTwo );
+            }
+            Vec_IntFree(vKnownMonotoneSignalsRoundTwo);
+            Vec_IntFree(anteConsecInstance->attrAntecedents);
+            if(anteConsecInstance->attrConsequentCandidates != vOldConsequentVector)
+            {
+                Vec_IntFree(anteConsecInstance->attrConsequentCandidates);
+                anteConsecInstance->attrConsequentCandidates = vOldConsequentVector;
+            }
+        }
+    }
+    #endif 
+
+#if 1
+    levelTwoMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelOneMonotne );
+    //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
+    appendVecToMasterVecInt(vMasterDisjunctions, levelTwoMonotne );
+#endif
+
+    //levelThreeMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelTwoMonotne );
+    //printAllIntVectors( levelThreeMonotne );
+    //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
+    //appendVecToMasterVecInt(vMasterDisjunctions, levelThreeMonotne );
+
+    deallocAigPoIndices(aigPoIndicesInstance);
+    deallocAntecedentConsequentVectorsStruct(anteConsecInstance);
+    //deallocPointersToMonotoneVectors(monotoneVectorsInstance);
+
+    deallocateVecOfIntVec( levelOneMonotne );
+    deallocateVecOfIntVec( levelTwoMonotne );
+
+    Aig_ManStop(pAig);
+    Vec_IntFree(vKnownMonotoneSignals);
+
+    return vMasterDisjunctions;
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/proof/live/kLiveConstraints.c b/src/proof/live/kLiveConstraints.c
new file mode 100644
index 00000000..de5983f2
--- /dev/null
+++ b/src/proof/live/kLiveConstraints.c
@@ -0,0 +1,177 @@
+/**CFile****************************************************************
+
+  FileName    [kLiveConstraints.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Liveness property checking.]
+
+  Synopsis    [Constraint analysis module for the k-Liveness algorithm
+        invented by Koen Classen, Niklas Sorensson.]
+
+  Author      [Sayak Ray]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 31, 2012.]
+
+  Revision    [$Id: liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include "base/main/main.h"
+#include "aig/aig/aig.h"
+#include "aig/saig/saig.h"
+#include <string.h>
+#include "base/main/mainInt.h"
+#include "proof/pdr/pdr.h"
+
+ABC_NAMESPACE_IMPL_START
+
+Aig_Obj_t *createConstrained0LiveCone( 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 *collectCSSignals( 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;
+}
+
+Aig_Man_t *createNewAigWith0LivePo( Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live )
+{
+    Aig_Man_t *pNewAig;
+    Aig_Obj_t *pObj, *pObjNewPoDriver;
+    int i;
+
+    //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 5: create register outputs
+    //****************************************************************
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+        pObj->pData = Aig_ObjCreateCi( pNewAig );
+        }
+
+    //********************************************************************
+    // Step 7: create internal nodes
+    //********************************************************************
+        Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
+    }
+
+    pObjNewPoDriver = createConstrained0LiveCone( pNewAig, signalList );
+    Aig_ObjCreateCo( pNewAig, pObjNewPoDriver );
+    *index0Live = i;
+
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
+    }
+
+    Aig_ManSetRegNum( pNewAig, Aig_ManRegNum(pAig) );
+    Aig_ManCleanup( pNewAig );
+
+    assert( Aig_ManCheck( pNewAig ) );
+    return pNewAig;
+}
+
+Vec_Ptr_t *checkMonotoneSignal()
+{
+    return NULL;
+}
+
+Vec_Ptr_t *gatherMonotoneSignals(Aig_Man_t *pAig)
+{
+    int i;
+    Aig_Obj_t *pObj;
+
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        Aig_ObjPrint( pAig, pObj );
+        printf("\n");
+    }
+    
+    return NULL;
+}
+
+Aig_Man_t *generateWorkingAig( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live )
+{
+    Vec_Ptr_t *vSignalVector;
+    Aig_Man_t *pAigNew;
+
+    vSignalVector = collectCSSignals( pNtk, pAig );    
+    assert(vSignalVector);
+    pAigNew = createNewAigWith0LivePo( pAig, vSignalVector, pIndex0Live );
+    Vec_PtrFree(vSignalVector);
+
+    return pAigNew;
+}
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/live/kliveness.c b/src/proof/live/kliveness.c
new file mode 100644
index 00000000..7ba67155
--- /dev/null
+++ b/src/proof/live/kliveness.c
@@ -0,0 +1,816 @@
+/**CFile****************************************************************
+
+  FileName    [kliveness.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Liveness property checking.]
+
+  Synopsis        [Main implementation module of the algorithm k-Liveness    ] 
+              [invented by Koen Claessen, Niklas Sorensson. Implements]
+              [the code for 'kcs'. 'kcs' pre-processes based on switch]
+        [and then runs the (absorber circuit >> pdr) loop  ]
+
+  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"
+#include <time.h>
+
+//#define WITHOUT_CONSTRAINTS
+
+ABC_NAMESPACE_IMPL_START
+
+/***************** Declaration of standard ABC related functions ********************/
+extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange );
+extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
+/***********************************************************************************/
+
+/***************** Declaration of kLiveness related functions **********************/
+//function defined in kLiveConstraints.c
+extern Aig_Man_t *generateWorkingAig( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live );
+
+//function defined in arenaViolation.c
+extern Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers );
+
+//function defined in disjunctiveMonotone.c
+extern Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk );
+extern Vec_Int_t *createSingletonIntVector( int i );
+/***********************************************************************************/
+extern Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK );
+extern Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK );
+
+//Definition of some macros pertaining to modes/switches
+#define SIMPLE_kCS 0
+#define kCS_WITH_SAFETY_INVARIANTS 1
+#define kCS_WITH_DISCOVER_MONOTONE_SIGNALS 2
+#define kCS_WITH_SAFETY_AND_DCS_INVARIANTS 3
+#define kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS 4
+
+//unused function
+#if 0
+Aig_Obj_t *readTargetPinSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk)
+{
+    Aig_Obj_t *pObj;
+    int i;
+
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "0Liveness_" ) != NULL  )
+        {
+            //return Aig_ObjFanin0(pObj);
+            return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
+        }
+    }    
+
+    return NULL;
+}
+#endif
+
+Aig_Obj_t *readLiveSignal_0( Aig_Man_t *pAig, int liveIndex_0 )
+{
+    Aig_Obj_t *pObj;
+
+    pObj = Aig_ManCo( pAig, liveIndex_0 );
+    return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
+}
+
+Aig_Obj_t *readLiveSignal_k( Aig_Man_t *pAig, int liveIndex_k )
+{
+    Aig_Obj_t *pObj;
+
+    pObj = Aig_ManCo( pAig, liveIndex_k );
+    return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
+}
+
+//unused funtion
+#if 0
+Aig_Obj_t *readTargetPoutSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int nonFirstIteration)
+{
+    Aig_Obj_t *pObj;
+    int i;
+
+    if( nonFirstIteration == 0 )
+        return NULL;
+    else
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "kLiveness_" ) != NULL  )
+            {
+                //return Aig_ObjFanin0(pObj);
+                return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
+            }
+        }    
+
+    return NULL;
+}
+#endif
+
+//unused function
+#if 0
+void updateNewNetworkNameManager_kCS( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, 
+            Vec_Ptr_t *vLoNames, Vec_Ptr_t *vPoNames, Vec_Ptr_t *vLiNames )
+{
+    Aig_Obj_t *pObj;
+    Abc_Obj_t *pNode;
+    int i, ntkObjId;
+
+    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );
+
+    if( vPiNames )
+    {
+        Saig_ManForEachPi( pAig, pObj, i )
+        {
+            ntkObjId = Abc_NtkCi( pNtk, i )->Id;
+            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
+        }
+    }
+    if( vLoNames )
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+            ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
+            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
+        }
+    }
+
+    if( vPoNames )
+    {
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            ntkObjId = Abc_NtkCo( pNtk, i )->Id;
+            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPoNames, i), NULL );    
+        }
+    }
+
+    if( vLiNames )
+    {
+        Saig_ManForEachLi( pAig, pObj, i )
+        {
+            ntkObjId = Abc_NtkCo( pNtk, Saig_ManPoNum( pAig ) + i )->Id;
+            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLiNames, i), NULL );
+        }
+    }
+
+    // assign latch input names
+    Abc_NtkForEachLatch(pNtk, pNode, i)
+        if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL )
+            Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL );
+}
+#endif
+
+Aig_Man_t *introduceAbsorberLogic( Aig_Man_t *pAig, int *pLiveIndex_0, int *pLiveIndex_k, int nonFirstIteration )
+{
+    Aig_Man_t *pNewAig;
+    Aig_Obj_t *pObj, *pObjAbsorberLo, *pPInNewArg, *pPOutNewArg;
+    Aig_Obj_t *pPIn = NULL, *pPOut = NULL, *pPOutCo = NULL;
+    Aig_Obj_t *pFirstAbsorberOr, *pSecondAbsorberOr;
+    int i;
+    int piCopied = 0, loCreated = 0, loCopied = 0, liCreated = 0, liCopied = 0; 
+    int nRegCount;
+
+    assert(*pLiveIndex_0 != -1);
+    if(nonFirstIteration == 0)
+        assert( *pLiveIndex_k == -1 );
+    else
+        assert( *pLiveIndex_k != -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("_kCS") + 1 );
+    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "kCS");
+        pNewAig->pSpec = NULL;
+
+    //****************************************************************
+    // reading the signal pIn, and pOut
+    //****************************************************************
+
+    pPIn = readLiveSignal_0( pAig, *pLiveIndex_0 );
+    if( *pLiveIndex_k == -1 )
+        pPOut = NULL;
+    else
+        pPOut = readLiveSignal_k( pAig, *pLiveIndex_k );
+    
+    //****************************************************************
+    // Step 2: map constant nodes
+    //****************************************************************
+        pObj = Aig_ManConst1( pAig );
+        pObj->pData = Aig_ManConst1( pNewAig );
+
+    //****************************************************************
+        // Step 3: create true PIs
+    //****************************************************************
+        Saig_ManForEachPi( pAig, pObj, i )
+    {
+        piCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+    }
+
+    //****************************************************************
+    // Step 5: create register outputs
+    //****************************************************************
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+        loCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+        }
+
+    //****************************************************************
+    // Step 6: create "D" register output for the ABSORBER logic
+    //****************************************************************
+    loCreated++;
+    pObjAbsorberLo = Aig_ObjCreateCi( pNewAig );
+
+    nRegCount = loCreated + loCopied;
+
+    //********************************************************************
+    // Step 7: create internal nodes
+    //********************************************************************
+        Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+
+    //****************************************************************
+    // Step 8: create the two OR gates of the OBSERVER logic
+    //****************************************************************
+    if( nonFirstIteration == 0 )
+    {
+        assert(pPIn);
+        
+        pPInNewArg = !Aig_IsComplement(pPIn)? 
+                (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : 
+                Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
+
+        pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPInNewArg), pObjAbsorberLo );
+        pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
+    }
+    else
+    {
+        assert( pPOut );
+
+        pPInNewArg = !Aig_IsComplement(pPIn)? 
+                (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : 
+                Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
+        pPOutNewArg = !Aig_IsComplement(pPOut)? 
+                (Aig_Obj_t *)((Aig_Regular(pPOut))->pData) : 
+                Aig_Not((Aig_Obj_t *)((Aig_Regular(pPOut))->pData));
+        
+        pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPOutNewArg), pObjAbsorberLo );
+        pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
+    }    
+    
+    //********************************************************************
+    // Step 9: create primary outputs 
+    //********************************************************************
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
+        if( i == *pLiveIndex_k )
+            pPOutCo = (Aig_Obj_t *)(pObj->pData);
+    }
+
+    //create new po
+    if( nonFirstIteration == 0 )
+    {
+        assert(pPOutCo == NULL);
+        pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );     
+
+        *pLiveIndex_k = i;
+    }    
+    else
+    {
+        assert( pPOutCo != NULL );
+        //pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );     
+        //*pLiveIndex_k = Saig_ManPoNum(pAig);
+
+        Aig_ObjPatchFanin0( pNewAig, pPOutCo, pSecondAbsorberOr );
+    }
+
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        liCopied++;
+        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
+    }
+
+    //create new li
+    liCreated++;
+    Aig_ObjCreateCo( pNewAig, pFirstAbsorberOr );
+
+    Aig_ManSetRegNum( pNewAig, nRegCount );
+    Aig_ManCleanup( pNewAig );
+    
+    assert( Aig_ManCheck( pNewAig ) );
+
+    assert( *pLiveIndex_k != - 1);
+    return pNewAig;
+}
+
+void modifyAigToApplySafetyInvar(Aig_Man_t *pAig, int csTarget, int safetyInvarPO)
+{
+    Aig_Obj_t *pObjPOSafetyInvar, *pObjSafetyInvar;
+    Aig_Obj_t *pObjPOCSTarget, *pObjCSTarget;
+    Aig_Obj_t *pObjCSTargetNew;
+
+    pObjPOSafetyInvar = Aig_ManCo( pAig, safetyInvarPO );
+    pObjSafetyInvar =  Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOSafetyInvar), Aig_ObjFaninC0(pObjPOSafetyInvar));    
+    pObjPOCSTarget = Aig_ManCo( pAig, csTarget );
+    pObjCSTarget = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOCSTarget), Aig_ObjFaninC0(pObjPOCSTarget));    
+
+    pObjCSTargetNew = Aig_And( pAig, pObjSafetyInvar, pObjCSTarget );
+    Aig_ObjPatchFanin0( pAig, pObjPOCSTarget, pObjCSTargetNew );
+}
+
+int flipConePdr( Aig_Man_t *pAig, int directive, int targetCSPropertyIndex, int safetyInvariantPOIndex, int absorberCount )
+{
+    int RetValue, i;
+    Aig_Obj_t *pObjTargetPo;
+    Aig_Man_t *pAigDupl;
+    Pdr_Par_t Pars, * pPars = &Pars;
+    Abc_Cex_t * pCex = NULL;
+
+    char *fileName;
+    
+    fileName = (char *)malloc(sizeof(char) * 50);
+    sprintf(fileName, "%s_%d.%s", "kLive", absorberCount, "blif" );
+
+    if( directive == kCS_WITH_SAFETY_INVARIANTS || directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS )
+    {
+        assert( safetyInvariantPOIndex != -1 );
+        modifyAigToApplySafetyInvar(pAig, targetCSPropertyIndex, safetyInvariantPOIndex);
+    }
+
+    pAigDupl = pAig;
+    pAig = Aig_ManDupSimple( pAigDupl );
+
+    for( i=0; i<Saig_ManPoNum(pAig); i++ )
+    {
+        pObjTargetPo = Aig_ManCo( pAig, i );
+        Aig_ObjChild0Flip( pObjTargetPo );
+    }
+
+    Pdr_ManSetDefaultParams( pPars );
+    pPars->fVerbose = 1;
+    pPars->fNotVerbose = 1;
+    pPars->fSolveAll = 1;
+    pAig->vSeqModelVec = NULL;
+
+    Aig_ManCleanup( pAig );
+    assert( Aig_ManCheck( pAig ) );
+
+    Pdr_ManSolve( pAig, pPars );    
+
+    if( pAig->vSeqModelVec )
+    {
+        pCex = (Abc_Cex_t *)Vec_PtrEntry( pAig->vSeqModelVec, targetCSPropertyIndex );
+        if( pCex == NULL )
+        {
+            RetValue = 1;
+        }
+        else
+            RetValue = 0;
+    }
+    else
+    {
+        RetValue = -1;
+        exit(0);
+    }
+
+    free(fileName);
+
+    for( i=0; i<Saig_ManPoNum(pAig); i++ )
+    {
+        pObjTargetPo = Aig_ManCo( pAig, i );
+        Aig_ObjChild0Flip( pObjTargetPo );
+    }
+    
+    Aig_ManStop( pAig );
+    return RetValue;
+}
+
+//unused function
+#if 0
+int read0LiveIndex( Abc_Ntk_t *pNtk )
+{
+    Abc_Obj_t *pObj;
+    int i;
+
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if( strstr( Abc_ObjName( pObj ), "0Liveness_" ) != NULL )
+            return i;
+    }        
+
+    return -1;
+}
+#endif
+
+int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk)
+{
+    Abc_Obj_t *pObj;
+    int i;
+
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if( strstr( Abc_ObjName( pObj ), "csSafetyInvar_" ) != NULL )
+            return i;
+    }        
+
+    return -1;
+}
+
+Vec_Ptr_t *collectUserGivenDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk )
+{
+    Abc_Obj_t *pObj;
+    int i;
+    Vec_Ptr_t *monotoneVector;
+    Vec_Int_t *newIntVector;
+
+    monotoneVector = Vec_PtrAlloc(0);    
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if( strstr( Abc_ObjName( pObj ), "csLevel1Stabil_" ) != NULL )
+        {
+            newIntVector = createSingletonIntVector(i);
+            Vec_PtrPush(monotoneVector, newIntVector);
+        }
+    }
+
+    if( Vec_PtrSize(monotoneVector) > 0 )
+        return monotoneVector;
+    else
+        return NULL;
+
+}
+
+void deallocateMasterBarrierDisjunctInt(Vec_Ptr_t *vMasterBarrierDisjunctsArg)
+{
+    Vec_Int_t *vInt;
+    int i;
+
+    if(vMasterBarrierDisjunctsArg)
+    {
+        Vec_PtrForEachEntry(Vec_Int_t *, vMasterBarrierDisjunctsArg, vInt, i)
+        {    
+            Vec_IntFree(vInt);
+        }
+        Vec_PtrFree(vMasterBarrierDisjunctsArg);
+    }
+}
+
+void deallocateMasterBarrierDisjunctVecPtrVecInt(Vec_Ptr_t *vMasterBarrierDisjunctsArg)
+{
+    Vec_Int_t *vInt;
+    Vec_Ptr_t *vPtr;
+    int i, j, k, iElem;
+
+    if(vMasterBarrierDisjunctsArg)
+    {
+        Vec_PtrForEachEntry(Vec_Ptr_t *, vMasterBarrierDisjunctsArg, vPtr, i)
+        {    
+            assert(vPtr);
+            Vec_PtrForEachEntry( Vec_Int_t *, vPtr, vInt, j )
+            {
+                //Vec_IntFree(vInt);
+                Vec_IntForEachEntry( vInt, iElem, k )
+                    printf("%d - ", iElem);
+                //printf("Chung Chang j = %d\n", j);
+            }
+            Vec_PtrFree(vPtr);
+        }
+        Vec_PtrFree(vMasterBarrierDisjunctsArg);
+    }
+}
+
+Vec_Ptr_t *getVecOfVecFairness(FILE *fp)
+{
+    Vec_Ptr_t *masterVector = Vec_PtrAlloc(0);
+    //Vec_Ptr_t *currSignalVector;
+    char stringBuffer[100];
+    //int i;
+    
+    while(fgets(stringBuffer, 50, fp))
+    {
+        if(strstr(stringBuffer, ":"))
+        {
+
+        }
+        else
+        {
+                
+        }
+    }
+
+    return masterVector;
+}
+
+
+int Abc_CommandCS_kLiveness( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+        Abc_Ntk_t * pNtk, * pNtkTemp;
+    Aig_Man_t * pAig, *pAigCS, *pAigCSNew;
+    int absorberCount;
+    int absorberLimit = 500;
+    int RetValue;
+    int liveIndex_0 = -1, liveIndex_k = -1;
+    int fVerbose = 1;
+    int directive = -1;
+    int c;
+    int safetyInvariantPO = -1;
+    clock_t beginTime, endTime;
+    double time_spent;
+    Vec_Ptr_t *vMasterBarrierDisjuncts = NULL;
+    Aig_Man_t *pWorkingAig;
+    //FILE *fp;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+
+    //fp = fopen("propFile.txt", "r");
+    //if( fp )
+    //    getVecOfVecFairness(fp);
+    //exit(0);
+
+    /*************************************************
+    Extraction of Command Line Argument    
+    *************************************************/
+    if( argc == 1 )
+    {
+        assert( directive == -1 );
+        directive = SIMPLE_kCS;
+    }
+    else
+    {
+        Extra_UtilGetoptReset();
+        while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
+        {
+            switch( c )
+            {
+            case 'c':
+                directive = kCS_WITH_SAFETY_INVARIANTS; 
+                break;
+            case 'm':
+                directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; 
+                break;
+            case 'C':
+                directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
+                break;
+            case 'g':
+                directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+            }
+        }
+    }
+    /*************************************************
+    Extraction of Command Line Argument Ends    
+    *************************************************/
+
+    if( !Abc_NtkIsStrash( pNtk ) )
+    {
+        printf("The input network was not strashed, strashing....\n");
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
+        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
+    }
+    else
+    {
+        pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        pNtkTemp = pNtk;
+    }
+
+    if( directive == kCS_WITH_SAFETY_INVARIANTS )
+    {
+        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
+        assert( safetyInvariantPO != -1 );
+    }
+
+    if(directive == kCS_WITH_DISCOVER_MONOTONE_SIGNALS)
+    {
+        beginTime = clock();
+        vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
+        endTime = clock();
+        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
+        printf("pre-processing time = %f\n",time_spent); 
+        return 0;
+    }
+
+    if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS)
+    {
+        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
+        assert( safetyInvariantPO != -1 );
+
+        beginTime = clock();
+        vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
+        endTime = clock();
+        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
+        printf("pre-processing time = %f\n",time_spent); 
+
+        assert( vMasterBarrierDisjuncts != NULL );
+        assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
+    }
+
+    if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
+    {
+        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
+        assert( safetyInvariantPO != -1 );
+
+        beginTime = clock();
+        vMasterBarrierDisjuncts = collectUserGivenDisjunctiveMonotoneSignals( pNtk );
+        endTime = clock();
+        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
+        printf("pre-processing time = %f\n",time_spent); 
+
+        assert( vMasterBarrierDisjuncts != NULL );
+        assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
+    }
+
+    if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
+    {
+        assert( vMasterBarrierDisjuncts != NULL );
+        pWorkingAig = generateWorkingAigWithDSC( pAig, pNtk, &liveIndex_0, vMasterBarrierDisjuncts );
+        pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
+    }
+    else
+    {
+        pWorkingAig = generateWorkingAig( pAig, pNtk, &liveIndex_0 );
+        pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
+    }
+
+    Aig_ManStop(pWorkingAig);
+
+    for( absorberCount=1; absorberCount<absorberLimit; absorberCount++ )
+    {
+        //printf( "\nindex of the liveness output = %d\n", liveIndex_k );
+        RetValue = flipConePdr( pAigCS, directive, liveIndex_k, safetyInvariantPO, absorberCount );
+
+        if ( RetValue == 1 )
+        {
+                Abc_Print( 1, "k = %d, Property proved\n", absorberCount );
+            break;
+        }
+            else if ( RetValue == 0 )
+        {
+            if( fVerbose )
+            {
+                Abc_Print( 1, "k = %d, Property DISPROVED\n", absorberCount );
+            }
+        }
+            else if ( RetValue == -1 )
+        {
+                Abc_Print( 1, "Property UNDECIDED with k = %d.\n", absorberCount );
+        }
+            else
+                assert( 0 );
+
+        pAigCSNew = introduceAbsorberLogic(pAigCS, &liveIndex_0, &liveIndex_k, absorberCount);
+        Aig_ManStop(pAigCS);
+        pAigCS = pAigCSNew;
+    }
+
+    Aig_ManStop(pAigCS);
+    Aig_ManStop(pAig);
+
+    if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
+    {
+        deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
+    }
+    else
+    {
+        //if(vMasterBarrierDisjuncts)
+        //    Vec_PtrFree(vMasterBarrierDisjuncts);
+        //deallocateMasterBarrierDisjunctVecPtrVecInt(vMasterBarrierDisjuncts);
+        deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
+    }
+    return 0;
+
+    usage:
+        fprintf( stdout, "usage: kcs [-cmgCh]\n" );
+            fprintf( stdout, "\timplements Claessen-Sorensson's k-Liveness algorithm\n" );
+        fprintf( stdout, "\t-c : verification with constraints, looks for POs prefixed with csSafetyInvar_\n");
+        fprintf( stdout, "\t-m : discovers monotone signals\n");
+            fprintf( stdout, "\t-g : verification with user-supplied barriers, looks for POs prefixed with csLevel1Stabil_\n");
+        fprintf( stdout, "\t-C : verification with discovered monotone signals\n");
+        fprintf( stdout, "\t-h : print usage\n");
+            return 1;
+
+}
+
+int Abc_CommandNChooseK( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkCombStabil;
+    Aig_Man_t * pAig, *pAigCombStabil;
+    int directive = -1;
+    int c;
+    int parameterizedCombK;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+
+
+    /*************************************************
+    Extraction of Command Line Argument    
+    *************************************************/
+    if( argc == 1 )
+    {
+        assert( directive == -1 );
+        directive = SIMPLE_kCS;
+    }
+    else
+    {
+        Extra_UtilGetoptReset();
+        while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
+        {
+            switch( c )
+            {
+            case 'c':
+                directive = kCS_WITH_SAFETY_INVARIANTS; 
+                break;
+            case 'm':
+                directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; 
+                break;
+            case 'C':
+                directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
+                break;
+            case 'g':
+                directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+            }
+        }
+    }
+    /*************************************************
+    Extraction of Command Line Argument Ends    
+    *************************************************/
+
+    if( !Abc_NtkIsStrash( pNtk ) )
+    {
+        printf("The input network was not strashed, strashing....\n");
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
+        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
+    }
+    else
+    {
+        pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        pNtkTemp = pNtk;
+    }
+
+/**********************Code for generation of nCk outputs**/
+    //combCount = countCombination(1000, 3);
+    //pAigCombStabil = generateDisjunctiveTester( pNtk, pAig, 7, 2 );
+    printf("Enter parameterizedCombK = " );
+    if( scanf("%d", &parameterizedCombK) != 1 )
+    {
+        printf("\nFailed to read integer!\n");
+        return 0;
+    }
+    printf("\n");
+
+    pAigCombStabil = generateGeneralDisjunctiveTester( pNtk, pAig, parameterizedCombK );
+    Aig_ManPrintStats(pAigCombStabil);
+    pNtkCombStabil = Abc_NtkFromAigPhase( pAigCombStabil );
+    pNtkCombStabil->pName = Abc_UtilStrsav( pAigCombStabil->pName );
+    if ( !Abc_NtkCheck( pNtkCombStabil ) )
+            fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
+    Abc_FrameSetCurrentNetwork( pAbc, pNtkCombStabil );
+
+    Aig_ManStop( pAigCombStabil );
+    Aig_ManStop( pAig );
+
+    return 1;
+    //printf("\ncombCount = %d\n", combCount);
+    //exit(0);
+/**********************************************************/
+
+    usage:
+        fprintf( stdout, "usage: nck [-cmgCh]\n" );
+            fprintf( stdout, "\tgenerates combinatorial signals for stabilization\n" );
+        fprintf( stdout, "\t-h : print usage\n");
+            return 1;
+
+}
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/proof/live/module.make b/src/proof/live/module.make
index 55c70fc8..ad9ed680 100644
--- a/src/proof/live/module.make
+++ b/src/proof/live/module.make
@@ -1,3 +1,9 @@
 SRC +=  src/proof/live/liveness.c \
     src/proof/live/liveness_sim.c \
-    src/proof/live/ltl_parser.c
+    src/proof/live/ltl_parser.c \
+    src/proof/live/kliveness.c \
+    src/proof/live/monotone.c \
+    src/proof/live/disjunctiveMonotone.c \
+    src/proof/live/arenaViolation.c \
+    src/proof/live/kLiveConstraints.c \
+    src/proof/live/combination.c
diff --git a/src/proof/live/monotone.c b/src/proof/live/monotone.c
new file mode 100644
index 00000000..c8b08ed3
--- /dev/null
+++ b/src/proof/live/monotone.c
@@ -0,0 +1,507 @@
+/**CFile****************************************************************
+
+  FileName    [kLiveConstraints.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Liveness property checking.]
+
+  Synopsis    [Constraint analysis module for the k-Liveness algorithm
+        invented by Koen Classen, Niklas Sorensson.]
+
+  Author      [Sayak Ray]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 31, 2012.]
+
+  Revision    [$Id: liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include "base/main/main.h"
+#include "aig/aig/aig.h"
+#include "aig/saig/saig.h"
+#include <string.h>
+#include "base/main/mainInt.h"
+#include "proof/pdr/pdr.h"
+
+ABC_NAMESPACE_IMPL_START
+
+extern Aig_Man_t *Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+//extern Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg, int *startMonotonePropPo);
+
+struct aigPoIndices
+{
+    int attrPendingSignalIndex;
+    int attrHintSingalBeginningMarker;
+    int attrHintSingalEndMarker;
+    int attrSafetyInvarIndex;
+};
+
+struct aigPoIndices *allocAigPoIndices()
+{
+    struct aigPoIndices *newAigPoIndices;
+
+    newAigPoIndices = (struct aigPoIndices *)malloc(sizeof (struct aigPoIndices));
+    newAigPoIndices->attrPendingSignalIndex = -1;
+    newAigPoIndices->attrHintSingalBeginningMarker = -1;
+    newAigPoIndices->attrHintSingalEndMarker = -1;
+    newAigPoIndices->attrSafetyInvarIndex = -1;
+
+    assert( newAigPoIndices != NULL );
+    return newAigPoIndices;
+}
+
+void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices)
+{
+    assert(toBeDeletedAigPoIndices != NULL );
+    free(toBeDeletedAigPoIndices);
+}
+
+struct monotoneVectorsStruct
+{
+    Vec_Int_t *attrKnownMonotone;
+    Vec_Int_t *attrCandMonotone;
+    Vec_Int_t *attrHintMonotone;
+};
+
+struct monotoneVectorsStruct *allocPointersToMonotoneVectors()
+{
+    struct monotoneVectorsStruct *newPointersToMonotoneVectors;
+
+    newPointersToMonotoneVectors = (struct monotoneVectorsStruct *)malloc(sizeof (struct monotoneVectorsStruct));
+
+    newPointersToMonotoneVectors->attrKnownMonotone = NULL;
+    newPointersToMonotoneVectors->attrCandMonotone = NULL;
+    newPointersToMonotoneVectors->attrHintMonotone = NULL;
+        
+    assert( newPointersToMonotoneVectors != NULL );
+    return newPointersToMonotoneVectors;
+}
+
+void deallocPointersToMonotoneVectors(struct monotoneVectorsStruct *toBeDeleted)
+{
+    assert( toBeDeleted != NULL );
+    free( toBeDeleted );
+}
+
+Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk)
+{
+    int i, numElementPush = 0;
+    Abc_Obj_t *pNode;
+    Vec_Int_t *vHintPoIntdex;
+
+    vHintPoIntdex = Vec_IntAlloc(0);
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        if( strstr( Abc_ObjName( pNode ), "hint_" ) != NULL )
+        {
+            Vec_IntPush( vHintPoIntdex, i );
+            numElementPush++;
+        }
+    }    
+    
+    if( numElementPush == 0 )
+        return NULL;
+    else
+        return vHintPoIntdex;
+}
+
+int findPendingSignal(Abc_Ntk_t *pNtk)
+{
+    int i, pendingSignalIndex = -1;
+    Abc_Obj_t *pNode;
+
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        if( strstr( Abc_ObjName( pNode ), "pendingSignal" ) != NULL )
+        {
+            pendingSignalIndex = i;
+            break;
+        }
+    }    
+    
+    return pendingSignalIndex;
+}
+
+int checkSanityOfKnownMonotone( Vec_Int_t *vKnownMonotone, Vec_Int_t *vCandMonotone, Vec_Int_t *vHintMonotone )
+{
+    int iElem, i;
+
+    Vec_IntForEachEntry( vKnownMonotone, iElem, i )
+        printf("%d ", iElem);
+    printf("\n");
+    Vec_IntForEachEntry( vCandMonotone, iElem, i )
+        printf("%d ", iElem);
+    printf("\n");
+    Vec_IntForEachEntry( vHintMonotone, iElem, i )
+        printf("%d ", iElem);
+    printf("\n");
+    return 1;
+}
+
+Aig_Man_t *createMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg, int *startMonotonePropPo)
+{
+    Aig_Man_t *pNewAig;
+    int iElem, i, nRegCount, oldPoNum, poSerialNum, iElemHint;
+    int piCopied = 0, liCopied = 0, liCreated = 0, loCopied = 0, loCreated = 0;
+    int poCopied = 0, poCreated = 0;
+    Aig_Obj_t *pObj, *pObjPo, *pObjDriver, *pObjDriverNew, *pObjPendingDriverNew, *pObjPendingAndNextPending;
+    Aig_Obj_t *pPendingFlop, *pHintSignalLo, *pHintMonotoneFlop, *pObjTemp1, *pObjTemp2, *pObjKnownMonotoneAnd;
+    Vec_Ptr_t *vHintMonotoneLocalDriverNew;
+    Vec_Ptr_t *vHintMonotoneLocalFlopOutput;
+    Vec_Ptr_t *vHintMonotoneLocalProp;
+
+    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
+    int hintSingalBeginningMarkerLocal = aigPoIndicesArg->attrHintSingalBeginningMarker;
+    //int hintSingalEndMarkerLocal = aigPoIndicesArg->attrHintSingalEndMarker;
+
+    Vec_Int_t *vKnownMonotoneLocal = monotoneVectorArg->attrKnownMonotone;
+    Vec_Int_t *vCandMonotoneLocal = monotoneVectorArg->attrCandMonotone;
+    Vec_Int_t *vHintMonotoneLocal = monotoneVectorArg->attrHintMonotone;
+    
+    //****************************************************************
+    // 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("_monotone") + 1 );
+    sprintf(pNewAig->pName, "%s_%s", pAig->pName, "_monotone");
+        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 )
+    {
+        piCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+    }
+
+    //****************************************************************
+    // Step 5: create register outputs
+    //****************************************************************
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+        loCopied++;
+        pObj->pData = Aig_ObjCreateCi(pNewAig);
+        }
+
+    //****************************************************************
+    // Step 6: create "D" register output for PENDING flop 
+    //****************************************************************
+    loCreated++;
+    pPendingFlop = Aig_ObjCreateCi( pNewAig );
+
+    //****************************************************************
+    // Step 6.a: create "D" register output for HINT_MONOTONE flop 
+    //****************************************************************
+    vHintMonotoneLocalFlopOutput = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
+    Vec_IntForEachEntry( vHintMonotoneLocal, iElem, i )
+    {
+        loCreated++;
+        pHintMonotoneFlop = Aig_ObjCreateCi( pNewAig );
+        Vec_PtrPush( vHintMonotoneLocalFlopOutput, pHintMonotoneFlop );
+    }
+
+    nRegCount = loCreated + loCopied;
+    printf("\nnRegCount = %d\n", nRegCount);
+
+    //********************************************************************
+    // Step 7: create internal nodes
+    //********************************************************************
+        Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    
+    //********************************************************************
+    // Step 8: mapping appropriate new flop drivers 
+    //********************************************************************
+
+    pObjPo = Aig_ManCo( pAig, pendingSignalIndexLocal );
+    pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+    pObjPendingDriverNew = !Aig_IsComplement(pObjDriver)? 
+                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
+                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
+
+    pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingDriverNew, pPendingFlop );
+
+    oldPoNum = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
+    pObjKnownMonotoneAnd = Aig_ManConst1( pNewAig );
+    #if 1
+    if( vKnownMonotoneLocal )
+    {
+        assert( checkSanityOfKnownMonotone( vKnownMonotoneLocal, vCandMonotoneLocal, vHintMonotoneLocal ) );
+
+        Vec_IntForEachEntry( vKnownMonotoneLocal, iElemHint, i )
+        {
+            iElem = (iElemHint - hintSingalBeginningMarkerLocal) + 1 + pendingSignalIndexLocal;
+            printf("\nProcessing knownMonotone = %d\n", iElem);
+            pObjPo = Aig_ManCo( pAig, iElem );
+            pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+            pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
+                    (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
+                    Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
+            pHintSignalLo = (Aig_Obj_t *)Vec_PtrEntry(vHintMonotoneLocalFlopOutput, iElem - oldPoNum);
+            pObjTemp1 = Aig_Or( pNewAig, Aig_And(pNewAig, pObjDriverNew, pHintSignalLo), 
+                        Aig_And(pNewAig, Aig_Not(pObjDriverNew), Aig_Not(pHintSignalLo)) );
+            
+            pObjKnownMonotoneAnd = Aig_And( pNewAig, pObjKnownMonotoneAnd, pObjTemp1 );
+        }
+        pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingAndNextPending, pObjKnownMonotoneAnd );
+    }
+    #endif
+
+    vHintMonotoneLocalDriverNew = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
+    vHintMonotoneLocalProp = Vec_PtrAlloc(Vec_IntSize(vHintMonotoneLocal));
+    Vec_IntForEachEntry( vHintMonotoneLocal, iElem, i )
+    {
+        pObjPo = Aig_ManCo( pAig, iElem );
+        pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
+        pObjDriverNew = !Aig_IsComplement(pObjDriver)? 
+                (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) : 
+                Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
+
+        if( vKnownMonotoneLocal != NULL && Vec_IntFind( vKnownMonotoneLocal, iElem ) != -1 )
+        {
+            Vec_PtrPush(vHintMonotoneLocalDriverNew, pObjDriverNew);
+        }
+        else
+        {
+            poSerialNum = Vec_IntFind( vHintMonotoneLocal, iElem );
+            pHintSignalLo = (Aig_Obj_t *)Vec_PtrEntry(vHintMonotoneLocalFlopOutput, poSerialNum );
+            pObjTemp1 = Aig_And( pNewAig, pObjPendingAndNextPending, pHintSignalLo);
+            pObjTemp2 = Aig_Or( pNewAig, Aig_Not(pObjTemp1), pObjDriverNew );
+            //pObjTemp2 = Aig_Or( pNewAig, Aig_Not(pObjTemp1), Aig_ManConst1( pNewAig ));
+            //pObjTemp2 = Aig_ManConst1( pNewAig );
+            Vec_PtrPush(vHintMonotoneLocalDriverNew, pObjDriverNew);
+            Vec_PtrPush(vHintMonotoneLocalProp, pObjTemp2); 
+        }
+    }
+
+    //********************************************************************
+    // Step 9: create primary outputs 
+    //********************************************************************
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        poCopied++;
+        pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
+    }
+
+    *startMonotonePropPo = i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vHintMonotoneLocalProp, pObj, i )
+    {
+        poCreated++;
+        pObjPo = Aig_ObjCreateCo( pNewAig, pObj ); 
+    }
+
+    //********************************************************************
+    // Step 9: create latch inputs 
+    //********************************************************************
+
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        liCopied++;
+        Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
+    }
+    
+    //********************************************************************
+    // Step 9.a: create latch input for PENDING_FLOP
+    //********************************************************************
+
+    liCreated++;
+    Aig_ObjCreateCo( pNewAig, pObjPendingDriverNew );
+
+    //********************************************************************
+    // Step 9.b: create latch input for MONOTONE_FLOP
+    //********************************************************************
+
+    Vec_PtrForEachEntry( Aig_Obj_t *, vHintMonotoneLocalDriverNew, pObj, i )
+    {
+        liCreated++;
+        Aig_ObjCreateCo( pNewAig, pObj );
+    }
+
+    printf("\npoCopied = %d, poCreated = %d\n", poCopied, poCreated);
+    printf("\nliCreated++ = %d\n", liCreated );
+    Aig_ManSetRegNum( pNewAig, nRegCount );
+    Aig_ManCleanup( pNewAig );
+    
+    assert( Aig_ManCheck( pNewAig ) );
+    assert( loCopied + loCreated == liCopied + liCreated );
+
+    printf("\nSaig_ManPoNum = %d\n", Saig_ManPoNum(pNewAig));
+    return pNewAig;
+}
+
+
+Vec_Int_t *findNewMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct monotoneVectorsStruct *monotoneVectorArg )
+{
+    Aig_Man_t *pAigNew;
+    Aig_Obj_t *pObjTargetPo;
+    int poMarker, oldPoNum;
+    int i, RetValue;
+    Pdr_Par_t Pars, * pPars = &Pars;
+    Abc_Cex_t * pCex = NULL;
+    Vec_Int_t *vMonotoneIndex;
+
+    int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
+    int hintSingalBeginningMarkerLocal = aigPoIndicesArg->attrHintSingalBeginningMarker;
+    //int hintSingalEndMarkerLocal = aigPoIndicesArg->attrHintSingalEndMarker;
+
+    //Vec_Int_t *vKnownMonotoneLocal = monotoneVectorArg->attrKnownMonotone;
+    //Vec_Int_t *vCandMonotoneLocal = monotoneVectorArg->attrCandMonotone;
+    //Vec_Int_t *vHintMonotoneLocal = monotoneVectorArg->attrHintMonotone;
+
+    pAigNew = createMonotoneTester(pAig, aigPoIndicesArg, monotoneVectorArg, &poMarker );
+    oldPoNum = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig);
+
+    vMonotoneIndex = Vec_IntAlloc(0);
+    printf("\nSaig_ManPoNum(pAigNew) = %d, poMarker = %d\n", Saig_ManPoNum(pAigNew), poMarker);
+    for( i=poMarker; i<Saig_ManPoNum(pAigNew); i++ )
+    {
+        pObjTargetPo = Aig_ManCo( pAigNew, i );
+        Aig_ObjChild0Flip( pObjTargetPo );
+
+        Pdr_ManSetDefaultParams( pPars );
+        pCex = NULL;
+        pPars->fVerbose = 0;
+        //pPars->iOutput = i;
+        //RetValue = Pdr_ManSolve( pAigNew, pPars, &pCex );    
+        RetValue = Pdr_ManSolve( pAigNew, pPars );    
+        if( RetValue == 1 )
+        {
+            printf("\ni = %d, RetValue = %d : %s (Frame %d)\n", i - oldPoNum + hintSingalBeginningMarkerLocal, RetValue, "Property Proved", pCex? (pCex)->iFrame : -1 );
+            Vec_IntPush( vMonotoneIndex, i - (pendingSignalIndexLocal + 1) + hintSingalBeginningMarkerLocal);
+        }
+        Aig_ObjChild0Flip( pObjTargetPo );
+    }
+    
+    if( Vec_IntSize( vMonotoneIndex ) > 0 )
+        return vMonotoneIndex;
+    else
+        return NULL;
+}
+
+Vec_Int_t *findRemainingMonotoneCandidates(Vec_Int_t *vKnownMonotone, Vec_Int_t *vHintMonotone)
+{
+    Vec_Int_t *vCandMonotone;
+    int iElem, i;
+
+    if( vKnownMonotone == NULL || Vec_IntSize(vKnownMonotone) <= 0 )
+        return vHintMonotone;
+    vCandMonotone = Vec_IntAlloc(0);
+    Vec_IntForEachEntry( vHintMonotone, iElem, i )
+    {
+        if( Vec_IntFind( vKnownMonotone, iElem ) == -1 )
+            Vec_IntPush( vCandMonotone, iElem );
+    }
+    
+    return vCandMonotone;
+}
+
+Vec_Int_t *findMonotoneSignals( Abc_Ntk_t *pNtk )
+{
+    Aig_Man_t *pAig;
+    Vec_Int_t *vCandidateMonotoneSignals;
+    Vec_Int_t *vKnownMonotoneSignals;
+    //Vec_Int_t *vKnownMonotoneSignalsNew;
+    //Vec_Int_t *vRemainingCanMonotone;
+    int i, iElem;
+    int pendingSignalIndex;
+    Abc_Ntk_t *pNtkTemp;
+    int hintSingalBeginningMarker;
+    int hintSingalEndMarker;
+    struct aigPoIndices *aigPoIndicesInstance;
+    struct monotoneVectorsStruct *monotoneVectorsInstance;
+    
+    /*******************************************/    
+    //Finding the PO index of the pending signal 
+    /*******************************************/    
+    pendingSignalIndex = findPendingSignal(pNtk);
+    if( pendingSignalIndex == -1 )
+    {
+        printf("\nNo Pending Signal Found\n");
+        return NULL;
+    }
+    else
+        printf("Po[%d] = %s\n", pendingSignalIndex, Abc_ObjName( Abc_NtkPo(pNtk, pendingSignalIndex) ) );
+
+    /*******************************************/    
+    //Finding the PO indices of all hint signals
+    /*******************************************/    
+    vCandidateMonotoneSignals = findHintOutputs(pNtk);
+    if( vCandidateMonotoneSignals == NULL )
+        return NULL;
+    else
+    {
+        Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
+            printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
+        hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
+        hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
+    }
+
+    /**********************************************/
+    //Allocating "struct" with necessary parameters
+    /**********************************************/
+    aigPoIndicesInstance = allocAigPoIndices();
+    aigPoIndicesInstance->attrPendingSignalIndex = pendingSignalIndex;
+    aigPoIndicesInstance->attrHintSingalBeginningMarker = hintSingalBeginningMarker;
+    aigPoIndicesInstance->attrHintSingalEndMarker = hintSingalEndMarker;
+
+    /****************************************************/
+    //Allocating "struct" with necessary monotone vectors
+    /****************************************************/
+    monotoneVectorsInstance = allocPointersToMonotoneVectors();
+    monotoneVectorsInstance->attrCandMonotone = vCandidateMonotoneSignals;
+    monotoneVectorsInstance->attrHintMonotone = vCandidateMonotoneSignals;
+
+    /*******************************************/    
+    //Generate AIG from Ntk
+    /*******************************************/    
+    if( !Abc_NtkIsStrash( pNtk ) )
+    {
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
+        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
+    }
+    else
+    {
+        pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        pNtkTemp = pNtk;
+    }
+
+    /*******************************************/    
+    //finding LEVEL 1 monotone signals
+    /*******************************************/    
+    vKnownMonotoneSignals = findNewMonotone( pAig, aigPoIndicesInstance, monotoneVectorsInstance );
+    monotoneVectorsInstance->attrKnownMonotone = vKnownMonotoneSignals;
+
+    /*******************************************/    
+    //finding LEVEL >1 monotone signals
+    /*******************************************/    
+    #if 0
+    if( vKnownMonotoneSignals )
+    {
+        printf("\nsize = %d\n", Vec_IntSize(vKnownMonotoneSignals) );
+        vRemainingCanMonotone = findRemainingMonotoneCandidates(vKnownMonotoneSignals, vCandidateMonotoneSignals);
+        monotoneVectorsInstance->attrCandMonotone = vRemainingCanMonotone; 
+        vKnownMonotoneSignalsNew = findNewMonotone( pAig, aigPoIndicesInstance, monotoneVectorsInstance );
+    }
+    #endif 
+
+    deallocAigPoIndices(aigPoIndicesInstance);
+    deallocPointersToMonotoneVectors(monotoneVectorsInstance);
+    return NULL;
+}
+
+ABC_NAMESPACE_IMPL_END