rwrDec.c 4.93 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    [rwrDec.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [DAG-aware AIG rewriting package.]

  Synopsis    [Evaluation and decomposition procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "rwr.h"
22
#include "bool/dec/dec.h"
Alan Mishchenko committed
23

24 25 26
ABC_NAMESPACE_IMPL_START


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

Alan Mishchenko committed
31 32
static Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
static Dec_Edge_t    Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph );
Alan Mishchenko committed
33 34

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

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

  Synopsis    [Preprocesses computed library of subgraphs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Rwr_ManPreprocess( Rwr_Man_t * p )
{
Alan Mishchenko committed
51
    Dec_Graph_t * pGraph;
Alan Mishchenko committed
52 53 54
    Rwr_Node_t * pNode;
    int i, k;
    // put the nodes into the structure
Alan Mishchenko committed
55
    p->pMapInv  = ABC_ALLOC( unsigned short, 222 );
Alan Mishchenko committed
56
    memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
Alan Mishchenko committed
57 58 59 60 61 62 63 64 65
    p->vClasses = Vec_VecStart( 222 );
    for ( i = 0; i < p->nFuncs; i++ )
    {
        if ( p->pTable[i] == NULL )
            continue;
        // consider all implementations of this function
        for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
        {
            assert( pNode->uTruth == p->pTable[i]->uTruth );
Alan Mishchenko committed
66
            assert( p->pMap[pNode->uTruth] < 222 ); // Guaranteed to be >=0 b/c unsigned
Alan Mishchenko committed
67
            Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
Alan Mishchenko committed
68
            p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth];
Alan Mishchenko committed
69 70
        }
    }
Alan Mishchenko committed
71
    // compute decomposition forms for each node and verify them
72
    Vec_VecForEachEntry( Rwr_Node_t *, p->vClasses, pNode, i, k )
Alan Mishchenko committed
73 74 75 76 77
    {
        pGraph = Rwr_NodePreprocess( p, pNode );
        pNode->pNext = (Rwr_Node_t *)pGraph;
        assert( pNode->uTruth == (Dec_GraphDeriveTruth(pGraph) & 0xFFFF) );
    }
Alan Mishchenko committed
78 79 80 81 82 83 84 85 86 87 88 89 90
}

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

  Synopsis    [Preprocesses subgraphs rooted at this node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
91
Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
Alan Mishchenko committed
92
{
Alan Mishchenko committed
93 94 95
    Dec_Graph_t * pGraph;
    Dec_Edge_t eRoot;
    assert( !Rwr_IsComplement(pNode) );
Alan Mishchenko committed
96 97
    // consider constant
    if ( pNode->uTruth == 0 )
Alan Mishchenko committed
98
        return Dec_GraphCreateConst0();
Alan Mishchenko committed
99 100
    // consider the case of elementary var
    if ( pNode->uTruth == 0x00FF )
Alan Mishchenko committed
101 102 103
        return Dec_GraphCreateLeaf( 3, 4, 1 );
    // start the subgraphs
    pGraph = Dec_GraphCreate( 4 );
Alan Mishchenko committed
104 105
    // collect the nodes
    Rwr_ManIncTravId( p );
Alan Mishchenko committed
106 107 108
    eRoot = Rwr_TravCollect_rec( p, pNode, pGraph );
    Dec_GraphSetRoot( pGraph, eRoot );
    return pGraph;
Alan Mishchenko committed
109 110 111 112 113 114 115 116 117 118 119 120 121
}

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

  Synopsis    [Adds one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
122
Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph )
Alan Mishchenko committed
123
{
Alan Mishchenko committed
124
    Dec_Edge_t eNode0, eNode1, eNode;
Alan Mishchenko committed
125 126
    // elementary variable
    if ( pNode->fUsed )
Alan Mishchenko committed
127
        return Dec_EdgeCreate( pNode->Id - 1, 0 );
Alan Mishchenko committed
128 129
    // previously visited node
    if ( pNode->TravId == p->nTravIds )
Alan Mishchenko committed
130
        return Dec_IntToEdge( pNode->Volume );
Alan Mishchenko committed
131 132
    pNode->TravId = p->nTravIds;
    // solve for children
Alan Mishchenko committed
133 134 135 136 137 138
    eNode0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), pGraph );
    if ( Rwr_IsComplement(pNode->p0) )    
        eNode0.fCompl = !eNode0.fCompl;
    eNode1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), pGraph );
    if ( Rwr_IsComplement(pNode->p1) )    
        eNode1.fCompl = !eNode1.fCompl;
Alan Mishchenko committed
139 140
    // create the decomposition node(s)
    if ( pNode->fExor )
Alan Mishchenko committed
141
        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1, 0 );
Alan Mishchenko committed
142
    else
Alan Mishchenko committed
143 144 145 146
        eNode = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
    // save the result
    pNode->Volume = Dec_EdgeToInt( eNode );
    return eNode;
Alan Mishchenko committed
147 148 149 150 151 152 153
}

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


154 155
ABC_NAMESPACE_IMPL_END