Integration of the liveness property prover developed by Sayak Ray.

1 files changed, 816 insertions, 0 deletions

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