src/base/abc/abcCheck.c File Reference

#include "abc.h"
#include "main.h"
Include dependency graph for abcCheck.c:

Go to the source code of this file.

Functions

static bool Abc_NtkCheckNames (Abc_Ntk_t *pNtk)
static bool Abc_NtkCheckPis (Abc_Ntk_t *pNtk)
static bool Abc_NtkCheckPos (Abc_Ntk_t *pNtk)
static bool Abc_NtkCheckNet (Abc_Ntk_t *pNtk, Abc_Obj_t *pNet)
static bool Abc_NtkCheckNode (Abc_Ntk_t *pNtk, Abc_Obj_t *pNode)
static bool Abc_NtkCheckLatch (Abc_Ntk_t *pNtk, Abc_Obj_t *pLatch)
static bool Abc_NtkComparePis (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb)
static bool Abc_NtkComparePos (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb)
static bool Abc_NtkCompareLatches (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb)
static char * Abc_ObjNameNet (Abc_Obj_t *pObj)
bool Abc_NtkCheck (Abc_Ntk_t *pNtk)
bool Abc_NtkCheckRead (Abc_Ntk_t *pNtk)
bool Abc_NtkDoCheck (Abc_Ntk_t *pNtk)
bool Abc_NtkCheckObj (Abc_Ntk_t *pNtk, Abc_Obj_t *pObj)
bool Abc_NtkCompareBoxes (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb)
bool Abc_NtkCompareSignals (Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fOnlyPis, int fComb)
int Abc_NtkIsAcyclicHierarchy_rec (Abc_Ntk_t *pNtk)
int Abc_NtkIsAcyclicHierarchy (Abc_Ntk_t *pNtk)
int Abc_NtkNamesCompare (char **pName1, char **pName2)
int Abc_NtkCheckUniqueCiNames (Abc_Ntk_t *pNtk)
int Abc_NtkCheckUniqueCoNames (Abc_Ntk_t *pNtk)
int Abc_NtkCheckUniqueCioNames (Abc_Ntk_t *pNtk)

Function Documentation

bool Abc_NtkCheck ( Abc_Ntk_t *  pNtk  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Checks the integrity of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file abcCheck.c.

00059 { 
00060    return !Abc_FrameIsFlagEnabled( "check" ) || Abc_NtkDoCheck( pNtk );
00061 }

bool Abc_NtkCheckLatch ( Abc_Ntk_t *  pNtk,
Abc_Obj_t *  pLatch 
) [static]

Function*************************************************************

Synopsis [Checks the integrity of a latch.]

Description []

SideEffects []

SeeAlso []

Definition at line 567 of file abcCheck.c.

00568 {
00569     int Value = 1;
00570     // check whether the object is a latch
00571     if ( !Abc_ObjIsLatch(pLatch) )
00572     {
00573         fprintf( stdout, "NodeCheck: Latch \"%s\" is in a latch list but is not a latch.\n", Abc_ObjName(pLatch) );
00574         Value = 0;
00575     }
00576     // make sure the latch has a reasonable return value
00577     if ( (int)pLatch->pData < ABC_INIT_ZERO || (int)pLatch->pData > ABC_INIT_DC )
00578     {
00579         fprintf( stdout, "NodeCheck: Latch \"%s\" has incorrect reset value (%d).\n", 
00580             Abc_ObjName(pLatch), (int)pLatch->pData );
00581         Value = 0;
00582     }
00583     // make sure the latch has only one fanin
00584     if ( Abc_ObjFaninNum(pLatch) != 1 )
00585     {
00586         fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanins.\n", Abc_ObjName(pLatch), Abc_ObjFaninNum(pLatch) );
00587         Value = 0;
00588     }
00589     // make sure the latch has only one fanout
00590     if ( Abc_ObjFanoutNum(pLatch) != 1 )
00591     {
00592         fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanouts.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) );
00593         Value = 0;
00594     }
00595     // make sure the latch input has only one fanin
00596     if ( Abc_ObjFaninNum(Abc_ObjFanin0(pLatch)) != 1 )
00597     {
00598         fprintf( stdout, "NodeCheck: Input of latch \"%s\" has wrong number (%d) of fanins.\n", 
00599             Abc_ObjName(Abc_ObjFanin0(pLatch)), Abc_ObjFaninNum(Abc_ObjFanin0(pLatch)) );
00600         Value = 0;
00601     }
00602     // make sure the latch input has only one fanout
00603     if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pLatch)) != 1 )
00604     {
00605         fprintf( stdout, "NodeCheck: Input of latch \"%s\" has wrong number (%d) of fanouts.\n", 
00606             Abc_ObjName(Abc_ObjFanin0(pLatch)), Abc_ObjFanoutNum(Abc_ObjFanin0(pLatch)) );
00607         Value = 0;
00608     }
00609     // make sure the latch output has only one fanin
00610     if ( Abc_ObjFaninNum(Abc_ObjFanout0(pLatch)) != 1 )
00611     {
00612         fprintf( stdout, "NodeCheck: Output of latch \"%s\" has wrong number (%d) of fanins.\n", 
00613             Abc_ObjName(Abc_ObjFanout0(pLatch)), Abc_ObjFaninNum(Abc_ObjFanout0(pLatch)) );
00614         Value = 0;
00615     }
00616     return Value;
00617 }

