Better resolution of CO drivers. Should impact the QoR after 'if'.

6 files changed, 266 insertions, 36 deletions

diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index eff904fd..6411265f 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -282,6 +282,7 @@ extern int             Hop_DagSize( Hop_Obj_t * pObj );
 extern void            Hop_ConeUnmark_rec( Hop_Obj_t * pObj );
 extern Hop_Obj_t *     Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars );
 extern Hop_Obj_t *     Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar );
+extern Hop_Obj_t *     Hop_Complement( Hop_Man_t * p, Hop_Obj_t * pRoot, int iVar );
 extern Hop_Obj_t *     Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars );
 /*=== hopMan.c ==========================================================*/
 extern Hop_Man_t *     Hop_ManStart();
diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c
index f6f8c507..e8ca970f 100644
--- a/src/aig/hop/hopDfs.c
+++ b/src/aig/hop/hopDfs.c
@@ -397,6 +397,60 @@ Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, in
 
 /**Function*************************************************************
 
+  Synopsis    [Complements the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Hop_Complement_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pVar )
+{
+    assert( !Hop_IsComplement(pObj) );
+    if ( Hop_ObjIsMarkA(pObj) )
+        return;
+    if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
+    {
+        pObj->pData = pObj == pVar ? Hop_Not(pObj) : pObj;
+        return;
+    }
+    Hop_Complement_rec( p, Hop_ObjFanin0(pObj), pVar ); 
+    Hop_Complement_rec( p, Hop_ObjFanin1(pObj), pVar );
+    pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Complements the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Hop_Complement( Hop_Man_t * p, Hop_Obj_t * pRoot, int iVar )
+{
+    // quit if the PI variable is not defined
+    if ( iVar >= Hop_ManPiNum(p) )
+    {
+        printf( "Hop_Complement(): The PI variable %d is not defined.\n", iVar );
+        return NULL;
+    }
+    // recursively perform composition
+    Hop_Complement_rec( p, Hop_Regular(pRoot), Hop_ManPi(p, iVar) );
+    // clear the markings
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+    return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Remaps the AIG (pRoot) to have the given support (uSupp).]
 
   Description []
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bc6f1bc3..56f1df85 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -746,6 +746,7 @@ extern ABC_DLL int                Abc_NodeIsConst1( Abc_Obj_t * pNode );
 extern ABC_DLL int                Abc_NodeIsBuf( Abc_Obj_t * pNode );    
 extern ABC_DLL int                Abc_NodeIsInv( Abc_Obj_t * pNode );    
 extern ABC_DLL void               Abc_NodeComplement( Abc_Obj_t * pNode );
+extern ABC_DLL void               Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin );
 /*=== abcOdc.c ==========================================================*/
 typedef struct Odc_Man_t_         Odc_Man_t;
 extern ABC_DLL Odc_Man_t *        Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 7741d963..901ffa31 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -952,14 +952,55 @@ void Abc_NodeComplement( Abc_Obj_t * pNode )
     assert( Abc_ObjIsNode(pNode) ); 
     if ( Abc_NtkHasSop(pNode->pNtk) )
         Abc_SopComplement( (char *)pNode->pData );
+    else if ( Abc_NtkHasAig(pNode->pNtk) )
+        pNode->pData = Hop_Not( (Hop_Obj_t *)pNode->pData );
     else if ( Abc_NtkHasBdd(pNode->pNtk) )
         pNode->pData = Cudd_Not( pNode->pData );
+    else
+        assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Changes the polarity of one fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
+{
+    int iFanin;
+    if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 )
+    {
+        printf( "Node %s should be among", Abc_ObjName(pFanin) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
+        return;
+    }
+    if ( Abc_NtkHasSop(pNode->pNtk) )
+        Abc_SopComplementVar( (char *)pNode->pData, iFanin );
     else if ( Abc_NtkHasAig(pNode->pNtk) )
-        pNode->pData = Hop_Not( (Hop_Obj_t *)pNode->pData );
+        pNode->pData = Hop_Complement( (Hop_Man_t *)pNode->pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, iFanin );
+    else if ( Abc_NtkHasBdd(pNode->pNtk) )
+    {
+        DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
+        DdNode * bVar, * bCof0, * bCof1;
+        bVar = Cudd_bddIthVar( dd, iFanin );
+        bCof0 = Cudd_Cofactor( dd, (DdNode *)pNode->pData, Cudd_Not(bVar) );   Cudd_Ref( bCof0 );
+        bCof1 = Cudd_Cofactor( dd, (DdNode *)pNode->pData, bVar );             Cudd_Ref( bCof1 );
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
+        pNode->pData = Cudd_bddIte( dd, bVar, bCof0, bCof1 );        Cudd_Ref( (DdNode *)pNode->pData );
+        Cudd_RecursiveDeref( dd, bCof0 );
+        Cudd_RecursiveDeref( dd, bCof1 );
+    }
     else
         assert( 0 );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 9d27158d..286624be 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -943,7 +943,7 @@ int Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, int fDuplicate )
