diff options
| -rw-r--r-- | src/base/abci/abc.c | 10 | ||||
| -rw-r--r-- | src/proof/live/arenaViolation.c | 549 | ||||
| -rw-r--r-- | src/proof/live/combination.c | 463 | ||||
| -rw-r--r-- | src/proof/live/disjunctiveMonotone.c | 757 | ||||
| -rw-r--r-- | src/proof/live/kLiveConstraints.c | 177 | ||||
| -rw-r--r-- | src/proof/live/kliveness.c | 816 | ||||
| -rw-r--r-- | src/proof/live/module.make | 8 | ||||
| -rw-r--r-- | src/proof/live/monotone.c | 507 |
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", ¶meterizedCombK) != 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 |