Version abc70930

1 files changed, 0 insertions, 273 deletions

diff --git a/src/aig/ivy/ivyCheck.c b/src/aig/ivy/ivyCheck.c
deleted file mode 100644
index 55448f19..00000000
--- a/src/aig/ivy/ivyCheck.c
+++ /dev/null
@@ -1,273 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivyCheck.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [AIG checking procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the consistency of the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManCheck( Ivy_Man_t * p )
-{
-    Ivy_Obj_t * pObj, * pObj2;
-    int i;
-    Ivy_ManForEachObj( p, pObj, i )
-    {
-        // skip deleted nodes
-        if ( Ivy_ObjId(pObj) != i )
-        {
-            printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
-            return 0;
-        }
-        // consider the constant node and PIs
-        if ( i == 0 || Ivy_ObjIsPi(pObj) )
-        {
-            if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) )
-            {
-                printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id );
-                return 0;
-            }
-            continue;
-        }
-        if ( Ivy_ObjIsPo(pObj) )
-        {
-            if ( Ivy_ObjFaninId1(pObj) )
-            {
-                printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id );
-                return 0;
-            }
-            continue;
-        }
-        if ( Ivy_ObjIsBuf(pObj) )
-        {
-            if ( Ivy_ObjFanin1(pObj) )
-            {
-                printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
-                return 0;
-            }
-            continue;
-        }
-        if ( Ivy_ObjIsLatch(pObj) )
-        {
-            if ( Ivy_ObjFanin1(pObj) )
-            {
-                printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
-                return 0;
-            }
-            if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
-            {
-                printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
-                return 0;
-            }
-            pObj2 = Ivy_TableLookup( p, pObj );
-            if ( pObj2 != pObj )
-                printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
-                continue;
-        }
-        // consider the AND node
-        if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
-        {
-            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
-            return 0;
-        }
-        if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
-        {
-            printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
-            return 0;
-        }
-        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
-            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
-        pObj2 = Ivy_TableLookup( p, pObj );
-        if ( pObj2 != pObj )
-            printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
-        if ( Ivy_ObjRefs(pObj) == 0 )
-            printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
-        // check fanouts
-        if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
-            printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
-    }
-    // count the number of nodes in the table
-    if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
-    {
-        printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
-        return 0;
-    }
-//    if ( !Ivy_ManCheckFanouts(p) )
-//        return 0;
-    if ( !Ivy_ManIsAcyclic(p) )
-        return 0;
-    return 1; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies the fanouts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManCheckFanoutNums( Ivy_Man_t * p )
-{
-    Ivy_Obj_t * pObj;
-    int i, Counter = 0;
-    Ivy_ManForEachObj( p, pObj, i )
-        if ( Ivy_ObjIsNode(pObj) )
-            Counter += (Ivy_ObjRefs(pObj) == 0);
-    if ( Counter )
-        printf( "Sequential AIG has %d dangling nodes.\n", Counter );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies the fanouts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManCheckFanouts( Ivy_Man_t * p )
-{
-    Vec_Ptr_t * vFanouts;
-    Ivy_Obj_t * pObj, * pFanout, * pFanin;
-    int i, k, RetValue = 1;
-    if ( !p->fFanout )
-        return 1;
-    vFanouts = Vec_PtrAlloc( 100 );
-    // make sure every fanin is a fanout
-    Ivy_ManForEachObj( p, pObj, i )
-    {
-        pFanin = Ivy_ObjFanin0(pObj);
-        if ( pFanin == NULL )
-            continue;
-        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
-            if ( pFanout == pObj )
-                break;
-        if ( k == Vec_PtrSize(vFanouts) )
-        {
-            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
-            RetValue = 0;
-        }
-
-        pFanin = Ivy_ObjFanin1(pObj);
-        if ( pFanin == NULL )
-            continue;
-        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
-            if ( pFanout == pObj )
-                break;
-        if ( k == Vec_PtrSize(vFanouts) )
-        {
-            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
-            RetValue = 0;
-        }
-        // check that the previous fanout has the same fanin
-        if ( pObj->pPrevFan0 )
-        {
-            if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
-                 Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && 
-                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
-                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
-            {
-                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
-                RetValue = 0;
-            }
-        }
-        // check that the previous fanout has the same fanin
-        if ( pObj->pPrevFan1 )
-        {
-            if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
-                 Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && 
-                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
-                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
-            {
-                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
-                RetValue = 0;
-            }
-        }
-    }
-    // make sure every fanout is a fanin
-    Ivy_ManForEachObj( p, pObj, i )
-    {
-        Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
-            if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
-            {
-                printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
-                RetValue = 0;
-            }
-    }
-    Vec_PtrFree( vFanouts );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks that each choice node has exactly one node with fanouts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManCheckChoices( Ivy_Man_t * p )
-{
-    Ivy_Obj_t * pObj, * pTemp;
-    int i;
-    Ivy_ManForEachObj( p->pHaig, pObj, i )
-    {
-        if ( Ivy_ObjRefs(pObj) == 0 )
-            continue;
-        // count the number of nodes in the loop
-        assert( !Ivy_IsComplement(pObj->pEquiv) );
-        for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
-            if ( Ivy_ObjRefs(pTemp) > 1 )
-                printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
-    }
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-