abs.h File Reference

#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"

Include dependency graph for abs.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Abs_Par_t_
struct	Gia_ParAbs_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_	Abs_Par_t
	INCLUDES ///.
typedef struct Gia_ParAbs_t_	Gia_ParAbs_t

Functions
Gia_Man_t *	Gia_ManDupAbsFlops (Gia_Man_t *p, Vec_Int_t *vFlopClasses)
	FUNCTION DECLARATIONS ///.
Gia_Man_t *	Gia_ManDupAbsGates (Gia_Man_t *p, Vec_Int_t *vGateClasses)
void	Gia_ManGlaCollect (Gia_Man_t *p, Vec_Int_t *vGateClasses, Vec_Int_t **pvPis, Vec_Int_t **pvPPis, Vec_Int_t **pvFlops, Vec_Int_t **pvNodes)
void	Gia_ManPrintFlopClasses (Gia_Man_t *p)
void	Gia_ManPrintObjClasses (Gia_Man_t *p)
void	Gia_ManPrintGateClasses (Gia_Man_t *p)
int	Gia_ManPerformGla (Gia_Man_t *p, Abs_Par_t *pPars)
int	Gia_ManPerformGlaOld (Gia_Man_t *p, Abs_Par_t *pPars, int fStartVta)
Gia_Man_t *	Gia_ManShrinkGla (Gia_Man_t *p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose)
void	Gia_GlaProveAbsracted (Gia_Man_t *p, int fSimpProver, int fVerbose)
	DECLARATIONS ///.
void	Gia_GlaProveCancel (int fVerbose)
int	Gia_GlaProveCheck (int fVerbose)
int	Gia_VtaPerform (Gia_Man_t *pAig, Abs_Par_t *pPars)
void	Abs_ParSetDefaults (Abs_Par_t *p)
	DECLARATIONS ///.
Vec_Int_t *	Gia_VtaConvertToGla (Gia_Man_t *p, Vec_Int_t *vVta)
Vec_Int_t *	Gia_VtaConvertFromGla (Gia_Man_t *p, Vec_Int_t *vGla, int nFrames)
Vec_Int_t *	Gia_FlaConvertToGla (Gia_Man_t *p, Vec_Int_t *vFla)
Vec_Int_t *	Gia_GlaConvertToFla (Gia_Man_t *p, Vec_Int_t *vGla)
int	Gia_GlaCountFlops (Gia_Man_t *p, Vec_Int_t *vGla)
int	Gia_GlaCountNodes (Gia_Man_t *p, Vec_Int_t *vGla)
Gia_Man_t *	Abs_RpmPerform (Gia_Man_t *p, int nCutMax, int fVerbose, int fVeryVerbose)
Gia_Man_t *	Abs_RpmPerformOld (Gia_Man_t *p, int fVerbose)
void	Gia_ManAbsSetDefaultParams (Gia_ParAbs_t *p)
	DECLARATIONS ///.
Vec_Int_t *	Saig_ManCexAbstractionFlops (Aig_Man_t *p, Gia_ParAbs_t *pPars)
Vec_Int_t *	Saig_ManCbaFilterFlops (Aig_Man_t *pAig, Abc_Cex_t *pAbsCex, Vec_Int_t *vFlopClasses, Vec_Int_t *vAbsFfsToAdd, int nFfsToSelect)
	FUNCTION DEFINITIONS ///.
