Version abc61122

1 files changed, 476 insertions, 0 deletions

diff --git a/src/aig/ivy/ivyObj.c b/src/aig/ivy/ivyObj.c
new file mode 100644
index 00000000..59dda19c
--- /dev/null
+++ b/src/aig/ivy/ivyObj.c
@@ -0,0 +1,476 @@
+/**CFile****************************************************************
+
+  FileName    [ivyObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Adding/removing objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreatePi( Ivy_Man_t * p )
+{
+    return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, NULL, NULL, IVY_PI, IVY_INIT_NONE) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver )
+{
+    return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pDriver, NULL, IVY_PO, IVY_INIT_NONE) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
+{
+    Ivy_Obj_t * pObj;
+    assert( !Ivy_IsComplement(pGhost) );
+    assert( Ivy_ObjIsGhost(pGhost) );
+    assert( Ivy_TableLookup(p, pGhost) == NULL );
+    // get memory for the new object
+    pObj = Ivy_ManFetchMemory( p );
+    assert( Ivy_ObjIsNone(pObj) );
+    pObj->Id = Vec_PtrSize(p->vObjs);
+    Vec_PtrPush( p->vObjs, pObj );
+    // add basic info (fanins, compls, type, init)
+    pObj->Type = pGhost->Type;
+    pObj->Init = pGhost->Init;
+    // add connections
+    Ivy_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
+    // compute level
+    if ( Ivy_ObjIsNode(pObj) )
+        pObj->Level = Ivy_ObjLevelNew(pObj);
+    else if ( Ivy_ObjIsLatch(pObj) )
+        pObj->Level = 0;
+    else if ( Ivy_ObjIsOneFanin(pObj) )
+        pObj->Level = Ivy_ObjFanin0(pObj)->Level;
+    else if ( !Ivy_ObjIsPi(pObj) )
+        assert( 0 );
+    // create phase
+    if ( Ivy_ObjIsNode(pObj) )
+        pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) & Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
+    else if ( Ivy_ObjIsOneFanin(pObj) )
+        pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
+    // set the fail TFO flag
+    if ( Ivy_ObjIsNode(pObj) )
+        pObj->fFailTfo = Ivy_ObjFanin0(pObj)->fFailTfo | Ivy_ObjFanin1(pObj)->fFailTfo;
+    // mark the fanins in a special way if the node is EXOR
+    if ( Ivy_ObjIsExor(pObj) )
+    {
+        Ivy_ObjFanin0(pObj)->fExFan = 1;
+        Ivy_ObjFanin1(pObj)->fExFan = 1;
+    }
+    // add PIs/POs to the arrays
+    if ( Ivy_ObjIsPi(pObj) )
+        Vec_PtrPush( p->vPis, pObj );
+    else if ( Ivy_ObjIsPo(pObj) )
+        Vec_PtrPush( p->vPos, pObj );
+//    else if ( Ivy_ObjIsBuf(pObj) )
+//        Vec_PtrPush( p->vBufs, pObj );
+    if ( p->vRequired && Vec_IntSize(p->vRequired) <= pObj->Id )
+        Vec_IntFillExtra( p->vRequired, 2 * Vec_IntSize(p->vRequired), 1000000 );
+    // update node counters of the manager
+    p->nObjs[Ivy_ObjType(pObj)]++;
+    p->nCreated++;
+
+//    printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " );
+//    Ivy_ObjPrintVerbose( p, pObj, p->pHaig==NULL );
+//    printf( "\n" );
+
+    // if HAIG is defined, create a corresponding node
+    if ( p->pHaig )
+        Ivy_ManHaigCreateObj( p, pObj );
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connect the object to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || pFan1 != NULL );
+    // add the first fanin
+    pObj->pFanin0 = pFan0;
+    pObj->pFanin1 = pFan1;
+    // increment references of the fanins and add their fanouts
+    if ( Ivy_ObjFanin0(pObj) != NULL )
+    {
+        Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
+        if ( p->fFanout )
+            Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
+    }
+    if ( Ivy_ObjFanin1(pObj) != NULL )
+    {
+        Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
+        if ( p->fFanout )
+            Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
+    }
+    // add the node to the structural hash table
+    Ivy_TableInsert( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connect the object to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL );
+    // remove connections
+    if ( pObj->pFanin0 != NULL )
+    {
+        Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
+        if ( p->fFanout )
+            Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj );
+    }
+    if ( pObj->pFanin1 != NULL )
+    {
+        Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
+        if ( p->fFanout )
+            Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj );
+    }
+    assert( pObj->pNextFan0 == NULL );
+    assert( pObj->pNextFan1 == NULL );
+    assert( pObj->pPrevFan0 == NULL );
+    assert( pObj->pPrevFan1 == NULL );
+    // remove the node from the structural hash table
+    Ivy_TableDelete( p, pObj );
+    // add the first fanin
+    pObj->pFanin0 = NULL;
+    pObj->pFanin1 = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the first fanin of the node by the new fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew )
+{
+    Ivy_Obj_t * pFaninOld;
+    assert( !Ivy_IsComplement(pObj) );
+    pFaninOld = Ivy_ObjFanin0(pObj);
+    // decrement ref and remove fanout
+    Ivy_ObjRefsDec( pFaninOld );
+    if ( p->fFanout )
+        Ivy_ObjDeleteFanout( p, pFaninOld, pObj );
+    // update the fanin
+    pObj->pFanin0 = pFaninNew;
+    // increment ref and add fanout
+    Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) );
+    if ( p->fFanout )
+        Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj );
+    // get rid of old fanin
+    if ( !Ivy_ObjIsPi(pFaninOld) && !Ivy_ObjIsConst1(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 )
+        Ivy_ObjDelete_rec( p, pFaninOld, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjRefs(pObj) == 0 || !fFreeTop );
+    // update node counters of the manager
+    p->nObjs[pObj->Type]--;
+    p->nDeleted++;
+    // remove connections
+    Ivy_ObjDisconnect( p, pObj );
+    // remove PIs/POs from the arrays
+    if ( Ivy_ObjIsPi(pObj) )
+        Vec_PtrRemove( p->vPis, pObj );
+    else if ( Ivy_ObjIsPo(pObj) )
+        Vec_PtrRemove( p->vPos, pObj );
+    else if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
+        Vec_PtrRemove( p->vBufs, pObj );
+    // clean and recycle the entry
+    if ( fFreeTop )
+    {
+        // free the node
+        Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+        Ivy_ManRecycleMemory( p, pObj );
+    }
+    else
+    {
+        int nRefsOld = pObj->nRefs;
+        Ivy_Obj_t * pFanout = pObj->pFanout;
+        Ivy_ObjClean( pObj );
+        pObj->pFanout = pFanout;
+        pObj->nRefs = nRefsOld;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
+{
+    Ivy_Obj_t * pFanin0, * pFanin1;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_ObjIsNone(pObj) );
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) )
+        return;
+    pFanin0 = Ivy_ObjFanin0(pObj);
+    pFanin1 = Ivy_ObjFanin1(pObj);
+    Ivy_ObjDelete( p, pObj, fFreeTop );
+    if ( pFanin0 && !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 )
+        Ivy_ObjDelete_rec( p, pFanin0, 1 );
+    if ( pFanin1 && !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 )
+        Ivy_ObjDelete_rec( p, pFanin1, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces one object by another.]
+
+  Description [Both objects are currently in the manager. The new object
+  (pObjNew) should be used instead of the old object (pObjOld). If the 
+  new object is complemented or used, the buffer is added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel )
+{
+    int nRefsOld;//, clk;
+    // the object to be replaced cannot be complemented
+    assert( !Ivy_IsComplement(pObjOld) );
+    // the object to be replaced cannot be a terminal
+    assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsPi(pObjOld) );
+    // the object to be used cannot be a PO or assert
+    assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) );
+    // the object cannot be the same
+    assert( pObjOld != Ivy_Regular(pObjNew) );
+//printf( "Replacing %d by %d.\n", Ivy_Regular(pObjOld)->Id, Ivy_Regular(pObjNew)->Id );
+
+    // if HAIG is defined, create the choice node
+    if ( p->pHaig )
+    {
+//        if ( pObjOld->Id == 31 )
+//        {
+//            Ivy_ManShow( p, 0 );
+//            Ivy_ManShow( p->pHaig, 1 );
+//        }
+        Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
+    }
+    // if the new object is complemented or already used, add the buffer
+    if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
+        pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
+    assert( !Ivy_IsComplement(pObjNew) );
+    if ( fUpdateLevel )
+    {
+//clk = clock();
+        // if the new node's arrival time is different, recursively update arrival time of the fanouts
+        if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+        {
+            assert( Ivy_ObjIsNode(pObjOld) );
+            pObjOld->Level = pObjNew->Level;
+            Ivy_ObjUpdateLevel_rec( p, pObjOld );
+        }
+//p->time1 += clock() - clk;
+        // if the new node's required time has changed, recursively update required time of the fanins
+//clk = clock();
+        if ( p->vRequired )
+        {
+            int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
+            if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
+            {
+                Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
+                Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
+            }
+        }
+//p->time2 += clock() - clk;
+    }
+    // delete the old object
+    if ( fDeleteOld )
+        Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
+    // make sure object is not pointing to itself
+    assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) );
+    assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) );
+    // make sure the old node has no fanin fanout pointers
+    if ( p->fFanout )
+    {
+        assert( pObjOld->pFanout != NULL );
+        assert( pObjNew->pFanout == NULL );
+        pObjNew->pFanout = pObjOld->pFanout;
+    }
+    // transfer the old object
+    assert( Ivy_ObjRefs(pObjNew) == 0 );
+    nRefsOld = pObjOld->nRefs;  
+    Ivy_ObjOverwrite( pObjOld, pObjNew );
+    pObjOld->nRefs = nRefsOld;
+    // patch the fanout of the fanins 
+    if ( p->fFanout )
+    {
+        Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld );
+        if ( Ivy_ObjFanin1(pObjOld) )
+        Ivy_ObjPatchFanout( p, Ivy_ObjFanin1(pObjOld), pObjNew, pObjOld );
+    }
+    // update the hash table
+    Ivy_TableUpdate( p, pObjNew, pObjOld->Id );
+    // recycle the object that was taken over by pObjOld
+    Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
+    Ivy_ManRecycleMemory( p, pObjNew );
+    // if the new node is the buffer propagate it
+    if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) )
+        Vec_PtrPush( p->vBufs, pObjOld );
+//    Ivy_ManCheckFanouts( p );
+//    printf( "\n" );
+/*
+    if ( p->pHaig )
+    {
+        int x;
+        Ivy_ManShow( p, 0, NULL );
+        Ivy_ManShow( p->pHaig, 1, NULL );
+        x = 0;
+    }
+*/
+//    if ( Ivy_ManCheckFanoutNums(p) )
+//    {
+//        int x = 0;
+//    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fixes buffer fanins.]
+
+  Description [This situation happens because NodeReplace is a lazy
+  procedure, which does not propagate the change to the fanouts but
+  instead records the change in the form of a buf/inv node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel )
+{
+    Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult;
+    if ( Ivy_ObjIsPo(pNode) )
+    {
+        if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) )
+            return;
+        pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
+        Ivy_ObjPatchFanin0( p, pNode, pFanReal0 );
+//        Ivy_ManCheckFanouts( p );
+        return;
+    }
+    if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
+        return;
+    // get the real fanins
+    pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
+    pFanReal1 = Ivy_ObjReal( Ivy_ObjChild1(pNode) );
+    // get the new node
+    if ( Ivy_ObjIsNode(pNode) )
+        pResult = Ivy_Oper( p, pFanReal0, pFanReal1, Ivy_ObjType(pNode) );
+    else if ( Ivy_ObjIsLatch(pNode) )
+        pResult = Ivy_Latch( p, pFanReal0, Ivy_ObjInit(pNode) );
+    else 
+        assert( 0 );
+
+//printf( "===== Replacing %d by %d.\n", pNode->Id, pResult->Id );
+//Ivy_ObjPrintVerbose( p, pNode, 0 );   printf( "\n" );
+//Ivy_ObjPrintVerbose( p, pResult, 0 ); printf( "\n" );
+
+    // perform the replacement
+    Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel ); 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+