sfmNtk.c 12 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 36 37 38 39 40 41 42 43 44
/**CFile****************************************************************

  FileName    [sfmNtk.c]

  SystemName  [ABC: Logic synthesis and verification system.]

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

  Synopsis    [Logic network.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "sfmInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
45
void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed )
Alan Mishchenko committed
46
{
Alan Mishchenko committed
47 48 49 50
    Vec_Int_t * vArray;
    int i, k, Fanin;
    // check entries
    Vec_WecForEachLevel( vFanins, vArray, i )
Alan Mishchenko committed
51
    {
Alan Mishchenko committed
52
        // PIs have no fanins
Alan Mishchenko committed
53
        if ( i < nPis )
Alan Mishchenko committed
54 55 56
            assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
        // nodes are in a topo order; POs cannot be fanins
        Vec_IntForEachEntry( vArray, Fanin, k )
57 58
//            assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
            assert( Fanin + nPos < Vec_WecSize(vFanins) );
Alan Mishchenko committed
59 60
        // POs have one fanout
        if ( i + nPos >= Vec_WecSize(vFanins) )
Alan Mishchenko committed
61
            assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
Alan Mishchenko committed
62 63 64 65 66 67 68 69 70 71 72 73 74 75
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
76
void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
Alan Mishchenko committed
77 78 79 80
{
    Vec_Int_t * vArray;
    int i, k, Fanin;
    // count fanouts
Alan Mishchenko committed
81
    Vec_WecInit( vFanouts, Vec_WecSize(vFanins) );
Alan Mishchenko committed
82 83 84 85 86 87 88 89
    Vec_WecForEachLevel( vFanins, vArray, i )
        Vec_IntForEachEntry( vArray, Fanin, k )
            Vec_WecEntry( vFanouts, Fanin )->nSize++;
    // allocate fanins
    Vec_WecForEachLevel( vFanouts, vArray, i )
    {
        k = vArray->nSize; vArray->nSize = 0;
        Vec_IntGrow( vArray, k );
Alan Mishchenko committed
90
    }
Alan Mishchenko committed
91 92 93 94 95
    // add fanouts
    Vec_WecForEachLevel( vFanins, vArray, i )
        Vec_IntForEachEntry( vArray, Fanin, k )
            Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
    // verify
Alan Mishchenko committed
96
    Vec_WecForEachLevel( vFanouts, vArray, i )
Alan Mishchenko committed
97 98 99 100 101 102 103 104 105 106 107 108 109 110
        assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
111
static inline int Sfm_ObjLevelNew( Vec_Int_t * vArray, Vec_Int_t * vLevels, int fAddLevel )
Alan Mishchenko committed
112
{
Alan Mishchenko committed
113 114
    int k, Fanin, Level = 0;
    Vec_IntForEachEntry( vArray, Fanin, k )
Alan Mishchenko committed
115
        Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) );
116
    return Level + fAddLevel;
Alan Mishchenko committed
117
}
118
void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels, Vec_Str_t * vEmpty )
Alan Mishchenko committed
119
{
Alan Mishchenko committed
120
    Vec_Int_t * vArray;
Alan Mishchenko committed
121
    int i;
Alan Mishchenko committed
122
    assert( Vec_IntSize(vLevels) == 0 );
Alan Mishchenko committed
123
    Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
Alan Mishchenko committed
124
    Vec_WecForEachLevel( vFanins, vArray, i )
125
        Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels, Sfm_ObjAddsLevelArray(vEmpty, i)) );
Alan Mishchenko committed
126 127 128 129 130 131 132 133 134 135 136 137 138
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
139
static inline int Sfm_ObjLevelNewR( Vec_Int_t * vArray, Vec_Int_t * vLevelsR, int fAddLevel )
Alan Mishchenko committed
140 141 142 143
{
    int k, Fanout, LevelR = 0;
    Vec_IntForEachEntry( vArray, Fanout, k )
        LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) );
144
    return LevelR + fAddLevel;
Alan Mishchenko committed
145
}
146
void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * vEmpty )
Alan Mishchenko committed
147 148 149 150 151 152
{
    Vec_Int_t * vArray;
    int i;
    assert( Vec_IntSize(vLevelsR) == 0 );
    Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 );
    Vec_WecForEachLevelReverse( vFanouts, vArray, i )
153
        Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR, Sfm_ObjAddsLevelArray(vEmpty, i)) );
Alan Mishchenko committed
154 155 156 157 158 159 160 161 162 163 164 165 166
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
167
Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths )
Alan Mishchenko committed
168 169 170 171 172 173 174 175 176 177
{
    Sfm_Ntk_t * p;
    Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
    p = ABC_CALLOC( Sfm_Ntk_t, 1 );
    p->nObjs    = Vec_WecSize( vFanins );
    p->nPis     = nPis;
    p->nPos     = nPos;
    p->nNodes   = p->nObjs - p->nPis - p->nPos;
    // user data
    p->vFixed   = vFixed;
178
    p->vEmpty   = vEmpty;
Alan Mishchenko committed
179
    p->vTruths  = vTruths;
Alan Mishchenko committed
180 181
    p->vFanins  = *vFanins;
    ABC_FREE( vFanins );
Alan Mishchenko committed
182
    // attributes
Alan Mishchenko committed
183
    Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
184 185
    Sfm_CreateLevel( &p->vFanins, &p->vLevels, vEmpty );
    Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR, vEmpty );
Alan Mishchenko committed
186 187 188
    Vec_IntFill( &p->vCounts,   p->nObjs,  0 );
    Vec_IntFill( &p->vTravIds,  p->nObjs,  0 );
    Vec_IntFill( &p->vTravIds2, p->nObjs,  0 );
Alan Mishchenko committed
189 190
    Vec_IntFill( &p->vId2Var,   2*p->nObjs, -1 );
    Vec_IntFill( &p->vVar2Id,   2*p->nObjs, -1 );
Alan Mishchenko committed
191 192
    p->vCover   = Vec_IntAlloc( 1 << 16 );
    p->vCnfs    = Sfm_CreateCnf( p );
Alan Mishchenko committed
193 194
    return p;
}
Alan Mishchenko committed
195 196
void Sfm_NtkPrepare( Sfm_Ntk_t * p )
{
Alan Mishchenko committed
197
    p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
Alan Mishchenko committed
198
    p->vNodes    = Vec_IntAlloc( 1000 );
Alan Mishchenko committed
199 200
    p->vDivs     = Vec_IntAlloc( 100 );
    p->vRoots    = Vec_IntAlloc( 1000 );
Alan Mishchenko committed
201
    p->vTfo      = Vec_IntAlloc( 1000 );
Alan Mishchenko committed
202
    p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax );
Alan Mishchenko committed
203 204 205 206
    p->vOrder    = Vec_IntAlloc( 100 );
    p->vDivVars  = Vec_IntAlloc( 100 );
    p->vDivIds   = Vec_IntAlloc( 1000 );
    p->vLits     = Vec_IntAlloc( 100 );
Alan Mishchenko committed
207
    p->vValues   = Vec_IntAlloc( 100 );
Alan Mishchenko committed
208 209
    p->vClauses  = Vec_WecAlloc( 100 );
    p->vFaninMap = Vec_IntAlloc( 10 );
Alan Mishchenko committed
210
    p->pSat      = sat_solver_new();
Alan Mishchenko committed
211
    sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax );
Alan Mishchenko committed
212
}
Alan Mishchenko committed
213 214
void Sfm_NtkFree( Sfm_Ntk_t * p )
{
Alan Mishchenko committed
215 216
    // user data
    Vec_StrFree( p->vFixed );
217
    Vec_StrFreeP( &p->vEmpty );
Alan Mishchenko committed
218
    Vec_WrdFree( p->vTruths );
Alan Mishchenko committed
219
    Vec_WecErase( &p->vFanins );
Alan Mishchenko committed
220
    // attributes
Alan Mishchenko committed
221 222
    Vec_WecErase( &p->vFanouts );
    ABC_FREE( p->vLevels.pArray );
Alan Mishchenko committed
223
    ABC_FREE( p->vLevelsR.pArray );
Alan Mishchenko committed
224
    ABC_FREE( p->vCounts.pArray );
Alan Mishchenko committed
225
    ABC_FREE( p->vTravIds.pArray );
Alan Mishchenko committed
226
    ABC_FREE( p->vTravIds2.pArray );
Alan Mishchenko committed
227 228 229 230 231 232
    ABC_FREE( p->vId2Var.pArray );
    ABC_FREE( p->vVar2Id.pArray );
    Vec_WecFree( p->vCnfs );
    Vec_IntFree( p->vCover );
    // other data
    Vec_IntFreeP( &p->vNodes );
Alan Mishchenko committed
233 234
    Vec_IntFreeP( &p->vDivs  );
    Vec_IntFreeP( &p->vRoots );
Alan Mishchenko committed
235
    Vec_IntFreeP( &p->vTfo   );
Alan Mishchenko committed
236
    Vec_WrdFreeP( &p->vDivCexes );
Alan Mishchenko committed
237 238
    Vec_IntFreeP( &p->vOrder );
    Vec_IntFreeP( &p->vDivVars );
Alan Mishchenko committed
239
    Vec_IntFreeP( &p->vDivIds );
Alan Mishchenko committed
240
    Vec_IntFreeP( &p->vLits  );
Alan Mishchenko committed
241
    Vec_IntFreeP( &p->vValues );
Alan Mishchenko committed
242 243
    Vec_WecFreeP( &p->vClauses );
    Vec_IntFreeP( &p->vFaninMap );
Alan Mishchenko committed
244
    if ( p->pSat  ) sat_solver_delete( p->pSat );
Alan Mishchenko committed
245 246 247
    ABC_FREE( p );
}

Alan Mishchenko committed
248 249
/**Function*************************************************************

Alan Mishchenko committed
250 251 252 253 254 255 256 257 258 259 260 261
  Synopsis    [Performs resubstitution for the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
{
    int RetValue;
Alan Mishchenko committed
262 263
    assert( Sfm_ObjIsNode(p, iNode) );
    assert( !Sfm_ObjIsPo(p, iFanin) );
Alan Mishchenko committed
264 265 266 267 268 269 270 271 272
    RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin );
    assert( RetValue );
    RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );
    assert( RetValue );
}
void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
{
    if ( iFanin < 0 )
        return;
Alan Mishchenko committed
273 274
    assert( Sfm_ObjIsNode(p, iNode) );
    assert( !Sfm_ObjIsPo(p, iFanin) );
Alan Mishchenko committed
275 276 277 278 279 280 281 282
    assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 );
    assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 );
    Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin );
    Vec_IntPush( Sfm_ObjFoArray(p, iFanin), iNode );
}
void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
{
    int i, iFanin;
Alan Mishchenko committed
283
    if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) || Sfm_ObjIsFixed(p, iNode) )
Alan Mishchenko committed
284
        return;
Alan Mishchenko committed
285
    assert( Sfm_ObjIsNode(p, iNode) );
Alan Mishchenko committed
286 287 288
    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
    {
        int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
Alan Mishchenko committed
289
        Sfm_NtkDeleteObj_rec( p, iFanin );
Alan Mishchenko committed
290 291
    }
    Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
Alan Mishchenko committed
292
    Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
Alan Mishchenko committed
293 294 295 296
}
void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
{
    int i, iFanout;
297
    int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels, Sfm_ObjAddsLevel(p, iNode) );
Alan Mishchenko committed
298 299 300
    if ( LevelNew == Sfm_ObjLevel(p, iNode) )
        return;
    Sfm_ObjSetLevel( p, iNode, LevelNew );
Alan Mishchenko committed
301 302 303 304 305 306
    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
        Sfm_NtkUpdateLevel_rec( p, iFanout );
}
void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
{
    int i, iFanin;
307
    int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR, Sfm_ObjAddsLevel(p, iNode) );
Alan Mishchenko committed
308 309 310 311 312
    if ( LevelNew == Sfm_ObjLevelR(p, iNode) )
        return;
    Sfm_ObjSetLevelR( p, iNode, LevelNew );
    Sfm_ObjForEachFanin( p, iNode, iFanin, i )
        Sfm_NtkUpdateLevelR_rec( p, iFanin );
Alan Mishchenko committed
313 314 315 316
}
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
{
    int iFanin = Sfm_ObjFanin( p, iNode, f );
Alan Mishchenko committed
317
    assert( Sfm_ObjIsNode(p, iNode) );
Alan Mishchenko committed
318 319 320 321 322 323
    assert( iFanin != iFaninNew );
    if ( uTruth == 0 || ~uTruth == 0 )
    {
        Sfm_ObjForEachFanin( p, iNode, iFanin, f )
        {
            int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
Alan Mishchenko committed
324
            Sfm_NtkDeleteObj_rec( p, iFanin );
Alan Mishchenko committed
325 326 327 328 329 330 331 332 333 334 335
        }
        Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
    }
    else
    {
        // replace old fanin by new fanin
        Sfm_NtkRemoveFanin( p, iNode, iFanin );
        Sfm_NtkAddFanin( p, iNode, iFaninNew );
        // recursively remove MFFC
        Sfm_NtkDeleteObj_rec( p, iFanin );
    }
Alan Mishchenko committed
336 337
    // update logic level
    Sfm_NtkUpdateLevel_rec( p, iNode );
Alan Mishchenko committed
338 339 340 341
    if ( iFaninNew != -1 )
        Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
    if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
        Sfm_NtkUpdateLevelR_rec( p, iFanin );
Alan Mishchenko committed
342 343 344 345 346 347 348
    // update truth table
    Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
    Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
}

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

Alan Mishchenko committed
349 350 351 352 353 354 355 356 357 358 359
  Synopsis    [Public APIs of this network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
{
Alan Mishchenko committed
360
    return Vec_WecEntry( &p->vFanins, i );
Alan Mishchenko committed
361
}
Alan Mishchenko committed
362
word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
Alan Mishchenko committed
363
{
Alan Mishchenko committed
364
    return Vec_WrdEntryP( p->vTruths, i );
Alan Mishchenko committed
365 366 367 368 369
}
int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
{
    return (int)Vec_StrEntry( p->vFixed, i );
}
Alan Mishchenko committed
370 371 372 373
int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
{
    return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
}
Alan Mishchenko committed
374 375 376 377 378 379 380 381

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


ABC_NAMESPACE_IMPL_END