bool Abc_NtkCheckNames ( Abc_Ntk_t *  pNtk  )  [static]

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

] DECLARATIONS ///

Function*************************************************************

Synopsis [Checks the names.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file abcCheck.c.

00239 {
00240     Abc_Obj_t * pObj;
00241     Vec_Int_t * vNameIds;
00242     char * pName;
00243     int i, NameId;
00244 
00245     if ( Abc_NtkIsNetlist(pNtk) )
00246         return 1;
00247 
00248     // check that each CI/CO has a name
00249     Abc_NtkForEachCi( pNtk, pObj, i )
00250     {
00251         pObj = Abc_ObjFanout0Ntk(pObj);
00252         if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
00253         {
00254             fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id );
00255             return 0;
00256         }
00257     }
00258     Abc_NtkForEachCo( pNtk, pObj, i )
00259     {
00260         pObj = Abc_ObjFanin0Ntk(pObj);
00261         if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
00262         {
00263             fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id );
00264             return 0;
00265         }
00266     }
00267 
00268     // return the array of all IDs, which have names
00269     vNameIds = Nm_ManReturnNameIds( pNtk->pManName );
00270     // make sure that these IDs correspond to live objects
00271     Vec_IntForEachEntry( vNameIds, NameId, i )
00272     {
00273         if ( Vec_PtrEntry( pNtk->vObjs, NameId ) == NULL )
00274         {
00275             Vec_IntFree( vNameIds );
00276             pName = Nm_ManFindNameById(pObj->pNtk->pManName, NameId);
00277             fprintf( stdout, "NetworkCheck: Object with ID %d is deleted but its name \"%s\" remains in the name table.\n", NameId, pName );
00278             return 0;
00279         }
00280     }
00281     Vec_IntFree( vNameIds );
00282 
00283     // make sure the CI names are unique
00284     if ( !Abc_NtkCheckUniqueCiNames(pNtk) )
00285         return 0;
00286 
00287     // make sure the CO names are unique
00288     if ( !Abc_NtkCheckUniqueCoNames(pNtk) )
00289         return 0;
00290 
00291     // make sure that if a CO has the same name as a CI, they point directly
00292     if ( !Abc_NtkCheckUniqueCioNames(pNtk) )
00293         return 0;
00294 
00295     return 1;
00296 }

bool Abc_NtkCheckNet ( Abc_Ntk_t *  pNtk,
Abc_Obj_t *  pNet 
) [static]

Function*************************************************************

