src/aig/ivy/ivyCheck.c File Reference

#include "ivy.h"
Include dependency graph for ivyCheck.c:

Go to the source code of this file.

Functions

int Ivy_ManCheck (Ivy_Man_t *p)
int Ivy_ManCheckFanoutNums (Ivy_Man_t *p)
int Ivy_ManCheckFanouts (Ivy_Man_t *p)
int Ivy_ManCheckChoices (Ivy_Man_t *p)

Function Documentation

int Ivy_ManCheck ( Ivy_Man_t *  p  ) 

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

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Checks the consistency of the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file ivyCheck.c.

00043 {
00044     Ivy_Obj_t * pObj, * pObj2;
00045     int i;
00046     Ivy_ManForEachObj( p, pObj, i )
00047     {
00048         // skip deleted nodes
00049         if ( Ivy_ObjId(pObj) != i )
00050         {
00051             printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
00052             return 0;
00053         }
00054         // consider the constant node and PIs
00055         if ( i == 0 || Ivy_ObjIsPi(pObj) )
00056         {
00057             if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) )
00058             {
00059                 printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id );
00060                 return 0;
00061             }
00062             continue;
00063         }
00064         if ( Ivy_ObjIsPo(pObj) )
00065         {
00066             if ( Ivy_ObjFaninId1(pObj) )
00067             {
00068                 printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id );
00069                 return 0;
00070             }
00071             continue;
00072         }
00073         if ( Ivy_ObjIsBuf(pObj) )
00074         {
00075             if ( Ivy_ObjFanin1(pObj) )
00076             {
00077                 printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
00078                 return 0;
00079             }
00080             continue;
00081         }
00082         if ( Ivy_ObjIsLatch(pObj) )
00083         {
00084             if ( Ivy_ObjFanin1(pObj) )
00085             {
00086                 printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
00087                 return 0;
00088             }
00089             if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
00090             {
00091                 printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
00092                 return 0;
00093             }
00094             pObj2 = Ivy_TableLookup( p, pObj );
00095             if ( pObj2 != pObj )
00096                 printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
00097                 continue;
00098         }
00099         // consider the AND node
00100         if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
00101         {
00102             printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
00103             return 0;
00104         }
00105         if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
00106         {
00107             printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
00108             return 0;
00109         }
00110         if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
00111             printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
00112         pObj2 = Ivy_TableLookup( p, pObj );
00113         if ( pObj2 != pObj )
00114             printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
00115         if ( Ivy_ObjRefs(pObj) == 0 )
00116             printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
00117         // check fanouts
00118         if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
00119             printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
00120     }
00121     // count the number of nodes in the table
00122     if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
00123     {
00124         printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
00125         return 0;
00126     }
00127 //    if ( !Ivy_ManCheckFanouts(p) )
00128 //        return 0;
00129     if ( !Ivy_ManIsAcyclic(p) )
00130         return 0;
00131     return 1; 
00132 }

int Ivy_ManCheckChoices ( Ivy_Man_t *  p  ) 

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

Synopsis [Checks that each choice node has exactly one node with fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file ivyCheck.c.

00253 {
00254     Ivy_Obj_t * pObj, * pTemp;
00255     int i;
00256     Ivy_ManForEachObj( p->pHaig, pObj, i )
00257     {
00258         if ( Ivy_ObjRefs(pObj) == 0 )
00259             continue;
00260         // count the number of nodes in the loop
00261         assert( !Ivy_IsComplement(pObj->pEquiv) );
00262         for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00263             if ( Ivy_ObjRefs(pTemp) > 1 )
00264                 printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
00265     }
00266     return 1;
00267 }

int Ivy_ManCheckFanoutNums ( Ivy_Man_t *  p  ) 

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

Synopsis [Verifies the fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file ivyCheck.c.

00146 {
00147     Ivy_Obj_t * pObj;
00148     int i, Counter = 0;
00149     Ivy_ManForEachObj( p, pObj, i )
00150         if ( Ivy_ObjIsNode(pObj) )
00151             Counter += (Ivy_ObjRefs(pObj) == 0);
00152     if ( Counter )
00153         printf( "Sequential AIG has %d dangling nodes.\n", Counter );
00154     return Counter;
00155 }

int Ivy_ManCheckFanouts ( Ivy_Man_t *  p  ) 

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

Synopsis [Verifies the fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file ivyCheck.c.

00169 {
00170     Vec_Ptr_t * vFanouts;
00171     Ivy_Obj_t * pObj, * pFanout, * pFanin;
00172     int i, k, RetValue = 1;
00173     if ( !p->fFanout )
00174         return 1;
00175     vFanouts = Vec_PtrAlloc( 100 );
00176     // make sure every fanin is a fanout
00177     Ivy_ManForEachObj( p, pObj, i )
00178     {
00179         pFanin = Ivy_ObjFanin0(pObj);
00180         if ( pFanin == NULL )
00181             continue;
00182         Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
00183             if ( pFanout == pObj )
00184                 break;
00185         if ( k == Vec_PtrSize(vFanouts) )
00186         {
00187             printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
00188             RetValue = 0;
00189         }
00190 
00191         pFanin = Ivy_ObjFanin1(pObj);
00192         if ( pFanin == NULL )
00193             continue;
00194         Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
00195             if ( pFanout == pObj )
00196                 break;
00197         if ( k == Vec_PtrSize(vFanouts) )
00198         {
00199             printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
00200             RetValue = 0;
00201         }
00202         // check that the previous fanout has the same fanin
00203         if ( pObj->pPrevFan0 )
00204         {
00205             if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
00206                  Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && 
00207                  Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
00208                  Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
00209             {
00210                 printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
00211                 RetValue = 0;
00212             }
00213         }
00214         // check that the previous fanout has the same fanin
00215         if ( pObj->pPrevFan1 )
00216         {
00217             if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
00218                  Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && 
00219                  Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
00220                  Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
00221             {
00222                 printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
00223                 RetValue = 0;
00224             }
00225         }
00226     }
00227     // make sure every fanout is a fanin
00228     Ivy_ManForEachObj( p, pObj, i )
00229     {
00230         Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
00231             if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
00232             {
00233                 printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
00234                 RetValue = 0;
00235             }
00236     }
00237     Vec_PtrFree( vFanouts );
00238     return RetValue;
00239 }

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