llb4Cluster.c 14.2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
/**CFile****************************************************************

  FileName    [llb2Cluster.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD based reachability.]

  Synopsis    [Non-linear quantification scheduling.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: llb2Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "llbInt.h"

ABC_NAMESPACE_IMPL_START
 

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Find good static variable ordering.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
{
    Aig_Obj_t * pFanin0, * pFanin1;
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent( pAig, pObj );
51
    assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
52
    if ( Aig_ObjIsCi(pObj) )
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
    {
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
        return;
    }
    // try fanins with higher level first
    pFanin0 = Aig_ObjFanin0(pObj);
    pFanin1 = Aig_ObjFanin1(pObj);
//    if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
    if ( pFanin0->Level > pFanin1->Level )
    {
        Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
        Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
    }
    else
    {
        Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
        Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
    }
71 72
    if ( pObj->fMarkA )
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
73 74 75 76 77 78 79 80 81 82 83 84 85
}

/**Function*************************************************************

  Synopsis    [Find good static variable ordering.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
86
Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter )
87 88 89 90 91
{
    Vec_Int_t * vNodes = NULL;
    Vec_Int_t * vOrder;
    Aig_Obj_t * pObj;
    int i, Counter = 0;
92 93 94 95 96
    // mark nodes to exclude:  AND with low level and CO drivers
    Aig_ManCleanMarkA( pAig );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Aig_ObjLevel(pObj) > 3 )
            pObj->fMarkA = 1;
97
    Aig_ManForEachCo( pAig, pObj, i )
98 99
        Aig_ObjFanin0(pObj)->fMarkA = 0;

100 101 102 103
    // collect nodes in the order
    vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
    Aig_ManIncrementTravId( pAig );
    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
104
//    Aig_ManForEachCo( pAig, pObj, i )
105
    Saig_ManForEachLi( pAig, pObj, i )
106 107 108 109
    {
        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
        Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
    }
110
    Aig_ManForEachCi( pAig, pObj, i )
111
        if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
112 113 114
            Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
    Aig_ManCleanMarkA( pAig );
    Vec_IntFreeP( &vNodes );
115 116 117 118
//    assert( Counter == Aig_ManObjNum(pAig) - 1 );

/*
    Saig_ManForEachPi( pAig, pObj, i )
119
        printf( "pi%d ", Llb_ObjBddVar(vOrder, pObj) );
120 121
    printf( "\n" );
    Saig_ManForEachLo( pAig, pObj, i )
122
        printf( "lo%d ", Llb_ObjBddVar(vOrder, pObj) );
123 124
    printf( "\n" );
    Saig_ManForEachPo( pAig, pObj, i )
125
        printf( "po%d ", Llb_ObjBddVar(vOrder, pObj) );
126 127
    printf( "\n" );
    Saig_ManForEachLi( pAig, pObj, i )
128
        printf( "li%d ", Llb_ObjBddVar(vOrder, pObj) );
129 130
    printf( "\n" );
    Aig_ManForEachNode( pAig, pObj, i )
131
        printf( "n%d ", Llb_ObjBddVar(vOrder, pObj) );
132 133 134 135
    printf( "\n" );
*/
    if ( pCounter )
        *pCounter = Counter;
136 137 138 139 140 141 142 143 144 145 146 147 148 149
    return vOrder;
}

