dch.h File Reference

Go to the source code of this file.

Data Structures
struct	Dch_Pars_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_	Dch_Pars_t
	INCLUDES ///. More...

Functions
Aig_Man_t *	Dch_DeriveTotalAig (Vec_Ptr_t *vAigs)
	MACRO DEFINITIONS ///. More...
void	Dch_ManSetDefaultParams (Dch_Pars_t *p)
	DECLARATIONS ///. More...
int	Dch_ManReadVerbose (Dch_Pars_t *p)
Aig_Man_t *	Dch_ComputeChoices (Aig_Man_t *pAig, Dch_Pars_t *pPars)
void	Dch_ComputeEquivalences (Aig_Man_t *pAig, Dch_Pars_t *pPars)
Aig_Man_t *	Dar_ManChoiceNew (Aig_Man_t *pAig, Dch_Pars_t *pPars)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t

INCLUDES ///.

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

FileName [dch.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 43 of file dch.h.

Function Documentation

Aig_Man_t* Dar_ManChoiceNew	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Reproduces script "compress2".]

Description [Consumes the input AIG to reduce memory usage.]

SideEffects []

SeeAlso []

Definition at line 849 of file darScript.c.

{
    extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
//    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
    extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
//    int fVerbose = pPars->fVerbose;
    Aig_Man_t * pMan, * pTemp;
    Gia_Man_t * pGia;
    Vec_Ptr_t * vPios;
    void * pManTime;
    char * pName, * pSpec;
    abctime clk;

    // save useful things
    pManTime = pAig->pManTime; pAig->pManTime = NULL;
    pName = Abc_UtilStrsav( pAig->pName );
    pSpec = Abc_UtilStrsav( pAig->pSpec );

    // perform synthesis
clk = Abc_Clock();
    pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
pPars->timeSynth = Abc_Clock() - clk;

    // perform choice computation
    if ( pPars->fUseGia )
        pMan = Cec_ComputeChoices( pGia, pPars );
    else
    {
        pMan = Gia_ManToAigSkip( pGia, 3 );
        Gia_ManStop( pGia );
        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
        Aig_ManStop( pTemp );
    }

    // create guidence
    vPios = Aig_ManOrderPios( pMan, pAig ); 
    Aig_ManStop( pAig );

    // reconstruct the network
    pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
    Aig_ManStop( pTemp );
    Vec_PtrFree( vPios );

    // reset levels
    pMan->pManTime = pManTime;
    Aig_ManChoiceLevel( pMan );

    // copy names
    ABC_FREE( pMan->pName );
    ABC_FREE( pMan->pSpec );
    pMan->pName = pName;
    pMan->pSpec = pSpec;
    return pMan;
}

Aig_Man_t* Dch_ComputeChoices	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description [Takes several AIGs and performs choicing.]

SideEffects []

SeeAlso []

Definition at line 89 of file dchCore.c.

{
    Dch_Man_t * p;
    Aig_Man_t * pResult;
    abctime clk, clkTotal = Abc_Clock();
    // reset random numbers
    Aig_ManRandom(1);
    // start the choicing manager
    p = Dch_ManCreate( pAig, pPars );
    // compute candidate equivalence classes
clk = Abc_Clock(); 
    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
p->timeSimInit = Abc_Clock() - clk;
//    Dch_ClassesPrint( p->ppClasses, 0 );
    p->nLits = Dch_ClassesLitNum( p->ppClasses );
    // perform SAT sweeping
    Dch_ManSweep( p );
    // free memory ahead of time
p->timeTotal = Abc_Clock() - clkTotal;
    Dch_ManStop( p );
    // create choices
    ABC_FREE( pAig->pTable );
    pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
    // count the number of representatives
    if ( pPars->fVerbose ) 
        Abc_Print( 1, "STATS:  Ands:%8d  ->%8d.  Reprs:%7d  ->%7d.  Choices =%7d.\n", 
               Aig_ManNodeNum(pAig), 
               Aig_ManNodeNum(pResult), 
               Dch_DeriveChoiceCountReprs( pAig ),
               Dch_DeriveChoiceCountEquivs( pResult ),
               Aig_ManChoiceNum( pResult ) );
    return pResult;
}

