deco.h 19.9 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
/**CFile****************************************************************

  FileName    [deco.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [A simple decomposition tree/node data structure and its APIs.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
 
#ifndef __DEC_H__
#define __DEC_H__

24

Alan Mishchenko committed
25 26 27 28 29 30 31 32
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

33 34 35 36


ABC_NAMESPACE_HEADER_START

Alan Mishchenko committed
37

Alan Mishchenko committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Dec_Edge_t_ Dec_Edge_t;
struct Dec_Edge_t_
{
    unsigned          fCompl   :  1;   // the complemented bit
    unsigned          Node     : 30;   // the decomposition node pointed by the edge
};

typedef struct Dec_Node_t_ Dec_Node_t;
struct Dec_Node_t_
{
    Dec_Edge_t        eEdge0;          // the left child of the node
    Dec_Edge_t        eEdge1;          // the right child of the node
    // other info
55 56
    union { int       iFunc;           // the literal of the node (AIG)
    void *            pFunc; };        // the function of the node (BDD or AIG)
Alan Mishchenko committed
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 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
    unsigned          Level    : 14;   // the level of this node in the global AIG
    // printing info 
    unsigned          fNodeOr  :  1;   // marks the original OR node
    unsigned          fCompl0  :  1;   // marks the original complemented edge
    unsigned          fCompl1  :  1;   // marks the original complemented edge
    // latch info
    unsigned          nLat0    :  5;   // the number of latches on the first edge
    unsigned          nLat1    :  5;   // the number of latches on the second edge
    unsigned          nLat2    :  5;   // the number of latches on the output edge
};

typedef struct Dec_Graph_t_ Dec_Graph_t;
struct Dec_Graph_t_
{
    int               fConst;          // marks the constant 1 graph
    int               nLeaves;         // the number of leaves
    int               nSize;           // the number of nodes (including the leaves) 
    int               nCap;            // the number of allocated nodes
    Dec_Node_t *      pNodes;          // the array of leaves and internal nodes
    Dec_Edge_t        eRoot;           // the pointer to the topmost node
};

typedef struct Dec_Man_t_ Dec_Man_t;
struct Dec_Man_t_
{
    void *            pMvcMem;         // memory manager for MVC cover (used for factoring)
    Vec_Int_t *       vCubes;          // storage for cubes
    Vec_Int_t *       vLits;           // storage for literals 
    // precomputation information about 4-variable functions
    unsigned short *  puCanons;        // canonical forms
    char *            pPhases;         // canonical phases
    char *            pPerms;          // canonical permutations
    unsigned char *   pMap;            // mapping of functions into class numbers
};


////////////////////////////////////////////////////////////////////////
///                        ITERATORS                                 ///
////////////////////////////////////////////////////////////////////////

// interator throught the leaves
#define Dec_GraphForEachLeaf( pGraph, pLeaf, i )                                              \
    for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ )
// interator throught the internal nodes
#define Dec_GraphForEachNode( pGraph, pAnd, i )                                               \
    for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ )

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

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

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

  Synopsis    [Creates an edge pointing to the node in the given polarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )   
{
    Dec_Edge_t eEdge = { fCompl, Node }; 
    return eEdge; 
}

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

  Synopsis    [Converts the edge into unsigned integer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )   
{
    return (eEdge.Node << 1) | eEdge.fCompl; 
}

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

  Synopsis    [Converts unsigned integer into the edge.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )   
{
    return Dec_EdgeCreate( Edge >> 1, Edge & 1 ); 
}

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

  Synopsis    [Converts the edge into unsigned integer.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
172 173
static inline unsigned Dec_EdgeToInt_( Dec_Edge_t m )  { union { Dec_Edge_t x; unsigned y; } v; v.x = m; return v.y;  }
/*
Alan Mishchenko committed
174 175 176 177
static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )   
{
    return *(unsigned *)&eEdge;
}
178
*/
Alan Mishchenko committed
179 180 181 182 183 184 185 186 187 188 189 190

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

  Synopsis    [Converts unsigned integer into the edge.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
191 192
static inline Dec_Edge_t Dec_IntToEdge_( unsigned m )    { union { Dec_Edge_t x; unsigned y; } v; v.y = m; return v.x;  }
/*
Alan Mishchenko committed
193 194 195 196
static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )   
{
    return *(Dec_Edge_t *)&Edge;
}
197
*/
Alan Mishchenko committed
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212

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

  Synopsis    [Creates a graph with the given number of leaves.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )   
{
    Dec_Graph_t * pGraph;
Alan Mishchenko committed
213
    pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
Alan Mishchenko committed
214 215 216 217
    memset( pGraph, 0, sizeof(Dec_Graph_t) );
    pGraph->nLeaves = nLeaves;
    pGraph->nSize = nLeaves;
    pGraph->nCap = 2 * nLeaves + 50;
Alan Mishchenko committed
218
    pGraph->pNodes = ABC_ALLOC( Dec_Node_t, pGraph->nCap );
Alan Mishchenko committed
219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
    memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize );
    return pGraph;
}

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

  Synopsis    [Creates constant 0 graph.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateConst0()   
{
    Dec_Graph_t * pGraph;
Alan Mishchenko committed
237
    pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
Alan Mishchenko committed
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
    memset( pGraph, 0, sizeof(Dec_Graph_t) );
    pGraph->fConst = 1;
    pGraph->eRoot.fCompl = 1;
    return pGraph;
}

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

  Synopsis    [Creates constant 1 graph.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateConst1()   
{
    Dec_Graph_t * pGraph;
Alan Mishchenko committed
258
    pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
Alan Mishchenko committed
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297
    memset( pGraph, 0, sizeof(Dec_Graph_t) );
    pGraph->fConst = 1;
    return pGraph;
}

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

  Synopsis    [Creates the literal graph.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )   
{
    Dec_Graph_t * pGraph;
    assert( 0 <= iLeaf && iLeaf < nLeaves );
    pGraph = Dec_GraphCreate( nLeaves );
    pGraph->eRoot.Node   = iLeaf;
    pGraph->eRoot.fCompl = fCompl;
    return pGraph;
}

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

  Synopsis    [Creates a graph with the given number of leaves.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Dec_GraphFree( Dec_Graph_t * pGraph )   
{
Alan Mishchenko committed
298 299
    ABC_FREE( pGraph->pNodes );
    ABC_FREE( pGraph );
Alan Mishchenko committed
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 333 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 375 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 401 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 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560
}

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

  Synopsis    [Returns 1 if the graph is a constant.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )   
{
    return pGraph->fConst;
}

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

  Synopsis    [Returns 1 if the graph is constant 0.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )   
{
    return pGraph->fConst && pGraph->eRoot.fCompl;
}

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

  Synopsis    [Returns 1 if the graph is constant 1.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
{
    return pGraph->fConst && !pGraph->eRoot.fCompl;
}

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

  Synopsis    [Returns 1 if the graph is complemented.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )   
{
    return pGraph->eRoot.fCompl;
}

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

  Synopsis    [Checks if the graph is complemented.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Dec_GraphComplement( Dec_Graph_t * pGraph )   
{
    pGraph->eRoot.fCompl ^= 1;
}


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

  Synopsis    [Returns the number of leaves.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )   
{
    return pGraph->nLeaves;
}

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

  Synopsis    [Returns the number of internal nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )   
{
    return pGraph->nSize - pGraph->nLeaves;
}

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

  Synopsis    [Returns the pointer to the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )   
{
    return pGraph->pNodes + i;
}

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

  Synopsis    [Returns the pointer to the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph )   
{
    return pGraph->pNodes + pGraph->nSize - 1;
}

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

  Synopsis    [Returns the number of the given node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
{
    return pNode - pGraph->pNodes;
}

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

  Synopsis    [Check if the graph represents elementary variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )   
{
    return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
}

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

  Synopsis    [Check if the graph represents elementary variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
{
    return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
}

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

  Synopsis    [Returns the elementary variable elementary variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph )   
{
    assert( Dec_GraphIsVar( pGraph ) );
    return Dec_GraphNode( pGraph, pGraph->eRoot.Node );
}

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

  Synopsis    [Returns the number of the elementary variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph )   
{
    assert( Dec_GraphIsVar( pGraph ) );
    return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) );
}

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

  Synopsis    [Sets the root of the graph.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot )   
{
    pGraph->eRoot = eRoot;
}

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

  Synopsis    [Appends a new node to the graph.]

  Description [This procedure is meant for internal use.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph )   
{
    Dec_Node_t * pNode;
    if ( pGraph->nSize == pGraph->nCap )
    {
Alan Mishchenko committed
561
        pGraph->pNodes = ABC_REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); 
Alan Mishchenko committed
562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702
        pGraph->nCap   = 2 * pGraph->nCap;
    }
    pNode = pGraph->pNodes + pGraph->nSize++;
    memset( pNode, 0, sizeof(Dec_Node_t) );
    return pNode;
}

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

  Synopsis    [Creates an AND node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
{
    Dec_Node_t * pNode;
    // get the new node
    pNode = Dec_GraphAppendNode( pGraph );
    // set the inputs and other info
    pNode->eEdge0 = eEdge0;
    pNode->eEdge1 = eEdge1;
    pNode->fCompl0 = eEdge0.fCompl;
    pNode->fCompl1 = eEdge1.fCompl;
    return Dec_EdgeCreate( pGraph->nSize - 1, 0 );
}

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

  Synopsis    [Creates an OR node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
{
    Dec_Node_t * pNode;
    // get the new node
    pNode = Dec_GraphAppendNode( pGraph );
    // set the inputs and other info
    pNode->eEdge0 = eEdge0;
    pNode->eEdge1 = eEdge1;
    pNode->fCompl0 = eEdge0.fCompl;
    pNode->fCompl1 = eEdge1.fCompl;
    // make adjustments for the OR gate
    pNode->fNodeOr = 1;
    pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
    pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
    return Dec_EdgeCreate( pGraph->nSize - 1, 1 );
}

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

  Synopsis    [Creates an XOR node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1, int Type )
{
    Dec_Edge_t eNode0, eNode1, eNode;
    if ( Type == 0 )
    {
        // derive the first AND
        eEdge0.fCompl ^= 1;
        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        eEdge0.fCompl ^= 1;
        // derive the second AND
        eEdge1.fCompl ^= 1;
        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        // derive the final OR
        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
    }
    else
    {
        // derive the first AND
        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        // derive the second AND
        eEdge0.fCompl ^= 1;
        eEdge1.fCompl ^= 1;
        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        // derive the final OR
        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
        eNode.fCompl ^= 1;
    }
    return eNode;
}

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

  Synopsis    [Creates an XOR node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t eEdgeC, Dec_Edge_t eEdgeT, Dec_Edge_t eEdgeE, int Type )
{
    Dec_Edge_t eNode0, eNode1, eNode;
    if ( Type == 0 )
    {
        // derive the first AND
        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
        // derive the second AND
        eEdgeC.fCompl ^= 1;
        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
        // derive the final OR
        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
    }
    else
    {
        // complement the arguments
        eEdgeT.fCompl ^= 1;
        eEdgeE.fCompl ^= 1;
        // derive the first AND
        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
        // derive the second AND
        eEdgeC.fCompl ^= 1;
        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
        // derive the final OR
        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
        eNode.fCompl ^= 1;
    }
    return eNode;
}

703 704 705 706 707


ABC_NAMESPACE_HEADER_END


Alan Mishchenko committed
708 709 710 711 712 713 714

#endif

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