Abc_Cex_t *	Saig_ManCbaFindCexCareBits (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
int	Gia_ManCexAbstractionRefine (Gia_Man_t *pGia, Abc_Cex_t *pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose)
Vec_Int_t *	Saig_ManExtendCounterExampleTest3 (Aig_Man_t *pAig, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
Vec_Int_t *	Saig_ManExtendCounterExampleTest2 (Aig_Man_t *p, int iFirstPi, Abc_Cex_t *pCex, int fVerbose)

Typedef Documentation

Abs_Par_t

typedef typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t

INCLUDES ///.

CFile****************************************************************

FileName [abs.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 46 of file abs.h.

Gia_ParAbs_t

typedef struct Gia_ParAbs_t_ Gia_ParAbs_t

Definition at line 84 of file abs.h.

Function Documentation

Abs_ParSetDefaults()

void Abs_ParSetDefaults ( Abs_Par_t * p )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [absUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Interface to pthreads.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

absUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file absUtil.c.

{
    memset( p, 0, sizeof(Abs_Par_t) );
    p->nFramesMax         =      0;   // maximum frames
    p->nFramesStart       =      0;   // starting frame 
    p->nFramesPast        =      4;   // overlap frames
    p->nConfLimit         =      0;   // conflict limit
    p->nLearnedMax        =   1000;   // max number of learned clauses
    p->nLearnedStart      =   1000;   // max number of learned clauses
    p->nLearnedDelta      =    200;   // max number of learned clauses
    p->nLearnedPerce      =     70;   // max number of learned clauses
    p->nTimeOut           =      0;   // timeout in seconds
    p->nRatioMin          =      0;   // stop when less than this % of object is abstracted
    p->nRatioMax          =     30;   // restart when more than this % of object is abstracted
    p->fUseTermVars       =      0;   // use terminal variables
    p->fUseRollback       =      0;   // use rollback to the starting number of frames
    p->fPropFanout        =      1;   // propagate fanouts during refinement
    p->fVerbose           =      0;   // verbose flag
    p->iFrame             =     -1;   // the number of frames covered 
    p->iFrameProved       =     -1;   // the number of frames proved
    p->nFramesNoChangeLim =      2;   // the number of frames without change to dump abstraction
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abs_RpmPerform()

Gia_Man_t * Abs_RpmPerform ( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose )

extern

Function*************************************************************

Synopsis [Performs structural reparametrization.]

Description []

SideEffects []

SeeAlso []

Definition at line 853 of file absRpm.c.

{
    Gia_Man_t * pNew;
//    Gia_ManTestDoms( p );
//    return NULL;
    // perform structural analysis
    Gia_ObjComputeTruthTableStart( p, nCutMax );
    Abs_RpmPerformMark( p, nCutMax, fVerbose, fVeryVerbose );
    Gia_ObjComputeTruthTableStop( p );
    // derive new AIG
    pNew = Gia_ManDupRpm( p );
    Gia_ManCleanMark1( p );
    return pNew;
}

Here is the call graph for this function:

Abs_RpmPerformOld()

Gia_Man_t * Abs_RpmPerformOld ( Gia_Man_t * p, int fVerbose )

extern

Function*************************************************************

Synopsis [Reparameterized to get rid of useless primary inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file absRpmOld.c.

{
//    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
    Aig_Man_t * pMan, * pTemp;
    Gia_Man_t * pNew, * pTmp;
    int nFlopsOld = Gia_ManRegNum(p);
    if ( fVerbose )
    {
        printf( "Original AIG:\n" );
        Gia_ManPrintStats( p, NULL );
    }
 
    // perform input trimming
    pNew = Gia_ManDupTrimmed( p, 1, 0, 0, -1 );
    if ( fVerbose )
    {
        printf( "After PI trimming:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }
    // transform GIA
    pNew = Gia_ManDupIn2Ff( pTmp = pNew );
    Gia_ManStop( pTmp );
    if ( fVerbose )
    {
        printf( "After PI-2-FF transformation:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }
 
    // derive AIG
    pMan = Gia_ManToAigSimple( pNew );
    Gia_ManStop( pNew );
    // perform min-reg retiming
    pMan = Saig_ManRetimeMinArea( pTemp = pMan, 10, 0, 0, 1, 0 );
    Aig_ManStop( pTemp );
    // derive GIA
    pNew = Gia_ManFromAigSimple( pMan );
    Aig_ManStop( pMan );
    if ( fVerbose )
    {
        printf( "After min-area retiming:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }
 
    // transform back
    pNew = Gia_ManDupFf2In( pTmp = pNew, nFlopsOld );
    Gia_ManStop( pTmp );
    if ( fVerbose )
    {
        printf( "After FF-2-PI transformation:\n" );
        Gia_ManPrintStats( pNew, NULL );
    }
    return pNew;
}

Here is the call graph for this function:

Gia_FlaConvertToGla()

Vec_Int_t * Gia_FlaConvertToGla ( Gia_Man_t * p, Vec_Int_t * vFla )

extern

Function*************************************************************

Synopsis [Converting FLA vector to GLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file absUtil.c.

{
    Vec_Int_t * vGla;
    Gia_Obj_t * pObj;
    int i;
    // mark const0 and relevant CI objects
    Gia_ManIncrementTravId( p );
    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
    Gia_ManForEachPi( p, pObj, i )
        Gia_ObjSetTravIdCurrent(p, pObj);
    Gia_ManForEachRo( p, pObj, i )
        if ( !Vec_IntEntry(vFla, i) )
            Gia_ObjSetTravIdCurrent(p, pObj);
    // label all objects reachable from the PO and selected flops
    vGla = Vec_IntStart( Gia_ManObjNum(p) );
    Vec_IntWriteEntry( vGla, 0, 1 );
    Gia_ManForEachPo( p, pObj, i )
        Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    Gia_ManForEachRi( p, pObj, i )
        if ( Vec_IntEntry(vFla, i) )
            Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
    return vGla;
}

Here is the call graph for this function:

Gia_GlaConvertToFla()

Vec_Int_t * Gia_GlaConvertToFla ( Gia_Man_t * p, Vec_Int_t * vGla )

extern

Function*************************************************************

Synopsis [Converting GLA vector to FLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file absUtil.c.

{
    Vec_Int_t * vFla;
    Gia_Obj_t * pObj;
    int i;
    vFla = Vec_IntStart( Gia_ManRegNum(p) );
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Vec_IntWriteEntry( vFla, i, 1 );
    return vFla;
}

Gia_GlaCountFlops()

int Gia_GlaCountFlops ( Gia_Man_t * p, Vec_Int_t * vGla )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 231 of file absUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Count = 0;
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Count++;
    return Count;
}

Here is the caller graph for this function:

Gia_GlaCountNodes()

int Gia_GlaCountNodes ( Gia_Man_t * p, Vec_Int_t * vGla )

extern

Definition at line 240 of file absUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Count = 0;
    Gia_ManForEachAnd( p, pObj, i )
        if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
            Count++;
    return Count;
}

Here is the caller graph for this function:

Gia_GlaProveAbsracted()

void Gia_GlaProveAbsracted ( Gia_Man_t * p, int fSimpProver, int fVerbose )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [absPth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Interface to pthreads.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

absPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 45 of file absPth.c.

{}

Here is the caller graph for this function:

Gia_GlaProveCancel()

void Gia_GlaProveCancel ( int fVerbose )

extern

Definition at line 46 of file absPth.c.

{}

Here is the caller graph for this function:

Gia_GlaProveCheck()

int Gia_GlaProveCheck ( int fVerbose )

extern

Definition at line 47 of file absPth.c.

{ return 0; }

Here is the caller graph for this function:

Gia_ManAbsSetDefaultParams()

void Gia_ManAbsSetDefaultParams ( Gia_ParAbs_t * p )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [saigAbsStart.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Counter-example-based abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

saigAbsStart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file absOldRef.c.

{
    memset( p, 0, sizeof(Gia_ParAbs_t) );
    p->Algo        =        0;    // algorithm: CBA
    p->nFramesMax  =       10;    // timeframes for PBA
    p->nConfMax    =    10000;    // conflicts for PBA
    p->fDynamic    =        1;    // dynamic unfolding for PBA
    p->fConstr     =        0;    // use constraints
    p->nFramesBmc  =      250;    // timeframes for BMC
    p->nConfMaxBmc =     5000;    // conflicts for BMC
    p->nStableMax  =  1000000;    // the number of stable frames to quit
    p->nRatio      =       10;    // ratio of flops to quit
    p->nBobPar     =  1000000;    // the number of frames before trying to quit
    p->fUseBdds    =        0;    // use BDDs to refine abstraction
    p->fUseDprove  =        0;    // use 'dprove' to refine abstraction
    p->fUseStart   =        1;    // use starting frame
    p->fVerbose    =        0;    // verbose output
    p->fVeryVerbose=        0;    // printing additional information
    p->Status      =       -1;    // the problem status
    p->nFramesDone =       -1;    // the number of rames covered
}

Here is the call graph for this function:

Gia_ManCexAbstractionRefine()

int Gia_ManCexAbstractionRefine ( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose )

extern

Function*************************************************************

Synopsis [Refines abstraction using the latch map.]

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file absOldRef.c.

{
    Aig_Man_t * pNew;
    Vec_Int_t * vFlops;
    if ( pGia->vFlopClasses == NULL )
    {
        printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" );
        return -1;
    }
    pNew = Gia_ManToAig( pGia, 0 );
    vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses );
    if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) )
    {
        pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
        Vec_IntFree( vFlops );
        Aig_ManStop( pNew );
        return 0;
    }
    Vec_IntFree( pGia->vFlopClasses );
    pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
    Vec_IntFree( vFlops );
    Aig_ManStop( pNew );
    return -1;
}

Here is the call graph for this function:

Gia_ManDupAbsFlops()

Gia_Man_t * Gia_ManDupAbsFlops ( Gia_Man_t * p, Vec_Int_t * vFlopClasses )

extern

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Extractes a flop-level abstraction given a flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file absDup.c.

{ 
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj;
    int i, nFlops = 0;
    Gia_ManFillValue( p );
    // start the new manager
    pNew = Gia_ManStart( 5000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create PIs
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachPi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create additional PIs
    Gia_ManForEachRo( p, pObj, i )
        if ( !Vec_IntEntry(vFlopClasses, i) )
            pObj->Value = Gia_ManAppendCi(pNew);
    // create ROs
    Gia_ManForEachRo( p, pObj, i )
        if ( Vec_IntEntry(vFlopClasses, i) )
            pObj->Value = Gia_ManAppendCi(pNew);
    // create POs
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachPo( p, pObj, i )
    {
        Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    // create RIs
    Gia_ManForEachRi( p, pObj, i )
        if ( Vec_IntEntry(vFlopClasses, i) )
        {
            Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
            nFlops++;
        }
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, nFlops );
    // clean up
    pNew = Gia_ManSeqCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Here is the call graph for this function:

Gia_ManDupAbsGates()

Gia_Man_t * Gia_ManDupAbsGates ( Gia_Man_t * p, Vec_Int_t * vGateClasses )

extern

Function*************************************************************

Synopsis [Extractes a gate-level abstraction given a gate map.]

Description [The array contains 1 for those objects (const, RO, AND) that are included in the abstraction; 0, otherwise.]

SideEffects []

SeeAlso []

Definition at line 220 of file absDup.c.

{ 
    Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pCopy;
    int i;//, nFlops = 0;
    assert( Gia_ManPoNum(p) == 1 );
    assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
 
    // create additional arrays
    Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
 
    // start the new manager
    pNew = Gia_ManStart( 5000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create constant
    Gia_ManFillValue( p );
    Gia_ManConst0(p)->Value = 0;
    // create PIs
    Gia_ManForEachObjVec( vPis, p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create additional PIs
    Gia_ManForEachObjVec( vPPis, p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create ROs
    Gia_ManForEachObjVec( vFlops, p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    // create internal nodes
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
//        Gia_ManDupAbsGates_rec( pNew, pObj );
    // create PO
    Gia_ManForEachPo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    // create RIs
    Gia_ManForEachObjVec( vFlops, p, pObj, i )
        Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
    Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
    // clean up
    pNew = Gia_ManSeqCleanup( pTemp = pNew );
    // transfer copy values: (p -> pTemp -> pNew) => (p -> pNew)
    if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) )
    {
//        printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" );
        Gia_ManForEachObj( p, pObj, i )
        {
            if ( !~pObj->Value )
                continue;
            assert( !Abc_LitIsCompl(pObj->Value) );
            pCopy = Gia_ObjCopy( pTemp, pObj );
            if ( !~pCopy->Value )
            {
                Vec_IntWriteEntry( vGateClasses, i, 0 );
                pObj->Value = ~0;
                continue;
            }
            assert( !Abc_LitIsCompl(pCopy->Value) );
            pObj->Value = pCopy->Value;
        }
    }
    Gia_ManStop( pTemp );
 
    Vec_IntFree( vPis );
    Vec_IntFree( vPPis );
    Vec_IntFree( vFlops );
    Vec_IntFree( vNodes );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManGlaCollect()

void Gia_ManGlaCollect ( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes )

extern

Function*************************************************************

Synopsis [Collects PIs and PPIs of the abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file absDup.c.

{ 
    Vec_Int_t * vAssigned;
    Gia_Obj_t * pObj;
    int i;
    assert( Gia_ManPoNum(p) == 1 );
    assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
    // create included objects and their fanins
    vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
    // create additional arrays
    if ( pvPis )   *pvPis   = Vec_IntAlloc( 100 );
    if ( pvPPis )  *pvPPis  = Vec_IntAlloc( 100 );
    if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 );
    if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 );
    Gia_ManForEachObjVec( vAssigned, p, pObj, i )
    {
        if ( Gia_ObjIsPi(p, pObj) )
            { if ( pvPis )   Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) );   }
        else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
            { if ( pvPPis )  Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) );  }
        else if ( Gia_ObjIsRo(p, pObj) )
            { if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); }
        else if ( Gia_ObjIsAnd(pObj) )
            { if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); }
        else assert( Gia_ObjIsConst0(pObj) );
    }
    Vec_IntFree( vAssigned );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManPerformGla()

int Gia_ManPerformGla ( Gia_Man_t * pAig, Abs_Par_t * pPars )

extern

Function*************************************************************

Synopsis [Performs gate-level abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 1500 of file absGla.c.

{
    int fUseSecondCore = 1;
    Ga2_Man_t * p;
    Vec_Int_t * vCore, * vPPis;
    abctime clk2, clk = Abc_Clock();
    int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
    int i, c, f, Lit;
    pPars->iFrame = -1;
    // check trivial case 
    assert( Gia_ManPoNum(pAig) == 1 ); 
    ABC_FREE( pAig->pCexSeq );
    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
    {
        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
        {
            Abc_Print( 1, "Sequential miter is trivially UNSAT.\n" );
            return 1;
        }
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        Abc_Print( 1, "Sequential miter is trivially SAT.\n" );
        return 0;
    }
    // create gate classes if not given
    if ( pAig->vGateClasses == NULL )
    {
        pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
        Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
        Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
    }
    // start the manager
    p = Ga2_ManStart( pAig, pPars );
    p->timeInit = Abc_Clock() - clk;
    // perform initial abstraction
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  Limit = %d %%  Limit2 = %d %%  RatioMax = %d %%\n", 
            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMin2, pPars->nRatioMax );
        Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
        if ( pPars->fDumpVabs || pPars->fDumpMabs )
            Abc_Print( 1, "%s will be continuously dumped into file \"%s\".\n", 
                pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
                Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
        if ( pPars->fDumpMabs )
        {
            {
                char Command[1000];
                Abc_FrameSetStatus( -1 );
                Abc_FrameSetCex( NULL );
                Abc_FrameSetNFrames( -1 );
                sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
            }
            {
                // create trivial abstraction map
                Gia_Obj_t * pObj; 
                char * pFileName = Ga2_GlaGetFileName(p, 0);
                Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
                pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
                Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
                Gia_ManForEachAnd( pAig, pObj, i )
                    Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
                Gia_ManForEachRo( pAig, pObj, i )
                    Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
                Gia_AigerWrite( pAig, pFileName, 0, 0, 0 );
                Vec_IntFree( pAig->vGateClasses );
                pAig->vGateClasses = vMap;
                if ( p->pPars->fVerbose )
                    Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
            }
        }
        Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
    }
    // iterate unrolling
    for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
    {
        int nAbsOld;
        // remember the timeframe
        p->pPars->iFrame = -1;
        // create new SAT solver
        Ga2_ManRestart( p );
        // remember abstraction size after the last restart
        nAbsOld = Vec_IntSize(p->vAbs);
        // unroll the circuit
        for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
        {
            // remember current limits
            int nConflsBeg = sat_solver2_nconflicts(p->pSat);
            int nAbs       = Vec_IntSize(p->vAbs);
            int nValues    = Vec_IntSize(p->vValues);
            int nVarsOld;
            // remember the timeframe
            p->pPars->iFrame = f;
            // extend and clear storage
            if ( f == Vec_PtrSize(p->vId2Lit) )
                Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
            Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
            // add static clauses to this timeframe
            Ga2_ManAddAbsClauses( p, f );
            // skip checking if skipcheck is enabled (&gla -s)
            if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved )
                continue;
            // skip checking if we need to skip several starting frames (&gla -S <num>)
            if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart )
                continue;
            // get the output literal
//            Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
            Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f );
            assert( Lit >= 0 );
            Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
            if ( Lit == 0 )
                continue;
            assert( Lit > 1 );
            // check for counter-examples
            if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
                sat_solver2_setnvars( p->pSat, p->nSatVars );
            nVarsOld = p->nSatVars;
            for ( c = 0; ; c++ )
            {
                // consider the special case when the target literal is implied false
                // by implications which happened as a result of previous refinements
                // note that incremental UNSAT core cannot be computed because there is no learned clauses
                // in this case, we will assume that UNSAT core cannot reduce the problem
                if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
                {
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    break;
                }
                // perform SAT solving
                clk2 = Abc_Clock();
                Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( Status == l_True ) // perform refinement
                {
                    p->nCexes++;
                    p->timeSat += Abc_Clock() - clk2;
 
                    // cancel old one if it was sent
                    if ( Abc_FrameIsBridgeMode() && fOneIsSent )
                    {
                        Gia_Ga2SendCancel( p, pPars->fVerbose );
                        fOneIsSent = 0;
                    }
                    if ( iFrameTryToProve >= 0 )
                    {
                        Gia_GlaProveCancel( pPars->fVerbose );
                        iFrameTryToProve = -1;
                    }
 
                    // perform refinement
                    clk2 = Abc_Clock();
                    Rnm_ManSetRefId( p->pRnm, c );
                    vPPis = Ga2_ManRefine( p );
                    p->timeCex += Abc_Clock() - clk2;
                    if ( vPPis == NULL )
                    {
                        if ( pPars->fVerbose )
                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
                        goto finish;
                    }
 
                    if ( c == 0 )
                    {
//                        Ga2_ManRefinePrintPPis( p );
                        // create bookmark to be used for rollback
                        assert( nVarsOld == p->pSat->size );
                        sat_solver2_bookmark( p->pSat );
                        // start incremental proof manager
                        assert( p->pSat->pPrf2 == NULL );
                        p->pSat->pPrf2 = Prf_ManAlloc();
                        if ( p->pSat->pPrf2 )
                        {
                            p->nProofIds = 0;
                            Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                            Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
                        }
                    }
                    else
                    {
                        // resize the proof logger
                        if ( p->pSat->pPrf2 )
                            Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
                    }
 
                    Ga2_ManAddToAbs( p, vPPis );
                    Vec_IntFree( vPPis );
                    if ( pPars->fVerbose )
                        Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 );
                    // check if the number of objects is below limit
                    if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
                    {
                        Status = l_Undef;
                        goto finish;
                    }
                    continue;
                }
                p->timeUnsat += Abc_Clock() - clk2;
                if ( Status == l_Undef ) // ran out of resources
                    goto finish;
                if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout
                    goto finish;
                if ( c == 0 )
                {
                    if ( f > p->pPars->iFrameProved )
                        p->pPars->nFramesNoChange++;
                    break;
                }
                if ( f > p->pPars->iFrameProved )
                    p->pPars->nFramesNoChange = 0;
 
                // derive the core
                assert( p->pSat->pPrf2 != NULL );
                vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                Prf_ManStopP( &p->pSat->pPrf2 );
                // update the SAT solver
                sat_solver2_rollback( p->pSat );
                // reduce abstraction
                Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
 
                // purify UNSAT core
                if ( fUseSecondCore )
                {
//                    int nOldCore = Vec_IntSize(vCore);
                    // reverse the order of objects in the core
//                    Vec_IntSort( vCore, 0 );
//                    Vec_IntPrint( vCore );
                    // create bookmark to be used for rollback
                    assert( nVarsOld == p->pSat->size );
                    sat_solver2_bookmark( p->pSat );
                    // start incremental proof manager
                    assert( p->pSat->pPrf2 == NULL );
                    p->pSat->pPrf2 = Prf_ManAlloc();
                    if ( p->pSat->pPrf2 )
                    {
                        p->nProofIds = 0;
                        Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                        Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) );
 
                        Ga2_ManAddToAbs( p, vCore );
                        Vec_IntFree( vCore );
                    }
                    // run SAT solver
                    clk2 = Abc_Clock();
                    Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                    if ( Status == l_Undef )
                        goto finish;
                    assert( Status == l_False );
                    p->timeUnsat += Abc_Clock() - clk2;
 
                    // derive the core
                    assert( p->pSat->pPrf2 != NULL );
                    vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    // update the SAT solver
                    sat_solver2_rollback( p->pSat );
                    // reduce abstraction
                    Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
//                    printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) );
                }
 
                Ga2_ManAddToAbs( p, vCore );
//                Ga2_ManRefinePrint( p, vCore );
                Vec_IntFree( vCore );
                break;
            }
            // remember the last proved frame
            if ( p->pPars->iFrameProved < f )
                p->pPars->iFrameProved = f;
            // print statistics
            if ( pPars->fVerbose )
                Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
            // check if abstraction was proved
            if ( Gia_GlaProveCheck( pPars->fVerbose ) )
            {
                RetValue = 1;
                goto finish;
            }
            if ( c > 0 ) 
            {
                if ( p->pPars->fVeryVerbose )
                    Abc_Print( 1, "\n" );
                // recompute the abstraction
                Vec_IntFreeP( &pAig->vGateClasses );
                pAig->vGateClasses = Ga2_ManAbsTranslate( p );
                // check if the number of objects is below limit
                if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
                {
                    Status = l_Undef;
                    goto finish;
                }
            }
            // check the number of stable frames
            if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
            {
                // dump the model into file
                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
                {
                    char Command[1000];
                    Abc_FrameSetStatus( -1 );
                    Abc_FrameSetCex( NULL );
                    Abc_FrameSetNFrames( f );
                    sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
                    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                    Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
                }
                // call the prover
                if ( p->pPars->fCallProver )
                {
                    // cancel old one if it is proving
                    if ( iFrameTryToProve >= 0 )
                        Gia_GlaProveCancel( pPars->fVerbose );
                    // prove new one
                    Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose );
                    iFrameTryToProve = f;
                    p->nPdrCalls++;
                }
                // speak to the bridge
                if ( Abc_FrameIsBridgeMode() )
                {
                    // cancel old one if it was sent
                    if ( fOneIsSent )
                        Gia_Ga2SendCancel( p, pPars->fVerbose );
                    // send new one 
                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
                    fOneIsSent = 1;
                }
            }
            // if abstraction grew more than a certain percentage, force a restart
            if ( pPars->nRatioMax == 0 )
                continue;
            if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
            {
                if ( p->pPars->fVerbose )
                Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
                    nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
                break;
            }
        }
    }
finish:
    Prf_ManStopP( &p->pSat->pPrf2 );
    // cancel old one if it is proving
    if ( iFrameTryToProve >= 0 )
        Gia_GlaProveCancel( pPars->fVerbose );
    // analize the results
    if ( !p->fUseNewLine )
        Abc_Print( 1, "\n" );
    if ( RetValue == 1 )
        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d  ", p->pPars->iFrameProved+1, iFrameTryToProve );
    else if ( pAig->pCexSeq == NULL )
    {
        Vec_IntFreeP( &pAig->vGateClasses );
        pAig->vGateClasses = Ga2_ManAbsTranslate( p );
        if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
            Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
            Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
            Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement.  ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
        else if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
            Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d.  ", pPars->nRatioMin, p->pPars->iFrameProved+1 );
        else
            Abc_Print( 1, "GLA finished %d frames and produced a %d-stable abstraction.  ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        p->pPars->iFrame = p->pPars->iFrameProved;
    }
    else
    {
        if ( p->pPars->fVerbose )
            Abc_Print( 1, "\n" );
        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
            Abc_Print( 1, "    Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
        Abc_Print( 1, "True counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = f - 1;
        Vec_IntFreeP( &pAig->vGateClasses );
        RetValue = 0;
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( p->pPars->fVerbose )
    {
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
        ABC_PRTP( "Runtime: Initializing", p->timeInit,   Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
        Ga2_ManReportMemory( p );
    }
//    Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
    Ga2_ManStop( p );
    fflush( stdout );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManPerformGlaOld()

int Gia_ManPerformGlaOld ( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )

extern

Function*************************************************************

Synopsis [Performs gate-level abstraction]

Description []

SideEffects []

SeeAlso []

Definition at line 1638 of file absGlaOld.c.

{
    extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars );
    extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
    Gla_Man_t * p;
    Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
    Abc_Cex_t * pCex = NULL;
    int f, i, iPrev, nConfls, Status, nVarsOld = 0, nCoreSize, fOneIsSent = 0, RetValue = -1;
    abctime clk2, clk = Abc_Clock();
    // preconditions
    assert( Gia_ManPoNum(pAig) == 1 );
    assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
    {
        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
        {
            printf( "Sequential miter is trivially UNSAT.\n" );
            return 1;
        }
        ABC_FREE( pAig->pCexSeq );
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        printf( "Sequential miter is trivially SAT.\n" );
        return 0;
    }
 
    // compute intial abstraction
    if ( pAig->vGateClasses == NULL )
    {
        if ( fStartVta )
        {
            int nFramesMaxOld   = pPars->nFramesMax;
            int nFramesStartOld = pPars->nFramesStart;
            int nTimeOutOld     = pPars->nTimeOut;
            int nDumpOld        = pPars->fDumpVabs;
            pPars->nFramesMax   = pPars->nFramesStart;
            pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
            pPars->nTimeOut     = 20;
            pPars->fDumpVabs    = 0;
            RetValue = Gia_VtaPerformInt( pAig, pPars );
            pPars->nFramesMax   = nFramesMaxOld;
            pPars->nFramesStart = nFramesStartOld;
            pPars->nTimeOut     = nTimeOutOld;
            pPars->fDumpVabs    = nDumpOld;
            // create gate classes
            Vec_IntFreeP( &pAig->vGateClasses );
            if ( pAig->vObjClasses )
                pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
            Vec_IntFreeP( &pAig->vObjClasses );
            // return if VTA solve the problem if could not start
            if ( RetValue == 0 || pAig->vGateClasses == NULL )
                return RetValue;
        }
        else
        {
            pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
            Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
            Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
        }
    }
    // start the manager
    p = Gla_ManStart( pAig, pPars );
    p->timeInit = Abc_Clock() - clk;
    // set runtime limit
    if ( p->pPars->nTimeOut )
        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
    // perform initial abstraction
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  RatioMin = %d %%.\n", 
            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
        Abc_Print( 1, "LearnStart = %d  LearnDelta = %d  LearnRatio = %d %%.\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
        Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
    }
    for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
    {
        int nConflsBeg = sat_solver2_nconflicts(p->pSat);
        p->pPars->iFrame = f;
 
        // load timeframe
        Gia_GlaAddTimeFrame( p, f );
 
        // iterate as long as there are counter-examples
        for ( i = 0; ; i++ )
        { 
            clk2 = Abc_Clock();
            vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
//            assert( (vCore != NULL) == (Status == 1) );
            if ( Status == -1 || (p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
            {
                Prf_ManStopP( &p->pSat->pPrf2 );
//                if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstraction
//                    Vec_IntShrink( p->vAbs, p->nAbsOld );
                goto finish;
            }
            if ( Status == 1 )
            {
                Prf_ManStopP( &p->pSat->pPrf2 );
                p->timeUnsat += Abc_Clock() - clk2;
                break;
            } 
            p->timeSat += Abc_Clock() - clk2;
            assert( Status == 0 );
            p->nCexes++;
 
            // cancel old one if it was sent
            if ( Abc_FrameIsBridgeMode() && fOneIsSent )
            {
                Gia_GlaSendCancel( p, pPars->fVerbose );
                fOneIsSent = 0;
            }
 
            // perform the refinement
            clk2 = Abc_Clock();
            if ( pPars->fAddLayer )
            {
                vPPis = Gla_ManCollectPPis( p, NULL );
//                Gla_ManExplorePPis( p, vPPis );
            }
            else
            {
                vPPis = Gla_ManRefinement( p );
                if ( vPPis == NULL )
                {
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
                    break;
                }
            } 
            assert( pCex == NULL );
 
            // start proof logging
            if ( i == 0 )
            {
                // create bookmark to be used for rollback
                sat_solver2_bookmark( p->pSat );
                Vec_IntClear( p->vAddedNew );
                p->nAbsOld = Vec_IntSize( p->vAbs );
                nVarsOld = p->nSatVars;
//                p->nLrnOld = sat_solver2_nlearnts( p->pSat );
//                p->nAbsNew = 0;
//                p->nLrnNew = 0;
 
                // start incremental proof manager
                assert( p->pSat->pPrf2 == NULL );
                if ( p->pSat->pPrf1 == NULL )
                    p->pSat->pPrf2 = Prf_ManAlloc();
                if ( p->pSat->pPrf2 )
                {
                    p->nProofIds = 0;
                    Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                    Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
                }
            }
            else
            {
                // resize the proof logger
                if ( p->pSat->pPrf2 )
                    Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
            }
 
            Gia_GlaAddToAbs( p, vPPis, 1 );
            Gia_GlaAddOneSlice( p, f, vPPis );
            Vec_IntFree( vPPis );
 
            // print the result (do not count it towards change)
            if ( p->pPars->fVerbose )
            Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
        }
        if ( pCex != NULL )
            break;
        assert( Status == 1 );
 
        // valid core is obtained
        nCoreSize = 1;
        if ( vCore )
        {
            nCoreSize += Vec_IntSize( vCore );
            Gia_GlaAddToCounters( p, vCore );
        }
        if ( i == 0 )
        {
            p->pPars->nFramesNoChange++;
            Vec_IntFreeP( &vCore );
        }
        else
        {
            p->pPars->nFramesNoChange = 0;
//            p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld;
//            p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld );
            // update the SAT solver
            sat_solver2_rollback( p->pSat );
            // update storage
            Gla_ManRollBack( p );
            p->nSatVars = nVarsOld;
            // load this timeframe
            Gia_GlaAddToAbs( p, vCore, 0 );
            Gia_GlaAddOneSlice( p, f, vCore );
            Vec_IntFree( vCore );
            // run SAT solver
            clk2 = Abc_Clock();
            vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
            p->timeUnsat += Abc_Clock() - clk2;
//            assert( (vCore != NULL) == (Status == 1) );
            Vec_IntFreeP( &vCore );
            if ( Status == -1 ) // resource limit is reached
                break;
            if ( Status == 0 )
            {
                assert( 0 );
    //            Vta_ManSatVerify( p );
                // make sure, there was no initial abstraction (otherwise, it was invalid)
                assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
    //            pCex = Vga_ManDeriveCex( p );
                break;
            }
        }
        // print the result
        if ( p->pPars->fVerbose )
        Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
 
        if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened
        {
            if ( Abc_FrameIsBridgeMode() )
            {
                // cancel old one if it was sent
                if ( fOneIsSent )
                    Gia_GlaSendCancel( p, pPars->fVerbose );
                // send new one 
                Gia_GlaSendAbsracted( p, pPars->fVerbose );
                fOneIsSent = 1;
            }
 
            // dump the model into file
            if ( p->pPars->fDumpVabs )
            {
                char Command[1000];
                Abc_FrameSetStatus( -1 );
                Abc_FrameSetCex( NULL );
                Abc_FrameSetNFrames( f+1 );
                sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status") );
                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                Gia_GlaDumpAbsracted( p, pPars->fVerbose );
            }
        }
 
        // check if the number of objects is below limit
        if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
        {
            Status = -1;
            break;
        }
    }
finish:
    // analize the results
    if ( pCex == NULL )
    {
        if ( p->pPars->fVerbose && Status == -1 )
            printf( "\n" );
//        if ( pAig->vGateClasses != NULL )
//            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
        Vec_IntFreeP( &pAig->vGateClasses );
        pAig->vGateClasses = Gla_ManTranslate( p );
        if ( Status == -1 )
        {
            if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
                Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
            else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
            else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
                Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, f );
            else
                Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d.  ", f );
        }
        else
        {
            p->pPars->iFrame++;
            Abc_Print( 1, "GLA completed %d frames with a %d-stable abstraction.  ", f, p->pPars->nFramesNoChange );
        }
    }
    else
    {
        if ( p->pPars->fVerbose )
            printf( "\n" );
        ABC_FREE( pAig->pCexSeq );
        pAig->pCexSeq = pCex;
        if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) )
            Abc_Print( 1, "    Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
        Abc_Print( 1, "Counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = pCex->iFrame - 1;
        Vec_IntFreeP( &pAig->vGateClasses );
        RetValue = 0;
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( p->pPars->fVerbose )
    {
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
        ABC_PRTP( "Runtime: Initializing", p->timeInit,   Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
        Gla_ManReportMemory( p );
    }
//    Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 );
    Gla_ManStop( p );
    fflush( stdout );
    return RetValue;
}

Here is the call graph for this function:

Gia_ManPrintFlopClasses()

void Gia_ManPrintFlopClasses ( Gia_Man_t * p )

extern

Function*************************************************************

Synopsis [Prints stats for the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file absDup.c.

{
    int Counter0, Counter1;
    if ( p->vFlopClasses == NULL )
        return;
    if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) )
    {
        printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" );
        return;
    }
    Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
    Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
    printf( "Flop-level abstraction:  Excluded FFs = %d  Included FFs = %d  (%.2f %%) ", 
        Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) );
    if ( Counter0 + Counter1 < Gia_ManRegNum(p) )
        printf( "and there are other FF classes..." );
    printf( "\n" );
}

Here is the caller graph for this function:

Gia_ManPrintGateClasses()

void Gia_ManPrintGateClasses ( Gia_Man_t * p )

extern

Function*************************************************************

Synopsis [Prints stats for the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file absDup.c.

{
    Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
    int nTotal;
    if ( p->vGateClasses == NULL )
        return;
    if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
    {
        printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
        return;
    }
    // create additional arrays
    Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
    nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
    printf( "Gate-level abstraction:  PI = %d  PPI = %d  FF = %d (%.2f %%)  AND = %d (%.2f %%)  Obj = %d (%.2f %%)\n", 
        Vec_IntSize(vPis), Vec_IntSize(vPPis), 
        Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), 
        Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1), 
        nTotal,              100.0*nTotal             /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
    Vec_IntFree( vPis );
    Vec_IntFree( vPPis );
    Vec_IntFree( vFlops );
    Vec_IntFree( vNodes );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManPrintObjClasses()

void Gia_ManPrintObjClasses ( Gia_Man_t * p )

extern

Function*************************************************************

Synopsis [Prints stats for the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file absDup.c.

{
    Vec_Int_t * vSeens;  // objects seen so far
    Vec_Int_t * vAbs = p->vObjClasses;
    int i, k, Entry, iStart, iStop = -1, nFrames;
    int nObjBits, nObjMask, iObj, iFrame, nWords;
    unsigned * pInfo;
    int * pCountAll, * pCountUni;
    if ( vAbs == NULL )
        return;
    nFrames = Vec_IntEntry( vAbs, 0 );
    assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
    pCountAll = ABC_ALLOC( int, nFrames + 1 );
    pCountUni = ABC_ALLOC( int, nFrames + 1 );
    // start storage for seen objects
    nWords = Abc_BitWordNum( nFrames );
    vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords );
    // get the bitmasks
    nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
    nObjMask = (1 << nObjBits) - 1;
    assert( Gia_ManObjNum(p) <= nObjMask );
    // print info about frames
    printf( "Frame   Core   F0   F1   F2   F3 ...\n" );
    for ( i = 0; i < nFrames; i++ )
    {
        iStart = Vec_IntEntry( vAbs, i+1 );
        iStop  = Vec_IntEntry( vAbs, i+2 );
        memset( pCountAll, 0, sizeof(int) * (nFrames + 1) );
        memset( pCountUni, 0, sizeof(int) * (nFrames + 1) );
        Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
        {
            iObj   = (Entry &  nObjMask);
            iFrame = (Entry >> nObjBits);
            pInfo  = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj );
            if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
            {
                Abc_InfoSetBit( pInfo, iFrame );
                pCountUni[iFrame+1]++;
                pCountUni[0]++;
            }
            pCountAll[iFrame+1]++;
            pCountAll[0]++;
        }
        assert( pCountAll[0] == (iStop - iStart) );
//        printf( "%5d%5d  ", pCountAll[0], pCountUni[0] ); 
        printf( "%3d :", i );
        printf( "%7d", pCountAll[0] ); 
        if ( i >= 10 )
        {
            for ( k = 0; k < 4; k++ )
                printf( "%5d", pCountAll[k+1] ); 
            printf( "  ..." );
            for ( k = i-4; k <= i; k++ )
                printf( "%5d", pCountAll[k+1] ); 
        }
        else
        {
            for ( k = 0; k <= i; k++ )
                if ( k <= i )
                    printf( "%5d", pCountAll[k+1] ); 
        }
//        for ( k = 0; k < nFrames; k++ )
//            if ( k <= i )
//                printf( "%5d", pCountAll[k+1] ); 
        printf( "\n" );
    }
    assert( iStop == Vec_IntSize(vAbs) );
    Vec_IntFree( vSeens );
    ABC_FREE( pCountAll );
    ABC_FREE( pCountUni );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManShrinkGla()

Gia_Man_t * Gia_ManShrinkGla ( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose )

extern

Definition at line 67 of file absIter.c.

{
    Gia_Obj_t * pObj;
    int i, iFrame0, iFrame;
    int nTotal = 0, nRemoved = 0;
    Vec_Int_t * vGScopy;
    abctime clk, clkTotal = Abc_Clock();
    assert( Gia_ManPoNum(p) == 1 );
    assert( p->vGateClasses != NULL );
    vGScopy = Vec_IntDup( p->vGateClasses );
    if ( nFrameMax == 0 )
        iFrame0 = Gia_IterTryImprove( p, 0, 0 );
    else
        iFrame0 = nFrameMax - 1;
    while ( 1 )
    {
        int fChanges = 0;
        Gia_ManForEachObj1( p, pObj, i )
        {
            if ( pObj->fMark0 )
                continue;
            if ( !Gia_ObjIsInGla(p, pObj) )
                continue;
            if ( pObj == Gia_ObjFanin0( Gia_ManPo(p, 0) ) )
                continue;
            if ( Gia_ObjIsAnd(pObj) )
            {
                if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsInGla(p, Gia_ObjFanin1(pObj)) )
                    continue;
            }
            if ( Gia_ObjIsRo(p, pObj) )
            {
                if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj))) )
                    continue;
            }        
            clk = Abc_Clock();
            printf( "%5d : ", nTotal );
            printf( "Obj =%7d   ", i );
            Gia_ObjRemFromGla( p, pObj );
            iFrame = Gia_IterTryImprove( p, nTimeOut, iFrame0 );
            if ( nFrameMax )
                assert( iFrame <= nFrameMax );
            else
                assert( iFrame <= iFrame0 );
            printf( "Frame =%6d   ", iFrame );
            if ( iFrame < iFrame0 )
            {
                pObj->fMark0 = 1;
                Gia_ObjAddToGla( p, pObj );
                printf( "           " );
            }
            else
            {
                fChanges = 1;
                nRemoved++;
                printf( "Removing   " );
                Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 );
            }
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            nTotal++;
            // update the classes
            Vec_IntFreeP( &p->vGateClasses );
            p->vGateClasses = Vec_IntDup(vGScopy);
        }
        if ( !fChanges )
            break;
    }
    Gia_ManCleanMark0(p);
    Vec_IntFree( vGScopy );
    printf( "Tried = %d.  ",     nTotal );
    printf( "Removed = %d. (%.2f %%)  ",  nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) );
    Abc_PrintTime( 1, "Time",  Abc_Clock() - clkTotal );
    return NULL;
}

Here is the call graph for this function:

Gia_VtaConvertFromGla()

Vec_Int_t * Gia_VtaConvertFromGla ( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )

extern

Function*************************************************************

Synopsis [Converting GLA vector to VTA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file absUtil.c.

{
    Vec_Int_t * vVta;
    int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
    int i, k, j, Entry, Counter, nGlaSize;
    //. get the GLA size
    nGlaSize = Vec_IntSum(vGla);
    // get the bitmask
    nObjBits = Abc_Base2Log(nObjs);
    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
    assert( nObjs <= nObjMask );
    // go through objects
    vVta = Vec_IntAlloc( 1000 );
    Vec_IntPush( vVta, nFrames );
    Counter = nFrames + 2;
    for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
        Vec_IntPush( vVta, Counter );
    for ( i = 0; i < nFrames; i++ )
        for ( k = 0; k <= i; k++ )
            Vec_IntForEachEntry( vGla, Entry, j )
                if ( Entry ) 
                    Vec_IntPush( vVta, (k << nObjBits) | j );
    Counter = Vec_IntEntry(vVta, nFrames+1);
    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
    return vVta;
}

Gia_VtaConvertToGla()

Vec_Int_t * Gia_VtaConvertToGla ( Gia_Man_t * p, Vec_Int_t * vVta )

extern

Function*************************************************************

Synopsis [Converting VTA vector to GLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file absUtil.c.

{
    Gia_Obj_t * pObj;
    Vec_Int_t * vGla;
    int nObjMask, nObjs = Gia_ManObjNum(p);
    int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
    assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
    // get the bitmask
    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
    assert( nObjs <= nObjMask );
    // go through objects
    vGla = Vec_IntStart( nObjs );
    Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
    {
        pObj = Gia_ManObj( p, (Entry &  nObjMask) );
        assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
        Vec_IntAddToEntry( vGla, (Entry &  nObjMask), 1 );
    }
    Vec_IntWriteEntry( vGla, 0, nFrames );
    return vGla;
}

Here is the caller graph for this function:

Gia_VtaPerform()

int Gia_VtaPerform ( Gia_Man_t * pAig, Abs_Par_t * pPars )

extern

Function*************************************************************

Synopsis [Collect nodes/flops involved in different timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1743 of file absVta.c.

{
    int RetValue = -1;
    if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
    {
        int nFramesMaxOld = pPars->nFramesMax;
        pPars->nFramesMax = pPars->nFramesStart;
        RetValue = Gia_VtaPerformInt( pAig, pPars );
        pPars->nFramesMax = nFramesMaxOld;
    }
    if ( RetValue == 0 )
        return RetValue;
    return Gia_VtaPerformInt( pAig, pPars );
}

Here is the call graph for this function:

Saig_ManCbaFilterFlops()

Vec_Int_t * Saig_ManCbaFilterFlops ( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect )

extern

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Selects the best flops from the given array.]

Description [Selects the best 'nFfsToSelect' flops among the array 'vAbsFfsToAdd' of flops that should be added to the abstraction. To this end, this procedure simulates the original AIG (pAig) using the given CEX (pAbsCex), which was detected for the abstraction.]

SideEffects []

SeeAlso []

Definition at line 66 of file absOldCex.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
    int i, k, f, Entry, iBit, * pPerm;
    assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
    assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
    // map previously abstracted flops into their original numbers
    vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
    Vec_IntForEachEntry( vFlopClasses, Entry, i )
        if ( Entry == 0 )
            Vec_IntPush( vMapEntries, i );
    // simulate one frame at a time
    assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
    vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
    // initialize the flops
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = 0;
    for ( f = 0; f < pAbsCex->iFrame; f++ )
    {
        // override the flop values according to the cex
        iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
        Vec_IntForEachEntry( vMapEntries, Entry, k )
            Saig_ManLo(pAig, Entry)->fMarkB = Abc_InfoHasBit(pAbsCex->pData, iBit + k);
        // simulate
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        // transfer
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
        // compare
        iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
        Vec_IntForEachEntry( vMapEntries, Entry, k )
            if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Abc_InfoHasBit(pAbsCex->pData, iBit + k) )
                Vec_IntAddToEntry( vFlopCosts, k, 1 );
    }
//    Vec_IntForEachEntry( vFlopCosts, Entry, i )
//        printf( "%d ", Entry );
//    printf( "\n" );
    // remap the cost
    vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
    Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
        Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
    // sort the flops
    pPerm = Abc_MergeSortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
    // shrink the array
    vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
    for ( i = 0; i < nFfsToSelect; i++ )
    {
//        printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
        Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
    }
//    printf( "\n" );
    // cleanup
    ABC_FREE( pPerm );
    Vec_IntFree( vMapEntries );
    Vec_IntFree( vFlopCosts );
    Vec_IntFree( vFlopAddCosts );
    Aig_ManCleanMarkB(pAig);
    // return the computed flops
    return vFfsToAddBest;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManCbaFindCexCareBits()

Abc_Cex_t * Saig_ManCbaFindCexCareBits ( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )

extern

Function*************************************************************

Synopsis [SAT-based refinement of the counter-example.]

Description [The first parameter (nInputs) indicates how many first primary inputs to skip without considering as care candidates.]

SideEffects []

SeeAlso []

Definition at line 718 of file absOldCex.c.

{
    Saig_ManCba_t * p;
    Vec_Int_t * vReasons;
    Abc_Cex_t * pCare;
    abctime clk = Abc_Clock();
 
    clk = Abc_Clock();
    p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );
 
//    p->vReg2Frame = Vec_VecStart( pCex->iFrame );
//    p->vReg2Value = Vec_VecStart( pCex->iFrame );
    p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame );
    vReasons = Saig_ManCbaFindReason( p );
    if ( p->vReg2Frame )
        Saig_ManCbaShrink( p );
 
 
//if ( fVerbose )
//Aig_ManPrintStats( p->pFrames );
 
    if ( fVerbose )
    {
        Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons );
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
        Vec_IntFree( vRes );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
 
    pCare = Saig_ManCbaReason2Cex( p, vReasons );
    Vec_IntFree( vReasons );
    Saig_ManCbaStop( p );
 
if ( fVerbose )
{
printf( "Real " );
Abc_CexPrintStats( pCex );
}
if ( fVerbose )
{
printf( "Care " );
Abc_CexPrintStats( pCare );
}
/*
    // verify the reduced counter-example using ternary simulation
    if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
        printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
    else if ( fVerbose )
        printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
*/
    Aig_ManCleanMarkAB( pAig );
    return pCare;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManCexAbstractionFlops()

Vec_Int_t * Saig_ManCexAbstractionFlops ( Aig_Man_t * p, Gia_ParAbs_t * pPars )

extern

Function*************************************************************

Synopsis [Computes the flops to remain after abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file absOldRef.c.

{
    int nUseStart = 0;
    Aig_Man_t * pAbs, * pTemp;
    Vec_Int_t * vFlops;
    int Iter;//, clk = Abc_Clock(), clk2 = Abc_Clock();//, iFlop;
    assert( Aig_ManRegNum(p) > 0 );
    if ( pPars->fVerbose )
        printf( "Performing counter-example-based refinement.\n" );
    Aig_ManSetCioIds( p );
    vFlops = Vec_IntStartNatural( 1 );
/*
    iFlop = Saig_ManFindFirstFlop( p );
    assert( iFlop >= 0 );
    vFlops = Vec_IntAlloc( 1 );
    Vec_IntPush( vFlops, iFlop );
*/
    // create the resulting AIG
    pAbs = Saig_ManDupAbstraction( p, vFlops );
    if ( !pPars->fVerbose )
    {
        printf( "Init : " );
        Aig_ManPrintStats( pAbs );
    }
    printf( "Refining abstraction...\n" );
    for ( Iter = 0; ; Iter++ )
    {
        pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
        if ( pTemp == NULL )
        {
            ABC_FREE( p->pSeqModel );
            p->pSeqModel = pAbs->pSeqModel;
            pAbs->pSeqModel = NULL;
            Aig_ManStop( pAbs );
            break;
        }
        Aig_ManStop( pAbs );
        pAbs = pTemp;
        printf( "ITER %4d : ", Iter );
        if ( !pPars->fVerbose )
            Aig_ManPrintStats( pAbs );
        // output the intermediate result of abstraction
        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
//            printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
        // check if the ratio is reached
        if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
        {
            printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
            Aig_ManStop( pAbs );
            pAbs = NULL;
            Vec_IntFree( vFlops );
            vFlops = NULL;
            break;
        }
    }
    return vFlops;
}

Here is the call graph for this function:

Saig_ManExtendCounterExampleTest2()

Vec_Int_t * Saig_ManExtendCounterExampleTest2 ( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )

extern

Function*************************************************************

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file absOldSim.c.

{
    Vec_Int_t * vRes;
    Vec_Ptr_t * vSimInfo;
    abctime clk;
    if ( Saig_ManPiNum(p) != pCex->nPis )
    {
        printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
            Aig_ManCiNum(p), pCex->nPis );
        return NULL;
    }
    Aig_ManFanoutStart( p );
    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
    Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );
 
clk = Abc_Clock();
    vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
    if ( fVerbose )
    {
        printf( "Total new PIs = %3d. Non-removable PIs = %3d.  ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    Vec_PtrFree( vSimInfo );
    Aig_ManFanoutStop( p );
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Saig_ManExtendCounterExampleTest3()

Vec_Int_t * Saig_ManExtendCounterExampleTest3 ( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )

extern

Function*************************************************************

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 930 of file saigRefSat.c.

{
    Saig_RefMan_t * p;
    Vec_Int_t * vRes, * vReasons;
    clock_t clk;
    if ( Saig_ManPiNum(pAig) != pCex->nPis )
    {
        printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
            Aig_ManCiNum(pAig), pCex->nPis );
        return NULL;
    }
 
clk = clock();
 
    p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
    vReasons = Saig_RefManFindReason( p );
    vRes = Saig_RefManReason2Inputs( p, vReasons );
 
//    if ( fVerbose )
    {
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
    }
 
/*
    Vec_IntFree( vReasons );
    vReasons = Saig_RefManRefineWithSat( p, vRes );
 
    // derive new result
    Vec_IntFree( vRes );
    vRes = Saig_RefManReason2Inputs( p, vReasons );
//    if ( fVerbose )
    {
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
    }
*/
 
    Vec_IntFree( vReasons );
    Saig_RefManStop( p );
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function: