arenaViolation.c File Reference

#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 dependency graph for arenaViolation.c:

Go to the source code of this file.

Macros
#define	BARRIER_MONOTONE_TEST

Functions
ABC_NAMESPACE_IMPL_START Vec_Ptr_t *	createArenaLO (Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
Vec_Ptr_t *	createArenaLi (Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal)
Vec_Ptr_t *	createMonotoneBarrierLO (Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
Aig_Obj_t *	driverToPoNew (Aig_Man_t *pAig, Aig_Obj_t *pObjPo)
Vec_Ptr_t *	collectBarrierDisjunctions (Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
Aig_Obj_t *	Aig_Xor (Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *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 *	createConstrained0LiveConeWithDSC (Aig_Man_t *pNewAig, Vec_Ptr_t *signalList)
Vec_Ptr_t *	collectCSSignalsWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
int	collectWindowBeginSignalWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
int	collectWithinWindowSignalWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
int	collectPendingSignalWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
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_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 *	generateWorkingAigWithDSC (Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers)

Macro Definition Documentation

BARRIER_MONOTONE_TEST

#define BARRIER_MONOTONE_TEST

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.]

Definition at line 29 of file arenaViolation.c.

Function Documentation

Aig_Xor()

Aig_Obj_t * Aig_Xor	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pObj1,
		Aig_Obj_t *	pObj2 )

Definition at line 160 of file arenaViolation.c.

{
    return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

collectBarrierDisjunctions()

Vec_Ptr_t * collectBarrierDisjunctions	(	Aig_Man_t *	pAigOld,
		Aig_Man_t *	pAigNew,
		Vec_Ptr_t *	vBarriers )

Definition at line 124 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

collectCSSignalsWithDSC()

Vec_Ptr_t * collectCSSignalsWithDSC	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig )

Definition at line 235 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

collectPendingSignalWithDSC()

int collectPendingSignalWithDSC	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig )

Definition at line 285 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

collectWindowBeginSignalWithDSC()

int collectWindowBeginSignalWithDSC	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig )

Definition at line 255 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

collectWithinWindowSignalWithDSC()

int collectWithinWindowSignalWithDSC	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig )

Definition at line 271 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

createAndGateForMonotonicityVerification()

Aig_Obj_t * createAndGateForMonotonicityVerification	(	Aig_Man_t *	pNewAig,
		Vec_Ptr_t *	vDisjunctionSignals,
		Vec_Ptr_t *	vDisjunctionLo,
		Aig_Obj_t *	pendingLo,
		Aig_Obj_t *	pendingSignal )

Definition at line 299 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

createArenaLi()

Vec_Ptr_t * createArenaLi	(	Aig_Man_t *	pAigNew,
		Vec_Ptr_t *	vBarriers,
		Vec_Ptr_t *	vArenaSignal )

Definition at line 57 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

createArenaLO()

ABC_NAMESPACE_IMPL_START Vec_Ptr_t * createArenaLO	(	Aig_Man_t *	pAigNew,
		Vec_Ptr_t *	vBarriers )

Definition at line 33 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

createArenaViolation()

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 )

Definition at line 165 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

createConstrained0LiveConeWithDSC()

Aig_Obj_t * createConstrained0LiveConeWithDSC	(	Aig_Man_t *	pNewAig,
		Vec_Ptr_t *	signalList )

Definition at line 212 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

createMonotoneBarrierLO()

Vec_Ptr_t * createMonotoneBarrierLO	(	Aig_Man_t *	pAigNew,
		Vec_Ptr_t *	vBarriers )

Definition at line 82 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

createNewAigWith0LivePoWithDSC()

Aig_Man_t * createNewAigWith0LivePoWithDSC	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	signalList,
		int *	index0Live,
		int	windowBeginIndex,
		int	withinWindowIndex,
		int	pendingSignalIndex,
		Vec_Ptr_t *	vBarriers )

Definition at line 323 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

driverToPoNew()

Aig_Obj_t * driverToPoNew	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pObjPo )

Definition at line 106 of file arenaViolation.c.

{
    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;
}

Here is the caller graph for this function:

generateWorkingAigWithDSC()

Aig_Man_t * generateWorkingAigWithDSC	(	Aig_Man_t *	pAig,
		Abc_Ntk_t *	pNtk,
		int *	pIndex0Live,
		Vec_Ptr_t *	vMasterBarriers )

Definition at line 529 of file arenaViolation.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function: