1 /**CFile****************************************************************
2
3 FileName [abcCheck.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Consistency checking procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "abc.h"
22 #include "base/main/main.h"
23
24 #ifdef ABC_USE_CUDD
25 #include "bdd/extrab/extraBdd.h"
26 #endif
27
28 ABC_NAMESPACE_IMPL_START
29
30
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 static int Abc_NtkCheckNames( Abc_Ntk_t * pNtk );
36 static int Abc_NtkCheckPis( Abc_Ntk_t * pNtk );
37 static int Abc_NtkCheckPos( Abc_Ntk_t * pNtk );
38 //static int Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
39 static int Abc_NtkCheckNet( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
40 static int Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
41 static int Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch );
42
43 static int Abc_NtkComparePis( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
44 static int Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
45 static int Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
46
Abc_ObjNameNet(Abc_Obj_t * pObj)47 static inline char * Abc_ObjNameNet( Abc_Obj_t * pObj ) { return (Abc_ObjIsNode(pObj) && Abc_NtkIsNetlist(pObj->pNtk)) ? Abc_ObjName(Abc_ObjFanout0(pObj)) : Abc_ObjName(pObj); }
48
49 ////////////////////////////////////////////////////////////////////////
50 /// FUNCTION DEFINITIONS ///
51 ////////////////////////////////////////////////////////////////////////
52
53 /**Function*************************************************************
54
55 Synopsis [Checks the integrity of the network.]
56
57 Description []
58
59 SideEffects []
60
61 SeeAlso []
62
63 ***********************************************************************/
Abc_NtkCheck(Abc_Ntk_t * pNtk)64 int Abc_NtkCheck( Abc_Ntk_t * pNtk )
65 {
66 return !Abc_FrameIsFlagEnabled( "check" ) || Abc_NtkDoCheck( pNtk );
67 }
68
69 /**Function*************************************************************
70
71 Synopsis [Checks the integrity of the network after reading.]
72
73 Description []
74
75 SideEffects []
76
77 SeeAlso []
78
79 ***********************************************************************/
Abc_NtkCheckRead(Abc_Ntk_t * pNtk)80 int Abc_NtkCheckRead( Abc_Ntk_t * pNtk )
81 {
82 return !Abc_FrameIsFlagEnabled( "checkread" ) || Abc_NtkDoCheck( pNtk );
83 }
84
85 /**Function*************************************************************
86
87 Synopsis [Checks the integrity of the network.]
88
89 Description []
90
91 SideEffects []
92
93 SeeAlso []
94
95 ***********************************************************************/
Abc_NtkDoCheck(Abc_Ntk_t * pNtk)96 int Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
97 {
98 Abc_Obj_t * pObj, * pNet, * pNode;
99 int i;
100
101 // check network types
102 if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
103 {
104 fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
105 return 0;
106 }
107 if ( !Abc_NtkHasSop(pNtk) && !Abc_NtkHasBdd(pNtk) && !Abc_NtkHasAig(pNtk) && !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasBlackbox(pNtk) )
108 {
109 fprintf( stdout, "NetworkCheck: Unknown functionality type.\n" );
110 return 0;
111 }
112 if ( Abc_NtkHasMapping(pNtk) )
113 {
114 if ( pNtk->pManFunc != Abc_FrameReadLibGen() )
115 {
116 fprintf( stdout, "NetworkCheck: The library of the mapped network is not the global library.\n" );
117 return 0;
118 }
119 }
120
121 if ( Abc_NtkHasOnlyLatchBoxes(pNtk) )
122 {
123 // check CI/CO numbers
124 if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) )
125 {
126 fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
127 fprintf( stdout, "One possible reason is that latches are added twice:\n" );
128 fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" );
129 return 0;
130 }
131 if ( Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
132 {
133 fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
134 fprintf( stdout, "One possible reason is that latches are added twice:\n" );
135 fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" );
136 return 0;
137 }
138 }
139
140 // check the names
141 if ( !Abc_NtkCheckNames( pNtk ) )
142 return 0;
143
144 // check PIs and POs
145 Abc_NtkCleanCopy( pNtk );
146 if ( !Abc_NtkCheckPis( pNtk ) )
147 return 0;
148 if ( !Abc_NtkCheckPos( pNtk ) )
149 return 0;
150
151 if ( Abc_NtkHasBlackbox(pNtk) )
152 return 1;
153
154 // check the connectivity of objects
155 Abc_NtkForEachObj( pNtk, pObj, i )
156 if ( !Abc_NtkCheckObj( pNtk, pObj ) )
157 return 0;
158
159 // if it is a netlist change nets and latches
160 if ( Abc_NtkIsNetlist(pNtk) )
161 {
162 if ( Abc_NtkNetNum(pNtk) == 0 )
163 fprintf( stdout, "NetworkCheck: Warning! Netlist has no nets.\n" );
164 // check the nets
165 Abc_NtkForEachNet( pNtk, pNet, i )
166 if ( !Abc_NtkCheckNet( pNtk, pNet ) )
167 return 0;
168 }
169 else
170 {
171 if ( Abc_NtkNetNum(pNtk) != 0 )
172 {
173 fprintf( stdout, "NetworkCheck: A network that is not a netlist has nets.\n" );
174 return 0;
175 }
176 }
177
178 // check the nodes
179 if ( Abc_NtkIsStrash(pNtk) )
180 Abc_AigCheck( (Abc_Aig_t *)pNtk->pManFunc );
181 else
182 {
183 Abc_NtkForEachNode( pNtk, pNode, i )
184 if ( !Abc_NtkCheckNode( pNtk, pNode ) )
185 return 0;
186 }
187
188 // check the latches
189 Abc_NtkForEachLatch( pNtk, pNode, i )
190 if ( !Abc_NtkCheckLatch( pNtk, pNode ) )
191 return 0;
192
193 // finally, check for combinational loops
194 // clk = Abc_Clock();
195 if ( !Abc_NtkIsAcyclic( pNtk ) )
196 {
197 fprintf( stdout, "NetworkCheck: Network contains a combinational loop.\n" );
198 return 0;
199 }
200 // ABC_PRT( "Acyclic ", Abc_Clock() - clk );
201
202 // check the EXDC network if present
203 if ( pNtk->pExdc )
204 Abc_NtkCheck( pNtk->pExdc );
205 /*
206 // check the hierarchy
207 if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
208 {
209 stmm_generator * gen;
210 Abc_Ntk_t * pNtkTemp;
211 char * pName;
212 // check other networks
213 stmm_foreach_item( pNtk->tName2Model, gen, &pName, (char **)&pNtkTemp )
214 {
215 pNtkTemp->fHiePath = pNtkTemp->fHieVisited = 0;
216 if ( !Abc_NtkCheck( pNtkTemp ) )
217 return 0;
218 }
219 // check acyclic dependency of the models
220 if ( !Abc_NtkIsAcyclicHierarchy( pNtk ) )
221 {
222 fprintf( stdout, "NetworkCheck: Network hierarchical dependences contains a cycle.\n" );
223 return 0;
224 }
225 }
226 */
227 return 1;
228 }
229
230 /**Function*************************************************************
231
232 Synopsis [Checks the names.]
233
234 Description []
235
236 SideEffects []
237
238 SeeAlso []
239
240 ***********************************************************************/
Abc_NtkCheckNames(Abc_Ntk_t * pNtk)241 int Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
242 {
243 Abc_Obj_t * pObj = NULL; // Ensure pObj isn't used uninitialized.
244 Vec_Int_t * vNameIds;
245 char * pName;
246 int i, NameId;
247
248 if ( Abc_NtkIsNetlist(pNtk) )
249 return 1;
250
251 // check that each CI/CO has a name
252 Abc_NtkForEachCi( pNtk, pObj, i )
253 {
254 pObj = Abc_ObjFanout0Ntk(pObj);
255 if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
256 {
257 fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id );
258 return 0;
259 }
260 }
261 Abc_NtkForEachCo( pNtk, pObj, i )
262 {
263 pObj = Abc_ObjFanin0Ntk(pObj);
264 if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
265 {
266 fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id );
267 return 0;
268 }
269 }
270
271 assert(pObj); // pObj should point to something here.
272
273 // return the array of all IDs, which have names
274 vNameIds = Nm_ManReturnNameIds( pNtk->pManName );
275 // make sure that these IDs correspond to live objects
276 Vec_IntForEachEntry( vNameIds, NameId, i )
277 {
278 if ( Vec_PtrEntry( pNtk->vObjs, NameId ) == NULL )
279 {
280 Vec_IntFree( vNameIds );
281 pName = Nm_ManFindNameById(pObj->pNtk->pManName, NameId);
282 fprintf( stdout, "NetworkCheck: Object with ID %d is deleted but its name \"%s\" remains in the name table.\n", NameId, pName );
283 return 0;
284 }
285 }
286 Vec_IntFree( vNameIds );
287
288 // make sure the CI names are unique
289 if ( !Abc_NtkCheckUniqueCiNames(pNtk) )
290 return 0;
291
292 // make sure the CO names are unique
293 if ( !Abc_NtkCheckUniqueCoNames(pNtk) )
294 return 0;
295
296 // make sure that if a CO has the same name as a CI, they point directly
297 if ( !Abc_NtkCheckUniqueCioNames(pNtk) )
298 return 0;
299
300 return 1;
301 }
302
303
304 /**Function*************************************************************
305
306 Synopsis [Checks the PIs of the network.]
307
308 Description []
309
310 SideEffects []
311
312 SeeAlso []
313
314 ***********************************************************************/
Abc_NtkCheckPis(Abc_Ntk_t * pNtk)315 int Abc_NtkCheckPis( Abc_Ntk_t * pNtk )
316 {
317 Abc_Obj_t * pObj;
318 int i;
319
320 // check that PIs are indeed PIs
321 Abc_NtkForEachPi( pNtk, pObj, i )
322 {
323 if ( !Abc_ObjIsPi(pObj) )
324 {
325 fprintf( stdout, "NetworkCheck: Object \"%s\" (id=%d) is in the PI list but is not a PI.\n", Abc_ObjName(pObj), pObj->Id );
326 return 0;
327 }
328 if ( pObj->pData )
329 {
330 fprintf( stdout, "NetworkCheck: A PI \"%s\" has a logic function.\n", Abc_ObjName(pObj) );
331 return 0;
332 }
333 if ( Abc_ObjFaninNum(pObj) > 0 )
334 {
335 fprintf( stdout, "NetworkCheck: A PI \"%s\" has fanins.\n", Abc_ObjName(pObj) );
336 return 0;
337 }
338 pObj->pCopy = (Abc_Obj_t *)1;
339 }
340 Abc_NtkForEachObj( pNtk, pObj, i )
341 {
342 if ( pObj->pCopy == NULL && Abc_ObjIsPi(pObj) )
343 {
344 fprintf( stdout, "NetworkCheck: Object \"%s\" (id=%d) is a PI but is not in the PI list.\n", Abc_ObjName(pObj), pObj->Id );
345 return 0;
346 }
347 pObj->pCopy = NULL;
348 }
349 return 1;
350 }
351
352 /**Function*************************************************************
353
354 Synopsis [Checks the POs of the network.]
355
356 Description []
357
358 SideEffects []
359
360 SeeAlso []
361
362 ***********************************************************************/
Abc_NtkCheckPos(Abc_Ntk_t * pNtk)363 int Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
364 {
365 Abc_Obj_t * pObj;
366 int i;
367
368 // check that POs are indeed POs
369 Abc_NtkForEachPo( pNtk, pObj, i )
370 {
371 if ( !Abc_ObjIsPo(pObj) )
372 {
373 fprintf( stdout, "NetworkCheck: Net \"%s\" (id=%d) is in the PO list but is not a PO.\n", Abc_ObjName(pObj), pObj->Id );
374 return 0;
375 }
376 if ( pObj->pData )
377 {
378 fprintf( stdout, "NetworkCheck: A PO \"%s\" has a logic function.\n", Abc_ObjName(pObj) );
379 return 0;
380 }
381 if ( Abc_ObjFaninNum(pObj) != 1 )
382 {
383 fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin (but %d).\n", Abc_ObjName(pObj), Abc_ObjFaninNum(pObj) );
384 return 0;
385 }
386 if ( Abc_ObjFanoutNum(pObj) > 0 )
387 {
388 fprintf( stdout, "NetworkCheck: A PO \"%s\" has %d fanout(s).\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
389 return 0;
390 }
391 pObj->pCopy = (Abc_Obj_t *)1;
392 }
393 Abc_NtkForEachObj( pNtk, pObj, i )
394 {
395 if ( pObj->pCopy == NULL && Abc_ObjIsPo(pObj) )
396 {
397 fprintf( stdout, "NetworkCheck: Net \"%s\" (id=%d) is in a PO but is not in the PO list.\n", Abc_ObjName(pObj), pObj->Id );
398 return 0;
399 }
400 pObj->pCopy = NULL;
401 }
402 return 1;
403 }
404
405
406 /**Function*************************************************************
407
408 Synopsis [Checks the connectivity of the object.]
409
410 Description []
411
412 SideEffects []
413
414 SeeAlso []
415
416 ***********************************************************************/
Abc_NtkCheckObj(Abc_Ntk_t * pNtk,Abc_Obj_t * pObj)417 int Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
418 {
419 Abc_Obj_t * pFanin, * pFanout;
420 int Value = 1;
421 int i, k;
422
423 // check the network
424 if ( pObj->pNtk != pNtk )
425 {
426 fprintf( stdout, "NetworkCheck: Object \"%s\" does not belong to the network.\n", Abc_ObjName(pObj) );
427 return 0;
428 }
429 // check the object ID
430 if ( pObj->Id < 0 || (int)pObj->Id >= Abc_NtkObjNumMax(pNtk) )
431 {
432 fprintf( stdout, "NetworkCheck: Object \"%s\" has incorrect ID.\n", Abc_ObjName(pObj) );
433 return 0;
434 }
435
436 if ( !Abc_FrameIsFlagEnabled("checkfio") )
437 return Value;
438
439 // go through the fanins of the object and make sure fanins have this object as a fanout
440 Abc_ObjForEachFanin( pObj, pFanin, i )
441 {
442 if ( Vec_IntFind( &pFanin->vFanouts, pObj->Id ) == -1 )
443 {
444 fprintf( stdout, "NodeCheck: Object \"%s\" has fanin ", Abc_ObjName(pObj) );
445 fprintf( stdout, "\"%s\" but the fanin does not have it as a fanout.\n", Abc_ObjName(pFanin) );
446 Value = 0;
447 }
448 }
449 // go through the fanouts of the object and make sure fanouts have this object as a fanin
450 Abc_ObjForEachFanout( pObj, pFanout, i )
451 {
452 if ( Vec_IntFind( &pFanout->vFanins, pObj->Id ) == -1 )
453 {
454 fprintf( stdout, "NodeCheck: Object \"%s\" has fanout ", Abc_ObjName(pObj) );
455 fprintf( stdout, "\"%s\" but the fanout does not have it as a fanin.\n", Abc_ObjName(pFanout) );
456 Value = 0;
457 }
458 }
459
460 // make sure fanins are not duplicated
461 for ( i = 0; i < pObj->vFanins.nSize; i++ )
462 for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
463 if ( pObj->vFanins.pArray[k] == pObj->vFanins.pArray[i] )
464 {
465 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
466 printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) );
467 }
468
469 // save time: do not check large fanout lists
470 if ( pObj->vFanouts.nSize > 100 )
471 return Value;
472
473 // make sure fanouts are not duplicated
474 for ( i = 0; i < pObj->vFanouts.nSize; i++ )
475 for ( k = i + 1; k < pObj->vFanouts.nSize; k++ )
476 if ( pObj->vFanouts.pArray[k] == pObj->vFanouts.pArray[i] )
477 {
478 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
479 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
480 }
481
482 return Value;
483 }
484
485 /**Function*************************************************************
486
487 Synopsis [Checks the integrity of a net.]
488
489 Description []
490
491 SideEffects []
492
493 SeeAlso []
494
495 ***********************************************************************/
Abc_NtkCheckNet(Abc_Ntk_t * pNtk,Abc_Obj_t * pNet)496 int Abc_NtkCheckNet( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
497 {
498 if ( Abc_ObjFaninNum(pNet) == 0 )
499 {
500 fprintf( stdout, "NetworkCheck: Net \"%s\" is not driven.\n", Abc_ObjName(pNet) );
501 return 0;
502 }
503 if ( Abc_ObjFaninNum(pNet) > 1 )
504 {
505 fprintf( stdout, "NetworkCheck: Net \"%s\" has more than one driver.\n", Abc_ObjName(pNet) );
506 return 0;
507 }
508 return 1;
509 }
510
511 /**Function*************************************************************
512
513 Synopsis [Checks the integrity of a node.]
514
515 Description []
516
517 SideEffects []
518
519 SeeAlso []
520
521 ***********************************************************************/
Abc_NtkCheckNode(Abc_Ntk_t * pNtk,Abc_Obj_t * pNode)522 int Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
523 {
524 // detect internal nodes that do not have nets
525 if ( Abc_NtkIsNetlist(pNtk) && Abc_ObjFanoutNum(pNode) == 0 )
526 {
527 fprintf( stdout, "Node (id = %d) has no net to drive.\n", pNode->Id );
528 return 0;
529 }
530 // the node should have a function assigned unless it is an AIG
531 if ( pNode->pData == NULL )
532 {
533 if ( Abc_ObjIsBarBuf(pNode) )
534 return 1;
535 fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_ObjNameNet(pNode) );
536 return 0;
537 }
538 // the netlist and SOP logic network should have SOPs
539 if ( Abc_NtkHasSop(pNtk) )
540 {
541 if ( !Abc_SopCheck( (char *)pNode->pData, Abc_ObjFaninNum(pNode) ) )
542 {
543 fprintf( stdout, "NodeCheck: SOP check for node \"%s\" has failed.\n", Abc_ObjNameNet(pNode) );
544 return 0;
545 }
546 }
547 else if ( Abc_NtkHasBdd(pNtk) )
548 {
549 #ifdef ABC_USE_CUDD
550 int nSuppSize = Cudd_SupportSize((DdManager *)pNtk->pManFunc, (DdNode *)pNode->pData);
551 if ( nSuppSize > Abc_ObjFaninNum(pNode) )
552 {
553 fprintf( stdout, "NodeCheck: BDD of the node \"%s\" has incorrect support size.\n", Abc_ObjNameNet(pNode) );
554 return 0;
555 }
556 #endif
557 }
558 else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasAig(pNtk) )
559 {
560 assert( 0 );
561 }
562 return 1;
563 }
564
565 /**Function*************************************************************
566
567 Synopsis [Checks the integrity of a latch.]
568
569 Description []
570
571 SideEffects []
572
573 SeeAlso []
574
575 ***********************************************************************/
Abc_NtkCheckLatch(Abc_Ntk_t * pNtk,Abc_Obj_t * pLatch)576 int Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
577 {
578 int Value = 1;
579 // check whether the object is a latch
580 if ( !Abc_ObjIsLatch(pLatch) )
581 {
582 fprintf( stdout, "NodeCheck: Latch \"%s\" is in a latch list but is not a latch.\n", Abc_ObjName(pLatch) );
583 Value = 0;
584 }
585 // make sure the latch has a reasonable return value
586 if ( (int)(ABC_PTRINT_T)pLatch->pData < ABC_INIT_ZERO || (int)(ABC_PTRINT_T)pLatch->pData > ABC_INIT_DC )
587 {
588 fprintf( stdout, "NodeCheck: Latch \"%s\" has incorrect reset value (%d).\n",
589 Abc_ObjName(pLatch), (int)(ABC_PTRINT_T)pLatch->pData );
590 Value = 0;
591 }
592 // make sure the latch has only one fanin
593 if ( Abc_ObjFaninNum(pLatch) != 1 )
594 {
595 fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanins.\n", Abc_ObjName(pLatch), Abc_ObjFaninNum(pLatch) );
596 Value = 0;
597 }
598 // make sure the latch has only one fanout
599 if ( Abc_ObjFanoutNum(pLatch) != 1 )
600 {
601 fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanouts.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) );
602 Value = 0;
603 }
604 // make sure the latch input has only one fanin
605 if ( Abc_ObjFaninNum(Abc_ObjFanin0(pLatch)) != 1 )
606 {
607 fprintf( stdout, "NodeCheck: Input of latch \"%s\" has wrong number (%d) of fanins.\n",
608 Abc_ObjName(Abc_ObjFanin0(pLatch)), Abc_ObjFaninNum(Abc_ObjFanin0(pLatch)) );
609 Value = 0;
610 }
611 // make sure the latch input has only one fanout
612 if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pLatch)) != 1 )
613 {
614 fprintf( stdout, "NodeCheck: Input of latch \"%s\" has wrong number (%d) of fanouts.\n",
615 Abc_ObjName(Abc_ObjFanin0(pLatch)), Abc_ObjFanoutNum(Abc_ObjFanin0(pLatch)) );
616 Value = 0;
617 }
618 // make sure the latch output has only one fanin
619 if ( Abc_ObjFaninNum(Abc_ObjFanout0(pLatch)) != 1 )
620 {
621 fprintf( stdout, "NodeCheck: Output of latch \"%s\" has wrong number (%d) of fanins.\n",
622 Abc_ObjName(Abc_ObjFanout0(pLatch)), Abc_ObjFaninNum(Abc_ObjFanout0(pLatch)) );
623 Value = 0;
624 }
625 return Value;
626 }
627
628
629
630
631 /**Function*************************************************************
632
633 Synopsis [Compares the PIs of the two networks.]
634
635 Description []
636
637 SideEffects []
638
639 SeeAlso []
640
641 ***********************************************************************/
Abc_NtkComparePis(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fComb)642 int Abc_NtkComparePis( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
643 {
644 Abc_Obj_t * pObj1;
645 int i;
646 if ( Abc_NtkPiNum(pNtk1) != Abc_NtkPiNum(pNtk2) )
647 {
648 printf( "Networks have different number of primary inputs.\n" );
649 return 0;
650 }
651 // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
652 Abc_NtkForEachPi( pNtk1, pObj1, i )
653 {
654 if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPi(pNtk2,i)) ) != 0 )
655 {
656 printf( "Primary input #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n",
657 i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPi(pNtk2,i)) );
658 return 0;
659 }
660 }
661 return 1;
662 }
663
664 /**Function*************************************************************
665
666 Synopsis [Compares the POs of the two networks.]
667
668 Description []
669
670 SideEffects []
671
672 SeeAlso []
673
674 ***********************************************************************/
Abc_NtkComparePos(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fComb)675 int Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
676 {
677 Abc_Obj_t * pObj1;
678 int i;
679 if ( Abc_NtkPoNum(pNtk1) != Abc_NtkPoNum(pNtk2) )
680 {
681 printf( "Networks have different number of primary outputs.\n" );
682 return 0;
683 }
684 // for each PO of pNet1 find corresponding PO of pNet2 and reorder them
685 Abc_NtkForEachPo( pNtk1, pObj1, i )
686 {
687 if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) ) != 0 )
688 {
689 printf( "Primary output #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n",
690 i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) );
691 return 0;
692 }
693 }
694 return 1;
695 }
696
697 /**Function*************************************************************
698
699 Synopsis [Compares the latches of the two networks.]
700
701 Description []
702
703 SideEffects []
704
705 SeeAlso []
706
707 ***********************************************************************/
Abc_NtkCompareBoxes(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fComb)708 int Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
709 {
710 Abc_Obj_t * pObj1;
711 int i;
712 assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
713 assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
714 if ( !fComb )
715 return 1;
716 if ( Abc_NtkBoxNum(pNtk1) != Abc_NtkBoxNum(pNtk2) )
717 {
718 printf( "Networks have different number of latches.\n" );
719 return 0;
720 }
721 // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
722 Abc_NtkForEachBox( pNtk1, pObj1, i )
723 {
724 if ( strcmp( Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) ) != 0 )
725 {
726 printf( "Box #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n",
727 i, Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) );
728 return 0;
729 }
730 }
731 return 1;
732 }
733
734 /**Function*************************************************************
735
736 Synopsis [Compares the signals of the networks.]
737
738 Description []
739
740 SideEffects [Ordering POs by name is a very bad idea! It destroys
741 the natural order of the logic in the circuit.]
742
743 SeeAlso []
744
745 ***********************************************************************/
Abc_NtkCompareSignals(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fOnlyPis,int fComb)746 int Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb )
747 {
748 Abc_NtkOrderObjsByName( pNtk1, fComb );
749 Abc_NtkOrderObjsByName( pNtk2, fComb );
750 if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) )
751 return 0;
752 if ( !fOnlyPis )
753 {
754 if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) )
755 return 0;
756 if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) )
757 return 0;
758 }
759 return 1;
760 }
761
762 /**Function*************************************************************
763
764 Synopsis [Returns 0 if the network hierachy contains a cycle.]
765
766 Description []
767
768 SideEffects []
769
770 SeeAlso []
771
772 ***********************************************************************/
Abc_NtkIsAcyclicHierarchy_rec(Abc_Ntk_t * pNtk)773 int Abc_NtkIsAcyclicHierarchy_rec( Abc_Ntk_t * pNtk )
774 {
775 Abc_Ntk_t * pNtkNext;
776 Abc_Obj_t * pObj;
777 int i;
778 // return if visited
779 if ( pNtk->fHieVisited )
780 return 1;
781 pNtk->fHieVisited = 1;
782 // return if black box
783 if ( Abc_NtkHasBlackbox(pNtk) )
784 return 1;
785 assert( Abc_NtkIsNetlist(pNtk) );
786 // go through all the children networks
787 Abc_NtkForEachBox( pNtk, pObj, i )
788 {
789 if ( Abc_ObjIsLatch(pObj) )
790 continue;
791 pNtkNext = (Abc_Ntk_t *)pObj->pData;
792 assert( pNtkNext != NULL );
793 if ( pNtkNext->fHiePath )
794 return 0;
795 pNtk->fHiePath = 1;
796 if ( !Abc_NtkIsAcyclicHierarchy_rec( pNtkNext ) )
797 return 0;
798 pNtk->fHiePath = 0;
799 }
800 return 1;
801 }
802
803 /**Function*************************************************************
804
805 Synopsis [Returns 0 if the network hierachy contains a cycle.]
806
807 Description []
808
809 SideEffects []
810
811 SeeAlso []
812
813 ***********************************************************************/
Abc_NtkIsAcyclicHierarchy(Abc_Ntk_t * pNtk)814 int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk )
815 {
816 Abc_Ntk_t * pTemp;
817 int i, RetValue;
818 assert( Abc_NtkIsNetlist(pNtk) && pNtk->pDesign );
819 // clear the modules
820 Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
821 pTemp->fHieVisited = pTemp->fHiePath = 0;
822 // traverse
823 pNtk->fHiePath = 1;
824 RetValue = Abc_NtkIsAcyclicHierarchy_rec( pNtk );
825 pNtk->fHiePath = 0;
826 // clear the modules
827 Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pTemp, i )
828 pTemp->fHieVisited = pTemp->fHiePath = 0;
829 return RetValue;
830 }
831
832 /**Function*************************************************************
833
834 Synopsis [Returns 0 if CI names are repeated.]
835
836 Description []
837
838 SideEffects []
839
840 SeeAlso []
841
842 ***********************************************************************/
Abc_NtkNamesCompare(char ** pName1,char ** pName2)843 int Abc_NtkNamesCompare( char ** pName1, char ** pName2 )
844 {
845 return strcmp( *pName1, *pName2 );
846 }
847
848 /**Function*************************************************************
849
850 Synopsis [Returns 0 if CI names are repeated.]
851
852 Description []
853
854 SideEffects []
855
856 SeeAlso []
857
858 ***********************************************************************/
Abc_NtkCheckUniqueCiNames(Abc_Ntk_t * pNtk)859 int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk )
860 {
861 Vec_Ptr_t * vNames;
862 Abc_Obj_t * pObj;
863 int i, fRetValue = 1;
864 assert( !Abc_NtkIsNetlist(pNtk) );
865 vNames = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
866 Abc_NtkForEachCi( pNtk, pObj, i )
867 Vec_PtrPush( vNames, Abc_ObjName(pObj) );
868 Vec_PtrSort( vNames, (int (*)())Abc_NtkNamesCompare );
869 for ( i = 1; i < Abc_NtkCiNum(pNtk); i++ )
870 if ( !strcmp( (const char *)Vec_PtrEntry(vNames,i-1), (const char *)Vec_PtrEntry(vNames,i) ) )
871 {
872 printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", (char*)Vec_PtrEntry(vNames,i-1), (char*)Vec_PtrEntry(vNames,i) );
873 fRetValue = 0;
874 }
875 Vec_PtrFree( vNames );
876 return fRetValue;
877 }
878
879 /**Function*************************************************************
880
881 Synopsis [Returns 0 if CO names are repeated.]
882
883 Description []
884
885 SideEffects []
886
887 SeeAlso []
888
889 ***********************************************************************/
Abc_NtkCheckUniqueCoNames(Abc_Ntk_t * pNtk)890 int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk )
891 {
892 Vec_Ptr_t * vNames;
893 Abc_Obj_t * pObj;
894 int i, fRetValue = 1;
895 assert( !Abc_NtkIsNetlist(pNtk) );
896 vNames = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
897 Abc_NtkForEachCo( pNtk, pObj, i )
898 Vec_PtrPush( vNames, Abc_ObjName(pObj) );
899 Vec_PtrSort( vNames, (int (*)())Abc_NtkNamesCompare );
900 for ( i = 1; i < Abc_NtkCoNum(pNtk); i++ )
901 {
902 // printf( "%s\n", Vec_PtrEntry(vNames,i) );
903 if ( !strcmp( (const char *)Vec_PtrEntry(vNames,i-1), (const char *)Vec_PtrEntry(vNames,i) ) )
904 {
905 printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", (char*)Vec_PtrEntry(vNames,i-1), (char*)Vec_PtrEntry(vNames,i) );
906 fRetValue = 0;
907 }
908 }
909 Vec_PtrFree( vNames );
910 return fRetValue;
911 }
912
913 /**Function*************************************************************
914
915 Synopsis [Returns 0 if there is a pair of CI/CO with the same name and logic in between.]
916
917 Description []
918
919 SideEffects []
920
921 SeeAlso []
922
923 ***********************************************************************/
Abc_NtkCheckUniqueCioNames(Abc_Ntk_t * pNtk)924 int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
925 {
926 Abc_Obj_t * pObj, * pObjCi, * pFanin;
927 int i, nCiId, fRetValue = 1;
928 assert( !Abc_NtkIsNetlist(pNtk) );
929 Abc_NtkForEachCo( pNtk, pObj, i )
930 {
931 nCiId = Nm_ManFindIdByNameTwoTypes( pNtk->pManName, Abc_ObjName(pObj), ABC_OBJ_PI, ABC_OBJ_BO );
932 if ( nCiId == -1 )
933 continue;
934 pObjCi = Abc_NtkObj( pNtk, nCiId );
935 assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) );
936 pFanin = Abc_ObjFanin0(pObj);
937 if ( pFanin != pObjCi )
938 {
939 printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly. The name of the CO fanin is %s.\n",
940 Abc_ObjName(pObj), Abc_ObjName(Abc_ObjFanin0(pObj)) );
941 fRetValue = 0;
942 }
943 }
944 return fRetValue;
945 }
946
947 ////////////////////////////////////////////////////////////////////////
948 /// END OF FILE ///
949 ////////////////////////////////////////////////////////////////////////
950
951
952 ABC_NAMESPACE_IMPL_END
953
954