ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaMffc.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22
24
25
29
30static inline int Gia_ObjDom( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vDoms, Gia_ObjId(p, pObj)); }
31static inline void Gia_ObjSetDom( Gia_Man_t * p, Gia_Obj_t * pObj, int d ) { Vec_IntWriteEntry(p->vDoms, Gia_ObjId(p, pObj), d); }
32
36
49static inline void Gia_ManAddDom( Gia_Man_t * p, Gia_Obj_t * pObj, int iDom0 )
50{
51 int iDom1, iDomNext;
52 if ( Gia_ObjDom(p, pObj) == -1 )
53 {
54 Gia_ObjSetDom( p, pObj, iDom0 );
55 return;
56 }
57 iDom1 = Gia_ObjDom( p, pObj );
58 while ( 1 )
59 {
60 if ( iDom0 > iDom1 )
61 {
62 iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom1) );
63 if ( iDomNext == iDom1 )
64 break;
65 iDom1 = iDomNext;
66 continue;
67 }
68 if ( iDom1 > iDom0 )
69 {
70 iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom0) );
71 if ( iDomNext == iDom0 )
72 break;
73 iDom0 = iDomNext;
74 continue;
75 }
76 assert( iDom0 == iDom1 );
77 Gia_ObjSetDom( p, pObj, iDom0 );
78 return;
79 }
80 Gia_ObjSetDom( p, pObj, Gia_ObjId(p, pObj) );
81}
82static inline void Gia_ManComputeDoms( Gia_Man_t * p )
83{
84 Gia_Obj_t * pObj;
85 int i;
86 if ( p->vDoms == NULL )
87 p->vDoms = Vec_IntAlloc( 0 );
88 Vec_IntFill( p->vDoms, Gia_ManObjNum(p), -1 );
89 Gia_ManForEachObjReverse( p, pObj, i )
90 {
91 if ( i == 0 || Gia_ObjIsCi(pObj) )
92 continue;
93 if ( Gia_ObjIsCo(pObj) )
94 {
95 Gia_ObjSetDom( p, pObj, i );
96 Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i );
97 continue;
98 }
99 assert( Gia_ObjIsAnd(pObj) );
100 Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i );
101 Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i );
102 }
103}
104
105
117static inline int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
118{
119 Gia_Obj_t * pFanin;
120 int Counter = 0;
121 if ( Gia_ObjIsCi(pNode) )
122 return 0;
123 assert( Gia_ObjIsAnd(pNode) );
124 pFanin = Gia_ObjFanin0(pNode);
125 assert( Gia_ObjRefNum(p, pFanin) > 0 );
126 if ( Gia_ObjRefDec(p, pFanin) == 0 )
127 Counter += Gia_NodeDeref_rec( p, pFanin );
128 pFanin = Gia_ObjFanin1(pNode);
129 assert( Gia_ObjRefNum(p, pFanin) > 0 );
130 if ( Gia_ObjRefDec(p, pFanin) == 0 )
131 Counter += Gia_NodeDeref_rec( p, pFanin );
132 return Counter + 1;
133}
134static inline int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
135{
136 Gia_Obj_t * pFanin;
137 int Counter = 0;
138 if ( Gia_ObjIsCi(pNode) )
139 return 0;
140 assert( Gia_ObjIsAnd(pNode) );
141 pFanin = Gia_ObjFanin0(pNode);
142 if ( Gia_ObjRefInc(p, pFanin) == 0 )
143 Counter += Gia_NodeRef_rec( p, pFanin );
144 pFanin = Gia_ObjFanin1(pNode);
145 if ( Gia_ObjRefInc(p, pFanin) == 0 )
146 Counter += Gia_NodeRef_rec( p, pFanin );
147 return Counter + 1;
148}
149static inline void Gia_NodeCollect_rec( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp, Vec_Int_t * vSuppRefs )
150{
151 if ( Gia_ObjIsTravIdCurrent(p, pNode) )
152 return;
153 Gia_ObjSetTravIdCurrent(p, pNode);
154 if ( Gia_ObjRefNum(p, pNode) || Gia_ObjIsCi(pNode) )
155 {
156 Vec_IntPush( vSupp, Gia_ObjId(p, pNode) );
157 Vec_IntPush( vSuppRefs, Gia_ObjRefNum(p, pNode) );
158 return;
159 }
160 assert( Gia_ObjIsAnd(pNode) );
161 Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp, vSuppRefs );
162 Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp, vSuppRefs );
163}
164static inline int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp, Vec_Int_t * vSuppRefs )
165{
166 int ConeSize1, ConeSize2, i, iObj;
167 assert( !Gia_IsComplement(pNode) );
168 assert( Gia_ObjIsAnd(pNode) );
169 Vec_IntClear( vSupp );
170 Vec_IntClear( vSuppRefs );
172 ConeSize1 = Gia_NodeDeref_rec( p, pNode );
173 Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp, vSuppRefs );
174 Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp, vSuppRefs );
175 ConeSize2 = Gia_NodeRef_rec( p, pNode );
176 assert( ConeSize1 == ConeSize2 );
177 assert( ConeSize1 >= 0 );
178 // record supp refs
179 Vec_IntForEachEntry( vSupp, iObj, i )
180 Vec_IntAddToEntry( vSuppRefs, i, -Gia_ObjRefNumId(p, iObj) );
181 return ConeSize1;
182}
183
196{
197 if ( Gia_ObjIsTravIdCurrent(p, pNode) )
198 return pNode->Value;
199 Gia_ObjSetTravIdCurrent(p, pNode);
200 assert( Gia_ObjIsAnd(pNode) );
201 Gia_ManDomDerive_rec( pNew, p, Gia_ObjFanin0(pNode) );
202 Gia_ManDomDerive_rec( pNew, p, Gia_ObjFanin1(pNode) );
203 return pNode->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pNode), Gia_ObjFanin1Copy(pNode) );
204}
205Gia_Man_t * Gia_ManDomDerive( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vSupp, int nVars )
206{
207 Gia_Man_t * pNew, * pTemp;
208 int nMints = 1 << nVars;
209 int i, m, iResLit;
210 assert( nVars >= 0 && nVars <= 5 );
211 pNew = Gia_ManStart( Gia_ManObjNum(p) );
212 pNew->pName = Abc_UtilStrsav( p->pName );
213 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
214 Gia_ManConst0(p)->Value = 0;
215 Gia_ManHashAlloc( pNew );
216 for ( i = 0; i < Vec_IntSize(vSupp); i++ )
217 Gia_ManAppendCi(pNew);
218 for ( m = 0; m < nMints; m++ )
219 {
220 Gia_Obj_t * pObj;
222 Gia_ManForEachObjVec( vSupp, p, pObj, i )
223 {
224 if ( i < nVars )
225 pObj->Value = (m >> i) & 1;
226 else
227 pObj->Value = Gia_ObjToLit(pNew, Gia_ManCi(pNew, i));
228 Gia_ObjSetTravIdCurrent( p, pObj );
229 }
230 iResLit = Gia_ManDomDerive_rec( pNew, p, pRoot );
231 Gia_ManAppendCo( pNew, iResLit );
232 }
233 Gia_ManHashStop( pNew );
234 pNew = Gia_ManCleanup( pTemp = pNew );
235 Gia_ManStop( pTemp );
236 return pNew;
237}
238
251{
252 extern void Gia_ManCollapseTestTest( Gia_Man_t * p );
253
254 Vec_Int_t * vSupp, * vSuppRefs;
255 Gia_Man_t * pNew;
256 Gia_Obj_t * pObj;
257 int i, nSize, Entry, k;
258 abctime clk = Abc_Clock();
259 ABC_FREE( p->pRefs );
262 Gia_ManComputeDoms( p );
263 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
264 vSupp = Vec_IntAlloc( 1000 );
265 vSuppRefs = Vec_IntAlloc( 1000 );
266 Gia_ManForEachObj( p, pObj, i )
267 {
268 if ( !Gia_ObjIsAnd(pObj) && !Gia_ObjIsCo(pObj) )
269 continue;
270 if ( Gia_ObjDom(p, pObj) != i )
271 continue;
272 if ( Gia_ObjIsCo(pObj) )
273 pObj = Gia_ObjFanin0(pObj);
274 if ( !Gia_ObjIsAnd(pObj) )
275 continue;
276 nSize = Gia_NodeMffcSizeSupp( p, pObj, vSupp, vSuppRefs );
277 if ( nSize < 10 )//|| nSize > 100 )
278 continue;
279 // sort by cost
280 Vec_IntSelectSortCost2( Vec_IntArray(vSupp), Vec_IntSize(vSupp), Vec_IntArray(vSuppRefs) );
281
282 printf( "Obj %6d : ", i );
283 printf( "Cone = %4d ", nSize );
284 printf( "Supp = %4d ", Vec_IntSize(vSupp) );
285// Vec_IntForEachEntry( vSuppRefs, Entry, k )
286// printf( "%d(%d) ", -Entry, Gia_ObjLevelId(p, Vec_IntEntry(vSupp, k)) );
287 printf( "\n" );
288
289 // selected k
290 for ( k = 0; k < Vec_IntSize(vSupp); k++ )
291 if ( Vec_IntEntry(vSuppRefs, k) == 1 )
292 break;
293 k = Abc_MinInt( k, 3 );
294 k = 0;
295
296 // dump
297 pNew = Gia_ManDomDerive( p, pObj, vSupp, k );
298 Gia_DumpAiger( pNew, "mffc", i, 6 );
299 Gia_ManCollapseTestTest( pNew );
300
301 Gia_ManStop( pNew );
302 }
303 Vec_IntFree( vSuppRefs );
304 Vec_IntFree( vSupp );
305}
306
310
311
313
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
Gia_Man_t * Gia_ManDomDerive(Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vSupp, int nVars)
Definition giaMffc.c:205
void Gia_ManComputeDomsTry(Gia_Man_t *p)
Definition giaMffc.c:250
int Gia_ManDomDerive_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pNode)
Definition giaMffc.c:195
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
int Gia_NodeMffcSizeSupp(Gia_Man_t *p, Gia_Obj_t *pNode, Vec_Int_t *vSupp)
Definition giaUtil.c:1279
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
#define Gia_ManForEachObjReverse(p, pObj, i)
Definition gia.h:1206
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
void Gia_DumpAiger(Gia_Man_t *p, char *pFilePrefix, int iFileNum, int nFileNumDigits)
Definition giaAiger.c:1611
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
char * pSpec
Definition gia.h:100
char * pName
Definition gia.h:99
unsigned Value
Definition gia.h:89
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54