abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
ivyCheck.c File Reference
#include "ivy.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Ivy_ManCheck (Ivy_Man_t *p)
 DECLARATIONS ///. More...
 
int Ivy_ManCheckFanoutNums (Ivy_Man_t *p)
 
int Ivy_ManCheckFanouts (Ivy_Man_t *p)
 
int Ivy_ManCheckChoices (Ivy_Man_t *p)
 

Function Documentation

ABC_NAMESPACE_IMPL_START int Ivy_ManCheck ( Ivy_Man_t *  p)

DECLARATIONS ///.

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

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

Synopsis [Checks the consistency of the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ivyCheck.c.

46 {
47  Ivy_Obj_t * pObj, * pObj2;
48  int i;
49  Ivy_ManForEachObj( p, pObj, i )
50  {
51  // skip deleted nodes
52  if ( Ivy_ObjId(pObj) != i )
53  {
54  printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
55  return 0;
56  }
57  // consider the constant node and PIs
58  if ( i == 0 || Ivy_ObjIsPi(pObj) )
59  {
60  if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) )
61  {
62  printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id );
63  return 0;
64  }
65  continue;
66  }
67  if ( Ivy_ObjIsPo(pObj) )
68  {
69  if ( Ivy_ObjFaninId1(pObj) )
70  {
71  printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id );
72  return 0;
73  }
74  continue;
75  }
76  if ( Ivy_ObjIsBuf(pObj) )
77  {
78  if ( Ivy_ObjFanin1(pObj) )
79  {
80  printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
81  return 0;
82  }
83  continue;
84  }
85  if ( Ivy_ObjIsLatch(pObj) )
86  {
87  if ( Ivy_ObjFanin1(pObj) )
88  {
89  printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
90  return 0;
91  }
92  if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
93  {
94  printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
95  return 0;
96  }
97  pObj2 = Ivy_TableLookup( p, pObj );
98  if ( pObj2 != pObj )
99  printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
100  continue;
101  }
102  // consider the AND node
103  if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
104  {
105  printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
106  return 0;
107  }
108  if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
109  {
110  printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
111  return 0;
112  }
113  if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
114  printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
115  pObj2 = Ivy_TableLookup( p, pObj );
116  if ( pObj2 != pObj )
117  printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
118  if ( Ivy_ObjRefs(pObj) == 0 )
119  printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
120  // check fanouts
121  if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
122  printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
123  }
124  // count the number of nodes in the table
125  if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
126  {
127  printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
128  return 0;
129  }
130 // if ( !Ivy_ManCheckFanouts(p) )
131 // return 0;
132  if ( !Ivy_ManIsAcyclic(p) )
133  return 0;
134  return 1;
135 }
Ivy_ManIsAcyclic
int Ivy_ManIsAcyclic(Ivy_Man_t *p)
Definition: ivyDfs.c:373
Ivy_ObjLevelNew
static int Ivy_ObjLevelNew(Ivy_Obj_t *pObj)
Definition: ivy.h:279
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ivy_ObjFaninId1
static int Ivy_ObjFaninId1(Ivy_Obj_t *pObj)
Definition: ivy.h:268
Ivy_TableCountEntries
int Ivy_TableCountEntries(Ivy_Man_t *p)
Definition: ivyTable.c:187
Ivy_ObjIsPi
static int Ivy_ObjIsPi(Ivy_Obj_t *pObj)
Definition: ivy.h:236
Ivy_ManExorNum
static int Ivy_ManExorNum(Ivy_Man_t *p)
Definition: ivy.h:223
Ivy_ManLatchNum
static int Ivy_ManLatchNum(Ivy_Man_t *p)
Definition: ivy.h:221
Ivy_Obj_t_::Id
int Id
Definition: ivy.h:75
Ivy_ObjIsLatch
static int Ivy_ObjIsLatch(Ivy_Obj_t *pObj)
Definition: ivy.h:241
Ivy_ObjFanin1
static Ivy_Obj_t * Ivy_ObjFanin1(Ivy_Obj_t *pObj)
Definition: ivy.h:272
Ivy_ObjLevel
static int Ivy_ObjLevel(Ivy_Obj_t *pObj)
Definition: ivy.h:278
Ivy_ObjFanin0
static Ivy_Obj_t * Ivy_ObjFanin0(Ivy_Obj_t *pObj)
Definition: ivy.h:271
Ivy_ObjFaninId0
static int Ivy_ObjFaninId0(Ivy_Obj_t *pObj)
Definition: ivy.h:267
Ivy_TableLookup
Ivy_Obj_t * Ivy_TableLookup(Ivy_Man_t *p, Ivy_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: ivyTable.c:71
Ivy_ObjRefs
static int Ivy_ObjRefs(Ivy_Obj_t *pObj)
Definition: ivy.h:264
Ivy_Obj_t_
Definition: ivy.h:73
Ivy_ObjFanoutNum
int Ivy_ObjFanoutNum(Ivy_Man_t *p, Ivy_Obj_t *pObj)
Definition: ivyFanout.c:299
Ivy_ObjIsBuf
static int Ivy_ObjIsBuf(Ivy_Obj_t *pObj)
Definition: ivy.h:244
Ivy_ObjIsPo
static int Ivy_ObjIsPo(Ivy_Obj_t *pObj)
Definition: ivy.h:237
Ivy_ManAndNum
static int Ivy_ManAndNum(Ivy_Man_t *p)
Definition: ivy.h:222
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
Ivy_ObjInit
static Ivy_Init_t Ivy_ObjInit(Ivy_Obj_t *pObj)
Definition: ivy.h:232
Ivy_ObjId
static int Ivy_ObjId(Ivy_Obj_t *pObj)
Definition: ivy.h:260
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 255 of file ivyCheck.c.

256 {
257  Ivy_Obj_t * pObj, * pTemp;
258  int i;
259  Ivy_ManForEachObj( p->pHaig, pObj, i )
260  {
261  if ( Ivy_ObjRefs(pObj) == 0 )
262  continue;
263  // count the number of nodes in the loop
264  assert( !Ivy_IsComplement(pObj->pEquiv) );
265  for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
266  if ( Ivy_ObjRefs(pTemp) > 1 )
267  printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
268  }
269  return 1;
270 }
Ivy_IsComplement
static int Ivy_IsComplement(Ivy_Obj_t *p)
Definition: ivy.h:196
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ivy_Obj_t_::Id
int Id
Definition: ivy.h:75
Ivy_ObjRefs
static int Ivy_ObjRefs(Ivy_Obj_t *pObj)
Definition: ivy.h:264
Ivy_Obj_t_
Definition: ivy.h:73
Ivy_Regular
static Ivy_Obj_t * Ivy_Regular(Ivy_Obj_t *p)
Definition: ivy.h:193
assert
#define assert(ex)
Definition: util_old.h:213
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
Ivy_Obj_t_::pEquiv
Ivy_Obj_t * pEquiv
Definition: ivy.h:93
int Ivy_ManCheckFanoutNums ( Ivy_Man_t *  p)

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

Synopsis [Verifies the fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file ivyCheck.c.

149 {
150  Ivy_Obj_t * pObj;
151  int i, Counter = 0;
152  Ivy_ManForEachObj( p, pObj, i )
153  if ( Ivy_ObjIsNode(pObj) )
154  Counter += (Ivy_ObjRefs(pObj) == 0);
155  if ( Counter )
156  printf( "Sequential AIG has %d dangling nodes.\n", Counter );
157  return Counter;
158 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ivy_ObjRefs
static int Ivy_ObjRefs(Ivy_Obj_t *pObj)
Definition: ivy.h:264
if
if(last==0)
Definition: sparse_int.h:34
Ivy_Obj_t_
Definition: ivy.h:73
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ivy_ObjIsNode
static int Ivy_ObjIsNode(Ivy_Obj_t *pObj)
Definition: ivy.h:245
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
int Ivy_ManCheckFanouts ( Ivy_Man_t *  p)

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

Synopsis [Verifies the fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 171 of file ivyCheck.c.

172 {
173  Vec_Ptr_t * vFanouts;
174  Ivy_Obj_t * pObj, * pFanout, * pFanin;
175  int i, k, RetValue = 1;
176  if ( !p->fFanout )
177  return 1;
178  vFanouts = Vec_PtrAlloc( 100 );
179  // make sure every fanin is a fanout
180  Ivy_ManForEachObj( p, pObj, i )
181  {
182  pFanin = Ivy_ObjFanin0(pObj);
183  if ( pFanin == NULL )
184  continue;
185  Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
186  if ( pFanout == pObj )
187  break;
188  if ( k == Vec_PtrSize(vFanouts) )
189  {
190  printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
191  RetValue = 0;
192  }
193 
194  pFanin = Ivy_ObjFanin1(pObj);
195  if ( pFanin == NULL )
196  continue;
197  Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
198  if ( pFanout == pObj )
199  break;
200  if ( k == Vec_PtrSize(vFanouts) )
201  {
202  printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
203  RetValue = 0;
204  }
205  // check that the previous fanout has the same fanin
206  if ( pObj->pPrevFan0 )
207  {
208  if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) &&
209  Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) &&
210  Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) &&
211  Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
212  {
213  printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
214  RetValue = 0;
215  }
216  }
217  // check that the previous fanout has the same fanin
218  if ( pObj->pPrevFan1 )
219  {
220  if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) &&
221  Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) &&
222  Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) &&
223  Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
224  {
225  printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
226  RetValue = 0;
227  }
228  }
229  }
230  // make sure every fanout is a fanin
231  Ivy_ManForEachObj( p, pObj, i )
232  {
233  Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
234  if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
235  {
236  printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
237  RetValue = 0;
238  }
239  }
240  Vec_PtrFree( vFanouts );
241  return RetValue;
242 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ivy_Obj_t_::pPrevFan0
Ivy_Obj_t * pPrevFan0
Definition: ivy.h:91
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ivy_ObjForEachFanout
#define Ivy_ObjForEachFanout(p, pObj, vArray, pFanout, i)
Definition: ivy.h:411
Ivy_Obj_t_::Id
int Id
Definition: ivy.h:75
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ivy_ObjFanin1
static Ivy_Obj_t * Ivy_ObjFanin1(Ivy_Obj_t *pObj)
Definition: ivy.h:272
Ivy_ObjFanin0
static Ivy_Obj_t * Ivy_ObjFanin0(Ivy_Obj_t *pObj)
Definition: ivy.h:271
if
if(last==0)
Definition: sparse_int.h:34
Ivy_Obj_t_
Definition: ivy.h:73
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
Ivy_Obj_t_::pPrevFan1
Ivy_Obj_t * pPrevFan1
Definition: ivy.h:92
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223