ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
aigCheck.c
Go to the documentation of this file.
1
20
21#include "aig.h"
22
24
25
29
33
46{
47 Aig_Obj_t * pObj, * pObj2;
48 int i;
49 // check primary inputs
50 Aig_ManForEachCi( p, pObj, i )
51 {
52 if ( Aig_ObjFanin0(pObj) || Aig_ObjFanin1(pObj) )
53 {
54 printf( "Aig_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
55 return 0;
56 }
57 }
58 // check primary outputs
59 Aig_ManForEachCo( p, pObj, i )
60 {
61 if ( !Aig_ObjFanin0(pObj) )
62 {
63 printf( "Aig_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
64 return 0;
65 }
66 if ( Aig_ObjFanin1(pObj) )
67 {
68 printf( "Aig_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
69 return 0;
70 }
71 }
72 // check internal nodes
73 Aig_ManForEachObj( p, pObj, i )
74 {
75 if ( !Aig_ObjIsNode(pObj) )
76 continue;
77 if ( !Aig_ObjFanin0(pObj) || !Aig_ObjFanin1(pObj) )
78 {
79 printf( "Aig_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
80 return 0;
81 }
82 if ( Aig_ObjFanin0(pObj)->Id >= Aig_ObjFanin1(pObj)->Id )
83 {
84 printf( "Aig_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
85 return 0;
86 }
87 pObj2 = Aig_TableLookup( p, pObj );
88 if ( pObj2 != pObj )
89 {
90 printf( "Aig_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
91 return 0;
92 }
93 }
94 // count the total number of nodes
95 if ( Aig_ManObjNum(p) != 1 + Aig_ManCiNum(p) + Aig_ManCoNum(p) +
96 Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) )
97 {
98 printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
99 printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Total = %d.\n",
100 1, Aig_ManCiNum(p), Aig_ManCoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p),
101 1 + Aig_ManCiNum(p) + Aig_ManCoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) );
102 printf( "Created = %d. Deleted = %d. Existing = %d.\n",
103 Aig_ManObjNumMax(p), p->nDeleted, Aig_ManObjNum(p) );
104 return 0;
105 }
106 // count the number of nodes in the table
107 if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) )
108 {
109 printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
110 printf( "Entries = %d. And = %d. Xor = %d. Total = %d.\n",
111 Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p),
112 Aig_ManAndNum(p) + Aig_ManExorNum(p) );
113
114 return 0;
115 }
116// if ( !Aig_ManIsAcyclic(p) )
117// return 0;
118 return 1;
119}
120
133{
134 Aig_Obj_t * pObj;
135 int i;
136 Aig_ManForEachObj( p, pObj, i )
137 assert( pObj->fMarkA == 0 );
138}
139
152{
153 Aig_Obj_t * pObj;
154 int i;
155 Aig_ManForEachObj( p, pObj, i )
156 if ( Aig_ObjIsCi(pObj) )
157 assert( (int)pObj->fPhase == 0 );
158 else
159 assert( (int)pObj->fPhase == (Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) & Aig_ObjPhaseReal(Aig_ObjChild1(pObj))) );
160}
161
165
166
168
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START int Aig_ManCheck(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigCheck.c:45
void Aig_ManCheckPhase(Aig_Man_t *p)
Definition aigCheck.c:151
void Aig_ManCheckMarkA(Aig_Man_t *p)
Definition aigCheck.c:132
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_Obj_t * Aig_TableLookup(Aig_Man_t *p, Aig_Obj_t *pGhost)
Definition aigTable.c:116
int Aig_TableCountEntries(Aig_Man_t *p)
Definition aigTable.c:218
Cube * p
Definition exorList.c:222
unsigned int fMarkA
Definition aig.h:79
unsigned int fPhase
Definition aig.h:78
#define assert(ex)
Definition util_old.h:213