Version abc80802

1 files changed, 306 insertions, 0 deletions

diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c
new file mode 100644
index 00000000..fe069fef
--- /dev/null
+++ b/src/aig/dch/dchChoice.c
@@ -0,0 +1,306 @@
+/**CFile****************************************************************
+
+  FileName    [dchChoice.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Contrustion of choices.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchChoice.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int i, nReprs = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pRepr = Aig_ObjRepr( pAig, pObj );
+        if ( pRepr == NULL )
+            continue;
+        assert( pRepr->Id < pObj->Id );
+        nReprs++;
+    }
+    return nReprs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pTemp;
+    int i, nEquivs = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( !Aig_ObjIsChoice(pAig, pObj) )
+            continue;
+        for ( pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; pTemp = Aig_ObjEquiv(pAig, pTemp) )
+        {
+            assert( pTemp->nRefs == 0 );
+            nEquivs++;
+        }
+    }
+    return nEquivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    // check the trivial cases
+    if ( pObj == NULL )
+        return 0;
+    if ( Aig_ObjIsPi(pObj) )
+        return 0;
+    if ( pObj->fMarkA )
+        return 1;
+    // skip the visited node
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    // check the children
+    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
+        return 1;
+    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
+        return 1;
+    // check equivalent nodes
+    return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pTemp;
+    int RetValue;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pRepr) );
+    // mark nodes of the choice node
+    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+        pTemp->fMarkA = 1;
+    // traverse the new node
+    Aig_ManIncrementTravId( p );
+    RetValue = Dch_ObjCheckTfi_rec( p, pObj );
+    // unmark nodes of the choice node
+    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+        pTemp->fMarkA = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_DeriveChoiceAig_rec( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+    if ( pObj->pData )
+        return;
+    // construct AIG for the representative
+    if ( (pRepr = Aig_ObjRepr(pAigOld, pObj)) )
+        Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, pRepr );
+    // construct AIG for the fanins
+    Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin0(pObj) );
+    Dch_DeriveChoiceAig_rec( pAigNew, pAigOld, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    if ( pRepr == NULL )
+        return;
+    // get the corresponding new nodes
+    pObjNew  = Aig_Regular(pObj->pData);
+    pReprNew = Aig_Regular(pRepr->pData);
+    if ( pObjNew == pReprNew )
+        return;
+    assert( pObjNew->nRefs == 0 );
+    // update new nodes of the object
+    pObj->pData = Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
+    if ( !Aig_ObjIsNode(pRepr) )
+        return;
+    // skip choices with combinational loops
+    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
+//    if ( Aig_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
+        return;
+    // add choice
+    pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
+    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns representatives of fanin in approapriate polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
+        return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
+    return pObj;
+}
+
+static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+    // get the new node
+    pObj->pData = Aig_And( pAigNew, 
+        Aig_ObjChild0CopyRepr(pAigNew, pObj), 
+        Aig_ObjChild1CopyRepr(pAigNew, pObj) );
+    pRepr = Aig_ObjRepr( pAigOld, pObj );
+    if ( pRepr == NULL )
+        return;
+    // get the corresponding new nodes
+    pObjNew  = Aig_Regular(pObj->pData);
+    pReprNew = Aig_Regular(pRepr->pData);
+    if ( pObjNew == pReprNew )
+        return;
+//    assert( pObjNew->nRefs == 0 );
+    // set the representatives
+    Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
+    // update new nodes of the object
+    if ( !Aig_ObjIsNode(pRepr) )
+        return;
+    if ( pObjNew->nRefs > 0 )
+        return;
+    // skip choices with combinational loops
+    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
+        return;
+    // add choice
+    pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id];
+    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pChoices, * pTemp;
+    Aig_Obj_t * pObj;
+    int i;
+    // start recording equivalences
+    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    pChoices->pReprs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    // map constants and PIs
+    Aig_ManCleanData( pAig );
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pChoices );
+    // construct choice nodes from the POs
+    assert( pAig->pReprs != NULL );
+/*
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) );
+        Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) );
+    }
+*/
+    Aig_ManForEachNode( pAig, pObj, i )
+        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
+    Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
+    Dch_DeriveChoiceCountEquivs( pChoices );
+    // there is no need for cleanup
+    FREE( pChoices->pReprs );
+    pChoices = Aig_ManDupDfs( pTemp = pChoices );
+    Aig_ManStop( pTemp );
+    return pChoices;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+