ssc.h File Reference

Go to the source code of this file.

Data Structures
struct	Ssc_Pars_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Ssc_Pars_t_	Ssc_Pars_t
	INCLUDES ///. More...

Functions
void	Ssc_ManSetDefaultParams (Ssc_Pars_t *p)
	MACRO DEFINITIONS ///. More...
Gia_Man_t *	Ssc_PerformSweeping (Gia_Man_t *pAig, Gia_Man_t *pCare, Ssc_Pars_t *pPars)
Gia_Man_t *	Ssc_PerformSweepingConstr (Gia_Man_t *p, Ssc_Pars_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Ssc_Pars_t_ Ssc_Pars_t

INCLUDES ///.

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

FileName [ssc.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sweeping under constraints.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

ssc.h,v 1.00 2008/07/29 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 43 of file ssc.h.

Function Documentation

void Ssc_ManSetDefaultParams

(

Ssc_Pars_t *

p

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

FileName [sscCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sweeping under constraints.]

Synopsis [The core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sscCore.c.

{
    memset( p, 0, sizeof(Ssc_Pars_t) );
    p->nWords         =     1;  // the number of simulation words
    p->nBTLimit       =  1000;  // conflict limit at a node
    p->nSatVarMax     =  5000;  // the max number of SAT variables
    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
    p->fVerbose       =     0;  // verbose stats
}

Gia_Man_t* Ssc_PerformSweeping	(	Gia_Man_t *	pAig,
		Gia_Man_t *	pCare,
		Ssc_Pars_t *	pPars
	)

Definition at line 413 of file sscCore.c.

{
    Gia_Man_t * pResult = Ssc_PerformSweepingInt( pAig, pCare, pPars );
    if ( pPars->fVerify )
        Ssc_PerformVerification( pAig, pResult, pCare );
    return pResult;
}

Gia_Man_t* Ssc_PerformSweepingConstr	(	Gia_Man_t *	p,
		Ssc_Pars_t *	pPars
	)

Definition at line 420 of file sscCore.c.

{
    Gia_Man_t * pAig, * pCare, * pResult;
    int i;
    if ( pPars->fVerbose )
        Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs );
    if ( p->nConstrs == 0 )
    {
        pAig = Gia_ManDup( p );
        pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
        pCare->pName = Abc_UtilStrsav( "care" );
        for ( i = 0; i < Gia_ManCiNum(p); i++ )
            Gia_ManAppendCi( pCare );
        Gia_ManAppendCo( pCare, 0 );
    }
    else
    {
        Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
        pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 );
        pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
        Vec_IntFree( vOuts );
    }
    if ( pPars->fVerbose )
    {
        printf( "User AIG: " );
        Gia_ManPrintStats( pAig, NULL );
        printf( "Care AIG: " );
        Gia_ManPrintStats( pCare, NULL );
    }

    pAig = Gia_ManDupLevelized( pResult = pAig );
    Gia_ManStop( pResult );
    pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
    if ( pPars->fAppend )
    {
        Gia_ManDupAppendShare( pResult, pCare );
        pResult->nConstrs = Gia_ManPoNum(pCare);
    }
    Gia_ManStop( pAig );
    Gia_ManStop( pCare );
    return pResult;
}