Synopsis [Checks the integrity of a net.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file abcCheck.c.

00492 {
00493     if ( Abc_ObjFaninNum(pNet) == 0 )
00494     {
00495         fprintf( stdout, "NetworkCheck: Net \"%s\" is not driven.\n", Abc_ObjName(pNet) );
00496         return 0;
00497     }
00498     if ( Abc_ObjFaninNum(pNet) > 1 )
00499     {
00500         fprintf( stdout, "NetworkCheck: Net \"%s\" has more than one driver.\n", Abc_ObjName(pNet) );
00501         return 0;
00502     }
00503     return 1;
00504 }

bool Abc_NtkCheckNode ( Abc_Ntk_t *  pNtk,
Abc_Obj_t *  pNode 
) [static]

Function*************************************************************

Synopsis [Checks the integrity of a node.]

Description []

SideEffects []

SeeAlso []

Definition at line 517 of file abcCheck.c.

00518 {
00519     // detect internal nodes that do not have nets
00520     if ( Abc_NtkIsNetlist(pNtk) && Abc_ObjFanoutNum(pNode) == 0 )
00521     {
00522         fprintf( stdout, "Node (id = %d) has no net to drive.\n", pNode->Id );
00523         return 0;
00524     }
00525     // the node should have a function assigned unless it is an AIG
00526     if ( pNode->pData == NULL )
00527     {
00528         fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_ObjNameNet(pNode) );
00529         return 0;
00530     }
00531     // the netlist and SOP logic network should have SOPs
00532     if ( Abc_NtkHasSop(pNtk) )
00533     {
00534         if ( !Abc_SopCheck( pNode->pData, Abc_ObjFaninNum(pNode) ) )
00535         {
00536             fprintf( stdout, "NodeCheck: SOP check for node \"%s\" has failed.\n", Abc_ObjNameNet(pNode) );
00537             return 0;
00538         }
00539     }
00540     else if ( Abc_NtkHasBdd(pNtk) )
00541     {
00542         int nSuppSize = Cudd_SupportSize(pNtk->pManFunc, pNode->pData);
00543         if ( nSuppSize > Abc_ObjFaninNum(pNode) )
00544         {
00545             fprintf( stdout, "NodeCheck: BDD of the node \"%s\" has incorrect support size.\n", Abc_ObjNameNet(pNode) );
00546             return 0;
00547         }
00548     }
00549     else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasAig(pNtk) )
00550     {
00551         assert( 0 );
00552     }
00553     return 1;
00554 }

bool Abc_NtkCheckObj ( Abc_Ntk_t *  pNtk,
Abc_Obj_t *  pObj 
)

Function*************************************************************

Synopsis [Checks the connectivity of the object.]

Description []

SideEffects []

SeeAlso []

Definition at line 412 of file abcCheck.c.

00413 {
00414     Abc_Obj_t * pFanin, * pFanout;
00415     int i, Value = 1;
00416     int k;
00417 
00418     // check the network
00419     if ( pObj->pNtk != pNtk )
00420     {
00421         fprintf( stdout, "NetworkCheck: Object \"%s\" does not belong to the network.\n", Abc_ObjName(pObj) );
00422         return 0;
00423     }
00424     // check the object ID
00425     if ( pObj->Id < 0 || (int)pObj->Id >= Abc_NtkObjNumMax(pNtk) )
00426     {
00427         fprintf( stdout, "NetworkCheck: Object \"%s\" has incorrect ID.\n", Abc_ObjName(pObj) );
00428         return 0;
00429     }
00430 
00431     if ( !Abc_FrameIsFlagEnabled("checkfio") )
00432         return Value;
00433 
00434     // go through the fanins of the object and make sure fanins have this object as a fanout
00435     Abc_ObjForEachFanin( pObj, pFanin, i )
00436     {
00437         if ( Vec_IntFind( &pFanin->vFanouts, pObj->Id ) == -1 )
00438         {
00439             fprintf( stdout, "NodeCheck: Object \"%s\" has fanin ", Abc_ObjName(pObj) );
00440             fprintf( stdout, "\"%s\" but the fanin does not have it as a fanout.\n", Abc_ObjName(pFanin) );
00441             Value = 0;
00442         }
00443     }
00444     // go through the fanouts of the object and make sure fanouts have this object as a fanin
00445     Abc_ObjForEachFanout( pObj, pFanout, i )
00446     {
00447         if ( Vec_IntFind( &pFanout->vFanins, pObj->Id ) == -1 )
00448         {
00449             fprintf( stdout, "NodeCheck: Object \"%s\" has fanout ", Abc_ObjName(pObj) );
00450             fprintf( stdout, "\"%s\" but the fanout does not have it as a fanin.\n", Abc_ObjName(pFanout) );
00451             Value = 0;
00452         }
00453     }
00454 
00455     // make sure fanins are not duplicated
00456     for ( i = 0; i < pObj->vFanins.nSize; i++ )
00457         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
00458             if ( pObj->vFanins.pArray[k] == pObj->vFanins.pArray[i] )
00459             {
00460                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
00461                 printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) );
00462             }
00463 
00464     // save time: do not check large fanout lists
00465     if ( pObj->vFanouts.nSize > 100 )
00466         return Value;
00467 
00468     // make sure fanouts are not duplicated
00469     for ( i = 0; i < pObj->vFanouts.nSize; i++ )
00470         for ( k = i + 1; k < pObj->vFanouts.nSize; k++ )
00471             if ( pObj->vFanouts.pArray[k] == pObj->vFanouts.pArray[i] )
00472             {
00473                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
00474                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
00475             }
00476 
00477     return Value;
00478 }

bool Abc_NtkCheckPis ( Abc_Ntk_t *  pNtk  )  [static]

Function*************************************************************

Synopsis [Checks the PIs of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file abcCheck.c.

00311 {
00312     Abc_Obj_t * pObj;
00313     int i;
00314 
00315     // check that PIs are indeed PIs
00316     Abc_NtkForEachPi( pNtk, pObj, i )
00317     {
00318         if ( !Abc_ObjIsPi(pObj) )
00319         {
00320             fprintf( stdout, "NetworkCheck: Object \"%s\" (id=%d) is in the PI list but is not a PI.\n", Abc_ObjName(pObj), pObj->Id );
00321             return 0;
00322         }
00323         if ( pObj->pData )
00324         {
00325             fprintf( stdout, "NetworkCheck: A PI \"%s\" has a logic function.\n", Abc_ObjName(pObj) );
00326             return 0;
00327         }
00328         if ( Abc_ObjFaninNum(pObj) > 0 )
00329         {
00330             fprintf( stdout, "NetworkCheck: A PI \"%s\" has fanins.\n", Abc_ObjName(pObj) );
00331             return 0;
00332         }
00333         pObj->pCopy = (Abc_Obj_t *)1;
00334     }
00335     Abc_NtkForEachObj( pNtk, pObj, i )
00336     {
00337         if ( pObj->pCopy == NULL && Abc_ObjIsPi(pObj) )
00338         {
00339             fprintf( stdout, "NetworkCheck: Object \"%s\" (id=%d) is a PI but is not in the PI list.\n", Abc_ObjName(pObj), pObj->Id );
00340             return 0;
00341         }
00342         pObj->pCopy = NULL;
00343     }
00344     return 1;
00345 }

bool Abc_NtkCheckPos ( Abc_Ntk_t *  pNtk  )  [static]

Function*************************************************************

Synopsis [Checks the POs of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file abcCheck.c.

00359 {
00360     Abc_Obj_t * pObj;
00361     int i;
00362 
00363     // check that POs are indeed POs
00364     Abc_NtkForEachPo( pNtk, pObj, i )
00365     {
00366         if ( !Abc_ObjIsPo(pObj) )
00367         {
00368             fprintf( stdout, "NetworkCheck: Net \"%s\" (id=%d) is in the PO list but is not a PO.\n", Abc_ObjName(pObj), pObj->Id );
00369             return 0;
00370         }
00371         if ( pObj->pData )
00372         {
00373             fprintf( stdout, "NetworkCheck: A PO \"%s\" has a logic function.\n", Abc_ObjName(pObj) );
00374             return 0;
00375         }
00376         if ( Abc_ObjFaninNum(pObj) != 1 )
00377         {
00378             fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin.\n", Abc_ObjName(pObj) );
00379             return 0;
00380         }
00381         if ( Abc_ObjFanoutNum(pObj) > 0 )
00382         {
00383             fprintf( stdout, "NetworkCheck: A PO \"%s\" has fanouts.\n", Abc_ObjName(pObj) );
00384             return 0;
00385         }
00386         pObj->pCopy = (Abc_Obj_t *)1;
00387     }
00388     Abc_NtkForEachObj( pNtk, pObj, i )
00389     {
00390         if ( pObj->pCopy == NULL && Abc_ObjIsPo(pObj) )
00391         {
00392             fprintf( stdout, "NetworkCheck: Net \"%s\" (id=%d) is in a PO but is not in the PO list.\n", Abc_ObjName(pObj), pObj->Id );
00393             return 0;
00394         }
00395         pObj->pCopy = NULL;
00396     }
00397     return 1;
00398 }

bool Abc_NtkCheckRead ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file abcCheck.c.

00075 {
00076    return !Abc_FrameIsFlagEnabled( "checkread" ) || Abc_NtkDoCheck( pNtk );
00077 }

int Abc_NtkCheckUniqueCiNames ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Returns 0 if CI names are repeated.]

Description []

SideEffects []

SeeAlso []

Definition at line 849 of file abcCheck.c.

00850 {
00851     Vec_Ptr_t * vNames;
00852     Abc_Obj_t * pObj;
00853     int i, fRetValue = 1;
00854     assert( !Abc_NtkIsNetlist(pNtk) );
00855     vNames = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
00856     Abc_NtkForEachCi( pNtk, pObj, i )
00857         Vec_PtrPush( vNames, Abc_ObjName(pObj) );
00858     Vec_PtrSort( vNames, Abc_NtkNamesCompare );
00859     for ( i = 1; i < Abc_NtkCiNum(pNtk); i++ )
00860         if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) )
00861         {
00862             printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) );
00863             fRetValue = 0;
00864         }
00865     Vec_PtrFree( vNames );
00866     return fRetValue;
00867 }

int Abc_NtkCheckUniqueCioNames ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 914 of file abcCheck.c.

00915 {
00916     Abc_Obj_t * pObj, * pObjCi;
00917     int i, nCiId, fRetValue = 1;
00918     assert( !Abc_NtkIsNetlist(pNtk) );
00919     Abc_NtkForEachCo( pNtk, pObj, i )
00920     {
00921         nCiId = Nm_ManFindIdByNameTwoTypes( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
00922         if ( nCiId == -1 )
00923             continue;
00924         pObjCi = Abc_NtkObj( pNtk, nCiId );
00925         assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) );
00926         if ( Abc_ObjFanin0(pObj) != pObjCi )
00927         {
00928             printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly.\n", Abc_ObjName(pObj) );
00929             fRetValue = 0;
00930         }
00931     }
00932     return fRetValue;
00933 }

int Abc_NtkCheckUniqueCoNames ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Returns 0 if CO names are repeated.]

Description []

SideEffects []

SeeAlso []

Definition at line 880 of file abcCheck.c.

00881 {
00882     Vec_Ptr_t * vNames;
00883     Abc_Obj_t * pObj;
00884     int i, fRetValue = 1;
00885     assert( !Abc_NtkIsNetlist(pNtk) );
00886     vNames = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
00887     Abc_NtkForEachCo( pNtk, pObj, i )
00888         Vec_PtrPush( vNames, Abc_ObjName(pObj) );
00889     Vec_PtrSort( vNames, Abc_NtkNamesCompare );
00890     for ( i = 1; i < Abc_NtkCoNum(pNtk); i++ )
00891     {
00892 //        printf( "%s\n", Vec_PtrEntry(vNames,i) );
00893         if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) )
00894         {
00895             printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) );
00896             fRetValue = 0;
00897         }
00898     }
00899     Vec_PtrFree( vNames );
00900     return fRetValue;
00901 }

bool Abc_NtkCompareBoxes ( Abc_Ntk_t *  pNtk1,
Abc_Ntk_t *  pNtk2,
int  fComb 
)

Function*************************************************************

Synopsis [Compares the latches of the two networks.]

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file abcCheck.c.

00700 {
00701     Abc_Obj_t * pObj1;
00702     int i;
00703     assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
00704     assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
00705     if ( !fComb )
00706         return 1;
00707     if ( Abc_NtkBoxNum(pNtk1) != Abc_NtkBoxNum(pNtk2) )
00708     {
00709         printf( "Networks have different number of latches.\n" );
00710         return 0;
00711     }
00712     // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
00713     Abc_NtkForEachBox( pNtk1, pObj1, i )
00714     {
00715         if ( strcmp( Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) ) != 0 )
00716         {
00717             printf( "Box #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", 
00718                 i, Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) );
00719             return 0;
00720         }
00721     }
00722     return 1;
00723 }

static bool Abc_NtkCompareLatches ( Abc_Ntk_t *  pNtk1,
Abc_Ntk_t *  pNtk2,
int  fComb 
) [static]
bool Abc_NtkComparePis ( Abc_Ntk_t *  pNtk1,
Abc_Ntk_t *  pNtk2,
int  fComb 
) [static]

Function*************************************************************

Synopsis [Compares the PIs of the two networks.]

Description []

SideEffects []

SeeAlso []

Definition at line 633 of file abcCheck.c.

00634 {
00635     Abc_Obj_t * pObj1;
00636     int i;
00637     if ( Abc_NtkPiNum(pNtk1) != Abc_NtkPiNum(pNtk2) )
00638     {
00639         printf( "Networks have different number of primary inputs.\n" );
00640         return 0;
00641     }
00642     // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
00643     Abc_NtkForEachPi( pNtk1, pObj1, i )
00644     {
00645         if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPi(pNtk2,i)) ) != 0 )
00646         {
00647             printf( "Primary input #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", 
00648                 i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPi(pNtk2,i)) );
00649             return 0;
00650         }
00651     }
00652     return 1;
00653 }

bool Abc_NtkComparePos ( Abc_Ntk_t *  pNtk1,
Abc_Ntk_t *  pNtk2,
int  fComb 
) [static]

Function*************************************************************

Synopsis [Compares the POs of the two networks.]

Description []

SideEffects []

SeeAlso []

Definition at line 666 of file abcCheck.c.

00667 {
00668     Abc_Obj_t * pObj1;
00669     int i;
00670     if ( Abc_NtkPoNum(pNtk1) != Abc_NtkPoNum(pNtk2) )
00671     {
00672         printf( "Networks have different number of primary outputs.\n" );
00673         return 0;
00674     }
00675     // for each PO of pNet1 find corresponding PO of pNet2 and reorder them
00676     Abc_NtkForEachPo( pNtk1, pObj1, i )
00677     {
00678         if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) ) != 0 )
00679         {
00680             printf( "Primary output #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", 
00681                 i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) );
00682             return 0;
00683         }
00684     }
00685     return 1;
00686 }

bool Abc_NtkCompareSignals ( Abc_Ntk_t *  pNtk1,
Abc_Ntk_t *  pNtk2,
int  fOnlyPis,
int  fComb 
)

Function*************************************************************

Synopsis [Compares the signals of the networks.]

Description []

SideEffects []

SeeAlso []

Definition at line 736 of file abcCheck.c.

00737 {
00738     Abc_NtkOrderObjsByName( pNtk1, fComb );
00739     Abc_NtkOrderObjsByName( pNtk2, fComb );
00740     if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) )
00741         return 0;
00742     if ( !fOnlyPis )
00743     {
00744         if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) )
00745             return 0;
00746         if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) )
00747             return 0;
00748     }
00749     return 1;
00750 }

