mfsCore.c 18.7 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8
/**CFile****************************************************************

  FileName    [mfsCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The good old minimization with complete don't-cares.]

Alan Mishchenko committed
9
  Synopsis    [Core procedures of this package.]
Alan Mishchenko committed
10 11

  Author      [Alan Mishchenko]
Alan Mishchenko committed
12

Alan Mishchenko committed
13 14 15 16 17 18 19 20 21 22
  Affiliation [UC Berkeley]

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

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

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

#include "mfsInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
30 31
extern int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate );

Alan Mishchenko committed
32 33 34 35 36 37 38 39 40
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

  Synopsis    []

  Description []
Alan Mishchenko committed
41

Alan Mishchenko committed
42 43 44 45 46
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
47 48
void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
{
Alan Mishchenko committed
49
    memset( pPars, 0, sizeof(Mfs_Par_t) );
Alan Mishchenko committed
50
    pPars->nWinTfoLevs  =    2;
Alan Mishchenko committed
51
    pPars->nFanoutsMax  =   30;
Alan Mishchenko committed
52
    pPars->nDepthMax    =   20;
53
    pPars->nWinMax      =  300;
Alan Mishchenko committed
54 55
    pPars->nGrowthLevel =    0;
    pPars->nBTLimit     = 5000;
Alan Mishchenko committed
56
    pPars->fRrOnly      =    0;
Alan Mishchenko committed
57 58 59 60
    pPars->fResub       =    1;
    pPars->fArea        =    0;
    pPars->fMoreEffort  =    0;
    pPars->fSwapEdge    =    0;
Alan Mishchenko committed
61
    pPars->fOneHotness  =    0;
Alan Mishchenko committed
62 63 64
    pPars->fVerbose     =    0;
    pPars->fVeryVerbose =    0;
}
Alan Mishchenko committed
65 66 67 68 69 70 71 72
/*
int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
    Abc_Obj_t * pFanin;
    int i;
    // try replacing area critical fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
    {
Alan Mishchenko committed
73
        if ( Abc_MfsObjProb(p, pFanin) >= 0.4 )
Alan Mishchenko committed
74 75 76
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                return 1;
Alan Mishchenko committed
77
        } else if ( Abc_MfsObjProb(p, pFanin) >= 0.3 )
Alan Mishchenko committed
78 79 80 81 82 83 84 85 86 87 88
        {
            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                return 1;
        }
    }
    return 0;
}
*/

int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
{
89
//    abctime clk;
Alan Mishchenko committed
90 91 92 93 94 95 96 97 98 99
//    Abc_Obj_t * pFanin;
//    int i;

    p->nNodesTried++;
    // prepare data structure for this node
    Mfs_ManClean( p );
    // compute window roots, window support, and window nodes
    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
100
    if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
Alan Mishchenko committed
101 102 103
        return 1;
    // compute the divisors of the window
    p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
Alan Mishchenko committed
104
    p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
Alan Mishchenko committed
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
    // construct AIG for the window
    p->pAigWin = Abc_NtkConstructAig( p, pNode );
    // translate it into CNF
    p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
    // create the SAT problem
    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
    if ( p->pSat == NULL )
    {
        p->nNodesBad++;
        return 1;
    }
    return 0;
}

/*
int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
122
    abctime clk;
Alan Mishchenko committed
123 124 125 126 127 128 129 130 131 132
    Abc_Obj_t * pFanin;
    int i;

    if (Abc_WinNode(p, pNode)  // something wrong
        return 1;

    // solve the SAT problem
    // Abc_NtkMfsEdgePower( p, pNode );
    // try replacing area critical fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
133
        if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
Alan Mishchenko committed
134 135 136
            return 1;

    Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
137
        if ( Abc_MfsObjProb(p, pFanin) >= 0.1 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
Alan Mishchenko committed
138 139 140 141 142 143 144
            return 1;

    if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
        return 0;

    // try replacing area critical fanins while adding two new fanins
    Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
145
            if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
Alan Mishchenko committed
146 147 148 149 150 151 152 153
                return 1;
        }
    return 0;

    return 1;
}
*/

