absRefJ.h File Reference

Go to the source code of this file.

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_	Rf2_Man_t
	INCLUDES ///. More...

Functions
Rf2_Man_t *	Rf2_ManStart (Gia_Man_t *pGia)
	MACRO DEFINITIONS ///. More...
void	Rf2_ManStop (Rf2_Man_t *p, int fProfile)
double	Rf2_ManMemoryUsage (Rf2_Man_t *p)
Vec_Int_t *	Rf2_ManRefine (Rf2_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, int fPropFanout, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_ Rf2_Man_t

INCLUDES ///.

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

FileName [absRef2.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Refinement manager to compute all justifying subsets.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 40 of file absRefJ.h.

Function Documentation

double Rf2_ManMemoryUsage

(

Rf2_Man_t *

p

)

Definition at line 249 of file absRefJ.c.

{
    return (double)(sizeof(Rf2_Man_t) + sizeof(Vec_Int_t) * Gia_ManObjNum(p->pGia));
}

Vec_Int_t* Rf2_ManRefine	(	Rf2_Man_t *	p,
		Abc_Cex_t *	pCex,
		Vec_Int_t *	vMap,
		int	fPropFanout,
		int	fVerbose
	)

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

Synopsis [Computes the refinement for a given counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 863 of file absRefJ.c.

{
    Vec_Int_t * vJusts;
//    Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
    Vec_Int_t * vSelected = NULL;
    clock_t clk, clk2 = clock();
    int nGroups;
    p->nCalls++;
    // initialize
    p->pCex = pCex;
    p->vMap = vMap;
    p->fPropFanout = fPropFanout;
    p->fVerbose    = fVerbose;
    // collects used objects
    Rf2_ManCollect( p );
    // collect reconvergence points
//    Rf2_ManGatherFanins( p, 2 );
    // propagate justification IDs
    nGroups = Rf2_ManAssignJustIds( p );
    vJusts = Rf2_ManPropagate( p, 32 );

//    printf( "\n" );
//    Rf2_ManPrintVector( vJusts, nGroups );
    Rf2_ManPrintVectorSpecial( p, vJusts );
    if ( Vec_IntSize(vJusts) == 0 )
    {
        printf( "Empty set of justifying subsets.\n" );
        return NULL;
    }

//    p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const
//    Rf2_ManBounds( p );

    // select the result
//    Abc_PrintTime( 1, "Time", clock() - clk2 );

    // verify (empty) refinement
    clk = clock();
//    Rf2_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
//    Vec_IntUniqify( vSelected );
//    Vec_IntReverseOrder( vSelected );
    p->timeVer += clock() - clk;
    p->timeTotal += clock() - clk2;
//    p->nRefines += Vec_IntSize(vSelected);
    return vSelected;
}

Rf2_Man_t* Rf2_ManStart

(

Gia_Man_t *

pGia

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file absRefJ.c.

{
    Rf2_Man_t * p;
    assert( Gia_ManPoNum(pGia) == 1 );
    p = ABC_CALLOC( Rf2_Man_t, 1 );
    p->pGia = pGia;
    p->vObjs = Vec_IntAlloc( 1000 );
    p->vFanins = Vec_IntAlloc( 1000 );
    p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) );
    p->vGrp2Ppi = Vec_VecStart( 100 );
    Gia_ManCleanMark0(pGia);
    Gia_ManCleanMark1(pGia);
    return p;
}

void Rf2_ManStop	(	Rf2_Man_t *	p,
		int	fProfile
	)

Definition at line 225 of file absRefJ.c.

{
    if ( !p ) return;
    // print runtime statistics
    if ( fProfile && p->nCalls )
    {
        double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc;
        double MemOther = sizeof(Rf2_Man_t) + sizeof(Rf2_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
        clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
        printf( "Abstraction refinement runtime statistics:\n" );
        ABC_PRTP( "Sensetization", p->timeFwd,   p->timeTotal );
        ABC_PRTP( "Justification", p->timeBwd,   p->timeTotal );
        ABC_PRTP( "Verification ", p->timeVer,   p->timeTotal );
        ABC_PRTP( "Other        ", timeOther,    p->timeTotal );
        ABC_PRTP( "TOTAL        ", p->timeTotal, p->timeTotal );
        printf( "Total calls = %d.  Average refine = %.1f. GIA mem = %.3f MB.  Other mem = %.3f MB.\n", 
            p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) );
    }
    Vec_IntFree( p->vObjs );
    Vec_IntFree( p->vFanins );
    Vec_VecFree( p->vGrp2Ppi );
    ABC_FREE( p->pvVecs );
    ABC_FREE( p );
}