bool Abc_NtkDoCheck ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Checks the integrity of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file abcCheck.c.

00091 {
00092     Abc_Obj_t * pObj, * pNet, * pNode;
00093     int i;
00094 
00095     // check network types
00096     if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
00097     {
00098         fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
00099         return 0;
00100     }
00101     if ( !Abc_NtkHasSop(pNtk) && !Abc_NtkHasBdd(pNtk) && !Abc_NtkHasAig(pNtk) && !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasBlackbox(pNtk) )
00102     {
00103         fprintf( stdout, "NetworkCheck: Unknown functionality type.\n" );
00104         return 0;
00105     }
00106     if ( Abc_NtkHasMapping(pNtk) )
00107     {
00108         if ( pNtk->pManFunc != Abc_FrameReadLibGen() )
00109         {
00110             fprintf( stdout, "NetworkCheck: The library of the mapped network is not the global library.\n" );
00111             return 0;
00112         }
00113     }
00114 
00115     if ( Abc_NtkHasOnlyLatchBoxes(pNtk) )
00116     {
00117         // check CI/CO numbers
00118         if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) )
00119         {
00120             fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
00121             fprintf( stdout, "One possible reason is that latches are added twice:\n" );
00122             fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" );
00123             return 0;
00124         }
00125         if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
00126         {
00127             fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
00128             fprintf( stdout, "One possible reason is that latches are added twice:\n" );
00129             fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" );
00130             return 0;
00131         }
00132     }
00133 
00134     // check the names
00135     if ( !Abc_NtkCheckNames( pNtk ) )
00136         return 0;
00137 
00138     // check PIs and POs
00139     Abc_NtkCleanCopy( pNtk );
00140     if ( !Abc_NtkCheckPis( pNtk ) )
00141         return 0;
00142     if ( !Abc_NtkCheckPos( pNtk ) )
00143         return 0;
00144 
00145     if ( Abc_NtkHasBlackbox(pNtk) )
00146         return 1;
00147 
00148     // check the connectivity of objects
00149     Abc_NtkForEachObj( pNtk, pObj, i )
00150         if ( !Abc_NtkCheckObj( pNtk, pObj ) )
00151             return 0;
00152 
00153     // if it is a netlist change nets and latches
00154     if ( Abc_NtkIsNetlist(pNtk) )
00155     {
00156         if ( Abc_NtkNetNum(pNtk) == 0 )
00157         {
00158             fprintf( stdout, "NetworkCheck: Netlist has no nets.\n" );
00159             return 0;
00160         }
00161         // check the nets
00162         Abc_NtkForEachNet( pNtk, pNet, i )
00163             if ( !Abc_NtkCheckNet( pNtk, pNet ) )
00164                 return 0;
00165     }
00166     else
00167     {
00168         if ( Abc_NtkNetNum(pNtk) != 0 )
00169         {
00170             fprintf( stdout, "NetworkCheck: A network that is not a netlist has nets.\n" );
00171             return 0;
00172         }
00173     }
00174 
00175     // check the nodes
00176     if ( Abc_NtkIsStrash(pNtk) )
00177         Abc_AigCheck( pNtk->pManFunc );
00178     else
00179     {
00180         Abc_NtkForEachNode( pNtk, pNode, i )
00181             if ( !Abc_NtkCheckNode( pNtk, pNode ) )
00182                 return 0;
00183     }
00184 
00185     // check the latches
00186     Abc_NtkForEachLatch( pNtk, pNode, i )
00187         if ( !Abc_NtkCheckLatch( pNtk, pNode ) )
00188             return 0;
00189 
00190     // finally, check for combinational loops
00191 //  clk = clock();
00192     if ( !Abc_NtkIsAcyclic( pNtk ) )
00193     {
00194         fprintf( stdout, "NetworkCheck: Network contains a combinational loop.\n" );
00195         return 0;
00196     }
00197 //  PRT( "Acyclic  ", clock() - clk );
00198 
00199     // check the EXDC network if present
00200     if ( pNtk->pExdc )
00201         Abc_NtkCheck( pNtk->pExdc );
00202 /*
00203     // check the hierarchy
00204     if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
00205     {
00206         stmm_generator * gen;
00207         Abc_Ntk_t * pNtkTemp;
00208         char * pName;
00209         // check other networks
00210         stmm_foreach_item( pNtk->tName2Model, gen, &pName, (char **)&pNtkTemp )
00211         {
00212             pNtkTemp->fHiePath = pNtkTemp->fHieVisited = 0;
00213             if ( !Abc_NtkCheck( pNtkTemp ) )
00214                 return 0;
00215         }
00216         // check acyclic dependency of the models
00217         if ( !Abc_NtkIsAcyclicHierarchy( pNtk ) )
00218         {
00219             fprintf( stdout, "NetworkCheck: Network hierarchical dependences contains a cycle.\n" );
00220             return 0;
00221         }
00222     }
00223 */
00224     return 1;
00225 }