154
void Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
Alan Mishchenko committed
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
{
    int i, k;
    Abc_Obj_t *pFanin, *pNode;
    Abc_Ntk_t *pNtk = p->pNtk;
    int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);

    Abc_NtkForEachNode( pNtk, pNode, k )
    {
        if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
            continue;
        if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
            continue;
        if (Abc_WinNode(p, pNode) )  // something wrong
            continue;

        // solve the SAT problem
        // Abc_NtkMfsEdgePower( p, pNode );
        // try replacing area critical fanins
        Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
174
            if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
Alan Mishchenko committed
175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
                continue;
    }

    Abc_NtkForEachNode( pNtk, pNode, k )
    {
        if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
            continue;
        if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
            continue;
        if (Abc_WinNode(p, pNode) )  // something wrong
            continue;

        // solve the SAT problem
        // Abc_NtkMfsEdgePower( p, pNode );
        // try replacing area critical fanins
        Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
191
            if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
Alan Mishchenko committed
192 193 194 195 196 197 198 199 200 201 202 203 204
                continue;
    }

    Abc_NtkForEachNode( pNtk, pNode, k )
    {
        if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
            continue;
        if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
            continue;
        if (Abc_WinNode(p, pNode) ) // something wrong
            continue;

        Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
205
            if ( Abc_MfsObjProb(p, pFanin) >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
Alan Mishchenko committed
206 207 208 209 210 211 212 213 214 215 216 217 218
                continue;
    }
/*
    Abc_NtkForEachNode( pNtk, pNode, k )
    {
        if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
            continue;
        if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax - 2)
            continue;
        if (Abc_WinNode(p, pNode) ) // something wrong
            continue;

        Abc_ObjForEachFanin( pNode, pFanin, i )
Alan Mishchenko committed
219
            if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
Alan Mishchenko committed
220 221 222 223
                continue;
    }
*/
}
Alan Mishchenko committed
224 225 226 227 228 229

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

  Synopsis    []

  Description []
Alan Mishchenko committed
230

Alan Mishchenko committed
231 232 233 234 235
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
236 237
int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
238
    abctime clk;
Alan Mishchenko committed
239 240
    p->nNodesTried++;
    // prepare data structure for this node
Alan Mishchenko committed
241
    Mfs_ManClean( p );
Alan Mishchenko committed
242
    // compute window roots, window support, and window nodes
243
clk = Abc_Clock();
Alan Mishchenko committed
244 245 246
    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
247
p->timeWin += Abc_Clock() - clk;
248 249 250
    if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
    {
        p->nMaxDivs++;
Alan Mishchenko committed
251
        return 1;
252
    }
Alan Mishchenko committed
253
    // compute the divisors of the window
254
clk = Abc_Clock();
Alan Mishchenko committed
255
    p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
Alan Mishchenko committed
256
    p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
257
p->timeDiv += Abc_Clock() - clk;
Alan Mishchenko committed
258
    // construct AIG for the window
259
clk = Abc_Clock();
Alan Mishchenko committed
260
    p->pAigWin = Abc_NtkConstructAig( p, pNode );
261
p->timeAig += Abc_Clock() - clk;
Alan Mishchenko committed
262
    // translate it into CNF
263
clk = Abc_Clock();
Alan Mishchenko committed
264
    p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
265
p->timeCnf += Abc_Clock() - clk;
Alan Mishchenko committed
266
    // create the SAT problem
267
clk = Abc_Clock();
Alan Mishchenko committed
268
    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
Alan Mishchenko committed
269 270 271 272 273
    if ( p->pSat == NULL )
    {
        p->nNodesBad++;
        return 1;
    }
274
//clk = Abc_Clock();
275 276
//    if ( p->pPars->fGiaSat )
//        Abc_NtkMfsConstructGia( p );
277
//p->timeGia += Abc_Clock() - clk;
Alan Mishchenko committed
278
    // solve the SAT problem
Alan Mishchenko committed
279 280 281
    if ( p->pPars->fPower )
        Abc_NtkMfsEdgePower( p, pNode );
    else if ( p->pPars->fSwapEdge )
Alan Mishchenko committed
282
        Abc_NtkMfsEdgeSwapEval( p, pNode );
Alan Mishchenko committed
283
    else
Alan Mishchenko committed
284 285 286 287 288
    {
        Abc_NtkMfsResubNode( p, pNode );
        if ( p->pPars->fMoreEffort )
            Abc_NtkMfsResubNode2( p, pNode );
    }
289
p->timeSat += Abc_Clock() - clk;
290 291
//    if ( p->pPars->fGiaSat )
//        Abc_NtkMfsDeconstructGia( p );
Alan Mishchenko committed
292 293 294 295 296 297 298 299
    return 1;
}

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

  Synopsis    []

  Description []
Alan Mishchenko committed
300

Alan Mishchenko committed
301 302 303 304 305
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
306 307
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Alan Mishchenko committed
308
    Hop_Obj_t * pObj;
Alan Mishchenko committed
309
    int RetValue;
Alan Mishchenko committed
310 311
    float dProb;
    extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb );
Alan Mishchenko committed
312

313
    int nGain;
314
    abctime clk;
Alan Mishchenko committed
315
    p->nNodesTried++;
Alan Mishchenko committed
316 317 318
    // prepare data structure for this node
    Mfs_ManClean( p );
    // compute window roots, window support, and window nodes
319
clk = Abc_Clock();
Alan Mishchenko committed
320 321 322
    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
323
p->timeWin += Abc_Clock() - clk;
Alan Mishchenko committed
324 325
    // count the number of patterns
//    p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode );
Alan Mishchenko committed
326
    // construct AIG for the window
327
clk = Abc_Clock();
Alan Mishchenko committed
328
    p->pAigWin = Abc_NtkConstructAig( p, pNode );
329
p->timeAig += Abc_Clock() - clk;
Alan Mishchenko committed
330
    // translate it into CNF
331
clk = Abc_Clock();
Alan Mishchenko committed
332
    p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) );
333
p->timeCnf += Abc_Clock() - clk;
Alan Mishchenko committed
334
    // create the SAT problem
335
clk = Abc_Clock();
336
    p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
Alan Mishchenko committed
337 338
    if ( p->pSat && p->pPars->fOneHotness )
        Abc_NtkAddOneHotness( p );
Alan Mishchenko committed
339 340
    if ( p->pSat == NULL )
        return 0;
Alan Mishchenko committed
341
    // solve the SAT problem
Alan Mishchenko committed
342 343
    RetValue = Abc_NtkMfsSolveSat( p, pNode );
    p->nTotConfLevel += p->pSat->stats.conflicts;
344
p->timeSat += Abc_Clock() - clk;
Alan Mishchenko committed
345 346 347 348 349 350
    if ( RetValue == 0 )
    {
        p->nTimeOutsLevel++;
        p->nTimeOuts++;
        return 0;
    }
Alan Mishchenko committed
351 352
    // minimize the local function of the node using bi-decomposition
    assert( p->nFanins == Abc_ObjFaninNum(pNode) );
Alan Mishchenko committed
353
    dProb = p->pPars->fPower? ((float *)p->vProbs->pArray)[pNode->Id] : -1.0;
354 355
    pObj = Abc_NodeIfNodeResyn( p->pManDec, (Hop_Man_t *)pNode->pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, p->nFanins, p->vTruth, p->uCare, dProb );
    nGain = Hop_DagSize((Hop_Obj_t *)pNode->pData) - Hop_DagSize(pObj);
Alan Mishchenko committed
356 357 358 359
    if ( nGain >= 0 )
    {
        p->nNodesDec++;
        p->nNodesGained += nGain;
Alan Mishchenko committed
360
        p->nNodesGainedLevel += nGain;
Alan Mishchenko committed
361
        pNode->pData = pObj;
Alan Mishchenko committed
362
    }
Alan Mishchenko committed
363 364 365 366 367 368 369 370
    return 1;
}

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

  Synopsis    []

  Description []
Alan Mishchenko committed
371

Alan Mishchenko committed
372 373 374 375 376 377 378
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
Alan Mishchenko committed
379
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Alan Mishchenko committed
380

Alan Mishchenko committed
381
    Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
Alan Mishchenko committed
382
    ProgressBar * pProgress;
Alan Mishchenko committed
383 384
    Mfs_Man_t * p;
    Abc_Obj_t * pObj;
Alan Mishchenko committed
385 386
    Vec_Vec_t * vLevels;
    Vec_Ptr_t * vNodes;
387
    int i, k, nNodes, nFaninMax;
388
    abctime clk = Abc_Clock(), clk2;
Alan Mishchenko committed
389 390
    int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
    int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
Alan Mishchenko committed
391 392

    assert( Abc_NtkIsLogic(pNtk) );
Alan Mishchenko committed
393
    nFaninMax = Abc_NtkGetFaninMax(pNtk);
Alan Mishchenko committed
394
    if ( pPars->fResub )
Alan Mishchenko committed
395
    {
Alan Mishchenko committed
396 397
        if ( nFaninMax > 8 )
        {
Alan Mishchenko committed
398
            printf( "Nodes with more than %d fanins will not be processed.\n", 8 );
Alan Mishchenko committed
399 400 401 402 403 404 405
            nFaninMax = 8;
        }
    }
    else
    {
        if ( nFaninMax > MFS_FANIN_MAX )
        {
Alan Mishchenko committed
406
            printf( "Nodes with more than %d fanins will not be processed.\n", MFS_FANIN_MAX );
Alan Mishchenko committed
407 408
            nFaninMax = MFS_FANIN_MAX;
        }
Alan Mishchenko committed
409 410
    }
    // perform the network sweep
Alan Mishchenko committed
411
//    Abc_NtkSweep( pNtk, 0 );
Alan Mishchenko committed
412 413 414
    // convert into the AIG
    if ( !Abc_NtkToAig(pNtk) )
    {
Alan Mishchenko committed
415
        fprintf( stdout, "Converting to AIGs has failed.\n" );
Alan Mishchenko committed
416 417 418 419 420
        return 0;
    }
    assert( Abc_NtkHasAig(pNtk) );

    // start the manager
Alan Mishchenko committed
421
    p = Mfs_ManAlloc( pPars );
Alan Mishchenko committed
422 423
    p->pNtk = pNtk;
    p->nFaninMax = nFaninMax;
Alan Mishchenko committed
424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439

    // precomputer power-aware metrics
    if ( pPars->fPower )
    {
        extern Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne );
        if ( pPars->fResub )
            p->vProbs = Abc_NtkPowerEstimate( pNtk, 0 );
        else
            p->vProbs = Abc_NtkPowerEstimate( pNtk, 1 );
#if 0
        printf( "Total switching before = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
#else
        p->TotalSwitchingBeg = Abc_NtkMfsTotalSwitching(pNtk);
#endif
    }

Alan Mishchenko committed
440 441 442
    if ( pNtk->pExcare )
    {
        Abc_Ntk_t * pTemp;
443
        if ( Abc_NtkPiNum((Abc_Ntk_t *)pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
Alan Mishchenko committed
444
            printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n",
445
                Abc_NtkPiNum((Abc_Ntk_t *)pNtk->pExcare), Abc_NtkCiNum(pNtk) );
Alan Mishchenko committed
446 447
        else
        {
448
            pTemp = Abc_NtkStrash( (Abc_Ntk_t *)pNtk->pExcare, 0, 0, 0 );
Alan Mishchenko committed
449
            p->pCare = Abc_NtkToDar( pTemp, 0, 0 );
Alan Mishchenko committed
450 451 452
            Abc_NtkDelete( pTemp );
            p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
        }
Alan Mishchenko committed
453
    }
Alan Mishchenko committed
454
    if ( p->pCare != NULL )
455
        printf( "Performing optimization with %d external care clauses.\n", Aig_ManCoNum(p->pCare) );
Alan Mishchenko committed
456
    // prepare the BDC manager
Alan Mishchenko committed
457
    if ( !pPars->fResub )
Alan Mishchenko committed
458
    {
Alan Mishchenko committed
459
        pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
Alan Mishchenko committed
460 461 462 463
        pDecPars->fVerbose = pPars->fVerbose;
        p->vTruth = Vec_IntAlloc( 0 );
        p->pManDec = Bdc_ManAlloc( pDecPars );
    }
Alan Mishchenko committed
464 465 466 467 468

    // label the register outputs
    if ( p->pCare )
    {
        Abc_NtkForEachCi( pNtk, pObj, i )
Alan Mishchenko committed
469
            pObj->pData = (void *)(ABC_PTRUINT_T)i;
Alan Mishchenko committed
470
    }
Alan Mishchenko committed
471

Alan Mishchenko committed
472 473 474
    // compute levels
    Abc_NtkLevel( pNtk );
    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
Alan Mishchenko committed
475 476

    // compute don't-cares for each node
Alan Mishchenko committed
477
    nNodes = 0;
Alan Mishchenko committed
478 479
    p->nTotalNodesBeg = nTotalNodesBeg;
    p->nTotalEdgesBeg = nTotalEdgesBeg;
Alan Mishchenko committed
480
    if ( pPars->fResub )
Alan Mishchenko committed
481
    {
Alan Mishchenko committed
482 483 484 485 486 487 488 489
#if 0
        printf( "TotalSwitching (%7.2f --> ", Abc_NtkMfsTotalSwitching(pNtk) );
#endif
        if (pPars->fPower)
        {
            Abc_NtkMfsPowerResub( p, pPars);
        } else
        {
Alan Mishchenko committed
490 491
        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
        Abc_NtkForEachNode( pNtk, pObj, i )
Alan Mishchenko committed
492 493 494
        {
            if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
                continue;
Alan Mishchenko committed
495 496 497 498
            if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
                continue;
            if ( !p->pPars->fVeryVerbose )
                Extra_ProgressBarUpdate( pProgress, i, NULL );
Alan Mishchenko committed
499 500
            if ( pPars->fResub )
                Abc_NtkMfsResub( p, pObj );
Alan Mishchenko committed
501
            else
Alan Mishchenko committed
502 503
                Abc_NtkMfsNode( p, pObj );
        }
Alan Mishchenko committed
504
        Extra_ProgressBarStop( pProgress );
Alan Mishchenko committed
505 506 507
#if 0
        printf( " %7.2f )\n", Abc_NtkMfsTotalSwitching(pNtk) );
#endif
Alan Mishchenko committed
508
    }
Alan Mishchenko committed
509
    } else
Alan Mishchenko committed
510
    {
Alan Mishchenko committed
511 512 513
#if 0
        printf( "Total switching before  = %7.2f,  ----> ", Abc_NtkMfsTotalSwitching(pNtk) );
#endif
Alan Mishchenko committed
514 515 516
        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
        vLevels = Abc_NtkLevelize( pNtk );
        Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
Alan Mishchenko committed
517
        {
Alan Mishchenko committed
518 519 520 521 522
            if ( !p->pPars->fVeryVerbose )
                Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
            p->nNodesGainedLevel = 0;
            p->nTotConfLevel = 0;
            p->nTimeOutsLevel = 0;
523
            clk2 = Abc_Clock();
524
            Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
Alan Mishchenko committed
525 526 527 528 529 530 531
            {
                if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
                    break;
                if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
                    continue;
                if ( pPars->fResub )
                    Abc_NtkMfsResub( p, pObj );
Alan Mishchenko committed
532
                else
Alan Mishchenko committed
533 534 535 536 537
                    Abc_NtkMfsNode( p, pObj );
            }
            nNodes += Vec_PtrSize(vNodes);
            if ( pPars->fVerbose )
            {
Alan Mishchenko committed
538 539
                /*
            printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %%  ",
Alan Mishchenko committed
540 541 542 543
                k, Vec_PtrSize(vNodes),
                1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
                1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
                100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
544
            ABC_PRT( "Time", Abc_Clock() - clk2 );
Alan Mishchenko committed
545
            */
Alan Mishchenko committed
546
            }
Alan Mishchenko committed
547
        }
Alan Mishchenko committed
548 549
        Extra_ProgressBarStop( pProgress );
        Vec_VecFree( vLevels );
Alan Mishchenko committed
550 551 552
#if 0
        printf( " %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
#endif
Alan Mishchenko committed
553 554
    }
    Abc_NtkStopReverseLevels( pNtk );
Alan Mishchenko committed
555 556 557 558 559

    // perform the sweeping
    if ( !pPars->fResub )
    {
        extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
Alan Mishchenko committed
560 561
//        Abc_NtkSweep( pNtk, 0 );
//        Abc_NtkBidecResyn( pNtk, 0 );
Alan Mishchenko committed
562 563
    }

Alan Mishchenko committed
564 565
    p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
    p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
Alan Mishchenko committed
566 567 568 569 570 571 572 573

    // undo labesl
    if ( p->pCare )
    {
        Abc_NtkForEachCi( pNtk, pObj, i )
            pObj->pData = NULL;
    }

Alan Mishchenko committed
574 575 576 577 578 579 580 581 582 583
    if ( pPars->fPower )
    {
#if 1
        p->TotalSwitchingEnd = Abc_NtkMfsTotalSwitching(pNtk);
//        printf( "Total switching after  = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
#else
        printf( "Total switching after  = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
#endif
    }

Alan Mishchenko committed
584
    // free the manager
585
    p->timeTotal = Abc_Clock() - clk;
Alan Mishchenko committed
586 587 588 589 590 591 592 593 594
    Mfs_ManStop( p );
    return 1;
}

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


595 596
ABC_NAMESPACE_IMPL_END