/**CFile****************************************************************

  FileName    [abcCheck.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Consistency checking procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: abcCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "abc.h"
#include "base/main/main.h"
#include "misc/extra/extraBdd.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

static int Abc_NtkCheckNames( Abc_Ntk_t * pNtk );
static int Abc_NtkCheckPis( Abc_Ntk_t * pNtk );
static int Abc_NtkCheckPos( Abc_Ntk_t * pNtk );
//static int Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
static int Abc_NtkCheckNet( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
static int Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
static int Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch );

static int Abc_NtkComparePis( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
static int Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
static int Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );

static inline char * Abc_ObjNameNet( Abc_Obj_t * pObj ) { return (Abc_ObjIsNode(pObj) && Abc_NtkIsNetlist(pObj->pNtk)) ? Abc_ObjName(Abc_ObjFanout0(pObj)) : Abc_ObjName(pObj); }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Checks the integrity of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheck( Abc_Ntk_t * pNtk )
{ 
   return !Abc_FrameIsFlagEnabled( "check" ) || Abc_NtkDoCheck( pNtk );
}

/**Function*************************************************************

  Synopsis    [Checks the integrity of the network after reading.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckRead( Abc_Ntk_t * pNtk )
{
   return !Abc_FrameIsFlagEnabled( "checkread" ) || Abc_NtkDoCheck( pNtk );
}

/**Function*************************************************************

  Synopsis    [Checks the integrity of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj, * pNet, * pNode;
    int i;

    // check network types
    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
    {
        fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
        return 0;
    }
    if ( !Abc_NtkHasSop(pNtk) && !Abc_NtkHasBdd(pNtk) && !Abc_NtkHasAig(pNtk) && !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasBlackbox(pNtk) )
    {
        fprintf( stdout, "NetworkCheck: Unknown functionality type.\n" );
        return 0;
    }
    if ( Abc_NtkHasMapping(pNtk) )
    {
        if ( pNtk->pManFunc != Abc_FrameReadLibGen() )
        {
            fprintf( stdout, "NetworkCheck: The library of the mapped network is not the global library.\n" );
            return 0;
        }
    }

    if ( Abc_NtkHasOnlyLatchBoxes(pNtk) )
    {
        // check CI/CO numbers
        if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) )
        {
            fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
            fprintf( stdout, "One possible reason is that latches are added twice:\n" );
            fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" );
            return 0;
        }
        if ( Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
        {
            fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
            fprintf( stdout, "One possible reason is that latches are added twice:\n" );
            fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" );
            return 0;
        }
    }

    // check the names
    if ( !Abc_NtkCheckNames( pNtk ) )
        return 0;

    // check PIs and POs
    Abc_NtkCleanCopy( pNtk );
    if ( !Abc_NtkCheckPis( pNtk ) )
        return 0;
    if ( !Abc_NtkCheckPos( pNtk ) )
        return 0;

    if ( Abc_NtkHasBlackbox(pNtk) )
        return 1;

    // check the connectivity of objects
    Abc_NtkForEachObj( pNtk, pObj, i )
        if ( !Abc_NtkCheckObj( pNtk, pObj ) )
            return 0;

    // if it is a netlist change nets and latches
    if ( Abc_NtkIsNetlist(pNtk) )
    {
        if ( Abc_NtkNetNum(pNtk) == 0 )
            fprintf( stdout, "NetworkCheck: Warning! Netlist has no nets.\n" );
        // check the nets
        Abc_NtkForEachNet( pNtk, pNet, i )
            if ( !Abc_NtkCheckNet( pNtk, pNet ) )
                return 0;
    }
    else
    {
        if ( Abc_NtkNetNum(pNtk) != 0 )
        {
            fprintf( stdout, "NetworkCheck: A network that is not a netlist has nets.\n" );
            return 0;
        }
    }

    // check the nodes
    if ( Abc_NtkIsStrash(pNtk) )
        Abc_AigCheck( (Abc_Aig_t *)pNtk->pManFunc );
    else
    {
        Abc_NtkForEachNode( pNtk, pNode, i )
            if ( !Abc_NtkCheckNode( pNtk, pNode ) )
                return 0;
    }

    // check the latches
    Abc_NtkForEachLatch( pNtk, pNode, i )
        if ( !Abc_NtkCheckLatch( pNtk, pNode ) )
            return 0;

    // finally, check for combinational loops
//  clk = Abc_Clock();
    if ( !Abc_NtkIsAcyclic( pNtk ) )
    {
        fprintf( stdout, "NetworkCheck: Network contains a combinational loop.\n" );
        return 0;
    }
//  ABC_PRT( "Acyclic  ", Abc_Clock() - clk );

    // check the EXDC network if present
    if ( pNtk->pExdc )
        Abc_NtkCheck( pNtk->pExdc );
/*
    // check the hierarchy
    if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
    {
        stmm_generator * gen;
        Abc_Ntk_t * pNtkTemp;
        char * pName;
        // check other networks
        stmm_foreach_item( pNtk->tName2Model, gen, &pName, (char **)&pNtkTemp )
        {
            pNtkTemp->fHiePath = pNtkTemp->fHieVisited = 0;
            if ( !Abc_NtkCheck( pNtkTemp ) )
                return 0;
        }
        // check acyclic dependency of the models
        if ( !Abc_NtkIsAcyclicHierarchy( pNtk ) )
        {
            fprintf( stdout, "NetworkCheck: Network hierarchical dependences contains a cycle.\n" );
            return 0;
        }
    }
*/
    return 1;
}

