llb2Driver.c File Reference

#include "llbInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Vec_Int_t *	Llb_DriverCountRefs (Aig_Man_t *p)
	DECLARATIONS ///. More...
Vec_Int_t *	Llb_DriverCollectNs (Aig_Man_t *pAig, Vec_Int_t *vDriRefs)
Vec_Int_t *	Llb_DriverCollectCs (Aig_Man_t *pAig)
DdNode *	Llb_DriverPhaseCube (Aig_Man_t *pAig, Vec_Int_t *vDriRefs, DdManager *dd)
DdManager *	Llb_DriverLastPartition (Aig_Man_t *p, Vec_Int_t *vVarsNs, abctime TimeTarget)

Function Documentation

Vec_Int_t* Llb_DriverCollectCs

(

Aig_Man_t *

pAig

)

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

Synopsis [Returns array of CS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file llb2Driver.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObj;
    int i;
    vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    Saig_ManForEachLo( pAig, pObj, i )
        Vec_IntPush( vVars, Aig_ObjId(pObj) );
    return vVars;
}

Vec_Int_t* Llb_DriverCollectNs	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vDriRefs
	)

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

Synopsis [Returns array of NS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file llb2Driver.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObj, * pDri;
    int i;
    vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        pDri = Aig_ObjFanin0(pObj);
        if ( Vec_IntEntry( vDriRefs, Aig_ObjId(pDri) ) != 1 || Saig_ObjIsPi(pAig, pDri) || Aig_ObjIsConst1(pDri) )
            Vec_IntPush( vVars, Aig_ObjId(pObj) );
        else
            Vec_IntPush( vVars, Aig_ObjId(pDri) );
    }
    return vVars;
}

ABC_NAMESPACE_IMPL_START Vec_Int_t* Llb_DriverCountRefs

(

Aig_Man_t *

p

)

DECLARATIONS ///.

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

FileName [llb2Driver.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Procedures working with flop drivers.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Returns the array of times each flop driver is referenced.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file llb2Driver.c.

{
    Vec_Int_t * vCounts;
    Aig_Obj_t * pObj;
    int i;
    vCounts = Vec_IntStart( Aig_ManObjNumMax(p) );
    Saig_ManForEachLi( p, pObj, i )
        Vec_IntAddToEntry( vCounts, Aig_ObjFaninId0(pObj), 1 );
    return vCounts;
}

DdManager* Llb_DriverLastPartition	(	Aig_Man_t *	p,
		Vec_Int_t *	vVarsNs,
		abctime	TimeTarget
	)

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

Synopsis [Compute the last partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file llb2Driver.c.

{
//    int fVerbose = 1;
    DdManager * dd;
    DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp;
    Aig_Obj_t * pObj;
    int i;
    dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
    dd->TimeStop = TimeTarget;
    bRes = Cudd_ReadOne(dd);                                   Cudd_Ref( bRes );

    // mark the duplicated flop inputs
    Aig_ManForEachObjVec( vVarsNs, p, pObj, i )
    {
        if ( !Saig_ObjIsLi(p, pObj) )
            continue;
        bVar1 = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
        bVar2 = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
            bVar2 = Cudd_ReadOne(dd);
        bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) );
        bProd = Cudd_bddXnor( dd, bVar1, bVar2 );              Cudd_Ref( bProd );
//        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );        Cudd_Ref( bRes );
//        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );  
        if ( bRes == NULL )
        {
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bProd );
            return NULL;
        }        
        Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }

/*
    Saig_ManForEachLi( p, pObj, i )
        printf( "%d ", Aig_ObjId(pObj) );
    printf( "\n" );
    Saig_ManForEachLi( p, pObj, i )
        printf( "%c%d ", Aig_ObjFaninC0(pObj)? '-':'+', Aig_ObjFaninId0(pObj) );
    printf( "\n" );
*/
    Cudd_AutodynDisable( dd );
//    Cudd_RecursiveDeref( dd, bRes );
//    Extra_StopManager( dd );
    dd->bFunc = bRes;
    dd->TimeStop = 0;
    return dd;
}

DdNode* Llb_DriverPhaseCube	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vDriRefs,
		DdManager *	dd
	)

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

Synopsis [Create cube for phase swapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file llb2Driver.c.

{
    DdNode * bCube, * bVar, * bTemp;
    Aig_Obj_t * pObj;
    int i;
    abctime TimeStop;
    TimeStop = dd->TimeStop; dd->TimeStop = 0;
    bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        assert( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) >= 1 );
        if ( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) != 1 )
            continue;
        if ( !Aig_ObjFaninC0(pObj) )
            continue;
        bVar  = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bCube );
    dd->TimeStop = TimeStop;
    return bCube;
}