Integration of the liveness property prover developed by Sayak Ray.

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

src/proof/live/kLiveConstraints.c

+/**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
+

src/proof/live/module.make

 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