diff options
Diffstat (limited to 'src/proof/live/arenaViolation.c')
| -rw-r--r-- | src/proof/live/arenaViolation.c | 549 |
1 files changed, 549 insertions, 0 deletions
diff --git a/src/proof/live/arenaViolation.c b/src/proof/live/arenaViolation.c new file mode 100644 index 00000000..8f78630b --- /dev/null +++ b/src/proof/live/arenaViolation.c @@ -0,0 +1,549 @@ +/**CFile**************************************************************** + + FileName [arenaViolation.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Liveness property checking.] + + Synopsis [module for addition of arena violator detector + induced by stabilizing constraints] + + Author [Sayak Ray] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 31, 2012.] + +***********************************************************************/ + +#include <stdio.h> +#include "base/main/main.h" +#include "aig/aig/aig.h" +#include "aig/saig/saig.h" +#include <string.h> +#include "base/main/mainInt.h" +#include "proof/pdr/pdr.h" + +//#define DISJUNCTIVE_CONSTRAINT_ENABLE_MODE +#define BARRIER_MONOTONE_TEST + +ABC_NAMESPACE_IMPL_START + +Vec_Ptr_t * createArenaLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers ) +{ + Vec_Ptr_t *vArenaLO; + int barrierCount; + Aig_Obj_t *pObj; + int i; + + if( vBarriers == NULL ) + return NULL; + + barrierCount = Vec_PtrSize(vBarriers); + if( barrierCount <= 0 ) + return NULL; + + vArenaLO = Vec_PtrAlloc(barrierCount); + for( i=0; i<barrierCount; i++ ) + { + pObj = Aig_ObjCreateCi( pAigNew ); + Vec_PtrPush( vArenaLO, pObj ); + } + + return vArenaLO; +} + +Vec_Ptr_t * createArenaLi( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal ) +{ + Vec_Ptr_t *vArenaLi; + int barrierCount; + int i; + Aig_Obj_t *pObj, *pObjDriver; + + if( vBarriers == NULL ) + return NULL; + + barrierCount = Vec_PtrSize(vBarriers); + if( barrierCount <= 0 ) + return NULL; + + vArenaLi = Vec_PtrAlloc(barrierCount); + for( i=0; i<barrierCount; i++ ) + { + pObjDriver = (Aig_Obj_t *)Vec_PtrEntry( vArenaSignal, i ); + pObj = Aig_ObjCreateCo( pAigNew, pObjDriver ); + Vec_PtrPush( vArenaLi, pObj ); + } + + return vArenaLi; +} + +Vec_Ptr_t *createMonotoneBarrierLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers ) +{ + Vec_Ptr_t *vMonotoneLO; + int barrierCount; + Aig_Obj_t *pObj; + int i; + + if( vBarriers == NULL ) + return NULL; + + barrierCount = Vec_PtrSize(vBarriers); + if( barrierCount <= 0 ) + return NULL; + + vMonotoneLO = Vec_PtrAlloc(barrierCount); + for( i=0; i<barrierCount; i++ ) + { + pObj = Aig_ObjCreateCi( pAigNew ); + Vec_PtrPush( vMonotoneLO, pObj ); + } + + return vMonotoneLO; +} + +Aig_Obj_t *driverToPoNew( Aig_Man_t *pAig, Aig_Obj_t *pObjPo ) +{ + Aig_Obj_t *poDriverOld; + Aig_Obj_t *poDriverNew; + + //Aig_ObjPrint( pAig, pObjPo ); + //printf("\n"); + + assert( Aig_ObjIsCo(pObjPo) ); + poDriverOld = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo)); + assert( !Aig_ObjIsCo(poDriverOld) ); + poDriverNew = !Aig_IsComplement(poDriverOld)? + (Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData) : + Aig_Not((Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData)); + //assert( !Aig_ObjIsCo(poDriverNew) ); + return poDriverNew; +} + +Vec_Ptr_t *collectBarrierDisjunctions(Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers) +{ + int barrierCount, i, j, jElem; + Vec_Int_t *vIthBarrier; + Aig_Obj_t *pObjBarrier, *pObjCurr, *pObjTargetPoOld; + Vec_Ptr_t *vNewBarrierSignals; + + if( vBarriers == NULL ) + return NULL; + barrierCount = Vec_PtrSize( vBarriers ); + if( barrierCount <= 0 ) + return NULL; + + vNewBarrierSignals = Vec_PtrAlloc( barrierCount ); + + for( i=0; i<barrierCount; i++ ) + { + vIthBarrier = (Vec_Int_t *)Vec_PtrEntry( vBarriers, i ); + assert( Vec_IntSize( vIthBarrier ) >= 1 ); + pObjBarrier = Aig_Not(Aig_ManConst1(pAigNew)); + Vec_IntForEachEntry( vIthBarrier, jElem, j ) + { + pObjTargetPoOld = Aig_ManCo( pAigOld, jElem ); + //Aig_ObjPrint( pAigOld, pObjTargetPoOld ); + //printf("\n"); + pObjCurr = driverToPoNew( pAigOld, pObjTargetPoOld ); + pObjBarrier = Aig_Or( pAigNew, pObjCurr, pObjBarrier ); + } + assert( pObjBarrier ); + Vec_PtrPush(vNewBarrierSignals, pObjBarrier); + } + assert( Vec_PtrSize( vNewBarrierSignals ) == barrierCount ); + + return vNewBarrierSignals; +} + +Aig_Obj_t *Aig_Xor( Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2 ) +{ + return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) ); +} + +Aig_Obj_t *createArenaViolation( + Aig_Man_t *pAigOld, + Aig_Man_t *pAigNew, + Aig_Obj_t *pWindowBegins, + Aig_Obj_t *pWithinWindow, + Vec_Ptr_t *vMasterBarriers, + Vec_Ptr_t *vBarrierLo, + Vec_Ptr_t *vBarrierLiDriver, + Vec_Ptr_t *vMonotoneDisjunctionNodes + ) +{ + Aig_Obj_t *pWindowBeginsLocal = pWindowBegins; + Aig_Obj_t *pWithinWindowLocal = pWithinWindow; + int i; + Aig_Obj_t *pObj, *pObjAnd1, *pObjOr1, *pObjAnd2, *pObjBarrierLo, *pObjBarrierSwitch, *pObjArenaViolation; + Vec_Ptr_t *vBarrierSignals; + + assert( vBarrierLiDriver != NULL ); + assert( vMonotoneDisjunctionNodes != NULL ); + + pObjArenaViolation = Aig_Not(Aig_ManConst1( pAigNew )); + + vBarrierSignals = collectBarrierDisjunctions(pAigOld, pAigNew, vMasterBarriers); + assert( vBarrierSignals != NULL ); + + assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == 0 ); + Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i ) + Vec_PtrPush( vMonotoneDisjunctionNodes, pObj ); + assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == Vec_PtrSize( vMasterBarriers ) ); + + Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i ) + { + //pObjNew = driverToPoNew( pAigOld, pObj ); + pObjAnd1 = Aig_And(pAigNew, pObj, pWindowBeginsLocal); + pObjBarrierLo = (Aig_Obj_t *)Vec_PtrEntry( vBarrierLo, i ); + pObjOr1 = Aig_Or(pAigNew, pObjAnd1, pObjBarrierLo); + Vec_PtrPush( vBarrierLiDriver, pObjOr1 ); + + pObjBarrierSwitch = Aig_Xor( pAigNew, pObj, pObjBarrierLo ); + pObjAnd2 = Aig_And( pAigNew, pObjBarrierSwitch, pWithinWindowLocal ); + pObjArenaViolation = Aig_Or( pAigNew, pObjAnd2, pObjArenaViolation ); + } + + Vec_PtrFree(vBarrierSignals); + return pObjArenaViolation; +} + +Aig_Obj_t *createConstrained0LiveConeWithDSC( Aig_Man_t *pNewAig, Vec_Ptr_t *signalList ) +{ + Aig_Obj_t *pConsequent, *pConsequentCopy, *pAntecedent, *p0LiveCone, *pObj; + int i, numSigAntecedent; + + numSigAntecedent = Vec_PtrSize( signalList ) - 1; + + pAntecedent = Aig_ManConst1( pNewAig ); + pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent ); + pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) ); + + for(i=0; i<numSigAntecedent; i++ ) + { + pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i ); + assert( Aig_Regular(pObj)->pData ); + pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) ); + } + + p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy ); + + return p0LiveCone; +} + +Vec_Ptr_t *collectCSSignalsWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) +{ + int i; + Aig_Obj_t *pObj, *pConsequent = NULL; + Vec_Ptr_t *vNodeArray; + + vNodeArray = Vec_PtrAlloc(1); + + Saig_ManForEachPo( pAig, pObj, i ) + { + if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL ) + Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) ); + else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL ) + pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); + } + assert( pConsequent ); + Vec_PtrPush( vNodeArray, pConsequent ); + return vNodeArray; +} + +int collectWindowBeginSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) +{ + int i; + Aig_Obj_t *pObj; + + Saig_ManForEachPo( pAig, pObj, i ) + { + if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "windowBegins_" ) != NULL ) + { + return i; + } + } + + return -1; +} + +int collectWithinWindowSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) +{ + int i; + Aig_Obj_t *pObj; + + Saig_ManForEachPo( pAig, pObj, i ) + { + if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "withinWindow_" ) != NULL ) + return i; + } + + return -1; +} + +int collectPendingSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) +{ + int i; + Aig_Obj_t *pObj; + + Saig_ManForEachPo( pAig, pObj, i ) + { + if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "pendingSignal" ) != NULL ) + return i; + } + + return -1; +} + +Aig_Obj_t *createAndGateForMonotonicityVerification( + Aig_Man_t *pNewAig, + Vec_Ptr_t *vDisjunctionSignals, + Vec_Ptr_t *vDisjunctionLo, + Aig_Obj_t *pendingLo, + Aig_Obj_t *pendingSignal + ) +{ + Aig_Obj_t *pObjBigAnd, *pObj, *pObjLo, *pObjImply; + Aig_Obj_t *pObjPendingAndPendingLo; + int i; + + pObjBigAnd = Aig_ManConst1( pNewAig ); + pObjPendingAndPendingLo = Aig_And( pNewAig, pendingLo, pendingSignal ); + Vec_PtrForEachEntry( Aig_Obj_t *, vDisjunctionSignals, pObj, i ) + { + pObjLo = (Aig_Obj_t *)Vec_PtrEntry( vDisjunctionLo, i ); + pObjImply = Aig_Or( pNewAig, Aig_Not(Aig_And( pNewAig, pObjPendingAndPendingLo, pObjLo)), + pObj ); + pObjBigAnd = Aig_And( pNewAig, pObjBigAnd, pObjImply ); + } + return pObjBigAnd; +} + +Aig_Man_t *createNewAigWith0LivePoWithDSC( Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers ) +{ + Aig_Man_t *pNewAig; + Aig_Obj_t *pObj, *pObjNewPoDriver; + int i; + int loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0; + Aig_Obj_t *pObjWindowBeginsNew, *pObjWithinWindowNew, *pObjArenaViolation, *pObjTarget, *pObjArenaViolationLiDriver; + Aig_Obj_t *pObjNewPoDriverArenaViolated, *pObjArenaViolationLo; + Vec_Ptr_t *vBarrierLo, *vBarrierLiDriver, *vBarrierLi; + Vec_Ptr_t *vMonotoneNodes; + +#ifdef BARRIER_MONOTONE_TEST + Aig_Obj_t *pObjPendingSignal; + Aig_Obj_t *pObjPendingFlopLo; + Vec_Ptr_t *vMonotoneBarrierLo; + Aig_Obj_t *pObjPendingAndPendingSignal, *pObjMonotoneAnd, *pObjCurrMonotoneLo; +#endif + + //assert( Vec_PtrSize( signalList ) > 1 ); + + //**************************************************************** + // Step1: create the new manager + // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)" + // nodes, but this selection is arbitrary - need to be justified + //**************************************************************** + pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) ); + pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_0Live") + 1 ); + sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live"); + pNewAig->pSpec = NULL; + + //**************************************************************** + // Step 2: map constant nodes + //**************************************************************** + pObj = Aig_ManConst1( pAig ); + pObj->pData = Aig_ManConst1( pNewAig ); + + //**************************************************************** + // Step 3: create true PIs + //**************************************************************** + Saig_ManForEachPi( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreateCi( pNewAig ); + } + + //**************************************************************** + // Step 4: create register outputs + //**************************************************************** + Saig_ManForEachLo( pAig, pObj, i ) + { + loCopied++; + pObj->pData = Aig_ObjCreateCi( pNewAig ); + } + + //**************************************************************** + // Step 4.a: create register outputs for the barrier flops + //**************************************************************** + vBarrierLo = createArenaLO( pNewAig, vBarriers ); + loCreated = Vec_PtrSize(vBarrierLo); + + //**************************************************************** + // Step 4.b: create register output for arenaViolationFlop + //**************************************************************** + pObjArenaViolationLo = Aig_ObjCreateCi( pNewAig ); + loCreated++; + +#ifdef BARRIER_MONOTONE_TEST + //**************************************************************** + // Step 4.c: create register output for pendingFlop + //**************************************************************** + pObjPendingFlopLo = Aig_ObjCreateCi( pNewAig ); + loCreated++; + + //**************************************************************** + // Step 4.d: create register outputs for the barrier flops + // for asserting monotonicity + //**************************************************************** + vMonotoneBarrierLo = createMonotoneBarrierLO( pNewAig, vBarriers ); + loCreated = loCreated + Vec_PtrSize(vMonotoneBarrierLo); +#endif + + //******************************************************************** + // Step 5: create internal nodes + //******************************************************************** + Aig_ManForEachNode( pAig, pObj, i ) + { + pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + } + + //******************************************************************** + // Step 5.a: create internal nodes corresponding to arenaViolation + //******************************************************************** + pObjTarget = Aig_ManCo( pAig, windowBeginIndex ); + pObjWindowBeginsNew = driverToPoNew( pAig, pObjTarget ); + + pObjTarget = Aig_ManCo( pAig, withinWindowIndex ); + pObjWithinWindowNew = driverToPoNew( pAig, pObjTarget ); + + vBarrierLiDriver = Vec_PtrAlloc( Vec_PtrSize(vBarriers) ); + vMonotoneNodes = Vec_PtrAlloc( Vec_PtrSize(vBarriers) ); + + pObjArenaViolation = createArenaViolation( pAig, pNewAig, + pObjWindowBeginsNew, pObjWithinWindowNew, + vBarriers, vBarrierLo, vBarrierLiDriver, vMonotoneNodes ); + assert( Vec_PtrSize(vMonotoneNodes) == Vec_PtrSize(vBarriers) ); + +#ifdef ARENA_VIOLATION_CONSTRAINT + +#endif + + pObjArenaViolationLiDriver = Aig_Or( pNewAig, pObjArenaViolation, pObjArenaViolationLo ); + +#ifdef BARRIER_MONOTONE_TEST + //******************************************************************** + // Step 5.b: Create internal nodes for monotone testing + //******************************************************************** + + pObjTarget = Aig_ManCo( pAig, pendingSignalIndex ); + pObjPendingSignal = driverToPoNew( pAig, pObjTarget ); + + pObjPendingAndPendingSignal = Aig_And( pNewAig, pObjPendingSignal, pObjPendingFlopLo ); + pObjMonotoneAnd = Aig_ManConst1( pNewAig ); + Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i ) + { + pObjCurrMonotoneLo = (Aig_Obj_t *)Vec_PtrEntry(vMonotoneBarrierLo, i); + pObjMonotoneAnd = Aig_And( pNewAig, pObjMonotoneAnd, + Aig_Or( pNewAig, + Aig_Not(Aig_And(pNewAig, pObjPendingAndPendingSignal, pObjCurrMonotoneLo)), + pObj ) ); + } +#endif + + //******************************************************************** + // Step 6: create primary outputs + //******************************************************************** + + Saig_ManForEachPo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); + } + + pObjNewPoDriver = createConstrained0LiveConeWithDSC( pNewAig, signalList ); + pObjNewPoDriverArenaViolated = Aig_Or( pNewAig, pObjNewPoDriver, pObjArenaViolationLo ); +#ifdef BARRIER_MONOTONE_TEST + pObjNewPoDriverArenaViolated = Aig_And( pNewAig, pObjNewPoDriverArenaViolated, pObjMonotoneAnd ); +#endif + Aig_ObjCreateCo( pNewAig, pObjNewPoDriverArenaViolated ); + + *index0Live = i; + + //******************************************************************** + // Step 7: create register inputs + //******************************************************************** + + Saig_ManForEachLi( pAig, pObj, i ) + { + liCopied++; + pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); + } + + //******************************************************************** + // Step 7.a: create register inputs for barrier flops + //******************************************************************** + assert( Vec_PtrSize(vBarrierLiDriver) == Vec_PtrSize(vBarriers) ); + vBarrierLi = createArenaLi( pNewAig, vBarriers, vBarrierLiDriver ); + liCreated = Vec_PtrSize( vBarrierLi ); + + //******************************************************************** + // Step 7.b: create register inputs for arenaViolation flop + //******************************************************************** + Aig_ObjCreateCo( pNewAig, pObjArenaViolationLiDriver ); + liCreated++; + +#ifdef BARRIER_MONOTONE_TEST + //**************************************************************** + // Step 7.c: create register input for pendingFlop + //**************************************************************** + Aig_ObjCreateCo( pNewAig, pObjPendingSignal); + liCreated++; + + //******************************************************************** + // Step 7.d: create register inputs for the barrier flops + // for asserting monotonicity + //******************************************************************** + Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i ) + { + Aig_ObjCreateCo( pNewAig, pObj ); + liCreated++; + } +#endif + + assert(loCopied + loCreated == liCopied + liCreated); + //next step should be changed + Aig_ManSetRegNum( pNewAig, loCopied + loCreated ); + Aig_ManCleanup( pNewAig ); + + assert( Aig_ManCheck( pNewAig ) ); + + Vec_PtrFree(vBarrierLo); + Vec_PtrFree(vMonotoneBarrierLo); + Vec_PtrFree(vBarrierLiDriver); + Vec_PtrFree(vBarrierLi); + Vec_PtrFree(vMonotoneNodes); + + return pNewAig; +} + +Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers ) +{ + Vec_Ptr_t *vSignalVector; + Aig_Man_t *pAigNew; + int pObjWithinWindow; + int pObjWindowBegin; + int pObjPendingSignal; + + vSignalVector = collectCSSignalsWithDSC( pNtk, pAig ); + + pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig ); + pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig ); + pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig ); + + pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers ); + Vec_PtrFree(vSignalVector); + + return pAigNew; +} + +ABC_NAMESPACE_IMPL_END |