sfmCore.c 10.6 KB
Newer Older
Alan Mishchenko committed
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
/**CFile****************************************************************

  FileName    [sfmCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SAT-based optimization using internal don't-cares.]

  Synopsis    [Core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "sfmInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

Alan Mishchenko committed
36
  Synopsis    [Setup parameter structure.]
Alan Mishchenko committed
37 38

  Description []
Alan Mishchenko committed
39 40 41 42 43 44 45 46 47 48

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sfm_ParSetDefault( Sfm_Par_t * pPars )
{
    memset( pPars, 0, sizeof(Sfm_Par_t) );
    pPars->nTfoLevMax   =    2;  // the maximum fanout levels
Alan Mishchenko committed
49
    pPars->nFanoutMax   =   30;  // the maximum number of fanouts
Alan Mishchenko committed
50
    pPars->nDepthMax    =   20;  // the maximum depth to try  
Alan Mishchenko committed
51
    pPars->nWinSizeMax  =  300;  // the maximum window size
Alan Mishchenko committed
52
    pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
Alan Mishchenko committed
53
    pPars->nBTLimit     = 5000;  // the maximum number of conflicts in one SAT run
Alan Mishchenko committed
54
    pPars->fRrOnly      =    0;  // perform redundancy removal
Alan Mishchenko committed
55 56 57 58 59 60 61 62
    pPars->fArea        =    0;  // performs optimization for area
    pPars->fMoreEffort  =    0;  // performs high-affort minimization
    pPars->fVerbose     =    0;  // enable basic stats
    pPars->fVeryVerbose =    0;  // enable detailed stats
}

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

Alan Mishchenko committed
63
  Synopsis    [Prints statistics.]
Alan Mishchenko committed
64 65

  Description []
Alan Mishchenko committed
66

Alan Mishchenko committed
67 68 69 70 71
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
72
void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
Alan Mishchenko committed
73
{
Alan Mishchenko committed
74
    p->timeOther = p->timeTotal - p->timeWin - p->timeDiv - p->timeCnf - p->timeSat;
Alan Mishchenko committed
75 76
    printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
        Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
Alan Mishchenko committed
77 78

    printf( "Attempts :   " );
Alan Mishchenko committed
79 80
    printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
    printf( "Resub  %6d out of %6d (%6.2f %%)   ", p->nResubs,  p->nTryResubs,  100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs)  );
Alan Mishchenko committed
81 82
    printf( "\n" );

Alan Mishchenko committed
83
    printf( "Reduction:   " );
Alan Mishchenko committed
84 85
    printf( "Nodes  %6d out of %6d (%6.2f %%)   ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesBeg, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
    printf( "Edges  %6d out of %6d (%6.2f %%)   ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesBeg, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
Alan Mishchenko committed
86 87 88 89 90 91
    printf( "\n" );

    ABC_PRTP( "Win", p->timeWin  ,  p->timeTotal );
    ABC_PRTP( "Div", p->timeDiv  ,  p->timeTotal );
    ABC_PRTP( "Cnf", p->timeCnf  ,  p->timeTotal );
    ABC_PRTP( "Sat", p->timeSat  ,  p->timeTotal );
Alan Mishchenko committed
92
    ABC_PRTP( "Oth", p->timeOther,  p->timeTotal );
Alan Mishchenko committed
93
    ABC_PRTP( "ALL", p->timeTotal,  p->timeTotal );
Alan Mishchenko committed
94
//    ABC_PRTP( "   ", p->time1    ,  p->timeTotal );
Alan Mishchenko committed
95 96
}

Alan Mishchenko committed
97 98 99 100 101 102 103 104 105 106 107 108 109
/**Function*************************************************************

  Synopsis    [Performs resubstitution for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
{
Alan Mishchenko committed
110
    int fSkipUpdate  = 0;
Alan Mishchenko committed
111
    int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
Alan Mishchenko committed
112 113
    int i, iFanin, iVar = -1;
    word uTruth, uSign, uMask;
114
    abctime clk;
Alan Mishchenko committed
115 116
    assert( Sfm_ObjIsNode(p, iNode) );
    assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
Alan Mishchenko committed
117
    p->nTryRemoves++;
Alan Mishchenko committed
118 119
    // report init stats
    if ( p->pPars->fVeryVerbose )
Alan Mishchenko committed
120
        printf( "%5d : Lev =%3d. Leaf =%3d.  Node =%3d.  Div=%3d.  Fanin =%4d (%d/%d). MFFC = %d\n", 
Alan Mishchenko committed
121
            iNode, Sfm_ObjLevel(p, iNode), 0, Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), 
Alan Mishchenko committed
122
            Sfm_ObjFanin(p, iNode, f), f, Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, Sfm_ObjFanin(p, iNode, f)) );
Alan Mishchenko committed
123 124 125 126 127 128 129 130
    // clean simulation info
    p->nCexes = 0;
    Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 );
    // try removing the critical fanin
    Vec_IntClear( p->vDivIds );
    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
        if ( i != f )
            Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
131
clk = Abc_Clock();
Alan Mishchenko committed
132
    uTruth = Sfm_ComputeInterpolant( p );
133
p->timeSat += Abc_Clock() - clk;
Alan Mishchenko committed
134 135
    // analyze outcomes
    if ( uTruth == SFM_SAT_UNDEC )
Alan Mishchenko committed
136 137
    {
        p->nTimeOuts++;
Alan Mishchenko committed
138
        return 0;
Alan Mishchenko committed
139 140
    }
    if ( uTruth != SFM_SAT_SAT )
Alan Mishchenko committed
141
        goto finish;
Alan Mishchenko committed
142
    if ( fRemoveOnly || p->pPars->fRrOnly || Vec_IntSize(p->vDivs) == 0 )
Alan Mishchenko committed
143
        return 0;
Alan Mishchenko committed
144

Alan Mishchenko committed
145
    p->nTryResubs++;
Alan Mishchenko committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
    if ( fVeryVerbose )
    {
        for ( i = 0; i < 9; i++ )
            printf( " " );
        for ( i = 0; i < Vec_IntSize(p->vDivs); i++ )
            printf( "%d", i % 10 );
        printf( "\n" );
    }
    while ( 1 ) 
    {
        if ( fVeryVerbose )
        {
            printf( "%3d: %3d ", p->nCexes, iVar );
            Vec_WrdForEachEntry( p->vDivCexes, uSign, i )
                printf( "%d", Abc_InfoHasBit((unsigned *)&uSign, p->nCexes-1) );
            printf( "\n" );
        }
        // find the next divisor to try
        uMask = (~(word)0) >> (64 - p->nCexes);
        Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar )
            if ( uSign == uMask )
                break;
        if ( iVar == Vec_IntSize(p->vDivs) )
            return 0;
        // try replacing the critical fanin
        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) );
172
clk = Abc_Clock();
Alan Mishchenko committed
173
        uTruth = Sfm_ComputeInterpolant( p );
174
p->timeSat += Abc_Clock() - clk;
Alan Mishchenko committed
175 176
        // analyze outcomes
        if ( uTruth == SFM_SAT_UNDEC )
Alan Mishchenko committed
177 178
        {
            p->nTimeOuts++;
Alan Mishchenko committed
179
            return 0;
Alan Mishchenko committed
180 181
        }
        if ( uTruth != SFM_SAT_SAT )
Alan Mishchenko committed
182 183 184 185 186 187 188 189 190 191
            goto finish;
        if ( p->nCexes == 64 )
            return 0;
        // remove the last variable
        Vec_IntPop( p->vDivIds );
    }
finish:
    if ( p->pPars->fVeryVerbose )
    {
        if ( iVar == -1 )
Alan Mishchenko committed
192
            printf( "Node %d: Fanin %d (%d) can be removed.  ", iNode, f, Sfm_ObjFanin(p, iNode, f) );
Alan Mishchenko committed
193
        else
Alan Mishchenko committed
194 195
            printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d (%d).   ", 
            iNode, f, Sfm_ObjFanin(p, iNode, f), iVar, Vec_IntEntry(p->vDivs, iVar) );
Alan Mishchenko committed
196 197 198 199 200 201 202
        Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" );
    }
    if ( iVar == -1 )
        p->nRemoves++;
    else
        p->nResubs++;
    if ( fSkipUpdate )
Alan Mishchenko committed
203
        return 0;
Alan Mishchenko committed
204 205 206 207 208 209 210
    // update the network
    Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
    return 1;
 }
int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
{
    int i, iFanin;
Alan Mishchenko committed
211
    p->nNodesTried++;
Alan Mishchenko committed
212
    // prepare SAT solver
Alan Mishchenko committed
213 214
    if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
        return 0;
Alan Mishchenko committed
215 216
    if ( !Sfm_NtkWindowToSolver( p ) )
        return 0;
Alan Mishchenko committed
217 218 219 220 221 222 223
    // try replacing area critical fanins
    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
        if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 )
        {
            if ( Sfm_NodeResubSolve( p, iNode, i, 0 ) )
                return 1;
        }
224 225
    if ( p->pPars->fArea )
        return 0;
Alan Mishchenko committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
    // try removing redundant edges
    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
        if ( !(Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1) )
        {
            if ( Sfm_NodeResubSolve( p, iNode, i, 1 ) )
                return 1;
        }
/*
    // try replacing area critical fanins while adding two new fanins
    if ( Sfm_ObjFaninNum(p, iNode) < p->nFaninMax )
        Abc_ObjForEachFanin( pNode, pFanin, i )
            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
            {
                if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
                    return 1;
            }
*/
    return 0;
}
Alan Mishchenko committed
245 246 247 248 249 250

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

  Synopsis    []

  Description []
Alan Mishchenko committed
251 252 253 254 255 256
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
257
int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
Alan Mishchenko committed
258
{
Alan Mishchenko committed
259
    int i, k, Counter = 0;
260
    p->timeTotal = Abc_Clock();
Alan Mishchenko committed
261 262 263 264 265 266 267
    if ( pPars->fVerbose )
    {
        int nFixed = p->vFixed ? Vec_StrSum(p->vFixed) : 0;
        int nEmpty = p->vEmpty ? Vec_StrSum(p->vEmpty) : 0;
        printf( "Performing MFS with %d PIs, %d POs, %d nodes (%d flexible, %d fixed, %d empty).\n", 
            p->nPis, p->nPos, p->nNodes, p->nNodes-nFixed, nFixed, nEmpty );
    }
Alan Mishchenko committed
268 269
    p->pPars = pPars;
    Sfm_NtkPrepare( p );
Alan Mishchenko committed
270 271
//    Sfm_ComputeInterpolantCheck( p );
//    return 0;
Alan Mishchenko committed
272
    p->nTotalNodesBeg = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
Alan Mishchenko committed
273
    p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
Alan Mishchenko committed
274 275
    Sfm_NtkForEachNode( p, i )
    {
Alan Mishchenko committed
276 277
        if ( Sfm_ObjIsFixed( p, i ) )
            continue;
Alan Mishchenko committed
278 279 280 281
        if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
            continue;
        if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
            continue;
Alan Mishchenko committed
282
        for ( k = 0; Sfm_NodeResub(p, i); k++ )
Alan Mishchenko committed
283 284 285 286
        {
//            Counter++;
//            break;
        }
Alan Mishchenko committed
287
        Counter += (k > 0);
288 289
        if ( pPars->nNodesMax && Counter >= pPars->nNodesMax )
            break;
Alan Mishchenko committed
290
    }
Alan Mishchenko committed
291
    p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
Alan Mishchenko committed
292
    p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
293
    p->timeTotal = Abc_Clock() - p->timeTotal;
Alan Mishchenko committed
294 295
    if ( pPars->fVerbose )
        Sfm_NtkPrintStats( p );
Alan Mishchenko committed
296
    return Counter;
Alan Mishchenko committed
297 298 299 300 301 302 303 304 305
}

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


ABC_NAMESPACE_IMPL_END