/**Function*************************************************************

  Synopsis    [Checks the names.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj = NULL; // Ensure pObj isn't used uninitialized.
    Vec_Int_t * vNameIds;
    char * pName;
    int i, NameId;

    if ( Abc_NtkIsNetlist(pNtk) )
        return 1;

    // check that each CI/CO has a name
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        pObj = Abc_ObjFanout0Ntk(pObj);
        if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
        {
            fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id );
            return 0;
        }
    }
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        pObj = Abc_ObjFanin0Ntk(pObj);
        if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
        {
            fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id );
            return 0;
        }
    }

    assert(pObj); // pObj should point to something here.

    // return the array of all IDs, which have names
    vNameIds = Nm_ManReturnNameIds( pNtk->pManName );
    // make sure that these IDs correspond to live objects
    Vec_IntForEachEntry( vNameIds, NameId, i )
    {
        if ( Vec_PtrEntry( pNtk->vObjs, NameId ) == NULL )
        {
            Vec_IntFree( vNameIds );
            pName = Nm_ManFindNameById(pObj->pNtk->pManName, NameId);
            fprintf( stdout, "NetworkCheck: Object with ID %d is deleted but its name \"%s\" remains in the name table.\n", NameId, pName );
            return 0;
        }
    }
    Vec_IntFree( vNameIds );

    // make sure the CI names are unique
    if ( !Abc_NtkCheckUniqueCiNames(pNtk) )
        return 0;

    // make sure the CO names are unique
    if ( !Abc_NtkCheckUniqueCoNames(pNtk) )
        return 0;

    // make sure that if a CO has the same name as a CI, they point directly
    if ( !Abc_NtkCheckUniqueCioNames(pNtk) )
        return 0;

    return 1;
}


/**Function*************************************************************

  Synopsis    [Checks the PIs of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckPis( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj;
    int i;

    // check that PIs are indeed PIs
    Abc_NtkForEachPi( pNtk, pObj, i )
    {
        if ( !Abc_ObjIsPi(pObj) )
        {
            fprintf( stdout, "NetworkCheck: Object \"%s\" (id=%d) is in the PI list but is not a PI.\n", Abc_ObjName(pObj), pObj->Id );
            return 0;
        }
        if ( pObj->pData )
        {
            fprintf( stdout, "NetworkCheck: A PI \"%s\" has a logic function.\n", Abc_ObjName(pObj) );
            return 0;
        }
        if ( Abc_ObjFaninNum(pObj) > 0 )
        {
            fprintf( stdout, "NetworkCheck: A PI \"%s\" has fanins.\n", Abc_ObjName(pObj) );
            return 0;
        }
        pObj->pCopy = (Abc_Obj_t *)1;
    }
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        if ( pObj->pCopy == NULL && Abc_ObjIsPi(pObj) )
        {
            fprintf( stdout, "NetworkCheck: Object \"%s\" (id=%d) is a PI but is not in the PI list.\n", Abc_ObjName(pObj), pObj->Id );
            return 0;
        }
        pObj->pCopy = NULL;
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Checks the POs of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj;
    int i;

    // check that POs are indeed POs
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
        if ( !Abc_ObjIsPo(pObj) )
        {
            fprintf( stdout, "NetworkCheck: Net \"%s\" (id=%d) is in the PO list but is not a PO.\n", Abc_ObjName(pObj), pObj->Id );
            return 0;
        }
        if ( pObj->pData )
        {
            fprintf( stdout, "NetworkCheck: A PO \"%s\" has a logic function.\n", Abc_ObjName(pObj) );
            return 0;
        }
        if ( Abc_ObjFaninNum(pObj) != 1 )
        {
            fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin (but %d).\n", Abc_ObjName(pObj), Abc_ObjFaninNum(pObj) );
            return 0;
        }
        if ( Abc_ObjFanoutNum(pObj) > 0 )
        {
            fprintf( stdout, "NetworkCheck: A PO \"%s\" has %d fanout(s).\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
            return 0;
        }
        pObj->pCopy = (Abc_Obj_t *)1;
    }
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        if ( pObj->pCopy == NULL && Abc_ObjIsPo(pObj) )
        {
            fprintf( stdout, "NetworkCheck: Net \"%s\" (id=%d) is in a PO but is not in the PO list.\n", Abc_ObjName(pObj), pObj->Id );
            return 0;
        }
        pObj->pCopy = NULL;
    }
    return 1;
}


/**Function*************************************************************

  Synopsis    [Checks the connectivity of the object.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
{
    Abc_Obj_t * pFanin, * pFanout;
    int Value = 1;
    int i, k;

    // check the network
    if ( pObj->pNtk != pNtk )
    {
        fprintf( stdout, "NetworkCheck: Object \"%s\" does not belong to the network.\n", Abc_ObjName(pObj) );
        return 0;
    }
    // check the object ID
    if ( pObj->Id < 0 || (int)pObj->Id >= Abc_NtkObjNumMax(pNtk) )
    {
        fprintf( stdout, "NetworkCheck: Object \"%s\" has incorrect ID.\n", Abc_ObjName(pObj) );
        return 0;
    }

    if ( !Abc_FrameIsFlagEnabled("checkfio") )
        return Value;

    // go through the fanins of the object and make sure fanins have this object as a fanout
    Abc_ObjForEachFanin( pObj, pFanin, i )
    {
        if ( Vec_IntFind( &pFanin->vFanouts, pObj->Id ) == -1 )
        {
            fprintf( stdout, "NodeCheck: Object \"%s\" has fanin ", Abc_ObjName(pObj) );
            fprintf( stdout, "\"%s\" but the fanin does not have it as a fanout.\n", Abc_ObjName(pFanin) );
            Value = 0;
        }
    }
    // go through the fanouts of the object and make sure fanouts have this object as a fanin
    Abc_ObjForEachFanout( pObj, pFanout, i )
    {
        if ( Vec_IntFind( &pFanout->vFanins, pObj->Id ) == -1 )
        {
            fprintf( stdout, "NodeCheck: Object \"%s\" has fanout ", Abc_ObjName(pObj) );
            fprintf( stdout, "\"%s\" but the fanout does not have it as a fanin.\n", Abc_ObjName(pFanout) );
            Value = 0;
        }
    }

    // make sure fanins are not duplicated
    for ( i = 0; i < pObj->vFanins.nSize; i++ )
        for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
            if ( pObj->vFanins.pArray[k] == pObj->vFanins.pArray[i] )
            {
                printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) );
            }

    // save time: do not check large fanout lists
    if ( pObj->vFanouts.nSize > 100 )
        return Value;

    // make sure fanouts are not duplicated
    for ( i = 0; i < pObj->vFanouts.nSize; i++ )
        for ( k = i + 1; k < pObj->vFanouts.nSize; k++ )
            if ( pObj->vFanouts.pArray[k] == pObj->vFanouts.pArray[i] )
            {
                printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
            }

    return Value;
}

/**Function*************************************************************

  Synopsis    [Checks the integrity of a net.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckNet( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
{
    if ( Abc_ObjFaninNum(pNet) == 0 )
    {
        fprintf( stdout, "NetworkCheck: Net \"%s\" is not driven.\n", Abc_ObjName(pNet) );
        return 0;
    }
    if ( Abc_ObjFaninNum(pNet) > 1 )
    {
        fprintf( stdout, "NetworkCheck: Net \"%s\" has more than one driver.\n", Abc_ObjName(pNet) );
        return 0;
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Checks the integrity of a node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
{
    // detect internal nodes that do not have nets
    if ( Abc_NtkIsNetlist(pNtk) && Abc_ObjFanoutNum(pNode) == 0 )
    {
        fprintf( stdout, "Node (id = %d) has no net to drive.\n", pNode->Id );
        return 0;
    }
    // the node should have a function assigned unless it is an AIG
    if ( pNode->pData == NULL )
    {
        fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_ObjNameNet(pNode) );
        return 0;
    }
    // the netlist and SOP logic network should have SOPs
    if ( Abc_NtkHasSop(pNtk) )
    {
        if ( !Abc_SopCheck( (char *)pNode->pData, Abc_ObjFaninNum(pNode) ) )
        {
            fprintf( stdout, "NodeCheck: SOP check for node \"%s\" has failed.\n", Abc_ObjNameNet(pNode) );
            return 0;
        }
    }
    else if ( Abc_NtkHasBdd(pNtk) )
    {
        int nSuppSize = Cudd_SupportSize((DdManager *)pNtk->pManFunc, (DdNode *)pNode->pData);
        if ( nSuppSize > Abc_ObjFaninNum(pNode) )
        {
            fprintf( stdout, "NodeCheck: BDD of the node \"%s\" has incorrect support size.\n", Abc_ObjNameNet(pNode) );
            return 0;
        }
    }
    else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasAig(pNtk) )
    {
        assert( 0 );
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Checks the integrity of a latch.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
{
    int Value = 1;
    // check whether the object is a latch
    if ( !Abc_ObjIsLatch(pLatch) )
    {
        fprintf( stdout, "NodeCheck: Latch \"%s\" is in a latch list but is not a latch.\n", Abc_ObjName(pLatch) );
        Value = 0;
    }
    // make sure the latch has a reasonable return value
    if ( (int)(ABC_PTRINT_T)pLatch->pData < ABC_INIT_ZERO || (int)(ABC_PTRINT_T)pLatch->pData > ABC_INIT_DC )
    {
        fprintf( stdout, "NodeCheck: Latch \"%s\" has incorrect reset value (%d).\n", 
            Abc_ObjName(pLatch), (int)(ABC_PTRINT_T)pLatch->pData );
        Value = 0;
    }
    // make sure the latch has only one fanin
    if ( Abc_ObjFaninNum(pLatch) != 1 )
    {
        fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanins.\n", Abc_ObjName(pLatch), Abc_ObjFaninNum(pLatch) );
        Value = 0;
    }
    // make sure the latch has only one fanout
    if ( Abc_ObjFanoutNum(pLatch) != 1 )
    {
        fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanouts.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) );
        Value = 0;
    }
    // make sure the latch input has only one fanin
    if ( Abc_ObjFaninNum(Abc_ObjFanin0(pLatch)) != 1 )
    {
        fprintf( stdout, "NodeCheck: Input of latch \"%s\" has wrong number (%d) of fanins.\n", 
            Abc_ObjName(Abc_ObjFanin0(pLatch)), Abc_ObjFaninNum(Abc_ObjFanin0(pLatch)) );
        Value = 0;
    }
    // make sure the latch input has only one fanout
    if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pLatch)) != 1 )
    {
        fprintf( stdout, "NodeCheck: Input of latch \"%s\" has wrong number (%d) of fanouts.\n", 
            Abc_ObjName(Abc_ObjFanin0(pLatch)), Abc_ObjFanoutNum(Abc_ObjFanin0(pLatch)) );
        Value = 0;
    }
    // make sure the latch output has only one fanin
    if ( Abc_ObjFaninNum(Abc_ObjFanout0(pLatch)) != 1 )
    {
        fprintf( stdout, "NodeCheck: Output of latch \"%s\" has wrong number (%d) of fanins.\n", 
            Abc_ObjName(Abc_ObjFanout0(pLatch)), Abc_ObjFaninNum(Abc_ObjFanout0(pLatch)) );
        Value = 0;
    }
    return Value;
}




/**Function*************************************************************

  Synopsis    [Compares the PIs of the two networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkComparePis( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
{
    Abc_Obj_t * pObj1;
    int i;
    if ( Abc_NtkPiNum(pNtk1) != Abc_NtkPiNum(pNtk2) )
    {
        printf( "Networks have different number of primary inputs.\n" );
        return 0;
    }
    // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
    Abc_NtkForEachPi( pNtk1, pObj1, i )
    {
        if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPi(pNtk2,i)) ) != 0 )
        {
            printf( "Primary input #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", 
                i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPi(pNtk2,i)) );
            return 0;
        }
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Compares the POs of the two networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
{
    Abc_Obj_t * pObj1;
    int i;
    if ( Abc_NtkPoNum(pNtk1) != Abc_NtkPoNum(pNtk2) )
    {
        printf( "Networks have different number of primary outputs.\n" );
        return 0;
    }
    // for each PO of pNet1 find corresponding PO of pNet2 and reorder them
    Abc_NtkForEachPo( pNtk1, pObj1, i )
    {
        if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) ) != 0 )
        {
            printf( "Primary output #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", 
                i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) );
            return 0;
        }
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Compares the latches of the two networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
{
    Abc_Obj_t * pObj1;
    int i;
    assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
    assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
    if ( !fComb )
        return 1;
    if ( Abc_NtkBoxNum(pNtk1) != Abc_NtkBoxNum(pNtk2) )
    {
        printf( "Networks have different number of latches.\n" );
        return 0;
    }
    // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
    Abc_NtkForEachBox( pNtk1, pObj1, i )
    {
        if ( strcmp( Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) ) != 0 )
        {
            printf( "Box #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", 
                i, Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) );
            return 0;
        }
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Compares the signals of the networks.]

  Description []
               
  SideEffects [Ordering POs by name is a very bad idea! It destroys
  the natural order of the logic in the circuit.]

  SeeAlso     []

***********************************************************************/
int Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb )
{
    Abc_NtkOrderObjsByName( pNtk1, fComb );
    Abc_NtkOrderObjsByName( pNtk2, fComb );
    if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) )
        return 0;
    if ( !fOnlyPis )
    {
        if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) )
            return 0;
        if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) )
            return 0;
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Returns 0 if the network hierachy contains a cycle.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkIsAcyclicHierarchy_rec( Abc_Ntk_t * pNtk )
{
    Abc_Ntk_t * pNtkNext;
    Abc_Obj_t * pObj;
    int i;
    // return if visited
    if ( pNtk->fHieVisited )
        return 1;
    pNtk->fHieVisited = 1;
    // return if black box
    if ( Abc_NtkHasBlackbox(pNtk) )
        return 1;
    assert( Abc_NtkIsNetlist(pNtk) );
    // go through all the children networks
    Abc_NtkForEachBox( pNtk, pObj, i )
    {
        if ( Abc_ObjIsLatch(pObj) )
            continue;
        pNtkNext = (Abc_Ntk_t *)pObj->pData;
        assert( pNtkNext != NULL );
        if ( pNtkNext->fHiePath )
            return 0;
        pNtk->fHiePath = 1;
        if ( !Abc_NtkIsAcyclicHierarchy_rec( pNtkNext ) )
            return 0;
        pNtk->fHiePath = 0;
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Returns 0 if the network hierachy contains a cycle.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk )
{
    Abc_Ntk_t * pTemp;
    int i, RetValue;
    assert( Abc_NtkIsNetlist(pNtk) && pNtk->pDesign );
    // clear the modules
    Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
        pTemp->fHieVisited = pTemp->fHiePath = 0;
    // traverse
    pNtk->fHiePath = 1;
    RetValue = Abc_NtkIsAcyclicHierarchy_rec( pNtk );
    pNtk->fHiePath = 0;
    // clear the modules
    Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
        pTemp->fHieVisited = pTemp->fHiePath = 0;
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Returns 0 if CI names are repeated.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkNamesCompare( char ** pName1, char ** pName2 )
{
    return strcmp( *pName1, *pName2 );
}

/**Function*************************************************************

  Synopsis    [Returns 0 if CI names are repeated.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk )
{
    Vec_Ptr_t * vNames;
    Abc_Obj_t * pObj;
    int i, fRetValue = 1;
    assert( !Abc_NtkIsNetlist(pNtk) );
    vNames = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Vec_PtrPush( vNames, Abc_ObjName(pObj) );
    Vec_PtrSort( vNames, (int (*)())Abc_NtkNamesCompare );
    for ( i = 1; i < Abc_NtkCiNum(pNtk); i++ )
        if ( !strcmp( (const char *)Vec_PtrEntry(vNames,i-1), (const char *)Vec_PtrEntry(vNames,i) ) )
        {
            printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", (char*)Vec_PtrEntry(vNames,i-1), (char*)Vec_PtrEntry(vNames,i) );
            fRetValue = 0;
        }
    Vec_PtrFree( vNames );
    return fRetValue;
}

/**Function*************************************************************

  Synopsis    [Returns 0 if CO names are repeated.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk )
{
    Vec_Ptr_t * vNames;
    Abc_Obj_t * pObj;
    int i, fRetValue = 1;
    assert( !Abc_NtkIsNetlist(pNtk) );
    vNames = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachCo( pNtk, pObj, i )
        Vec_PtrPush( vNames, Abc_ObjName(pObj) );
    Vec_PtrSort( vNames, (int (*)())Abc_NtkNamesCompare );
    for ( i = 1; i < Abc_NtkCoNum(pNtk); i++ )
    {
//        printf( "%s\n", Vec_PtrEntry(vNames,i) );
        if ( !strcmp( (const char *)Vec_PtrEntry(vNames,i-1), (const char *)Vec_PtrEntry(vNames,i) ) )
        {
            printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", (char*)Vec_PtrEntry(vNames,i-1), (char*)Vec_PtrEntry(vNames,i) );
            fRetValue = 0;
        }
    }
    Vec_PtrFree( vNames );
    return fRetValue;
}

/**Function*************************************************************

  Synopsis    [Returns 0 if there is a pair of CI/CO with the same name and logic in between.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj, * pObjCi, * pFanin;
    int i, nCiId, fRetValue = 1;
    assert( !Abc_NtkIsNetlist(pNtk) );
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        nCiId = Nm_ManFindIdByNameTwoTypes( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
        if ( nCiId == -1 )
            continue;
        pObjCi = Abc_NtkObj( pNtk, nCiId );
        assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) );
        pFanin = Abc_ObjFanin0(pObj);
        if ( pFanin != pObjCi )
        {
            printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly. The name of the CO fanin is %s.\n", 
                Abc_ObjName(pObj), Abc_ObjName(Abc_ObjFanin0(pObj)) );
            fRetValue = 0;
        }
    }
    return fRetValue;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END