/**Function*************************************************************

  Synopsis    [Derives BDDs for the partitions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
150 151 152 153 154
DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots )
{
    DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
    if ( Aig_ObjIsConst1(pObj) )
        return Cudd_ReadOne(dd); 
155
    if ( Aig_ObjIsCi(pObj) )
156 157 158
        return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
    if ( pObj->pData )
        return (DdNode *)pObj->pData;
159
    if ( Aig_ObjIsCo(pObj) )
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
    {
        bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
        bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 );  Cudd_Ref( bPart );
        Vec_PtrPush( vRoots, bPart );
        return NULL;
    }
    bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
    bBdd1 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) );
    bBdd  = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( bBdd );
    if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
    {
        vVar  = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
        bPart = Cudd_bddXnor( dd, vVar, bBdd );  Cudd_Ref( bPart );
        Vec_PtrPush( vRoots, bPart );
        Cudd_RecursiveDeref( dd, bBdd );
        bBdd = vVar;  Cudd_Ref( vVar );
    }
    pObj->pData = bBdd;
    return bBdd;
}

/**Function*************************************************************

  Synopsis    [Derives BDDs for the partitions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fOutputs )
193 194 195 196 197 198
{
    Vec_Ptr_t * vRoots;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanData( pAig );
    vRoots = Vec_PtrAlloc( 100 );
199
    if ( fOutputs )
200
    {
201 202
        Saig_ManForEachPo( pAig, pObj, i )
            Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots );
203
    }
204
    else
205
    {
206 207
        Saig_ManForEachLi( pAig, pObj, i )
            Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots );
208 209 210 211
    }
    Aig_ManForEachNode( pAig, pObj, i )
        if ( pObj->pData )
            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
212
    return vRoots;
213 214 215 216
}

/**Function*************************************************************

217
  Synopsis    [Creates quantifiable variables for both types of traversal.]
218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
    Vec_Int_t * vVars2Q;
    Aig_Obj_t * pObj;
    int i;
    vVars2Q = Vec_IntAlloc( 0 );
    Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
    Saig_ManForEachLo( pAig, pObj, i )
234
        Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
235
//    Aig_ManForEachCo( pAig, pObj, i )
236
    Saig_ManForEachLi( pAig, pObj, i )
237
        Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
238 239 240 241 242
    return vVars2Q;
}

/**Function*************************************************************

243
  Synopsis    [Creates quantifiable variables for both types of traversal.]
244 245 246 247 248 249 250 251 252 253 254 255 256

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop )
{
    DdNode * bSupp;
    Aig_Obj_t * pObj;
    int i, Counter = 0;
257
    bSupp = Cudd_Support( dd, bFunc );  Cudd_Ref( bSupp );
258 259 260
    if ( !fCo && !fFlop )
    {
        Saig_ManForEachPi( pAig, pObj, i )
261 262
            if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
263 264 265 266
    }
    else if ( fCo && !fFlop )
    {
        Saig_ManForEachPo( pAig, pObj, i )
267 268
            if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
269 270 271 272
    }
    else if ( !fCo && fFlop )
    {
        Saig_ManForEachLo( pAig, pObj, i )
273 274
            if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
275 276 277 278
    }
    else if ( fCo && fFlop )
    {
        Saig_ManForEachLi( pAig, pObj, i )
279 280
            if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
281
    }
282
    Cudd_RecursiveDeref( dd, bSupp );
283 284 285 286 287
    return Counter;
}

/**Function*************************************************************

288
  Synopsis    [Creates quantifiable variables for both types of traversal.]
289 290 291 292 293 294 295 296 297 298 299 300 301 302

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
{
    DdNode * bTemp;
    int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
    Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
    {
303
//Extra_bddPrintSupport(dd, bTemp);  printf("\n" );
304 305 306 307 308 309 310
        nSuppAll = Cudd_SupportSize(dd,bTemp);
        nSuppPi  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
        nSuppPo  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
        nSuppLi  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1);
        nSuppLo  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
        nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);

311 312 313
        if ( Cudd_DagSize(bTemp) <= 10 )
            continue;

314 315 316 317 318 319 320 321 322 323 324 325
        printf( "%4d : bdd =%6d  supp =%3d  ", i, Cudd_DagSize(bTemp), nSuppAll );
        printf( "pi =%3d ",  nSuppPi );
        printf( "po =%3d ",  nSuppPo );
        printf( "lo =%3d ",  nSuppLo );
        printf( "li =%3d ",  nSuppLi );
        printf( "and =%3d",  nSuppAnd );
        printf( "\n" );
    }
}

/**Function*************************************************************

326
  Synopsis    [Creates quantifiable variables for both types of traversal.]
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_Nonlin4PrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
{
    Aig_Obj_t * pObj;
    int i, * pSupp;
    int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;

    pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
    Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );

    Aig_ManForEachObj( pAig, pObj, i )
    {
346
        if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
347 348
            continue;
        // remove variables that do not participate
349
        if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 )
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368
        {
            if ( Aig_ObjIsNode(pObj) )
                Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
            continue;
        }
        nSuppAll++;
        if ( Saig_ObjIsPi(pAig, pObj) )
            nSuppPi++;
        else if ( Saig_ObjIsLo(pAig, pObj) )
            nSuppLo++;
        else if ( Saig_ObjIsPo(pAig, pObj) )
            nSuppPo++;
        else if ( Saig_ObjIsLi(pAig, pObj) )
            nSuppLi++;
        else
            nSuppAnd++;
    }
    ABC_FREE( pSupp );

369 370
    printf( "Groups =%3d  ", Vec_PtrSize(vGroups) );
    printf( "Variables: all =%4d ",  nSuppAll );
371 372 373 374 375 376 377 378 379 380
    printf( "pi =%4d ",  nSuppPi );
    printf( "po =%4d ",  nSuppPo );
    printf( "lo =%4d ",  nSuppLo );
    printf( "li =%4d ",  nSuppLi );
    printf( "and =%4d",  nSuppAnd );
    printf( "\n" );
}

/**Function*************************************************************

381 382 383 384 385 386 387 388 389
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
390
void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose )
391 392 393 394 395
{
    DdManager * dd;
    Vec_Int_t * vOrder, * vVars2Q;
    Vec_Ptr_t * vParts, * vGroups;
    DdNode * bTemp;
396
    int i, nVarNum;
397 398

    // create the BDD manager
399 400
    vOrder  = Llb_Nonlin4FindOrder( pAig, &nVarNum );
    dd      = Cudd_Init( nVarNum, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
401
//    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
402

403
    vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
404
    vParts  = Llb_Nonlin4FindPartitions( dd, pAig, vOrder, 0 );
405

406 407 408 409 410 411 412
    vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddMax );
    Vec_IntFree( vVars2Q );

    Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
        Cudd_RecursiveDeref( dd, bTemp );
    Vec_PtrFree( vParts );

413

414 415 416 417 418
//    if ( fVerbose )
    Llb_Nonlin4PrintSuppProfile( dd, pAig, vOrder, vGroups );
    if ( fVerbose )
    printf( "Before reordering\n" );
    if ( fVerbose )
419 420
    Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );

421 422 423
//    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
//    printf( "After reordering\n" );
//    Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
424

425 426 427 428
    if ( pvOrder )
        *pvOrder = vOrder;
    else
        Vec_IntFree( vOrder );
429

430 431 432 433 434 435 436 437 438 439 440 441 442 443
    if ( pvGroups )
        *pvGroups = vGroups;
    else
    {
        Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
            Cudd_RecursiveDeref( dd, bTemp );
        Vec_PtrFree( vGroups );
    }

    if ( pdd )
        *pdd = dd;
    else
        Extra_StopManager( dd );
//    Cudd_Quit( dd );
444 445 446 447 448 449 450 451 452
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END