ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
aigCheck.c File Reference
#include "aig.h"
Include dependency graph for aigCheck.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Aig_ManCheck (Aig_Man_t *p)
 DECLARATIONS ///.
 
void Aig_ManCheckMarkA (Aig_Man_t *p)
 
void Aig_ManCheckPhase (Aig_Man_t *p)
 

Function Documentation

◆ Aig_ManCheck()

ABC_NAMESPACE_IMPL_START int Aig_ManCheck ( Aig_Man_t * p)

DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

CFile****************************************************************

FileName [aigCheck.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [AIG checking procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
aigCheck.c,v 1.00 2007/04/28 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 aigCheck.c.

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}
#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
#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
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_ManCheckMarkA()

void Aig_ManCheckMarkA ( Aig_Man_t * p)

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

Synopsis [Checks if the markA is reset.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file aigCheck.c.

133{
134 Aig_Obj_t * pObj;
135 int i;
136 Aig_ManForEachObj( p, pObj, i )
137 assert( pObj->fMarkA == 0 );
138}
unsigned int fMarkA
Definition aig.h:79
#define assert(ex)
Definition util_old.h:213

◆ Aig_ManCheckPhase()

void Aig_ManCheckPhase ( Aig_Man_t * p)

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

Synopsis [Checks the consistency of phase assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file aigCheck.c.

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}
unsigned int fPhase
Definition aig.h:78
Here is the caller graph for this function: