Version abc61122

1 files changed, 408 insertions, 0 deletions

diff --git a/src/aig/ivy/ivyRwrAlg.c b/src/aig/ivy/ivyRwrAlg.c
new file mode 100644
index 00000000..fc48deb0
--- /dev/null
+++ b/src/aig/ivy/ivyRwrAlg.c
@@ -0,0 +1,408 @@
+/**CFile****************************************************************
+
+  FileName    [ivyRwrAlg.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Algebraic AIG rewriting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyRwrAlg.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
+static Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost );
+static int Ivy_NodeCountMffc( Ivy_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Algebraic AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
+{
+    Vec_Int_t * vRequired;
+    Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol;
+    Ivy_Obj_t * pObj, * pResult;
+    int i, RetValue, LevelR, nNodesOld;
+    int CountUsed, CountUndo;
+    vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL;
+    vFront    = Vec_PtrAlloc( 100 );
+    vLeaves   = Vec_PtrAlloc( 100 );
+    vCone     = Vec_PtrAlloc( 100 );
+    vSol      = Vec_PtrAlloc( 100 );
+    // go through the nodes in the topological order
+    CountUsed = CountUndo = 0;
+    nNodesOld = Ivy_ManObjIdNext(p);
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        assert( !Ivy_ObjIsBuf(pObj) );
+        if ( i >= nNodesOld )
+            break;
+        // skip no-nodes and MUX roots
+        if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) )
+            continue;
+//        if ( pObj->Id > 297 ) // 296 --- 297 
+//            break;
+        if ( pObj->Id == 297 )
+        {
+            int x = 0;
+        }
+        // get the largest algebraic cut
+        RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone );
+        // the case of a trivial tree cut
+        if ( RetValue == 1 )
+            continue;
+        // the case of constant 0 cone
+        if ( RetValue == -1 )
+        {
+            Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 ); 
+            continue;
+        }
+        assert( Vec_PtrSize(vLeaves) > 2 );
+        // get the required level for this node
+        LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000;
+        // create a new cone
+        pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost );
+        if ( pResult == NULL || pResult == pObj )
+            continue;
+        assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) );
+        if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
+            Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
+        else
+            Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++; 
+    }
+    printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
+    Vec_PtrFree( vFront );
+    Vec_PtrFree( vCone );
+    Vec_PtrFree( vSol );
+    if ( vRequired ) Vec_IntFree( vRequired );
+    if ( i = Ivy_ManCleanup(p) )
+        printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
+    if ( !Ivy_ManCheck(p) )
+        printf( "Ivy_ManRewriteAlg(): The check has failed.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Analizes one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost )
+{
+    int fVerbose = 0;
+    Ivy_Obj_t * pTemp;
+    int k, Counter, nMffc, RetValue;
+
+    if ( fVerbose )
+    {
+        if ( Ivy_ObjIsExor(pObj) )
+            printf( "x " );
+        else
+            printf( "  " );
+    }
+
+/*       
+    printf( "%d ", Vec_PtrSize(vFront) );
+    printf( "( " );
+    Vec_PtrForEachEntry( vFront, pTemp, k )
+        printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+    printf( ")\n" );
+*/
+    // collect nodes in the cone
+    if ( Ivy_ObjIsExor(pObj) )
+        Ivy_ManCollectCone( pObj, vFront, vCone );
+    else
+        Ivy_ManCollectCone( pObj, vLeaves, vCone );
+
+    // deref nodes in the cone
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+    {
+        Ivy_ObjRefsDec( Ivy_ObjFanin0(pTemp) );
+        Ivy_ObjRefsDec( Ivy_ObjFanin1(pTemp) );
+        pTemp->fMarkB = 1;
+    }
+
+    // count the MFFC size
+    Vec_PtrForEachEntry( vFront, pTemp, k )
+        Ivy_Regular(pTemp)->fMarkA = 1;
+    nMffc = Ivy_NodeCountMffc( pObj );
+    Vec_PtrForEachEntry( vFront, pTemp, k )
+        Ivy_Regular(pTemp)->fMarkA = 0;
+
+    if ( fVerbose )
+    {
+    Counter = 0;
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+        Counter += (Ivy_ObjRefs(pTemp) > 0);
+    printf( "%5d : Leaves = %2d. Cone = %2d. ConeRef = %2d.   Mffc = %d.   Lev = %d.  LevR = %d.\n", 
+        pObj->Id, Vec_PtrSize(vFront), Vec_PtrSize(vCone), Counter-1, nMffc, Ivy_ObjLevel(pObj), LevelR );
+    }
+/*
+    printf( "Leaves:" );
+    Vec_PtrForEachEntry( vLeaves, pTemp, k )
+        printf( " %d%s", Ivy_Regular(pTemp)->Id, Ivy_IsComplement(pTemp)? "\'" : "" );
+    printf( "\n" );
+    printf( "Cone:\n" );
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+        printf( " %5d = %d%s %d%s\n", pTemp->Id,
+            Ivy_ObjFaninId0(pTemp), Ivy_ObjFaninC0(pTemp)? "\'" : "",
+            Ivy_ObjFaninId1(pTemp), Ivy_ObjFaninC1(pTemp)? "\'" : "" );
+*/
+
+    RetValue = Ivy_MultiPlus( vLeaves, vCone, Ivy_ObjType(pObj), nMffc + fUseZeroCost, vSols );
+
+    // ref nodes in the cone
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+    {
+        Ivy_ObjRefsInc( Ivy_ObjFanin0(pTemp) );
+        Ivy_ObjRefsInc( Ivy_ObjFanin1(pTemp) );
+        pTemp->fMarkA = 0;
+        pTemp->fMarkB = 0;
+    }
+
+    if ( !RetValue )
+        return NULL;
+
+    if ( Vec_PtrSize( vSols ) == 1 )
+        return Vec_PtrEntry( vSols, 0 );
+    return Ivy_NodeBalanceBuildSuper( vSols, Ivy_ObjType(pObj), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCountMffc_rec( Ivy_Obj_t * pNode )
+{
+    if ( Ivy_ObjRefs(pNode) > 0 || Ivy_ObjIsCi(pNode) || pNode->fMarkA )
+        return 0;
+    assert( pNode->fMarkB );
+    pNode->fMarkA = 1;
+//    printf( "%d ", pNode->Id );
+    if ( Ivy_ObjIsBuf(pNode) )
+        return Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) );
+    return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCountMffc( Ivy_Obj_t * pNode )
+{
+    assert( pNode->fMarkB );
+    return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing one algebraic cut.]
+
+  Description [Returns 1 if the tree-leaves of this node where traversed 
+  and found to have no external references (and have not been collected). 
+  Returns 0 if the tree-leaves have external references and are collected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pObj, Ivy_Type_t Type, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
+{
+    int RetValue0, RetValue1;
+    Ivy_Obj_t * pObjR = Ivy_Regular(pObj);
+    assert( !Ivy_ObjIsBuf(pObjR) );
+    assert( Type != IVY_EXOR || !Ivy_IsComplement(pObj) );
+
+    // make sure the node is not visited twice in different polarities
+    if ( Ivy_IsComplement(pObj) )
+    { // if complemented, mark B
+        if ( pObjR->fMarkA )
+            return -1;
+        pObjR->fMarkB = 1;
+    }
+    else
+    { // if non-complicated, mark A
+        if ( pObjR->fMarkB )
+            return -1;
+        pObjR->fMarkA = 1;
+    }
+    Vec_PtrPush( vCone, pObjR );
+
+    // if the node is the end of the tree, return
+    if ( Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Type )
+    {
+        if ( Ivy_ObjRefs(pObjR) == 1 )
+            return 1;
+        assert( Ivy_ObjRefs(pObjR) > 1 );
+        Vec_PtrPush( vFront, pObj );
+        return 0;
+    }
+
+    // branch on the node
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    // what if buffer has more than one fanout???
+    RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild0(pObj) ), Type, vFront, vCone );
+    RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild1(pObj) ), Type, vFront, vCone );
+    if ( RetValue0 == -1 || RetValue1 == -1 )
+        return -1;
+
+    // the case when both have no external references
+    if ( RetValue0 && RetValue1 )
+    {
+        if ( Ivy_ObjRefs(pObj) == 1 )
+            return 1;
+        assert( Ivy_ObjRefs(pObj) > 1 );
+        Vec_PtrPush( vFront, pObj );
+        return 0;
+    }
+    // the case when one of them has external references
+    if ( RetValue0 )
+        Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild0(pObj) ) );
+    if ( RetValue1 )
+        Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild1(pObj) ) );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing one algebraic cut.]
+
+  Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
+  (c) boundary of different gates. Returns 1 if this is a pure tree.
+  Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+{
+    Ivy_Obj_t * pObj, * pPrev;
+    int RetValue, i;
+    assert( !Ivy_IsComplement(pRoot) );
+    assert( Ivy_ObjIsNode(pRoot) );
+    // clear the frontier and collect the nodes
+    Vec_PtrClear( vCone );
+    Vec_PtrClear( vFront );
+    Vec_PtrClear( vLeaves );
+    RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront, vCone );
+    // clean the marks
+    Vec_PtrForEachEntry( vCone, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = 0;
+    // quit if the same node is found in both polarities
+    if ( RetValue == -1 )
+        return -1;
+    // return if the node is the root of a tree
+    if ( RetValue == 1 )
+        return 1;
+    // return if the cut is composed of two nodes
+    if ( Vec_PtrSize(vFront) <= 2 )
+        return 1;
+    // sort the entries in increasing order
+    Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
+    // remove duplicates from vFront and save the nodes in vLeaves
+    pPrev = Vec_PtrEntry(vFront, 0);
+    Vec_PtrPush( vLeaves, pPrev );
+    Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
+    {
+        // compare current entry and the previous entry
+        if ( pObj == pPrev )
+        {
+            if ( Ivy_ObjIsExor(pRoot) ) // A <+> A = 0
+            {
+                // vLeaves are no longer structural support of pRoot!!!
+                Vec_PtrPop(vLeaves);  
+                pPrev = Vec_PtrSize(vLeaves) == 0 ? NULL : Vec_PtrEntryLast(vLeaves);
+            }
+            continue;
+        }
+        if ( pObj == Ivy_Not(pPrev) )
+        {
+            assert( Ivy_ObjIsAnd(pRoot) );
+            return -1;
+        }
+        pPrev = pObj;
+        Vec_PtrPush( vLeaves, pObj );
+    }
+    if ( Vec_PtrSize(vLeaves) == 0 )
+        return -1;
+    if ( Vec_PtrSize(vLeaves) <= 2 )
+        return 1;
+    return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+