dchSweep.c 4.99 KB
Newer Older
Alan Mishchenko committed
1 2
/**CFile****************************************************************

Alan Mishchenko committed
3
  FileName    [dchSweep.c]
Alan Mishchenko committed
4 5 6 7 8

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Choice computation for tech-mapping.]

Alan Mishchenko committed
9
  Synopsis    [One round of SAT sweeping.]
Alan Mishchenko committed
10 11 12 13 14 15 16

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

Alan Mishchenko committed
17
  Revision    [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
Alan Mishchenko committed
18 19 20 21

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

#include "dchInt.h"
22
#include "misc/bar/bar.h"
Alan Mishchenko committed
23

24 25 26
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }

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

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

  Synopsis    [Performs fraiging for one node.]

  Description [Returns the fraiged node.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
{ 
    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
    int RetValue;
    // get representative of this class
    pObjRepr = Aig_ObjRepr( p->pAigTotal, pObj );
    if ( pObjRepr == NULL )
        return;
    // get the fraiged node
    pObjFraig = Dch_ObjFraig( pObj );
Alan Mishchenko committed
59 60
    if ( pObjFraig == NULL )
        return;
Alan Mishchenko committed
61 62
    // get the fraiged representative
    pObjReprFraig = Dch_ObjFraig( pObjRepr );
Alan Mishchenko committed
63 64
    if ( pObjReprFraig == NULL )
        return;
Alan Mishchenko committed
65 66 67 68 69 70 71 72 73 74
    // if the fraiged nodes are the same, return
    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
    {
        // remember the proved equivalence
        p->pReprsProved[ pObj->Id ] = pObjRepr;
        return;
    }
    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
    RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
    if ( RetValue == -1 ) // timed out
Alan Mishchenko committed
75 76
    {
        Dch_ObjSetFraig( pObj, NULL );
Alan Mishchenko committed
77
        return;
Alan Mishchenko committed
78
    }
Alan Mishchenko committed
79 80 81 82 83 84 85 86 87
    if ( RetValue == 1 )  // proved equivalent
    {
        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
        Dch_ObjSetFraig( pObj, pObjFraig2 );
        // remember the proved equivalence
        p->pReprsProved[ pObj->Id ] = pObjRepr;
        return;
    }
    // disproved the equivalence
Alan Mishchenko committed
88 89 90 91
    if ( p->pPars->fSimulateTfo )
        Dch_ManResimulateCex( p, pObj, pObjRepr );
    else
        Dch_ManResimulateCex2( p, pObj, pObjRepr );
Alan Mishchenko committed
92
    assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
Alan Mishchenko committed
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
}

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

  Synopsis    [Performs fraiging for the internal nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManSweep( Dch_Man_t * p )
{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    // map constants and PIs
    p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) );
    Aig_ManCleanData( p->pAigTotal );
    Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
115 116
    Aig_ManForEachCi( p->pAigTotal, pObj, i )
        pObj->pData = Aig_ObjCreateCi( p->pAigFraig );
Alan Mishchenko committed
117 118 119 120 121
    // sweep internal nodes
    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
    Aig_ManForEachNode( p->pAigTotal, pObj, i )
    {
        Bar_ProgressUpdate( pProgress, i, NULL );
Alan Mishchenko committed
122 123 124
        if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL || 
             Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
            continue;
Alan Mishchenko committed
125 126 127 128 129 130
        pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
        if ( pObjNew == NULL )
            continue;
        Dch_ObjSetFraig( pObj, pObjNew );
        Dch_ManSweepNode( p, pObj );
    }
Alan Mishchenko committed
131
    Bar_ProgressStop( pProgress );
Alan Mishchenko committed
132
    // update the representatives of the nodes (makes classes invalid)
Alan Mishchenko committed
133
    ABC_FREE( p->pAigTotal->pReprs );
Alan Mishchenko committed
134 135 136 137 138 139 140 141 142 143 144
    p->pAigTotal->pReprs = p->pReprsProved;
    p->pReprsProved = NULL;
    // clean the mark
    Aig_ManCleanMarkB( p->pAigTotal );
}

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


145 146
ABC_NAMESPACE_IMPL_END