void Dch_ComputeEquivalences	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description [Takes several AIGs and performs choicing.]

SideEffects []

SeeAlso []

Definition at line 134 of file dchCore.c.

{
    Dch_Man_t * p;
    abctime clk, clkTotal = Abc_Clock();
    // reset random numbers
    Aig_ManRandom(1);
    // start the choicing manager
    p = Dch_ManCreate( pAig, pPars );
    // compute candidate equivalence classes
clk = Abc_Clock(); 
    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
p->timeSimInit = Abc_Clock() - clk;
//    Dch_ClassesPrint( p->ppClasses, 0 );
    p->nLits = Dch_ClassesLitNum( p->ppClasses );
    // perform SAT sweeping
    Dch_ManSweep( p );
    // free memory ahead of time
p->timeTotal = Abc_Clock() - clkTotal;
    Dch_ManStop( p );
}

Aig_Man_t* Dch_DeriveTotalAig

(

Vec_Ptr_t *

vAigs

)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Derives the cumulative AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file dchAig.c.

{
    Aig_Man_t * pAig, * pAig2, * pAigTotal;
    Aig_Obj_t * pObj, * pObjPi, * pObjPo;
    int i, k, nNodes;
    assert( Vec_PtrSize(vAigs) > 0 );
    // make sure they have the same number of PIs/POs
    nNodes = 0;
    pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
    {
        assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pAig2) );
        assert( Aig_ManCoNum(pAig) == Aig_ManCoNum(pAig2) );
        nNodes += Aig_ManNodeNum(pAig2);
        Aig_ManCleanData( pAig2 );
    }
    // map constant nodes
    pAigTotal = Aig_ManStart( nNodes );
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
        Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
    // map primary inputs
    Aig_ManForEachCi( pAig, pObj, i )
    {
        pObjPi = Aig_ObjCreateCi( pAigTotal );
        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
            Aig_ManCi( pAig2, i )->pData = pObjPi;
    }
    // construct the AIG in the order of POs
    Aig_ManForEachCo( pAig, pObj, i )
    {
        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
        {
            pObjPo = Aig_ManCo( pAig2, i );
            Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
        }
        Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) );
    }
/*
    // mark the cone of the first AIG
    Aig_ManIncrementTravId( pAigTotal );
    Aig_ManForEachObj( pAig, pObj, i )
        if ( pObj->pData ) 
            Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData );
*/
    // cleanup should not be done
    return pAigTotal;
}

int Dch_ManReadVerbose

(

Dch_Pars_t *

p

)

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

Synopsis [Returns verbose parameter.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file dchCore.c.

{
    return p->fVerbose;
}

void Dch_ManSetDefaultParams

(

Dch_Pars_t *

p

)

DECLARATIONS ///.

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

FileName [dchCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [The core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

dchCore.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 45 of file dchCore.c.

{
    memset( p, 0, sizeof(Dch_Pars_t) );
    p->nWords         =     8;  // the number of simulation words
    p->nBTLimit       =  1000;  // conflict limit at a node
    p->nSatVarMax     =  5000;  // the max number of SAT variables
    p->fSynthesis     =     1;  // derives three snapshots
    p->fPolarFlip     =     1;  // uses polarity adjustment
    p->fSimulateTfo   =     1;  // simulate TFO
    p->fPower         =     0;  // power-aware rewriting
    p->fLightSynth    =     0;  // uses lighter version of synthesis
    p->fSkipRedSupp   =     0;  // skips choices with redundant structural support
    p->fVerbose       =     0;  // verbose stats
    p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
}