summaryrefslogtreecommitdiffstats
path: root/src/aig/ivy/ivyCheck.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ivy/ivyCheck.c')
-rw-r--r--src/aig/ivy/ivyCheck.c273
1 files changed, 273 insertions, 0 deletions
diff --git a/src/aig/ivy/ivyCheck.c b/src/aig/ivy/ivyCheck.c
new file mode 100644
index 00000000..55448f19
--- /dev/null
+++ b/src/aig/ivy/ivyCheck.c
@@ -0,0 +1,273 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-07 10:06:57 +0000