fxuCreate.c 15.7 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
/**CFile****************************************************************

  FileName    [fxuCreate.c]

  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

  Synopsis    [Create matrix from covers and covers from matrix.]

  Author      [MVSIS Group]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: fxuCreate.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]

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

#include "fxuInt.h"
#include "fxu.h"

22 23 24
ABC_NAMESPACE_IMPL_START


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

Alan Mishchenko committed
29
static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder );
Alan Mishchenko committed
30 31 32
static int         Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
static void        Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
static Fxu_Cube *  Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
Alan Mishchenko committed
33
static int * s_pLits;
Alan Mishchenko committed
34

Alan Mishchenko committed
35 36
extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );

Alan Mishchenko committed
37
////////////////////////////////////////////////////////////////////////
Alan Mishchenko committed
38
///                     FUNCTION DEFINITIONS                         ///
Alan Mishchenko committed
39 40 41 42
////////////////////////////////////////////////////////////////////////

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

Alan Mishchenko committed
43
  Synopsis    [Creates the sparse matrix from the array of SOPs.]
Alan Mishchenko committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
{
    Fxu_Matrix * p;
    Fxu_Var * pVar;
    Fxu_Cube * pCubeFirst, * pCubeNew;
    Fxu_Cube * pCube1, * pCube2;
Alan Mishchenko committed
58
    Vec_Int_t * vFanins;
Alan Mishchenko committed
59 60 61 62 63 64 65 66 67 68 69 70
    char * pSopCover;
    char * pSopCube;
    int * pOrder, nBitsMax;
    int i, v, c;
    int nCubesTotal;
    int nPairsTotal;
    int nPairsStore;
    int nCubes;
    int iCube, iPair;
    int nFanins;

    // collect all sorts of statistics
Alan Mishchenko committed
71 72 73
    nCubesTotal =  0;
    nPairsTotal =  0;
    nPairsStore =  0;
Alan Mishchenko committed
74
    nBitsMax    = -1; 
Alan Mishchenko committed
75
    for ( i = 0; i < pData->nNodesOld; i++ )
76
        if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
Alan Mishchenko committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
        {
            nCubes       = Abc_SopGetCubeNum( pSopCover );
            nFanins      = Abc_SopGetVarNum( pSopCover );
            assert( nFanins > 1 && nCubes > 0 );

            nCubesTotal += nCubes;
            nPairsTotal += nCubes * (nCubes - 1) / 2;
            nPairsStore += nCubes * nCubes;
            if ( nBitsMax < nFanins )
                nBitsMax = nFanins;
        }
    if ( nBitsMax <= 0 )
    {
        printf( "The current network does not have SOPs to perform extraction.\n" );
        return NULL;
    }
Alan Mishchenko committed
93

Alan Mishchenko committed
94
    if ( nPairsStore > 50000000 )
Alan Mishchenko committed
95 96 97 98
    {
        printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
        return NULL;
    }
Alan Mishchenko committed
99

Alan Mishchenko committed
100 101 102
    // start the matrix
    p = Fxu_MatrixAllocate();
    // create the column labels 
Alan Mishchenko committed
103
    p->ppVars = ABC_ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
Alan Mishchenko committed
104 105 106 107
    for ( i = 0; i < 2 * pData->nNodesOld; i++ )
        p->ppVars[i] = Fxu_MatrixAddVar( p );

    // allocate storage for all cube pairs at once
Alan Mishchenko committed
108 109
    p->pppPairs = ABC_ALLOC( Fxu_Pair **, nCubesTotal + 100 );
    p->ppPairs  = ABC_ALLOC( Fxu_Pair *,  nPairsStore + 100 );
Alan Mishchenko committed
110 111 112 113
    memset( p->ppPairs, 0, sizeof(Fxu_Pair *) * nPairsStore );
    iCube = 0;
    iPair = 0;
    for ( i = 0; i < pData->nNodesOld; i++ )
114
        if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
Alan Mishchenko committed
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
        {
            // get the number of cubes
            nCubes = Abc_SopGetCubeNum( pSopCover );
            // get the new var in the matrix
            pVar = p->ppVars[2*i+1];
            // assign the pair storage
            pVar->nCubes     = nCubes;
            if ( nCubes > 0 )
            {
                pVar->ppPairs    = p->pppPairs + iCube;
                pVar->ppPairs[0] = p->ppPairs  + iPair;
                for ( v = 1; v < nCubes; v++ )
                    pVar->ppPairs[v] = pVar->ppPairs[v-1] + nCubes;
            }
            // update
            iCube += nCubes;
            iPair += nCubes * nCubes;
        }
    assert( iCube == nCubesTotal );
    assert( iPair == nPairsStore );


    // allocate room for the reordered literals
Alan Mishchenko committed
138
    pOrder = ABC_ALLOC( int, nBitsMax );
Alan Mishchenko committed
139 140
    // create the rows
    for ( i = 0; i < pData->nNodesOld; i++ )
141
    if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
Alan Mishchenko committed
142 143 144 145 146 147
    {
        // get the new var in the matrix
        pVar = p->ppVars[2*i+1];
        // here we sort the literals of the cover
        // in the increasing order of the numbers of the corresponding nodes
        // because literals should be added to the matrix in this order
148
        vFanins = (Vec_Int_t *)pData->vFanins->pArray[i];
Alan Mishchenko committed
149 150 151 152 153 154 155
        s_pLits = vFanins->pArray;
        // start the variable order
        nFanins = Abc_SopGetVarNum( pSopCover );
        for ( v = 0; v < nFanins; v++ )
            pOrder[v] = v;
        // reorder the fanins
        qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
Alan Mishchenko committed
156
        assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
Alan Mishchenko committed
157 158 159 160 161 162
        // create the corresponding cubes in the matrix
        pCubeFirst = NULL;
        c = 0;
        Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
        {
            // create the cube
Alan Mishchenko committed
163
            pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
Alan Mishchenko committed
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
            Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
            if ( pCubeFirst == NULL )
                pCubeFirst = pCubeNew;
            pCubeNew->pFirst = pCubeFirst;
        }
        // set the first cube of this var
        pVar->pFirst = pCubeFirst;
        // create the divisors without preprocessing
        if ( nPairsTotal <= pData->nPairsMax )
        {
            for ( pCube1 = pCubeFirst; pCube1; pCube1 = pCube1->pNext )
                for ( pCube2 = pCube1? pCube1->pNext: NULL; pCube2; pCube2 = pCube2->pNext )
                    Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
        }
    }
Alan Mishchenko committed
179
    ABC_FREE( pOrder );
Alan Mishchenko committed
180 181 182

    // consider the case when cube pairs should be preprocessed
    // before adding them to the set of divisors
Alan Mishchenko committed
183 184 185 186 187 188 189 190
//    if ( pData->fVerbose )
//        printf( "The total number of cube pairs is %d.\n", nPairsTotal );
    if ( nPairsTotal > 10000000 )
    {
        printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
        printf( "that the user changes the network by reducing the size of logic node and\n" );
        printf( "consequently the number of cube pairs to be processed by this command.\n" );
191
        printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
Alan Mishchenko committed
192 193 194
        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
        return NULL;
    }
Alan Mishchenko committed
195
    if ( nPairsTotal > pData->nPairsMax )
Alan Mishchenko committed
196 197 198 199
        if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
            return NULL;
//    if ( pData->fVerbose )
//        printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
Alan Mishchenko committed
200

201 202 203 204 205 206 207 208 209 210 211 212
    if ( p->lVars.nItems > 1000000 )
    {
        printf( "The total number of variables is more than 1,000,000.\n" );
        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
        printf( "that the user changes the network by reducing the size of logic node and\n" );
        printf( "consequently the number of cube pairs to be processed by this command.\n" );
        printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
        return NULL;
    }


Alan Mishchenko committed
213
    // add the var pairs to the heap
Alan Mishchenko committed
214
    Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
Alan Mishchenko committed
215

Alan Mishchenko committed
216
    // print stats
Alan Mishchenko committed
217 218 219 220 221 222 223 224
    if ( pData->fVerbose )
    {
        double Density;
        Density = ((double)p->nEntries) / p->lVars.nItems / p->lCubes.nItems;
        fprintf( stdout, "Matrix: [vars x cubes] = [%d x %d]  ",
            p->lVars.nItems, p->lCubes.nItems );
        fprintf( stdout, "Lits = %d  Density = %.5f%%\n", 
            p->nEntries, Density );
Alan Mishchenko committed
225 226
        fprintf( stdout, "1-cube divs = %6d. (Total = %6d)  ",  p->lSingles.nItems, p->nSingleTotal );
        fprintf( stdout, "2-cube divs = %6d. (Total = %6d)",  p->nDivsTotal, nPairsTotal );
Alan Mishchenko committed
227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
        fprintf( stdout, "\n" );
    }
//    Fxu_MatrixPrint( stdout, p );
    return p;
}

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

  Synopsis    [Adds one cube with literals to the matrix.]

  Description [Create the cube and literals in the matrix corresponding 
  to the given cube in the SOP cover. Co-singleton transform is performed here.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
245
void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
Alan Mishchenko committed
246 247 248 249 250 251 252 253 254
{
    Fxu_Var * pVar;
    int Value, i;
    // add literals to the matrix
    Abc_CubeForEachVar( pSopCube, Value, i )
    {
        Value = pSopCube[pOrder[i]];
        if ( Value == '0' )
        {
Alan Mishchenko committed
255
            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ];  // CST
Alan Mishchenko committed
256 257 258 259
            Fxu_MatrixAddLiteral( p, pCube, pVar );
        }
        else if ( Value == '1' )
        {
Alan Mishchenko committed
260
            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ];  // CST
Alan Mishchenko committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
            Fxu_MatrixAddLiteral( p, pCube, pVar );
        }
    }
}


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

  Synopsis    [Creates the new array of Sop covers from the sparse matrix.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
{
    Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
    char * pSopCover;
Alan Mishchenko committed
282
    int iNode, n;
Alan Mishchenko committed
283 284 285 286 287 288

    // get the first cube of the first internal node 
    pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );

    // go through the internal nodes
    for ( n = 0; n < pData->nNodesOld; n++ )
289
    if ( (pSopCover = (char *)pData->vSops->pArray[n]) )
Alan Mishchenko committed
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332
    {
        // get the number of this node
        iNode = n;
        // get the next first cube
        pCubeNext = Fxu_CreateCoversFirstCube(  p, pData, iNode + 1 );
        // check if there any new variables in these cubes
        for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
            if ( pCube->lLits.pTail && pCube->lLits.pTail->iVar >= 2 * pData->nNodesOld )
                break;
        if ( pCube != pCubeNext )
            Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
        // update the first cube
        pCubeFirst = pCubeNext;
    }

    // add the covers for the extracted nodes
    for ( n = 0; n < pData->nNodesNew; n++ )
    {
        // get the number of this node
        iNode = pData->nNodesOld + n;
        // get the next first cube
        pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
        // the node should be added
        Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
        // update the first cube
        pCubeFirst = pCubeNext;
    }
}

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

  Synopsis    [Create Sop covers for one node that has changed.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
{
    Vec_Int_t * vInputsNew;
Alan Mishchenko committed
333
    char * pSopCover, * pSopCube;
Alan Mishchenko committed
334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
    Fxu_Var * pVar;
    Fxu_Cube * pCube;
    Fxu_Lit * pLit;
    int iNum, nCubes, v;

    // collect positive polarity variable in the cubes between pCubeFirst and pCubeNext
    Fxu_MatrixRingVarsStart( p );
    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
        for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
        {
            pVar = p->ppVars[ 2 * (pLit->pVar->iVar/2) + 1 ];
            if ( pVar->pOrder == NULL )
                Fxu_MatrixRingVarsAdd( p, pVar );
        }
    Fxu_MatrixRingVarsStop( p );

    // collect the variable numbers
    vInputsNew = Vec_IntAlloc( 4 );
    Fxu_MatrixForEachVarInRing( p, pVar )
        Vec_IntPush( vInputsNew, pVar->iVar / 2 );
    Fxu_MatrixRingVarsUnmark( p );

    // sort the vars by their number
    Vec_IntSort( vInputsNew, 0 );

    // mark the vars with their numbers in the sorted array
    for ( v = 0; v < vInputsNew->nSize; v++ )
    {
        p->ppVars[ 2 * vInputsNew->pArray[v] + 0 ]->lLits.nItems = v; // hack - reuse lLits.nItems
        p->ppVars[ 2 * vInputsNew->pArray[v] + 1 ]->lLits.nItems = v; // hack - reuse lLits.nItems
    }

    // count the number of cubes
    nCubes = 0;
    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
        if ( pCube->lLits.nItems )
            nCubes++;

    // allocate room for the new cover
    pSopCover = Abc_SopStart( pData->pManSop, nCubes, vInputsNew->nSize );
    // set the correct polarity of the cover
375
    if ( iNode < pData->nNodesOld && Abc_SopGetPhase( (char *)pData->vSops->pArray[iNode] ) == 0 )
Alan Mishchenko committed
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400
        Abc_SopComplement( pSopCover );

    // add the cubes
    nCubes = 0;
    for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
    {
        if ( pCube->lLits.nItems == 0 )
            continue;
        // get hold of the SOP cube
        pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
        // insert literals
        for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
        {
            iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems
            assert( iNum < vInputsNew->nSize );
            if ( pLit->pVar->iVar / 2 < pData->nNodesOld )
                pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1';   // reverse CST
            else
                pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0';   // no CST
        }
        // count the cube
        nCubes++;
    }
    assert( nCubes == Abc_SopGetCubeNum(pSopCover) );

Alan Mishchenko committed
401
    // set the new cover and the array of fanins
Alan Mishchenko committed
402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439
    pData->vSopsNew->pArray[iNode]   = pSopCover;
    pData->vFaninsNew->pArray[iNode] = vInputsNew;
}


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

  Synopsis    [Adds the var to storage.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iVar )
{
    int v;
    for ( v = iVar; v < pData->nNodesOld + pData->nNodesNew; v++ )
        if ( p->ppVars[ 2*v + 1 ]->pFirst )
            return p->ppVars[ 2*v + 1 ]->pFirst;
    return NULL;
}

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

  Synopsis    [Compares the vars by their number.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
{
Alan Mishchenko committed
440
    return s_pLits[*ptrX] - s_pLits[*ptrY];
Alan Mishchenko committed
441 442 443 444 445
} 

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////
446 447
ABC_NAMESPACE_IMPL_END