diff options
Diffstat (limited to 'src/aig/ivy/ivyCheck.c')
-rw-r--r-- | src/aig/ivy/ivyCheck.c | 273 |
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 /// -//////////////////////////////////////////////////////////////////////// - - |