Version abc90215

1 files changed, 248 insertions, 0 deletions

diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
new file mode 100644
index 00000000..ee9e5b5f
--- /dev/null
+++ b/src/aig/gia/giaFront.c
@@ -0,0 +1,248 @@
+/**CFile****************************************************************
+
+  FileName    [giaFront.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Frontier representation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaFront.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find the next place on the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManFrontFindNext( char * pFront, int nFront, int iFront )
+{
+    assert( iFront < nFront );
+    for ( ; pFront[iFront]; iFront = (iFront + 1) % nFront );
+    assert( pFront[iFront] == 0 );
+    pFront[iFront] = 1;
+    return iFront;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the frontier manager to its initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManFrontTransform( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, * pFrontToId; // mapping of nodes into frontier variables
+    assert( p->nFront > 0 );
+    pFrontToId = ABC_ALLOC( int, p->nFront );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsCo(pObj) )
+        {
+            assert( pObj->Value == GIA_NONE );
+            pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
+        }
+        else if ( Gia_ObjIsAnd(pObj) )
+        {
+            assert( (int)pObj->Value < p->nFront );
+            pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
+            pObj->iDiff1 = i - pFrontToId[Gia_ObjDiff1(pObj)];
+            pFrontToId[pObj->Value] = i;
+        }
+        else
+        {
+            assert( (int)pObj->Value < p->nFront );
+            pFrontToId[pObj->Value] = i;
+        }
+        pObj->Value = 0;
+    }
+    ABC_FREE( pFrontToId );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
+    char * pFront;    // places used for the frontier
+    int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
+    int nCrossCutMaxInit = Gia_ManCrossCut( p );
+    int iFront = 0, clk = clock(); 
+    // set references for all objects
+    Gia_ManSetRefs( p );
+    // start the new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit); 
+    // start the frontier
+    pFront = ABC_CALLOC( char, pNew->nFront );
+    // add constant node
+    Gia_ManConst0(pNew)->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
+    if ( Gia_ObjValue(Gia_ManConst0(p)) == 0 )
+        pFront[iFront] = 0;
+    else
+        nCrossCut = 1;
+    // iterate through the objects
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) )
+        {
+            if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
+                nCrossCutMax = nCrossCut;
+            // create new node
+            iLit = Gia_ManAppendCi( pNew );
+            pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) );
+            assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
+            pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
+            // handle CIs without fanout
+            if ( Gia_ObjValue(pObj) == 0 )
+                pFront[iFront] = 0;
+            continue;
+        }
+        if ( Gia_ObjIsCo(pObj) )
+        {
+            assert( Gia_ObjValue(pObj) == 0 );
+            // create new node
+            iLit = Gia_ManAppendCo( pNew, 0 );
+            pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) );
+            assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
+            // get the fanin
+            pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
+            assert( pFanin0New->Value != GIA_NONE );
+            pObjNew->Value = GIA_NONE;
+            pObjNew->iDiff0 = pFanin0New->Value;
+            pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
+            // deref the fanin
+            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
+            {
+                pFront[pFanin0New->Value] = 0;
+                nCrossCut--;
+            }
+            continue;
+        }
+        if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
+            nCrossCutMax = nCrossCut;
+        // create new node
+        pObjNew = Gia_ManAppendObj( pNew );
+        assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
+        // assign the first fanin
+        pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
+        assert( pFanin0New->Value != GIA_NONE );
+        pObjNew->iDiff0 = pFanin0New->Value;
+        pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
+        // assign the second fanin
+        pFanin1New = Gia_ManObj( pNew, Gia_ObjFaninId1(pObj, i) );
+        assert( pFanin1New->Value != GIA_NONE );
+        pObjNew->iDiff1 = pFanin1New->Value;
+        pObjNew->fCompl1 = Gia_ObjFaninC1(pObj);
+        // assign the frontier number
+        pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
+        // deref the fanins
+        if ( --Gia_ObjFanin0(pObj)->Value == 0 )
+        {
+            pFront[pFanin0New->Value] = 0;
+            nCrossCut--;
+        }
+        if ( --Gia_ObjFanin1(pObj)->Value == 0 )
+        {
+            pFront[pFanin1New->Value] = 0;
+            nCrossCut--;
+        }
+        // handle nodes without fanout (choice nodes)
+        if ( Gia_ObjValue(pObj) == 0 )
+            pFront[iFront] = 0;
+    }
+    assert( pNew->nObjs == p->nObjs );
+    assert( nCrossCut == 0 && nCrossCutMax == nCrossCutMaxInit );
+    for ( i = 0; i < pNew->nFront; i++ )
+        assert( pFront[i] == 0 );
+    ABC_FREE( pFront );
+//printf( "Crosscut = %6d. Frontier = %6d. ", nCrossCutMaxInit, pNew->nFront );
+//ABC_PRT( "Time", clock() - clk );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManFrontTest( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    pNew  = Gia_ManFront( p );
+    Gia_ManFrontTransform( pNew );
+//    Gia_ManCleanValue( p );
+//    Gia_ManCleanValue( pNew );
+    if ( memcmp( pNew->pObjs, p->pObjs, sizeof(Gia_Obj_t) * p->nObjs ) )
+    {
+/*
+        Gia_Obj_t * pObj, * pObjNew;
+        int i;
+        Gia_ManForEachObj( p, pObj, i )
+        {
+            pObjNew = Gia_ManObj( pNew, i );
+            printf( "%5d %5d   %5d %5d\n", 
+                pObj->iDiff0, pObjNew->iDiff0, 
+                pObj->iDiff1, pObjNew->iDiff1 );
+        }
+*/
+        printf( "Verification failed.\n" );
+    }
+    else
+        printf( "Verification successful.\n" );
+    Gia_ManStop( pNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+