+int Abc_NtkLogicMakeSimpleCos2( Abc_Ntk_t * pNtk, int fDuplicate )
 {
     Abc_Obj_t * pNode, * pDriver;
     int i, nDupGates = 0;
@@ -985,6 +985,173 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, int fDuplicate )
     return nDupGates;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the network to have simple COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, int fDuplicate )
+{
+    Vec_Ptr_t * vDrivers, * vCoTerms;
+    Abc_Obj_t * pNode, * pDriver, * pDriverNew, * pFanin;
+    int i, k, LevelMax, nTotal = 0;
+    assert( Abc_NtkIsLogic(pNtk) );
+    LevelMax = Abc_NtkLevel(pNtk);
+
+    // collect drivers pointed by complemented edges
+    vDrivers = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCo( pNtk, pNode, i ) 
+    {
+        if ( !Abc_ObjFaninC0(pNode) )
+            continue;
+        pDriver = Abc_ObjFanin0(pNode);
+        if ( Abc_NodeIsTravIdCurrent(pDriver) )
+            continue;
+        Abc_NodeSetTravIdCurrent(pDriver);
+        Vec_PtrPush( vDrivers, pDriver );
+    }
+    // fix complemented drivers
+    if ( Vec_PtrSize(vDrivers) > 0 )
+    {
+        int nDupGates = 0, nDupInvs = 0, nDupChange = 0;
+        Vec_Ptr_t * vFanouts = Vec_PtrAlloc( 100 );
+        Vec_PtrForEachEntry( Abc_Obj_t *, vDrivers, pDriver, i )
+        {
+            int fHasDir = 0, fHasInv = 0, fHasOther = 0;
+            Abc_ObjForEachFanout( pDriver, pNode, k )
+            {
+                if ( !Abc_ObjIsCo(pNode) )
+                {
+                    assert( !Abc_ObjFaninC0(pNode) );
+                    fHasOther = 1;
+                    continue;
+                }
+                if ( Abc_ObjFaninC0(pNode) )
+                    fHasInv = 1;
+                else //if ( Abc_ObjFaninC0(pNode) )
+                    fHasDir = 1;
+            }
+            assert( fHasInv );
+            if ( Abc_ObjIsCi(pDriver) || fHasDir || (fHasOther && Abc_NtkHasMapping(pNtk)) ) // cannot change
+            {
+                // duplicate if critical
+                if ( fDuplicate && Abc_ObjIsNode(pDriver) && Abc_ObjLevel(pDriver) == LevelMax )
+                {
+                    pDriverNew = Abc_NtkDupObj( pNtk, pDriver, 0 ); 
+                    Abc_ObjForEachFanin( pDriver, pFanin, k )
+                        Abc_ObjAddFanin( pDriverNew, pFanin );
+                    Abc_NodeComplement( pDriverNew );
+                    nDupGates++;
+                }
+                else // add inverter
+                {
+                    pDriverNew = Abc_NtkCreateNodeInv( pNtk, pDriver );
+                    nDupInvs++;
+                }
+                // collect CO fanouts to be redirected to the new node
+                Vec_PtrClear( vFanouts );
+                Abc_ObjForEachFanout( pDriver, pNode, k )
+                    if ( Abc_ObjIsCo(pNode) && Abc_ObjFaninC0(pNode) )
+                        Vec_PtrPush( vFanouts, pNode );
+                assert( Vec_PtrSize(vFanouts) > 0 );
+                Vec_PtrForEachEntry( Abc_Obj_t *, vFanouts, pNode, k )
+                {
+                    Abc_ObjXorFaninC( pNode, 0 );
+                    Abc_ObjPatchFanin( pNode, pDriver, pDriverNew );
+                    assert( Abc_ObjIsCi(pDriver) || Abc_ObjFanoutNum(pDriver) > 0 );
+                }
+            }
+            else // can change
+            {
+                // change polarity of the driver
+                assert( Abc_ObjIsNode(pDriver) );
+                Abc_NodeComplement( pDriver );
+                Abc_ObjForEachFanout( pDriver, pNode, k )
+                {
+                    if ( Abc_ObjIsCo(pNode) )
+                    {
+                        assert( Abc_ObjFaninC0(pNode) );
+                        Abc_ObjXorFaninC( pNode, 0 );
+                    }
+                    else if ( Abc_ObjIsNode(pNode) )
+                        Abc_NodeComplementInput( pNode, pDriver );
+                    else assert( 0 );
+                }
+                nDupChange++;
+            }
+        }
+        Vec_PtrFree( vFanouts );
+//        printf( "Resolving inverted CO drivers: Invs = %d. Dups = %d. Changes = %d.\n",
+//            nDupInvs, nDupGates, nDupChange );
+        nTotal += nDupInvs + nDupGates;
+    }
+    Vec_PtrFree( vDrivers );
+
+    // collect COs that needs fixing by adding buffers or duplicating
+    vCoTerms = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        // if the driver is a CI and has different name, this is an error
+        pDriver = Abc_ObjFanin0(pNode);
+        if ( Abc_ObjIsCi(pDriver) && strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) )
+        {
+            Vec_PtrPush( vCoTerms, pNode );
+            continue;
+        }
+        // if the driver is visited for the first time, remember the CO name
+        if ( !Abc_NodeIsTravIdCurrent(pDriver) )
+        {
+            pDriver->pNext = (Abc_Obj_t *)Abc_ObjName(pNode);
+            Abc_NodeSetTravIdCurrent(pDriver);
+            continue;
+        }
+        // the driver has second CO - if they have different name, this is an error
+        if ( strcmp((char *)pDriver->pNext, Abc_ObjName(pNode)) ) // diff names
+        {
+            Vec_PtrPush( vCoTerms, pNode );
+            continue;
+        }
+    }
+    // fix duplication problem
+    if ( Vec_PtrSize(vCoTerms) > 0 )
+    {
+        int nDupBufs = 0, nDupGates = 0;
+        Vec_PtrForEachEntry( Abc_Obj_t *, vCoTerms, pNode, i )
+        {
+            pDriver = Abc_ObjFanin0(pNode);
+            // duplicate if critical
+            if ( fDuplicate && Abc_ObjIsNode(pDriver) && Abc_ObjLevel(pDriver) == LevelMax )
+            {
+                pDriverNew = Abc_NtkDupObj( pNtk, pDriver, 0 ); 
+                Abc_ObjForEachFanin( pDriver, pFanin, k )
+                    Abc_ObjAddFanin( pDriverNew, pFanin );
+                nDupGates++;
+            }
+            else // add buffer
+            {
+                pDriverNew = Abc_NtkCreateNodeBuf( pNtk, pDriver );
+                nDupBufs++;
+            }
+            // swing the PO
+            Abc_ObjPatchFanin( pNode, pDriver, pDriverNew );
+            assert( Abc_ObjIsCi(pDriver) || Abc_ObjFanoutNum(pDriver) > 0 );
+        }
+//        printf( "Resolving shared CO drivers: Bufs = %d. Dups = %d.\n", nDupBufs, nDupGates );
+        nTotal += nDupBufs + nDupGates;
+    }
+    Vec_PtrFree( vCoTerms );
+    return nTotal;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Inserts a new node in the order by levels.]
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 2670939b..453dd9ba 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -39,7 +39,6 @@ static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 static int            Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
 static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
 static void           Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, int fConst0 );
-static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -684,39 +683,6 @@ void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, int fConst0 )
     Cudd_RecursiveDeref( dd, bTemp );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Changes the polarity of one fanin.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
-{
-    DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
-    DdNode * bVar, * bCof0, * bCof1;
-    int iFanin;
-    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
-    if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 )
-    {
-        printf( "Node %s should be among", Abc_ObjName(pFanin) );
-        printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
-        return;
-    }
-    bVar = Cudd_bddIthVar( dd, iFanin );
-    bCof0 = Cudd_Cofactor( dd, (DdNode *)pNode->pData, Cudd_Not(bVar) );   Cudd_Ref( bCof0 );
-    bCof1 = Cudd_Cofactor( dd, (DdNode *)pNode->pData, bVar );             Cudd_Ref( bCof1 );
-    Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
-    pNode->pData = Cudd_bddIte( dd, bVar, bCof0, bCof1 );        Cudd_Ref( (DdNode *)pNode->pData );
-    Cudd_RecursiveDeref( dd, bCof0 );
-    Cudd_RecursiveDeref( dd, bCof1 );
-}
-
-
 
 /**Function*************************************************************