rwrLib.c 11 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
/**CFile****************************************************************

  FileName    [rwrLib.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [DAG-aware AIG rewriting package.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "rwr.h"

23 24 25
ABC_NAMESPACE_IMPL_START


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

Alan Mishchenko committed
30 31
static Rwr_Node_t *        Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
static void                Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode );
Alan Mishchenko committed
32 33

////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
34
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
35 36 37 38 39 40 41 42 43 44 45 46 47
////////////////////////////////////////////////////////////////////////

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

  Synopsis    [Precomputes the forest in the manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
48
void Rwr_ManPrecompute( Rwr_Man_t * p )
Alan Mishchenko committed
49 50 51 52 53 54
{
    Rwr_Node_t * p0, * p1;
    int i, k, Level, Volume;
    int LevelOld = -1;
    int nNodes;

55 56
    Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 1 )
    Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p1, k, 1 )
Alan Mishchenko committed
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
    {
        if ( LevelOld < (int)p0->Level )
        {
            LevelOld = p0->Level;
            printf( "Starting level %d  (at %d nodes).\n", LevelOld+1, i );
            printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
                p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
        }

        if ( k == i )
            break;
//        if ( p0->Level + p1->Level > 6 ) // hard
//            break;

        if ( p0->Level + p1->Level > 5 ) // easy 
            break;

//        if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
//            break;

        // compute the level and volume of the new nodes
78
        Level  = 1 + Abc_MaxInt( p0->Level, p1->Level );
Alan Mishchenko committed
79
        Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
Alan Mishchenko committed
80
        // try four different AND nodes
Alan Mishchenko committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
        Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
        Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
        Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
        Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
        // try EXOR
        Rwr_ManTryNode( p,         p0 ,         p1 , 1, Level, Volume + 1 );
        // report the progress
        if ( p->nConsidered % 50000000 == 0 )
            printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
                p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
        // quit after some time
        if ( p->vForest->nSize == RWR_LIMIT + 5 )
        {
            printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
                p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
            goto save;
        }
    }
save :

    // mark the relevant ones
    Rwr_ManIncTravId( p );
    k = 5;
    nNodes = 0;
105
    Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
Alan Mishchenko committed
106 107 108 109 110 111 112 113
        if ( p0->uTruth == p->puCanons[p0->uTruth] )
        {
            Rwr_MarkUsed_rec( p, p0 );
            nNodes++;
        }

    // compact the array by throwing away non-canonical
    k = 5;
114
    Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
Alan Mishchenko committed
115 116 117
        if ( p0->fUsed )
        {
            p->vForest->pArray[k] = p0;
Alan Mishchenko committed
118
            p0->Id = k++;
Alan Mishchenko committed
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
        }
    p->vForest->nSize = k;
    printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
}

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

  Synopsis    [Adds one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
135
Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
Alan Mishchenko committed
136 137
{
    Rwr_Node_t * pOld, * pNew, ** ppPlace;
Alan Mishchenko committed
138
    unsigned uTruth;
Alan Mishchenko committed
139 140 141 142 143 144 145 146 147 148 149
    // compute truth table, level, volume
    p->nConsidered++;
    if ( fExor )
    {
//        printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
        uTruth = (p0->uTruth ^ p1->uTruth);
    }
    else
        uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
                 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
    // skip non-practical classes
Alan Mishchenko committed
150
    if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
Alan Mishchenko committed
151 152
        return NULL;
    // enumerate through the nodes with the same canonical form
Alan Mishchenko committed
153
    ppPlace = p->pTable + uTruth;
Alan Mishchenko committed
154 155 156 157 158 159 160 161 162
    for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
    {
        if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
            return NULL;
        if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
            return NULL;
//        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
//            return NULL;
    }
Alan Mishchenko committed
163
/*
Alan Mishchenko committed
164 165 166 167 168 169 170 171 172 173
    // enumerate through the nodes with the opposite polarity
    for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
    {
        if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
            return NULL;
        if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
            return NULL;
//        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
//            return NULL;
    }
Alan Mishchenko committed
174
*/
Alan Mishchenko committed
175 176 177
    // count the classes
    if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
        p->nClasses++;
Alan Mishchenko committed
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
    // create the new node
    pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
    pNew->Id     = p->vForest->nSize;
    pNew->TravId = 0;
    pNew->uTruth = uTruth;
    pNew->Level  = Level;
    pNew->Volume = Volume;
    pNew->fUsed  = 0;
    pNew->fExor  = fExor;
    pNew->p0     = p0;
    pNew->p1     = p1;
    pNew->pNext  = NULL;
    Vec_PtrPush( p->vForest, pNew );
    *ppPlace     = pNew;
    return pNew;
}

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

  Synopsis    [Adds one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
206
Rwr_Node_t * Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
Alan Mishchenko committed
207
{
Alan Mishchenko committed
208 209
    Rwr_Node_t * pNew;
    unsigned uTruth;
Alan Mishchenko committed
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
    // compute truth table, leve, volume
    p->nConsidered++;
    if ( fExor )
        uTruth = (p0->uTruth ^ p1->uTruth);
    else
        uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
                 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
    // create the new node
    pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
    pNew->Id     = p->vForest->nSize;
    pNew->TravId = 0;
    pNew->uTruth = uTruth;
    pNew->Level  = Level;
    pNew->Volume = Volume;
    pNew->fUsed  = 0;
    pNew->fExor  = fExor;
    pNew->p0     = p0;
    pNew->p1     = p1;
    pNew->pNext  = NULL;
    Vec_PtrPush( p->vForest, pNew );
    // do not add if the node is not essential
Alan Mishchenko committed
231
    if ( uTruth != p->puCanons[uTruth] )
Alan Mishchenko committed
232 233 234 235
        return pNew;

    // add to the list
    p->nAdded++;
Alan Mishchenko committed
236
    if ( p->pTable[uTruth] == NULL )
Alan Mishchenko committed
237
        p->nClasses++;
Alan Mishchenko committed
238
    Rwr_ListAddToTail( p->pTable + uTruth, pNew );
Alan Mishchenko committed
239 240 241 242 243 244 245 246 247 248 249 250 251 252
    return pNew;
}

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

  Synopsis    [Adds one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
253
Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute )
Alan Mishchenko committed
254 255 256 257 258 259 260 261 262 263 264
{
    Rwr_Node_t * pNew;
    pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
    pNew->Id     = p->vForest->nSize;
    pNew->TravId = 0;
    pNew->uTruth = uTruth;
    pNew->Level  = 0;
    pNew->Volume = 0;
    pNew->fUsed  = 1;
    pNew->fExor  = 0;
    pNew->p0     = NULL;
Alan Mishchenko committed
265 266
    pNew->p1     = NULL;    
    pNew->pNext  = NULL;
Alan Mishchenko committed
267
    Vec_PtrPush( p->vForest, pNew );
Alan Mishchenko committed
268
    if ( fPrecompute )
Alan Mishchenko committed
269
        Rwr_ListAddToTail( p->pTable + uTruth, pNew );
Alan Mishchenko committed
270 271 272 273
    return pNew;
}


Alan Mishchenko committed
274 275 276

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

Alan Mishchenko committed
277
  Synopsis    [Adds one node.]
Alan Mishchenko committed
278 279 280 281 282 283 284 285

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
286
void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode )
Alan Mishchenko committed
287
{
Alan Mishchenko committed
288
    if ( pNode->fUsed || pNode->TravId == p->nTravIds )
Alan Mishchenko committed
289
        return;
Alan Mishchenko committed
290 291 292 293
    pNode->TravId = p->nTravIds;
    pNode->fUsed = 1;
    Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
    Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
Alan Mishchenko committed
294 295 296 297
}

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

Alan Mishchenko committed
298
  Synopsis    [Adds one node.]
Alan Mishchenko committed
299 300 301 302 303 304 305 306

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
307
void Rwr_Trav_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
Alan Mishchenko committed
308
{
Alan Mishchenko committed
309 310 311 312 313 314 315 316
    if ( pNode->fUsed || pNode->TravId == p->nTravIds )
        return;
    pNode->TravId = p->nTravIds;
    (*pVolume)++;
    if ( pNode->fExor )
        (*pVolume)++;
    Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
    Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
Alan Mishchenko committed
317 318 319 320
}

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

Alan Mishchenko committed
321
  Synopsis    [Adds one node.]
Alan Mishchenko committed
322 323 324 325 326 327 328 329

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
330
int Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
Alan Mishchenko committed
331
{
Alan Mishchenko committed
332 333 334 335 336
    int Volume = 0;
    Rwr_ManIncTravId( p );
    Rwr_Trav_rec( p, p0, &Volume );
    Rwr_Trav_rec( p, p1, &Volume );
    return Volume;
Alan Mishchenko committed
337 338 339 340
}

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

Alan Mishchenko committed
341
  Synopsis    [Adds one node.]
Alan Mishchenko committed
342 343 344 345 346 347 348 349

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
350
void Rwr_ManIncTravId( Rwr_Man_t * p )
Alan Mishchenko committed
351
{
Alan Mishchenko committed
352 353
    Rwr_Node_t * pNode;
    int i;
Alan Mishchenko committed
354 355
    if ( p->nTravIds++ < 0x8FFFFFFF )
        return;
356
    Vec_PtrForEachEntry( Rwr_Node_t *, p->vForest, pNode, i )
Alan Mishchenko committed
357 358
        pNode->TravId = 0;
    p->nTravIds = 1;
Alan Mishchenko committed
359 360 361 362 363 364 365
}

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


366 367
ABC_NAMESPACE_IMPL_END