| /**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" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// 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 /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