int Abc_NtkIsAcyclicHierarchy ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 804 of file abcCheck.c.

00805 {
00806     Abc_Ntk_t * pTemp;
00807     int i, RetValue;
00808     assert( Abc_NtkIsNetlist(pNtk) && pNtk->pDesign );
00809     // clear the modules
00810     Vec_PtrForEachEntry( pNtk->pDesign->vModules, pTemp, i )
00811         pTemp->fHieVisited = pTemp->fHiePath = 0;
00812     // traverse
00813     pNtk->fHiePath = 1;
00814     RetValue = Abc_NtkIsAcyclicHierarchy_rec( pNtk );
00815     pNtk->fHiePath = 0;
00816     // clear the modules
00817     Vec_PtrForEachEntry( pNtk->pDesign->vModules, pTemp, i )
00818         pTemp->fHieVisited = pTemp->fHiePath = 0;
00819     return RetValue;
00820 }

int Abc_NtkIsAcyclicHierarchy_rec ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

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

Description []

SideEffects []

SeeAlso []

Definition at line 763 of file abcCheck.c.

00764 {
00765     Abc_Ntk_t * pNtkNext;
00766     Abc_Obj_t * pObj;
00767     int i;
00768     // return if visited
00769     if ( pNtk->fHieVisited )
00770         return 1;
00771     pNtk->fHieVisited = 1;
00772     // return if black box
00773     if ( Abc_NtkHasBlackbox(pNtk) )
00774         return 1;
00775     assert( Abc_NtkIsNetlist(pNtk) );
00776     // go through all the children networks
00777     Abc_NtkForEachBox( pNtk, pObj, i )
00778     {
00779         if ( Abc_ObjIsLatch(pObj) )
00780             continue;
00781         pNtkNext = pObj->pData;
00782         assert( pNtkNext != NULL );
00783         if ( pNtkNext->fHiePath )
00784             return 0;
00785         pNtk->fHiePath = 1;
00786         if ( !Abc_NtkIsAcyclicHierarchy_rec( pNtkNext ) )
00787             return 0;
00788         pNtk->fHiePath = 0;
00789     }
00790     return 1;
00791 }

int Abc_NtkNamesCompare ( char **  pName1,
char **  pName2 
)

Function*************************************************************

Synopsis [Returns 0 if CI names are repeated.]

Description []

SideEffects []

SeeAlso []

Definition at line 833 of file abcCheck.c.

00834 {
00835     return strcmp( *pName1, *pName2 );
00836 }

static char* Abc_ObjNameNet ( Abc_Obj_t *  pObj  )  [inline, static]

Definition at line 41 of file abcCheck.c.

00041 { return (Abc_ObjIsNode(pObj) && Abc_NtkIsNetlist(pObj->pNtk)) ? Abc_ObjName(Abc_ObjFanout0(pObj)) : Abc_ObjName(pObj); }

Generated on Tue Jan 5 12:18:30 2010 for abc70930 by  doxygen 1.6.1